{-# LANGUAGE ExistentialQuantification, OverloadedStrings #-}
{- |
Module      :  ./TopHybrid/StatAna.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  nevrenato@gmail.com
Stability   :  experimental
Portability :  not portable

Description :
Static analysis of hybrid logic with an arbitrary logic below.
-}

module TopHybrid.StatAna (thAna, anaForm', simSen) where

import Logic.Logic
import TopHybrid.AS_TopHybrid
import TopHybrid.TopHybridSign
import TopHybrid.Print_AS ()
import TopHybrid.Utilities
import TopHybrid.ATC_TopHybrid ()
import CASL.Sign -- Symbols, this should be removed...
import Common.GlobalAnnotations
import Common.Result
import Common.ExtSign
import Common.AS_Annotation
import Common.Id
import Common.DocUtils
import Control.Monad
import Data.List
import Data.Set
import Unsafe.Coerce
import ATerm.Lib
import Data.Aeson(FromJSON, ToJSON, parseJSON, toJSON, object, (.=), Value(Null))

bimap :: (t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap :: (t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap f :: t1 -> t2
f g :: s1 -> s2
g (a :: t1
a, b :: s1
b) = (t1 -> t2
f t1
a, s1 -> s2
g s1
b)

-- | Collects the newly declared nomies and modies
colnomsMods :: [TH_BASIC_ITEM] -> ([MODALITY], [NOMINAL])
colnomsMods :: [TH_BASIC_ITEM] -> ([MODALITY], [MODALITY])
colnomsMods = (TH_BASIC_ITEM
 -> ([MODALITY], [MODALITY]) -> ([MODALITY], [MODALITY]))
-> ([MODALITY], [MODALITY])
-> [TH_BASIC_ITEM]
-> ([MODALITY], [MODALITY])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Data.List.foldr TH_BASIC_ITEM
-> ([MODALITY], [MODALITY]) -> ([MODALITY], [MODALITY])
f ([], [])
        where f :: TH_BASIC_ITEM
-> ([MODALITY], [MODALITY]) -> ([MODALITY], [MODALITY])
f (Simple_mod_decl ms :: [MODALITY]
ms) = ([MODALITY] -> [MODALITY])
-> ([MODALITY] -> [MODALITY])
-> ([MODALITY], [MODALITY])
-> ([MODALITY], [MODALITY])
forall t1 t2 s1 s2.
(t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap ([MODALITY] -> [MODALITY] -> [MODALITY]
forall a. [a] -> [a] -> [a]
++ [MODALITY]
ms) [MODALITY] -> [MODALITY]
forall a. a -> a
id
              f (Simple_nom_decl ns :: [MODALITY]
ns) = ([MODALITY] -> [MODALITY])
-> ([MODALITY] -> [MODALITY])
-> ([MODALITY], [MODALITY])
-> ([MODALITY], [MODALITY])
forall t1 t2 s1 s2.
(t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap [MODALITY] -> [MODALITY]
forall a. a -> a
id ([MODALITY] -> [MODALITY] -> [MODALITY]
forall a. [a] -> [a] -> [a]
++ [MODALITY]
ns)

{- | Adds the newly declared nomies/modies, and the analysed base
signature to a new sig
checking for redundancy of modalities and nominals declarations
Note : If there are repeated declarations, the size of the sets should
be differnt that the size of the lists -}
topAna :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
                [TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
topAna :: [TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
topAna ds :: [TH_BASIC_ITEM]
ds l :: l
l sig :: sign
sig = if Bool -> Bool
not Bool
rep then Sgn_Wrap -> Result Sgn_Wrap
forall (m :: * -> *) a. Monad m => a -> m a
return Sgn_Wrap
newSig else Sgn_Wrap -> String -> Result Sgn_Wrap
forall a. a -> String -> Result a
mkHint Sgn_Wrap
newSig String
forall a. a
msg
                where
                x :: ([MODALITY], [MODALITY])
x = [TH_BASIC_ITEM] -> ([MODALITY], [MODALITY])
colnomsMods [TH_BASIC_ITEM]
ds
                x' :: (Set MODALITY, Set MODALITY)
x' = ([MODALITY] -> Set MODALITY)
-> ([MODALITY] -> Set MODALITY)
-> ([MODALITY], [MODALITY])
-> (Set MODALITY, Set MODALITY)
forall t1 t2 s1 s2.
(t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
bimap [MODALITY] -> Set MODALITY
forall a. Ord a => [a] -> Set a
fromList [MODALITY] -> Set MODALITY
forall a. Ord a => [a] -> Set a
fromList ([MODALITY], [MODALITY])
x
                rep :: Bool
rep = Set MODALITY -> Int
forall a. Set a -> Int
size ((Set MODALITY -> Set MODALITY -> Set MODALITY)
-> (Set MODALITY, Set MODALITY) -> Set MODALITY
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set MODALITY -> Set MODALITY -> Set MODALITY
forall a. Ord a => Set a -> Set a -> Set a
Data.Set.union (Set MODALITY, Set MODALITY)
x') Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=
                      [MODALITY] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([MODALITY] -> [MODALITY] -> [MODALITY])
-> ([MODALITY], [MODALITY]) -> [MODALITY]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [MODALITY] -> [MODALITY] -> [MODALITY]
forall a. [a] -> [a] -> [a]
(++) ([MODALITY], [MODALITY])
x)
                s :: THybridSign sign
s = (Set MODALITY -> Set MODALITY -> sign -> THybridSign sign)
-> (Set MODALITY, Set MODALITY) -> sign -> THybridSign sign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set MODALITY -> Set MODALITY -> sign -> THybridSign sign
forall s. Set MODALITY -> Set MODALITY -> s -> THybridSign s
THybridSign (Set MODALITY, Set MODALITY)
x' sign
sig
                newSig :: Sgn_Wrap
newSig = l -> THybridSign sign -> Sgn_Wrap
forall l sub bs f s sm sign mo sy rw pf.
Logic l sub bs f s sm sign mo sy rw pf =>
l -> THybridSign sign -> Sgn_Wrap
Sgn_Wrap l
l THybridSign sign
s
                msg :: a
msg = Int -> Maybe a -> a
forall a. Int -> Maybe a -> a
maybeE 0 Maybe a
forall a. Maybe a
Nothing

{- Checks if the modalities and nominals referred in a sentence, really exist
in the signature -}
nomOrModCheck :: (Pretty f, GetRange f) => Set SIMPLE_ID -> SIMPLE_ID ->
                                           TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck :: Set MODALITY -> MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck xs :: Set MODALITY
xs x :: MODALITY
x = if MODALITY -> Set MODALITY -> Bool
forall a. Ord a => a -> Set a -> Bool
member MODALITY
x Set MODALITY
xs then TH_FORMULA f -> Result (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return else String -> TH_FORMULA f -> Result (TH_FORMULA f)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError String
forall a. a
msg
     where msg :: a
msg = Int -> Maybe a -> a
forall a. Int -> Maybe a -> a
maybeE 1 Maybe a
forall a. Maybe a
Nothing


{- | Top Formula analyser
The l argument could be discarded, but then we would need an extra unsafe
function, to convert the spec type...
As l corresponds to the underlying logic bs should correspond to the
underlying spec, as some formula analysers need the spec associated
with it -}
anaForm :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
        l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
anaForm :: l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
anaForm l :: l
l bs :: bs
bs s :: Sgn_Wrap
s (Frm_Wrap _ f :: TH_FORMULA f
f) = (TH_FORMULA sen -> Frm_Wrap)
-> Result (TH_FORMULA sen) -> Result Frm_Wrap
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (l -> TH_FORMULA sen -> Frm_Wrap
forall l sub bs f s sm si mo sy rw pf.
Logic l sub bs f s sm si mo sy rw pf =>
l -> TH_FORMULA f -> Frm_Wrap
Frm_Wrap l
l) (Result (TH_FORMULA sen) -> Result Frm_Wrap)
-> Result (TH_FORMULA sen) -> Result Frm_Wrap
forall a b. (a -> b) -> a -> b
$ l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s TH_FORMULA f
f

{- Static analysis of an hybridized sentence, when it's called by an upper
level logic. (This is only used when we want to analyse 2 or more times
hybridized, sentences). Probably this function can be merged smoothly with
the above. I will check this later

An hybridized sentence, with the correpondent sign already built, doesn't
need the top spec, hence we can discard it and just use the underlying (und) -}
anaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
anaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
anaForm' (Spc_Wrap l :: l
l bs :: TH_BSPEC bs
bs _, s :: Sgn_Wrap
s, f :: Frm_Wrap
f) = l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
forall l sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
anaForm l
l (TH_BSPEC bs -> bs
forall s. TH_BSPEC s -> s
und TH_BSPEC bs
bs) Sgn_Wrap
s Frm_Wrap
f

-- | Unrolling the formula, so that we can analyse it further
unroll :: (Show f, GetRange f, ShATermConvertible f,
             Logic l sub bs sen sy sm si mo sy' rs pf) =>
                l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll :: l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l :: l
l bs :: bs
bs s' :: Sgn_Wrap
s'@(Sgn_Wrap _ s :: THybridSign sign
s) f :: TH_FORMULA f
f =
        case TH_FORMULA f
f of
                  (At n :: MODALITY
n f' :: TH_FORMULA f
f') -> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (MODALITY -> TH_FORMULA sen -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
At MODALITY
n) (Result (TH_FORMULA sen) -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f' Result (TH_FORMULA sen)
-> (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                                 Set MODALITY
-> MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
Set MODALITY -> MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s) MODALITY
n
                  (Box m :: MODALITY
m f' :: TH_FORMULA f
f') -> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (MODALITY -> TH_FORMULA sen -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Box MODALITY
m) (Result (TH_FORMULA sen) -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f' Result (TH_FORMULA sen)
-> (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                                 Set MODALITY
-> MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
Set MODALITY -> MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s) MODALITY
m
                  (Dia m :: MODALITY
m f' :: TH_FORMULA f
f') -> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (MODALITY -> TH_FORMULA sen -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Dia MODALITY
m) (Result (TH_FORMULA sen) -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f' Result (TH_FORMULA sen)
-> (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                                 Set MODALITY
-> MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
Set MODALITY -> MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s) MODALITY
m
                  (Conjunction f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'') -> (TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Conjunction
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f'')
                  (Disjunction f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'') -> (TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Disjunction
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f'')
                  (Implication f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'') -> (TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Implication
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                                           (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f'')
                  (BiImplication f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'') -> (TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 TH_FORMULA sen -> TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
BiImplication
                                             (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                                             (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f'')
                  (Here n :: MODALITY
n) -> Set MODALITY
-> MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
Set MODALITY -> MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
nomOrModCheck (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s) MODALITY
n (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ MODALITY -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f
Here MODALITY
n
                  (Neg f' :: TH_FORMULA f
f') -> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f
Neg (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                  (Uni n :: MODALITY
n f' :: TH_FORMULA f
f') -> ((TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((TH_FORMULA sen -> TH_FORMULA sen)
 -> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen))
-> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ MODALITY -> TH_FORMULA sen -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Uni MODALITY
n) (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs
                   (MODALITY -> Sgn_Wrap -> Sgn_Wrap
addNomToSig MODALITY
n Sgn_Wrap
s') TH_FORMULA f
f') Result (TH_FORMULA sen)
-> (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MODALITY
-> Set MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
MODALITY -> Set MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
checkForRepNom MODALITY
n (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s)
                  (Exist n :: MODALITY
n f' :: TH_FORMULA f
f') -> ((TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((TH_FORMULA sen -> TH_FORMULA sen)
 -> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen))
-> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen)
-> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ MODALITY -> TH_FORMULA sen -> TH_FORMULA sen
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Exist MODALITY
n) (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs
                   (MODALITY -> Sgn_Wrap -> Sgn_Wrap
addNomToSig MODALITY
n Sgn_Wrap
s') TH_FORMULA f
f') Result (TH_FORMULA sen)
-> (TH_FORMULA sen -> Result (TH_FORMULA sen))
-> Result (TH_FORMULA sen)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MODALITY
-> Set MODALITY -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall f.
(Pretty f, GetRange f) =>
MODALITY -> Set MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
checkForRepNom MODALITY
n (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s)
                  (UnderLogic f' :: f
f') ->
                   (sen -> TH_FORMULA sen) -> Result sen -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM sen -> TH_FORMULA sen
forall f. f -> TH_FORMULA f
UnderLogic (Result sen -> Result (TH_FORMULA sen))
-> Result sen -> Result (TH_FORMULA sen)
forall a b. (a -> b) -> a -> b
$ l -> sign -> f -> bs -> Result sen
forall l bs sen si smi sign mor symb raw a b.
StaticAnalysis l bs sen si smi sign mor symb raw =>
l -> a -> b -> bs -> Result sen
undFormAna l
l (THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s) f
f' bs
bs
                  (Par f' :: TH_FORMULA f
f') -> (TH_FORMULA sen -> TH_FORMULA sen)
-> Result (TH_FORMULA sen) -> Result (TH_FORMULA sen)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM TH_FORMULA sen -> TH_FORMULA sen
forall f. TH_FORMULA f -> TH_FORMULA f
Par (l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
forall f l sub bs sen sy sm si mo sy' rs pf.
(Show f, GetRange f, ShATermConvertible f,
 Logic l sub bs sen sy sm si mo sy' rs pf) =>
l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
unroll l
l bs
bs Sgn_Wrap
s' TH_FORMULA f
f')
                  TrueA -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA sen
forall f. TH_FORMULA f
TrueA
                  FalseA -> TH_FORMULA sen -> Result (TH_FORMULA sen)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA sen
forall f. TH_FORMULA f
FalseA
unroll _ _ EmptySign _ = String -> Result (TH_FORMULA sen)
forall a. HasCallStack => String -> a
error "Signature not computable"

-- helper function
addNomToSig :: NOMINAL -> Sgn_Wrap -> Sgn_Wrap
addNomToSig :: MODALITY -> Sgn_Wrap -> Sgn_Wrap
addNomToSig n :: MODALITY
n (Sgn_Wrap l :: l
l s :: THybridSign sign
s) = l -> THybridSign sign -> Sgn_Wrap
forall l sub bs f s sm sign mo sy rw pf.
Logic l sub bs f s sm sign mo sy rw pf =>
l -> THybridSign sign -> Sgn_Wrap
Sgn_Wrap l
l THybridSign sign
s
 { nomies :: Set MODALITY
nomies = MODALITY -> Set MODALITY -> Set MODALITY
forall a. Ord a => a -> Set a -> Set a
Data.Set.insert MODALITY
n (Set MODALITY -> Set MODALITY) -> Set MODALITY -> Set MODALITY
forall a b. (a -> b) -> a -> b
$ THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s}
addNomToSig _ EmptySign = String -> Sgn_Wrap
forall a. HasCallStack => String -> a
error "Signature not computable"

checkForRepNom :: (Pretty f, GetRange f) =>
        NOMINAL -> Set NOMINAL -> TH_FORMULA f -> Result (TH_FORMULA f)
checkForRepNom :: MODALITY -> Set MODALITY -> TH_FORMULA f -> Result (TH_FORMULA f)
checkForRepNom n :: MODALITY
n s :: Set MODALITY
s = if MODALITY -> Set MODALITY -> Bool
forall a. Ord a => a -> Set a -> Bool
member MODALITY
n Set MODALITY
s
        then String -> TH_FORMULA f -> Result (TH_FORMULA f)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "conflict in nominal decl and quantification"
        else TH_FORMULA f -> Result (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return
{- | Lift of the formula analyser
Analyses each formula and collects the results. Converting also the
annotations to the correct format. The function flipM is needed because
we want the annotations independent from the analyser -}
anaForms :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
        l -> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
anaForms :: l
-> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
anaForms l :: l
l bs :: bs
bs f :: [Annoted Frm_Wrap]
f s :: Sgn_Wrap
s = (Annoted Frm_Wrap -> Result (Named Frm_Wrap))
-> [Annoted Frm_Wrap] -> Result [Named Frm_Wrap]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Named (Result Frm_Wrap) -> Result (Named Frm_Wrap)
forall (m :: * -> *) a. Monad m => Named (m a) -> m (Named a)
flipM (Named (Result Frm_Wrap) -> Result (Named Frm_Wrap))
-> (Annoted Frm_Wrap -> Named (Result Frm_Wrap))
-> Annoted Frm_Wrap
-> Result (Named Frm_Wrap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (Result Frm_Wrap) -> Named (Result Frm_Wrap)
forall a. Annoted a -> Named a
makeNamedSen (Annoted (Result Frm_Wrap) -> Named (Result Frm_Wrap))
-> (Annoted Frm_Wrap -> Annoted (Result Frm_Wrap))
-> Annoted Frm_Wrap
-> Named (Result Frm_Wrap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Frm_Wrap -> Result Frm_Wrap)
-> Annoted Frm_Wrap -> Annoted (Result Frm_Wrap)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
forall l sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
anaForm l
l bs
bs Sgn_Wrap
s)) [Annoted Frm_Wrap]
f

-- Just flips the monad position with the functor
flipM :: (Monad m) => Named (m a) -> m (Named a)
flipM :: Named (m a) -> m (Named a)
flipM y :: Named (m a)
y = Named (m a) -> m a
forall s a. SenAttr s a -> s
sentence Named (m a)
y m a -> (a -> m (Named a)) -> m (Named a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ a :: a
a -> Named a -> m (Named a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named a -> m (Named a)) -> Named a -> m (Named a)
forall a b. (a -> b) -> a -> b
$ (m a -> a) -> Named (m a) -> Named a
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (a -> m a -> a
forall a b. a -> b -> a
const a
a) Named (m a)
y

{- | Examining the list of formulas and collecting results

Analyses first the underlying spec; Then analyses the top spec
(without the axioms) and merges the resulting sig with the underlying one.
Also translates the underlying axioms into hybridized ones, so that in the
end all axioms are of the same type;
Next analyses the hybrid axioms and puts them together with the already
translated axioms.
Finnaly prepares the tuple format for outputting. -}
thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) ->
        Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
thAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos)
-> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
thAna (Spc_Wrap l :: l
l sp :: TH_BSPEC bs
sp fs :: [Annoted Frm_Wrap]
fs, _, _) = Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
forall symbol.
Result (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap])
finalRes
        where
        undA :: Result (bs, ExtSign sign symb, [Named sen])
undA = l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
forall l bs sen si smi sign mor symb raw.
StaticAnalysis l bs sen si smi sign mor symb raw =>
l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
undAna l
l (bs -> Result (bs, ExtSign sign symb, [Named sen]))
-> bs -> Result (bs, ExtSign sign symb, [Named sen])
forall a b. (a -> b) -> a -> b
$ TH_BSPEC bs -> bs
forall s. TH_BSPEC s -> s
und TH_BSPEC bs
sp
        partMerge :: Result (bs, Sgn_Wrap, [Named Frm_Wrap])
partMerge = Result (bs, ExtSign sign symb, [Named sen])
undA Result (bs, ExtSign sign symb, [Named sen])
-> ((bs, ExtSign sign symb, [Named sen])
    -> Result (bs, Sgn_Wrap, [Named Frm_Wrap]))
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (x1 :: bs
x1, x2 :: ExtSign sign symb
x2, x3 :: [Named sen]
x3) -> [TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
forall l sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
[TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
topAna (TH_BSPEC bs -> [TH_BASIC_ITEM]
forall s. TH_BSPEC s -> [TH_BASIC_ITEM]
bitems TH_BSPEC bs
sp) l
l
                     (ExtSign sign symb -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symb
x2) Result Sgn_Wrap
-> (Sgn_Wrap -> Result (bs, Sgn_Wrap, [Named Frm_Wrap]))
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ x :: Sgn_Wrap
x -> (bs, Sgn_Wrap, [Named Frm_Wrap])
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a. Monad m => a -> m a
return (bs
x1, Sgn_Wrap
x, [Named sen] -> [Named Frm_Wrap]
forall a. [SenAttr sen a] -> [SenAttr Frm_Wrap a]
formMap [Named sen]
x3)
        partMerge' :: Result (bs, Sgn_Wrap, [Named Frm_Wrap])
partMerge' = Result (bs, Sgn_Wrap, [Named Frm_Wrap])
partMerge Result (bs, Sgn_Wrap, [Named Frm_Wrap])
-> ((bs, Sgn_Wrap, [Named Frm_Wrap])
    -> Result (bs, Sgn_Wrap, [Named Frm_Wrap]))
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (x1 :: bs
x1, x2 :: Sgn_Wrap
x2, x3 :: [Named Frm_Wrap]
x3) ->
                      l
-> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
forall l sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
l
-> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
anaForms l
l bs
x1 [Annoted Frm_Wrap]
fs Sgn_Wrap
x2 Result [Named Frm_Wrap]
-> ([Named Frm_Wrap] -> Result (bs, Sgn_Wrap, [Named Frm_Wrap]))
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ x :: [Named Frm_Wrap]
x -> (bs, Sgn_Wrap, [Named Frm_Wrap])
-> Result (bs, Sgn_Wrap, [Named Frm_Wrap])
forall (m :: * -> *) a. Monad m => a -> m a
return (bs
x1, Sgn_Wrap
x2, [Named Frm_Wrap]
x3 [Named Frm_Wrap] -> [Named Frm_Wrap] -> [Named Frm_Wrap]
forall a. [a] -> [a] -> [a]
++ [Named Frm_Wrap]
x)
        finalRes :: Result (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap])
finalRes = Result (bs, Sgn_Wrap, [Named Frm_Wrap])
partMerge' Result (bs, Sgn_Wrap, [Named Frm_Wrap])
-> ((bs, Sgn_Wrap, [Named Frm_Wrap])
    -> Result (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap]))
-> Result (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (x1 :: bs
x1, x2 :: Sgn_Wrap
x2, x3 :: [Named Frm_Wrap]
x3) ->
                    (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap])
-> Result (Spc_Wrap, ExtSign Sgn_Wrap symbol, [Named Frm_Wrap])
forall (m :: * -> *) a. Monad m => a -> m a
return (bs -> Spc_Wrap
forall sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
bs -> Spc_Wrap
mergSpec bs
x1, Sgn_Wrap -> ExtSign Sgn_Wrap symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign Sgn_Wrap
x2, [Named Frm_Wrap]
x3)
        formMap :: [SenAttr sen a] -> [SenAttr Frm_Wrap a]
formMap = (SenAttr sen a -> SenAttr Frm_Wrap a)
-> [SenAttr sen a] -> [SenAttr Frm_Wrap a]
forall a b. (a -> b) -> [a] -> [b]
Data.List.map ((SenAttr sen a -> SenAttr Frm_Wrap a)
 -> [SenAttr sen a] -> [SenAttr Frm_Wrap a])
-> (SenAttr sen a -> SenAttr Frm_Wrap a)
-> [SenAttr sen a]
-> [SenAttr Frm_Wrap a]
forall a b. (a -> b) -> a -> b
$ (sen -> Frm_Wrap) -> SenAttr sen a -> SenAttr Frm_Wrap a
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((sen -> Frm_Wrap) -> SenAttr sen a -> SenAttr Frm_Wrap a)
-> (sen -> Frm_Wrap) -> SenAttr sen a -> SenAttr Frm_Wrap a
forall a b. (a -> b) -> a -> b
$ l -> TH_FORMULA sen -> Frm_Wrap
forall l sub bs f s sm si mo sy rw pf.
Logic l sub bs f s sm si mo sy rw pf =>
l -> TH_FORMULA f -> Frm_Wrap
Frm_Wrap l
l (TH_FORMULA sen -> Frm_Wrap)
-> (sen -> TH_FORMULA sen) -> sen -> Frm_Wrap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sen -> TH_FORMULA sen
forall f. f -> TH_FORMULA f
UnderLogic
        mergSpec :: bs -> Spc_Wrap
mergSpec e :: bs
e = l -> TH_BSPEC bs -> [Annoted Frm_Wrap] -> Spc_Wrap
forall l sub bs sen si smi sign mor symb raw pf.
Logic l sub bs sen si smi sign mor symb raw pf =>
l -> TH_BSPEC bs -> [Annoted Frm_Wrap] -> Spc_Wrap
Spc_Wrap l
l ([TH_BASIC_ITEM] -> bs -> TH_BSPEC bs
forall s. [TH_BASIC_ITEM] -> s -> TH_BSPEC s
Bspec (TH_BSPEC bs -> [TH_BASIC_ITEM]
forall s. TH_BSPEC s -> [TH_BASIC_ITEM]
bitems TH_BSPEC bs
sp) bs
e) [Annoted Frm_Wrap]
fs


-- Analysis of the underlying logic spec
undAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
undAna :: l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
undAna l :: l
l b :: bs
b = (Int
-> Maybe
     ((bs, sign, GlobalAnnos)
      -> Result (bs, ExtSign sign symb, [Named sen]))
-> (bs, sign, GlobalAnnos)
-> Result (bs, ExtSign sign symb, [Named sen])
forall a. Int -> Maybe a -> a
maybeE 2 (Maybe
   ((bs, sign, GlobalAnnos)
    -> Result (bs, ExtSign sign symb, [Named sen]))
 -> (bs, sign, GlobalAnnos)
 -> Result (bs, ExtSign sign symb, [Named sen]))
-> Maybe
     ((bs, sign, GlobalAnnos)
      -> Result (bs, ExtSign sign symb, [Named sen]))
-> (bs, sign, GlobalAnnos)
-> Result (bs, ExtSign sign symb, [Named sen])
forall a b. (a -> b) -> a -> b
$ l
-> Maybe
     ((bs, sign, GlobalAnnos)
      -> Result (bs, ExtSign sign symb, [Named sen]))
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
basic_analysis l
l) (bs, sign, GlobalAnnos)
x
        where x :: (bs, sign, GlobalAnnos)
x = (bs
b, l -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature l
l, GlobalAnnos
emptyGlobalAnnos)

unsafeToForm :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> a -> sen
unsafeToForm :: l -> a -> sen
unsafeToForm _ = a -> sen
forall a b. a -> b
unsafeCoerce
unsafeToSig :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
               l -> a -> sign
unsafeToSig :: l -> a -> sign
unsafeToSig _ = a -> sign
forall a b. a -> b
unsafeCoerce

{- Analysis of the sentences part the corresponds to the underlying logic. We
   need to use the unsafe functions here, because the typechecker has no way
   to check the (simple) relations (l -> sig) and (l -> sen). In other words
   it can't check that the arguments l and a belong to the Logic class,
   likewise for l -> b. The unsafe functions will give the "right"
   type associated with l. -}
undFormAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
                l -> a -> b -> bs -> Result sen
undFormAna :: l -> a -> b -> bs -> Result sen
undFormAna l :: l
l a :: a
a b :: b
b c :: bs
c = (Int
-> Maybe ((bs, sign, sen) -> Result sen)
-> (bs, sign, sen)
-> Result sen
forall a. Int -> Maybe a -> a
maybeE 4 (Maybe ((bs, sign, sen) -> Result sen)
 -> (bs, sign, sen) -> Result sen)
-> Maybe ((bs, sign, sen) -> Result sen)
-> (bs, sign, sen)
-> Result sen
forall a b. (a -> b) -> a -> b
$ l -> Maybe ((bs, sign, sen) -> Result sen)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Maybe ((basic_spec, sign, sentence) -> Result sentence)
sen_analysis l
l) (bs
c, sign
a', sen
b')
        where a' :: sign
a' = l -> a -> sign
forall l bs sen si smi sign mor symb raw a.
StaticAnalysis l bs sen si smi sign mor symb raw =>
l -> a -> sign
unsafeToSig l
l a
a
              b' :: sen
b' = l -> b -> sen
forall l bs sen si smi sign mor symb raw a.
StaticAnalysis l bs sen si smi sign mor symb raw =>
l -> a -> sen
unsafeToForm l
l b
b


{- -- Operations on sentences ----
How can we guarantee that the l in Sgn_Wrap is equal
to the l in Frm_Wrap ? -}
simSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
simSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
simSen (Sgn_Wrap _ s :: THybridSign sign
s) (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) = l -> TH_FORMULA f -> Frm_Wrap
forall l sub bs f s sm si mo sy rw pf.
Logic l sub bs f s sm si mo sy rw pf =>
l -> TH_FORMULA f -> Frm_Wrap
Frm_Wrap l
l (TH_FORMULA f -> Frm_Wrap) -> TH_FORMULA f -> Frm_Wrap
forall a b. (a -> b) -> a -> b
$
                l -> si -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l (sign -> si
forall a b. a -> b
unsafeCoerce (THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s)) TH_FORMULA f
f
simSen EmptySign _ = String -> Frm_Wrap
forall a. HasCallStack => String -> a
error "The signature cannot be empty"

uroll :: (Logic l sub bs f s sm sgn mo sy rw pf) =>
        l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll :: l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l :: l
l s :: sgn
s f :: TH_FORMULA f
f = case TH_FORMULA f
f of
                At n :: MODALITY
n f' :: TH_FORMULA f
f' -> MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
At MODALITY
n (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f'
                Box m :: MODALITY
m f' :: TH_FORMULA f
f' -> MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Box MODALITY
m (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f'
                Dia m :: MODALITY
m f' :: TH_FORMULA f
f' -> MODALITY -> TH_FORMULA f -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f -> TH_FORMULA f
Dia MODALITY
m (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f'
                Conjunction f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'' -> TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Conjunction (l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f') (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f''
                Disjunction f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'' -> TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Disjunction (l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f') (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f''
                Implication f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'' -> TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Implication (l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f') (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f''
                BiImplication f' :: TH_FORMULA f
f' f'' :: TH_FORMULA f
f'' -> TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
BiImplication (l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f') (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$
                                         l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f''
                Here n :: MODALITY
n -> MODALITY -> TH_FORMULA f
forall f. MODALITY -> TH_FORMULA f
Here MODALITY
n
                Neg f' :: TH_FORMULA f
f' -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Neg (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f'
                Par f' :: TH_FORMULA f
f' -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Par (TH_FORMULA f -> TH_FORMULA f) -> TH_FORMULA f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> TH_FORMULA f -> TH_FORMULA f
forall l sub bs f s sm sgn mo sy rw pf.
Logic l sub bs f s sm sgn mo sy rw pf =>
l -> sgn -> TH_FORMULA f -> TH_FORMULA f
uroll l
l sgn
s TH_FORMULA f
f'
                UnderLogic f' :: f
f' -> f -> TH_FORMULA f
forall f. f -> TH_FORMULA f
UnderLogic (f -> TH_FORMULA f) -> f -> TH_FORMULA f
forall a b. (a -> b) -> a -> b
$ l -> sgn -> f -> f
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen l
l sgn
s f
f'
                x :: TH_FORMULA f
x -> TH_FORMULA f
x

{- These instances should be automatically generated by DriFT, but it cannot
since they are not declared in a usual format -}
instance ShATermConvertible Sgn_Wrap where
         toShATermAux :: ATermTable -> Sgn_Wrap -> IO (ATermTable, Int)
toShATermAux att :: ATermTable
att (Sgn_Wrap _ s :: THybridSign sign
s) = ATermTable -> THybridSign sign -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATermAux ATermTable
att THybridSign sign
s
         toShATermAux _ EmptySign = String -> IO (ATermTable, Int)
forall a. HasCallStack => String -> a
error "I entered in emptySign"
         fromShATermAux :: Int -> ATermTable -> (ATermTable, Sgn_Wrap)
fromShATermAux _ _ = String -> (ATermTable, Sgn_Wrap)
forall a. HasCallStack => String -> a
error "I entered here"

instance ShATermConvertible Spc_Wrap where
         toShATermAux :: ATermTable -> Spc_Wrap -> IO (ATermTable, Int)
toShATermAux att :: ATermTable
att (Spc_Wrap _ s :: TH_BSPEC bs
s _) = ATermTable -> TH_BSPEC bs -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATermAux ATermTable
att TH_BSPEC bs
s
         fromShATermAux :: Int -> ATermTable -> (ATermTable, Spc_Wrap)
fromShATermAux _ _ = String -> (ATermTable, Spc_Wrap)
forall a. HasCallStack => String -> a
error "I entered here"

instance ShATermConvertible Frm_Wrap where
        toShATermAux :: ATermTable -> Frm_Wrap -> IO (ATermTable, Int)
toShATermAux att :: ATermTable
att (Frm_Wrap _ f :: TH_FORMULA f
f) = ATermTable -> TH_FORMULA f -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATermAux ATermTable
att TH_FORMULA f
f
        fromShATermAux :: Int -> ATermTable -> (ATermTable, Frm_Wrap)
fromShATermAux _ _ = String -> (ATermTable, Frm_Wrap)
forall a. HasCallStack => String -> a
error "I entered here"



instance ToJSON Sgn_Wrap where
  toJSON :: Sgn_Wrap -> Value
toJSON (Sgn_Wrap _ s :: THybridSign sign
s) = THybridSign sign -> Value
forall a. ToJSON a => a -> Value
toJSON THybridSign sign
s
  toJSON EmptySign = Value
Null
instance FromJSON Sgn_Wrap where
  parseJSON :: Value -> Parser Sgn_Wrap
parseJSON = String -> Value -> Parser Sgn_Wrap
forall a. HasCallStack => String -> a
error "fromJSON not implemented for Sgn_Wrap"

instance ToJSON Spc_Wrap where
  toJSON :: Spc_Wrap -> Value
toJSON (Spc_Wrap _ spec :: TH_BSPEC bs
spec sen :: [Annoted Frm_Wrap]
sen) = [Pair] -> Value
object ["spec" Text -> TH_BSPEC bs -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= TH_BSPEC bs
spec, "sen" Text -> [Annoted Frm_Wrap] -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= [Annoted Frm_Wrap]
sen]
instance FromJSON Spc_Wrap where
  parseJSON :: Value -> Parser Spc_Wrap
parseJSON = String -> Value -> Parser Spc_Wrap
forall a. HasCallStack => String -> a
error "fromJSON not implemented for Spc_Wrap"

instance ToJSON Frm_Wrap where
  toJSON :: Frm_Wrap -> Value
toJSON (Frm_Wrap _ f :: TH_FORMULA f
f) = TH_FORMULA f -> Value
forall a. ToJSON a => a -> Value
toJSON TH_FORMULA f
f
instance FromJSON Frm_Wrap where
  parseJSON :: Value -> Parser Frm_Wrap
parseJSON = String -> Value -> Parser Frm_Wrap
forall a. HasCallStack => String -> a
error "fromJSON not implemented for Frm_Wrap"