Ana.hs revision dece9056c18ada64bcc8f2fba285270374139ee8
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-# LANGUAGE TypeSynonymInstances #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiDescription : static analysis of VSE parts
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) C. Maeder, DFKI Bremen 2008
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskianalysis of VSE logic extension of CASL
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder , constBoolType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , procsToOpMap
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , procsToPredMap
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , profileToOpType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , profileToPredType
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowski , mapDlformula
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder , simpDlformula
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , correctSign
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , correctTarget
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , VSEBasicSpec
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , extVSEColimit
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Data.Char (toLower)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Data.Map as Map
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Data.Set as Set
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Common.Lib.MapSet as MapSet
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport Common.Utils (hasMany)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype VSESign = Sign Dlformula Procs
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaedergetVariables :: Sentence -> Set.Set Token
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedergetVariables = foldFormula $ getVarsRec $ getVSEVars . unRanged
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedergetVarsRec :: (f -> Set.Set Token) -> Record f (Set.Set Token) (Set.Set Token)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetVarsRec f =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder { foldQuantification = \ _ _ vs r _ -> Set.union r
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder $ Set.fromList $ map fst $ flatVAR_DECLs vs
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , foldQual_var = \ _ v _ _ -> Set.singleton v }
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetVSEVars :: VSEforms -> Set.Set Token
5e46b572ed576c0494768998b043d9d340594122Till MossakowskigetVSEVars vf = case vf of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Dlformula _ p s -> Set.union (getProgVars p) $ getVariables s
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Defprocs l -> Set.unions $ map getDefprogVars l
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> Set.empty -- no variables in a sort generation constraint
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetProgVars :: Program -> Set.Set Token
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let vrec = getVarsRec $ const Set.empty
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder getTermVars = foldTerm vrec
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder getCondVars = foldFormula vrec
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in foldProg (progToSetRec getTermVars getCondVars)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder { foldAssign = \ _ v t -> Set.insert v $ getTermVars t
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , foldBlock = \ _ vs p -> Set.union p
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ Set.fromList $ map fst $ flatVAR_DECLs vs }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetDefprogVars :: Defproc -> Set.Set Token
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetDefprogVars (Defproc _ _ vs p _) = Set.union (getProgVars p)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertokenToLower :: Token -> Token
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertokenToLower (Token s r) = Token (map toLower s) r
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederidToLower :: Id -> Id
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederidToLower (Id ts cs r) = Id (map tokenToLower ts) (map idToLower cs) r
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedergetCases :: String -> Set.Set Id -> [Diagnosis]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedergetCases msg =
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder map (mkDiag Error ("overlapping " ++ msg ++ " identifiers") . Set.toList)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder . filter hasMany . Map.elems
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder . Set.fold (\ i -> MapSet.setInsert (idToLower i) i) Map.empty
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedergetCaseDiags :: Sign f e -> [Diagnosis]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetCaseDiags sig =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder getCases "sort" (sortSet sig)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ++ getCases "op or function" (MapSet.keysSet $ opMap sig)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder ++ getCases "pred or proc" (MapSet.keysSet $ predMap sig)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederuBoolean :: Id
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederuBoolean = stringToId "Boolean"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederuTrue = stringToId "True"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederuFalse = stringToId "False"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertBoolean :: OP_TYPE
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertBoolean = Op_type Total [] uBoolean nullRange
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederconstBoolType :: OpType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederconstBoolType = toOpType tBoolean
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederqBoolean :: Id -> OP_SYMB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiqBoolean c = Qual_op_name c tBoolean nullRange
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederqTrue :: OP_SYMB
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederqTrue = qBoolean uTrue
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederqFalse :: OP_SYMB
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiqFalse = qBoolean uFalse
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermkConstAppl :: OP_SYMB -> TERM f
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimkConstAppl o = Application o [] nullRange
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederaTrue :: TERM f
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederaTrue = mkConstAppl qTrue
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaFalse :: TERM f
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaFalse = mkConstAppl qFalse
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederuOpMap :: OpMap
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederuOpMap = MapSet.fromList $ map (\ c -> (c, [constBoolType]))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder [uFalse, uTrue]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederboolSig :: Sign f Procs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederboolSig = (emptySign emptyProcs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { sortRel = MapSet.insert uBoolean uBoolean MapSet.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , opMap = uOpMap }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskilookupProc :: Id -> Sign f Procs -> Maybe Profile
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederlookupProc i = Map.lookup i . procsMap . extendedInfo
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprocsSign :: Sign f Procs -> Sign f Procs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprocsSign sig = (emptySign emptyProcs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { predMap = procsToPredMap $ extendedInfo sig }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | add procs as predicate
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddProcs :: Sign f Procs -> Sign f Procs
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiaddProcs sig = addSig const sig $ procsSign sig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | remove procs as predicate
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisubProcs :: Sign f Procs -> Sign f Procs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisubProcs sig = diffSig const sig $ procsSign sig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicheckCases :: Sign f e -> [Named Sentence] -> [Diagnosis]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicheckCases sig2 sens = getCaseDiags sig2 ++ concatMap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (getCases "var" . Set.map simpleIdToId . getVariables . sentence) sens
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype VSEBasicSpec = BASIC_SPEC () Procdecls Dlformula
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederbasicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskibasicAna (bs, sig, ga) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let sigIn = subProcs $ addSig const sig boolSig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (bs2, ExtSign sig2 syms, sens) <-
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski basicAnalysis minExpForm (const return) anaProcdecls anaMix
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (bs, sigIn, ga)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski appendDiags $ checkCases sig2 sens
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski appendDiags . map
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (mkDiag Error "illegal predicate declaration for procedure")
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder . Set.toList . MapSet.keysSet . interMapSet
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (diffMapSet (predMap sig2) $ predMap sigIn)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder . procsToPredMap $ extendedInfo sig2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let sig3 = diffSig const sig2 boolSig
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (rSens, fSens) = partition (foldFormula (checkRec True) . sentence) sens
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder appendDiags $ map (mkDiag Error "unsupported VSE formula" . sentence) fSens
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski appendDiags . map (mkDiag Error "illegal overloading of")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski . Set.toList . Set.intersection (MapSet.keysSet $ opMap sig3)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (bs2, ExtSign (addProcs $ diffSig const sig2 boolSig) syms, rSens)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskianaMix :: Mix () Procdecls Dlformula Procs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaMix = emptyMix
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder { putParen = parenDlFormula
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , mixResolve = resolveDlformula }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | put parens around ambiguous mixfix formulas (for error messages)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenDlFormula :: Dlformula -> Dlformula
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenDlFormula (Ranged f r) = case f of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Dlformula b p s ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let n = mapFormula parenDlFormula s
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in Ranged (Dlformula b (parenProg p) n) r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Defprocs ps -> Ranged (Defprocs $ map parenDefproc ps) r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder _ -> Ranged f r -- no mixfix formulas?
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenProg :: Program -> Program
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenProg = foldProg $ mapProg (Paren.mapTerm id) $ mapFormula id
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenDefproc :: Defproc -> Defproc
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederparenDefproc (Defproc k i vs p r) = Defproc k i vs (parenProg p) r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederprocsToPredMap :: Procs -> PredMap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprocsToPredMap (Procs m) =
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder foldr (\ (n, pr@(Profile _ mr)) pm -> case mr of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Nothing -> MapSet.insert n (profileToPredType pr) pm
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederprocsToOpMap :: Procs -> OpMap
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederprocsToOpMap (Procs m) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder foldr (\ (n, pr) om -> case profileToOpType pr of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Just ot -> MapSet.insert n ot om
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder-- | resolve mixfix applications of terms and formulas
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveDlformula :: MixResolve Dlformula
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveDlformula ga rules (Ranged f r) = case f of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Dlformula b p s -> do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder np <- resolveProg ga rules p
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder n <- resolveMixFrm id resolveDlformula ga rules s
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return $ Ranged (Dlformula b np n) r
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Defprocs ps -> do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder nps <- mapM (resolveDefproc ga rules) ps
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return $ Ranged (Defprocs nps) r
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder _ -> return $ Ranged f r -- no mixfix?
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveT :: MixResolve (TERM ())
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveT = resolveMixTrm id (mixResolve emptyMix)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveF :: MixResolve (FORMULA ())
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolveF = resolveMixFrm id (mixResolve emptyMix)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiresolveProg :: MixResolve Program
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiresolveProg ga rules p@(Ranged prg r) = case prg of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Abort -> return p
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Skip -> return p
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Assign v t -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nt <- resolveT ga rules t
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder return $ Ranged (Assign v nt) r
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder nf <- resolveF ga rules f
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ Ranged (Call nf) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Return t -> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder nt <- resolveT ga rules t
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ Ranged (Return nt) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Block vs q -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder np <- resolveProg ga rules q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Ranged (Block vs np) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Seq p1 p2 -> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder p3 <- resolveProg ga rules p1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder p4 <- resolveProg ga rules p2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Ranged (Seq p3 p4) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder If f p1 p2 -> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder c <- resolveF ga rules f
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder p3 <- resolveProg ga rules p1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder p4 <- resolveProg ga rules p2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Ranged (If c p3 p4) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder While f q -> do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder c <- resolveF ga rules f
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder np <- resolveProg ga rules q
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Ranged (While c np) r
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederresolveDefproc :: MixResolve Defproc
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederresolveDefproc ga rules (Defproc k i vs p r) = do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder np <- resolveProg ga rules p
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ Defproc k i vs np r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | resolve overloading and type check terms and formulas
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederminExpForm :: Min Dlformula Procs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederminExpForm sign (Ranged f r) = let sig = castSign sign in case f of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Dlformula b p s -> do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski np <- minExpProg Set.empty Nothing sig p
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder n <- minExpFORMULA minExpForm sign s
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ Ranged (Dlformula b np n) r
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Defprocs ps -> do
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder nps <- mapM (minProcdecl sig) ps
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder return $ Ranged (Defprocs nps) r
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder _ -> fail "nyi for restricted constraints"
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederoneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederoneExpT = oneExpTerm (const return)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederminExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederminExpF = minExpFORMULA (const return)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedercheckRec :: Bool -> Record f Bool Bool
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedercheckRec b = (constRecord (const False) and True)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder { foldQuantification = \ _ _ _ _ _ -> b
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder , foldDefinedness = \ _ _ _ -> False
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , foldExistl_equation = \ _ _ _ _ -> False
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder , foldMembership = \ _ _ _ _ -> False
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , foldCast = \ _ _ _ _ -> False
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder , foldConditional = \ _ _ _ _ _ -> False
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder , foldExtFORMULA = \ _ _ -> b }
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederminExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -> Program -> Result Program
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederminExpProg invars res sig p@(Ranged prg r) = let
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder checkCond f = if foldFormula (checkRec False) f then return f else
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder mkError "illegal formula" f
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder checkTerm t = if foldTerm (checkRec False) t then return t else
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder mkError "illegal term" t
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in case prg of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Abort -> return p
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Skip -> return p
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Assign v t -> case Map.lookup v $ varMap sig of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Nothing -> Result [mkDiag Error "undeclared program variable" v] Nothing
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder nt <- oneExpT sig $ Sorted_term t s r
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski when (Set.member v invars)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder $ appendDiags [mkDiag Warning "assignment to input variable" v]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Ranged (Assign v nt) r
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Call f -> case f of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Predication ps ts _ -> let i = predSymbName ps in
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder case lookupProc i sig of
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just pr@(Profile l re) -> let
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder nl = case re of
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Just s -> l ++ [Procparam Out s]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski in if length nl /= length ts then
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Result [mkDiag Error "non-matching number of parameters for" i]
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sign <- if length l < length nl then
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Result [mkDiag Warning "function used as procedure" i] $ Just
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sig { predMap = MapSet.insert i (funProfileToPredType pr)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder $ predMap sig }
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski else return sig { predMap = MapSet.insert i (profileToPredType pr)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski $ predMap sig }
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski nf <- minExpF sign f
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Ranged (Call nf) r
a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski _ -> Result [mkDiag Error "no procedure call" f] Nothing
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Return t -> case res of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Nothing -> Result [mkDiag Error "unexpected return statement" t] Nothing
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski nt <- oneExpT sig $ Sorted_term t s r
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder return $ Ranged (Return nt) r
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Block vs q -> do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let sign' = execState (mapM_ addVSEVars vs) sig { envDiags = [] }
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski appendDiags $ envDiags sign'
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski np <- minExpProg invars res sign' q
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Ranged (Block vs np) r
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Seq p1 p2 -> do
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski p3 <- minExpProg invars res sig p1
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski p4 <- minExpProg invars res sig p2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Ranged (Seq p3 p4) r
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder If f p1 p2 -> do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder c <- minExpF sig f
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski p3 <- minExpProg invars res sig p1
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski p4 <- minExpProg invars res sig p2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ Ranged (If c p3 p4) r
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski While f q -> do
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski c <- minExpF sig f
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski np <- minExpProg invars res sig q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Ranged (While c np) r
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaddVSEVars :: VAR_DECL -> State (Sign f Procs) ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaddVSEVars vd@(Var_decl vs _ _) = do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder p <- gets $ procsMap . extendedInfo
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder mapM_ (addDiags . checkWithMap "var" "procedure" p . simpleIdToId) vs
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederminProcdecl :: Sign () Procs -> Defproc -> Result Defproc
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederminProcdecl sig (Defproc k i vs p r) = case lookupProc i sig of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Just (Profile l re) -> if length vs /= length l then
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Result [mkDiag Error "unknown procedure" i] Nothing
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let invars = Set.fromList $ map fst $
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder filter (\ (_, Procparam j _) -> j == In) $ zip vs l
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder np <- minExpProg invars re sig { varMap = Map.fromList $ zipWith
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (\ v (Procparam _ s) -> (v, s)) vs l } p
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ Defproc k i vs np r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | analyse and add procedure declarations
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian MaederanaProcdecls _ ds@(Procdecls ps _) = do
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder mapM_ (anaProcdecl . item) ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaProcdecl (Procedure i p@(Profile ps mr) q) = do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let prM = predMap e
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ea = emptyAnno ()
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder isPred = case mr of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> Set.member (profileToPredType p) l
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder updateExtInfo (\ pm@(Procs m) ->
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder let n = Procs $ Map.insert i p m in case Map.lookup i m of
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Just o -> if p == o then
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder hint n ("repeated procedure " ++ showId i "") q
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder else plain_error pm
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ("cannot change profile of procedure " ++ showId i "") q
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> if isPred then plain_error pm
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ("cannot change predicate to procedure " ++ showId i "") q
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski else return n)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder case profileToOpType p of
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder unless (all (\ (Procparam j _) -> j == In) ps)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder $ addDiags [mkDiag Warning "function must have IN params only" i]
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder _ -> unless isPred
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder $ addAnnoSet ea $ Symbol i $ PredAsItemType $ profileToPredType p
746440cc1b984a852f5864235b8fa3930963a081Christian MaederparamsToArgs :: [Procparam] -> [SORT]
746440cc1b984a852f5864235b8fa3930963a081Christian MaederparamsToArgs = map (\ (Procparam _ s) -> s)
746440cc1b984a852f5864235b8fa3930963a081Christian MaederprofileToPredType :: Profile -> PredType
746440cc1b984a852f5864235b8fa3930963a081Christian MaederprofileToPredType (Profile a _) = PredType $ paramsToArgs a
746440cc1b984a852f5864235b8fa3930963a081Christian MaederfunProfileToPredType :: Profile -> PredType
746440cc1b984a852f5864235b8fa3930963a081Christian MaederfunProfileToPredType (Profile a r) = case r of
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> error "funProfileToPredType"
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Just s -> PredType $ paramsToArgs a ++ [s]
746440cc1b984a852f5864235b8fa3930963a081Christian MaederprofileToOpType :: Profile -> Maybe OpType
746440cc1b984a852f5864235b8fa3930963a081Christian MaederprofileToOpType (Profile a r) = case r of
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> Nothing
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Just s -> Just $ OpType Partial (paramsToArgs a) s
746440cc1b984a852f5864235b8fa3930963a081Christian MaedercastSign :: Sign f e -> Sign a e
746440cc1b984a852f5864235b8fa3930963a081Christian MaedercastSign s = s { sentences = [] }
746440cc1b984a852f5864235b8fa3930963a081Christian MaedercastMor :: Morphism f e b -> Morphism a e b
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder { msource = castSign $ msource m
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder , mtarget = castSign $ mtarget m }
746440cc1b984a852f5864235b8fa3930963a081Christian Maedertype VSEMorExt = DefMorExt Procs
746440cc1b984a852f5864235b8fa3930963a081Christian Maedertype VSEMor = Morphism Dlformula Procs VSEMorExt
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder-- | apply a morphism
746440cc1b984a852f5864235b8fa3930963a081Christian MaedermapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapMorProg mor = let m = castMor mor in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldProg (mapProg (MapSen.mapTerm (const id) m)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ mapSen (const id) m)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { foldBlock = \ (Ranged _ r) vs p ->
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder Ranged (Block (map (mapVars m) vs) p) r
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder , foldCall = \ (Ranged _ r) f -> case f of
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder Predication (Qual_pred_name i (Pred_type args r1) r2) ts r3 ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case lookupProc i $ msource mor of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> error "mapMorProg"
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder Just pr -> let
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski j = mapProcIdProfile mor i pr
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder nargs = map (mapSrt mor) args
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder nts = map (MapSen.mapTerm (const id) m) ts
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in Ranged (Call $ Predication
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Qual_pred_name j (Pred_type nargs r1) r2) nts r3) r
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder _ -> error $ "mapMorProg " ++ show f }
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapProcId :: Morphism f Procs VSEMorExt -> Id -> Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapProcId m i = case lookupProc i $ msource m of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just p -> mapProcIdProfile m i p
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> error $ "VSE.mapProcId unknown " ++ show i
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermapProcIdProfile :: Morphism f Procs VSEMorExt -> Id -> Profile -> Id
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermapProcIdProfile m = mapProcIdProfileExt (sort_map m) (op_map m) (pred_map m)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaedermapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> Id -> Profile -> Id
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaedermapProcIdProfileExt sm om pm i p = case profileToOpType p of
cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski Just t -> fst $ mapOpSym sm om (i, t)
8001ead00e2d306a1cf4735a3d2c1378fc8e3e31Christian Maeder Nothing -> fst $ mapPredSym sm pm (i, profileToPredType p)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapMorDefproc m (Defproc k i vs p r) =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Defproc k (mapProcId m i) vs (mapMorProg m p) r
(map (MapSen.mapConstr m) constr)
$ Map.toList restr)
_ -> error "VSE.Ana.simpProg" }
else sign { varMap = Map.fromList $ zipWith
{ foldAssign = \ _ v t -> (case Map.lookup v $ varMap sig of
Just s -> Set.insert (v, s)
Nothing -> Set.insert (v, sortOfTerm t)) $ ft t
Set.difference (freeProgVars (execState (mapM_ addVars vs) sig) p)
$ Set.fromList $ flatVAR_DECLs vs
_ -> error "VSE.Ana.freeProgVars" }
Dlformula _ p s -> Set.union (freeProgVars (castSign sig) p) $
Defprocs _ -> Set.empty
RestrictedConstraint _ _ _ -> Set.empty
inducedExt sm om pm _ = Procs . Map.fromList
. Map.toList . procsMap . extendedInfo
{ extendedInfo = Procs $ Map.filterWithKey (\ i p -> case profileToOpType p of
Just t -> let s = MapSet.lookup i $ opMap sig in
toSen = foldFormula $ mapRecord (error "CASL2VSEImport.mapSen")
Map.Map Int VSEMor ->
(Procs, Map.Map Int VSEMorExt)
procs = Map.fromList $ nub $
phi = Map.findWithDefault (error "extVSEColimit") n morMap
Map.toList p) $
in (Procs procs, Map.fromList $ map (\ n -> (n, emptyMorExt)) $
sm = Map.toList $ sort_map m
eqOps = Map.fromList $ map (\ (s, t) ->
restrPreds = Map.fromList $ map (\ (s, t) ->
opsProcs = Map.fromList $ map (\ ((idN, OpType _ w s), (idN', _)) ->
, (mkGenName idN', Partial))) $ Map.toList om
predProcs = Map.fromList $ map (\ ((idN, PredType w), idN') ->
((mkGenName idN, PredType w), mkGenName idN')) $ Map.toList pm