Ana.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx{-# LANGUAGE TypeSynonymInstances #-}
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxModule : $Header$
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxDescription : static analysis of VSE parts
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxCopyright : (c) C. Maeder, DFKI Bremen 2008
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxLicense : GPLv2 or higher
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxMaintainer : Christian.Maeder@dfki.de
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxStability : provisional
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxPortability : portable
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxanalysis of VSE logic extension of CASL
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , uBoolean
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , constBoolType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , lookupProc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , procsToOpMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , procsToPredMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , profileToOpType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , profileToPredType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , checkCases
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , basicAna
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , mapDlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , minExpForm
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , simpDlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , correctSign
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , correctTarget
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , inducedExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , VSEMorExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , VSEBasicSpec
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , extVSEColimit
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , vseMorExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport Data.Char (toLower)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport qualified Data.Map as Map
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport qualified Data.Set as Set
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport qualified Common.Lib.Rel as Rel
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport Common.Utils (hasMany)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport CASL.MapSentence as MapSen
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hximport CASL.ShowMixfix as Paren
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtype VSESign = Sign Dlformula Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVariables :: Sentence -> Set.Set Token
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVariables = foldFormula $ getVarsRec $ getVSEVars . unRanged
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVarsRec :: (f -> Set.Set Token) -> Record f (Set.Set Token) (Set.Set Token)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVarsRec f =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { foldQuantification = \ _ _ vs r _ -> Set.union r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ Set.fromList $ map fst $ flatVAR_DECLs vs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldQual_var = \ _ v _ _ -> Set.singleton v }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVSEVars :: VSEforms -> Set.Set Token
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetVSEVars vf = case vf of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula _ p s -> Set.union (getProgVars p) $ getVariables s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs l -> Set.unions $ map getDefprogVars l
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> Set.empty -- no variables in a sort generation constraint
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetProgVars :: Program -> Set.Set Token
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetProgVars =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let vrec = getVarsRec $ const Set.empty
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx getTermVars = foldTerm vrec
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx getCondVars = foldFormula vrec
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in foldProg (progToSetRec getTermVars getCondVars)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { foldAssign = \ _ v t -> Set.insert v $ getTermVars t
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldBlock = \ _ vs p -> Set.union p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ Set.fromList $ map fst $ flatVAR_DECLs vs }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetDefprogVars :: Defproc -> Set.Set Token
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetDefprogVars (Defproc _ _ vs p _) = Set.union (getProgVars p)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtokenToLower :: Token -> Token
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtokenToLower (Token s r) = Token (map toLower s) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxidToLower :: Id -> Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxidToLower (Id ts cs r) = Id (map tokenToLower ts) (map idToLower cs) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetCases :: String -> Set.Set Id -> [Diagnosis]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetCases msg =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx map (mkDiag Error ("overlapping " ++ msg ++ " identifiers") . Set.toList)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx . filter hasMany . Map.elems
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx . Set.fold (\ i -> Rel.setInsert (idToLower i) i) Map.empty
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetCaseDiags :: Sign f e -> [Diagnosis]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxgetCaseDiags sig =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx getCases "sort" (sortSet sig)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ++ getCases "op or function" (Map.keysSet $ opMap sig)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ++ getCases "pred or proc" (Map.keysSet $ predMap sig)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuBoolean :: Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuBoolean = stringToId "Boolean"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuTrue :: Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuTrue = stringToId "True"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuFalse :: Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuFalse = stringToId "False"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtBoolean :: OP_TYPE
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtBoolean = Op_type Total [] uBoolean nullRange
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxconstBoolType :: OpType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxconstBoolType = toOpType tBoolean
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqBoolean :: Id -> OP_SYMB
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqBoolean c = Qual_op_name c tBoolean nullRange
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqTrue :: OP_SYMB
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqTrue = qBoolean uTrue
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqFalse :: OP_SYMB
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxqFalse = qBoolean uFalse
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmkConstAppl :: OP_SYMB -> TERM f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmkConstAppl o = Application o [] nullRange
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaTrue :: TERM f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaTrue = mkConstAppl qTrue
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaFalse :: TERM f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaFalse = mkConstAppl qFalse
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuOpMap :: OpMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxuOpMap = Map.fromList $ map (\ c -> (c, Set.singleton constBoolType))
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx [uFalse, uTrue]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxboolSig :: Sign f Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxboolSig = (emptySign emptyProcs)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { sortSet = Set.singleton uBoolean
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , opMap = uOpMap }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxlookupProc :: Id -> Sign f Procs -> Maybe Profile
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxlookupProc i = Map.lookup i . procsMap . extendedInfo
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprocsSign :: Sign f Procs -> Sign f Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprocsSign sig = (emptySign emptyProcs)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { predMap = procsToPredMap $ extendedInfo sig }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | add procs as predicate
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaddProcs :: Sign f Procs -> Sign f Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaddProcs sig = addSig const sig $ procsSign sig
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | remove procs as predicate
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsubProcs :: Sign f Procs -> Sign f Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsubProcs sig = diffSig const sig $ procsSign sig
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcheckCases :: Sign f e -> [Named Sentence] -> [Diagnosis]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcheckCases sig2 sens = getCaseDiags sig2 ++ concatMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (getCases "var" . Set.map simpleIdToId . getVariables . sentence) sens
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtype VSEBasicSpec = BASIC_SPEC () Procdecls Dlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxbasicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxbasicAna (bs, sig, ga) = do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let sigIn = subProcs $ addSig const sig boolSig
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (bs2, ExtSign sig2 syms, sens) <-
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx basicAnalysis minExpForm (const return) anaProcdecls anaMix
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (bs, sigIn, ga)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx appendDiags $ checkCases sig2 sens
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx appendDiags $ map
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (mkDiag Error "illegal predicate declaration for procedure")
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ Map.keys $ interMapSet (diffMapSet (predMap sig2) $ predMap sigIn)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ procsToPredMap $ extendedInfo sig2
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let sig3 = diffSig const sig2 boolSig
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (rSens, fSens) = partition (foldFormula (checkRec True) . sentence) sens
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx appendDiags $ map (mkDiag Error "unsupported VSE formula" . sentence) fSens
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx appendDiags $ map (mkDiag Error "illegal overloading of")
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ Set.toList $ Set.intersection (Map.keysSet $ opMap sig3)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return (bs2, ExtSign (addProcs $ diffSig const sig2 boolSig) syms, rSens)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxanaMix :: Mix () Procdecls Dlformula Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxanaMix = emptyMix
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { putParen = parenDlFormula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , mixResolve = resolveDlformula }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | put parens around ambiguous mixfix formulas (for error messages)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenDlFormula :: Dlformula -> Dlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenDlFormula (Ranged f r) = case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula b p s ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let n = mapFormula parenDlFormula s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in Ranged (Dlformula b (parenProg p) n) r
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf Defprocs ps -> Ranged (Defprocs $ map parenDefproc ps) r
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf _ -> Ranged f r -- no mixfix formulas?
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenProg :: Program -> Program
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenProg = foldProg $ mapProg (Paren.mapTerm id) $ mapFormula id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenDefproc :: Defproc -> Defproc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparenDefproc (Defproc k i vs p r) = Defproc k i vs (parenProg p) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprocsToPredMap (Procs m) =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx foldr (\ (n, pr@(Profile _ mr)) pm -> case mr of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Rel.setInsert n (profileToPredType pr) pm
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprocsToOpMap :: Procs -> OpMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprocsToOpMap (Procs m) =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx foldr (\ (n, pr) om -> case profileToOpType pr of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just ot -> Rel.setInsert n ot om
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | resolve mixfix applications of terms and formulas
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveDlformula :: MixResolve Dlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveDlformula ga rules (Ranged f r) = case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula b p s -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- resolveProg ga rules p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx n <- resolveMixFrm id resolveDlformula ga rules s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Dlformula b np n) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs ps -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nps <- mapM (resolveDefproc ga rules) ps
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Defprocs nps) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> return $ Ranged f r -- no mixfix?
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveT :: MixResolve (TERM ())
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveT = resolveMixTrm id (mixResolve emptyMix)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveF :: MixResolve (FORMULA ())
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveF = resolveMixFrm id (mixResolve emptyMix)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveProg :: MixResolve Program
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveProg ga rules p@(Ranged prg r) = case prg of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Abort -> return p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Skip -> return p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Assign v t -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nt <- resolveT ga rules t
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Assign v nt) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Call f -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nf <- resolveF ga rules f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Call nf) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Return t -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nt <- resolveT ga rules t
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan return $ Ranged (Return nt) r
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan Block vs q -> do
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan np <- resolveProg ga rules q
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer return $ Ranged (Block vs np) r
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer Seq p1 p2 -> do
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer p3 <- resolveProg ga rules p1
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx p4 <- resolveProg ga rules p2
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Seq p3 p4) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx If f p1 p2 -> do
6f12def440a1ce798ab128210a43414d173669f0pengcheng chen - Sun Microsystems - Beijing China c <- resolveF ga rules f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx p3 <- resolveProg ga rules p1
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx p4 <- resolveProg ga rules p2
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (If c p3 p4) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx While f q -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx c <- resolveF ga rules f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- resolveProg ga rules q
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (While c np) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveDefproc :: MixResolve Defproc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxresolveDefproc ga rules (Defproc k i vs p r) = do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- resolveProg ga rules p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Defproc k i vs np r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | resolve overloading and type check terms and formulas
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpForm :: Min Dlformula Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpForm sign (Ranged f r) = let sig = castSign sign in case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula b p s -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- minExpProg Set.empty Nothing sig p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx n <- minExpFORMULA minExpForm sign s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Dlformula b np n) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs ps -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nps <- mapM (minProcdecl sig) ps
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Defprocs nps) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> fail "nyi for restricted constraints"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxoneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxoneExpT = oneExpTerm (const return)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpF = minExpFORMULA (const return)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcheckRec :: Bool -> Record f Bool Bool
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcheckRec b = (constRecord (const False) and True)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { foldQuantification = \ _ _ _ _ _ -> b
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldDefinedness = \ _ _ _ -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldExistl_equation = \ _ _ _ _ -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldMembership = \ _ _ _ _ -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldCast = \ _ _ _ _ -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldConditional = \ _ _ _ _ _ -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldExtFORMULA = \ _ _ -> b }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx -> Program -> Result Program
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminExpProg invars res sig p@(Ranged prg r) = let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx checkCond f = if foldFormula (checkRec False) f then return f else
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx mkError "illegal formula" f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx checkTerm t = if foldTerm (checkRec False) t then return t else
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx mkError "illegal term" t
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in case prg of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Abort -> return p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Skip -> return p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Assign v t -> case Map.lookup v $ varMap sig of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Result [mkDiag Error "undeclared program variable" v] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nt <- oneExpT sig $ Sorted_term t s r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx checkTerm nt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx when (Set.member v invars)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ appendDiags [mkDiag Warning "assignment to input variable" v]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Assign v nt) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Call f -> case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Predication ps ts _ -> let i = predSymbName ps in
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx case lookupProc i sig of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just pr@(Profile l re) -> let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nl = case re of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> l
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> l ++ [Procparam Out s]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in if length nl /= length ts then
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Result [mkDiag Error "non-matching number of parameters for" i]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx sign <- if length l < length nl then
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Result [mkDiag Warning "function used as procedure" i] $ Just
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx sig { predMap = Rel.setInsert i (funProfileToPredType pr)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ predMap sig }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx else return sig { predMap = Rel.setInsert i (profileToPredType pr)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ predMap sig }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nf <- minExpF sign f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx checkCond nf
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Call nf) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> Result [mkDiag Error "no procedure call" f] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Return t -> case res of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Result [mkDiag Error "unexpected return statement" t] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nt <- oneExpT sig $ Sorted_term t s r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Return nt) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Block vs q -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let sign' = execState (mapM_ addVSEVars vs) sig { envDiags = [] }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx appendDiags $ envDiags sign'
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- minExpProg invars res sign' q
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (Block vs np) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Seq p1 p2 -> do
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer p3 <- minExpProg invars res sig p1
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan p4 <- minExpProg invars res sig p2
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan return $ Ranged (Seq p3 p4) r
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan If f p1 p2 -> do
bcb5c89da22515e2ccf139578bad3caebcd716adSowmini Varadhan c <- minExpF sig f
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer p3 <- minExpProg invars res sig p1
0dc2366f7b9f9f36e10909b1e95edbf2a261c2acVenugopal Iyer p4 <- minExpProg invars res sig p2
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (If c p3 p4) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx While f q -> do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx c <- minExpF sig f
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx checkCond c
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- minExpProg invars res sig q
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Ranged (While c np) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaddVSEVars :: VAR_DECL -> State (Sign f Procs) ()
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxaddVSEVars vd@(Var_decl vs _ _) = do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx addVars vd
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx p <- gets $ procsMap . extendedInfo
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx mapM_ (addDiags . checkWithOtherMap "var" "procedure" p . simpleIdToId) vs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminProcdecl :: Sign () Procs -> Defproc -> Result Defproc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxminProcdecl sig (Defproc k i vs p r) = case lookupProc i sig of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just (Profile l re) -> if length vs /= length l then
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Result [mkDiag Error "unknown procedure" i] Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let invars = Set.fromList $ map fst $
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx filter (\ (_, Procparam j _) -> j == In) $ zip vs l
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx np <- minExpProg invars re sig { varMap = Map.fromList $ zipWith
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (\ v (Procparam _ s) -> (v, s)) vs l } p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx return $ Defproc k i vs np r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | analyse and add procedure declarations
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxanaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxanaProcdecls _ ds@(Procdecls ps _) = do
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx mapM_ (anaProcdecl . item) ps
19b23afcc35b3926d062efc1930e65c5fed1084dhxanaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()
19b23afcc35b3926d062efc1930e65c5fed1084dhxanaProcdecl (Procedure i p@(Profile ps mr) q) = do
19b23afcc35b3926d062efc1930e65c5fed1084dhx let prM = predMap e
19b23afcc35b3926d062efc1930e65c5fed1084dhx ea = emptyAnno ()
09539a3c2da6fef054f5306232ef0480de261eabpengcheng chen - Sun Microsystems - Beijing China isPred = case mr of
09539a3c2da6fef054f5306232ef0480de261eabpengcheng chen - Sun Microsystems - Beijing China Nothing -> Set.member (profileToPredType p) l
09539a3c2da6fef054f5306232ef0480de261eabpengcheng chen - Sun Microsystems - Beijing China _ -> False
09539a3c2da6fef054f5306232ef0480de261eabpengcheng chen - Sun Microsystems - Beijing China updateExtInfo (\ pm@(Procs m) ->
09539a3c2da6fef054f5306232ef0480de261eabpengcheng chen - Sun Microsystems - Beijing China let n = Procs $ Map.insert i p m in case Map.lookup i m of
d40f4da491abdcae192eb797766f5f44772a832fpengcheng chen - Sun Microsystems - Beijing China Just o -> if p == o then
d40f4da491abdcae192eb797766f5f44772a832fpengcheng chen - Sun Microsystems - Beijing China hint n ("repeated procedure " ++ showId i "") q
d40f4da491abdcae192eb797766f5f44772a832fpengcheng chen - Sun Microsystems - Beijing China else plain_error pm
19b23afcc35b3926d062efc1930e65c5fed1084dhx ("cannot change profile of procedure " ++ showId i "") q
d40f4da491abdcae192eb797766f5f44772a832fpengcheng chen - Sun Microsystems - Beijing China Nothing -> if isPred then plain_error pm
19b23afcc35b3926d062efc1930e65c5fed1084dhx ("cannot change predicate to procedure " ++ showId i "") q
d40f4da491abdcae192eb797766f5f44772a832fpengcheng chen - Sun Microsystems - Beijing China else return n)
19b23afcc35b3926d062efc1930e65c5fed1084dhx case profileToOpType p of
19b23afcc35b3926d062efc1930e65c5fed1084dhx Just t -> do
19b23afcc35b3926d062efc1930e65c5fed1084dhx unless (all (\ (Procparam j _) -> j == In) ps)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ addDiags [mkDiag Warning "function must have IN params only" i]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx addOp ea t i
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> unless isPred
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ addAnnoSet ea $ Symbol i $ PredAsItemType $ profileToPredType p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparamsToArgs :: [Procparam] -> [SORT]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxparamsToArgs = map (\ (Procparam _ s) -> s)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprofileToPredType :: Profile -> PredType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprofileToPredType (Profile a _) = PredType $ paramsToArgs a
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxfunProfileToPredType :: Profile -> PredType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxfunProfileToPredType (Profile a r) = case r of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> error "funProfileToPredType"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> PredType $ paramsToArgs a ++ [s]
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprofileToOpType :: Profile -> Maybe OpType
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxprofileToOpType (Profile a r) = case r of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> Nothing
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> Just $ OpType Partial (paramsToArgs a) s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcastSign :: Sign f e -> Sign a e
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcastSign s = s { sentences = [] }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcastMor :: Morphism f e b -> Morphism a e b
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcastMor m = m
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { msource = castSign $ msource m
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , mtarget = castSign $ mtarget m }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtype VSEMorExt = DefMorExt Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtype VSEMor = Morphism Dlformula Procs VSEMorExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | apply a morphism
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapMorProg mor = let m = castMor mor in
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx foldProg (mapProg (MapSen.mapTerm (const id) m)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ mapSen (const id) m)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { foldBlock = \ (Ranged _ r) vs p ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Ranged (Block (map (mapVars m) vs) p) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldCall = \ (Ranged _ r) f -> case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Predication (Qual_pred_name i (Pred_type args r1) r2) ts r3 ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx case lookupProc i $ msource mor of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> error "mapMorProg"
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just pr -> let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx j = mapProcIdProfile mor i pr
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nargs = map (mapSrt mor) args
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nts = map (MapSen.mapTerm (const id) m) ts
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in Ranged (Call $ Predication
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (Qual_pred_name j (Pred_type nargs r1) r2) nts r3) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx _ -> error $ "mapMorProg " ++ show f }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcId :: Morphism f Procs VSEMorExt -> Id -> Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcId m i = case lookupProc i $ msource m of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just p -> mapProcIdProfile m i p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> error $ "VSE.mapProcId unknown " ++ show i
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcIdProfile :: Morphism f Procs VSEMorExt -> Id -> Profile -> Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcIdProfile m = mapProcIdProfileExt (sort_map m) (op_map m) (pred_map m)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> Id -> Profile -> Id
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProcIdProfileExt sm om pm i p = case profileToOpType p of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just t -> fst $ mapOpSym sm om (i, t)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> fst $ mapPredSym sm pm (i, profileToPredType p)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapMorDefproc m (Defproc k i vs p r) =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defproc k (mapProcId m i) vs (mapMorProg m p) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapDlformula :: MapSen Dlformula Procs VSEMorExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapDlformula m (Ranged f r) = case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula b p s ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let n = mapSen mapDlformula m s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in Ranged (Dlformula b (mapMorProg m p) n) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs ps -> Ranged (Defprocs $ map (mapMorDefproc m) ps) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx RestrictedConstraint constr restr flag ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (RestrictedConstraint
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (map (MapSen.mapConstr m) constr)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ map (\ (s, i) -> (mapSort (sort_map m) s, mapProcId m i))
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | simplify fully qualified terms and formulas for pretty printing sentences
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpProg :: Sign () e -> Program -> Program
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpProg sig =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx foldProg (mapProg (simplifyTerm dummyMin (const id) sig)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ simplifySen dummyMin (const id) sig)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { foldBlock = \ (Ranged (Block vs p) r) _ _ ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Ranged (Block vs $ simpProg
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (execState (mapM_ addVars vs) sig) p) r }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpDefproc :: Sign () Procs -> Defproc -> Defproc
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpDefproc sign (Defproc k i vs p r) =
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx let sig = case lookupProc i sign of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> sign
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just (Profile l _) -> if length vs /= length l then sign
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx else sign { varMap = Map.fromList $ zipWith
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (\ v (Procparam _ s) -> (v, s)) vs l }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in Defproc k i vs (simpProg sig p) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpDlformula :: Sign Dlformula Procs -> Dlformula -> Dlformula
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxsimpDlformula sign (Ranged f r) = let sig = castSign sign in case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula b p s -> let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx q = simpProg sig p
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx n = simplifySen minExpForm simpDlformula sign s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in Ranged (Dlformula b q n) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs ps -> Ranged (Defprocs $ map (simpDefproc sig) ps) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx RestrictedConstraint _ _ _ -> Ranged f r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx -- how should this be for restricted constraints?
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | free variables to be universally bound on the top level
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zffreeProgVars :: Sign () e -> Program -> VarSet
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zffreeProgVars sig = let ft = freeTermVars sig in
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf foldProg (progToSetRec ft (freeVars sig))
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf { foldAssign = \ _ v t -> (case Map.lookup v $ varMap sig of
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf Just s -> Set.insert (v, s)
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf Nothing -> Set.insert (v, sortOfTerm t)) $ ft t
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , foldBlock = \ (Ranged (Block vs p) _) _ _ ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Set.difference (freeProgVars (execState (mapM_ addVars vs) sig) p)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ Set.fromList $ flatVAR_DECLs vs }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxfreeDlVars :: Sign Dlformula e -> Dlformula -> VarSet
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxfreeDlVars sig (Ranged f _) = case f of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Dlformula _ p s -> Set.union (freeProgVars (castSign sig) p) $
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx freeVars sig s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Defprocs _ -> Set.empty
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx RestrictedConstraint _ _ _ -> Set.empty
626dff7950e2fd00077128f6e79bacf668f45cf7pengcheng chen - Sun Microsystems - Beijing Chinainstance GetRange (Ranged a) where
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx getRange (Ranged _ r) = r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxinstance FreeVars Dlformula where
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx freeVarsOfExt = freeDlVars
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx-- | adjust procs map in morphism target signature
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcorrectTarget :: Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcorrectTarget m = m
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf { mtarget = correctSign $ mtarget m
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf , msource = correctSign $ msource m }
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zfinducedExt :: InducedSign f Procs VSEMorExt Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxinducedExt sm om pm _ = Procs . Map.fromList
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx . map (\ (i, p) -> (mapProcIdProfileExt sm om pm i p, mapProfile sm p))
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx . Map.toList . procsMap . extendedInfo
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcorrectSign :: Sign f Procs -> Sign f Procs
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxcorrectSign sig = sig
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx { extendedInfo = Procs $ Map.filterWithKey (\ i p -> case profileToOpType p of
3a1a8936dac0ebe7e956fa122b0b0d15e62d4108zf Just t -> case Map.lookup i $ opMap sig of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> Set.member t s || Set.member t { opKind = Total } s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> False
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> case Map.lookup i $ predMap sig of
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Just s -> Set.member (profileToPredType p) s
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Nothing -> False) $ procsMap $ extendedInfo sig }
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProfile :: Sort_map -> Profile -> Profile
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxmapProfile m (Profile l r) = Profile
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (map (\ (Procparam k s) -> Procparam k $ mapSort m s) l)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx $ fmap (mapSort m) r
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtoSen :: CASLFORMULA -> Sentence
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxtoSen = foldFormula $ mapRecord (error "CASL2VSEImport.mapSen")
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxextVSEColimit :: Gr Procs (Int, VSEMorExt) ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx Map.Map Int VSEMor ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (Procs, Map.Map Int VSEMorExt)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxextVSEColimit graph morMap = let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx procs = Map.fromList $ nub $
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx concatMap (\ (n, Procs p) -> let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx phi = Map.findWithDefault (error "extVSEColimit") n morMap
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in map (\ (idN, profile) ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx (mapProcId phi idN, mapProfile (sort_map phi) profile)) $
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx labNodes graph
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in (Procs procs, Map.fromList $ map (\ n -> (n, emptyMorExt)) $
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx nodes graph)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxvseMorExt :: CASLMor -> (Op_map, Pred_map)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hxvseMorExt m = let
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx sm = Map.toList $ sort_map m
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx om = op_map m
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx pm = pred_map m
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx eqOps = Map.fromList $ map (\ (s, t) ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ((gnEqName s, OpType Partial [s, s] uBoolean)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , (gnEqName t, Partial))) sm
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx restrPreds = Map.fromList $ map (\ (s, t) ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ((gnRestrName s, PredType [s]), gnRestrName t)) sm
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx opsProcs = Map.fromList $ map (\ ((idN, OpType _ w s), (idN', _)) ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ((mkGenName idN, OpType Partial w s)
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx , (mkGenName idN', Partial))) $ Map.toList om
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx predProcs = Map.fromList $ map (\ ((idN, PredType w), idN') ->
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx ((mkGenName idN, PredType w), mkGenName idN')) $ Map.toList pm
84f7a9b9dca4f23b5f50edef0e59d7eb44301114hx in (Map.union eqOps opsProcs, Map.union restrPreds predProcs)