{- |
Module      :  ./Modal/StatAna.hs
Copyright   :  (c) Christian Maeder, Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis of modal logic parts
-}

module Modal.StatAna (basicModalAnalysis, minExpForm) where

import Modal.AS_Modal
import Modal.Print_AS ()
import Modal.ModalSign

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.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 qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List as List
import Data.Function

instance TermExtension M_FORMULA where
    freeVarsOfExt :: Sign M_FORMULA e -> M_FORMULA -> VarSet
freeVarsOfExt sign :: Sign M_FORMULA e
sign (BoxOrDiamond _ _ f :: FORMULA M_FORMULA
f _) = Sign M_FORMULA e -> FORMULA M_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign M_FORMULA e
sign FORMULA M_FORMULA
f

basicModalAnalysis
  :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
      Sign M_FORMULA ModalSign, GlobalAnnos)
  -> Result (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
             ExtSign (Sign M_FORMULA ModalSign) Symbol,
             [Named (FORMULA M_FORMULA)])
basicModalAnalysis :: (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
 Sign M_FORMULA ModalSign, GlobalAnnos)
-> Result
     (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
      ExtSign (Sign M_FORMULA ModalSign) Symbol,
      [Named (FORMULA M_FORMULA)])
basicModalAnalysis =
    Min M_FORMULA ModalSign
-> Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
    Sign M_FORMULA ModalSign, GlobalAnnos)
-> Result
     (BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA,
      ExtSign (Sign M_FORMULA ModalSign) Symbol,
      [Named (FORMULA M_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 M_FORMULA ModalSign
minExpForm Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_BASIC_ITEM Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_SIG_ITEM Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_Mix

ana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_Mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_Mix = Mix M_BASIC_ITEM Any Any ModalSign
forall b s f e. Mix b s f e
emptyMix
    { getSigIds :: M_SIG_ITEM -> IdSets
getSigIds = M_SIG_ITEM -> IdSets
ids_M_SIG_ITEM
    , putParen :: M_FORMULA -> M_FORMULA
putParen = M_FORMULA -> M_FORMULA
mapM_FORMULA
    , mixResolve :: MixResolve M_FORMULA
mixResolve = MixResolve M_FORMULA
resolveM_FORMULA
    }

-- rigid ops will also be part of the CASL signature
ids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets
ids_M_SIG_ITEM :: M_SIG_ITEM -> IdSets
ids_M_SIG_ITEM si :: M_SIG_ITEM
si = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case M_SIG_ITEM
si of
    Rigid_op_items _ al :: [Annoted (OP_ITEM M_FORMULA)]
al _ ->
        ([(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 M_FORMULA) -> (Set SORT, Set SORT))
-> [Annoted (OP_ITEM M_FORMULA)] -> [(Set SORT, Set SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM M_FORMULA -> (Set SORT, Set SORT)
forall f. OP_ITEM f -> (Set SORT, Set SORT)
ids_OP_ITEM (OP_ITEM M_FORMULA -> (Set SORT, Set SORT))
-> (Annoted (OP_ITEM M_FORMULA) -> OP_ITEM M_FORMULA)
-> Annoted (OP_ITEM M_FORMULA)
-> (Set SORT, Set SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM M_FORMULA) -> OP_ITEM M_FORMULA
forall a. Annoted a -> a
item) [Annoted (OP_ITEM M_FORMULA)]
al, Set SORT
forall a. Set a
e)
    Rigid_pred_items _ al :: [Annoted (PRED_ITEM M_FORMULA)]
al _ ->
        ((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 M_FORMULA) -> Set SORT)
-> [Annoted (PRED_ITEM M_FORMULA)] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (PRED_ITEM M_FORMULA -> Set SORT
forall f. PRED_ITEM f -> Set SORT
ids_PRED_ITEM (PRED_ITEM M_FORMULA -> Set SORT)
-> (Annoted (PRED_ITEM M_FORMULA) -> PRED_ITEM M_FORMULA)
-> Annoted (PRED_ITEM M_FORMULA)
-> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (PRED_ITEM M_FORMULA) -> PRED_ITEM M_FORMULA
forall a. Annoted a -> a
item) [Annoted (PRED_ITEM M_FORMULA)]
al)

mapMODALITY :: MODALITY -> MODALITY
mapMODALITY :: MODALITY -> MODALITY
mapMODALITY m :: MODALITY
m = case MODALITY
m of
    Term_mod t :: TERM M_FORMULA
t -> TERM M_FORMULA -> MODALITY
Term_mod (TERM M_FORMULA -> MODALITY) -> TERM M_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ (M_FORMULA -> M_FORMULA) -> TERM M_FORMULA -> TERM M_FORMULA
forall f. (f -> f) -> TERM f -> TERM f
mapTerm M_FORMULA -> M_FORMULA
mapM_FORMULA TERM M_FORMULA
t
    _ -> MODALITY
m

mapM_FORMULA :: M_FORMULA -> M_FORMULA
mapM_FORMULA :: M_FORMULA -> M_FORMULA
mapM_FORMULA (BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA M_FORMULA
f ps :: Range
ps) =
    Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
b (MODALITY -> MODALITY
mapMODALITY MODALITY
m) ((M_FORMULA -> M_FORMULA) -> FORMULA M_FORMULA -> FORMULA M_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula M_FORMULA -> M_FORMULA
mapM_FORMULA FORMULA M_FORMULA
f) Range
ps

resolveMODALITY :: MixResolve MODALITY
resolveMODALITY :: MixResolve MODALITY
resolveMODALITY ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids m :: MODALITY
m = case MODALITY
m of
    Term_mod t :: TERM M_FORMULA
t -> (TERM M_FORMULA -> MODALITY)
-> Result (TERM M_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM M_FORMULA -> MODALITY
Term_mod (Result (TERM M_FORMULA) -> Result MODALITY)
-> Result (TERM M_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ (M_FORMULA -> M_FORMULA)
-> MixResolve M_FORMULA -> MixResolve (TERM M_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm M_FORMULA -> M_FORMULA
mapM_FORMULA
                  MixResolve M_FORMULA
resolveM_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids TERM M_FORMULA
t
    _ -> MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
m

resolveM_FORMULA :: MixResolve M_FORMULA
resolveM_FORMULA :: MixResolve M_FORMULA
resolveM_FORMULA ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids cf :: M_FORMULA
cf = case M_FORMULA
cf of
   BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA M_FORMULA
f ps :: Range
ps -> do
       MODALITY
nm <- MixResolve MODALITY
resolveMODALITY GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
m
       FORMULA M_FORMULA
nf <- (M_FORMULA -> M_FORMULA)
-> MixResolve M_FORMULA -> MixResolve (FORMULA M_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm M_FORMULA -> M_FORMULA
mapM_FORMULA MixResolve M_FORMULA
resolveM_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA M_FORMULA
f
       M_FORMULA -> Result M_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (M_FORMULA -> Result M_FORMULA) -> M_FORMULA -> Result M_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA M_FORMULA
nf Range
ps

minExpForm :: Min M_FORMULA ModalSign
minExpForm :: Min M_FORMULA ModalSign
minExpForm s :: Sign M_FORMULA ModalSign
s form :: M_FORMULA
form =
    let minMod :: MODALITY -> t -> Result MODALITY
minMod md :: MODALITY
md ps :: t
ps = case MODALITY
md of
                  Simple_mod i :: SIMPLE_ID
i -> MODALITY -> t -> Result MODALITY
minMod (TERM M_FORMULA -> MODALITY
Term_mod (SIMPLE_ID -> TERM M_FORMULA
forall f. SIMPLE_ID -> TERM f
Mixfix_token SIMPLE_ID
i)) t
ps
                  Term_mod t :: TERM M_FORMULA
t -> let
                    r :: Result MODALITY
r = do
                      TERM M_FORMULA
t2 <- Min M_FORMULA ModalSign
-> Sign M_FORMULA ModalSign
-> TERM M_FORMULA
-> Result (TERM M_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min M_FORMULA ModalSign
minExpForm Sign M_FORMULA ModalSign
s TERM M_FORMULA
t
                      let srt :: SORT
srt = TERM M_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM M_FORMULA
t2
                          trm :: MODALITY
trm = TERM M_FORMULA -> MODALITY
Term_mod TERM M_FORMULA
t2
                          supers :: Set SORT
supers = SORT -> Sign M_FORMULA ModalSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
srt Sign M_FORMULA ModalSign
s
                      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 -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Map SORT [AnModFORM] -> Set SORT
forall k a. Map k a -> Set k
Map.keysSet (Map SORT [AnModFORM] -> Set SORT)
-> Map SORT [AnModFORM] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SORT [AnModFORM]
termModies (ModalSign -> Map SORT [AnModFORM])
-> ModalSign -> Map SORT [AnModFORM]
forall a b. (a -> b) -> a -> b
$ Sign M_FORMULA ModalSign -> ModalSign
forall f e. Sign f e -> e
extendedInfo Sign M_FORMULA ModalSign
s
                         then [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> TERM M_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 M_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 M_FORMULA
t of
                       Mixfix_token tm :: SIMPLE_ID
tm ->
                           if SIMPLE_ID -> Map SIMPLE_ID [AnModFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
tm (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies (ModalSign -> Map SIMPLE_ID [AnModFORM])
-> ModalSign -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ Sign M_FORMULA ModalSign -> ModalSign
forall f e. Sign f e -> e
extendedInfo Sign M_FORMULA ModalSign
s)
                              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
Simple_mod 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
Simple_mod SIMPLE_ID
tm
                       Application (Op_name (Id [tm :: SIMPLE_ID
tm] [] _)) [] _ ->
                           if SIMPLE_ID -> Map SIMPLE_ID [AnModFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
tm (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies (ModalSign -> Map SIMPLE_ID [AnModFORM])
-> ModalSign -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ Sign M_FORMULA ModalSign -> ModalSign
forall f e. Sign f e -> e
extendedInfo Sign M_FORMULA ModalSign
s)
                           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
Simple_mod SIMPLE_ID
tm
                           else Result MODALITY
r
                       _ -> Result MODALITY
r
    in case M_FORMULA
form of
        BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA M_FORMULA
f ps :: Range
ps ->
            do MODALITY
nm <- MODALITY -> Range -> Result MODALITY
forall t. MODALITY -> t -> Result MODALITY
minMod MODALITY
m Range
ps
               FORMULA M_FORMULA
f2 <- Min M_FORMULA ModalSign
-> Sign M_FORMULA ModalSign
-> FORMULA M_FORMULA
-> Result (FORMULA M_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min M_FORMULA ModalSign
minExpForm Sign M_FORMULA ModalSign
s FORMULA M_FORMULA
f
               M_FORMULA -> Result M_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (M_FORMULA -> Result M_FORMULA) -> M_FORMULA -> Result M_FORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> MODALITY -> FORMULA M_FORMULA -> Range -> M_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA M_FORMULA
f2 Range
ps

ana_M_SIG_ITEM :: Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_SIG_ITEM :: Ana M_SIG_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_SIG_ITEM mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix mi :: M_SIG_ITEM
mi =
    case M_SIG_ITEM
mi of
    Rigid_op_items r :: RIGOR
r al :: [Annoted (OP_ITEM M_FORMULA)]
al ps :: Range
ps ->
        do [Annoted (OP_ITEM M_FORMULA)]
ul <- (Annoted (OP_ITEM M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) (Annoted (OP_ITEM M_FORMULA)))
-> [Annoted (OP_ITEM M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [Annoted (OP_ITEM M_FORMULA)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min M_FORMULA ModalSign
-> Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> Annoted (OP_ITEM M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (Annoted (OP_ITEM M_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 M_FORMULA ModalSign
minExpForm Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix) [Annoted (OP_ITEM M_FORMULA)]
al
           case RIGOR
r of
               Flexible -> (Annoted (OP_ITEM M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted (OP_ITEM M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ aoi :: Annoted (OP_ITEM M_FORMULA)
aoi -> case Annoted (OP_ITEM M_FORMULA) -> OP_ITEM M_FORMULA
forall a. Annoted a -> a
item Annoted (OP_ITEM M_FORMULA)
aoi of
                   Op_decl ops :: [SORT]
ops ty :: OP_TYPE
ty _ _ ->
                       (SORT -> State (Sign M_FORMULA ModalSign) ())
-> [SORT] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SORT -> ModalSign -> Result ModalSign)
-> SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> SORT -> ModalSign -> Result ModalSign
addFlexOp (OP_TYPE -> OpType
toOpType OP_TYPE
ty)) [SORT]
ops
                   Op_defn i :: SORT
i par :: OP_HEAD
par _ _ -> State (Sign M_FORMULA ModalSign) ()
-> (OP_TYPE -> State (Sign M_FORMULA ModalSign) ())
-> Maybe OP_TYPE
-> State (Sign M_FORMULA ModalSign) ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> State (Sign M_FORMULA ModalSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                       (\ ty :: OP_TYPE
ty -> (ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall a b. (a -> b) -> a -> b
$ OpType -> SORT -> ModalSign -> Result ModalSign
addFlexOp (OP_TYPE -> OpType
toOpType OP_TYPE
ty) SORT
i)
                       (Maybe OP_TYPE -> State (Sign M_FORMULA ModalSign) ())
-> Maybe OP_TYPE -> State (Sign M_FORMULA ModalSign) ()
forall a b. (a -> b) -> a -> b
$ OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
par) [Annoted (OP_ITEM M_FORMULA)]
ul
               Rigid -> () -> State (Sign M_FORMULA ModalSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM)
-> M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM
forall a b. (a -> b) -> a -> b
$ RIGOR -> [Annoted (OP_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM
Rigid_op_items RIGOR
r [Annoted (OP_ITEM M_FORMULA)]
ul Range
ps
    Rigid_pred_items r :: RIGOR
r al :: [Annoted (PRED_ITEM M_FORMULA)]
al ps :: Range
ps ->
        do [Annoted (PRED_ITEM M_FORMULA)]
ul <- (Annoted (PRED_ITEM M_FORMULA)
 -> State
      (Sign M_FORMULA ModalSign) (Annoted (PRED_ITEM M_FORMULA)))
-> [Annoted (PRED_ITEM M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [Annoted (PRED_ITEM M_FORMULA)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min M_FORMULA ModalSign
-> Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> Annoted (PRED_ITEM M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (Annoted (PRED_ITEM M_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 M_FORMULA ModalSign
minExpForm Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix) [Annoted (PRED_ITEM M_FORMULA)]
al
           case RIGOR
r of
               Flexible -> (Annoted (PRED_ITEM M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted (PRED_ITEM M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ aoi :: Annoted (PRED_ITEM M_FORMULA)
aoi -> case Annoted (PRED_ITEM M_FORMULA) -> PRED_ITEM M_FORMULA
forall a. Annoted a -> a
item Annoted (PRED_ITEM M_FORMULA)
aoi of
                   Pred_decl ops :: [SORT]
ops ty :: PRED_TYPE
ty _ ->
                       (SORT -> State (Sign M_FORMULA ModalSign) ())
-> [SORT] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SORT -> ModalSign -> Result ModalSign)
-> SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> SORT -> ModalSign -> Result ModalSign
addFlexPred (PRED_TYPE -> PredType
toPredType PRED_TYPE
ty)) [SORT]
ops
                   Pred_defn i :: SORT
i (Pred_head args :: [VAR_DECL]
args _) _ _ ->
                       (ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall a b. (a -> b) -> a -> b
$ PredType -> SORT -> ModalSign -> Result ModalSign
addFlexPred
                                ([SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
args) SORT
i ) [Annoted (PRED_ITEM M_FORMULA)]
ul
               Rigid -> () -> State (Sign M_FORMULA ModalSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM)
-> M_SIG_ITEM -> State (Sign M_FORMULA ModalSign) M_SIG_ITEM
forall a b. (a -> b) -> a -> b
$ RIGOR -> [Annoted (PRED_ITEM M_FORMULA)] -> Range -> M_SIG_ITEM
Rigid_pred_items RIGOR
r [Annoted (PRED_ITEM M_FORMULA)]
ul Range
ps

addFlexOp :: OpType -> Id -> ModalSign -> Result ModalSign
addFlexOp :: OpType -> SORT -> ModalSign -> Result ModalSign
addFlexOp ty :: OpType
ty i :: SORT
i m :: ModalSign
m = ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return
       ModalSign
m { flexOps :: OpMap
flexOps = SORT -> OpType -> OpMap -> OpMap
addOpTo SORT
i OpType
ty (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> OpMap
flexOps ModalSign
m }

addFlexPred :: PredType -> Id -> ModalSign -> Result ModalSign
addFlexPred :: PredType -> SORT -> ModalSign -> Result ModalSign
addFlexPred ty :: PredType
ty i :: SORT
i m :: ModalSign
m = ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return
       ModalSign
m { 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
ty (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> PredMap
flexPreds ModalSign
m }

ana_M_BASIC_ITEM
    :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_BASIC_ITEM :: Ana M_BASIC_ITEM M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
ana_M_BASIC_ITEM mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix bi :: M_BASIC_ITEM
bi = case M_BASIC_ITEM
bi of
        Simple_mod_decl al :: [Annoted SIMPLE_ID]
al fs :: [AnModFORM]
fs ps :: Range
ps -> do
            (Annoted SIMPLE_ID -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SIMPLE_ID -> ModalSign -> Result ModalSign)
-> SIMPLE_ID
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> ModalSign -> Result ModalSign
preAddModId) (SIMPLE_ID -> State (Sign M_FORMULA ModalSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
al
            [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs <- (FORMULA M_FORMULA
 -> State
      (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA))
-> [AnModFORM]
-> State
     (Sign M_FORMULA ModalSign)
     [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> FORMULA M_FORMULA
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
ana_FORMULA Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix) [AnModFORM]
fs
            [AnModFORM]
resFs <- ((FORMULA M_FORMULA, FORMULA M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [AnModFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA M_FORMULA
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> ((FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA)
-> (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA
forall a b. (a, b) -> a
fst) [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs
            [AnModFORM]
anaFs <- ((FORMULA M_FORMULA, FORMULA M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [AnModFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA M_FORMULA
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> ((FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA)
-> (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA
forall a b. (a, b) -> b
snd) [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs
            (Annoted SIMPLE_ID -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SIMPLE_ID -> ModalSign -> Result ModalSign)
-> SIMPLE_ID
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
addModId [AnModFORM]
anaFs) (SIMPLE_ID -> State (Sign M_FORMULA ModalSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
al
            M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM)
-> M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SIMPLE_ID] -> [AnModFORM] -> Range -> M_BASIC_ITEM
Simple_mod_decl [Annoted SIMPLE_ID]
al [AnModFORM]
resFs Range
ps
        Term_mod_decl al :: [Annoted SORT]
al fs :: [AnModFORM]
fs ps :: Range
ps -> do
            Sign M_FORMULA ModalSign
e <- State (Sign M_FORMULA ModalSign) (Sign M_FORMULA ModalSign)
forall s. State s s
get
            (Annoted SORT -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted SORT] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SORT -> ModalSign -> Result ModalSign)
-> SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign
preAddModSort Sign M_FORMULA ModalSign
e) (SORT -> State (Sign M_FORMULA ModalSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item) [Annoted SORT]
al
            [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs <- (FORMULA M_FORMULA
 -> State
      (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA))
-> [AnModFORM]
-> State
     (Sign M_FORMULA ModalSign)
     [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> FORMULA M_FORMULA
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
ana_FORMULA Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix) [AnModFORM]
fs
            [AnModFORM]
resFs <- ((FORMULA M_FORMULA, FORMULA M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [AnModFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA M_FORMULA
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> ((FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA)
-> (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA
forall a b. (a, b) -> a
fst) [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs
            [AnModFORM]
anaFs <- ((FORMULA M_FORMULA, FORMULA M_FORMULA)
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
-> State (Sign M_FORMULA ModalSign) [AnModFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA M_FORMULA
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
 -> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA))
-> ((FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA)
-> (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA M_FORMULA, FORMULA M_FORMULA) -> FORMULA M_FORMULA
forall a b. (a, b) -> b
snd) [Annoted (FORMULA M_FORMULA, FORMULA M_FORMULA)]
newFs
            (Annoted SORT -> State (Sign M_FORMULA ModalSign) ())
-> [Annoted SORT] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((ModalSign -> Result ModalSign)
-> State (Sign M_FORMULA ModalSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((ModalSign -> Result ModalSign)
 -> State (Sign M_FORMULA ModalSign) ())
-> (SORT -> ModalSign -> Result ModalSign)
-> SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnModFORM] -> SORT -> ModalSign -> Result ModalSign
addModSort [AnModFORM]
anaFs) (SORT -> State (Sign M_FORMULA ModalSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign M_FORMULA ModalSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item) [Annoted SORT]
al
            M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM)
-> M_BASIC_ITEM -> State (Sign M_FORMULA ModalSign) M_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SORT] -> [AnModFORM] -> Range -> M_BASIC_ITEM
Term_mod_decl [Annoted SORT]
al [AnModFORM]
resFs Range
ps

preAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
preAddModId :: SIMPLE_ID -> ModalSign -> Result ModalSign
preAddModId i :: SIMPLE_ID
i m :: ModalSign
m =
    let ms :: Map SIMPLE_ID [AnModFORM]
ms = ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
m in
    if SIMPLE_ID -> Map SIMPLE_ID [AnModFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
i Map SIMPLE_ID [AnModFORM]
ms then
       [Diagnosis] -> Maybe ModalSign -> Result ModalSign
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
Hint "repeated modality" SIMPLE_ID
i] (Maybe ModalSign -> Result ModalSign)
-> Maybe ModalSign -> Result ModalSign
forall a b. (a -> b) -> a -> b
$ ModalSign -> Maybe ModalSign
forall a. a -> Maybe a
Just ModalSign
m
       else ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return ModalSign
m { modies :: Map SIMPLE_ID [AnModFORM]
modies = SIMPLE_ID
-> [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SIMPLE_ID
i [] Map SIMPLE_ID [AnModFORM]
ms }

addModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
addModId :: [AnModFORM] -> SIMPLE_ID -> ModalSign -> Result ModalSign
addModId frms :: [AnModFORM]
frms i :: SIMPLE_ID
i m :: ModalSign
m = ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return ModalSign
m
  { modies :: Map SIMPLE_ID [AnModFORM]
modies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> SIMPLE_ID
-> [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union SIMPLE_ID
i [AnModFORM]
frms (Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM])
-> Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
m }

preAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign
              -> Result ModalSign
preAddModSort :: Sign M_FORMULA ModalSign -> SORT -> ModalSign -> Result ModalSign
preAddModSort e :: Sign M_FORMULA ModalSign
e i :: SORT
i m :: ModalSign
m =
    let ms :: Map SORT [AnModFORM]
ms = ModalSign -> Map SORT [AnModFORM]
termModies ModalSign
m
        ds :: [Diagnosis]
ds = Sign M_FORMULA ModalSign -> SORT -> [Diagnosis]
forall f e. Sign f e -> SORT -> [Diagnosis]
hasSort Sign M_FORMULA ModalSign
e SORT
i
    in if SORT -> Map SORT [AnModFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SORT
i Map SORT [AnModFORM]
ms Bool -> Bool -> Bool
|| Bool -> Bool
not ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds) then
       [Diagnosis] -> Maybe ModalSign -> Result ModalSign
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
i Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds) (Maybe ModalSign -> Result ModalSign)
-> Maybe ModalSign -> Result ModalSign
forall a b. (a -> b) -> a -> b
$ ModalSign -> Maybe ModalSign
forall a. a -> Maybe a
Just ModalSign
m
       else ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return ModalSign
m { termModies :: Map SORT [AnModFORM]
termModies = SORT -> [AnModFORM] -> Map SORT [AnModFORM] -> Map SORT [AnModFORM]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
i [] Map SORT [AnModFORM]
ms }

addModSort :: [AnModFORM] -> SORT -> ModalSign -> Result ModalSign
addModSort :: [AnModFORM] -> SORT -> ModalSign -> Result ModalSign
addModSort frms :: [AnModFORM]
frms i :: SORT
i m :: ModalSign
m = ModalSign -> Result ModalSign
forall (m :: * -> *) a. Monad m => a -> m a
return ModalSign
m
  { termModies :: Map SORT [AnModFORM]
termModies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> SORT
-> [AnModFORM]
-> Map SORT [AnModFORM]
-> Map SORT [AnModFORM]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union SORT
i [AnModFORM]
frms (Map SORT [AnModFORM] -> Map SORT [AnModFORM])
-> Map SORT [AnModFORM] -> Map SORT [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SORT [AnModFORM]
termModies ModalSign
m }

ana_FORMULA :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
            -> FORMULA M_FORMULA -> State (Sign M_FORMULA ModalSign)
               (FORMULA M_FORMULA, FORMULA M_FORMULA)
ana_FORMULA :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> FORMULA M_FORMULA
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
ana_FORMULA mix :: Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix f :: FORMULA M_FORMULA
f = do
           let ps :: [SORT]
ps = (SIMPLE_ID -> SORT) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> SORT
simpleIdToId ([SIMPLE_ID] -> [SORT]) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Set SIMPLE_ID -> [SIMPLE_ID]
forall a. Set a -> [a]
Set.toList (Set SIMPLE_ID -> [SIMPLE_ID]) -> Set SIMPLE_ID -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f
           PredMap
pm <- (Sign M_FORMULA ModalSign -> PredMap)
-> State (Sign M_FORMULA ModalSign) PredMap
forall s a. (s -> a) -> State s a
gets Sign M_FORMULA ModalSign -> PredMap
forall f e. Sign f e -> PredMap
predMap
           (SORT -> State (Sign M_FORMULA ModalSign) ())
-> [SORT] -> State (Sign M_FORMULA ModalSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annoted ()
-> PredType -> SORT -> State (Sign M_FORMULA ModalSign) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) (PredType -> SORT -> State (Sign M_FORMULA ModalSign) ())
-> PredType -> SORT -> State (Sign M_FORMULA ModalSign) ()
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType []) [SORT]
ps
           GlobalAnnos
newGa <- (Sign M_FORMULA ModalSign -> GlobalAnnos)
-> State (Sign M_FORMULA ModalSign) GlobalAnnos
forall s a. (s -> a) -> State s a
gets Sign M_FORMULA ModalSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos
           let Result es :: [Diagnosis]
es m :: Maybe (FORMULA M_FORMULA)
m = (M_FORMULA -> M_FORMULA)
-> MixResolve M_FORMULA -> MixResolve (FORMULA M_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula M_FORMULA -> M_FORMULA
mapM_FORMULA
                             MixResolve M_FORMULA
resolveM_FORMULA GlobalAnnos
newGa (Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
-> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix M_BASIC_ITEM M_SIG_ITEM M_FORMULA ModalSign
mix) FORMULA M_FORMULA
f
           [Diagnosis] -> State (Sign M_FORMULA ModalSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
es
           Sign M_FORMULA ModalSign
e <- State (Sign M_FORMULA ModalSign) (Sign M_FORMULA ModalSign)
forall s. State s s
get
           (FORMULA M_FORMULA, FORMULA M_FORMULA)
phi <- case Maybe (FORMULA M_FORMULA)
m of
               Nothing -> (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
f, FORMULA M_FORMULA
f)
               Just r :: FORMULA M_FORMULA
r -> do
                   FORMULA M_FORMULA
n <- (FORMULA M_FORMULA -> Result (FORMULA M_FORMULA))
-> FORMULA M_FORMULA
-> State (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA)
forall a f e. (a -> Result a) -> a -> State (Sign f e) a
resultToState (Min M_FORMULA ModalSign
-> Sign M_FORMULA ModalSign
-> FORMULA M_FORMULA
-> Result (FORMULA M_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min M_FORMULA ModalSign
minExpForm Sign M_FORMULA ModalSign
e) FORMULA M_FORMULA
r
                   (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA
r, FORMULA M_FORMULA
n)
           Sign M_FORMULA ModalSign
e2 <- State (Sign M_FORMULA ModalSign) (Sign M_FORMULA ModalSign)
forall s. State s s
get
           Sign M_FORMULA ModalSign -> State (Sign M_FORMULA ModalSign) ()
forall s. s -> State s ()
put Sign M_FORMULA ModalSign
e2 {predMap :: PredMap
predMap = PredMap
pm}
           (FORMULA M_FORMULA, FORMULA M_FORMULA)
-> State
     (Sign M_FORMULA ModalSign) (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA M_FORMULA, FORMULA M_FORMULA)
phi

getFormPredToks :: FORMULA M_FORMULA -> Set.Set Token
getFormPredToks :: FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks frm :: FORMULA M_FORMULA
frm = case FORMULA M_FORMULA
frm of
    Quantification _ _ f :: FORMULA M_FORMULA
f _ -> FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f
    Junction _ fs :: [FORMULA M_FORMULA]
fs _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (FORMULA M_FORMULA -> Set SIMPLE_ID)
-> [FORMULA M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks [FORMULA M_FORMULA]
fs
    Relation f1 :: FORMULA M_FORMULA
f1 _ f2 :: FORMULA M_FORMULA
f2 _ -> (Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID)
-> (FORMULA M_FORMULA -> Set SIMPLE_ID)
-> FORMULA M_FORMULA
-> FORMULA M_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 M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f1 FORMULA M_FORMULA
f2
    Negation f :: FORMULA M_FORMULA
f _ -> FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f
    Mixfix_formula (Mixfix_token t :: SIMPLE_ID
t) -> SIMPLE_ID -> Set SIMPLE_ID
forall a. a -> Set a
Set.singleton SIMPLE_ID
t
    Mixfix_formula t :: TERM M_FORMULA
t -> TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t
    ExtFORMULA (BoxOrDiamond _ _ f :: FORMULA M_FORMULA
f _) -> FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f
    Predication _ ts :: [TERM M_FORMULA]
ts _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    Definedness t :: TERM M_FORMULA
t _ -> TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t
    Equation t1 :: TERM M_FORMULA
t1 _ t2 :: TERM M_FORMULA
t2 _ -> (Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID)
-> (TERM M_FORMULA -> Set SIMPLE_ID)
-> TERM M_FORMULA
-> TERM M_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 TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t1 TERM M_FORMULA
t2
    Membership t :: TERM M_FORMULA
t _ _ -> TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t
    _ -> Set SIMPLE_ID
forall a. Set a
Set.empty

getTermPredToks :: TERM M_FORMULA -> Set.Set Token
getTermPredToks :: TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks trm :: TERM M_FORMULA
trm = case TERM M_FORMULA
trm of
    Application _ ts :: [TERM M_FORMULA]
ts _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    Sorted_term t :: TERM M_FORMULA
t _ _ -> TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t
    Cast t :: TERM M_FORMULA
t _ _ -> TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t
    Conditional t1 :: TERM M_FORMULA
t1 f :: FORMULA M_FORMULA
f t2 :: TERM M_FORMULA
t2 _ -> Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t1) (Set SIMPLE_ID -> Set SIMPLE_ID) -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$
        Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => Set a -> Set a -> Set a
Set.union (FORMULA M_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA M_FORMULA
f) (Set SIMPLE_ID -> Set SIMPLE_ID) -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM M_FORMULA
t2
    Mixfix_term ts :: [TERM M_FORMULA]
ts -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    Mixfix_parenthesized ts :: [TERM M_FORMULA]
ts _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    Mixfix_bracketed ts :: [TERM M_FORMULA]
ts _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    Mixfix_braced ts :: [TERM M_FORMULA]
ts _ -> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SIMPLE_ID] -> Set SIMPLE_ID)
-> [Set SIMPLE_ID] -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ (TERM M_FORMULA -> Set SIMPLE_ID)
-> [TERM M_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM M_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM M_FORMULA]
ts
    _ -> Set SIMPLE_ID
forall a. Set a
Set.empty