c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2004-2005

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederMaintainer : luettich@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederPortability : portable

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederstatic analysis of modal logic parts

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule Modal.StatAna where

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Modal.AS_Modal

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Modal.Print_AS()

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Modal.ModalSign

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport CASL.Sign

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport CASL.MixfixParser

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport CASL.StaticAna

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport CASL.Utils

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport CASL.AS_Basic_CASL

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport CASL.ShowMixfix

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport CASL.Overload

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport CASL.Inject

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.AS_Annotation

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.GlobalAnnotations

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport qualified Common.Lib.Map as Map

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport qualified Common.Lib.Set as Set

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Common.Lib.State

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Id

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Common.Result

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaederbasicModalAnalysis :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Sign M_FORMULA ModalSign, GlobalAnnos)

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Sign M_FORMULA ModalSign,

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder Sign M_FORMULA ModalSign,

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [Named (FORMULA M_FORMULA)])

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederbasicModalAnalysis = basicAnalysis minExpForm ana_M_BASIC_ITEM

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder ana_M_SIG_ITEM ana_Mix diffModalSign

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederana_Mix = emptyMix

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder { getSigIds = ids_M_SIG_ITEM

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder , putParen = mapM_FORMULA

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , mixResolve = resolveM_FORMULA

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder , checkMix = noExtMixfixM

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , putInj = injM_FORMULA }

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- rigid ops will also be part of the CASL signature

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederids_M_SIG_ITEM si = case si of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Rigid_op_items _ al _ ->

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Rigid_pred_items _ al _ ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedermapMODALITY :: MODALITY -> MODALITY

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermapMODALITY m = case m of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Term_mod t -> Term_mod $ mapTerm mapM_FORMULA t

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> m

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedermapM_FORMULA :: M_FORMULA -> M_FORMULA

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedermapM_FORMULA (BoxOrDiamond b m f ps) =

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder BoxOrDiamond b (mapMODALITY m) (mapFormula mapM_FORMULA f) ps

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederinjMODALITY :: MODALITY -> MODALITY

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederinjMODALITY m = case m of

f94e26f892cf0fe2aa54252ec98920aed3a5c5ecChristian Maeder Term_mod t -> Term_mod $ injTerm injM_FORMULA t

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> m

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederinjM_FORMULA :: M_FORMULA -> M_FORMULA

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederinjM_FORMULA (BoxOrDiamond b m f ps) =

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder BoxOrDiamond b (injMODALITY m) (injFormula injM_FORMULA f) ps

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederresolveMODALITY :: MixResolve MODALITY

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederresolveMODALITY ga ids m = case m of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Term_mod t -> fmap Term_mod $ resolveMixTrm mapM_FORMULA

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder resolveM_FORMULA ga ids t

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder _ -> return m

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveM_FORMULA :: MixResolve M_FORMULA

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveM_FORMULA ga ids cf = case cf of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder BoxOrDiamond b m f ps -> do

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder nm <- resolveMODALITY ga ids m

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder nf <- resolveMixFrm mapM_FORMULA resolveM_FORMULA ga ids f

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ BoxOrDiamond b nm nf ps

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedernoExtMixfixM :: M_FORMULA -> Bool

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedernoExtMixfixM mf =

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder let noInner = noMixfixF noExtMixfixM in

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case mf of

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder BoxOrDiamond _ _ f _ -> noInner f

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederminExpForm :: Min M_FORMULA ModalSign

27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaederminExpForm ga s form =

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder let minMod md ps = case md of

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Term_mod t -> let

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder r = do

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder t2 <- oneExpTerm minExpForm ga s t

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder let srt = term_sort t2

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski trm = Term_mod t2

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder if Map.member srt $ termModies $ extendedInfo s

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder then return trm

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder else Result [mkDiag Error

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ("unknown term modality sort '"

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ++ showId srt "' for term") t ]

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder $ Just trm

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder in case t of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Mixfix_token tm ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder if Map.member tm $ modies $ extendedInfo s

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder then return $ Simple_mod tm

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else case maybeResult r of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Nothing -> Result

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder [mkDiag Error "unknown modality" tm]

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder $ Just $ Simple_mod tm

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> r

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> r

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder in case form of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder BoxOrDiamond b m f ps ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder do nm <- minMod m ps

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder f2 <- minExpFORMULA minExpForm ga s f

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ BoxOrDiamond b nm f2 ps

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederana_M_SIG_ITEM :: Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederana_M_SIG_ITEM mix ga mi =

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case mi of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Rigid_op_items r al ps ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder do ul <- mapM (ana_OP_ITEM minExpForm mix ga) al

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case r of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Op_decl ops ty _ _ ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Op_defn i par _ _ ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder updateExtInfo $ addRigidOp (toOpType $ headToType par)

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder i ) ul

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> return ()

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ Rigid_op_items r ul ps

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Rigid_pred_items r al ps ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder do ul <- mapM (ana_PRED_ITEM minExpForm mix ga) al

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case r of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Rigid -> mapM_ ( \ aoi -> case item aoi of

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Pred_decl ops ty _ ->

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Pred_defn i (Pred_head args _) _ _ ->

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder updateExtInfo $ addRigidPred

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (PredType $ sortsOfArgs args) i ) ul

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return ()

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ Rigid_pred_items r ul ps

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederaddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederaddRigidOp ty i m = return

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder m { rigidOps = addOpTo i ty $ rigidOps m }

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederaddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederaddRigidPred ty i m = return

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder m { rigidPreds = let rps = rigidPreds m in Map.insert i

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder (Set.insert ty $ Map.findWithDefault Set.empty i rps) rps }

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederana_M_BASIC_ITEM

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederana_M_BASIC_ITEM mix ga bi = do

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder case bi of

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Simple_mod_decl al fs ps -> do

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mapM_ ((updateExtInfo . preAddModId) . item) al

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder newFs <- mapAnM (ana_FORMULA False mix ga) fs

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mapM_ ((updateExtInfo . addModId newFs) . item) al

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder return $ Simple_mod_decl al newFs ps

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Term_mod_decl al fs ps -> do

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder e <- get

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder mapM_ ((updateExtInfo . preAddModSort e) . item) al

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder newFs <- mapAnM (ana_FORMULA True mix ga) fs

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder mapM_ ((updateExtInfo . addModSort newFs) . item) al

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder return $ Term_mod_decl al newFs ps

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederpreAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederpreAddModId i m =

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder let ms = modies m in

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder if Map.member i ms then

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder Result [mkDiag Hint "repeated modality" i] $ Just m

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder else return m { modies = Map.insert i [] ms }

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederaddModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederaddModId frms i m = return m { modies = Map.insert i frms $ modies m }

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederpreAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder -> Result ModalSign

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederpreAddModSort e i m =

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let ms = termModies m

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ds = hasSort e i

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder in if Map.member i ms || not (null ds) then

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Result (mkDiag Hint "repeated term modality" i : ds) $ Just m

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder else return m { termModies = Map.insert i [] ms }

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder

15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaederaddModSort :: [AnModFORM] -> SORT -> ModalSign -> Result ModalSign

e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederaddModSort frms i m =

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski return m { termModies = Map.insert i frms $ termModies m }

ana_FORMULA

:: Bool

-> Ana (FORMULA M_FORMULA) M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign

ana_FORMULA b mix ga f =

if isPropForm b f then do

let ps = map (mkId . (: [])) $ Set.toList $ getFormPredToks f

pm <- gets predMap

mapM_ (addPred $ PredType []) ps

newGa <- gets globAnnos

let Result es m = resolveFormula mapM_FORMULA

resolveM_FORMULA newGa (mixRules mix) f

addDiags es

e <- get

phi <- case m of

Nothing -> return f

Just r -> resultToState (minExpFORMULA minExpForm ga e) r

e2 <- get

put e2 {predMap = pm}

return phi

else do addDiags [mkDiag Error

"Modality declarations may only contain propositional axioms"

f] >> return f

getFormPredToks :: FORMULA M_FORMULA -> Set.Set Token

getFormPredToks frm = case frm of

Quantification _ _ f _ -> getFormPredToks f

Conjunction fs _ -> Set.unions $ map getFormPredToks fs

Disjunction fs _ -> Set.unions $ map getFormPredToks fs

Implication f1 f2 _ _ ->

Set.union (getFormPredToks f1) $ getFormPredToks f2

Equivalence f1 f2 _ ->

Set.union (getFormPredToks f1) $ getFormPredToks f2

Negation f _ -> getFormPredToks f

Mixfix_formula (Mixfix_token t) -> Set.singleton t

Mixfix_formula t -> getTermPredToks t

ExtFORMULA (BoxOrDiamond _ _ f _) -> getFormPredToks f

Predication _ ts _ -> Set.unions $ map getTermPredToks ts

Definedness t _ -> getTermPredToks t

Existl_equation t1 t2 _ ->

Set.union (getTermPredToks t1) $ getTermPredToks t2

Strong_equation t1 t2 _ ->

Set.union (getTermPredToks t1) $ getTermPredToks t2

Membership t _ _ -> getTermPredToks t

_ -> Set.empty

getTermPredToks :: TERM M_FORMULA -> Set.Set Token

getTermPredToks trm = case trm of

Application _ ts _ -> Set.unions $ map getTermPredToks ts

Sorted_term t _ _ -> getTermPredToks t

Cast t _ _ -> getTermPredToks t

Conditional t1 f t2 _ -> Set.union (getTermPredToks t1) $

Set.union (getFormPredToks f) $ getTermPredToks t2

Mixfix_term ts -> Set.unions $ map getTermPredToks ts

Mixfix_parenthesized ts _ -> Set.unions $ map getTermPredToks ts

Mixfix_bracketed ts _ -> Set.unions $ map getTermPredToks ts

Mixfix_braced ts _ -> Set.unions $ map getTermPredToks ts

_ -> Set.empty

isPropForm :: Bool -> FORMULA M_FORMULA -> Bool

isPropForm b frm = case frm of

Quantification _ _ f _ -> b && isPropForm b f

Conjunction fs _ -> all (isPropForm b) fs

Disjunction fs _ -> all (isPropForm b) fs

Implication f1 f2 _ _ -> isPropForm b f1 && isPropForm b f2

Equivalence f1 f2 _ -> isPropForm b f1 && isPropForm b f2

Negation f _ -> isPropForm b f

Mixfix_formula _ -> True

ExtFORMULA (BoxOrDiamond _ _ f _) -> isPropForm b f

Predication _ _ _ -> True

False_atom _ -> True

True_atom _ -> True

_ -> False