Sign.hs revision 03136b84a0c70d877e227444f0875e209506b9e4
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederDescription : CASL signatures (serve as local environments for the basic static analysis)
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederMaintainer : Christian.Maeder@dfki.de
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederStability : provisional
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederCASL signatures (serve as local environments for the basic static analysis)
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-}
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedermodule CASL.Sign where
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederimport CASL.AS_Basic_CASL
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport CASL.ToDoc ()
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederimport qualified Data.Map as Map
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport qualified Data.Set as Set
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport qualified Common.Lib.Rel as Rel
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport qualified Common.Lib.State as State
f353be6210f67ffd4a46967bba749afc968cee52Christian Maederimport Common.Keywords
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport Common.Id
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport Common.Result
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport Common.AS_Annotation
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport Common.GlobalAnnotations
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport Common.Doc
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederimport Common.DocUtils
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport Data.List (isPrefixOf)
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- constants have empty argument lists
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SORT], opRes :: SORT}
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder deriving (Show, Eq, Ord)
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maedertype OpMap = Map.Map Id (Set.Set OpType)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederdata SymbType = OpAsItemType OpType
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder -- since symbols do not speak about totality, the totality
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- information in OpType has to be ignored
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder | PredAsItemType PredType
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder | SortAsItemType
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder deriving (Show)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- Ordering and equality of symbol types has to ingore totality information
04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance Ord SymbType where
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder compare (OpAsItemType ot1) (OpAsItemType ot2) =
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder compare (opArgs ot1,opRes ot1) (opArgs ot2,opRes ot2)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder compare (OpAsItemType _) _ = LT
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder compare (PredAsItemType pt1) (PredAsItemType pt2) =
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder compare pt1 pt2
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder compare (PredAsItemType _) (OpAsItemType _) = GT
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder compare (PredAsItemType _) SortAsItemType = LT
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder compare SortAsItemType SortAsItemType = EQ
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder compare SortAsItemType _ = GT
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Eq SymbType where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder t1 == t2 = compare t1 t2 == EQ
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbType}
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder deriving (Show, Eq, Ord)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance PosItem Symbol where
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder getRange = getRange . symName
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToSortSymbol :: Id -> Symbol
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederidToSortSymbol idt = Symbol idt SortAsItemType
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian MaederidToOpSymbol :: Id -> OpType -> Symbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToPredSymbol :: Id -> PredType -> Symbol
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdata Sign f e = Sign
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder { sortSet :: Set.Set SORT
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , sortRel :: Rel.Rel SORT
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski , opMap :: OpMap
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , assocOps :: OpMap
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , predMap :: Map.Map Id (Set.Set PredType)
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder , varMap :: Map.Map SIMPLE_ID SORT
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , sentences :: [Named (FORMULA f)]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , declaredSymbols :: Set.Set Symbol
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , envDiags :: [Diagnosis]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , annoMap :: Map.Map Symbol (Set.Set Annotation)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , globAnnos :: GlobalAnnos
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , extendedInfo :: e
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder } deriving Show
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- better ignore assoc flags for equality
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederinstance (Eq f, Eq e) => Eq (Sign f e) where
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder e1 == e2 =
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder sortSet e1 == sortSet e2 &&
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder sortRel e1 == sortRel e2 &&
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder opMap e1 == opMap e2 &&
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder predMap e1 == predMap e2 &&
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder extendedInfo e1 == extendedInfo e2
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederemptySign :: e -> Sign f e
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederemptySign e = Sign
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder { sortSet = Set.empty
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , sortRel = Rel.empty
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , opMap = Map.empty
d48085f765fca838c1d972d2123601997174583dChristian Maeder , assocOps = Map.empty
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , predMap = Map.empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , varMap = Map.empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , sentences = []
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , declaredSymbols = Set.empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , envDiags = []
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , annoMap = Map.empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , globAnnos = emptyGlobalAnnos
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , extendedInfo = e }
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- | proper subsorts (possibly excluding input sort)
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedersubsortsOf :: SORT -> Sign f e -> Set.Set SORT
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersubsortsOf s e = Rel.predecessors (sortRel e) s
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-- | proper supersorts (possibly excluding input sort)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersupersortsOf :: SORT -> Sign f e -> Set.Set SORT
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersupersortsOf s e = Rel.succs (sortRel e) s
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedertoOP_TYPE :: OpType -> OP_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Op_type k args res nullRange
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPRED_TYPE :: PredType -> PRED_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoOpType :: OP_TYPE -> OpType
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedertoOpType (Op_type k args r _) = OpType k args r
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPredType :: PRED_TYPE -> PredType
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPredType (Pred_type args _) = PredType args
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinstance Pretty OpType where
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder pretty = pretty . toOP_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance Pretty PredType where
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder pretty = pretty . toPRED_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederinstance (Pretty f, Pretty e) => Pretty (Sign f e) where
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder pretty = printSign pretty pretty
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederinstance Pretty Symbol where
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder pretty sy = pretty (symName sy) <>
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder case symbType sy of
6a546f84de613989a2a7a708d310915c7bc3fbddChristian Maeder SortAsItemType -> empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder st -> space <> colon <> pretty st
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederinstance Pretty SymbType where
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder pretty st = case st of
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder OpAsItemType ot -> pretty ot
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder PredAsItemType pt -> space <> pretty pt
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder SortAsItemType -> empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederprintSign :: (f -> Doc) -> (e -> Doc) -> Sign f e -> Doc
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederprintSign _ fE s =
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder (if Set.null (sortSet s) then empty else text (sortS++sS) <+>
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder sepByCommas (map idDoc (Set.toList $ sortSet s))) $+$
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder (if Rel.null (sortRel s) then empty
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder else text (sortS++sS) <+>
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (fsep $ punctuate semi $ map printRel $ Map.toList
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder $ Rel.toMap $ Rel.transpose $ sortRel s))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $+$ printSetMap (text opS) empty (opMap s)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $+$ printSetMap (text predS) space (predMap s)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $+$ fE (extendedInfo s)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder where printRel (supersort, subsorts) =
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder ppWithCommas (Set.toList subsorts) <+> text lessS <+>
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder idDoc supersort
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- working with Sign
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
20fe556546c9277cf017931a07d90add61f199d9Christian MaederdiffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederdiffSig dif a b = a
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder { sortSet = sortSet a `Set.difference` sortSet b
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder , sortRel = Rel.transClosure $ Rel.difference (sortRel a) $ sortRel b
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , opMap = opMap a `diffMapSet` opMap b
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , assocOps = assocOps a `diffMapSet` assocOps b
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , predMap = predMap a `diffMapSet` predMap b
c9b711a46e5138b2742727817c8071960e673073Christian Maeder , annoMap = annoMap a `diffMapSet` annoMap b
c9b711a46e5138b2742727817c8071960e673073Christian Maeder , extendedInfo = dif (extendedInfo a) $ extendedInfo b }
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- transClosure needed: {a < b < c} - {a < c; b}
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- is not transitive!
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederdiffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder -> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
59c036af82aff7fbe074455dad50477b7878e2d8Christian MaederdiffMapSet =
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Map.differenceWith ( \ s t -> let d = Set.difference s t in
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder if Set.null d then Nothing
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder else Just d )
59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederaddMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
-> Map.Map a (Set.Set b)
addMapSet = Map.unionWith Set.union
addOpMapSet :: OpMap -> OpMap -> OpMap
addOpMapSet m = remPartOpsM . addMapSet m
addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig ad a b = a
{ sortSet = sortSet a `Set.union` sortSet b
, sortRel = Rel.transClosure $ Rel.union (sortRel a) $ sortRel b
, opMap = addOpMapSet (opMap a) $ opMap b
, assocOps = addOpMapSet (assocOps a) $ assocOps b
, predMap = addMapSet (predMap a) $ predMap b
, annoMap = addMapSet (annoMap a) $ annoMap b
, extendedInfo = ad (extendedInfo a) $ extendedInfo b }
isEmptySig :: (e -> Bool) -> Sign f e -> Bool
isEmptySig ie s =
Set.null (sortSet s) &&
Rel.null (sortRel s) &&
Map.null (opMap s) &&
Map.null (predMap s) && ie (extendedInfo s)
isSubMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
-> Bool
isSubMapSet = Map.isSubmapOfBy Set.isSubsetOf
isSubOpMap :: OpMap -> OpMap -> Bool
isSubOpMap = Map.isSubmapOfBy $ \ s t ->
Set.fold ( \ e r -> r && (Set.member e t || case opKind e of
Partial -> Set.member e {opKind = Total} t
Total -> False)) True s
isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig isSubExt a b = Set.isSubsetOf (sortSet a) (sortSet b)
&& Rel.isSubrelOf (sortRel a) (sortRel b)
&& isSubOpMap (opMap a) (opMap b)
-- ignore associativity properties!
&& isSubMapSet (predMap a) (predMap b)
&& isSubExt (extendedInfo a) (extendedInfo b)
partOps :: Set.Set OpType -> [OpType]
partOps s = map ( \ t -> t { opKind = Partial } )
$ Set.toList $ Set.filter ((== Total) . opKind) s
remPartOps :: Set.Set OpType -> Set.Set OpType
remPartOps s = foldr Set.delete s $ partOps s
remPartOpsM :: Ord a => Map.Map a (Set.Set OpType)
-> Map.Map a (Set.Set OpType)
remPartOpsM = Map.map remPartOps
addDiags :: [Diagnosis] -> State.State (Sign f e) ()
addDiags ds =
do e <- State.get
State.put e { envDiags = reverse ds ++ envDiags e }
addAnnoSet :: Annoted a -> Symbol -> State.State (Sign f e) ()
addAnnoSet a s = let v = Set.union (Set.fromList $ l_annos a)
$ Set.fromList $ r_annos a
in if Set.null v then return () else do
e <- State.get
State.put e { annoMap = Map.insertWith (Set.union) s v $ annoMap e }
addSort :: Annoted a -> SORT -> State.State (Sign f e) ()
addSort a s =
do e <- State.get
let m = sortSet e
if Set.member s m then
addDiags [mkDiag Hint "redeclared sort" s]
else do State.put e { sortSet = Set.insert s m }
addDiags $ checkNamePrefix s
addAnnoSet a $ Symbol s SortAsItemType
hasSort :: Sign f e -> SORT -> [Diagnosis]
hasSort e s = if Set.member s $ sortSet e then []
else [mkDiag Error "unknown sort" s]
checkSorts :: [SORT] -> State.State (Sign f e) ()
checkSorts s =
do e <- State.get
addDiags $ concatMap (hasSort e) s
addSubsort :: SORT -> SORT -> State.State (Sign f e) ()
addSubsort = addSubsortOrIso True
addSubsortOrIso :: Bool -> SORT -> SORT -> State.State (Sign f e) ()
addSubsortOrIso b super sub =
do if b then checkSorts [super, sub] else return ()
e <- State.get
let r = sortRel e
State.put e { sortRel = (if b then id else
Rel.insert super sub) $ Rel.insert sub super r }
let p = posOfId sub
rel = " '" ++ showDoc sub (if b then " < "
else " = ") ++ showDoc super "'"
if super == sub then
addDiags [mkDiag Warning
"void reflexive subsort" sub]
else if b then
if Rel.path super sub r then
if Rel.path sub super r then
addDiags [Diag Warning
("sorts are isomorphic" ++ rel) p]
else addDiags [Diag Warning
("added subsort cycle by" ++ rel) p]
else if Rel.path sub super r then
addDiags [Diag Hint ("redeclared subsort" ++ rel) p]
else return ()
else if Rel.path super sub r then
if Rel.path sub super r then
addDiags [Diag Hint
("redeclared isomoprhic sorts" ++ rel) p]
else addDiags [Diag Warning
("subsort '" ++ showDoc super
"' made isomorphic by" ++ rel)
$ posOfId super]
else if Rel.path sub super r then
addDiags [Diag Warning
("subsort '" ++ showDoc sub
"' made isomorphic by" ++ rel) p]
else return()
closeSubsortRel :: State.State (Sign f e) ()
closeSubsortRel=
do e <- State.get
State.put e { sortRel = Rel.transClosure $ sortRel e }
checkNamePrefix :: Id -> [Diagnosis]
checkNamePrefix i = if isPrefixOf genNamePrefix $ showId i "" then
[mkDiag Warning "identifier may conflict with generated names" i]
else []
alsoWarning :: String -> String -> Id -> [Diagnosis]
alsoWarning new old i = let is = ' ' : showId i "'" in
[Diag Warning ("new '" ++ new ++ is ++ " is also known as '" ++ old ++ is)
$ posOfId i]
checkWithOtherMap :: String -> String -> Map.Map Id a -> Id -> [Diagnosis]
checkWithOtherMap s1 s2 m i =
case Map.lookup i m of
Nothing -> []
Just _ -> alsoWarning s1 s2 i
addVars :: VAR_DECL -> State.State (Sign f e) ()
addVars (Var_decl vs s _) = do
checkSorts [s]
mapM_ (addVar s) vs
addVar :: SORT -> SIMPLE_ID -> State.State (Sign f e) ()
addVar s v =
do e <- State.get
let m = varMap e
i = simpleIdToId v
ds = case Map.lookup v m of
Just _ -> [mkDiag Hint "known variable shadowed" v]
Nothing -> []
State.put e { varMap = Map.insert v s m }
addDiags $ ds ++ checkWithOtherMap varS opS (opMap e) i
++ checkWithOtherMap varS predS (predMap e) i
++ checkNamePrefix i
addOpTo :: Id -> OpType -> OpMap -> OpMap
addOpTo k v m =
let l = Map.findWithDefault Set.empty k m
n = Map.insert k (Set.insert v l) m
in case opKind v of
Total -> let vp = v { opKind = Partial } in
if Set.member vp l then
Map.insert k (Set.insert v $ Set.delete vp l) m
else n
_ -> if Set.member v { opKind = Total } l then m
else n