StaticAna.hs revision 18c1d987ce5818ecf0bfc8af3f43aed2ce86e1ea
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : maeder@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCASL static analysis for basic specifications
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederFollows Chaps. III:2 and III:3 of the CASL Reference Manual.
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport qualified Common.Lib.Map as Map
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Common.Lib.Set as Set
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maederimport qualified Common.Lib.Rel as Rel
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian MaedercheckPlaces :: [SORT] -> Id -> [Diagnosis]
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedercheckPlaces args i =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder if let n = placeCount i in n == 0 || n == length args then []
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder else [mkDiag Error "wrong number of places" i]
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian MaedercheckWithVars :: Map.Map SIMPLE_ID a -> Id -> [Diagnosis]
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian MaedercheckWithVars m i@(Id ts _ _) = if isSimpleId i then
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder case Map.lookup (head ts) m of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> []
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder Just _ -> alsoWarning "variable" i
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederaddOp :: OpType -> Id -> State (Sign f e) ()
05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder do checkSorts (opRes ty : opArgs ty)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder let m = opMap e
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder check = addDiags $ checkPlaces (opArgs ty) i
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder ++ checkWithOtherMap "predicate" (predMap e) i
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder ++ checkWithVars (varMap e) i
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder store = do put e { opMap = addOpTo i ty m }
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder addDiags [mkDiag Hint "redeclared op" i]
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder else case opKind ty of
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder Partial -> if Set.member ty {opKind = Total} l then
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder addDiags [mkDiag Warning "partially redeclared" i]
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder else store >> check
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Total -> do store
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder if Set.member ty {opKind = Partial} l then
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder addDiags [mkDiag Hint "redeclared as total" i]
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian MaederaddAssocOp :: OpType -> Id -> State (Sign f e) ()
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian MaederaddAssocOp ty i = do
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder put e { assocOps = addOpTo i ty $ assocOps e
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder , globAnnos = updAssocMap (addAssocId i) $ globAnnos e
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederupdateExtInfo :: (e -> Result e) -> State (Sign f e) ()
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaederupdateExtInfo upd = do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let re = upd $ extendedInfo s
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder case maybeResult re of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just e -> put s { extendedInfo = e }
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder addDiags $ diags re
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddPred :: PredType -> Id -> State (Sign f e) ()
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederaddPred ty i =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder do checkSorts $ predArgs ty
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let m = predMap e
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder addDiags [mkDiag Hint "redeclared pred" i]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder else do put e { predMap = Map.insert i (Set.insert ty l) m }
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder addDiags $ checkPlaces (predArgs ty) i
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder ++ checkWithOtherMap "operation" (opMap e) i
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder ++ checkWithVars (varMap e) i
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian MaederallOpIds :: Sign f e -> Set.Set Id
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaederallOpIds = Rel.keysSet . opMap
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian MaederaddAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
2d130d212db7208777ca896a7ecad619a8944971Christian MaederaddAssocs e = updAssocMap (\ m -> foldr addAssocId m $ Map.keys $ assocOps e)
2d130d212db7208777ca896a7ecad619a8944971Christian MaederupdAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
2d130d212db7208777ca896a7ecad619a8944971Christian MaederupdAssocMap f ga = ga { assoc_annos = f $ assoc_annos ga }
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian MaederaddAssocId :: Id -> AssocMap -> AssocMap
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian MaederaddAssocId i m = case Map.lookup i m of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Nothing -> Map.insert i ALeft m
a9b59eb2ce961014974276cdae0e9df4419bd212Christian MaederformulaIds :: Sign f e -> Set.Set Id
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederformulaIds e = let ops = allOpIds e in
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederallPredIds :: Sign f e -> Set.Set Id
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian MaederallPredIds = Rel.keysSet . predMap
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederaddSentences ds =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder put e { sentences = reverse ds ++ sentences e }
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- * traversing all data types of the abstract syntax
b568982efd0997d877286faa592d81b03c8c67b8Christian Maederana_BASIC_SPEC :: PrettyPrint f => Min f e
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> Ana b b s f e -> Ana s b s f e -> Mix b s f e -> GlobalAnnos
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederana_BASIC_SPEC mef ab anas mix ga (Basic_spec al) = fmap Basic_spec $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapAnM (ana_BASIC_ITEMS mef ab anas mix ga) al
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- looseness of a datatype
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermkForall :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermkForall vl f ps = if null vl then f else
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Quantification Universal vl f ps
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederunionGenAx :: [GenAx] -> GenAx
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederunionGenAx = foldr ( \ (s1, r1, f1) (s2, r2, f2) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Set.union f1 f2)) emptyGenAx
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_BASIC_ITEMS :: PrettyPrint f => Min f e -> Ana b b s f e -> Ana s b s f e
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Mix b s f e -> GlobalAnnos
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederana_BASIC_ITEMS mef ab anas mix ga bi =
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder Sig_items sis -> fmap Sig_items $
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder ana_SIG_ITEMS mef anas mix ga Loose sis
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Free_datatype al ps ->
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder mapM_ addSort sorts
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder mapAnM (ana_DATATYPE_DECL Free) al
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder toSortGenAx ps True $ getDataGenSig al
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder closeSubsortRel
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder Sort_gen al ps ->
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder do (gs,ul) <- ana_Generated mef anas mix ga al
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder toSortGenAx ps False $ unionGenAx gs
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder return $ Sort_gen ul ps
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Var_items il _ ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do mapM_ addVars il
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder Local_var_axioms il afs ps ->
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder do e <- get -- save
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder mapM_ addVars il
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder vds <- gets envDiags
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder put e { envDiags = vds } -- restore with shadowing warnings
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder let (es, resFs, anaFs) = foldr ( \ f (dss, ress, ranas) ->
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder let Result ds m = anaForm mef mix ga sign $ item f
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Nothing -> (ds ++ dss, ress, ranas)
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder Just (resF, anaF) ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (ds ++ dss, f {item = resF} : ress,
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder f {item = anaF} : ranas))
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder ([], [], []) afs
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder fufs = map (mapAn (\ f -> let
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder vs = map ( \ (v, s) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Var_decl [v] s ps)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder in stripQuant $ mkForall (vs ++ il) f ps))
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder sens = map ( \ a -> NamedSen (getRLabel a)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder (notImplied a) False $ item a) fufs
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang addSentences sens
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett return $ Local_var_axioms il resFs ps
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder Axiom_items afs ps ->
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder let (es, resFs, anaFs) = foldr ( \ f (dss, ress, ranas) ->
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers let Result ds m = anaForm mef mix ga
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder sign $ item f
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> (ds ++ dss, ress, ranas)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (resF, anaF) ->
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder (ds ++ dss, f {item = resF} : ress,
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder f {item = anaF} : ranas))
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder ([], [], []) afs
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder fufs = map (mapAn (\ f -> let
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers vs = map ( \ (v, s) ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Var_decl [v] s ps)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in stripQuant $ mkForall vs f ps)) anaFs
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sens = map ( \ a -> NamedSen (getRLabel a)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (notImplied a) False $ item a) fufs
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder addSentences sens
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder return $ Axiom_items resFs ps
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Ext_BASIC_ITEMS b -> fmap Ext_BASIC_ITEMS $ ab mix ga b
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermapAn :: (a -> b) -> Annoted a -> Annoted b
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaedermapAn f an = replaceAnnoted (f $ item an) an
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maedertype GenAx = (Set.Set SORT, Rel.Rel SORT, Set.Set Component)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederemptyGenAx :: GenAx
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederemptyGenAx = (Set.empty, Rel.empty, Set.empty)
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedertoSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian MaedertoSortGenAx ps isFree (sorts, rel, ops) = do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let sortList = Set.toList sorts
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder opSyms = map ( \ c -> let ide = compId c in Qual_op_name ide
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder injSyms = map ( \ (s, t) -> let p = posOfId s in
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Qual_op_name injName
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder (Op_type Total [s] t p) p) $ Rel.toList
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder resType _ (Op_name _) = False
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder resType s (Qual_op_name _ t _) = res_OP_TYPE t ==s
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder getIndex s = maybe (-1) id $ findIndex (==s) sortList
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder addIndices (Op_name _) =
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder error "CASL/StaticAna: Internal error in function addIndices"
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder addIndices os@(Qual_op_name _ t _) =
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder (os,map getIndex $ args_OP_TYPE t)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder collectOps s =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Constraint s (map addIndices $ filter (resType s)
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder (opSyms ++ injSyms)) s
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder constrs = map collectOps sortList
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder f = Sort_gen_ax constrs isFree
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder if null sortList then
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder addDiags[Diag Error "missing generated sort" ps]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder else return ()
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder addSentences [NamedSen
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ("ga_generated_" ++
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder showSepList (showString "_") showId sortList "")
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder True False f]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederana_SIG_ITEMS :: PrettyPrint f => Min f e
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder -> Ana s b s f e -> Mix b s f e -> GlobalAnnos -> GenKind
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder -> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maederana_SIG_ITEMS mef anas mix ga gk si =
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder Sort_items al ps ->
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder do ul <- mapM (ana_SORT_ITEM mef mix ga) al
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder closeSubsortRel
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder return $ Sort_items ul ps
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Op_items al ps ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do ul <- mapM (ana_OP_ITEM mef mix ga) al
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder return $ Op_items ul ps
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Pred_items al ps ->
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder do ul <- mapM (ana_PRED_ITEM mef mix ga) al
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly return $ Pred_items ul ps
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Datatype_items al _ ->
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder mapM_ addSort sorts
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder mapAnM (ana_DATATYPE_DECL gk) al
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder closeSubsortRel
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder Ext_SIG_ITEMS s -> fmap Ext_SIG_ITEMS $ anas mix ga s
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Lueckeana_Generated :: PrettyPrint f => Min f e -> Ana s b s f e -> Mix b s f e
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke -> GlobalAnnos -> [Annoted (SIG_ITEMS s f)]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederana_Generated mef anas mix ga al = do
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder ul <- mapAnM (ana_SIG_ITEMS mef anas mix ga Generated) al
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder return (map (getGenSig . item) ul, ul)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaedergetGenSig :: SIG_ITEMS s f -> GenAx
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergetGenSig si = case si of
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder Sort_items al _ -> unionGenAx $ map (getGenSorts . item) al
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Set.unions (map (getOps . item) al))
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Datatype_items dl _ -> getDataGenSig dl
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke _ -> emptyGenAx
247cc88aa55d0a7b6831767cd593ea885c6747a0Christian MaederisConsAlt :: ALTERNATIVE -> Bool
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederisConsAlt a = case a of
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder Subsorts _ _ -> False
abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichgetDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian MaedergetDataGenSig dl =
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder let alts = concatMap (( \ (Datatype_decl s al _) ->
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder map ( \ a -> (s, item a)) al) . item) dl
76b9b2974795a6fb31f242fd032de3ff66df6204Christian Maeder sorts = map fst alts
76b9b2974795a6fb31f242fd032de3ff66df6204Christian Maeder (realAlts, subs) = partition (isConsAlt . snd) alts
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder cs = map ( \ (s, a) ->
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich let (i, ty, _) = getConsType s a
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich in Component i ty) realAlts
5724300b30738b6298ac5dc162f41e33c40f9c12Karl Luc rel = foldr ( \ (t, a) r ->
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder foldr ( \ s ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder r $ getAltSubsorts a)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in (Set.fromList sorts, rel, Set.fromList cs)
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetGenSorts :: SORT_ITEM f -> GenAx
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetGenSorts si =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let (sorts, rel) = case si of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Sort_decl il _ -> (Set.fromList il, Rel.empty)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Subsort_decl il i _ -> (Set.fromList (i:il)
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder , foldr (flip Rel.insert i) Rel.empty il)
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder Subsort_defn sub _ super _ _ -> (Set.singleton sub
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Iso_decl il _ -> (Set.fromList il
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , foldr ( \ s r -> foldr ( \ t ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in (sorts, rel, Set.empty)
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetOps :: OP_ITEM f -> Set.Set Component
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedergetOps oi = case oi of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Op_decl is ty _ _ ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Set.fromList $ map ( \ i -> Component i $ toOpType ty) is
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Op_defn i par _ _ ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Set.singleton $ Component i $ toOpType $ headToType par
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederana_SORT_ITEM :: PrettyPrint f => Min f e -> Mix b s f e
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> GlobalAnnos -> Annoted (SORT_ITEM f)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> State (Sign f e) (Annoted (SORT_ITEM f))
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederana_SORT_ITEM mef mix ga asi =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder case item asi of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Sort_decl il _ ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do mapM_ addSort il
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Subsort_decl il i _ ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do mapM_ addSort (i:il)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mapM_ (addSubsort i) il
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Subsort_defn sub v super af ps ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do e <- get -- save
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder put e { varMap = Map.empty }
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder addVars (Var_decl [v] super ps)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder put e -- restore
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let Result ds mf = anaForm mef mix ga sign $ item af
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder lb = getRLabel af
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder lab = if null lb then getRLabel asi else lb
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder addSubsort super sub
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder Nothing -> return asi { item = Subsort_decl [sub] super ps}
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just (resF, anaF) -> do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let p = posOfId sub
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder pv = tokPos v
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder addSentences[NamedSen lab (notImplied af) True $
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova mkForall [Var_decl [v] super pv]
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova (Membership (Qual_var v super pv) sub p)
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder return asi { item = Subsort_defn sub v super
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder af { item = resF } ps}
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder Iso_decl il _ ->
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder do mapM_ addSort il
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich [] -> return ()
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich _ : tl -> mapM_ (uncurry $ addSubsortOrIso False)
7165a916d2fa1bf87c4741ec63b253413eebbf69Karl Lucana_OP_ITEM :: PrettyPrint f => Min f e -> Mix b s f e -> GlobalAnnos
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maederana_OP_ITEM mef mix ga aoi =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder case item aoi of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Op_decl ops ty il ps ->
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers do let oty = toOpType ty
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ni = notImplied aoi
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mapM_ (addOp oty) ops
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ul <- mapM (ana_OP_ATTR mef mix ga oty ni ops) il
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder if null $ filter ( \ i -> case i of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Assoc_op_attr -> True
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder _ -> False) il
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder then return ()
2b33802ca26124644f4311db4319376ecffdc8d2Christian Maeder else mapM_ (addAssocOp oty) ops
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return aoi {item = Op_decl ops ty (catMaybes ul) ps}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Op_defn i ohd at ps ->
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski do let ty = headToType ohd
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder lb = getRLabel at
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder lab = if null lb then getRLabel aoi else lb
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder args = case ohd of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Op_head _ as _ _ -> as
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder arg = concatMap ( \ (Var_decl v s qs) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder map ( \ j -> Qual_var j s qs) v) vs
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich addOp (toOpType ty) i
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder e <- get -- save
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder put e { varMap = Map.empty }
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder mapM_ addVars vs
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder put e -- restore
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski let Result ds mt = anaTerm mef mix ga sign
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich (res_OP_TYPE ty) ps $ item at
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Nothing -> return aoi { item = Op_decl [i] ty [] ps }
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder Just (resT, anaT) -> do
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder let p = posOfId i
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder addSentences [NamedSen lab (notImplied at) True $ mkForall vs
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder (Strong_equation
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder (Application (Qual_op_name i ty p) arg ps)
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder return aoi {item = Op_defn i ohd at { item = resT } ps }
10883d13973c46cac98964b66ace7a52b2d059abChristian MaederheadToType :: OP_HEAD -> OP_TYPE
10883d13973c46cac98964b66ace7a52b2d059abChristian MaederheadToType (Op_head k args r ps) = Op_type k (sortsOfArgs args) r ps
bf25e8c286cda74ef89a9cbc3c2143557e0d49c3Christian MaedersortsOfArgs :: [ARG_DECL] -> [SORT]
10883d13973c46cac98964b66ace7a52b2d059abChristian MaedersortsOfArgs = concatMap ( \ (Arg_decl l s _) -> map (const s) l)
10883d13973c46cac98964b66ace7a52b2d059abChristian Maederana_OP_ATTR :: PrettyPrint f => Min f e -> Mix b s f e -> GlobalAnnos
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder -> OpType -> Bool -> [Id] -> (OP_ATTR f)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder -> State (Sign f e) (Maybe (OP_ATTR f))
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maederana_OP_ATTR mef mix ga ty ni ois oa = do
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder let sty = toOP_TYPE ty
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder rty = opRes ty
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder atys = opArgs ty
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder q = posOfId rty
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder [t1,t2] | t1 == t2 -> case oa of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Comm_op_attr -> return ()
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich _ -> if t1 == rty then return ()
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich else addDiags [Diag Error
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder "result sort must be equal to argument sorts" q]
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich _ -> addDiags [Diag Error
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich "expecting two arguments of equal sort" q]
a883cd4d01fe39d23219cf5333425f195be24d8bChristian Maeder Unit_op_attr t ->
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich do sign <- get
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich let Result ds mt = anaTerm mef mix ga
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich sign { varMap = Map.empty } rty q t
5818d884784339c1b8aa6c6d972bad4eafd36ccbKlaus Luettich Nothing -> return Nothing
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich Just (resT, anaT) -> do
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich addSentences $ map (makeUnit True anaT ty ni) ois
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder addSentences $ map (makeUnit False anaT ty ni) ois
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich return $ Just $ Unit_op_attr resT
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich Assoc_op_attr -> do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let ns = map mkSimpleId ["x", "y", "z"]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder vs = map ( \ v -> Var_decl [v] rty q) ns
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder [v1, v2, v3] = map ( \ v -> Qual_var v rty q) ns
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder makeAssoc i = let p = posOfId i
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder qi = Qual_op_name i sty p in
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder NamedSen ("ga_assoc_" ++ showId i "") ni False $
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder (Strong_equation
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder (Application qi [v1, Application qi [v2, v3] p] p)
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder (Application qi [Application qi [v1, v2] p, v3] p) p) p
f38b3687c5558128515e34fb85d8b466d22dc300Christian Maeder addSentences $ map makeAssoc ois
a545f813d2f8006ef79617e4fedc841d89195e2dChristian Maeder return $ Just oa
a545f813d2f8006ef79617e4fedc841d89195e2dChristian Maeder Comm_op_attr -> do
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich let ns = map mkSimpleId ["x", "y"]
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder vs = zipWith ( \ v t -> Var_decl [v] t
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder $ concatMapRange posOfId atys) ns atys
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder args = map toQualVar vs
e05fd774e0181e93963d4302303b20698603a505Christian Maeder makeComm i = let p = posOfId i
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder qi = Qual_op_name i sty p in
aebb0b18fe5e6ba7dd7e4c66a16a905611ef7ba9Christian Maeder NamedSen ("ga_comm_" ++ showId i "") ni False $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Strong_equation
e05fd774e0181e93963d4302303b20698603a505Christian Maeder (Application qi args p)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (Application qi (reverse args) p) p) p
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian Maeder addSentences $ map makeComm ois
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder return $ Just oa
43bb71dfe7ec405f563864d57c1cacdaa8ce9a80Christian Maeder Idem_op_attr -> do
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian Maeder let v = mkSimpleId "x"
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski vd = Var_decl [v] rty q
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder qv = toQualVar vd
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder makeIdem i = let p = posOfId i in
1dfba1f850f6a43094962b459998d1ea11472461Christian Maeder NamedSen ("ga_idem_" ++ showId i "") ni False $
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mkForall [vd]
fa0f3519d71f719d88577b716b1579776b4a2535Christian Maeder (Strong_equation
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (Application (Qual_op_name i sty p) [qv, qv] p)
fa0f3519d71f719d88577b716b1579776b4a2535Christian Maeder addSentences $ map makeIdem ois
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder return $ Just oa
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder-- first bool for left and right, second one for no implied annotation
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian MaedermakeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermakeUnit b t ty ni i =
68b77966b2cf7bf2e340bf0fb6b9efc3e6a00467Christian Maeder let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"
99afa6000472f3d291fdf9193ea19d334a58658dChristian Maeder ++ showId i ""
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder v = mkSimpleId "x"
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder vty = opRes ty
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder q = posOfId vty
c59d1c38ef94b4fb1c8d9fda9573bc1e1d2801e7Christian Maeder p = posOfId i
cd36bffee51c77cdadcb9f916b34fa512e311946Christian Maeder qv = Qual_var v vty q
99afa6000472f3d291fdf9193ea19d334a58658dChristian Maeder args = [qv, t]
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder rargs = if b then args else reverse args
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in NamedSen lab ni False $ mkForall [Var_decl [v] vty q]
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (Strong_equation
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichana_PRED_ITEM :: PrettyPrint f => Min f e -> Mix b s f e
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> GlobalAnnos -> Annoted (PRED_ITEM f)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -> State (Sign f e) (Annoted (PRED_ITEM f))
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichana_PRED_ITEM mef mix ga ap =
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich case item ap of
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Pred_decl preds ty _ ->
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich do mapM (addPred $ toPredType ty) preds
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Pred_defn i phd@(Pred_head args rs) at ps ->
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do let lb = getRLabel at
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder lab = if null lb then getRLabel ap else lb
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ty = Pred_type (sortsOfArgs args) rs
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich arg = concatMap ( \ (Var_decl v s qs) ->
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich map ( \ j -> Qual_var j s qs) v) vs
82e29b77f0ef4cccd7ed734692c5e1e93dbbc645Christian Maeder addPred (toPredType ty) i
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich e <- get -- save
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian Maeder put e { varMap = Map.empty }
5f0e3e4cb7dd31033c9682cafa712d2a66b2f3bcChristian Maeder mapM_ addVars vs
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder put e -- restore
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let Result ds mt = anaForm mef mix ga sign $ item at
210aa1071465039588fa9e38c10e343631c34655Christian Maeder Nothing -> return ap {item = Pred_decl [i] ty ps}
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Just (resF, anaF) -> do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let p = posOfId i
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder addSentences [NamedSen lab True True $
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (Equivalence (Predication (Qual_pred_name i ty p)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich arg p) anaF p) p]
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder return ap {item = Pred_defn i phd at { item = resF } ps}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- full function type of a selector (result sort is component sort)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederdata Component = Component { compId :: Id, compType :: OpType }
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder deriving (Show)
10883d13973c46cac98964b66ace7a52b2d059abChristian Maederinstance Eq Component where
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Component i1 t1 == Component i2 t2 =
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder (i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederinstance Ord Component where
c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian Maeder Component i1 t1 <= Component i2 t2 =
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder (i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance PrettyPrint Component where
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder printText0 ga (Component i ty) =
e1559d046eb2c6dde0e6e272b37b6756eac0e8adChristian Maeder printText0 ga i <+> colon <> printText0 ga ty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance PosItem Component where
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder getRange = getRange . compId
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | return list of constructors
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühlana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühlana_DATATYPE_DECL gk (Datatype_decl s al _) =
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl do ul <- mapM (ana_ALTERNATIVE s . item) al
e284004f10a315dbdb624c8b2522f65d485eaa48Martin Kühl let constr = catMaybes ul
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder cs = map fst constr
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder if null constr then return ()
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder else do addDiags $ checkUniqueness cs
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder let totalSels = Set.unions $ map snd constr
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder wrongConstr = filter ((totalSels /=) . snd) constr
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder addDiags $ map ( \ (c, _) -> mkDiag Error
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ("total selectors '" ++ showSepList (showString ",")
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showPretty (Set.toList totalSels)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "'\n must appear in alternative") c) wrongConstr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let allts = map item al
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski (alts, subs) = partition isConsAlt allts
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski sbs = concatMap getAltSubsorts subs
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski comps = map (getConsType s) alts
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini ttrips = map (( \ (a, vs, t, ses) -> (a, vs, t, catSels ses))
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder . selForms1 "X" ) comps
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini sels = concatMap ( \ (_, _, _, ses) -> ses) ttrips
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder addSentences $ map makeInjective
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder $ filter ( \ (_, _, ces) -> not $ null ces)
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini addSentences $ makeDisjSubsorts s sbs
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder addSentences $ concatMap ( \ c -> map (makeDisjToSort c) sbs)
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder addSentences $ makeDisjoint comps
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich addSentences $ catMaybes $ concatMap
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder map (makeUndefForm ses) ttrips) sels
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder _ -> return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermakeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
99afa6000472f3d291fdf9193ea19d334a58658dChristian MaedermakeDisjSubsorts d subs = case subs of
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder s : rs -> map (makeDisjSubsort s) rs ++ makeDisjSubsorts d rs
d5d349836d8b1fa93ea49a59d977b106c6e9233bKlaus Luettich makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder makeDisjSubsort s1 s2 = let
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder n = mkSimpleId "x"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder pd = posOfId d
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder p1 = posOfId s1
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder p2 = posOfId s2
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich p = pd `appRange` p1 `appRange` p2
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder v = Var_decl [n] d pd
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder qv = toQualVar v
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder in NamedSen ("ga_disjoint_sorts_" ++ showId s1 "_"
e112e83352048f3db8c8f93ae104193e7338c10fChristian Maeder ++ showId s2 "") True False $
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich mkForall [v] (Negation (Conjunction [
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich Membership qv s1 p1, Membership qv s2 p2] p) p) p
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaedermakeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
e112e83352048f3db8c8f93ae104193e7338c10fChristian MaedermakeDisjToSort a s =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let (c, v, t, _) = selForms1 "X" a
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder p = posOfId s in
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder NamedSen ("ga_disjoint_" ++ showId c "_sort_"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ++ showId s "") True False $
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mkForall v (Negation (Membership t s p) p) p
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedermakeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian MaedermakeInjective a =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let (c, v1, t1, _) = selForms1 "X" a
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder (_, v2, t2, _) = selForms1 "Y" a
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder p = posOfId c
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder in NamedSen ("ga_injective_" ++ showId c "") True False $
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder mkForall (v1 ++ v2)
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder (Equivalence (Strong_equation t1 t2 p)
fdef3358918491badb0e29e42b5d3b5a01950716Christian Maeder (let ces = zipWith ( \ w1 w2 -> Strong_equation
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (toQualVar w1) (toQualVar w2) p) v1 v2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder in if isSingle ces then head ces else Conjunction ces p)
88318aafc287e92931dceffbb943d58a9310001dChristian MaedermakeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermakeDisjoint l = case l of
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder c : cs -> map (makeDisj c) cs ++ makeDisjoint cs
bf76f4fcf07abaebea587df8135de8356c26a363Till Mossakowski makeDisj :: (Id, OpType, [COMPONENTS]) -> (Id, OpType, [COMPONENTS])
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder -> Named (FORMULA f)
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski makeDisj a1 a2 =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let (c1, v1, t1, _) = selForms1 "X" a1
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich (c2, v2, t2, _) = selForms1 "Y" a2
473bc1f3f3443f18e0ee83e4642fab42183470f2Christian Maeder p = posOfId c1 `appRange` posOfId c2
473bc1f3f3443f18e0ee83e4642fab42183470f2Christian Maeder in NamedSen ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "") True False
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich $ mkForall (v1 ++ v2)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (Negation (Strong_equation t1 t2 p) p) p
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichcatSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedercatSels = map ( \ (m, t) -> (fromJust m, t)) .
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder filter ( \ (m, _) -> isJust m)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermakeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> Maybe (Named (FORMULA f))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermakeUndefForm (s, ty) (i, vs, t, sels) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let p = posOfId s in
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if any ( \ (se, ts) -> s == se && opRes ts == opRes ty ) sels
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder then Nothing else
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just $ NamedSen ("ga_selector_undef_" ++ showId s "_"
1a6464613c59e35072b90ca296ae402cbe956144Christian Maeder ++ showId i "") True False $
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedergetAltSubsorts :: ALTERNATIVE -> [SORT]
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetAltSubsorts c = case c of
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Subsorts cs _ -> cs
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetConsType s c =
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich let getConsTypeAux (part, i, il) =
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich (i, OpType part (concatMap
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich (map (opRes . snd) . getCompType s) il) s, il)
5818d884784339c1b8aa6c6d972bad4eafd36ccbKlaus Luettich Subsorts _ _ -> error "getConsType"
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Alt_construct k a l _ -> getConsTypeAux (k, a, l)
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetCompType s (Cons_select k l cs _) =
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich map (\ i -> (Just i, OpType k [s] cs)) l
0be0db405c49906bd7057255069bf6df53395ac9Klaus LuettichgetCompType s (Sort cs) = [(Nothing, OpType Partial [s] cs)]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedergenSelVars :: String -> Int -> [OpType] -> [VAR_DECL]
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergenSelVars _ _ [] = []
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedergenSelVars str n (ty:rs) =
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder Var_decl [mkSelVar str n] (opRes ty) nullRange : genSelVars str (n+1) rs
88318aafc287e92931dceffbb943d58a9310001dChristian MaedermkSelVar :: String -> Int -> Token
feac53e31a8351e3e3c6621f6a14b5714008bfc7Heng JiangmkSelVar str n = mkSimpleId (str ++ show n)
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermakeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder -> [Named (FORMULA f)]
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermakeSelForms _ (_, _, _, []) = []
f78ce817f35574674d54e30ad1861a9b4ced20caChristian MaedermakeSelForms n (i, vs, t, (mi, ty):rs) =
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder Nothing -> []
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder Just j -> let p = posOfId j
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder rty = opRes ty
89c9d707aa817684b88036a2dad66c3437840677Heng Jiang q = posOfId rty in
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder [NamedSen ("ga_selector_" ++ showId j "") True False
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder $ mkForall vs
f78ce817f35574674d54e30ad1861a9b4ced20caChristian Maeder (Strong_equation
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder (Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder (Qual_var (mkSelVar "X" n) rty q) p) p]
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder ) ++ makeSelForms (n+1) (i, vs, t, rs)
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckeselForms1 :: String -> (Id, OpType, [COMPONENTS])
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
c802a1041ed9251f8ad79139454267e802900e2aChristian MaederselForms1 str (i, ty, il) =
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder let cs = concatMap (getCompType (opRes ty)) il
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder vs = genSelVars str 1 $ map snd cs
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder in (i, vs, Application (Qual_op_name i (toOP_TYPE ty) nullRange)
c802a1041ed9251f8ad79139454267e802900e2aChristian Maeder (map toQualVar vs) nullRange, cs)
53bbc1c9a4e986d1ee9c081d6f0ac7b9546f212bDominik LuecketoQualVar :: VAR_DECL -> TERM f
bf7b17b0e19362e9228672782218678cab275d1eDominik LuecketoQualVar (Var_decl v s ps) =
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke if isSingle v then Qual_var (head v) s ps else error "toQualVar"
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckeselForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
bf7b17b0e19362e9228672782218678cab275d1eDominik LueckeselForms = makeSelForms 1 . selForms1 "X"
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke-- | return the constructor and the set of total selectors
75b0c0c2cbfb7edd3f4c0555227aabbe6c1aa195Christian Maederana_ALTERNATIVE :: SORT -> ALTERNATIVE
bf7b17b0e19362e9228672782218678cab275d1eDominik Luecke -> State (Sign f e) (Maybe (Component, Set.Set Component))
return $ Just (Component i ty, Set.fromList ts)
cleanSig = accSig { envDiags = [], sentences = [], varMap = Map.empty }