module ExtModal.StatAna where
import ExtModal.AS_ExtModal
import ExtModal.Print_AS ()
import ExtModal.ExtModalSign
import CASL.Fold
import CASL.Sign
import CASL.MixfixParser
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.Overload
import CASL.Quantification
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.GlobalAnnotations
import Common.Keywords
import Common.Lib.State
import Common.Id
import Common.Result
import Common.ExtSign
import qualified Common.Lib.MapSet as MapSet
import Data.Function
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad
import qualified Control.Monad.Fail as Fail
instance TermExtension EM_FORMULA where
freeVarsOfExt :: Sign EM_FORMULA e -> EM_FORMULA -> VarSet
freeVarsOfExt sign :: Sign EM_FORMULA e
sign frm :: EM_FORMULA
frm = case EM_FORMULA
frm of
PrefixForm p :: FormPrefix
p f :: FORMULA EM_FORMULA
f _ ->
VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign EM_FORMULA e -> FormPrefix -> VarSet
forall e. Sign EM_FORMULA e -> FormPrefix -> VarSet
freePrefixVars Sign EM_FORMULA e
sign FormPrefix
p) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA e -> FORMULA EM_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign EM_FORMULA e
sign FORMULA EM_FORMULA
f
UntilSince _ f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 _ -> (VarSet -> VarSet -> VarSet)
-> (FORMULA EM_FORMULA -> VarSet)
-> FORMULA EM_FORMULA
-> FORMULA EM_FORMULA
-> VarSet
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign EM_FORMULA e -> FORMULA EM_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign EM_FORMULA e
sign) FORMULA EM_FORMULA
f1 FORMULA EM_FORMULA
f2
ModForm (ModDefn _ _ _ afs :: [Annoted FrameForm]
afs _) ->
[VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ (Annoted (FORMULA EM_FORMULA) -> VarSet)
-> [Annoted (FORMULA EM_FORMULA)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Sign EM_FORMULA e -> FORMULA EM_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign EM_FORMULA e
sign (FORMULA EM_FORMULA -> VarSet)
-> (Annoted (FORMULA EM_FORMULA) -> FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA)
-> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (FORMULA EM_FORMULA) -> FORMULA EM_FORMULA
forall a. Annoted a -> a
item)
([Annoted (FORMULA EM_FORMULA)] -> [VarSet])
-> [Annoted (FORMULA EM_FORMULA)] -> [VarSet]
forall a b. (a -> b) -> a -> b
$ (Annoted FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> [Annoted FrameForm] -> [Annoted (FORMULA EM_FORMULA)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FrameForm -> [Annoted (FORMULA EM_FORMULA)]
frameForms (FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> (Annoted FrameForm -> FrameForm)
-> Annoted FrameForm
-> [Annoted (FORMULA EM_FORMULA)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item) [Annoted FrameForm]
afs
freePrefixVars :: Sign EM_FORMULA e -> FormPrefix -> Set.Set (VAR, SORT)
freePrefixVars :: Sign EM_FORMULA e -> FormPrefix -> VarSet
freePrefixVars sign :: Sign EM_FORMULA e
sign fp :: FormPrefix
fp = case FormPrefix
fp of
BoxOrDiamond _ m :: MODALITY
m _ _ -> Sign EM_FORMULA e -> MODALITY -> VarSet
forall e. Sign EM_FORMULA e -> MODALITY -> VarSet
freeModVars Sign EM_FORMULA e
sign MODALITY
m
_ -> VarSet
forall a. Set a
Set.empty
freeModVars :: Sign EM_FORMULA e -> MODALITY -> Set.Set (VAR, SORT)
freeModVars :: Sign EM_FORMULA e -> MODALITY -> VarSet
freeModVars sign :: Sign EM_FORMULA e
sign md :: MODALITY
md = case MODALITY
md of
SimpleMod _ -> VarSet
forall a. Set a
Set.empty
TermMod t :: TERM EM_FORMULA
t -> Sign EM_FORMULA e -> TERM EM_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign EM_FORMULA e
sign TERM EM_FORMULA
t
ModOp _ m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> (VarSet -> VarSet -> VarSet)
-> (MODALITY -> VarSet) -> MODALITY -> MODALITY -> VarSet
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign EM_FORMULA e -> MODALITY -> VarSet
forall e. Sign EM_FORMULA e -> MODALITY -> VarSet
freeModVars Sign EM_FORMULA e
sign) MODALITY
m1 MODALITY
m2
TransClos m :: MODALITY
m -> Sign EM_FORMULA e -> MODALITY -> VarSet
forall e. Sign EM_FORMULA e -> MODALITY -> VarSet
freeModVars Sign EM_FORMULA e
sign MODALITY
m
Guard f :: FORMULA EM_FORMULA
f -> Sign EM_FORMULA e -> FORMULA EM_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign EM_FORMULA e
sign FORMULA EM_FORMULA
f
basicEModalAnalysis
:: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
, Sign EM_FORMULA EModalSign, GlobalAnnos)
-> Result (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA
, ExtSign (Sign EM_FORMULA EModalSign) Symbol
, [Named (FORMULA EM_FORMULA)])
basicEModalAnalysis :: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
Sign EM_FORMULA EModalSign, GlobalAnnos)
-> Result
(BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
basicEModalAnalysis s :: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
Sign EM_FORMULA EModalSign, GlobalAnnos)
s = do
a :: (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
a@(_, ExtSign sig :: Sign EM_FORMULA EModalSign
sig _, sens :: [Named (FORMULA EM_FORMULA)]
sens) <-
Min EM_FORMULA EModalSign
-> Ana
EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
Sign EM_FORMULA EModalSign, GlobalAnnos)
-> Result
(BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
(BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis Min EM_FORMULA EModalSign
frmTypeAna Ana EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
basItemStatAna Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
sigItemStatAna Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mixfixAna (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
Sign EM_FORMULA EModalSign, GlobalAnnos)
s
Sign EM_FORMULA EModalSign
-> [Named (FORMULA EM_FORMULA)] -> Result ()
checkConstr Sign EM_FORMULA EModalSign
sig [Named (FORMULA EM_FORMULA)]
sens
(BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
-> Result
(BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA,
ExtSign (Sign EM_FORMULA EModalSign) Symbol,
[Named (FORMULA EM_FORMULA)])
a
checkConstr :: Sign EM_FORMULA EModalSign -> [Named (FORMULA EM_FORMULA)]
-> Result ()
checkConstr :: Sign EM_FORMULA EModalSign
-> [Named (FORMULA EM_FORMULA)] -> Result ()
checkConstr sig :: Sign EM_FORMULA EModalSign
sig sens :: [Named (FORMULA EM_FORMULA)]
sens =
let cs :: OpMap
cs = OpMap -> OpMap -> OpMap
interOpMapSet
(((SORT, OpType) -> OpMap -> OpMap)
-> OpMap -> Set (SORT, OpType) -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((SORT -> OpType -> OpMap -> OpMap)
-> (SORT, OpType) -> OpMap -> OpMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> OpType -> OpMap -> OpMap
addOpTo) OpMap
forall a b. MapSet a b
MapSet.empty (Set (SORT, OpType) -> OpMap) -> Set (SORT, OpType) -> OpMap
forall a b. (a -> b) -> a -> b
$ [Named (FORMULA EM_FORMULA)] -> Set (SORT, OpType)
forall f. [Named (FORMULA f)] -> Set (SORT, OpType)
getConstructors [Named (FORMULA EM_FORMULA)]
sens)
(OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps (EModalSign -> OpMap) -> EModalSign -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sig
in Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OpMap -> Bool
forall a b. MapSet a b -> Bool
MapSet.null OpMap
cs) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "constructors must not be flexible:\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Doc -> Doc -> Map SORT (Set OpType) -> Doc
forall k a.
(Pretty k, Pretty a) =>
Doc -> Doc -> Map k (Set a) -> Doc
printSetMap Doc
empty Doc
empty (Map SORT (Set OpType) -> Doc) -> Map SORT (Set OpType) -> Doc
forall a b. (a -> b) -> a -> b
$ OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
cs)
frmTypeAna :: Min EM_FORMULA EModalSign
frmTypeAna :: Min EM_FORMULA EModalSign
frmTypeAna sign :: Sign EM_FORMULA EModalSign
sign form :: EM_FORMULA
form = let
checkMod :: MODALITY -> Result MODALITY
checkMod term_mod :: MODALITY
term_mod = case MODALITY
term_mod of
SimpleMod s_id :: SIMPLE_ID
s_id ->
if SIMPLE_ID -> String
tokStr SIMPLE_ID
s_id String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
emptyS
Bool -> Bool -> Bool
|| SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
s_id) (EModalSign -> Set SORT
modalities (EModalSign -> Set SORT) -> EModalSign -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sign)
then MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
SimpleMod SIMPLE_ID
s_id
else [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SIMPLE_ID -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown modality" SIMPLE_ID
s_id]
(Maybe MODALITY -> Result MODALITY)
-> Maybe MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Maybe MODALITY
forall a. a -> Maybe a
Just (MODALITY -> Maybe MODALITY) -> MODALITY -> Maybe MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
SimpleMod SIMPLE_ID
s_id
ModOp o :: ModOp
o md1 :: MODALITY
md1 md2 :: MODALITY
md2 -> do
MODALITY
new_md1 <- MODALITY -> Result MODALITY
checkMod MODALITY
md1
MODALITY
new_md2 <- MODALITY -> Result MODALITY
checkMod MODALITY
md2
MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ ModOp -> MODALITY -> MODALITY -> MODALITY
ModOp ModOp
o MODALITY
new_md1 MODALITY
new_md2
TransClos md :: MODALITY
md -> (MODALITY -> MODALITY) -> Result MODALITY -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MODALITY -> MODALITY
TransClos (Result MODALITY -> Result MODALITY)
-> Result MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Result MODALITY
checkMod MODALITY
md
Guard frm :: FORMULA EM_FORMULA
frm -> (FORMULA EM_FORMULA -> MODALITY)
-> Result (FORMULA EM_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FORMULA EM_FORMULA -> MODALITY
Guard (Result (FORMULA EM_FORMULA) -> Result MODALITY)
-> Result (FORMULA EM_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign FORMULA EM_FORMULA
frm
TermMod t :: TERM EM_FORMULA
t -> let
ms :: Set SORT
ms = EModalSign -> Set SORT
modalities (EModalSign -> Set SORT) -> EModalSign -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sign
r :: Result MODALITY
r = do
TERM EM_FORMULA
t2 <- Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> TERM EM_FORMULA
-> Result (TERM EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign TERM EM_FORMULA
t
let srt :: SORT
srt = TERM EM_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM EM_FORMULA
t2
trm :: MODALITY
trm = TERM EM_FORMULA -> MODALITY
TermMod TERM EM_FORMULA
t2
supers :: Set SORT
supers = SORT -> Sign EM_FORMULA EModalSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
srt Sign EM_FORMULA EModalSign
sign
if Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
srt Set SORT
supers) Set SORT
ms
then [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> TERM EM_FORMULA -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
("unknown term modality sort '"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
showId SORT
srt "' for term") TERM EM_FORMULA
t ]
(Maybe MODALITY -> Result MODALITY)
-> Maybe MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Maybe MODALITY
forall a. a -> Maybe a
Just MODALITY
trm
else MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
trm
in case TERM EM_FORMULA
t of
Mixfix_token tm :: SIMPLE_ID
tm ->
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
tm) Set SORT
ms
Bool -> Bool -> Bool
|| SIMPLE_ID -> String
tokStr SIMPLE_ID
tm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
emptyS
then MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
SimpleMod SIMPLE_ID
tm
else [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result
[DiagKind -> String -> SIMPLE_ID -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown modality" SIMPLE_ID
tm]
(Maybe MODALITY -> Result MODALITY)
-> Maybe MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MODALITY -> Maybe MODALITY
forall a. a -> Maybe a
Just (MODALITY -> Maybe MODALITY) -> MODALITY -> Maybe MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
SimpleMod SIMPLE_ID
tm
Application (Op_name (Id [tm :: SIMPLE_ID
tm] [] _)) [] _ ->
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
tm) Set SORT
ms
then MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> MODALITY
SimpleMod SIMPLE_ID
tm
else Result MODALITY
r
_ -> Result MODALITY
r
checkFrame :: FrameForm -> Result FrameForm
checkFrame (FrameForm vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA EM_FORMULA)]
fs r :: Range
r) = do
[Annoted (FORMULA EM_FORMULA)]
nfs <- (FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA))
-> [Annoted (FORMULA EM_FORMULA)]
-> Result [Annoted (FORMULA EM_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign (FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA))
-> (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vs) [Annoted (FORMULA EM_FORMULA)]
fs
FrameForm -> Result FrameForm
forall (m :: * -> *) a. Monad m => a -> m a
return (FrameForm -> Result FrameForm) -> FrameForm -> Result FrameForm
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [] [Annoted (FORMULA EM_FORMULA)]
nfs Range
r
checkPrefix :: FormPrefix -> Result FormPrefix
checkPrefix pf :: FormPrefix
pf = case FormPrefix
pf of
BoxOrDiamond choice :: BoxOp
choice md :: MODALITY
md leq_geq :: Bool
leq_geq number :: Int
number -> do
MODALITY
new_md <- MODALITY -> Result MODALITY
checkMod MODALITY
md
let new_pf :: FormPrefix
new_pf = BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
choice MODALITY
new_md Bool
leq_geq Int
number
if Int
number Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0
then FormPrefix -> Result FormPrefix
forall (m :: * -> *) a. Monad m => a -> m a
return FormPrefix
new_pf
else [Diagnosis] -> Maybe FormPrefix -> Result FormPrefix
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Int -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "negative number grading" Int
number]
(Maybe FormPrefix -> Result FormPrefix)
-> Maybe FormPrefix -> Result FormPrefix
forall a b. (a -> b) -> a -> b
$ FormPrefix -> Maybe FormPrefix
forall a. a -> Maybe a
Just FormPrefix
new_pf
Hybrid _ nm :: SIMPLE_ID
nm ->
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SIMPLE_ID -> SORT
nomPId SIMPLE_ID
nm) (EModalSign -> Set SORT
nominals (EModalSign -> Set SORT) -> EModalSign -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign EM_FORMULA EModalSign
sign)
then FormPrefix -> Result FormPrefix
forall (m :: * -> *) a. Monad m => a -> m a
return FormPrefix
pf
else [Diagnosis] -> Maybe FormPrefix -> Result FormPrefix
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SIMPLE_ID -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown nominal" SIMPLE_ID
nm]
(Maybe FormPrefix -> Result FormPrefix)
-> Maybe FormPrefix -> Result FormPrefix
forall a b. (a -> b) -> a -> b
$ FormPrefix -> Maybe FormPrefix
forall a. a -> Maybe a
Just FormPrefix
pf
_ -> FormPrefix -> Result FormPrefix
forall (m :: * -> *) a. Monad m => a -> m a
return FormPrefix
pf
in case EM_FORMULA
form of
PrefixForm pf :: FormPrefix
pf f :: FORMULA EM_FORMULA
f pos :: Range
pos -> do
FormPrefix
new_pf <- FormPrefix -> Result FormPrefix
checkPrefix FormPrefix
pf
FORMULA EM_FORMULA
new_f <- Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign FORMULA EM_FORMULA
f
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
PrefixForm FormPrefix
new_pf FORMULA EM_FORMULA
new_f Range
pos
UntilSince choice :: Bool
choice f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 pos :: Range
pos -> do
FORMULA EM_FORMULA
new_f1 <- Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign FORMULA EM_FORMULA
f1
FORMULA EM_FORMULA
new_f2 <- Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sign FORMULA EM_FORMULA
f2
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
choice FORMULA EM_FORMULA
new_f1 FORMULA EM_FORMULA
new_f2 Range
pos
ModForm (ModDefn is_time :: Bool
is_time isTerm :: Bool
isTerm anno_list :: [Annoted SORT]
anno_list forms :: [Annoted FrameForm]
forms pos :: Range
pos) -> do
[Annoted FrameForm]
new_forms <- (FrameForm -> Result FrameForm)
-> [Annoted FrameForm] -> Result [Annoted FrameForm]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM FrameForm -> Result FrameForm
checkFrame [Annoted FrameForm]
forms
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ ModDefn -> EM_FORMULA
ModForm (ModDefn -> EM_FORMULA) -> ModDefn -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> [Annoted SORT]
-> [Annoted FrameForm]
-> Range
-> ModDefn
ModDefn Bool
is_time Bool
isTerm [Annoted SORT]
anno_list [Annoted FrameForm]
new_forms Range
pos
anaFrameForm :: Mix b s EM_FORMULA EModalSign -> FrameForm
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
anaFrameForm :: Mix b s EM_FORMULA EModalSign
-> FrameForm
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
anaFrameForm mix :: Mix b s EM_FORMULA EModalSign
mix ff :: FrameForm
ff@(FrameForm vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA EM_FORMULA)]
fs r :: Range
r) = if [Annoted (FORMULA EM_FORMULA)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (FORMULA EM_FORMULA)]
fs then do
(VAR_DECL -> State (Sign EM_FORMULA EModalSign) ())
-> [VAR_DECL] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign EM_FORMULA EModalSign) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs
(FrameForm, FrameForm)
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
forall (m :: * -> *) a. Monad m => a -> m a
return (FrameForm
ff, FrameForm
ff)
else do
(resFs :: [Annoted (FORMULA EM_FORMULA)]
resFs, fufs :: [Annoted (FORMULA EM_FORMULA)]
fufs) <- (Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA))
-> [VAR_DECL]
-> [Annoted (FORMULA EM_FORMULA)]
-> Range
-> State
(Sign EM_FORMULA EModalSign)
([Annoted (FORMULA EM_FORMULA)], [Annoted (FORMULA EM_FORMULA)])
forall f e.
TermExtension f =>
(Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
anaLocalVarForms (Mix b s EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)
forall b s.
Mix b s EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)
anaFORMULA Mix b s EM_FORMULA EModalSign
mix) [VAR_DECL]
vs [Annoted (FORMULA EM_FORMULA)]
fs Range
r
(FrameForm, FrameForm)
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs [Annoted (FORMULA EM_FORMULA)]
resFs Range
r, [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [] [Annoted (FORMULA EM_FORMULA)]
fufs Range
r)
clearVarMap :: State (Sign f e) ()
clearVarMap :: State (Sign f e) ()
clearVarMap = do
Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get
Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty }
modItemStatAna
:: Ana ModDefn EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
modItemStatAna :: Ana ModDefn EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
modItemStatAna mix :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix (ModDefn is_time :: Bool
is_time isTerm :: Bool
isTerm anno_list :: [Annoted SORT]
anno_list forms :: [Annoted FrameForm]
forms pos :: Range
pos) = do
(Annoted SORT -> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted SORT] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (SORT -> EModalSign -> Result EModalSign)
-> SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> EModalSign -> Result EModalSign
addMod) (SORT -> State (Sign EM_FORMULA EModalSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item ) [Annoted SORT]
anno_list
State (Sign EM_FORMULA EModalSign) ()
forall f e. State (Sign f e) ()
clearVarMap
[Annoted (FrameForm, FrameForm)]
new_forms <- (FrameForm
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm))
-> [Annoted FrameForm]
-> State
(Sign EM_FORMULA EModalSign) [Annoted (FrameForm, FrameForm)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> FrameForm
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
forall b s.
Mix b s EM_FORMULA EModalSign
-> FrameForm
-> State (Sign EM_FORMULA EModalSign) (FrameForm, FrameForm)
anaFrameForm Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix) [Annoted FrameForm]
forms
State (Sign EM_FORMULA EModalSign) ()
forall f e. State (Sign f e) ()
clearVarMap
let res_forms :: [Annoted FrameForm]
res_forms = (Annoted (FrameForm, FrameForm) -> Annoted FrameForm)
-> [Annoted (FrameForm, FrameForm)] -> [Annoted FrameForm]
forall a b. (a -> b) -> [a] -> [b]
map (((FrameForm, FrameForm) -> FrameForm)
-> Annoted (FrameForm, FrameForm) -> Annoted FrameForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FrameForm, FrameForm) -> FrameForm
forall a b. (a, b) -> a
fst) [Annoted (FrameForm, FrameForm)]
new_forms
ana_forms :: [Annoted FrameForm]
ana_forms = (Annoted FrameForm -> Bool)
-> [Annoted FrameForm] -> [Annoted FrameForm]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Annoted FrameForm -> Bool) -> Annoted FrameForm -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Annoted (FORMULA EM_FORMULA)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Annoted (FORMULA EM_FORMULA)] -> Bool)
-> (Annoted FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> Annoted FrameForm
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FrameForm -> [Annoted (FORMULA EM_FORMULA)]
frameForms (FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> (Annoted FrameForm -> FrameForm)
-> Annoted FrameForm
-> [Annoted (FORMULA EM_FORMULA)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item)
([Annoted FrameForm] -> [Annoted FrameForm])
-> [Annoted FrameForm] -> [Annoted FrameForm]
forall a b. (a -> b) -> a -> b
$ (Annoted (FrameForm, FrameForm) -> Annoted FrameForm)
-> [Annoted (FrameForm, FrameForm)] -> [Annoted FrameForm]
forall a b. (a -> b) -> [a] -> [b]
map (((FrameForm, FrameForm) -> FrameForm)
-> Annoted (FrameForm, FrameForm) -> Annoted FrameForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FrameForm, FrameForm) -> FrameForm
forall a b. (a, b) -> b
snd) [Annoted (FrameForm, FrameForm)]
new_forms
Bool
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Annoted FrameForm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted FrameForm]
ana_forms)
(State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ())
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ [Named (FORMULA EM_FORMULA)]
-> State (Sign EM_FORMULA EModalSign) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA EM_FORMULA)]
-> State (Sign EM_FORMULA EModalSign) ())
-> [Named (FORMULA EM_FORMULA)]
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ (Annoted FrameForm -> Named (FORMULA EM_FORMULA))
-> [Annoted FrameForm] -> [Named (FORMULA EM_FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map (\ af :: Annoted FrameForm
af ->
(String -> FORMULA EM_FORMULA -> Named (FORMULA EM_FORMULA)
forall a s. a -> s -> SenAttr s a
makeNamed (Annoted FrameForm -> String
forall a. Annoted a -> String
getRLabel Annoted FrameForm
af) (FORMULA EM_FORMULA -> Named (FORMULA EM_FORMULA))
-> FORMULA EM_FORMULA -> Named (FORMULA EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ EM_FORMULA -> FORMULA EM_FORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA -> FORMULA EM_FORMULA
forall a b. (a -> b) -> a -> b
$ ModDefn -> EM_FORMULA
ModForm
(ModDefn -> EM_FORMULA) -> ModDefn -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> [Annoted SORT]
-> [Annoted FrameForm]
-> Range
-> ModDefn
ModDefn Bool
is_time Bool
isTerm [Annoted SORT]
anno_list [FrameForm -> Annoted FrameForm
forall a. a -> Annoted a
emptyAnno (FrameForm -> Annoted FrameForm) -> FrameForm -> Annoted FrameForm
forall a b. (a -> b) -> a -> b
$ Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item Annoted FrameForm
af] Range
pos)
{ isAxiom :: Bool
isAxiom = Annoted FrameForm -> Bool
forall a. Annoted a -> Bool
notImplied Annoted FrameForm
af })
[Annoted FrameForm]
ana_forms
Bool
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
is_time (State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ())
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ (Annoted SORT -> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted SORT] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (Annoted SORT -> EModalSign -> Result EModalSign)
-> Annoted SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> EModalSign -> Result EModalSign
addTimeMod (SORT -> EModalSign -> Result EModalSign)
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> EModalSign
-> Result EModalSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item ) [Annoted SORT]
anno_list
Bool
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isTerm (State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ())
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ do
Sign EM_FORMULA EModalSign
sig <- State (Sign EM_FORMULA EModalSign) (Sign EM_FORMULA EModalSign)
forall s. State s s
get
(Annoted SORT -> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted SORT] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (SORT -> EModalSign -> Result EModalSign)
-> SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign EM_FORMULA EModalSign
-> SORT -> EModalSign -> Result EModalSign
forall f e. Sign f e -> SORT -> EModalSign -> Result EModalSign
addTermMod Sign EM_FORMULA EModalSign
sig) (SORT -> State (Sign EM_FORMULA EModalSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item ) [Annoted SORT]
anno_list
ModDefn -> State (Sign EM_FORMULA EModalSign) ModDefn
forall (m :: * -> *) a. Monad m => a -> m a
return (ModDefn -> State (Sign EM_FORMULA EModalSign) ModDefn)
-> ModDefn -> State (Sign EM_FORMULA EModalSign) ModDefn
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> [Annoted SORT]
-> [Annoted FrameForm]
-> Range
-> ModDefn
ModDefn Bool
is_time Bool
isTerm [Annoted SORT]
anno_list [Annoted FrameForm]
res_forms Range
pos
basItemStatAna
:: Ana EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
basItemStatAna :: Ana EM_BASIC_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
basItemStatAna mix :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix basic_item :: EM_BASIC_ITEM
basic_item = case EM_BASIC_ITEM
basic_item of
ModItem md :: ModDefn
md -> (ModDefn -> EM_BASIC_ITEM)
-> State (Sign EM_FORMULA EModalSign) ModDefn
-> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModDefn -> EM_BASIC_ITEM
ModItem (State (Sign EM_FORMULA EModalSign) ModDefn
-> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM)
-> State (Sign EM_FORMULA EModalSign) ModDefn
-> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ Ana ModDefn EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
modItemStatAna Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix ModDefn
md
Nominal_decl anno_list :: [Annoted SIMPLE_ID]
anno_list pos :: Range
pos -> do
(Annoted SIMPLE_ID -> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (Annoted SIMPLE_ID -> EModalSign -> Result EModalSign)
-> Annoted SIMPLE_ID
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> EModalSign -> Result EModalSign
addNom (SORT -> EModalSign -> Result EModalSign)
-> (Annoted SIMPLE_ID -> SORT)
-> Annoted SIMPLE_ID
-> EModalSign
-> Result EModalSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> SORT
nomPId (SIMPLE_ID -> SORT)
-> (Annoted SIMPLE_ID -> SIMPLE_ID) -> Annoted SIMPLE_ID -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
anno_list
(Annoted SIMPLE_ID -> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annoted ()
-> PredType -> SORT -> State (Sign EM_FORMULA EModalSign) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) PredType
nomPType (SORT -> State (Sign EM_FORMULA EModalSign) ())
-> (Annoted SIMPLE_ID -> SORT)
-> Annoted SIMPLE_ID
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> SORT
nomPId (SIMPLE_ID -> SORT)
-> (Annoted SIMPLE_ID -> SIMPLE_ID) -> Annoted SIMPLE_ID -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
anno_list
EM_BASIC_ITEM -> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_BASIC_ITEM -> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM)
-> EM_BASIC_ITEM
-> State (Sign EM_FORMULA EModalSign) EM_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SIMPLE_ID] -> Range -> EM_BASIC_ITEM
Nominal_decl [Annoted SIMPLE_ID]
anno_list Range
pos
addTermMod :: Sign f e -> Id -> EModalSign -> Result EModalSign
addTermMod :: Sign f e -> SORT -> EModalSign -> Result EModalSign
addTermMod fullSign :: Sign f e
fullSign tmi :: SORT
tmi sgn :: EModalSign
sgn = let
tm :: Set SORT
tm = EModalSign -> Set SORT
termMods EModalSign
sgn
srts :: Set SORT
srts = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
fullSign
in if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
tmi Set SORT
srts then
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
tmi Set SORT
tm
then [Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "repeated term modality" SORT
tmi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else let sps :: Set SORT
sps = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
tm (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
tmi Sign f e
fullSign in
if Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
sps
then EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return EModalSign
sgn { termMods :: Set SORT
termMods = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
tmi Set SORT
tm }
else [Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
("term modality known for supersorts " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set SORT
sps "")
SORT
tmi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else [Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown sort in term modality" SORT
tmi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
addTimeMod :: Id -> EModalSign -> Result EModalSign
addTimeMod :: SORT -> EModalSign -> Result EModalSign
addTimeMod tmi :: SORT
tmi sgn :: EModalSign
sgn = let tm :: Set SORT
tm = EModalSign -> Set SORT
timeMods EModalSign
sgn in
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
tmi Set SORT
tm
then [Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "repeated time modality" SORT
tmi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else if Set SORT -> Int
forall a. Set a -> Int
Set.size Set SORT
tm Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1
then [Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "more than one time modality" SORT
tmi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return EModalSign
sgn { timeMods :: Set SORT
timeMods = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
tmi Set SORT
tm }
addMod :: Id -> EModalSign -> Result EModalSign
addMod :: SORT -> EModalSign -> Result EModalSign
addMod mi :: SORT
mi sgn :: EModalSign
sgn =
let m :: Set SORT
m = EModalSign -> Set SORT
modalities EModalSign
sgn in
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
mi Set SORT
m then
[Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "repeated modality" SORT
mi] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return EModalSign
sgn { modalities :: Set SORT
modalities = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
mi Set SORT
m }
addNom :: Id -> EModalSign -> Result EModalSign
addNom :: SORT -> EModalSign -> Result EModalSign
addNom ni :: SORT
ni sgn :: EModalSign
sgn =
let n :: Set SORT
n = EModalSign -> Set SORT
nominals EModalSign
sgn in
if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
ni Set SORT
n then
[Diagnosis] -> Maybe EModalSign -> Result EModalSign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "repeated nominal" SORT
ni] (Maybe EModalSign -> Result EModalSign)
-> Maybe EModalSign -> Result EModalSign
forall a b. (a -> b) -> a -> b
$ EModalSign -> Maybe EModalSign
forall a. a -> Maybe a
Just EModalSign
sgn
else EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return EModalSign
sgn { nominals :: Set SORT
nominals = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
ni Set SORT
n }
sigItemStatAna
:: Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
sigItemStatAna :: Ana EM_SIG_ITEM EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
sigItemStatAna mix :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix sig_item :: EM_SIG_ITEM
sig_item = case EM_SIG_ITEM
sig_item of
Rigid_op_items rig :: Bool
rig ann_list :: [Annoted (OP_ITEM EM_FORMULA)]
ann_list pos :: Range
pos -> do
[Annoted (OP_ITEM EM_FORMULA)]
new_list <- (Annoted (OP_ITEM EM_FORMULA)
-> State
(Sign EM_FORMULA EModalSign) (Annoted (OP_ITEM EM_FORMULA)))
-> [Annoted (OP_ITEM EM_FORMULA)]
-> State
(Sign EM_FORMULA EModalSign) [Annoted (OP_ITEM EM_FORMULA)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min EM_FORMULA EModalSign
-> Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> Annoted (OP_ITEM EM_FORMULA)
-> State
(Sign EM_FORMULA EModalSign) (Annoted (OP_ITEM EM_FORMULA))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Annoted (OP_ITEM f)
-> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM Min EM_FORMULA EModalSign
frmTypeAna Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix) [Annoted (OP_ITEM EM_FORMULA)]
ann_list
Bool
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
rig (State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ())
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ (Annoted (OP_ITEM EM_FORMULA)
-> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted (OP_ITEM EM_FORMULA)]
-> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
(\ nlitem :: Annoted (OP_ITEM EM_FORMULA)
nlitem -> case Annoted (OP_ITEM EM_FORMULA) -> OP_ITEM EM_FORMULA
forall a. Annoted a -> a
item Annoted (OP_ITEM EM_FORMULA)
nlitem of
Op_decl ops :: [SORT]
ops typ :: OP_TYPE
typ _ _ ->
(SORT -> State (Sign EM_FORMULA EModalSign) ())
-> [SORT] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (SORT -> EModalSign -> Result EModalSign)
-> SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> SORT -> EModalSign -> Result EModalSign
addFlexOp (OP_TYPE -> OpType
toOpType OP_TYPE
typ)) [SORT]
ops
Op_defn op :: SORT
op hd :: OP_HEAD
hd _ _ -> State (Sign EM_FORMULA EModalSign) ()
-> (OP_TYPE -> State (Sign EM_FORMULA EModalSign) ())
-> Maybe OP_TYPE
-> State (Sign EM_FORMULA EModalSign) ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> State (Sign EM_FORMULA EModalSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
(\ ty :: OP_TYPE
ty -> (EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ OpType -> SORT -> EModalSign -> Result EModalSign
addFlexOp (OP_TYPE -> OpType
toOpType OP_TYPE
ty) SORT
op)
(Maybe OP_TYPE -> State (Sign EM_FORMULA EModalSign) ())
-> Maybe OP_TYPE -> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
hd
) [Annoted (OP_ITEM EM_FORMULA)]
new_list
EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM)
-> EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM
forall a b. (a -> b) -> a -> b
$ Bool -> [Annoted (OP_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM
Rigid_op_items Bool
rig [Annoted (OP_ITEM EM_FORMULA)]
new_list Range
pos
Rigid_pred_items rig :: Bool
rig ann_list :: [Annoted (PRED_ITEM EM_FORMULA)]
ann_list pos :: Range
pos -> do
[Annoted (PRED_ITEM EM_FORMULA)]
new_list <- (Annoted (PRED_ITEM EM_FORMULA)
-> State
(Sign EM_FORMULA EModalSign) (Annoted (PRED_ITEM EM_FORMULA)))
-> [Annoted (PRED_ITEM EM_FORMULA)]
-> State
(Sign EM_FORMULA EModalSign) [Annoted (PRED_ITEM EM_FORMULA)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min EM_FORMULA EModalSign
-> Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
-> Annoted (PRED_ITEM EM_FORMULA)
-> State
(Sign EM_FORMULA EModalSign) (Annoted (PRED_ITEM EM_FORMULA))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Annoted (PRED_ITEM f)
-> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM Min EM_FORMULA EModalSign
frmTypeAna Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mix) [Annoted (PRED_ITEM EM_FORMULA)]
ann_list
Bool
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
rig (State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ())
-> State (Sign EM_FORMULA EModalSign) ()
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ (Annoted (PRED_ITEM EM_FORMULA)
-> State (Sign EM_FORMULA EModalSign) ())
-> [Annoted (PRED_ITEM EM_FORMULA)]
-> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ nlitem :: Annoted (PRED_ITEM EM_FORMULA)
nlitem -> case Annoted (PRED_ITEM EM_FORMULA) -> PRED_ITEM EM_FORMULA
forall a. Annoted a -> a
item Annoted (PRED_ITEM EM_FORMULA)
nlitem of
Pred_decl preds :: [SORT]
preds typ :: PRED_TYPE
typ _ ->
(SORT -> State (Sign EM_FORMULA EModalSign) ())
-> [SORT] -> State (Sign EM_FORMULA EModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (SORT -> EModalSign -> Result EModalSign)
-> SORT
-> State (Sign EM_FORMULA EModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> SORT -> EModalSign -> Result EModalSign
addFlexPred (PRED_TYPE -> PredType
toPredType PRED_TYPE
typ) ) [SORT]
preds
Pred_defn prd :: SORT
prd (Pred_head args :: [VAR_DECL]
args _ ) _ _ ->
(EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ())
-> (EModalSign -> Result EModalSign)
-> State (Sign EM_FORMULA EModalSign) ()
forall a b. (a -> b) -> a -> b
$ PredType -> SORT -> EModalSign -> Result EModalSign
addFlexPred ([SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
args) SORT
prd
) [Annoted (PRED_ITEM EM_FORMULA)]
new_list
EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM)
-> EM_SIG_ITEM -> State (Sign EM_FORMULA EModalSign) EM_SIG_ITEM
forall a b. (a -> b) -> a -> b
$ Bool -> [Annoted (PRED_ITEM EM_FORMULA)] -> Range -> EM_SIG_ITEM
Rigid_pred_items Bool
rig [Annoted (PRED_ITEM EM_FORMULA)]
new_list Range
pos
addFlexOp :: OpType -> Id -> EModalSign -> Result EModalSign
addFlexOp :: OpType -> SORT -> EModalSign -> Result EModalSign
addFlexOp typ :: OpType
typ i :: SORT
i sgn :: EModalSign
sgn = EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return
EModalSign
sgn { flexOps :: OpMap
flexOps = SORT -> OpType -> OpMap -> OpMap
addOpTo SORT
i OpType
typ (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
sgn }
addFlexPred :: PredType -> Id -> EModalSign -> Result EModalSign
addFlexPred :: PredType -> SORT -> EModalSign -> Result EModalSign
addFlexPred typ :: PredType
typ i :: SORT
i sgn :: EModalSign
sgn = EModalSign -> Result EModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return
EModalSign
sgn { flexPreds :: PredMap
flexPreds = SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
i PredType
typ (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> PredMap
flexPreds EModalSign
sgn }
mixfixAna :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mixfixAna :: Mix EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA EModalSign
mixfixAna = Mix EM_BASIC_ITEM Any Any EModalSign
forall b s f e. Mix b s f e
emptyMix
{ getSigIds :: EM_SIG_ITEM -> IdSets
getSigIds = EM_SIG_ITEM -> IdSets
extraSigItems
, putParen :: EM_FORMULA -> EM_FORMULA
putParen = EM_FORMULA -> EM_FORMULA
parenExtForm
, mixResolve :: MixResolve EM_FORMULA
mixResolve = MixResolve EM_FORMULA
resolveExtForm
}
extraSigItems :: EM_SIG_ITEM -> IdSets
s :: EM_SIG_ITEM
s = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case EM_SIG_ITEM
s of
Rigid_op_items _ annoted_list :: [Annoted (OP_ITEM EM_FORMULA)]
annoted_list _ ->
([(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
unite2 ([(Set SORT, Set SORT)] -> (Set SORT, Set SORT))
-> [(Set SORT, Set SORT)] -> (Set SORT, Set SORT)
forall a b. (a -> b) -> a -> b
$ (Annoted (OP_ITEM EM_FORMULA) -> (Set SORT, Set SORT))
-> [Annoted (OP_ITEM EM_FORMULA)] -> [(Set SORT, Set SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM EM_FORMULA -> (Set SORT, Set SORT)
forall f. OP_ITEM f -> (Set SORT, Set SORT)
ids_OP_ITEM (OP_ITEM EM_FORMULA -> (Set SORT, Set SORT))
-> (Annoted (OP_ITEM EM_FORMULA) -> OP_ITEM EM_FORMULA)
-> Annoted (OP_ITEM EM_FORMULA)
-> (Set SORT, Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM EM_FORMULA) -> OP_ITEM EM_FORMULA
forall a. Annoted a -> a
item) [Annoted (OP_ITEM EM_FORMULA)]
annoted_list, Set SORT
forall a. Set a
e)
Rigid_pred_items _ annoted_list :: [Annoted (PRED_ITEM EM_FORMULA)]
annoted_list _ ->
((Set SORT
forall a. Set a
e, Set SORT
forall a. Set a
e), [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Annoted (PRED_ITEM EM_FORMULA) -> Set SORT)
-> [Annoted (PRED_ITEM EM_FORMULA)] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (PRED_ITEM EM_FORMULA -> Set SORT
forall f. PRED_ITEM f -> Set SORT
ids_PRED_ITEM (PRED_ITEM EM_FORMULA -> Set SORT)
-> (Annoted (PRED_ITEM EM_FORMULA) -> PRED_ITEM EM_FORMULA)
-> Annoted (PRED_ITEM EM_FORMULA)
-> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (PRED_ITEM EM_FORMULA) -> PRED_ITEM EM_FORMULA
forall a. Annoted a -> a
item) [Annoted (PRED_ITEM EM_FORMULA)]
annoted_list)
parenExtForm :: EM_FORMULA -> EM_FORMULA
parenExtForm :: EM_FORMULA -> EM_FORMULA
parenExtForm = (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA -> EM_FORMULA
mapExtForm ((EM_FORMULA -> EM_FORMULA)
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula EM_FORMULA -> EM_FORMULA
parenExtForm)
mapExtMod :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> MODALITY -> MODALITY
mapExtMod :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> MODALITY -> MODALITY
mapExtMod f :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f m :: MODALITY
m = case MODALITY
m of
ModOp o :: ModOp
o md1 :: MODALITY
md1 md2 :: MODALITY
md2 -> (MODALITY -> MODALITY -> MODALITY)
-> (MODALITY -> MODALITY) -> MODALITY -> MODALITY -> MODALITY
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (ModOp -> MODALITY -> MODALITY -> MODALITY
ModOp ModOp
o) ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> MODALITY -> MODALITY
mapExtMod FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f) MODALITY
md1 MODALITY
md2
TransClos md :: MODALITY
md -> MODALITY -> MODALITY
TransClos (MODALITY -> MODALITY) -> MODALITY -> MODALITY
forall a b. (a -> b) -> a -> b
$ (FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> MODALITY -> MODALITY
mapExtMod FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f MODALITY
md
Guard frm :: FORMULA EM_FORMULA
frm -> FORMULA EM_FORMULA -> MODALITY
Guard (FORMULA EM_FORMULA -> MODALITY) -> FORMULA EM_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f FORMULA EM_FORMULA
frm
TermMod t :: TERM EM_FORMULA
t -> let Mixfix_formula n :: TERM EM_FORMULA
n = FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f (TERM EM_FORMULA -> FORMULA EM_FORMULA
forall f. TERM f -> FORMULA f
Mixfix_formula TERM EM_FORMULA
t) in TERM EM_FORMULA -> MODALITY
TermMod TERM EM_FORMULA
n
_ -> MODALITY
m
mapExtPrefix :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FormPrefix -> FormPrefix
mapExtPrefix :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FormPrefix -> FormPrefix
mapExtPrefix f :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f pf :: FormPrefix
pf = case FormPrefix
pf of
BoxOrDiamond choice :: BoxOp
choice md :: MODALITY
md leq_geq :: Bool
leq_geq nr :: Int
nr ->
BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
choice ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA) -> MODALITY -> MODALITY
mapExtMod FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f MODALITY
md) Bool
leq_geq Int
nr
_ -> FormPrefix
pf
mapExtForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA -> EM_FORMULA
mapExtForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> EM_FORMULA -> EM_FORMULA
mapExtForm f :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f ef :: EM_FORMULA
ef = case EM_FORMULA
ef of
PrefixForm p :: FormPrefix
p frm :: FORMULA EM_FORMULA
frm pos :: Range
pos ->
FormPrefix -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
PrefixForm ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FormPrefix -> FormPrefix
mapExtPrefix FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f FormPrefix
p) (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f FORMULA EM_FORMULA
frm) Range
pos
UntilSince choice :: Bool
choice f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 pos :: Range
pos ->
Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
choice (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f FORMULA EM_FORMULA
f1) (FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f FORMULA EM_FORMULA
f2) Range
pos
ModForm (ModDefn ti :: Bool
ti te :: Bool
te is :: [Annoted SORT]
is fs :: [Annoted FrameForm]
fs pos :: Range
pos) -> ModDefn -> EM_FORMULA
ModForm (ModDefn -> EM_FORMULA) -> ModDefn -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> [Annoted SORT]
-> [Annoted FrameForm]
-> Range
-> ModDefn
ModDefn
Bool
ti Bool
te [Annoted SORT]
is ((Annoted FrameForm -> Annoted FrameForm)
-> [Annoted FrameForm] -> [Annoted FrameForm]
forall a b. (a -> b) -> [a] -> [b]
map ((FrameForm -> FrameForm) -> Annoted FrameForm -> Annoted FrameForm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FrameForm -> FrameForm)
-> Annoted FrameForm -> Annoted FrameForm)
-> (FrameForm -> FrameForm)
-> Annoted FrameForm
-> Annoted FrameForm
forall a b. (a -> b) -> a -> b
$ (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FrameForm -> FrameForm
mapExtFrameForm FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f) [Annoted FrameForm]
fs) Range
pos
mapExtFrameForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FrameForm -> FrameForm
mapExtFrameForm :: (FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FrameForm -> FrameForm
mapExtFrameForm f :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f (FrameForm vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA EM_FORMULA)]
fs r :: Range
r) = [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs ((Annoted (FORMULA EM_FORMULA) -> Annoted (FORMULA EM_FORMULA))
-> [Annoted (FORMULA EM_FORMULA)] -> [Annoted (FORMULA EM_FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA) -> Annoted (FORMULA EM_FORMULA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FORMULA EM_FORMULA -> FORMULA EM_FORMULA
f) [Annoted (FORMULA EM_FORMULA)]
fs) Range
r
resolveMod :: MixResolve MODALITY
resolveMod :: MixResolve MODALITY
resolveMod ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids m :: MODALITY
m = case MODALITY
m of
ModOp o :: ModOp
o md1 :: MODALITY
md1 md2 :: MODALITY
md2 -> do
MODALITY
new_md1 <- MixResolve MODALITY
resolveMod GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
md1
MODALITY
new_md2 <- MixResolve MODALITY
resolveMod GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
md2
MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> Result MODALITY) -> MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ ModOp -> MODALITY -> MODALITY -> MODALITY
ModOp ModOp
o MODALITY
new_md1 MODALITY
new_md2
TransClos md :: MODALITY
md -> (MODALITY -> MODALITY) -> Result MODALITY -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MODALITY -> MODALITY
TransClos (Result MODALITY -> Result MODALITY)
-> Result MODALITY -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ MixResolve MODALITY
resolveMod GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
md
Guard frm :: FORMULA EM_FORMULA
frm -> (FORMULA EM_FORMULA -> MODALITY)
-> Result (FORMULA EM_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FORMULA EM_FORMULA -> MODALITY
Guard
(Result (FORMULA EM_FORMULA) -> Result MODALITY)
-> Result (FORMULA EM_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ (EM_FORMULA -> EM_FORMULA)
-> MixResolve EM_FORMULA -> MixResolve (FORMULA EM_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm EM_FORMULA -> EM_FORMULA
parenExtForm MixResolve EM_FORMULA
resolveExtForm GlobalAnnos
ga (TokRules, Rules)
ids FORMULA EM_FORMULA
frm
TermMod t :: TERM EM_FORMULA
t -> (TERM EM_FORMULA -> MODALITY)
-> Result (TERM EM_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM EM_FORMULA -> MODALITY
TermMod
(Result (TERM EM_FORMULA) -> Result MODALITY)
-> Result (TERM EM_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ (EM_FORMULA -> EM_FORMULA)
-> MixResolve EM_FORMULA -> MixResolve (TERM EM_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm EM_FORMULA -> EM_FORMULA
parenExtForm MixResolve EM_FORMULA
resolveExtForm GlobalAnnos
ga (TokRules, Rules)
ids TERM EM_FORMULA
t
_ -> MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
m
resolvePrefix :: MixResolve FormPrefix
resolvePrefix :: MixResolve FormPrefix
resolvePrefix ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids pf :: FormPrefix
pf = case FormPrefix
pf of
BoxOrDiamond choice :: BoxOp
choice ms :: MODALITY
ms leq_geq :: Bool
leq_geq nr :: Int
nr -> do
MODALITY
nms <- MixResolve MODALITY
resolveMod GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
ms
FormPrefix -> Result FormPrefix
forall (m :: * -> *) a. Monad m => a -> m a
return (FormPrefix -> Result FormPrefix)
-> FormPrefix -> Result FormPrefix
forall a b. (a -> b) -> a -> b
$ BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
choice MODALITY
nms Bool
leq_geq Int
nr
_ -> FormPrefix -> Result FormPrefix
forall (m :: * -> *) a. Monad m => a -> m a
return FormPrefix
pf
resolveExtForm :: MixResolve EM_FORMULA
resolveExtForm :: MixResolve EM_FORMULA
resolveExtForm ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids f :: EM_FORMULA
f =
let recResolve :: FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA)
recResolve = (EM_FORMULA -> EM_FORMULA)
-> MixResolve EM_FORMULA -> MixResolve (FORMULA EM_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm EM_FORMULA -> EM_FORMULA
parenExtForm MixResolve EM_FORMULA
resolveExtForm GlobalAnnos
ga (TokRules, Rules)
ids
in case EM_FORMULA
f of
PrefixForm p :: FormPrefix
p frm :: FORMULA EM_FORMULA
frm pos :: Range
pos -> do
FormPrefix
np <- MixResolve FormPrefix
resolvePrefix GlobalAnnos
ga (TokRules, Rules)
ids FormPrefix
p
FORMULA EM_FORMULA
new_frm <- FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA)
recResolve FORMULA EM_FORMULA
frm
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ FormPrefix -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
PrefixForm FormPrefix
np FORMULA EM_FORMULA
new_frm Range
pos
UntilSince choice :: Bool
choice f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 pos :: Range
pos -> do
FORMULA EM_FORMULA
new_f1 <- FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA)
recResolve FORMULA EM_FORMULA
f1
FORMULA EM_FORMULA
new_f2 <- FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA)
recResolve FORMULA EM_FORMULA
f2
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> FORMULA EM_FORMULA -> FORMULA EM_FORMULA -> Range -> EM_FORMULA
UntilSince Bool
choice FORMULA EM_FORMULA
new_f1 FORMULA EM_FORMULA
new_f2 Range
pos
ModForm (ModDefn ti :: Bool
ti te :: Bool
te is :: [Annoted SORT]
is fs :: [Annoted FrameForm]
fs pos :: Range
pos) -> do
[Annoted FrameForm]
nfs <- (FrameForm -> Result FrameForm)
-> [Annoted FrameForm] -> Result [Annoted FrameForm]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (MixResolve FrameForm
resolveFrameForm GlobalAnnos
ga (TokRules, Rules)
ids) [Annoted FrameForm]
fs
EM_FORMULA -> Result EM_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (EM_FORMULA -> Result EM_FORMULA)
-> EM_FORMULA -> Result EM_FORMULA
forall a b. (a -> b) -> a -> b
$ ModDefn -> EM_FORMULA
ModForm (ModDefn -> EM_FORMULA) -> ModDefn -> EM_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> [Annoted SORT]
-> [Annoted FrameForm]
-> Range
-> ModDefn
ModDefn Bool
ti Bool
te [Annoted SORT]
is [Annoted FrameForm]
nfs Range
pos
resolveFrameForm :: MixResolve FrameForm
resolveFrameForm :: MixResolve FrameForm
resolveFrameForm ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids (FrameForm vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA EM_FORMULA)]
fs r :: Range
r) = do
let ts :: Set SIMPLE_ID
ts = [VAR_DECL] -> Set SIMPLE_ID
varDeclTokens [VAR_DECL]
vs
[Annoted (FORMULA EM_FORMULA)]
nfs <- (FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA))
-> [Annoted (FORMULA EM_FORMULA)]
-> Result [Annoted (FORMULA EM_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM ((EM_FORMULA -> EM_FORMULA)
-> MixResolve EM_FORMULA -> MixResolve (FORMULA EM_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm EM_FORMULA -> EM_FORMULA
parenExtForm
(Set SIMPLE_ID -> MixResolve EM_FORMULA -> MixResolve EM_FORMULA
forall f. Set SIMPLE_ID -> MixResolve f -> MixResolve f
extendMixResolve Set SIMPLE_ID
ts MixResolve EM_FORMULA
resolveExtForm) GlobalAnnos
ga
((TokRules, Rules)
-> FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA))
-> (TokRules, Rules)
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall a b. (a -> b) -> a -> b
$ Set SIMPLE_ID -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set SIMPLE_ID
ts (TokRules, Rules)
ids) [Annoted (FORMULA EM_FORMULA)]
fs
FrameForm -> Result FrameForm
forall (m :: * -> *) a. Monad m => a -> m a
return (FrameForm -> Result FrameForm) -> FrameForm -> Result FrameForm
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [Annoted (FORMULA EM_FORMULA)] -> Range -> FrameForm
FrameForm [VAR_DECL]
vs [Annoted (FORMULA EM_FORMULA)]
nfs Range
r
anaFORMULA :: Mix b s EM_FORMULA EModalSign -> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA -> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)
anaFORMULA :: Mix b s EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)
anaFORMULA mix :: Mix b s EM_FORMULA EModalSign
mix sig :: Sign EM_FORMULA EModalSign
sig f :: FORMULA EM_FORMULA
f = do
let mix2 :: Mix b s EM_FORMULA EModalSign
mix2 = Set SIMPLE_ID
-> Mix b s EM_FORMULA EModalSign -> Mix b s EM_FORMULA EModalSign
forall b s f e. Set SIMPLE_ID -> Mix b s f e -> Mix b s f e
extendMix (Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall k a. Map k a -> Set k
Map.keysSet (Map SIMPLE_ID SORT -> Set SIMPLE_ID)
-> Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ Sign EM_FORMULA EModalSign -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign EM_FORMULA EModalSign
sig) Mix b s EM_FORMULA EModalSign
mix
FORMULA EM_FORMULA
r <- (EM_FORMULA -> EM_FORMULA)
-> MixResolve EM_FORMULA -> MixResolve (FORMULA EM_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula EM_FORMULA -> EM_FORMULA
parenExtForm
MixResolve EM_FORMULA
resolveExtForm (Sign EM_FORMULA EModalSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign EM_FORMULA EModalSign
sig) (Mix b s EM_FORMULA EModalSign -> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix b s EM_FORMULA EModalSign
mix2) FORMULA EM_FORMULA
f
let q :: FORMULA EM_FORMULA
q = (SIMPLE_ID -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA)
-> FORMULA EM_FORMULA -> Set SIMPLE_ID -> FORMULA EM_FORMULA
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
(\ t :: SIMPLE_ID
t -> SORT -> PRED_TYPE -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred (SIMPLE_ID -> SORT
simpleIdToId SIMPLE_ID
t) ([SORT] -> Range -> PRED_TYPE
Pred_type [] (Range -> PRED_TYPE) -> Range -> PRED_TYPE
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> Range
tokPos SIMPLE_ID
t))
FORMULA EM_FORMULA
r (Set SIMPLE_ID -> FORMULA EM_FORMULA)
-> Set SIMPLE_ID -> FORMULA EM_FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA EM_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA EM_FORMULA
f
FORMULA EM_FORMULA
n <- Min EM_FORMULA EModalSign
-> Sign EM_FORMULA EModalSign
-> FORMULA EM_FORMULA
-> Result (FORMULA EM_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min EM_FORMULA EModalSign
frmTypeAna Sign EM_FORMULA EModalSign
sig FORMULA EM_FORMULA
q
(FORMULA EM_FORMULA, FORMULA EM_FORMULA)
-> Result (FORMULA EM_FORMULA, FORMULA EM_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA EM_FORMULA
r, FORMULA EM_FORMULA
n)
getEFormPredToks :: EM_FORMULA -> Set.Set Token
getEFormPredToks :: EM_FORMULA -> Set SIMPLE_ID
getEFormPredToks ef :: EM_FORMULA
ef = case EM_FORMULA
ef of
PrefixForm _ f :: FORMULA EM_FORMULA
f _ -> FORMULA EM_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA EM_FORMULA
f
UntilSince _ f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 _ -> (Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID)
-> (FORMULA EM_FORMULA -> Set SIMPLE_ID)
-> FORMULA EM_FORMULA
-> FORMULA EM_FORMULA
-> Set SIMPLE_ID
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => Set a -> Set a -> Set a
Set.union FORMULA EM_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA EM_FORMULA
f1 FORMULA EM_FORMULA
f2
ModForm _ -> Set SIMPLE_ID
forall a. Set a
Set.empty
getFormPredToks :: FORMULA EM_FORMULA -> Set.Set Token
getFormPredToks :: FORMULA EM_FORMULA -> Set SIMPLE_ID
getFormPredToks = Record EM_FORMULA (Set SIMPLE_ID) (Set SIMPLE_ID)
-> FORMULA EM_FORMULA -> Set SIMPLE_ID
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
((EM_FORMULA -> Set SIMPLE_ID)
-> ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> Set SIMPLE_ID
-> Record EM_FORMULA (Set SIMPLE_ID) (Set SIMPLE_ID)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord EM_FORMULA -> Set SIMPLE_ID
getEFormPredToks [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set SIMPLE_ID
forall a. Set a
Set.empty)
{ foldMixfix_formula :: FORMULA EM_FORMULA -> Set SIMPLE_ID -> Set SIMPLE_ID
foldMixfix_formula = \ f :: FORMULA EM_FORMULA
f ts :: Set SIMPLE_ID
ts -> case FORMULA EM_FORMULA
f of
Mixfix_formula (Mixfix_token t :: SIMPLE_ID
t) -> SIMPLE_ID -> Set SIMPLE_ID
forall a. a -> Set a
Set.singleton SIMPLE_ID
t
_ -> Set SIMPLE_ID
ts
, foldQuantPred :: FORMULA EM_FORMULA
-> SORT -> PRED_TYPE -> Set SIMPLE_ID -> Set SIMPLE_ID
foldQuantPred = \ _ i :: SORT
i _ ts :: Set SIMPLE_ID
ts -> if SORT -> Bool
isSimpleId SORT
i then
SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => a -> Set a -> Set a
Set.delete (SORT -> SIMPLE_ID
idToSimpleId SORT
i) Set SIMPLE_ID
ts else Set SIMPLE_ID
ts
}