StatAna.hs revision 0e2ae85e2453466d03c1fc5884a3d693235bb9d9
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule : $Header$
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2004
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederMaintainer : hets@tzi.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability : provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability : portable
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder static analysis of modal logic parts
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski check quantifiers (sorts, variables in body) in ana_M_FORMULA
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport qualified Common.Lib.Set as Set
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowskiimport qualified Common.Lib.Map as Map
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm :: Min M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm ga s form =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let newGa = addAssocs ga s
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ops = formulaIds s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder preds = allPredIds s
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder res = resolveFormula newGa ops preds
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder minMod md ps = case md of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Term_mod t -> let
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder t1 <- resolveMixfix newGa (allOpIds s) preds t
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ts <- minExpTerm minExpForm ga s t1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder t2 <- is_unambiguous t ts ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let srt = term_sort t2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder trm = Term_mod t2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder if Map.member srt $ termModies $ extendedInfo s
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder then return trm
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else Result [mkDiag Error
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ("unknown term modality sort '"
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ++ showId srt "' for term") t ]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Mixfix_token tm ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder if Map.member tm $ modies $ extendedInfo s
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder then return $ Simple_mod tm
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else case maybeResult r of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Nothing -> Result
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder [mkDiag Error "unknown modality" tm]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ Just $ Simple_mod tm
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder in case form of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Box m f ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do nm <- minMod m ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder f2 <- minExpFORMULA minExpForm ga s f1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Box nm f2 ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Diamond m f ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do nm <- minMod m ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder f2 <- minExpFORMULA minExpForm ga s f1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Diamond nm f2 ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_SIG_ITEM :: Ana M_SIG_ITEM M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_SIG_ITEM ga mi =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid_op_items r al ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do ul <- mapM (ana_OP_ITEM ga) al
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Op_decl ops ty _ _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Op_defn i par _ _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder updateExtInfo $ addRigidOp (toOpType $ headToType par)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder _ -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Rigid_op_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid_pred_items r al ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do ul <- mapM (ana_PRED_ITEM ga) al
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Pred_decl ops ty _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Pred_defn i (Pred_head args _) _ _ ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder updateExtInfo $ addRigidPred
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (PredType $ sortsOfArgs args) i ) ul
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder _ -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Rigid_pred_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp ty i m = return
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder m { rigidOps = addOpTo i ty $ rigidOps m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred ty i m = return
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder m { rigidPreds = Map.setInsert i ty $ rigidPreds m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_BASIC_ITEM :: Ana M_BASIC_ITEM M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_BASIC_ITEM _ bi = do
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder Simple_mod_decl al fs ps -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newFs <- mapAnM (resultToState (ana_M_FORMULA False)) fs
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mapM_ ((updateExtInfo . addModId newFs) . item) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Simple_mod_decl al newFs ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Term_mod_decl al fs ps -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newFs <- mapAnM (resultToState (ana_M_FORMULA True)) fs
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mapM_ ((updateExtInfo . addModSort newFs e) . item) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Term_mod_decl al newFs ps
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian MaederresultToState :: (a -> Result a) -> a -> State (Sign f e) a
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian MaederresultToState f a = do
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder addDiags $ reverse $ diags r
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder case maybeResult r of
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder Nothing -> return a
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder Just b -> return b
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till MossakowskiaddModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till MossakowskiaddModId frms i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let ms = modies m in
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Result [mkDiag Hint "repeated modality" i] $ Just m
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski else return m { modies = Map.insert i frms ms }
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till MossakowskiaddModSort :: [AnModFORM] ->
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till MossakowskiaddModSort frms e i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let ms = termModies m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ds = hasSort e i
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski in if Map.member i ms || not (null ds) then
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Result (mkDiag Hint "repeated term modality" i : ds) $ Just m
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski else return m { termModies = Map.insert i frms ms }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermap_M_FORMULA :: MapSen M_FORMULA ModalSign ()
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermap_M_FORMULA mor frm =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let mapMod m = case m of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Simple_mod _ -> return m
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Term_mod t -> do newT <- mapTerm map_M_FORMULA mor t
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Term_mod newT
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder in case frm of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Box m f ps -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newF <- mapSen map_M_FORMULA mor f
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newM <- mapMod m
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Box newM newF ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Diamond m f ps -> do
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newF <- mapSen map_M_FORMULA mor f
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder newM <- mapMod m
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ Diamond newM newF ps
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA :: Bool -> FORMULA M_FORMULA -> Result (FORMULA M_FORMULA)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (Conjunction phis pos) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phis' <- mapM (ana_M_FORMULA b) phis
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Conjunction phis' pos)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (Disjunction phis pos) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phis' <- mapM (ana_M_FORMULA b) phis
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Disjunction phis' pos)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (Implication phi1 phi2 b1 pos) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi1' <- ana_M_FORMULA b phi1
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi2' <- ana_M_FORMULA b phi2
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski return (Implication phi1' phi2' b1 pos)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (Equivalence phi1 phi2 pos) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi1' <- ana_M_FORMULA b phi1
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi2' <- ana_M_FORMULA b phi2
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Equivalence phi1' phi2' pos)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (Negation phi pos) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi' <- ana_M_FORMULA b phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Negation phi' pos)
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(True_atom _) = return phi
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(False_atom _) = return phi
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ (Mixfix_formula (Mixfix_token ident)) =
bd2fcea378d43e789ef682e0f14096149f72410bTill Mossakowski return (Predication (Qual_pred_name (mkId [ident])
bd2fcea378d43e789ef682e0f14096149f72410bTill Mossakowski (Pred_type [] []) [])
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (ExtFORMULA (Box m phi pos)) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi' <- ana_M_FORMULA b phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return(ExtFORMULA (Box m phi' pos))
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b (ExtFORMULA (Diamond m phi pos)) = do
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski phi' <- ana_M_FORMULA b phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return(ExtFORMULA (Diamond m phi' pos))
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA b phi@(Quantification _ _ phi1 pos) =
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski if b then ana_M_FORMULA b phi1
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski else anaError phi pos
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Predication _ _ pos) =
ae3f41e377915dbff957ad6e46efe3cc42ec7e60Till Mossakowski return phi -- should lookup predicate!
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Definedness _ pos) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi pos
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Existl_equation _ _ pos) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi pos
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Strong_equation _ _ pos) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi pos
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Membership _ _ pos) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi pos
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Mixfix_formula _) =
ae3f41e377915dbff957ad6e46efe3cc42ec7e60Till Mossakowski return phi -- should do mixfix analysis and lookup predicate!
ae3f41e377915dbff957ad6e46efe3cc42ec7e60Till Mossakowski -- anaError phi [nullPos]
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowskiana_M_FORMULA _ phi@(Unparsed_formula _ pos) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi pos
6caada8926a23123aee618f61d64fe82cfd6e91eTill Mossakowskiana_M_FORMULA _ phi@(Sort_gen_ax _ _) =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski anaError phi [nullPos]
3a56a4779ffd06f0d878e6926230a38bb92d5601Till MossakowskianaError :: a -> [Pos] -> Result a
3a56a4779ffd06f0d878e6926230a38bb92d5601Till MossakowskianaError phi pos =
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski plain_error phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski "Modality declarations may only contain propositional axioms"
3a56a4779ffd06f0d878e6926230a38bb92d5601Till Mossakowski (headPos pos)