hets/Modal/StatAna.hs

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule      :  ./Modal/StatAna.hs
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian MaederCopyright   :  (c) Christian Maeder, Uni Bremen 2004-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense     :  GPLv2 or higher, see LICENSE.txt
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer  :  luecke@informatik.uni-bremen.de
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability   :  provisional
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability :  portable
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederstatic analysis of modal logic parts
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maedermodule Modal.StatAna (basicModalAnalysis, minExpForm) where
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.AS_Modal
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Modal.Print_AS ()
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Modal.ModalSign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.Sign
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.MixfixParser
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.StaticAna
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.AS_Basic_CASL
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederimport CASL.ShowMixfix
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport CASL.Overload
ae179fb240298858539e0ff2b2e515d39ac17efcChristian Maederimport CASL.Quantification
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.AS_Annotation
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.GlobalAnnotations
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maederimport Common.Keywords
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Lib.State
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Id
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Common.Result
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport Common.ExtSign
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Set as Set
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian Maederimport Data.List as List
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederimport Data.Function
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maederinstance TermExtension M_FORMULA where
7aeb33d3af3230641a33c39b7e7ba546bb35b969Christian Maeder    freeVarsOfExt sign (BoxOrDiamond _ _ f _) = freeVars sign f
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederbasicModalAnalysis
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder  :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder      Sign M_FORMULA ModalSign, GlobalAnnos)
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder  -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder             ExtSign (Sign M_FORMULA ModalSign) Symbol,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder             [Named (FORMULA M_FORMULA)])
9f29e77d1b758a260223874ac6956e290134cb9dChristian MaederbasicModalAnalysis =
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder    basicAnalysis minExpForm ana_M_BASIC_ITEM ana_M_SIG_ITEM ana_Mix
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederana_Mix = emptyMix
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    { getSigIds = ids_M_SIG_ITEM
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , putParen = mapM_FORMULA
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder    , mixResolve = resolveM_FORMULA
57fce7f12e914e6165f83e4d0bbfdebf9c55ea9bChristian Maeder    }
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder-- rigid ops will also be part of the CASL signature
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_M_SIG_ITEM si = let e = Set.empty in case si of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    Rigid_op_items _ al _ ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder        (unite2 $ map (ids_OP_ITEM . item) al, e)
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    Rigid_pred_items _ al _ ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder        ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder
fe216849cef7b87c6800aad21178d1e686575d8fChristian MaedermapMODALITY :: MODALITY -> MODALITY
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian 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
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedermapM_FORMULA (BoxOrDiamond b m f ps) =
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder    BoxOrDiamond b (mapMODALITY m) (mapFormula mapM_FORMULA f) ps
fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederresolveMODALITY :: MixResolve MODALITY
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederresolveMODALITY ga ids m = case m of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian 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
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederresolveM_FORMULA ga ids cf = case cf of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian 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
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederminExpForm :: Min M_FORMULA ModalSign
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederminExpForm 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
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder                      t2 <- oneExpTerm minExpForm s t
6a50fa6b0d93a521d8e52c61a3ceb71d9f878cebChristian Maeder                      let srt = sortOfTerm t2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                          trm = Term_mod t2
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                          supers = supersortsOf srt s
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                      if Set.null $ Set.intersection
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                        (Set.insert srt supers)
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                         $ Map.keysSet $ termModies $ extendedInfo s
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                         then Result [mkDiag Error
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                              ("unknown term modality sort '"
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                               ++ showId srt "' for term") t ]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                              $ Just trm
83a2a69a740839f5646a7bd47a5ebdc2f45f97fcChristian Maeder                         else return trm
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                    in case t of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder                       Mixfix_token tm ->
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder                           if Map.member tm (modies $ extendedInfo s)
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder                              || tokStr tm == emptyS
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                              then return $ Simple_mod tm
41076bb5f87e3dbebb53d762ccb9795801b4a27aChristian Maeder                              else Result
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                                      [mkDiag Error "unknown modality" tm]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                                      $ Just $ Simple_mod tm
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder                       Application (Op_name (Id [tm] [] _)) [] _ ->
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder                           if Map.member tm (modies $ extendedInfo s)
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder                           then return $ Simple_mod tm
ee1ceac4345bc824210b2f7c6d6b182cb1902547Christian Maeder                           else r
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                       _ -> r
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    in case form of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder        BoxOrDiamond b m f ps ->
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder            do nm <- minMod m ps
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder               f2 <- minExpFORMULA minExpForm 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
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederana_M_SIG_ITEM mix mi =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    case mi of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    Rigid_op_items r al ps ->
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder        do ul <- mapM (ana_OP_ITEM minExpForm mix) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           case r of
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder               Flexible -> mapM_ (\ aoi -> case item aoi of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder                   Op_decl ops ty _ _ ->
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder                       mapM_ (updateExtInfo . addFlexOp (toOpType ty)) ops
51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder                   Op_defn i par _ _ -> maybe (return ())
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder                       (\ ty -> updateExtInfo $ addFlexOp (toOpType ty) i)
51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder                       $ headToType par) ul
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder               Rigid -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           return $ Rigid_op_items r ul ps
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    Rigid_pred_items r al ps ->
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder        do ul <- mapM (ana_PRED_ITEM minExpForm mix) al
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           case r of
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder               Flexible -> mapM_ (\ aoi -> case item aoi of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder                   Pred_decl ops ty _ ->
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder                       mapM_ (updateExtInfo . addFlexPred (toPredType ty)) ops
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder                   Pred_defn i (Pred_head args _) _ _ ->
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder                       updateExtInfo $ addFlexPred
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder                                (PredType $ sortsOfArgs args) i ) ul
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder               Rigid -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder           return $ Rigid_pred_items r ul ps
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian MaederaddFlexOp :: OpType -> Id -> ModalSign -> Result ModalSign
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian MaederaddFlexOp ty i m = return
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder       m { flexOps = addOpTo i ty $ flexOps m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian MaederaddFlexPred :: PredType -> Id -> ModalSign -> Result ModalSign
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian MaederaddFlexPred ty i m = return
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder       m { flexPreds = MapSet.insert i ty $ flexPreds m }
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederana_M_BASIC_ITEM
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder    :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederana_M_BASIC_ITEM mix bi = case bi of
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder        Simple_mod_decl al fs ps -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . preAddModId) . item) al
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder            newFs <- mapAnM (ana_FORMULA mix) fs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            resFs <- mapAnM (return . fst) newFs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            anaFs <- mapAnM (return . snd) newFs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            mapM_ ((updateExtInfo . addModId anaFs) . item) al
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            return $ Simple_mod_decl al resFs ps
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder        Term_mod_decl al fs ps -> do
0678d323bee844db79af13113ae252546629a594Christian Maeder            e <- get
0678d323bee844db79af13113ae252546629a594Christian Maeder            mapM_ ((updateExtInfo . preAddModSort e) . item) al
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maeder            newFs <- mapAnM (ana_FORMULA mix) fs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            resFs <- mapAnM (return . fst) newFs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            anaFs <- mapAnM (return . snd) newFs
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            mapM_ ((updateExtInfo . addModSort anaFs) . item) al
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            return $ Term_mod_decl al resFs ps
36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaederpreAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederpreAddModId i m =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    let ms = modies m in
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    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
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian MaederaddModId frms i m = return m
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian Maeder  { modies = Map.insertWith List.union i frms $ modies m }
0678d323bee844db79af13113ae252546629a594Christian Maeder
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederpreAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign
0678d323bee844db79af13113ae252546629a594Christian Maeder              -> Result ModalSign
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederpreAddModSort e i m =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder    let ms = termModies m
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder        ds = hasSort e i
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder    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
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian MaederaddModSort frms i m = return m
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian Maeder  { termModies = Map.insertWith List.union i frms $ termModies m }
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maederana_FORMULA :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder            -> FORMULA M_FORMULA -> State (Sign M_FORMULA ModalSign)
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder               (FORMULA M_FORMULA, FORMULA M_FORMULA)
c29fabd288a7c6c0b46e134f70b48138aae9214aChristian Maederana_FORMULA mix f = do
81700fac589336e88451a2a8474a893a28506438Christian Maeder           let ps = map simpleIdToId $ Set.toList $ getFormPredToks f
0678d323bee844db79af13113ae252546629a594Christian Maeder           pm <- gets predMap
a625226f55956c1dccb72888417d1f25db3cf173Christian Maeder           mapM_ (addPred (emptyAnno ()) $ PredType []) ps
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maeder           newGa <- gets globAnnos
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder           let Result es m = resolveFormula mapM_FORMULA
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder                             resolveM_FORMULA newGa (mixRules mix) f
0678d323bee844db79af13113ae252546629a594Christian Maeder           addDiags es
0678d323bee844db79af13113ae252546629a594Christian Maeder           e <- get
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder           phi <- case m of
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder               Nothing -> return (f, f)
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder               Just r -> do
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder                   n <- resultToState (minExpFORMULA minExpForm e) r
a4edd5298ae0ab7382ecfbffb04ab577fa6a3431Christian Maeder                   return (r, n)
0678d323bee844db79af13113ae252546629a594Christian Maeder           e2 <- get
0678d323bee844db79af13113ae252546629a594Christian Maeder           put e2 {predMap = pm}
0678d323bee844db79af13113ae252546629a594Christian Maeder           return phi
0678d323bee844db79af13113ae252546629a594Christian Maeder
0678d323bee844db79af13113ae252546629a594Christian MaedergetFormPredToks :: FORMULA M_FORMULA -> Set.Set Token
0678d323bee844db79af13113ae252546629a594Christian MaedergetFormPredToks frm = case frm of
0678d323bee844db79af13113ae252546629a594Christian Maeder    Quantification _ _ f _ -> getFormPredToks f
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder    Junction _ fs _ -> Set.unions $ map getFormPredToks fs
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder    Relation f1 _ f2 _ -> on Set.union getFormPredToks f1 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
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder    Equation t1 _ t2 _ -> on Set.union getTermPredToks t1 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) $
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian 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