Sign.hs revision 26d11a256b1433604a3dbc69913b520fff7586ac
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : maeder@tzi.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThis module provides CASL signatures that also serve as local
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski environments for the basic static analysis.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Rel as Rel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.State as State
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Data.List (isPrefixOf)
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski-- constants have empty argument lists
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SORT], opRes :: SORT}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederdata SymbType = OpAsItemType OpType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- since symbols do not speak about totality, the totality
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- information in OpType has to be ignored
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski | PredAsItemType PredType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski | SortAsItemType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Ordering and equality of symbol types has to ingore totality information
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Ord SymbType where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (OpAsItemType ot1) (OpAsItemType ot2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (opArgs ot1,opRes ot1) (opArgs ot2,opRes ot2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (OpAsItemType _) _ = LT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType pt1) (PredAsItemType pt2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare pt1 pt2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType _) (OpAsItemType _) = GT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType _) SortAsItemType = LT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder compare SortAsItemType SortAsItemType = EQ
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder compare SortAsItemType _ = GT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Eq SymbType where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski t1 == t2 = compare t1 t2 == EQ
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata Symbol = Symbol {symName :: Id, symbType :: SymbType}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Show, Eq, Ord)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance PosItem Symbol where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski getRange = getRange . symName
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata Sign f e = Sign { sortSet :: Set.Set SORT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , sortRel :: Rel.Rel SORT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , opMap :: OpMap
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , assocOps :: OpMap
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , varMap :: Map.Map SIMPLE_ID SORT
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , sentences :: [Named (FORMULA f)]
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , envDiags :: [Diagnosis]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , globAnnos :: GlobalAnnos
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , extendedInfo :: e
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder } deriving Show
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- better ignore assoc flags for equality
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maederinstance (Eq f, Eq e) => Eq (Sign f e) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sortSet e1 == sortSet e2 &&
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sortRel e1 == sortRel e2 &&
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder opMap e1 == opMap e2 &&
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder predMap e1 == predMap e2 &&
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder extendedInfo e1 == extendedInfo e2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederemptySign :: e -> Sign f e
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederemptySign e = Sign { sortSet = Set.empty
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , sentences = []
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , envDiags = []
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , globAnnos = emptyGlobalAnnos
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , extendedInfo = e }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | proper subsorts (possibly excluding input sort)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedersubsortsOf :: SORT -> Sign f e -> Set.Set SORT
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersubsortsOf s e = Rel.predecessors (sortRel e) s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | proper supersorts (possibly excluding input sort)
10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till MossakowskisupersortsOf :: SORT -> Sign f e -> Set.Set SORT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisupersortsOf s e = Rel.succs (sortRel e) s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitoOP_TYPE :: OpType -> OP_TYPE
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertoOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Op_type k args res nullRange
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedertoPRED_TYPE :: PredType -> PRED_TYPE
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedertoPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedertoOpType :: OP_TYPE -> OpType
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedertoOpType (Op_type k args r _) = OpType k args r
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedertoPredType :: PRED_TYPE -> PredType
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedertoPredType (Pred_type args _) = PredType args
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty OpType where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty = printOpType . toOP_TYPE
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Pretty PredType where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pretty = printPredType . toPRED_TYPE
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance (Pretty f, Pretty e) => Pretty (Sign f e) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty = printSign pretty pretty
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintSign :: (f -> Doc) -> (e -> Doc) -> Sign f e -> Doc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintSign _ fE s = text (sortS++sS) <+>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sepByCommas (map idDoc (Set.toList $ sortSet s)) $+$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (if Rel.null (sortRel s) then empty
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else text (sortS++sS) <+>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (fsep $ punctuate semi $ map printRel $ Map.toList
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ printSetMap (text opS) empty (opMap s)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ printSetMap (text predS) space (predMap s)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $+$ fE (extendedInfo s)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder where printRel (supersort, subsorts) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ppWithCommas (Set.toList subsorts) <+> text lessS <+>
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder idDoc supersort
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintSetMap :: (Pretty k,Pretty a,Ord a,Ord k) => Doc -> Doc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprintSetMap header sepa m = vcat $ map (\ (i, t) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty i <+> colon <> sepa <>
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski $ concatMap (\ (o, ts) ->
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder map ( \ ty -> (o, ty) ) $ Set.toList ts)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder-- working with Sign
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederdiffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederdiffSig dif a b =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder a { sortSet = sortSet a `Set.difference` sortSet b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , sortRel = Rel.transClosure $ Rel.difference (sortRel a) $ sortRel b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , opMap = opMap a `diffMapSet` opMap b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , assocOps = assocOps a `diffMapSet` assocOps b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , predMap = predMap a `diffMapSet` predMap b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , extendedInfo = dif (extendedInfo a) $ extendedInfo b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- transClosure needed: {a < b < c} - {a < c; b}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- is not transitive!
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskidiffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Map.differenceWith ( \ s t -> let d = Set.difference s t in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if Set.null d then Nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else Just d )
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiaddOpMapSet :: OpMap -> OpMap -> OpMap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddOpMapSet m = remPartOpsM . addMapSet m
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddSig ad a b =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski a { sortSet = sortSet a `Set.union` sortSet b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , sortRel = Rel.transClosure $ Rel.union (sortRel a) $ sortRel b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , opMap = addOpMapSet (opMap a) $ opMap b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , assocOps = addOpMapSet (assocOps a) $ assocOps b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , predMap = addMapSet (predMap a) $ predMap b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , extendedInfo = ad (extendedInfo a) $ extendedInfo b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisEmptySig :: (e -> Bool) -> Sign f e -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisEmptySig ie s =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Set.null (sortSet s) &&
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Rel.null (sortRel s) &&
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Map.null (predMap s) && ie (extendedInfo s)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisSubMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederisSubMapSet = Map.isSubmapOfBy Set.isSubsetOf
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederisSubOpMap :: OpMap -> OpMap -> Bool
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederisSubOpMap a b = Map.isSubmapOfBy ( \ s t ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Set.fold ( \ e r -> r && (Set.member e t || case opKind e of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Partial -> Set.member e {opKind = Total} t
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Total -> False)) True s) a b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederisSubSig isSubExt a b =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Set.isSubsetOf (sortSet a) (sortSet b)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski && Rel.isSubrelOf (sortRel a) (sortRel b)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder && isSubOpMap (opMap a) (opMap b)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- ignore associativity properties!
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder && isSubMapSet (predMap a) (predMap b)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder && isSubExt (extendedInfo a) (extendedInfo b)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederpartOps :: Set.Set OpType -> [OpType]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederpartOps s = map ( \ t -> t { opKind = Partial } )
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ Set.toList $ Set.filter ((==Total) . opKind) s
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederremPartOps :: Set.Set OpType -> Set.Set OpType
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederremPartOps s = foldr Set.delete s $ partOps s
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederremPartOpsM :: Ord a => Map.Map a (Set.Set OpType)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederremPartOpsM = Map.map remPartOps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederaddDiags :: [Diagnosis] -> State.State (Sign f e) ()
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder State.put e { envDiags = reverse ds ++ envDiags e }
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederaddSort :: SORT -> State.State (Sign f e) ()
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let m = sortSet e
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags [mkDiag Hint "redeclared sort" s]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else do State.put e { sortSet = Set.insert s m }
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags $ checkNamePrefix s
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederhasSort :: Sign f e -> SORT -> [Diagnosis]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederhasSort e s = if Set.member s $ sortSet e then []
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else [mkDiag Error "unknown sort" s]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedercheckSorts :: [SORT] -> State.State (Sign f e) ()
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedercheckSorts s =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags $ concatMap (hasSort e) s
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederaddSubsort :: SORT -> SORT -> State.State (Sign f e) ()
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederaddSubsort = addSubsortOrIso True
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederaddSubsortOrIso :: Bool -> SORT -> SORT -> State.State (Sign f e) ()
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederaddSubsortOrIso b super sub =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do if b then checkSorts [super, sub] else return ()
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let r = sortRel e
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder State.put e { sortRel = (if b then id else
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Rel.insert super sub) $ Rel.insert sub super r }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let p = posOfId sub
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rel = " '" ++ showDoc sub (if b then " < "
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else " = ") ++ showDoc super "'"
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder if super == sub then
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder addDiags [mkDiag Warning
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "void reflexive subsort" sub]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder else if b then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if Rel.path super sub r then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if Rel.path sub super r then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addDiags [Diag Warning
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("sorts are isomorphic" ++ rel) p]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else addDiags [Diag Warning
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("added subsort cycle by" ++ rel) p]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else if Rel.path sub super r then
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder addDiags [Diag Hint ("redeclared subsort" ++ rel) p]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else return ()
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else if Rel.path super sub r then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if Rel.path sub super r then
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder addDiags [Diag Hint
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ("redeclared isomoprhic sorts" ++ rel) p]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else addDiags [Diag Warning
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ("subsort '" ++ showDoc super
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder "' made isomorphic by" ++ rel)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ posOfId super]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else if Rel.path sub super r then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder addDiags [Diag Warning
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ("subsort '" ++ showDoc sub
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder "' made isomorphic by" ++ rel) p]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else return()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercloseSubsortRel :: State.State (Sign f e) ()
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedercloseSubsortRel=
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder State.put e { sortRel = Rel.transClosure $ sortRel e }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | a prefix for generated names
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergenNamePrefix :: String
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergenNamePrefix = "gn_"
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskicheckNamePrefix :: Id -> [Diagnosis]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedercheckNamePrefix i = if isPrefixOf genNamePrefix $ showId i "" then
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder [mkDiag Warning "identifier may conflict with generated names" i]
578b677874296e4ba48e57b5e4b4b0270d995603Christian MaederalsoWarning :: String -> Id -> [Diagnosis]
578b677874296e4ba48e57b5e4b4b0270d995603Christian MaederalsoWarning msg i = [mkDiag Warning ("also known as " ++ msg) i]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedercheckWithOtherMap :: String -> Map.Map Id a -> Id -> [Diagnosis]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedercheckWithOtherMap msg m i =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Nothing -> []
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Just _ -> alsoWarning msg i
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddVars :: VAR_DECL -> State.State (Sign f e) ()
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddVars (Var_decl vs s _) = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder checkSorts [s]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder mapM_ (addVar s) vs
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddVar :: SORT -> SIMPLE_ID -> State.State (Sign f e) ()
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let m = varMap e
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder i = simpleIdToId v
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder ds = case Map.lookup v m of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Just _ -> [mkDiag Hint "known variable shadowed" v]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Nothing -> []
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder addDiags $ ds ++ checkWithOtherMap "operation" (opMap e) i
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder ++ checkWithOtherMap "predicate" (predMap e) i
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder ++ checkNamePrefix i
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddOpTo :: Id -> OpType -> OpMap -> OpMap
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddOpTo k v m =
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in case opKind v of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Total -> let vp = v { opKind = Partial } in
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Map.insert k (Set.insert v $ Set.delete vp l) m
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski _ -> if Set.member v { opKind = Total } l then m