hets/Modal/StatAna.hs

	StatAna.hs revision bec7e681b0ba4d085638ec7af0cf7ae5068840ca
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- |
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule      :  $Header$
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederCopyright   :  (c) Christian Maeder, Uni Bremen 2004
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederMaintainer  :  hets@tzi.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability   :  provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability :  portable
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder   static analysis of modal logic parts
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermodule Modal.StatAna where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.AS_Modal
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.Print_AS
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.Sign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.MixfixParser
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.StaticAna
02a2037f53b925617df45eb62ca743d777672265Klaus Luettichimport CASL.Utils
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.AS_Basic_CASL
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederimport CASL.ShowMixfix
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.Overload
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederimport CASL.Inject
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.AS_Annotation
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.GlobalAnnotations
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowskiimport qualified Common.Lib.Map as Map
0678d323bee844db79af13113ae252546629a594Christian Maederimport qualified Common.Lib.Set as Set
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Lib.State
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Id
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Result
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian MaederbasicModalAnalysis :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder               Sign M_FORMULA ModalSign, GlobalAnnos)
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder           -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder                  Sign M_FORMULA ModalSign,
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder                  Sign M_FORMULA ModalSign,
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder                  [Named (FORMULA M_FORMULA)])
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederbasicModalAnalysis =
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    basicAnalysis minExpForm ana_M_BASIC_ITEM ana_M_SIG_ITEM diffModalSign
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederinstance Resolver M_FORMULA where
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    putParen = mapM_FORMULA
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    mixResolve = resolveM_FORMULA
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    checkMix = noExtMixfixM
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    putInj = injM_FORMULA
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedermapMODALITY :: MODALITY -> MODALITY
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedermapMODALITY m = case m of
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder    Term_mod t -> Term_mod $ mapTerm mapM_FORMULA t
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder    _ -> m
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedermapM_FORMULA :: M_FORMULA -> M_FORMULA
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedermapM_FORMULA (BoxOrDiamond b m f ps) =
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder    BoxOrDiamond b (mapMODALITY m) (mapFormula mapM_FORMULA f) ps
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederinjMODALITY :: MODALITY -> MODALITY
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederinjMODALITY m = case m of
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    Term_mod t -> Term_mod $ injTerm injM_FORMULA t
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    _ -> m
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederinjM_FORMULA :: M_FORMULA -> M_FORMULA
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian MaederinjM_FORMULA (BoxOrDiamond b m f ps) =
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder    BoxOrDiamond b (injMODALITY m) (injFormula injM_FORMULA f) ps
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederresolveMODALITY :: MixResolve MODALITY
a255351561838b3743d03c1629d335cfb8b83804Christian MaederresolveMODALITY ga ids m = case m of
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder    Term_mod t -> fmap Term_mod $ resolveMixTrm mapM_FORMULA
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder                  resolveM_FORMULA ga ids t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder    _ -> return m
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederresolveM_FORMULA :: MixResolve M_FORMULA
a255351561838b3743d03c1629d335cfb8b83804Christian MaederresolveM_FORMULA ga ids cf = case cf of
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder   BoxOrDiamond b m f ps -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder       nm <- resolveMODALITY ga ids m
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder       nf <- resolveMixFrm mapM_FORMULA resolveM_FORMULA ga ids f
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder       return $ BoxOrDiamond b nm nf ps
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich
02a2037f53b925617df45eb62ca743d777672265Klaus LuettichnoExtMixfixM :: M_FORMULA -> Bool
02a2037f53b925617df45eb62ca743d777672265Klaus LuettichnoExtMixfixM mf =
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich    let noInner = noMixfixF noExtMixfixM in
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich    case mf of
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder    BoxOrDiamond _ _ f _     -> noInner f
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm :: Min M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm ga s form =
5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder    let minMod md ps = case md of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                  Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                  Term_mod t -> let
02a2037f53b925617df45eb62ca743d777672265Klaus Luettich                    r = do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder                      ts <- minExpTerm minExpForm ga s t
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                              $ Just trm
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                    in case t of
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
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                                  _ -> r
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                       _ -> r
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    in case form of
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder        BoxOrDiamond b m f ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder            do nm <- minMod m ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder               f2 <- minExpFORMULA minExpForm ga s f
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder               return $ BoxOrDiamond b nm f2 ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_SIG_ITEM :: Ana M_SIG_ITEM M_FORMULA ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_SIG_ITEM ga mi =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    case mi of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    Rigid_op_items r al ps ->
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder        do ul <- mapM (ana_OP_ITEM mapM_FORMULA resolveM_FORMULA
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder                       noExtMixfixM ga) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           case r of
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)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                                i ) ul
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder               _ -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           return $ Rigid_op_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    Rigid_pred_items r al ps ->
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder        do ul <- mapM (ana_PRED_ITEM mapM_FORMULA
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder                       resolveM_FORMULA noExtMixfixM ga) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           case r of
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 Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp :: OpType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidOp ty i m = return
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder       m { rigidOps = addOpTo i ty $ rigidOps m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred :: PredType -> Id -> ModalSign -> Result ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederaddRigidPred ty i m = return
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder       m { rigidPreds = Map.setInsert i ty $ rigidPreds m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_M_BASIC_ITEM :: Ana M_BASIC_ITEM M_FORMULA ModalSign
91f4f0335ac32768d819e202263f713aef5d7fe6Christian Maederana_M_BASIC_ITEM ga bi = do
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    case bi of
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder        Simple_mod_decl al fs ps -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . preAddModId) . item) al
0678d323bee844db79af13113ae252546629a594Christian Maeder            newFs <- mapAnM (ana_FORMULA False ga) 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
0678d323bee844db79af13113ae252546629a594Christian Maeder            e <- get
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . preAddModSort e) . item) al
0678d323bee844db79af13113ae252546629a594Christian Maeder            newFs <- mapAnM (ana_FORMULA True ga) fs
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . addModSort newFs) . item) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder            return $ Term_mod_decl al newFs ps
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaederpreAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
0678d323bee844db79af13113ae252546629a594Christian MaederpreAddModId i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    let ms = modies m in
b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski    if Map.member i ms then
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder       Result [mkDiag Hint "repeated modality" i] $ Just m
0678d323bee844db79af13113ae252546629a594Christian Maeder       else return m { modies = Map.insert i [] ms }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaederaddModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
0678d323bee844db79af13113ae252546629a594Christian MaederaddModId frms i m = return m { modies = Map.insert i frms $ modies m }
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaederpreAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign
0678d323bee844db79af13113ae252546629a594Christian Maeder              -> Result ModalSign
0678d323bee844db79af13113ae252546629a594Christian MaederpreAddModSort 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
0678d323bee844db79af13113ae252546629a594Christian Maeder       else return m { termModies = Map.insert i [] ms }
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaederaddModSort :: [AnModFORM] -> SORT -> ModalSign -> Result ModalSign
0678d323bee844db79af13113ae252546629a594Christian MaederaddModSort frms i m =
0678d323bee844db79af13113ae252546629a594Christian Maeder       return m { termModies = Map.insert i frms $ termModies m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
0678d323bee844db79af13113ae252546629a594Christian Maederana_FORMULA :: Bool -> Ana (FORMULA M_FORMULA) M_FORMULA ModalSign
0678d323bee844db79af13113ae252546629a594Christian Maederana_FORMULA b ga f =
0678d323bee844db79af13113ae252546629a594Christian Maeder    if isPropForm b f then do
0678d323bee844db79af13113ae252546629a594Christian Maeder           let ps = map (mkId . (: [])) $ Set.toList $ getFormPredToks f
0678d323bee844db79af13113ae252546629a594Christian Maeder           pm <- gets predMap
0678d323bee844db79af13113ae252546629a594Christian Maeder           mapM_ (addPred $ PredType []) ps
0678d323bee844db79af13113ae252546629a594Christian Maeder           ops <- gets formulaIds
0678d323bee844db79af13113ae252546629a594Christian Maeder           preds <- gets allPredIds
0678d323bee844db79af13113ae252546629a594Christian Maeder           newGa <- gets $ addAssocs ga
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder           let Result es m = resolveFormula mapM_FORMULA
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder                             resolveM_FORMULA newGa ops preds f
0678d323bee844db79af13113ae252546629a594Christian Maeder           addDiags es
0678d323bee844db79af13113ae252546629a594Christian Maeder           e <- get
0678d323bee844db79af13113ae252546629a594Christian Maeder           phi <- case m of
0678d323bee844db79af13113ae252546629a594Christian Maeder               Nothing -> return f
0678d323bee844db79af13113ae252546629a594Christian Maeder               Just r -> resultToState (minExpFORMULA minExpForm ga e) r
0678d323bee844db79af13113ae252546629a594Christian Maeder           e2 <- get
0678d323bee844db79af13113ae252546629a594Christian Maeder           put e2 {predMap = pm}
0678d323bee844db79af13113ae252546629a594Christian Maeder           return phi
0678d323bee844db79af13113ae252546629a594Christian Maeder    else do addDiags [mkDiag Error
0678d323bee844db79af13113ae252546629a594Christian Maeder               "Modality declarations may only contain propositional axioms"
0678d323bee844db79af13113ae252546629a594Christian Maeder                f] >> return f
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaedergetFormPredToks :: FORMULA M_FORMULA -> Set.Set Token
0678d323bee844db79af13113ae252546629a594Christian MaedergetFormPredToks frm = case frm of
0678d323bee844db79af13113ae252546629a594Christian Maeder    Quantification _ _ f _ -> getFormPredToks f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Conjunction fs _ -> Set.unions $ map getFormPredToks fs
0678d323bee844db79af13113ae252546629a594Christian Maeder    Disjunction fs _ -> Set.unions $ map getFormPredToks fs
0678d323bee844db79af13113ae252546629a594Christian Maeder    Implication f1 f2 _ _ ->
0678d323bee844db79af13113ae252546629a594Christian Maeder        Set.union (getFormPredToks f1) $ getFormPredToks f2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Equivalence f1 f2 _  ->
0678d323bee844db79af13113ae252546629a594Christian Maeder        Set.union (getFormPredToks f1) $ getFormPredToks f2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Negation f _ -> getFormPredToks f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_formula (Mixfix_token t) -> Set.single t
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_formula t -> getTermPredToks t
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder    ExtFORMULA (BoxOrDiamond _ _ f _) -> getFormPredToks f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Predication _ ts _ -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    Definedness t _ -> getTermPredToks t
0678d323bee844db79af13113ae252546629a594Christian Maeder    Existl_equation t1 t2 _ ->
0678d323bee844db79af13113ae252546629a594Christian Maeder        Set.union (getTermPredToks t1) $ getTermPredToks t2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Strong_equation t1 t2 _ ->
0678d323bee844db79af13113ae252546629a594Christian Maeder        Set.union (getTermPredToks t1) $ getTermPredToks t2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Membership t _ _ -> getTermPredToks t
0678d323bee844db79af13113ae252546629a594Christian Maeder    _ -> Set.empty
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaedergetTermPredToks :: TERM M_FORMULA -> Set.Set Token
0678d323bee844db79af13113ae252546629a594Christian MaedergetTermPredToks trm = case trm of
0678d323bee844db79af13113ae252546629a594Christian Maeder    Application _ ts _ -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    Sorted_term t _ _ -> getTermPredToks t
0678d323bee844db79af13113ae252546629a594Christian Maeder    Cast t _ _ -> getTermPredToks t
0678d323bee844db79af13113ae252546629a594Christian Maeder    Conditional t1 f t2 _ -> Set.union (getTermPredToks t1) $
0678d323bee844db79af13113ae252546629a594Christian Maeder        Set.union (getFormPredToks f) $ getTermPredToks t2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_term ts -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_parenthesized ts _ -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_bracketed ts _ -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_braced ts _ -> Set.unions $ map getTermPredToks ts
0678d323bee844db79af13113ae252546629a594Christian Maeder    _ -> Set.empty
3ef9708a35cddb7ba66458ad4a065de549ce7db6Till Mossakowski
0678d323bee844db79af13113ae252546629a594Christian MaederisPropForm :: Bool -> FORMULA M_FORMULA -> Bool
0678d323bee844db79af13113ae252546629a594Christian MaederisPropForm b frm = case frm of
0678d323bee844db79af13113ae252546629a594Christian Maeder    Quantification _ _ f _ -> b && isPropForm b f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Conjunction fs _ -> all (isPropForm b) fs
0678d323bee844db79af13113ae252546629a594Christian Maeder    Disjunction fs _ -> all (isPropForm b) fs
0678d323bee844db79af13113ae252546629a594Christian Maeder    Implication f1 f2 _ _ -> isPropForm b f1 && isPropForm b f2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Equivalence f1 f2 _  -> isPropForm b f1 && isPropForm b f2
0678d323bee844db79af13113ae252546629a594Christian Maeder    Negation f _ -> isPropForm b f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Mixfix_formula _ -> True
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder    ExtFORMULA (BoxOrDiamond _ _ f _) -> isPropForm b f
0678d323bee844db79af13113ae252546629a594Christian Maeder    Predication _ _ _ -> True
0678d323bee844db79af13113ae252546629a594Christian Maeder    False_atom _ -> True
0678d323bee844db79af13113ae252546629a594Christian Maeder    True_atom _ -> True
0678d323bee844db79af13113ae252546629a594Christian Maeder    _ -> False