hets/Modal/StatAna.hs

	StatAna.hs revision 18c1d987ce5818ecf0bfc8af3f43aed2ce86e1ea
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- |
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule      :  $Header$
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederCopyright   :  (c) Christian Maeder, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer  :  luettich@tzi.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability   :  provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability :  portable
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederstatic analysis of modal logic parts
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermodule Modal.StatAna where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.AS_Modal
25a0b76bc87e80c0f697951d9817862755a71d33Christian 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,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder                       Sign M_FORMULA ModalSign, GlobalAnnos)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder                   -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder                              Sign M_FORMULA ModalSign,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder                              Sign M_FORMULA ModalSign,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder                              [Named (FORMULA M_FORMULA)])
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederbasicModalAnalysis = basicAnalysis minExpForm ana_M_BASIC_ITEM
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder                     ana_M_SIG_ITEM ana_Mix diffModalSign
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maederana_Mix = emptyMix
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    { getSigIds = ids_M_SIG_ITEM
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , putParen = mapM_FORMULA
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , mixResolve = resolveM_FORMULA
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , checkMix = noExtMixfixM
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , putInj = injM_FORMULA }
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder-- rigid ops will also be part of the CASL signature
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_M_SIG_ITEM si = case si of
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    Rigid_op_items _ al _ ->
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder        (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    Rigid_pred_items _ al _ ->
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder        (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian 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
e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder                      t2 <- oneExpTerm minExpForm ga s t
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
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_M_SIG_ITEM :: Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_M_SIG_ITEM mix ga mi =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    case mi of
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    Rigid_op_items r al ps ->
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder        do ul <- mapM (ana_OP_ITEM minExpForm mix 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 ->
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder        do ul <- mapM (ana_PRED_ITEM minExpForm mix 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
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder       m { rigidPreds = let rps = rigidPreds m in Map.insert i
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder             (Set.insert ty $ Map.findWithDefault Set.empty i rps) rps }
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_M_BASIC_ITEM
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_M_BASIC_ITEM mix ga bi = do
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    case bi of
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder        Simple_mod_decl al fs ps -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . preAddModId) . item) al
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder            newFs <- mapAnM (ana_FORMULA False mix 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
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder            newFs <- mapAnM (ana_FORMULA True mix 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
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_FORMULA
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    :: Bool
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    -> Ana (FORMULA M_FORMULA) M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_FORMULA b mix 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
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder           newGa <- gets globAnnos
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder           let Result es m = resolveFormula mapM_FORMULA
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder                             resolveM_FORMULA newGa (mixRules mix) 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
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder    Mixfix_formula (Mixfix_token t) -> Set.singleton 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