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

Maintainer  :  nevrenato@gmail.com
Stability   :  provisional
Portability :  portable


Description  :
Parser for an hybridized arbitrary logic
-}

module TopHybrid.Parse_AS where

import Common.AnnoState
import Common.AS_Annotation
import Common.GlobalAnnotations (PrefixMap)
import Common.Token
import Data.Maybe
import qualified Data.Map as Map
import Text.ParserCombinators.Parsec
import Logic.Logic
import TopHybrid.AS_TopHybrid
import Control.Monad (liftM)

-- the top parser; parses an entire specification
thBasic :: (String -> AnyLogic) -> AParser st Spc_Wrap
thBasic :: (String -> AnyLogic) -> AParser st Spc_Wrap
thBasic getLogic :: String -> AnyLogic
getLogic =
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "baselogic"
        Token
logicName <- AParser st Token
forall st. GenParser Char st Token
simpleId
        AnyLogic -> AParser st Spc_Wrap
forall st. AnyLogic -> AParser st Spc_Wrap
thSpec (AnyLogic -> AParser st Spc_Wrap)
-> AnyLogic -> AParser st Spc_Wrap
forall a b. (a -> b) -> a -> b
$ String -> AnyLogic
getLogic (String -> AnyLogic) -> String -> AnyLogic
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
logicName

basicSpec :: (Syntax lid basic_spec s si sim) =>
 lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpec l :: lid
l = Maybe (PrefixMap -> AParser st basic_spec)
-> ((PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
    -> Maybe (PrefixMap -> AParser st basic_spec))
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> Maybe (PrefixMap -> AParser st basic_spec)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (lid -> Maybe (PrefixMap -> AParser st basic_spec)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st basic_spec)
parse_basic_spec lid
l) ((PrefixMap -> AParser st basic_spec)
-> Maybe (PrefixMap -> AParser st basic_spec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st basic_spec)
 -> Maybe (PrefixMap -> AParser st basic_spec))
-> ((PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
    -> PrefixMap -> AParser st basic_spec)
-> (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> Maybe (PrefixMap -> AParser st basic_spec)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
-> PrefixMap -> AParser st basic_spec
forall a b. (a, b) -> a
fst)
 (Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Maybe IRI
-> lid
-> Maybe (PrefixMap -> AParser st basic_spec, basic_spec -> Doc)
parserAndPrinter Maybe IRI
forall a. Maybe a
Nothing lid
l)

{- Parses the specification after knowing
the underlying logic -}
thSpec :: AnyLogic -> AParser st Spc_Wrap
thSpec :: AnyLogic -> AParser st Spc_Wrap
thSpec (Logic l :: lid
l) =
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "Basic_Spec"
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "{"
        basic_spec
s <- lid
-> (lid -> Maybe (PrefixMap -> AParser st basic_spec))
-> PrefixMap
-> AParser st basic_spec
forall a x. Show a => a -> (a -> Maybe x) -> x
callParser lid
l lid -> Maybe (PrefixMap -> AParser st basic_spec)
forall lid basic_spec s si sim st.
Syntax lid basic_spec s si sim =>
lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpec PrefixMap
forall k a. Map k a
Map.empty
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "}"
        [TH_BASIC_ITEM]
i <- ParsecT String (AnnoState st) Identity TH_BASIC_ITEM
-> ParsecT String (AnnoState st) Identity [TH_BASIC_ITEM]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String (AnnoState st) Identity TH_BASIC_ITEM
forall st. AParser st TH_BASIC_ITEM
itemParser
        [Annoted Frm_Wrap]
fs <- ParsecT String (AnnoState st) Identity (Annoted Frm_Wrap)
-> AParser st Token
-> ParsecT String (AnnoState st) Identity [Annoted Frm_Wrap]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy (lid
-> basic_spec
-> ParsecT String (AnnoState st) Identity (Annoted Frm_Wrap)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (Annoted Frm_Wrap)
annoFormParser lid
l basic_spec
s) AParser st Token
forall st. AParser st Token
anSemiOrComma
        Spc_Wrap -> AParser st Spc_Wrap
forall (m :: * -> *) a. Monad m => a -> m a
return (Spc_Wrap -> AParser st Spc_Wrap)
-> Spc_Wrap -> AParser st Spc_Wrap
forall a b. (a -> b) -> a -> b
$ lid -> TH_BSPEC basic_spec -> [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 lid
l ([TH_BASIC_ITEM] -> basic_spec -> TH_BSPEC basic_spec
forall s. [TH_BASIC_ITEM] -> s -> TH_BSPEC s
Bspec [TH_BASIC_ITEM]
i basic_spec
s) [Annoted Frm_Wrap]
fs

{- Calls the underlying logic parser, only if exists. Otherwise
will throw out an error -}
callParser :: (Show a) => a -> (a -> Maybe x) -> x
callParser :: a -> (a -> Maybe x) -> x
callParser l :: a
l f :: a -> Maybe x
f =
 x -> Maybe x -> x
forall a. a -> Maybe a -> a
fromMaybe (String -> x
forall a. HasCallStack => String -> a
error (String -> x) -> String -> x
forall a b. (a -> b) -> a -> b
$ "Failed! No parser for logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
l) (Maybe x -> x) -> Maybe x -> x
forall a b. (a -> b) -> a -> b
$ a -> Maybe x
f a
l

-- Parses the declaration of nominals and modalities
itemParser :: AParser st TH_BASIC_ITEM
itemParser :: AParser st TH_BASIC_ITEM
itemParser =
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "modalities"
        [Token]
ms <- ParsecT String (AnnoState st) Identity [Token]
forall st. ParsecT String (AnnoState st) Identity [Token]
ids
        TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM)
-> TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Token] -> TH_BASIC_ITEM
Simple_mod_decl [Token]
ms
        AParser st TH_BASIC_ITEM
-> AParser st TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "nominals"
        [Token]
ns <- ParsecT String (AnnoState st) Identity [Token]
forall st. ParsecT String (AnnoState st) Identity [Token]
ids
        TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM)
-> TH_BASIC_ITEM -> AParser st TH_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Token] -> TH_BASIC_ITEM
Simple_nom_decl [Token]
ns
        where ids :: ParsecT String (AnnoState st) Identity [Token]
ids = ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity [Token]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT String (AnnoState st) Identity Token
forall st. GenParser Char st Token
simpleId ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
anSemiOrComma


-- Formula parser with annotations
annoFormParser :: (Logic l sub bs f s sm si mo sy rw pf) =>
                        l -> bs -> AParser st (Annoted Frm_Wrap)
annoFormParser :: l -> bs -> AParser st (Annoted Frm_Wrap)
annoFormParser l :: l
l b :: bs
b = AParser st Frm_Wrap -> AParser st (Annoted Frm_Wrap)
forall st a. AParser st a -> AParser st (Annoted a)
allAnnoParser (AParser st Frm_Wrap -> AParser st (Annoted Frm_Wrap))
-> AParser st Frm_Wrap -> AParser st (Annoted Frm_Wrap)
forall a b. (a -> b) -> a -> b
$ l -> bs -> AParser st Frm_Wrap
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st Frm_Wrap
formParser l
l bs
b

-- Just parses the formula, and wraps it in Frm_Wrap
formParser :: (Logic l sub bs f s sm si mo sy rw pf) =>
                        l -> bs -> AParser st Frm_Wrap
formParser :: l -> bs -> AParser st Frm_Wrap
formParser l :: l
l bs :: bs
bs = (TH_FORMULA f -> Frm_Wrap)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
-> AParser st Frm_Wrap
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (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) (ParsecT String (AnnoState st) Identity (TH_FORMULA f)
 -> AParser st Frm_Wrap)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
-> AParser st Frm_Wrap
forall a b. (a -> b) -> a -> b
$ l -> bs -> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs

-- Parser of hybridization of hybridization of sentences
formParser' :: Spc_Wrap -> AParser st Frm_Wrap
formParser' :: Spc_Wrap -> AParser st Frm_Wrap
formParser' (Spc_Wrap l :: l
l b :: TH_BSPEC bs
b _) = (TH_FORMULA sen -> Frm_Wrap)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA sen)
-> AParser st 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) (ParsecT String (AnnoState st) Identity (TH_FORMULA sen)
 -> AParser st Frm_Wrap)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA sen)
-> AParser st Frm_Wrap
forall a b. (a -> b) -> a -> b
$ l -> bs -> ParsecT String (AnnoState st) Identity (TH_FORMULA sen)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l (TH_BSPEC bs -> bs
forall s. TH_BSPEC s -> s
und TH_BSPEC bs
b)

{- Parser of sentences
The precendence order is left associative and when the priority
is defined is as follows : () > (not,@,[],<>) > /\ > \/ > (->,<->) -}
topParser :: (Logic l sub bs f s sm si mo sy rw pf) =>
                l -> bs -> AParser st (TH_FORMULA f)
topParser :: l -> bs -> AParser st (TH_FORMULA f)
topParser l :: l
l bs :: bs
bs = AParser st (TH_FORMULA f)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (a -> a -> a) -> ParsecT s u m a
chainl1 AParser st (TH_FORMULA f)
forall st. ParsecT String (AnnoState st) Identity (TH_FORMULA f)
fp1 ParsecT
  String
  (AnnoState st)
  Identity
  (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall st f.
AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
impAndBiP
        where fp1 :: ParsecT String (AnnoState st) Identity (TH_FORMULA f)
fp1 = ParsecT String (AnnoState st) Identity (TH_FORMULA f)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (a -> a -> a) -> ParsecT s u m a
chainl1 ParsecT String (AnnoState st) Identity (TH_FORMULA f)
forall st. ParsecT String (AnnoState st) Identity (TH_FORMULA f)
fp2 ParsecT
  String
  (AnnoState st)
  Identity
  (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall st f.
AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
disjP
              fp2 :: ParsecT String (AnnoState st) Identity (TH_FORMULA f)
fp2 = ParsecT String (AnnoState st) Identity (TH_FORMULA f)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (a -> a -> a) -> ParsecT s u m a
chainl1 (l -> bs -> ParsecT String (AnnoState st) Identity (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs) ParsecT
  String
  (AnnoState st)
  Identity
  (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall st f.
AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
conjP

{- BinaryOps parsers, the reason to separate them, is that so we can get a
precedence order -}
conjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
conjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
conjP = String -> AParser st Token
forall st. String -> AParser st Token
asKey "/\\" AParser st Token
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Conjunction

disjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
disjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
disjP = String -> AParser st Token
forall st. String -> AParser st Token
asKey "\\/" AParser st Token
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Disjunction

impAndBiP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
impAndBiP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
impAndBiP = (String -> AParser st Token
forall st. String -> AParser st Token
asKey "=>" AParser st Token
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Implication) AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            (String -> AParser st Token
forall st. String -> AParser st Token
asKey "<=>" AParser st Token
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
BiImplication)
-- ------------

-- Parser of sentences without the binary operators
fParser :: (Logic l sub bs f s sm si mo sy rw pf) =>
                l -> bs -> AParser st (TH_FORMULA f)
fParser :: l -> bs -> AParser st (TH_FORMULA f)
fParser l :: l
l bs :: bs
bs =
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "("
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        String -> AParser st Token
forall st. String -> AParser st Token
asKey ")"
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Par TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "not"
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f
Neg TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "@"
        Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
At Token
n TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "!"
        Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Uni Token
n TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "?"
        Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Exist Token
n TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "["
        Token
m <- AParser st Token
forall st. GenParser Char st Token
simpleId
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "]"
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Box Token
m TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "<"
        Token
m <- AParser st Token
forall st. GenParser Char st Token
simpleId
        String -> AParser st Token
forall st. String -> AParser st Token
asKey ">\""
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ 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
$ TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
forall f. TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Conjunction (Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Dia Token
m TH_FORMULA f
f) (Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Box Token
m TH_FORMULA f
f))
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "<"
        Token
m <- AParser st Token
forall st. GenParser Char st Token
simpleId
        String -> AParser st Token
forall st. String -> AParser st Token
asKey ">"
        TH_FORMULA f
f <- l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
fParser l
l bs
bs AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> l -> bs -> AParser st (TH_FORMULA f)
forall l sub bs f s sm si mo sy rw pf st.
Logic l sub bs f s sm si mo sy rw pf =>
l -> bs -> AParser st (TH_FORMULA f)
topParser l
l bs
bs
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f -> TH_FORMULA f
forall f. Token -> TH_FORMULA f -> TH_FORMULA f
Dia Token
m TH_FORMULA f
f
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "true"
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f
forall f. TH_FORMULA f
TrueA
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "false"
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return TH_FORMULA f
forall f. TH_FORMULA f
FalseA
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> TH_FORMULA f
forall f. Token -> TH_FORMULA f
Here Token
n
        AParser st (TH_FORMULA f)
-> AParser st (TH_FORMULA f) -> AParser st (TH_FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "{"
        f
f <- l -> (l -> Maybe (bs -> AParser st f)) -> bs -> AParser st f
forall a x. Show a => a -> (a -> Maybe x) -> x
callParser l
l l -> Maybe (bs -> AParser st f)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree st.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Maybe (basic_spec -> AParser st sentence)
parse_basic_sen bs
bs
        String -> AParser st Token
forall st. String -> AParser st Token
asKey "}"
        TH_FORMULA f -> AParser st (TH_FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TH_FORMULA f -> AParser st (TH_FORMULA f))
-> TH_FORMULA f -> AParser st (TH_FORMULA f)
forall a b. (a -> b) -> a -> b
$ f -> TH_FORMULA f
forall f. f -> TH_FORMULA f
UnderLogic f
f