81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederCopyright : (c) Christian Maeder, Uni Bremen 2004-2005
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederMaintainer : luecke@informatik.uni-bremen.de
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederStability : provisional
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederPortability : portable
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederstatic analysis of hybrid logic parts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroedermodule Hybrid.StatAna (basicHybridAnalysis, minExpForm) where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Common.Lib.MapSet as MapSet
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Data.Map as Map
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport qualified Data.Set as Set
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance TermExtension H_FORMULA where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder freeVarsOfExt sign (BoxOrDiamond _ _ f _) = freeVars sign f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder freeVarsOfExt sign (At _ f _ ) = freeVars sign f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder freeVarsOfExt sign (Univ _ f _) = freeVars sign f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder freeVarsOfExt sign (Exist _ f _) = freeVars sign f
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder freeVarsOfExt _ (Here _ _ ) = Set.empty
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederbasicHybridAnalysis
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder :: (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Sign H_FORMULA HybridSign, GlobalAnnos)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> Result (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtSign (Sign H_FORMULA HybridSign) Symbol,
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder [Named (FORMULA H_FORMULA)])
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederbasicHybridAnalysis =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder basicAnalysis minExpForm ana_H_BASIC_ITEM ana_H_SIG_ITEM ana_Mix
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_Mix :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_Mix = emptyMix
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder { getSigIds = ids_H_SIG_ITEM
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , putParen = mapH_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder , mixResolve = resolveH_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- rigid ops will also be part of the CASL signature
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederids_H_SIG_ITEM :: H_SIG_ITEM -> IdSets
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederids_H_SIG_ITEM si = let e = Set.empty in case si of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid_op_items _ al _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (unite2 $ map (ids_OP_ITEM . item) al, e)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid_pred_items _ al _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapMODALITY :: MODALITY -> MODALITY
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapMODALITY m = case m of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Term_mod t -> Term_mod $ mapTerm mapH_FORMULA t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapH_FORMULA :: H_FORMULA -> H_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapH_FORMULA (BoxOrDiamond b m f ps) =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder BoxOrDiamond b (mapMODALITY m) (mapFormula mapH_FORMULA f) ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapH_FORMULA (At n f ps) = At n (mapFormula mapH_FORMULA f) ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapH_FORMULA (Univ n f ps) = Univ n (mapFormula mapH_FORMULA f) ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedermapH_FORMULA (Exist n f ps) = Exist n (mapFormula mapH_FORMULA f) ps
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedermapH_FORMULA (Here n ps) = Here n ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederresolveMODALITY :: MixResolve MODALITY
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederresolveMODALITY ga ids m = case m of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Term_mod t -> fmap Term_mod $ resolveMixTrm mapH_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder resolveH_FORMULA ga ids t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederresolveH_FORMULA :: MixResolve H_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederresolveH_FORMULA ga ids cf = case cf of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder BoxOrDiamond b m f ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder nm <- resolveMODALITY ga ids m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder nf <- resolveMixFrm mapH_FORMULA resolveH_FORMULA ga ids f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (BoxOrDiamond b nm nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder At n f ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder nf <- resolveMixFrm mapH_FORMULA resolveH_FORMULA ga ids f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (At n nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Univ n f ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder nf <- resolveMixFrm mapH_FORMULA resolveH_FORMULA ga ids f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (Univ n nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Exist n f ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder nf <- resolveMixFrm mapH_FORMULA resolveH_FORMULA ga ids f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (Exist n nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Here n ps -> return (Here n ps)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederminExpForm :: Min H_FORMULA HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederminExpForm s form =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let minMod md ps = case md of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Simple_mod i -> minMod (Term_mod (Mixfix_token i)) ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Term_mod t -> let
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder t2 <- oneExpTerm minExpForm s t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let srt = sortOfTerm t2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder trm = Term_mod t2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder supers = supersortsOf srt s
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $ Map.keysSet $ termModies $ extendedInfo s
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder then Result [mkDiag Error
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ("unknown term modality sort '"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ++ showId srt "' for term") t ]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else return trm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_token tm ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder if Map.member tm (modies $ extendedInfo s)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder || tokStr tm == emptyS
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder then return $ Simple_mod tm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder [mkDiag Error "unknown modality" tm]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $ Just $ Simple_mod tm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Application (Op_name (Id [tm] [] _)) [] _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder if Map.member tm (modies $ extendedInfo s)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder then return $ Simple_mod tm
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder minNom (Simple_nom n) = if Map.member n (nomies $ extendedInfo s)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder then return (Simple_nom n)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else Result [mkDiag Error "unknown nominal" n]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $ Just (Simple_nom n)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder colNom (Simple_nom n)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder | Map.member n (nomies $ extendedInfo s) = Result
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder [mkDiag Error "collision on nominals" n] $ Just (Simple_nom n)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder | wPrefix n = Result
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder [mkDiag Error "\"world\" prefixes are reserved" n] Nothing
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder | otherwise = return (Simple_nom n)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder addUniv (Simple_nom n) = addNomId [] n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder addExist (Simple_nom n ) = addNomId [] n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder in case form of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder BoxOrDiamond b m f ps ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do nm <- minMod m ps
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nf <- minExpFORMULA minExpForm s f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (BoxOrDiamond b nm nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do nn <- minNom n
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nf <- minExpFORMULA minExpForm s f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (At nn nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do nn <- colNom n
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder {- add the binder in the sign (for this formula only)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder so it can be used a normal nominal -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder bs <- addUniv nn (extendedInfo s)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nf <- minExpFORMULA minExpForm (s {extendedInfo = bs}) f
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder return (Univ nn nf ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Exist n f ps ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do nn <- colNom n
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder {- add the binder in the sign (for this formula only)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder so it can be used a normal nominal -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder bs <- addExist nn (extendedInfo s)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nf <- minExpFORMULA minExpForm (s {extendedInfo = bs}) f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (Exist nn nf ps)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder do nn <- minNom n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return (Here nn ps)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_H_SIG_ITEM :: Ana H_SIG_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_H_SIG_ITEM mix mi =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid_op_items r al ps ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do ul <- mapM (ana_OP_ITEM minExpForm mix) al
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid -> mapM_ (\ aoi -> case item aoi of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Op_decl ops ty _ _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ (updateExtInfo . addRigidOp (toOpType ty)) ops
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Op_defn i par _ _ -> maybe (return ())
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (\ ty -> updateExtInfo $ addRigidOp (toOpType ty) i)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder $ headToType par) ul
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return $ Rigid_op_items r ul ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid_pred_items r al ps ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder do ul <- mapM (ana_PRED_ITEM minExpForm mix) al
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Rigid -> mapM_ (\ aoi -> case item aoi of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Pred_decl ops ty _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ (updateExtInfo . addRigidPred (toPredType ty)) ops
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Pred_defn i (Pred_head args _) _ _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder updateExtInfo $ addRigidPred
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (PredType $ sortsOfArgs args) i ) ul
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return $ Rigid_pred_items r ul ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddRigidOp :: OpType -> Id -> HybridSign -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddRigidOp ty i m = return
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder m { rigidOps = addOpTo i ty $ rigidOps m }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddRigidPred :: PredType -> Id -> HybridSign -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddRigidPred ty i m = return
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder m { rigidPreds = MapSet.insert i ty $ rigidPreds m }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_H_BASIC_ITEM
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder :: Ana H_BASIC_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederana_H_BASIC_ITEM mix bi =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder let anaHlp fs = do
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder newFs <- mapAnM (ana_FORMULA mix) fs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder resFs <- mapAnM (return . fst) newFs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder anaFs <- mapAnM (return . snd) newFs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder return (resFs, anaFs)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Simple_mod_decl al fs ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . preAddModId) . item) al
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (resFs, anaFs) <- anaHlp fs
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . addModId anaFs) . item) al
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return $ Simple_mod_decl al resFs ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Term_mod_decl al fs ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . preAddModSort e) . item) al
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (resFs, anaFs) <- anaHlp fs
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . addModSort anaFs) . item) al
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return $ Term_mod_decl al resFs ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Simple_nom_decl ids fs ps -> do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . preAddNomId) . item) ids
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (resFs, anaFs) <- anaHlp fs
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ ((updateExtInfo . addNomId anaFs) . item) ids
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return $ Simple_nom_decl ids resFs ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederpreAddNomId :: SIMPLE_ID -> HybridSign -> Result HybridSign
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederpreAddNomId i hs =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let ns = nomies hs in
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Result [mkDiag Hint "repeated nominal" i] $ Just hs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder else if wPrefix i
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder then Result [mkDiag Error "\"world\" prefixes are reserved" i]
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder else return hs { nomies = Map.insert i [] ns }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederpreAddModId :: SIMPLE_ID -> HybridSign -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederpreAddModId i m =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let ms = modies m in
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Result [mkDiag Hint "repeated modality" i] $ Just m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else return m { modies = Map.insert i [] ms }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddNomId :: [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederaddNomId frms i s =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder return s { nomies = Map.insertWith List.union i frms $ nomies s}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddModId :: [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddModId frms i m = return m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder { modies = Map.insertWith List.union i frms $ modies m }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederpreAddModSort :: Sign H_FORMULA HybridSign -> SORT -> HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederpreAddModSort e i m =
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let ms = termModies m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ds = hasSort e i
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder in if Map.member i ms || not (null ds) then
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Result (mkDiag Hint "repeated term modality" i : ds) $ Just m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder else return m { termModies = Map.insert i [] ms }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddModSort :: [AnHybFORM] -> SORT -> HybridSign -> Result HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddModSort frms i m = return m
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder { termModies = Map.insertWith List.union i frms $ termModies m }
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_FORMULA :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -> FORMULA H_FORMULA -> State (Sign H_FORMULA HybridSign)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (FORMULA H_FORMULA, FORMULA H_FORMULA)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederana_FORMULA mix f = do
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let ps = map (mkId . (: [])) $ Set.toList $ getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder pm <- gets predMap
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mapM_ (addPred (emptyAnno ()) $ PredType []) ps
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder newGa <- gets globAnnos
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder let Result es m = resolveFormula mapH_FORMULA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder resolveH_FORMULA newGa (mixRules mix) f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder phi <- case m of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Nothing -> return (f, f)
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder n <- resultToState (minExpFORMULA minExpForm e) r
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder put e2 {predMap = pm}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergetFormPredToks :: FORMULA H_FORMULA -> Set.Set Token
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergetFormPredToks frm = case frm of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Quantification _ _ f _ -> getFormPredToks f
1288401b122a6bcb27fa6730a9a75370438d9892Jonathan von Schroeder Junction _ fs _ -> Set.unions $ map getFormPredToks fs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Relation f1 _ f2 _ ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Set.union (getFormPredToks f1) $ getFormPredToks f2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Negation f _ -> getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_formula (Mixfix_token t) -> Set.singleton t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_formula t -> getTermPredToks t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtFORMULA (BoxOrDiamond _ _ f _) -> getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtFORMULA (At _ f _ ) -> getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtFORMULA (Univ _ f _ ) -> getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ExtFORMULA (Exist _ f _ ) -> getFormPredToks f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Predication _ ts _ -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Definedness t _ -> getTermPredToks t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Membership t _ _ -> getTermPredToks t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergetTermPredToks :: TERM H_FORMULA -> Set.Set Token
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedergetTermPredToks trm = case trm of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Application _ ts _ -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Sorted_term t _ _ -> getTermPredToks t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Cast t _ _ -> getTermPredToks t
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Conditional t1 f t2 _ -> Set.union (getTermPredToks t1) $
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Set.union (getFormPredToks f) $ getTermPredToks t2
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_term ts -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_parenthesized ts _ -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_bracketed ts _ -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Mixfix_braced ts _ -> Set.unions $ map getTermPredToks ts
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederwPrefix :: Token -> Bool
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederwPrefix = isPrefixOf "world" . tokStr