0d03aadb6c364ae976af4c904aa3625d2512d101sf{- |

0d03aadb6c364ae976af4c904aa3625d2512d101sfModule : $Header$

0d03aadb6c364ae976af4c904aa3625d2512d101sfCopyright : DFKI GmbH 2009

0d03aadb6c364ae976af4c904aa3625d2512d101sfLicense : GPLv2 or higher, see LICENSE.txt

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfMaintainer : codruta.liliana@gmail.com

0d03aadb6c364ae976af4c904aa3625d2512d101sfStability : experimental

0d03aadb6c364ae976af4c904aa3625d2512d101sfPortability : portable

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfstatic analysis of modal logic parts

0d03aadb6c364ae976af4c904aa3625d2512d101sf-}

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfmodule ExtModal.StatAna where

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport ExtModal.AS_ExtModal

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport ExtModal.Print_AS ()

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport ExtModal.ExtModalSign

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.Fold

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.Sign

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.MixfixParser

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.StaticAna

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.AS_Basic_CASL

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.ShowMixfix

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.Overload

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport CASL.Quantification

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.AS_Annotation

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.DocUtils

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.GlobalAnnotations

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.Keywords

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.Lib.State

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.Id

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.Result

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Common.ExtSign

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport qualified Common.Lib.MapSet as MapSet

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport qualified Data.Map as Map

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport qualified Data.Set as Set

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfimport Control.Monad

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfinstance TermExtension EM_FORMULA where

0d03aadb6c364ae976af4c904aa3625d2512d101sf freeVarsOfExt sign frm = case frm of

0d03aadb6c364ae976af4c904aa3625d2512d101sf BoxOrDiamond _ m _ _ f _ ->

0d03aadb6c364ae976af4c904aa3625d2512d101sf Set.union (freeModVars sign m) $ freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf Hybrid _ _ f _ -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf UntilSince _ f1 f2 _ -> Set.union (freeVars sign f1) $ freeVars sign f2

0d03aadb6c364ae976af4c904aa3625d2512d101sf PathQuantification _ f _ -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf StateQuantification _ _ f _ -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf NextY _ f _ -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf FixedPoint _ _ f _ -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf ModForm (ModDefn _ _ _ afs _) ->

0d03aadb6c364ae976af4c904aa3625d2512d101sf Set.unions $ map (freeVars sign . item)

0d03aadb6c364ae976af4c904aa3625d2512d101sf $ concatMap (frameForms . item) afs

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sffreeModVars :: Sign EM_FORMULA e -> MODALITY -> Set.Set (VAR, SORT)

0d03aadb6c364ae976af4c904aa3625d2512d101sffreeModVars sign md = case md of

0d03aadb6c364ae976af4c904aa3625d2512d101sf SimpleMod _ -> Set.empty

0d03aadb6c364ae976af4c904aa3625d2512d101sf TermMod t -> freeTermVars sign t

0d03aadb6c364ae976af4c904aa3625d2512d101sf ModOp _ m1 m2 -> Set.union (freeModVars sign m1) $ freeModVars sign m2

0d03aadb6c364ae976af4c904aa3625d2512d101sf TransClos m -> freeModVars sign m

0d03aadb6c364ae976af4c904aa3625d2512d101sf Guard f -> freeVars sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfbasicEModalAnalysis

0d03aadb6c364ae976af4c904aa3625d2512d101sf :: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA

0d03aadb6c364ae976af4c904aa3625d2512d101sf , Sign EM_FORMULA EModalSign, GlobalAnnos)

0d03aadb6c364ae976af4c904aa3625d2512d101sf -> Result (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA

0d03aadb6c364ae976af4c904aa3625d2512d101sf , ExtSign (Sign EM_FORMULA EModalSign) Symbol

0d03aadb6c364ae976af4c904aa3625d2512d101sf , [Named (FORMULA EM_FORMULA)])

0d03aadb6c364ae976af4c904aa3625d2512d101sfbasicEModalAnalysis =

0d03aadb6c364ae976af4c904aa3625d2512d101sf basicAnalysis frmTypeAna basItemStatAna sigItemStatAna mixfixAna

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sffrmTypeAna :: Min EM_FORMULA EModalSign

0d03aadb6c364ae976af4c904aa3625d2512d101sffrmTypeAna sign form = let

0d03aadb6c364ae976af4c904aa3625d2512d101sf checkMod term_mod = case term_mod of

0d03aadb6c364ae976af4c904aa3625d2512d101sf SimpleMod s_id ->

0d03aadb6c364ae976af4c904aa3625d2512d101sf if tokStr s_id == emptyS

0d03aadb6c364ae976af4c904aa3625d2512d101sf || Set.member (simpleIdToId s_id) (modalities $ extendedInfo sign)

0d03aadb6c364ae976af4c904aa3625d2512d101sf then return $ SimpleMod s_id

0d03aadb6c364ae976af4c904aa3625d2512d101sf else Result [mkDiag Error "unknown modality" s_id]

0d03aadb6c364ae976af4c904aa3625d2512d101sf $ Just $ SimpleMod s_id

0d03aadb6c364ae976af4c904aa3625d2512d101sf ModOp o md1 md2 -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_md1 <- checkMod md1

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_md2 <- checkMod md2

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ ModOp o new_md1 new_md2

0d03aadb6c364ae976af4c904aa3625d2512d101sf TransClos md -> fmap TransClos $ checkMod md

0d03aadb6c364ae976af4c904aa3625d2512d101sf Guard frm -> fmap Guard $ minExpFORMULA frmTypeAna sign frm

0d03aadb6c364ae976af4c904aa3625d2512d101sf TermMod t -> let

0d03aadb6c364ae976af4c904aa3625d2512d101sf ms = modalities $ extendedInfo sign

0d03aadb6c364ae976af4c904aa3625d2512d101sf r = do

0d03aadb6c364ae976af4c904aa3625d2512d101sf t2 <- oneExpTerm frmTypeAna sign t

0d03aadb6c364ae976af4c904aa3625d2512d101sf let srt = sortOfTerm t2

0d03aadb6c364ae976af4c904aa3625d2512d101sf trm = TermMod t2

0d03aadb6c364ae976af4c904aa3625d2512d101sf supers = supersortsOf srt sign

0d03aadb6c364ae976af4c904aa3625d2512d101sf if Set.null $ Set.intersection (Set.insert srt supers) ms

0d03aadb6c364ae976af4c904aa3625d2512d101sf then Result [mkDiag Error

0d03aadb6c364ae976af4c904aa3625d2512d101sf ("unknown term modality sort '"

0d03aadb6c364ae976af4c904aa3625d2512d101sf ++ showId srt "' for term") t ]

0d03aadb6c364ae976af4c904aa3625d2512d101sf $ Just trm

0d03aadb6c364ae976af4c904aa3625d2512d101sf else return trm

0d03aadb6c364ae976af4c904aa3625d2512d101sf in case t of

0d03aadb6c364ae976af4c904aa3625d2512d101sf Mixfix_token tm ->

0d03aadb6c364ae976af4c904aa3625d2512d101sf if Set.member (simpleIdToId tm) ms

0d03aadb6c364ae976af4c904aa3625d2512d101sf || tokStr tm == emptyS

0d03aadb6c364ae976af4c904aa3625d2512d101sf then return $ SimpleMod tm

0d03aadb6c364ae976af4c904aa3625d2512d101sf else Result

0d03aadb6c364ae976af4c904aa3625d2512d101sf [mkDiag Error "unknown modality" tm]

0d03aadb6c364ae976af4c904aa3625d2512d101sf $ Just $ SimpleMod tm

0d03aadb6c364ae976af4c904aa3625d2512d101sf Application (Op_name (Id [tm] [] _)) [] _ ->

0d03aadb6c364ae976af4c904aa3625d2512d101sf if Set.member (simpleIdToId tm) ms

0d03aadb6c364ae976af4c904aa3625d2512d101sf then return $ SimpleMod tm

0d03aadb6c364ae976af4c904aa3625d2512d101sf else r

0d03aadb6c364ae976af4c904aa3625d2512d101sf _ -> r

0d03aadb6c364ae976af4c904aa3625d2512d101sf checkFrame (FrameForm vs fs r) = do

0d03aadb6c364ae976af4c904aa3625d2512d101sf nfs <- mapAnM (minExpFORMULA frmTypeAna sign . mkForall vs) fs

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ FrameForm [] nfs r

0d03aadb6c364ae976af4c904aa3625d2512d101sf in case form of

0d03aadb6c364ae976af4c904aa3625d2512d101sf BoxOrDiamond choice md leq_geq number f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_md <- checkMod md

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf if number >= 0

0d03aadb6c364ae976af4c904aa3625d2512d101sf then return $ BoxOrDiamond choice new_md leq_geq number new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf else Result [mkDiag Error "negative number grading" number]

0d03aadb6c364ae976af4c904aa3625d2512d101sf $ Just $ BoxOrDiamond choice new_md leq_geq number new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf Hybrid choice nm f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf if Set.member nm (nominals $ extendedInfo sign)

0d03aadb6c364ae976af4c904aa3625d2512d101sf then return $ Hybrid choice nm new_f pos

3d27420bf1f5d019774995b66e3ba0955de6df6csf else Result [mkDiag Error "unknown nominal" nm]

3d27420bf1f5d019774995b66e3ba0955de6df6csf $ Just $ Hybrid choice nm new_f pos

3d27420bf1f5d019774995b66e3ba0955de6df6csf UntilSince choice f1 f2 pos -> do

3d27420bf1f5d019774995b66e3ba0955de6df6csf new_f1 <- minExpFORMULA frmTypeAna sign f1

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f2 <- minExpFORMULA frmTypeAna sign f2

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ UntilSince choice new_f1 new_f2 pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf PathQuantification choice f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ PathQuantification choice new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf StateQuantification t_dir choice f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ StateQuantification t_dir choice new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf NextY choice f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ NextY choice new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf FixedPoint choice fpvar f pos -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_f <- minExpFORMULA frmTypeAna sign f

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ FixedPoint choice fpvar new_f pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf ModForm (ModDefn is_time isTerm anno_list forms pos) -> do

0d03aadb6c364ae976af4c904aa3625d2512d101sf new_forms <- mapAnM checkFrame forms

0d03aadb6c364ae976af4c904aa3625d2512d101sf return $ ModForm $ ModDefn is_time isTerm anno_list new_forms pos

0d03aadb6c364ae976af4c904aa3625d2512d101sf

0d03aadb6c364ae976af4c904aa3625d2512d101sfanaFrameForm :: Mix b s EM_FORMULA EModalSign -> FrameForm

0d03aadb6c364ae976af4c904aa3625d2512d101sf -> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)

0d03aadb6c364ae976af4c904aa3625d2512d101sfanaFrameForm mix ff@(FrameForm vs fs r) = if null fs then do

0d03aadb6c364ae976af4c904aa3625d2512d101sf mapM_ addVars vs

0d03aadb6c364ae976af4c904aa3625d2512d101sf return (ff, ff)

0d03aadb6c364ae976af4c904aa3625d2512d101sf else do

0d03aadb6c364ae976af4c904aa3625d2512d101sf (resFs, fufs) <- anaLocalVarForms (anaFORMULA mix) vs fs r

0d03aadb6c364ae976af4c904aa3625d2512d101sf return (FrameForm vs resFs r, FrameForm [] fufs r)

clearVarMap :: State (Sign f e) ()

clearVarMap = do

e <- get

put e { varMap = Map.empty }

modItemStatAna

:: Ana ModDefn EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

modItemStatAna mix (ModDefn is_time isTerm anno_list forms pos) = do

mapM_ ( (updateExtInfo . addMod) . item ) anno_list

clearVarMap -- forget vars beyond this point

new_forms <- mapAnM (anaFrameForm mix) forms

clearVarMap -- forget vars after this point

let res_forms = map (fmap fst) new_forms

ana_forms = filter (not . null . frameForms . item)

$ map (fmap snd) new_forms

unless (null ana_forms)

$ addSentences $ map (\ af ->

makeNamed (getRLabel af) $ ExtFORMULA $ ModForm

$ ModDefn is_time isTerm anno_list [emptyAnno $ item af] pos)

ana_forms

when is_time $ mapM_ ( (updateExtInfo . addTimeMod ) . item ) anno_list

when isTerm $ do

sig <- get

mapM_ ( (updateExtInfo . addTermMod sig) . item ) anno_list

return $ ModDefn is_time isTerm anno_list res_forms pos

basItemStatAna

:: Ana EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

basItemStatAna mix basic_item = case basic_item of

ModItem md -> fmap ModItem $ modItemStatAna mix md

Nominal_decl anno_list pos -> do

mapM_ (updateExtInfo . addNom . item) anno_list

mapM_ (addPred (emptyAnno ()) (PredType []) . mkId . (: []) . item)

anno_list

return $ Nominal_decl anno_list pos

addTermMod :: Sign f e -> Id -> EModalSign -> Result EModalSign

addTermMod fullSign tmi sgn = let

tm = termMods sgn

srts = sortSet fullSign

in if Set.member tmi srts then

if Set.member tmi tm

then Result [mkDiag Hint "repeated term modality" tmi] $ Just sgn

else let sps = Set.difference tm $ supersortsOf tmi fullSign in

if Set.null sps

then return sgn { termMods = Set.insert tmi tm }

else Result [mkDiag Warning

("term modality known for supersorts " ++ showDoc sps "")

tmi] $ Just sgn

else Result [mkDiag Error "unknown sort in term modality" tmi] $ Just sgn

addTimeMod :: Id -> EModalSign -> Result EModalSign

addTimeMod tmi sgn = let tm = time_modalities sgn in

if Set.member tmi tm

then Result [mkDiag Hint "repeated time modality" tmi] $ Just sgn

else if Set.size tm >= 1

then Result [mkDiag Hint "more than one time modality" tmi] $ Just sgn

else return sgn { time_modalities = Set.insert tmi tm }

addMod :: Id -> EModalSign -> Result EModalSign

addMod mi sgn =

let m = modalities sgn in

if Set.member mi m then

Result [mkDiag Hint "repeated modality" mi] $ Just sgn

else return sgn { modalities = Set.insert mi m }

addNom :: SIMPLE_ID -> EModalSign -> Result EModalSign

addNom ni sgn =

let n = nominals sgn in

if Set.member ni n then

Result [mkDiag Hint "repeated nominal" ni] $ Just sgn

else return sgn { nominals = Set.insert ni n }

sigItemStatAna

:: Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

sigItemStatAna mix sig_item = case sig_item of

Rigid_op_items rig ann_list pos -> do

new_list <- mapM (ana_OP_ITEM frmTypeAna mix) ann_list

unless rig $ mapM_

(\ nlitem -> case item nlitem of

Op_decl ops typ _ _ ->

mapM_ (updateExtInfo . addFlexOp (toOpType typ)) ops

Op_defn op hd _ _ -> maybe (return ())

(\ ty -> updateExtInfo $ addFlexOp (toOpType ty) op)

$ headToType hd

) new_list

return $ Rigid_op_items rig new_list pos

Rigid_pred_items rig ann_list pos -> do

new_list <- mapM (ana_PRED_ITEM frmTypeAna mix) ann_list

unless rig $ mapM_ ( \ nlitem -> case item nlitem of

Pred_decl preds typ _ ->

mapM_ (updateExtInfo . addFlexPred (toPredType typ) ) preds

Pred_defn prd (Pred_head args _ ) _ _ ->

updateExtInfo $ addFlexPred (PredType $ sortsOfArgs args) prd

) new_list

return $ Rigid_pred_items rig new_list pos

addFlexOp :: OpType -> Id -> EModalSign -> Result EModalSign

addFlexOp typ i sgn = return

sgn { flexOps = addOpTo i typ $ flexOps sgn }

addFlexPred :: PredType -> Id -> EModalSign -> Result EModalSign

addFlexPred typ i sgn = return

sgn { flexPreds = MapSet.insert i typ $ flexPreds sgn }

mixfixAna :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign

mixfixAna = emptyMix

{ getSigIds = extraSigItems

, putParen = parenExtForm

, mixResolve = resolveExtForm

}

extraSigItems :: EM_SIG_ITEM -> IdSets

extraSigItems s = let e = Set.empty in case s of

Rigid_op_items _ annoted_list _ ->

(unite2 $ map (ids_OP_ITEM . item) annoted_list, e)

Rigid_pred_items _ annoted_list _ ->

((e, e), Set.unions $ map (ids_PRED_ITEM . item) annoted_list)

parenMod :: MODALITY -> MODALITY

parenMod m = case m of

ModOp o md1 md2 -> ModOp o (parenMod md1) $ parenMod md2

TransClos md -> TransClos $ parenMod md

Guard frm -> Guard $ mapFormula parenExtForm frm

TermMod t -> TermMod $ mapTerm parenExtForm t

_ -> m

parenExtForm :: EM_FORMULA -> EM_FORMULA

parenExtForm f = case f of

BoxOrDiamond choice md leq_geq nr frm pos ->

BoxOrDiamond choice (parenMod md) leq_geq nr

(mapFormula parenExtForm frm) pos

Hybrid choice nom frm pos ->

Hybrid choice nom (mapFormula parenExtForm frm) pos

UntilSince choice f1 f2 pos ->

UntilSince choice (mapFormula parenExtForm f1)

(mapFormula parenExtForm f2) pos

PathQuantification choice frm pos ->

PathQuantification choice (mapFormula parenExtForm frm) pos

StateQuantification t_dir choice frm pos ->

StateQuantification t_dir choice (mapFormula parenExtForm frm) pos

NextY choice frm pos ->

NextY choice (mapFormula parenExtForm frm) pos

FixedPoint choice fpvar frm pos ->

FixedPoint choice fpvar (mapFormula parenExtForm frm) pos

ModForm (ModDefn ti te is fs pos) -> ModForm $ ModDefn

ti te is (map (fmap parenFrameForm) fs) pos

parenFrameForm :: FrameForm -> FrameForm

parenFrameForm (FrameForm vs fs r) =

FrameForm vs (map (fmap $ mapFormula parenExtForm) fs) r

resolveMod :: MixResolve MODALITY

resolveMod ga ids m = case m of

ModOp o md1 md2 -> do

new_md1 <- resolveMod ga ids md1

new_md2 <- resolveMod ga ids md2

return $ ModOp o new_md1 new_md2

TransClos md -> fmap TransClos $ resolveMod ga ids md

Guard frm -> fmap Guard

$ resolveMixFrm parenExtForm resolveExtForm ga ids frm

TermMod t -> fmap TermMod

$ resolveMixTrm parenExtForm resolveExtForm ga ids t

_ -> return m

resolveExtForm :: MixResolve EM_FORMULA

resolveExtForm ga ids f =

let recResolve = resolveMixFrm parenExtForm resolveExtForm ga ids

in case f of

BoxOrDiamond choice ms leq_geq nr frm pos -> do

nms <- resolveMod ga ids ms

new_frm <- recResolve frm

return $ BoxOrDiamond choice nms leq_geq nr new_frm pos

Hybrid choice nom frm pos -> do

new_frm <- recResolve frm

return $ Hybrid choice nom new_frm pos

UntilSince choice f1 f2 pos -> do

new_f1 <- recResolve f1

new_f2 <- recResolve f2

return $ UntilSince choice new_f1 new_f2 pos

PathQuantification choice frm pos -> do

new_frm <- recResolve frm

return $ PathQuantification choice new_frm pos

StateQuantification t_dir choice frm pos -> do

new_frm <- recResolve frm

return $ StateQuantification t_dir choice new_frm pos

NextY choice frm pos -> do

new_frm <- recResolve frm

return $ NextY choice new_frm pos

FixedPoint choice fpvar frm pos -> do

new_frm <- recResolve frm

return $ FixedPoint choice fpvar new_frm pos

ModForm (ModDefn ti te is fs pos) -> do

nfs <- mapAnM (resolveFrameForm ga ids) fs

return $ ModForm $ ModDefn ti te is nfs pos

resolveFrameForm :: MixResolve FrameForm

resolveFrameForm ga ids (FrameForm vs fs r) = do

let ts = varDeclTokens vs

nfs <- mapAnM (resolveMixFrm parenExtForm

(extendMixResolve ts resolveExtForm) ga

$ extendRules ts ids) fs

return $ FrameForm vs nfs r

anaFORMULA :: Mix b s EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign

-> FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)

anaFORMULA mix sig f = do

let mix2 = extendMix (Map.keysSet $ varMap sig) mix

-- the unknown predicates are not needed for mixfix resolution

r <- resolveFormula parenExtForm

resolveExtForm (globAnnos sig) (mixRules mix2) f

let pm2 = Set.fold

(\ t -> MapSet.insert (simpleIdToId t) (PredType []))

(predMap sig)

$ getFormPredToks f

sig2 = sig { predMap = pm2 }

n <- minExpFORMULA frmTypeAna sig2 r

return (r, n)

getEFormPredToks :: EM_FORMULA -> Set.Set Token

getEFormPredToks ef = case ef of

BoxOrDiamond _ _ _ _ f _ -> getFormPredToks f

Hybrid _ _ f _ -> getFormPredToks f

UntilSince _ f1 f2 _ ->

Set.union (getFormPredToks f1) (getFormPredToks f2)

NextY _ f _ -> getFormPredToks f

PathQuantification _ f _ -> getFormPredToks f

StateQuantification _ _ f _ -> getFormPredToks f

FixedPoint _ _ f _ -> getFormPredToks f

ModForm _ -> Set.empty

getFormPredToks :: FORMULA EM_FORMULA -> Set.Set Token

getFormPredToks = foldFormula

(constRecord getEFormPredToks Set.unions Set.empty)

{ foldMixfix_formula = \ f ts -> case f of

Mixfix_formula (Mixfix_token t) -> Set.singleton t

_ -> ts }