{- |
Module      :  ./Hybrid/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 hybrid logic parts
-}

module Hybrid.StatAna (basicHybridAnalysis, minExpForm) where

import Hybrid.AS_Hybrid
import Hybrid.Print_AS ()
import Hybrid.HybridSign

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

instance TermExtension H_FORMULA where
        freeVarsOfExt :: Sign H_FORMULA e -> H_FORMULA -> VarSet
freeVarsOfExt sign :: Sign H_FORMULA e
sign (BoxOrDiamond _ _ f :: FORMULA H_FORMULA
f _) = Sign H_FORMULA e -> FORMULA H_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign H_FORMULA e
sign FORMULA H_FORMULA
f
        freeVarsOfExt sign :: Sign H_FORMULA e
sign (At _ f :: FORMULA H_FORMULA
f _ ) = Sign H_FORMULA e -> FORMULA H_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign H_FORMULA e
sign FORMULA H_FORMULA
f
        freeVarsOfExt sign :: Sign H_FORMULA e
sign (Univ _ f :: FORMULA H_FORMULA
f _) = Sign H_FORMULA e -> FORMULA H_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign H_FORMULA e
sign FORMULA H_FORMULA
f
        freeVarsOfExt sign :: Sign H_FORMULA e
sign (Exist _ f :: FORMULA H_FORMULA
f _) = Sign H_FORMULA e -> FORMULA H_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign H_FORMULA e
sign FORMULA H_FORMULA
f
        freeVarsOfExt _ (Here _ _ ) = VarSet
forall a. Set a
Set.empty

basicHybridAnalysis
  :: (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
      Sign H_FORMULA HybridSign, GlobalAnnos)
  -> Result (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
             ExtSign (Sign H_FORMULA HybridSign) Symbol,
             [Named (FORMULA H_FORMULA)])
basicHybridAnalysis :: (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
 Sign H_FORMULA HybridSign, GlobalAnnos)
-> Result
     (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
      ExtSign (Sign H_FORMULA HybridSign) Symbol,
      [Named (FORMULA H_FORMULA)])
basicHybridAnalysis =
       Min H_FORMULA HybridSign
-> Ana H_BASIC_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> Ana H_SIG_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
    Sign H_FORMULA HybridSign, GlobalAnnos)
-> Result
     (BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA,
      ExtSign (Sign H_FORMULA HybridSign) Symbol,
      [Named (FORMULA H_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 H_FORMULA HybridSign
minExpForm Ana H_BASIC_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_H_BASIC_ITEM Ana H_SIG_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_H_SIG_ITEM Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_Mix

ana_Mix :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_Mix :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_Mix = Mix H_BASIC_ITEM Any Any HybridSign
forall b s f e. Mix b s f e
emptyMix
    { getSigIds :: H_SIG_ITEM -> IdSets
getSigIds = H_SIG_ITEM -> IdSets
ids_H_SIG_ITEM
    , putParen :: H_FORMULA -> H_FORMULA
putParen = H_FORMULA -> H_FORMULA
mapH_FORMULA
    , mixResolve :: MixResolve H_FORMULA
mixResolve = MixResolve H_FORMULA
resolveH_FORMULA
    }

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

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

mapH_FORMULA :: H_FORMULA -> H_FORMULA
mapH_FORMULA :: H_FORMULA -> H_FORMULA
mapH_FORMULA (BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA H_FORMULA
f ps :: Range
ps) =
    Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
b (MODALITY -> MODALITY
mapMODALITY MODALITY
m) ((H_FORMULA -> H_FORMULA) -> FORMULA H_FORMULA -> FORMULA H_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula H_FORMULA -> H_FORMULA
mapH_FORMULA FORMULA H_FORMULA
f) Range
ps
mapH_FORMULA (At n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
n ((H_FORMULA -> H_FORMULA) -> FORMULA H_FORMULA -> FORMULA H_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula H_FORMULA -> H_FORMULA
mapH_FORMULA FORMULA H_FORMULA
f) Range
ps
mapH_FORMULA (Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
n ((H_FORMULA -> H_FORMULA) -> FORMULA H_FORMULA -> FORMULA H_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula H_FORMULA -> H_FORMULA
mapH_FORMULA FORMULA H_FORMULA
f) Range
ps
mapH_FORMULA (Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
n ((H_FORMULA -> H_FORMULA) -> FORMULA H_FORMULA -> FORMULA H_FORMULA
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula H_FORMULA -> H_FORMULA
mapH_FORMULA FORMULA H_FORMULA
f) Range
ps
mapH_FORMULA (Here n :: NOMINAL
n ps :: Range
ps) = NOMINAL -> Range -> H_FORMULA
Here NOMINAL
n 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 H_FORMULA
t -> (TERM H_FORMULA -> MODALITY)
-> Result (TERM H_FORMULA) -> Result MODALITY
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM H_FORMULA -> MODALITY
Term_mod (Result (TERM H_FORMULA) -> Result MODALITY)
-> Result (TERM H_FORMULA) -> Result MODALITY
forall a b. (a -> b) -> a -> b
$ (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (TERM H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm H_FORMULA -> H_FORMULA
mapH_FORMULA
                  MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids TERM H_FORMULA
t
    _ -> MODALITY -> Result MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return MODALITY
m

resolveH_FORMULA :: MixResolve H_FORMULA
resolveH_FORMULA :: MixResolve H_FORMULA
resolveH_FORMULA ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids cf :: H_FORMULA
cf = case H_FORMULA
cf of
   BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA H_FORMULA
f ps :: Range
ps -> do
       MODALITY
nm <- MixResolve MODALITY
resolveMODALITY GlobalAnnos
ga (TokRules, Rules)
ids MODALITY
m
       FORMULA H_FORMULA
nf <- (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (FORMULA H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm H_FORMULA -> H_FORMULA
mapH_FORMULA MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA H_FORMULA
f
       H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA H_FORMULA
nf Range
ps)
   At n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps -> do
       FORMULA H_FORMULA
nf <- (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (FORMULA H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm H_FORMULA -> H_FORMULA
mapH_FORMULA MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA H_FORMULA
f
       H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
n FORMULA H_FORMULA
nf Range
ps)
   Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps -> do
       FORMULA H_FORMULA
nf <- (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (FORMULA H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm H_FORMULA -> H_FORMULA
mapH_FORMULA MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA H_FORMULA
f
       H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
n FORMULA H_FORMULA
nf Range
ps)
   Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps -> do
       FORMULA H_FORMULA
nf <- (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (FORMULA H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm H_FORMULA -> H_FORMULA
mapH_FORMULA MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA H_FORMULA
f
       H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
n FORMULA H_FORMULA
nf Range
ps)
   Here n :: NOMINAL
n ps :: Range
ps -> H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> Range -> H_FORMULA
Here NOMINAL
n Range
ps)

minExpForm :: Min H_FORMULA HybridSign
minExpForm :: Min H_FORMULA HybridSign
minExpForm s :: Sign H_FORMULA HybridSign
s form :: H_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 H_FORMULA -> MODALITY
Term_mod (SIMPLE_ID -> TERM H_FORMULA
forall f. SIMPLE_ID -> TERM f
Mixfix_token SIMPLE_ID
i)) t
ps
                  Term_mod t :: TERM H_FORMULA
t -> let
                    r :: Result MODALITY
r = do
                      TERM H_FORMULA
t2 <- Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> TERM H_FORMULA
-> Result (TERM H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min H_FORMULA HybridSign
minExpForm Sign H_FORMULA HybridSign
s TERM H_FORMULA
t
                      let srt :: SORT
srt = TERM H_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM H_FORMULA
t2
                          trm :: MODALITY
trm = TERM H_FORMULA -> MODALITY
Term_mod TERM H_FORMULA
t2
                          supers :: Set SORT
supers = SORT -> Sign H_FORMULA HybridSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
srt Sign H_FORMULA HybridSign
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 [AnHybFORM] -> Set SORT
forall k a. Map k a -> Set k
Map.keysSet (Map SORT [AnHybFORM] -> Set SORT)
-> Map SORT [AnHybFORM] -> Set SORT
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SORT [AnHybFORM]
termModies (HybridSign -> Map SORT [AnHybFORM])
-> HybridSign -> Map SORT [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
s
                         then [Diagnosis] -> Maybe MODALITY -> Result MODALITY
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> TERM H_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 H_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 H_FORMULA
t of
                       Mixfix_token tm :: SIMPLE_ID
tm ->
                           if SIMPLE_ID -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
tm (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
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 [AnHybFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
tm (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
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
        minNom :: NOMINAL -> Result NOMINAL
minNom (Simple_nom n :: SIMPLE_ID
n) = if SIMPLE_ID -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
n (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
s)
                                then NOMINAL -> Result NOMINAL
forall (m :: * -> *) a. Monad m => a -> m a
return (SIMPLE_ID -> NOMINAL
Simple_nom SIMPLE_ID
n)
                                else [Diagnosis] -> Maybe NOMINAL -> Result NOMINAL
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
n]
                                            (Maybe NOMINAL -> Result NOMINAL)
-> Maybe NOMINAL -> Result NOMINAL
forall a b. (a -> b) -> a -> b
$ NOMINAL -> Maybe NOMINAL
forall a. a -> Maybe a
Just (SIMPLE_ID -> NOMINAL
Simple_nom SIMPLE_ID
n)
        colNom :: NOMINAL -> Result NOMINAL
colNom (Simple_nom n :: SIMPLE_ID
n)
         | SIMPLE_ID -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
n (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies (HybridSign -> Map SIMPLE_ID [AnHybFORM])
-> HybridSign -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
s) = [Diagnosis] -> Maybe NOMINAL -> Result NOMINAL
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 "collision on nominals" SIMPLE_ID
n] (Maybe NOMINAL -> Result NOMINAL)
-> Maybe NOMINAL -> Result NOMINAL
forall a b. (a -> b) -> a -> b
$ NOMINAL -> Maybe NOMINAL
forall a. a -> Maybe a
Just (SIMPLE_ID -> NOMINAL
Simple_nom SIMPLE_ID
n)
         | SIMPLE_ID -> Bool
wPrefix SIMPLE_ID
n = [Diagnosis] -> Maybe NOMINAL -> Result NOMINAL
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 "\"world\" prefixes are reserved" SIMPLE_ID
n] Maybe NOMINAL
forall a. Maybe a
Nothing
         | Bool
otherwise = NOMINAL -> Result NOMINAL
forall (m :: * -> *) a. Monad m => a -> m a
return (SIMPLE_ID -> NOMINAL
Simple_nom SIMPLE_ID
n)
        addUniv :: NOMINAL -> HybridSign -> Result HybridSign
addUniv (Simple_nom n :: SIMPLE_ID
n) = [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addNomId [] SIMPLE_ID
n
        addExist :: NOMINAL -> HybridSign -> Result HybridSign
addExist (Simple_nom n :: SIMPLE_ID
n ) = [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addNomId [] SIMPLE_ID
n
    in case H_FORMULA
form of
        BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA H_FORMULA
f ps :: Range
ps ->
            do MODALITY
nm <- MODALITY -> Range -> Result MODALITY
forall t. MODALITY -> t -> Result MODALITY
minMod MODALITY
m Range
ps
               FORMULA H_FORMULA
nf <- Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min H_FORMULA HybridSign
minExpForm Sign H_FORMULA HybridSign
s FORMULA H_FORMULA
f
               H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
b MODALITY
nm FORMULA H_FORMULA
nf Range
ps)
        At n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps ->
            do NOMINAL
nn <- NOMINAL -> Result NOMINAL
minNom NOMINAL
n
               FORMULA H_FORMULA
nf <- Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min H_FORMULA HybridSign
minExpForm Sign H_FORMULA HybridSign
s FORMULA H_FORMULA
f
               H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
nn FORMULA H_FORMULA
nf Range
ps)
        Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps ->
            do NOMINAL
nn <- NOMINAL -> Result NOMINAL
colNom NOMINAL
n
               {- add the binder in the sign (for this formula only)
               so it can be used a normal nominal -}
               HybridSign
bs <- NOMINAL -> HybridSign -> Result HybridSign
addUniv NOMINAL
nn (Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
s)
               FORMULA H_FORMULA
nf <- Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min H_FORMULA HybridSign
minExpForm (Sign H_FORMULA HybridSign
s {extendedInfo :: HybridSign
extendedInfo = HybridSign
bs}) FORMULA H_FORMULA
f
               H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
nn FORMULA H_FORMULA
nf Range
ps)
        Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps ->
            do NOMINAL
nn <- NOMINAL -> Result NOMINAL
colNom NOMINAL
n
               {- add the binder in the sign (for this formula only)
               so it can be used a normal nominal -}
               HybridSign
bs <- NOMINAL -> HybridSign -> Result HybridSign
addExist NOMINAL
nn (Sign H_FORMULA HybridSign -> HybridSign
forall f e. Sign f e -> e
extendedInfo Sign H_FORMULA HybridSign
s)
               FORMULA H_FORMULA
nf <- Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min H_FORMULA HybridSign
minExpForm (Sign H_FORMULA HybridSign
s {extendedInfo :: HybridSign
extendedInfo = HybridSign
bs}) FORMULA H_FORMULA
f
               H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
nn FORMULA H_FORMULA
nf Range
ps)

        Here n :: NOMINAL
n ps :: Range
ps ->
            do NOMINAL
nn <- NOMINAL -> Result NOMINAL
minNom NOMINAL
n
               H_FORMULA -> Result H_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (NOMINAL -> Range -> H_FORMULA
Here NOMINAL
nn Range
ps)

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

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

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

ana_H_BASIC_ITEM
    :: Ana H_BASIC_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_H_BASIC_ITEM :: Ana H_BASIC_ITEM H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
ana_H_BASIC_ITEM mix :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
mix bi :: H_BASIC_ITEM
bi =
 let anaHlp :: [AnHybFORM]
-> State (Sign H_FORMULA HybridSign) ([AnHybFORM], [AnHybFORM])
anaHlp fs :: [AnHybFORM]
fs = do
      [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
newFs <- (FORMULA H_FORMULA
 -> State
      (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA))
-> [AnHybFORM]
-> State
     (Sign H_FORMULA HybridSign)
     [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> State
     (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA)
ana_FORMULA Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
mix) [AnHybFORM]
fs
      [AnHybFORM]
resFs <- ((FORMULA H_FORMULA, FORMULA H_FORMULA)
 -> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA))
-> [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
-> State (Sign H_FORMULA HybridSign) [AnHybFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA H_FORMULA
-> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA
 -> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA))
-> ((FORMULA H_FORMULA, FORMULA H_FORMULA) -> FORMULA H_FORMULA)
-> (FORMULA H_FORMULA, FORMULA H_FORMULA)
-> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA H_FORMULA, FORMULA H_FORMULA) -> FORMULA H_FORMULA
forall a b. (a, b) -> a
fst) [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
newFs
      [AnHybFORM]
anaFs <- ((FORMULA H_FORMULA, FORMULA H_FORMULA)
 -> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA))
-> [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
-> State (Sign H_FORMULA HybridSign) [AnHybFORM]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (FORMULA H_FORMULA
-> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA
 -> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA))
-> ((FORMULA H_FORMULA, FORMULA H_FORMULA) -> FORMULA H_FORMULA)
-> (FORMULA H_FORMULA, FORMULA H_FORMULA)
-> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA H_FORMULA, FORMULA H_FORMULA) -> FORMULA H_FORMULA
forall a b. (a, b) -> b
snd) [Annoted (FORMULA H_FORMULA, FORMULA H_FORMULA)]
newFs
      ([AnHybFORM], [AnHybFORM])
-> State (Sign H_FORMULA HybridSign) ([AnHybFORM], [AnHybFORM])
forall (m :: * -> *) a. Monad m => a -> m a
return ([AnHybFORM]
resFs, [AnHybFORM]
anaFs)
 in case H_BASIC_ITEM
bi of
        Simple_mod_decl al :: [Annoted SIMPLE_ID]
al fs :: [AnHybFORM]
fs ps :: Range
ps -> do
            (Annoted SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SIMPLE_ID -> HybridSign -> Result HybridSign)
-> SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> HybridSign -> Result HybridSign
preAddModId) (SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
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
            (resFs :: [AnHybFORM]
resFs, anaFs :: [AnHybFORM]
anaFs) <- [AnHybFORM]
-> State (Sign H_FORMULA HybridSign) ([AnHybFORM], [AnHybFORM])
anaHlp [AnHybFORM]
fs
            (Annoted SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SIMPLE_ID -> HybridSign -> Result HybridSign)
-> SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addModId [AnHybFORM]
anaFs) (SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
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
            H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM)
-> H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SIMPLE_ID] -> [AnHybFORM] -> Range -> H_BASIC_ITEM
Simple_mod_decl [Annoted SIMPLE_ID]
al [AnHybFORM]
resFs Range
ps
        Term_mod_decl al :: [Annoted SORT]
al fs :: [AnHybFORM]
fs ps :: Range
ps -> do
            Sign H_FORMULA HybridSign
e <- State (Sign H_FORMULA HybridSign) (Sign H_FORMULA HybridSign)
forall s. State s s
get
            (Annoted SORT -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SORT] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SORT -> HybridSign -> Result HybridSign)
-> SORT
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign H_FORMULA HybridSign
-> SORT -> HybridSign -> Result HybridSign
preAddModSort Sign H_FORMULA HybridSign
e) (SORT -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item) [Annoted SORT]
al
            (resFs :: [AnHybFORM]
resFs, anaFs :: [AnHybFORM]
anaFs) <- [AnHybFORM]
-> State (Sign H_FORMULA HybridSign) ([AnHybFORM], [AnHybFORM])
anaHlp [AnHybFORM]
fs
            (Annoted SORT -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SORT] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SORT -> HybridSign -> Result HybridSign)
-> SORT
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnHybFORM] -> SORT -> HybridSign -> Result HybridSign
addModSort [AnHybFORM]
anaFs) (SORT -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SORT -> SORT)
-> Annoted SORT
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SORT -> SORT
forall a. Annoted a -> a
item) [Annoted SORT]
al
            H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM)
-> H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SORT] -> [AnHybFORM] -> Range -> H_BASIC_ITEM
Term_mod_decl [Annoted SORT]
al [AnHybFORM]
resFs Range
ps
        Simple_nom_decl ids :: [Annoted SIMPLE_ID]
ids fs :: [AnHybFORM]
fs ps :: Range
ps -> do
           (Annoted SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SIMPLE_ID -> HybridSign -> Result HybridSign)
-> SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> HybridSign -> Result HybridSign
preAddNomId) (SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
ids
           (resFs :: [AnHybFORM]
resFs, anaFs :: [AnHybFORM]
anaFs) <- [AnHybFORM]
-> State (Sign H_FORMULA HybridSign) ([AnHybFORM], [AnHybFORM])
anaHlp [AnHybFORM]
fs
           (Annoted SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> [Annoted SIMPLE_ID] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((HybridSign -> Result HybridSign)
-> State (Sign H_FORMULA HybridSign) ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((HybridSign -> Result HybridSign)
 -> State (Sign H_FORMULA HybridSign) ())
-> (SIMPLE_ID -> HybridSign -> Result HybridSign)
-> SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addNomId [AnHybFORM]
anaFs) (SIMPLE_ID -> State (Sign H_FORMULA HybridSign) ())
-> (Annoted SIMPLE_ID -> SIMPLE_ID)
-> Annoted SIMPLE_ID
-> State (Sign H_FORMULA HybridSign) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SIMPLE_ID -> SIMPLE_ID
forall a. Annoted a -> a
item) [Annoted SIMPLE_ID]
ids
           H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM)
-> H_BASIC_ITEM -> State (Sign H_FORMULA HybridSign) H_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Annoted SIMPLE_ID] -> [AnHybFORM] -> Range -> H_BASIC_ITEM
Simple_nom_decl [Annoted SIMPLE_ID]
ids [AnHybFORM]
resFs Range
ps

preAddNomId :: SIMPLE_ID -> HybridSign -> Result HybridSign
preAddNomId :: SIMPLE_ID -> HybridSign -> Result HybridSign
preAddNomId i :: SIMPLE_ID
i hs :: HybridSign
hs =
    let ns :: Map SIMPLE_ID [AnHybFORM]
ns = HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
hs in
    if SIMPLE_ID -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member SIMPLE_ID
i Map SIMPLE_ID [AnHybFORM]
ns then
        [Diagnosis] -> Maybe HybridSign -> Result HybridSign
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 nominal" SIMPLE_ID
i] (Maybe HybridSign -> Result HybridSign)
-> Maybe HybridSign -> Result HybridSign
forall a b. (a -> b) -> a -> b
$ HybridSign -> Maybe HybridSign
forall a. a -> Maybe a
Just HybridSign
hs
        else if SIMPLE_ID -> Bool
wPrefix SIMPLE_ID
i
                then [Diagnosis] -> Maybe HybridSign -> Result HybridSign
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 "\"world\" prefixes are reserved" SIMPLE_ID
i]
                      Maybe HybridSign
forall a. Maybe a
Nothing
                else HybridSign -> Result HybridSign
forall (m :: * -> *) a. Monad m => a -> m a
return HybridSign
hs { nomies :: Map SIMPLE_ID [AnHybFORM]
nomies = SIMPLE_ID
-> [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SIMPLE_ID
i [] Map SIMPLE_ID [AnHybFORM]
ns }

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

addNomId :: [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addNomId :: [AnHybFORM] -> SIMPLE_ID -> HybridSign -> Result HybridSign
addNomId frms :: [AnHybFORM]
frms i :: SIMPLE_ID
i s :: HybridSign
s =
        HybridSign -> Result HybridSign
forall (m :: * -> *) a. Monad m => a -> m a
return HybridSign
s { nomies :: Map SIMPLE_ID [AnHybFORM]
nomies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> SIMPLE_ID
-> [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union SIMPLE_ID
i [AnHybFORM]
frms (Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
s}

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

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

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

ana_FORMULA :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
            -> FORMULA H_FORMULA -> State (Sign H_FORMULA HybridSign)
               (FORMULA H_FORMULA, FORMULA H_FORMULA)
ana_FORMULA :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> State
     (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA)
ana_FORMULA mix :: Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
mix f :: FORMULA H_FORMULA
f = do
           let ps :: [SORT]
ps = (SIMPLE_ID -> SORT) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map ([SIMPLE_ID] -> SORT
mkId ([SIMPLE_ID] -> SORT)
-> (SIMPLE_ID -> [SIMPLE_ID]) -> SIMPLE_ID -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SIMPLE_ID -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. a -> [a] -> [a]
: [])) ([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 H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
           PredMap
pm <- (Sign H_FORMULA HybridSign -> PredMap)
-> State (Sign H_FORMULA HybridSign) PredMap
forall s a. (s -> a) -> State s a
gets Sign H_FORMULA HybridSign -> PredMap
forall f e. Sign f e -> PredMap
predMap
           (SORT -> State (Sign H_FORMULA HybridSign) ())
-> [SORT] -> State (Sign H_FORMULA HybridSign) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annoted ()
-> PredType -> SORT -> State (Sign H_FORMULA HybridSign) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) (PredType -> SORT -> State (Sign H_FORMULA HybridSign) ())
-> PredType -> SORT -> State (Sign H_FORMULA HybridSign) ()
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType []) [SORT]
ps
           GlobalAnnos
newGa <- (Sign H_FORMULA HybridSign -> GlobalAnnos)
-> State (Sign H_FORMULA HybridSign) GlobalAnnos
forall s a. (s -> a) -> State s a
gets Sign H_FORMULA HybridSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos
           let Result es :: [Diagnosis]
es m :: Maybe (FORMULA H_FORMULA)
m = (H_FORMULA -> H_FORMULA)
-> MixResolve H_FORMULA -> MixResolve (FORMULA H_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula H_FORMULA -> H_FORMULA
mapH_FORMULA
                             MixResolve H_FORMULA
resolveH_FORMULA GlobalAnnos
newGa (Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
-> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix H_BASIC_ITEM H_SIG_ITEM H_FORMULA HybridSign
mix) FORMULA H_FORMULA
f
           [Diagnosis] -> State (Sign H_FORMULA HybridSign) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
es
           Sign H_FORMULA HybridSign
e <- State (Sign H_FORMULA HybridSign) (Sign H_FORMULA HybridSign)
forall s. State s s
get
           (FORMULA H_FORMULA, FORMULA H_FORMULA)
phi <- case Maybe (FORMULA H_FORMULA)
m of
               Nothing -> (FORMULA H_FORMULA, FORMULA H_FORMULA)
-> State
     (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA
f, FORMULA H_FORMULA
f)
               Just r :: FORMULA H_FORMULA
r -> do
                   FORMULA H_FORMULA
n <- (FORMULA H_FORMULA -> Result (FORMULA H_FORMULA))
-> FORMULA H_FORMULA
-> State (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA)
forall a f e. (a -> Result a) -> a -> State (Sign f e) a
resultToState (Min H_FORMULA HybridSign
-> Sign H_FORMULA HybridSign
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min H_FORMULA HybridSign
minExpForm Sign H_FORMULA HybridSign
e) FORMULA H_FORMULA
r
                   (FORMULA H_FORMULA, FORMULA H_FORMULA)
-> State
     (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA
r, FORMULA H_FORMULA
n)
           Sign H_FORMULA HybridSign
e2 <- State (Sign H_FORMULA HybridSign) (Sign H_FORMULA HybridSign)
forall s. State s s
get
           Sign H_FORMULA HybridSign -> State (Sign H_FORMULA HybridSign) ()
forall s. s -> State s ()
put Sign H_FORMULA HybridSign
e2 {predMap :: PredMap
predMap = PredMap
pm}
           (FORMULA H_FORMULA, FORMULA H_FORMULA)
-> State
     (Sign H_FORMULA HybridSign) (FORMULA H_FORMULA, FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA, FORMULA H_FORMULA)
phi

getFormPredToks :: FORMULA H_FORMULA -> Set.Set Token
getFormPredToks :: FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks frm :: FORMULA H_FORMULA
frm = case FORMULA H_FORMULA
frm of
    Quantification _ _ f :: FORMULA H_FORMULA
f _ -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
    Junction _ fs :: [FORMULA H_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 H_FORMULA -> Set SIMPLE_ID)
-> [FORMULA H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks [FORMULA H_FORMULA]
fs
    Relation f1 :: FORMULA H_FORMULA
f1 _ f2 :: FORMULA H_FORMULA
f2 _ ->
        Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => Set a -> Set a -> Set a
Set.union (FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f1) (Set SIMPLE_ID -> Set SIMPLE_ID) -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f2
    Negation f :: FORMULA H_FORMULA
f _ -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_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 H_FORMULA
t -> TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t
    ExtFORMULA (BoxOrDiamond _ _ f :: FORMULA H_FORMULA
f _) -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
    ExtFORMULA (At _ f :: FORMULA H_FORMULA
f _ ) -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
    ExtFORMULA (Univ _ f :: FORMULA H_FORMULA
f _ ) -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
    ExtFORMULA (Exist _ f :: FORMULA H_FORMULA
f _ ) -> FORMULA H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f
    Predication _ ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    Definedness t :: TERM H_FORMULA
t _ -> TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t
    Membership t :: TERM H_FORMULA
t _ _ -> TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t
    _ -> Set SIMPLE_ID
forall a. Set a
Set.empty

getTermPredToks :: TERM H_FORMULA -> Set.Set Token
getTermPredToks :: TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks trm :: TERM H_FORMULA
trm = case TERM H_FORMULA
trm of
    Application _ ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    Sorted_term t :: TERM H_FORMULA
t _ _ -> TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t
    Cast t :: TERM H_FORMULA
t _ _ -> TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t
    Conditional t1 :: TERM H_FORMULA
t1 f :: FORMULA H_FORMULA
f t2 :: TERM H_FORMULA
t2 _ -> Set SIMPLE_ID -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_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 H_FORMULA -> Set SIMPLE_ID
getFormPredToks FORMULA H_FORMULA
f) (Set SIMPLE_ID -> Set SIMPLE_ID) -> Set SIMPLE_ID -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks TERM H_FORMULA
t2
    Mixfix_term ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    Mixfix_parenthesized ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    Mixfix_bracketed ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    Mixfix_braced ts :: [TERM H_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 H_FORMULA -> Set SIMPLE_ID)
-> [TERM H_FORMULA] -> [Set SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map TERM H_FORMULA -> Set SIMPLE_ID
getTermPredToks [TERM H_FORMULA]
ts
    _ -> Set SIMPLE_ID
forall a. Set a
Set.empty


wPrefix :: Token -> Bool
wPrefix :: SIMPLE_ID -> Bool
wPrefix = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "world" (String -> Bool) -> (SIMPLE_ID -> String) -> SIMPLE_ID -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIMPLE_ID -> String
tokStr