Sign.hs revision 03136b84a0c70d877e227444f0875e209506b9e4
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
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederMaintainer : Christian.Maeder@dfki.de
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederStability : provisional
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : portable
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederCASL signatures (serve as local environments for the basic static analysis)
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
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport Data.List (isPrefixOf)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- constants have empty argument lists
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SORT], opRes :: SORT}
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder deriving (Show, Eq, Ord)
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)
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
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Eq SymbType where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder t1 == t2 = compare t1 t2 == EQ
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbType}
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder deriving (Show, Eq, Ord)
04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance PosItem Symbol where
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder getRange = getRange . symName
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToSortSymbol :: Id -> Symbol
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederidToSortSymbol idt = Symbol idt SortAsItemType
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian MaederidToOpSymbol :: Id -> OpType -> Symbol
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToPredSymbol :: Id -> PredType -> Symbol
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)
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
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
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- better ignore assoc flags for equality
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederinstance (Eq f, Eq e) => Eq (Sign f e) where
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 MaederemptySign :: e -> Sign f e
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederemptySign e = Sign
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , sentences = []
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , declaredSymbols = Set.empty
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , envDiags = []
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , globAnnos = emptyGlobalAnnos
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , extendedInfo = e }
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
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 MaedertoOP_TYPE :: OpType -> OP_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Op_type k args res nullRange
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPRED_TYPE :: PredType -> PRED_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoOpType :: OP_TYPE -> OpType
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedertoOpType (Op_type k args r _) = OpType k args r
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPredType :: PRED_TYPE -> PredType
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedertoPredType (Pred_type args _) = PredType args
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinstance Pretty OpType where
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder pretty = pretty . toOP_TYPE
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance Pretty PredType where
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder pretty = pretty . toPRED_TYPE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maederinstance (Pretty f, Pretty e) => Pretty (Sign f e) where
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder pretty = printSign pretty pretty
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
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
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
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
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- working with Sign
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 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)
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 )
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederaddMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
{ sortSet = sortSet a `Set.union` sortSet b
Set.null (sortSet s) &&
Rel.null (sortRel s) &&
Map.null (opMap s) &&
Map.null (predMap s) && ie (extendedInfo s)
isSubOpMap = Map.isSubmapOfBy $ \ s t ->
Partial -> Set.member e {opKind = Total} t
isSubSig isSubExt a b = Set.isSubsetOf (sortSet a) (sortSet b)
&& Rel.isSubrelOf (sortRel a) (sortRel b)
partOps :: Set.Set OpType -> [OpType]
remPartOps s = foldr Set.delete s $ partOps s
remPartOpsM = Map.map remPartOps
addDiags :: [Diagnosis] -> State.State (Sign f e) ()
do e <- State.get
State.put e { envDiags = reverse ds ++ envDiags e }
addAnnoSet :: Annoted a -> Symbol -> State.State (Sign f e) ()
$ Set.fromList $ r_annos a
in if Set.null v then return () else do
e <- State.get
addSort :: Annoted a -> SORT -> State.State (Sign f e) ()
do e <- State.get
if Set.member s m then
hasSort e s = if Set.member s $ sortSet e then []
checkSorts :: [SORT] -> State.State (Sign f e) ()
do e <- State.get
addSubsort :: SORT -> SORT -> State.State (Sign f e) ()
addSubsortOrIso :: Bool -> SORT -> SORT -> State.State (Sign f e) ()
e <- State.get
State.put e { sortRel = (if b then id else
if Rel.path super sub r then
if Rel.path sub super r then
else if Rel.path sub super r then
else if Rel.path super sub r then
if Rel.path sub super r then
else if Rel.path sub super r then
closeSubsortRel :: State.State (Sign f e) ()
do e <- State.get
checkWithOtherMap :: String -> String -> Map.Map Id a -> Id -> [Diagnosis]
case Map.lookup i m of
addVars :: VAR_DECL -> State.State (Sign f e) ()
addVar :: SORT -> SIMPLE_ID -> State.State (Sign f e) ()
do e <- State.get
ds = case Map.lookup v m of
if Set.member vp l then
_ -> if Set.member v { opKind = Total } l then m