Ana.hs revision c3ebe5e0a6545997d56e4156de02d00518c71c0c
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : static analysis of VSE parts
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederCopyright : (c) C. Maeder, DFKI Bremen 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederanalysis of VSE logic extension of CASL
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Data.Char (toLower)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Data.Map as Map
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Data.Set as Set
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport qualified Common.Lib.Rel as Rel
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaedertokenToLower :: Token -> Token
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertokenToLower (Token s r) = Token (map toLower s) r
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederidToLower :: Id -> Id
8f88a86e9656713ea4608541b8b47bb47a755bffChristian MaederidToLower (Id ts cs r) = Id (map tokenToLower ts) (map idToLower cs) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederhasMany :: Set.Set a -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederhasMany s = Set.size s > 1
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedergetCases :: String -> Set.Set Id -> [Diagnosis]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetCases msg =
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder map (mkDiag Error ("overlapping " ++ msg ++ " identifiers") . Set.toList)
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder . filter hasMany . Map.elems
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder . Set.fold (\ i -> Rel.setInsert (idToLower i) i) Map.empty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetCaseDiags :: Sign f e -> [Diagnosis]
df33a9af92444f63ad545da6bb326aac9284318eChristian MaedergetCaseDiags sig =
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder getCases "sort" (sortSet sig)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder ++ getCases "op or function" (Map.keysSet $ opMap sig)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder ++ getCases "pred or proc" (Map.keysSet $ predMap sig)
df33a9af92444f63ad545da6bb326aac9284318eChristian MaederboolSig :: Sign f Procs
df33a9af92444f63ad545da6bb326aac9284318eChristian MaederboolSig = execState (do
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder let e = emptyAnno ()
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder bi = stringToId "Boolean"
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder ot = OpType Total [] bi
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder addSort NonEmptySorts e bi
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder addOp e ot (stringToId "False")
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder addOp e ot (stringToId "True")) $ emptySign emptyProcs
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaederlookupProc :: Id -> Sign f Procs -> Maybe Profile
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlookupProc i sig = Map.lookup i $ procsMap $ extendedInfo sig
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder :: (BASIC_SPEC () Procdecls Dlformula,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Sign Dlformula Procs, GlobalAnnos)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -> Result (BASIC_SPEC () Procdecls Dlformula,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ExtSign (Sign Dlformula Procs) Symbol,
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder [Named Sentence])
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederbasicAna (bs, sig, ga) = do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (bs2, ExtSign sig2 syms, sens) <-
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder basicAnalysis minExpForm (const return) anaProcdecls anaMix
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (bs, addSig const sig boolSig, ga)
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder Result (getCaseDiags sig2) $ Just () -- add diags
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (bs2, ExtSign (diffSig const sig2 boolSig) syms, sens)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaMix :: Mix () Procdecls Dlformula Procs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaMix = emptyMix
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder { putParen = parenDlFormula
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , mixResolve = resolveDlformula }
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-- | put parens around ambiguous mixfix formulas (for error messages)
99f16a0f9ca757410960ff51a79b034503384fe2Christian MaederparenDlFormula :: Dlformula -> Dlformula
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederparenDlFormula (Ranged f r) = case f of
d48085f765fca838c1d972d2123601997174583dChristian Maeder Dlformula b p s ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder let n = mapFormula parenDlFormula s
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder in Ranged (Dlformula b (parenProg p) n) r
d48085f765fca838c1d972d2123601997174583dChristian Maeder Defprocs ps -> Ranged (Defprocs $ map parenDefproc ps) r
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederparenProg :: Program -> Program
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederparenProg = foldProg $ mapProg (Paren.mapTerm id) $ mapFormula id
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederparenDefproc :: Defproc -> Defproc
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederparenDefproc (Defproc k i vs p r) = Defproc k i vs (parenProg p) r
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederprocsToPredMap :: Procs -> Map.Map Id (Set.Set PredType)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaederprocsToPredMap (Procs m) =
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder foldr (\ (n, pr@(Profile _ mr)) pm -> case mr of
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Nothing -> Rel.setInsert n (profileToPredType pr) pm
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederprocsToOpMap :: Procs -> OpMap
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederprocsToOpMap (Procs m) =
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder foldr (\ (n, pr) om -> case profileToOpType pr of
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Just ot -> Rel.setInsert n ot om
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder-- | resolve mixfix applications of terms and formulas
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian MaederresolveDlformula :: MixResolve Dlformula
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederresolveDlformula ga rules (Ranged f r) = case f of
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Dlformula b p s -> do
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder np <- resolveProg ga rules p
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder n <- resolveMixFrm id resolveDlformula ga rules s
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder return $ Ranged (Dlformula b np n) r
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder Defprocs ps -> do
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder nps <- mapM (resolveDefproc ga rules) ps
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder return $ Ranged (Defprocs nps) r
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaederresolveT :: MixResolve (TERM ())
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaederresolveT = resolveMixTrm id (mixResolve emptyMix)
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaederresolveF :: MixResolve (FORMULA ())
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian MaederresolveF = resolveMixFrm id (mixResolve emptyMix)
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaederresolveProg :: MixResolve Program
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederresolveProg ga rules p@(Ranged prg r) = case prg of
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder Abort -> return p
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder Skip -> return p
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Assign v t -> do
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder nt <- resolveT ga rules t
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder return $ Ranged (Assign v nt) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder nf <- resolveF ga rules f
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder return $ Ranged (Call nf) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Return t -> do
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder nt <- resolveT ga rules t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder return $ Ranged (Return nt) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Block vs q -> do
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder np <- resolveProg ga rules q
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder return $ Ranged (Block vs np) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder Seq p1 p2 -> do
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder p3 <- resolveProg ga rules p1
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder p4 <- resolveProg ga rules p2
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder return $ Ranged (Seq p3 p4) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder If f p1 p2 -> do
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder c <- resolveF ga rules f
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder p3 <- resolveProg ga rules p1
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder p4 <- resolveProg ga rules p2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ Ranged (If c p3 p4) r
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder While f q -> do
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder c <- resolveF ga rules f
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder np <- resolveProg ga rules q
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return $ Ranged (While c np) r
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveDefproc :: MixResolve Defproc
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveDefproc ga rules (Defproc k i vs p r) = do
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder np <- resolveProg ga rules p
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder return $ Defproc k i vs np r
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- | resolve overloading and type check terms and formulas
48c4688439e0aade4faeebf25ca8b16d661e47afChristian MaederminExpForm :: Min Dlformula Procs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederminExpForm sign (Ranged f r) = let sig = castSign sign in case f of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Dlformula b p s -> do
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder np <- minExpProg Set.empty Nothing sig p
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder n <- minExpFORMULA minExpForm sign s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return $ Ranged (Dlformula b np n) r
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Defprocs ps -> do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder nps <- mapM (minProcdecl sig) ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ Ranged (Defprocs nps) r
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederoneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederoneExpT = oneExpTerm (const return)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederminExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederminExpF = minExpFORMULA (const return)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercheckRec :: Record f Bool Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercheckRec = (constRecord (const False) and True)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { foldQuantification = \ _ _ _ _ _ -> False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldDefinedness = \ _ _ _ -> False
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder , foldExistl_equation = \ _ _ _ _ -> False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldMembership = \ _ _ _ _ -> False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldCast = \ _ _ _ _ -> False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , foldConditional = \ _ _ _ _ _ -> False }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederminExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Program -> Result Program
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederminExpProg invars res sig p@(Ranged prg r) = let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder checkCond f = if foldFormula checkRec f then return f else
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkError "illegal formula" f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder checkTerm t = if foldTerm checkRec t then return t else
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder mkError "illegal term" t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case prg of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder Abort -> return p
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder Skip -> return p
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder Assign v t -> case Map.lookup v $ varMap sig of
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder Nothing -> Result [mkDiag Error "undeclared program variable" v] Nothing
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder nt <- oneExpT sig $ Sorted_term t s r
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Set.member v invars then
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder Result [mkDiag Warning "assignment to input variable" v] $ Just ()
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder else return ()
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder return $ Ranged (Assign v nt) r
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Call f -> case f of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Predication ps ts _ -> let i = predSymbName ps in
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder case lookupProc i sig of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
79bf169bcae16ce390683c698bae248c1ed6ab13Christian Maeder Just pr@(Profile l re) -> let
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder nl = case re of
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder Just s -> l ++ [Procparam Out s]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder in if length nl /= length ts then
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Result [mkDiag Error "non-matching number of parameters for" i]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder sign <- if length l < length nl then
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Result [mkDiag Warning "function used as procedure" i] $ Just
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder sig { predMap = Rel.setInsert i (funProfileToPredType pr)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder $ predMap sig }
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder else return sig { predMap = Rel.setInsert i (profileToPredType pr)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder $ predMap sig }
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder nf <- minExpF sign f
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder return $ Ranged (Call nf) r
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder _ -> Result [mkDiag Error "no procedure call" f] Nothing
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Return t -> case res of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Nothing -> Result [mkDiag Error "unexpected return statement" t] Nothing
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder nt <- oneExpT sig $ Sorted_term t s r
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder return $ Ranged (Return nt) r
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder Block vs q -> do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let (_, sign') = runState (mapM_ addVars vs) sig { envDiags = [] }
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder Result (envDiags sign') $ Just ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder np <- minExpProg invars res sign' q
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ Ranged (Block vs np) r
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder Seq p1 p2 -> do
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder p3 <- minExpProg invars res sig p1
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder p4 <- minExpProg invars res sig p2
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder return $ Ranged (Seq p3 p4) r
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder If f p1 p2 -> do
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder c <- minExpF sig f
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder p3 <- minExpProg invars res sig p1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder p4 <- minExpProg invars res sig p2
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder return $ Ranged (If c p3 p4) r
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder While f q -> do
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder c <- minExpF sig f
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder np <- minExpProg invars res sig q
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return $ Ranged (While c np) r
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederminProcdecl :: Sign () Procs -> Defproc -> Result Defproc
b06572b54fcf9d6976cfff57da22672f996b4748Christian MaederminProcdecl sig (Defproc k i vs p r) = case lookupProc i sig of
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder Just (Profile l re) -> if length vs /= length l then
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder Result [mkDiag Error "unknown procedure" i] Nothing
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder let invars = Set.fromList $ map fst $
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder filter (\ (_, Procparam j _) -> j == In) $ zip vs l
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder np <- minExpProg invars re sig { varMap = Map.fromList $ zipWith
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder (\ v (Procparam _ s) -> (v, s)) vs l } p
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return $ Defproc k i vs np r
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder-- | analyse and add procedure declarations
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederanaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs
8f88a86e9656713ea4608541b8b47bb47a755bffChristian MaederanaProcdecls _ ds@(Procdecls ps _) = do
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder mapM_ (anaProcdecl . item) ps
bbde799eb4f0cbc0924cee44ccd3de42fa61d360Christian MaederanaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()
bbde799eb4f0cbc0924cee44ccd3de42fa61d360Christian MaederanaProcdecl (Procedure i p@(Profile ps _) q) = do
bbde799eb4f0cbc0924cee44ccd3de42fa61d360Christian Maeder updateExtInfo (\ pm@(Procs m) ->
30e50372105eacc129a413e390e06036735b69b2Christian Maeder let n = Procs $ Map.insert i p m in case Map.lookup i m of
30e50372105eacc129a413e390e06036735b69b2Christian Maeder Just o -> if p == o then
95a732a847b41efa43b43608fcfcbac3b18dbb4fChristian Maeder hint n ("repeated procedure " ++ showId i "") q
30e50372105eacc129a413e390e06036735b69b2Christian Maeder else plain_error pm ("redeclared procedure " ++ showId i "") q
95a732a847b41efa43b43608fcfcbac3b18dbb4fChristian Maeder Nothing -> return n)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder let e = emptyAnno ()
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder case profileToOpType p of
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder if all (\ (Procparam j _) -> j == In) ps then return () else
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder addDiags [mkDiag Warning "function must have IN params only" i]
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder _ -> addPred e (profileToPredType p) i
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederparamsToArgs :: [Procparam] -> [SORT]
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederparamsToArgs = map (\ (Procparam _ s) -> s)
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederprofileToPredType :: Profile -> PredType
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederprofileToPredType (Profile a _) = PredType $ paramsToArgs a
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederfunProfileToPredType :: Profile -> PredType
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederfunProfileToPredType (Profile a r) = case r of
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder Nothing -> error "funProfileToPredType"
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder Just s -> PredType $ paramsToArgs a ++ [s]
f7663514e02f6095198371a64e574c50e6ec857aChristian MaederprofileToOpType :: Profile -> Maybe OpType
99edc5256de959957a8c27b05ae4ad4f0572233dChristian MaederprofileToOpType (Profile a r) = case r of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> Nothing
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder Just s -> Just $ OpType Partial (paramsToArgs a) s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercastSign :: Sign f e -> Sign a e
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaedercastSign s = s { sentences = [] }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercastMor :: Morphism f e b -> Morphism a e b
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder { msource = castSign $ msource m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , mtarget = castSign $ mtarget m }
966e627a1c06b302a06d59d08b8ab45905f3509cChristian Maeder-- | apply a morphism
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermapMorProg :: Morphism f Procs () -> Program -> Program
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapMorProg mor = let m = castMor mor in
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder foldProg (mapProg (MapSen.mapTerm (const id) m)
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder $ mapSen (const id) m)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder { foldBlock = \ (Ranged _ r) vs p ->
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder Ranged (Block (map (mapVars m) vs) p) r
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder , foldCall = \ (Ranged _ r)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Predication (Qual_pred_name i (Pred_type args r1) r2) ts r3) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case lookupProc i $ msource mor of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> error "mapMorProg"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just pr -> let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder j = mapProcIdProfile mor i pr
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder nargs = map (mapSrt mor) args
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder nts = map (MapSen.mapTerm (const id) m) ts
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder in Ranged (Call $ Predication
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder (Qual_pred_name j (Pred_type nargs r1) r2) nts r3) r }
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedermapProcId :: Morphism f Procs () -> Id -> Id
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedermapProcId m i = case lookupProc i $ msource m of
5b2a749acd03ab4f09585251cf38b89bb012dbdcChristian Maeder Just p -> mapProcIdProfile m i p
5b2a749acd03ab4f09585251cf38b89bb012dbdcChristian Maeder Nothing -> error $ "VSE.mapProcId unknown " ++ show i
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedermapProcIdProfile :: Morphism f Procs () -> Id -> Profile -> Id
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapProcIdProfile m i p = case profileToOpType p of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just t -> fst $ mapOpSym (sort_map m) (fun_map m) (i, t)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> fst $ mapPredSym (sort_map m) (pred_map m)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (i, profileToPredType p)
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedermapMorDefproc :: Morphism f Procs () -> Defproc -> Defproc
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedermapMorDefproc m (Defproc k i vs p r) =
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder Defproc k (mapProcId m i) vs (mapMorProg m p) r
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedermapDlformula :: MapSen Dlformula Procs ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapDlformula m (Ranged f r) = case f of
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder Dlformula b p s ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let n = mapSen mapDlformula m s
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder in Ranged (Dlformula b (mapMorProg m p) n) r
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder Defprocs ps -> Ranged (Defprocs $ map (mapMorDefproc m) ps) r
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder-- | simplify fully qualified terms and formulas for pretty printing sentences
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedersimpProg :: Sign () e -> Program -> Program
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedersimpProg sig =
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder foldProg (mapProg (simplifyTerm dummyMin (const id) sig)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ simplifySen dummyMin (const id) sig)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder { foldBlock = \ (Ranged (Block vs p) r) _ _ ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Ranged (Block vs $ simpProg
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder (execState (mapM_ addVars vs) sig) p) r }
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedersimpDefproc :: Sign () Procs -> Defproc -> Defproc
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedersimpDefproc sign (Defproc k i vs p r) =
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder let sig = case lookupProc i sign of
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder Nothing -> sign
aaf68b27b802d3b9bf39202fa781478dcab8fde5Christian Maeder Just (Profile l _) -> if length vs /= length l then sign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else sign { varMap = Map.fromList $ zipWith
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder (\ v (Procparam _ s) -> (v, s)) vs l }
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder in Defproc k i vs (simpProg sig p) r
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedersimpDlformula :: Sign Dlformula Procs -> Dlformula -> Dlformula
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedersimpDlformula sign (Ranged f r) = let sig = castSign sign in case f of
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder Dlformula b p s -> let
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder q = simpProg sig p
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder n = simplifySen minExpForm simpDlformula sign s
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder in Ranged (Dlformula b q n) r
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Defprocs ps -> Ranged (Defprocs $ map (simpDefproc sig) ps) r
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder-- | free variables to be universally bound on the top level
8f88a86e9656713ea4608541b8b47bb47a755bffChristian MaederfreeProgVars :: Sign () e -> Program -> VarSet
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederfreeProgVars sig = let ft = freeTermVars sig in
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder foldProg (progToSetRec ft (freeVars sig))
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder { foldAssign = \ _ v t -> (case Map.lookup v $ varMap sig of
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder Just s -> Set.insert (v, s)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder Nothing -> Set.insert (v, sortOfTerm t)) $ ft t
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder , foldBlock = \ (Ranged (Block vs p) _) _ _ ->
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder Set.difference (freeProgVars (execState (mapM_ addVars vs) sig) p)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder $ Set.fromList $ flatVAR_DECLs vs }
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaederfreeDlVars :: Sign Dlformula e -> Dlformula -> VarSet
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederfreeDlVars sig (Ranged f _) = case f of
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder Dlformula _ p s -> Set.union (freeProgVars (castSign sig) p) $
de2f13b8310de00ca228385b1530660e036054c2Christian Maeder freeVars sig s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance GetRange (Ranged a) where
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder getRange (Ranged _ r) = r
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maederinstance FreeVars Dlformula where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder freeVarsOfExt = freeDlVars
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | adjust procs map in morphism target signature
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercorrectTarget :: Morphism f Procs () -> Morphism f Procs ()
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedercorrectTarget m = let tar = mtarget m in m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { mtarget = correctSign tar
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { extendedInfo = Procs $ Map.fromList
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder $ map (\ (i, p) -> (mapProcIdProfile m i p, mapProfile (sort_map m) p))
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $ Map.toList $ procsMap $ extendedInfo tar }
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , msource = correctSign $ msource m }
d92635f998347112e5d5803301c2abfe7832ab65Christian MaedercorrectSign :: Sign f Procs -> Sign f Procs
8f88a86e9656713ea4608541b8b47bb47a755bffChristian MaedercorrectSign sig = sig
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { extendedInfo = Procs $ Map.filterWithKey (\ i p -> case profileToOpType p of
8f88a86e9656713ea4608541b8b47bb47a755bffChristian Maeder Just t -> case Map.lookup i $ opMap sig of
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder Just s -> Set.member t s || Set.member t { opKind = Total } s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> False
32a2f5f00ff72c095b39629101043db4407974f9Christian Maeder Nothing -> case Map.lookup i $ predMap sig of
32a2f5f00ff72c095b39629101043db4407974f9Christian Maeder Just s -> Set.member (profileToPredType p) s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> False) $ procsMap $ extendedInfo sig }
1090553a9231ceb536cb8007219c08be0c8c313dChristian MaedermapProfile :: Sort_map -> Profile -> Profile
1090553a9231ceb536cb8007219c08be0c8c313dChristian MaedermapProfile m (Profile l r) = Profile
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (map (\ (Procparam k s) -> Procparam k $ mapSort m s) l)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ fmap (mapSort m) r