4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

5ba323da9f037264b4a356085e844889aedeac23Christian MaederModule : $Header$

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2004

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : maeder@tzi.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederCASL signature

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maedermodule CASL.Sign where

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CASL.AS_Basic_CASL

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport CASL.Print_AS_Basic()

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Common.Lib.Map as Map

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Set as Set

af621d0066770895fd79562728e93099c8c52060Christian Maederimport qualified Common.Lib.Rel as Rel

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Common.PrettyPrint

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.PPUtils

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Common.Lib.Pretty

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Common.Lib.State

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Common.Keywords

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Id

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport Common.Result

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport Common.AS_Annotation

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport Common.GlobalAnnotations

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder-- constants have empty argument lists

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SORT], opRes :: SORT}

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder deriving (Show, Eq, Ord)

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederdata PredType = PredType {predArgs :: [SORT]} deriving (Show, Eq, Ord)

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maedertype OpMap = Map.Map Id (Set.Set OpType)

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederdata Sign f e = Sign { sortSet :: !(Set.Set SORT)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sortRel :: !(Rel.Rel SORT)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , opMap :: !OpMap

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , assocOps :: !OpMap

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , predMap :: !(Map.Map Id (Set.Set PredType))

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , varMap :: !(Map.Map SIMPLE_ID SORT)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sentences :: ![Named (FORMULA f)]

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , envDiags :: ![Diagnosis]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , extendedInfo :: !e

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder } deriving Show

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- better ignore assoc flags for equality

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederinstance (Eq f, Eq e) => Eq (Sign f e) where

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder e1 == e2 =

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder sortSet e1 == sortSet e2 &&

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder sortRel e1 == sortRel e2 &&

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder opMap e1 == opMap e2 &&

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder predMap e1 == predMap e2 &&

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder extendedInfo e1 == extendedInfo e2

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederemptySign :: e -> Sign f e

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederemptySign e = Sign { sortSet = Set.empty

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sortRel = Rel.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , opMap = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , assocOps = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , predMap = Map.empty

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , varMap = Map.empty

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , sentences = []

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder , envDiags = []

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder , extendedInfo = e }

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder-- | proper subsorts (possibly excluding input sort)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedersubsortsOf :: SORT -> Sign f e -> Set.Set SORT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersubsortsOf s e = Rel.predecessors (sortRel e) s

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | proper supersorts (possibly excluding input sort)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersupersortsOf :: SORT -> Sign f e -> Set.Set SORT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersupersortsOf s e = Rel.succs (sortRel e) s

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertoOP_TYPE :: OpType -> OP_TYPE

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertoOP_TYPE OpType { opArgs = args, opRes = res, opKind = k } =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Op_type k args res nullRange

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertoPRED_TYPE :: PredType -> PRED_TYPE

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaedertoPRED_TYPE PredType { predArgs = args } = Pred_type args nullRange

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertoOpType :: OP_TYPE -> OpType

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertoOpType (Op_type k args r _) = OpType k args r

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaedertoPredType :: PRED_TYPE -> PredType

986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian MaedertoPredType (Pred_type args _) = PredType args

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maederinstance PrettyPrint OpType where

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder printText0 ga ot = printText0 ga $ toOP_TYPE ot

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederinstance PrettyPrint PredType where

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder printText0 ga pt = printText0 ga $ toPRED_TYPE pt

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maederinstance (PrettyPrint f, PrettyPrint e) => PrettyPrint (Sign f e) where

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder printText0 ga s =

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder ptext (sortS++sS) <+> commaT_text ga (Set.toList $ sortSet s)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder $$

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder (if Rel.null (sortRel s) then empty

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder else ptext (sortS++sS) <+>

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (fsep . punctuate semi $ map printRel $ Map.toList

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder $ Rel.toMap $ Rel.transpose $ sortRel s))

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $$ printSetMap (ptext opS) empty ga (opMap s)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder $$ printSetMap (ptext predS) space ga (predMap s)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder $$ printText0 ga (extendedInfo s)

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder where printRel (supersort, subsorts) =

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder printSet ga subsorts <+> ptext lessS <+> printText0 ga supersort

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederprintSetMap :: (PrettyPrint k, PrettyPrint a, Ord k, Ord a) => Doc

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder -> Doc -> GlobalAnnos -> Map.Map k (Set.Set a) -> Doc

31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederprintSetMap header sepa ga m =

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder vcat $ map (\ (i, t) ->

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder header <+>

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder printText0 ga i <+> colon <> sepa <>

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder printText0 ga t)

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder $ concatMap (\ (o, ts) ->

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder map ( \ ty -> (o, ty) ) $ Set.toList ts)

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder $ Map.toList m

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder-- working with Sign

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaederdiffSig :: Sign f e -> Sign f e -> Sign f e

ad187062b0009820118c1b773a232e29b879a2faChristian MaederdiffSig a b =

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder a { sortSet = sortSet a `Set.difference` sortSet b

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , sortRel = Rel.transClosure $ Rel.difference (sortRel a) $ sortRel b

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , opMap = opMap a `diffMapSet` opMap b

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , assocOps = assocOps a `diffMapSet` assocOps b

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , predMap = predMap a `diffMapSet` predMap b

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder }

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder -- transClosure needed: {a < b < c} - {a < c; b}

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder -- is not transitive!

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederdiffMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederdiffMapSet =

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Map.differenceWith ( \ s t -> let d = Set.difference s t in

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder if Set.null d then Nothing

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder else Just d )

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederaddMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder -> Map.Map a (Set.Set b)

8485da94b57d8b5135ee685b55c982b037ed4140Christian MaederaddMapSet = Map.unionWith Set.union

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederaddOpMapSet :: OpMap -> OpMap -> OpMap

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederaddOpMapSet m = remPartOpsM . addMapSet m

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian MaederaddSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederaddSig ad a b =

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder a { sortSet = sortSet a `Set.union` sortSet b

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , sortRel = Rel.transClosure $ Rel.union (sortRel a) $ sortRel b

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , opMap = addOpMapSet (opMap a) $ opMap b

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder , assocOps = addOpMapSet (assocOps a) $ assocOps b

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder , predMap = addMapSet (predMap a) $ predMap b

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder , extendedInfo = ad (extendedInfo a) $ extendedInfo b

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder }

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederisEmptySig :: (e -> Bool) -> Sign f e -> Bool

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederisEmptySig ie s =

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Set.null (sortSet s) &&

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Rel.null (sortRel s) &&

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Map.null (opMap s) &&

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Map.null (predMap s) && ie (extendedInfo s)

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisSubMapSet :: (Ord a, Ord b) => Map.Map a (Set.Set b) -> Map.Map a (Set.Set b)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder -> Bool

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederisSubMapSet = Map.isSubmapOfBy Set.isSubsetOf

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederisSubOpMap :: OpMap -> OpMap -> Bool

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederisSubOpMap a b = Map.isSubmapOfBy ( \ s t ->

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Set.fold ( \ e r -> r && (Set.member e t || case opKind e of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Partial -> Set.member e {opKind = Total} t

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Total -> False)) True s) a b

f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian MaederisSubSig :: (PrettyPrint e, PrettyPrint f) =>

fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisSubSig isSubExt a b =

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Set.isSubsetOf (sortSet a) (sortSet b)

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder && Rel.isSubrelOf (sortRel a) (sortRel b)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder && isSubOpMap (opMap a) (opMap b)

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder -- ignore associativity properties!

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder && isSubMapSet (predMap a) (predMap b)

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder && isSubExt (extendedInfo a) (extendedInfo b)

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederpartOps :: Set.Set OpType -> [OpType]

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian MaederpartOps s = map ( \ t -> t { opKind = Partial } )

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder $ Set.toList $ Set.filter ((==Total) . opKind) s

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian MaederremPartOps :: Set.Set OpType -> Set.Set OpType

021d7137df04ec1834911d99d90243a092841cedChristian MaederremPartOps s = foldr Set.delete s $ partOps s

021d7137df04ec1834911d99d90243a092841cedChristian Maeder

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian MaederremPartOpsM :: Ord a => Map.Map a (Set.Set OpType)

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder -> Map.Map a (Set.Set OpType)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederremPartOpsM = Map.map remPartOps

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederaddDiags :: [Diagnosis] -> State (Sign f e) ()

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian MaederaddDiags ds =

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder do e <- get

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder put e { envDiags = reverse ds ++ envDiags e }

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederaddSort :: SORT -> State (Sign f e) ()

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederaddSort s =

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder do e <- get

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let m = sortSet e

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder if Set.member s m then

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder addDiags [mkDiag Hint "redeclared sort" s]

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder else put e { sortSet = Set.insert s m }

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder

908a6351595b57641353608c4449d5faa0d1adf8Christian MaederhasSort :: Sign f e -> SORT -> [Diagnosis]

bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian MaederhasSort e s = if Set.member s $ sortSet e then []

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder else [mkDiag Error "unknown sort" s]

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaedercheckSorts :: [SORT] -> State (Sign f e) ()

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercheckSorts s =

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder do e <- get

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder addDiags $ concatMap (hasSort e) s

addSubsort :: SORT -> SORT -> State (Sign f e) ()

addSubsort = addSubsortOrIso True

addSubsortOrIso :: Bool -> SORT -> SORT -> State (Sign f e) ()

addSubsortOrIso b super sub =

do if b then checkSorts [super, sub] else return ()

e <- get

let r = sortRel e

put e { sortRel = (if b then id else

Rel.insert super sub) $ Rel.insert sub super r }

let p = posOfId sub

rel = " '" ++ showPretty sub (if b then " < "

else " = ") ++ showPretty 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 '" ++ showPretty super

"' made isomorphic by" ++ rel)

$ posOfId super]

else if Rel.path sub super r then

addDiags [Diag Warning

("subsort '" ++ showPretty sub

"' made isomorphic by" ++ rel) p]

else return()

closeSubsortRel :: State (Sign f e) ()

closeSubsortRel=

do e <- get

put e { sortRel = Rel.transClosure $ sortRel e }

addVars :: VAR_DECL -> State (Sign f e) ()

addVars (Var_decl vs s _) = mapM_ (addVar s) vs

addVar :: SORT -> SIMPLE_ID -> State (Sign f e) ()

addVar s v =

do e <- get

let m = varMap e

case Map.lookup v m of

Just _ -> addDiags [mkDiag Warning "variable shadowed" v]

Nothing -> return ()

put e { varMap = Map.insert v s m }

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