StatAna.hs revision 6caada8926a23123aee618f61d64fe82cfd6e91e
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
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm :: Min M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm ga s form =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let newGa = addAssocs ga s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ops = formulaIds s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder preds = allPredIds s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder res = resolveFormula newGa ops preds
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder minMod md ps = case md of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Term_mod t -> let
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder t1 <- resolveMixfix newGa (allOpIds s) preds False t
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ts <- minExpTerm minExpForm ga s t1
36968f55942e973058ae8d1e2ac69c6f5d53a681Christian Maeder t2 <- is_unambiguous t ts ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let srt = term_sort t2
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder trm = Term_mod t2
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder if Set.member srt $ termModies $ extendedInfo s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder then return trm
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder else Result [mkDiag Error
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ("unknown term modality sort '"
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ++ showId srt "' for term") t ]
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Mixfix_token tm ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder if Set.member tm $ modies $ extendedInfo s
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder then return $ Simple_mod tm
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder else case maybeResult r of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Nothing -> Result
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder [mkDiag Error "unknown modality" tm]
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder $ Just $ Simple_mod tm
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder in case form of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Box m f ps ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder do nm <- minMod m ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder f2 <- minExpFORMULA minExpForm ga s f1
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Box nm f2 ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Diamond m f ps ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder do nm <- minMod m ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder f2 <- minExpFORMULA minExpForm ga s f1
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian 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 ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder do ul <- mapM (ana_OP_ITEM ga) al
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Op_decl ops ty _ _ ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Op_defn i par _ _ ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder updateExtInfo $ addRigidOp (toOpType $ headToType par)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder _ -> return ()
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Rigid_op_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid_pred_items r al ps ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder do ul <- mapM (ana_PRED_ITEM ga) al
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Pred_decl ops ty _ ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Pred_defn i (Pred_head args _) _ _ ->
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder updateExtInfo $ addRigidPred
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (PredType $ sortsOfArgs args) i ) ul
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder _ -> return ()
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Rigid_pred_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp ty i m = return
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder m { rigidOps = addTo i ty { opKind = Partial } $ rigidOps m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred ty i m = return
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder m { rigidPreds = addTo 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
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder mapM_ ((updateExtInfo . addModId) . item) al
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski newFs <- mapAnM (resultToState (ana_M_FORMULA False)) fs
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder return $ Simple_mod_decl al newFs ps
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder Term_mod_decl al fs ps -> do
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder mapM_ ((updateExtInfo . addModSort e) . item) al
b97b5d4285b3b17eae6258b3ec35708dd392dd80Till Mossakowski newFs <- mapAnM (resultToState (ana_M_FORMULA True)) fs
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian 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
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddModId i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let ms = modies m in
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Result [mkDiag Hint "repeated modality" i] $ Just m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder else return m { modies = Set.insert i ms }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddModSort e i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let ms = termModies m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ds = hasSort e i
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder in if Set.member i ms || not (null ds) then
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Result (mkDiag Hint "repeated term modality" i : ds) $ Just m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder else return m { termModies = Set.insert i ms }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermap_M_FORMULA :: MapSen M_FORMULA ModalSign ()
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermap_M_FORMULA mor frm =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let mapMod m = case m of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Simple_mod _ -> return m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Term_mod t -> do newT <- mapTerm map_M_FORMULA mor t
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Term_mod newT
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder in case frm of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Box m f ps -> do
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newF <- mapSen map_M_FORMULA mor f
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newM <- mapMod m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Box newM newF ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Diamond m f ps -> do
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newF <- mapSen map_M_FORMULA mor f
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder newM <- mapMod m
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian 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)