{- |
Module      :  ./ExtModal/StatAna.hs
Copyright   :  DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  codruta.liliana@gmail.com
Stability   :  experimental
Portability :  portable

static analysis of modal logic parts
-}

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 -- forget vars beyond this point
    [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 -- forget vars after this point
    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
extraSigItems :: EM_SIG_ITEM -> IdSets
extraSigItems 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
    -- the unknown predicates are not needed for mixfix resolution
    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
    }