StatAna.hs revision bd2fcea378d43e789ef682e0f14096149f72410b
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
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
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder Simple_mod_decl al _ _ -> mapM_ ((updateExtInfo . addModId) . item) al
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder Term_mod_decl al _ _ ->
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder mapM_ ((updateExtInfo . addModSort e) . item) al
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
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA :: FORMULA M_FORMULA -> Result (FORMULA M_FORMULA)
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (Conjunction phis pos) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phis' <- mapM ana_M_FORMULA phis
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Conjunction phis' pos)
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (Disjunction phis pos) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phis' <- mapM ana_M_FORMULA phis
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Disjunction phis' pos)
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (Implication phi1 phi2 b pos) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi1' <- ana_M_FORMULA phi1
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi2' <- ana_M_FORMULA phi2
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Implication phi1' phi2' b pos)
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (Equivalence phi1 phi2 pos) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi1' <- ana_M_FORMULA phi1
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi2' <- ana_M_FORMULA phi2
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Equivalence phi1' phi2' pos)
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (Negation phi pos) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi' <- ana_M_FORMULA phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return (Negation phi' pos)
e318fd2335b27b19a602bf7f2fc068897df1e4eaTill Mossakowskiana_M_FORMULA phi@(True_atom _) = return phi
e318fd2335b27b19a602bf7f2fc068897df1e4eaTill Mossakowskiana_M_FORMULA phi@(False_atom _) = return phi
bd2fcea378d43e789ef682e0f14096149f72410bTill Mossakowskiana_M_FORMULA (Mixfix_formula (Mixfix_token ident)) =
bd2fcea378d43e789ef682e0f14096149f72410bTill Mossakowski return (Predication (Qual_pred_name (mkId [ident])
bd2fcea378d43e789ef682e0f14096149f72410bTill Mossakowski (Pred_type [] []) [])
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (ExtFORMULA (Box m phi pos)) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi' <- ana_M_FORMULA phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return(ExtFORMULA (Box m phi' pos))
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA (ExtFORMULA (Diamond m phi pos)) = do
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski phi' <- ana_M_FORMULA phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski return(ExtFORMULA (Diamond m phi' pos))
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowskiana_M_FORMULA phi =
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski plain_error phi
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski "Modality declarations may only contain propositional axioms"