{- |
Module      :  ./DFOL/Parse_AS_DFOL.hs
Description :  A parser for first-order logic with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Parse_AS_DFOL
       (
           basicSpec           -- parser for DFOL specifications
       , symbItems           -- parser for symbol lists
       , symbMapItems        -- parser for symbol map lists
       )
       where

import qualified Common.Lexer as Lexer
import Common.Parsec
import Common.Token (criticalKeywords)
import qualified Common.Keywords as Keywords
import qualified Common.AnnoState as AnnoState
import Common.GlobalAnnotations (PrefixMap)
import DFOL.AS_DFOL
import Text.ParserCombinators.Parsec

-- keywords which cannot appear as identifiers in a signature
dfolKeys :: [String]
dfolKeys :: [String]
dfolKeys = [String
Keywords.trueS,
            String
Keywords.falseS,
            String
Keywords.notS,
            String
Keywords.forallS,
            String
Keywords.existsS,
            "Univ",
            "Sort",
            "Form",
            "Pi"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
criticalKeywords

-- parser for basic spec
basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec :: PrefixMap -> AParser st BASIC_SPEC
basicSpec _ = ([Annoted BASIC_ITEM] -> BASIC_SPEC)
-> ParsecT String (AnnoState st) Identity [Annoted BASIC_ITEM]
-> AParser st BASIC_SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec (AParser st BASIC_ITEM
-> ParsecT String (AnnoState st) Identity [Annoted BASIC_ITEM]
forall st a. AParser st a -> AParser st [Annoted a]
AnnoState.trailingAnnosParser AParser st BASIC_ITEM
forall st. AParser st BASIC_ITEM
basicItemP)
            AParser st BASIC_SPEC
-> AParser st BASIC_SPEC -> AParser st BASIC_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            (CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.oBraceT CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.cBraceT CharParser (AnnoState st) Token
-> AParser st BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec []))

-- parser for basic items
basicItemP :: AnnoState.AParser st BASIC_ITEM
basicItemP :: AParser st BASIC_ITEM
basicItemP = do AParser st Token
forall st. AParser st Token
AnnoState.dotT
                FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formulaP
                BASIC_ITEM -> AParser st BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEM -> AParser st BASIC_ITEM)
-> BASIC_ITEM -> AParser st BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ FORMULA -> BASIC_ITEM
Axiom_item FORMULA
f
             AParser st BASIC_ITEM
-> AParser st BASIC_ITEM -> AParser st BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
             do [Token]
ns <- AParser st [Token]
forall st. AParser st [Token]
namesP
                String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey "::"
                TYPE
t <- AParser st TYPE
forall st. AParser st TYPE
typeP
                BASIC_ITEM -> AParser st BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEM -> AParser st BASIC_ITEM)
-> BASIC_ITEM -> AParser st BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ DECL -> BASIC_ITEM
Decl_item ([Token]
ns, TYPE
t)

-- parser for all types
typeP :: AnnoState.AParser st TYPE
typeP :: AParser st TYPE
typeP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey "Pi"
           [DECL]
vs <- AParser st [DECL]
forall st. AParser st [DECL]
varsP
           TYPE
t <- AParser st TYPE
forall st. AParser st TYPE
typeP
           TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (TYPE -> AParser st TYPE) -> TYPE -> AParser st TYPE
forall a b. (a -> b) -> a -> b
$ [DECL] -> TYPE -> TYPE
Pi [DECL]
vs TYPE
t
        AParser st TYPE -> AParser st TYPE -> AParser st TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
        do TYPE
t <- AParser st TYPE
forall st. AParser st TYPE
type1P
           (do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.funS
               (ts :: [TYPE]
ts, _) <- AParser st TYPE
forall st. AParser st TYPE
type1P AParser st TYPE
-> AParser st Token
-> GenParser Char (AnnoState st) ([TYPE], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy`
                            String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.funS
               let xs :: [TYPE]
xs = TYPE
t TYPE -> [TYPE] -> [TYPE]
forall a. a -> [a] -> [a]
: [TYPE]
ts
               TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (TYPE -> AParser st TYPE) -> TYPE -> AParser st TYPE
forall a b. (a -> b) -> a -> b
$ [TYPE] -> TYPE -> TYPE
Func ([TYPE] -> [TYPE]
forall a. [a] -> [a]
init [TYPE]
xs) ([TYPE] -> TYPE
forall a. [a] -> a
last [TYPE]
xs))
            AParser st TYPE -> AParser st TYPE -> AParser st TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return TYPE
t

-- parser for basic types and types enclosed in parentheses
type1P :: AnnoState.AParser st TYPE
type1P :: AParser st TYPE
type1P = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey "Sort"
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return TYPE
Sort
         AParser st TYPE -> AParser st TYPE -> AParser st TYPE
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
AnnoState.asKey "Form"
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return TYPE
Form
         AParser st TYPE -> AParser st TYPE -> AParser st TYPE
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
AnnoState.asKey "Univ"
            AParser st Token
forall st. CharParser st Token
Lexer.oParenT
            TERM
t <- AParser st TERM
forall st. AParser st TERM
termP
            AParser st Token
forall st. CharParser st Token
Lexer.cParenT
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (TYPE -> AParser st TYPE) -> TYPE -> AParser st TYPE
forall a b. (a -> b) -> a -> b
$ TERM -> TYPE
Univ TERM
t
         AParser st TYPE -> AParser st TYPE -> AParser st TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
         do TERM
t <- AParser st TERM
forall st. AParser st TERM
termP
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (TYPE -> AParser st TYPE) -> TYPE -> AParser st TYPE
forall a b. (a -> b) -> a -> b
$ TERM -> TYPE
Univ TERM
t
         AParser st TYPE -> AParser st TYPE -> AParser st TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
         do AParser st Token
forall st. CharParser st Token
Lexer.oParenT
            TYPE
t <- AParser st TYPE
forall st. AParser st TYPE
typeP
            AParser st Token
forall st. CharParser st Token
Lexer.cParenT
            TYPE -> AParser st TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return TYPE
t

-- parser for terms
termP :: AnnoState.AParser st TERM
termP :: AParser st TERM
termP = do Token
f <- AParser st Token
forall st. AParser st Token
nameP
           do AParser st Token
forall st. CharParser st Token
Lexer.oParenT
              (as :: [TERM]
as, _) <- AParser st TERM
forall st. AParser st TERM
termP AParser st TERM
-> AParser st Token
-> GenParser Char (AnnoState st) ([TERM], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy` AParser st Token
forall st. AParser st Token
AnnoState.anComma
              AParser st Token
forall st. CharParser st Token
Lexer.cParenT
              TERM -> AParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> AParser st TERM) -> TERM -> AParser st TERM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM] -> TERM
Appl (Token -> TERM
Identifier Token
f) [TERM]
as
             AParser st TERM -> AParser st TERM -> AParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TERM -> AParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> TERM
Identifier Token
f)

-- parsers for names
nameP :: AnnoState.AParser st NAME
nameP :: AParser st Token
nameP = CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
Lexer.pToken (CharParser (AnnoState st) String -> AParser st Token)
-> CharParser (AnnoState st) String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ [String]
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
dfolKeys CharParser (AnnoState st) String
forall st. CharParser st String
Lexer.scanAnyWords

namesP :: AnnoState.AParser st [NAME]
namesP :: AParser st [Token]
namesP = (([Token], [Token]) -> [Token])
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
-> AParser st [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Token], [Token]) -> [Token]
forall a b. (a, b) -> a
fst (ParsecT String (AnnoState st) Identity ([Token], [Token])
 -> AParser st [Token])
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
-> AParser st [Token]
forall a b. (a -> b) -> a -> b
$ AParser st Token
forall st. AParser st Token
nameP AParser st Token
-> AParser st Token
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy` AParser st Token
forall st. AParser st Token
AnnoState.anComma

-- parser for variable declarations
varP :: AnnoState.AParser st ([NAME], TYPE)
varP :: AParser st DECL
varP = do [Token]
ns <- AParser st [Token]
forall st. AParser st [Token]
namesP
          String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.colonS
          TYPE
t <- AParser st TYPE
forall st. AParser st TYPE
typeP
          DECL -> AParser st DECL
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token]
ns, TYPE
t)

varsP :: AnnoState.AParser st [([NAME], TYPE)]
varsP :: AParser st [DECL]
varsP = do (vs :: [DECL]
vs, _) <- AParser st DECL
forall st. AParser st DECL
varP AParser st DECL
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([DECL], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy` String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
AnnoState.asKey ";"
           GenParser Char (AnnoState st) Token
forall st. AParser st Token
AnnoState.dotT
           [DECL] -> AParser st [DECL]
forall (m :: * -> *) a. Monad m => a -> m a
return [DECL]
vs

-- parser for all formulas
formulaP :: AnnoState.AParser st FORMULA
formulaP :: AParser st FORMULA
formulaP = AParser st FORMULA
forall st. AParser st FORMULA
forallP
           AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
           AParser st FORMULA
forall st. AParser st FORMULA
existsP
           AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
           AParser st FORMULA
forall st. AParser st FORMULA
formula1P

{- parser for equivalences, implications, conjunctions, disjunctions,
   negations, equalities, atomic formulas, and formulas in parentheses -}
formula1P :: AnnoState.AParser st FORMULA
formula1P :: AParser st FORMULA
formula1P = do FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formula2P
                -- equivalences
               (do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.equivS
                   FORMULA
g <- AParser st FORMULA
forall st. AParser st FORMULA
formula2P
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA -> FORMULA
Equivalence FORMULA
f FORMULA
g)
                AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                -- implications
                do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.implS
                   FORMULA
g <- AParser st FORMULA
forall st. AParser st FORMULA
formula2P
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA -> FORMULA
Implication FORMULA
f FORMULA
g
                AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
f -- all other cases

{- parser for conjunctions, disjunctions, negations, equalities,
   atomic formulas, and formulas in parentheses -}
formula2P :: AnnoState.AParser st FORMULA
formula2P :: AParser st FORMULA
formula2P = do FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formula3P
                -- conjunctions
               (do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lAnd
                   (fs :: [FORMULA]
fs, _) <- AParser st FORMULA
forall st. AParser st FORMULA
formula3P AParser st FORMULA
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy`
                                String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lAnd
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ [FORMULA] -> FORMULA
Conjunction (FORMULA
f FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
fs))
                AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                -- disjunctions
                do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lOr
                   (fs :: [FORMULA]
fs, _) <- AParser st FORMULA
forall st. AParser st FORMULA
formula3P AParser st FORMULA
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy`
                                String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lOr
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ [FORMULA] -> FORMULA
Disjunction (FORMULA
f FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
fs)
                AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
f -- all other cases

{- parser for negations, equalities, atomic formulas,
   and formulas in parentheses -}
formula3P :: AnnoState.AParser st FORMULA
formula3P :: AParser st FORMULA
formula3P = AParser st FORMULA
forall st. AParser st FORMULA
parenFormulaP
            AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            AParser st FORMULA
forall st. AParser st FORMULA
negP
            AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            AParser st FORMULA
forall st. AParser st FORMULA
formula4P
            AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            AParser st FORMULA
forall st. AParser st FORMULA
trueP
            AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
            AParser st FORMULA
forall st. AParser st FORMULA
falseP

-- parser for equalities and predicate formulas
formula4P :: AnnoState.AParser st FORMULA
formula4P :: AParser st FORMULA
formula4P = do TERM
x <- AParser st TERM
forall st. AParser st TERM
termP
                -- equalities
               (do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey "=="
                   TERM
y <- AParser st TERM
forall st. AParser st TERM
termP
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> FORMULA
Equality TERM
x TERM
y)
                AParser st FORMULA -> AParser st FORMULA -> AParser st FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                -- predicates
                FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> FORMULA
Pred TERM
x)

-- parser for formulas enclosed in parentheses
parenFormulaP :: AnnoState.AParser st FORMULA
parenFormulaP :: AParser st FORMULA
parenFormulaP = do CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.oParenT
                   FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formulaP
                   CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.cParenT
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
f

-- parser for forall formulas
forallP :: AnnoState.AParser st FORMULA
forallP :: AParser st FORMULA
forallP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.forallS
             [DECL]
vs <- AParser st [DECL]
forall st. AParser st [DECL]
varsP
             FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formulaP
             FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Forall [DECL]
vs FORMULA
f

-- parser for exists formulas
existsP :: AnnoState.AParser st FORMULA
existsP :: AParser st FORMULA
existsP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.existsS
             [DECL]
vs <- AParser st [DECL]
forall st. AParser st [DECL]
varsP
             FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formulaP
             FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ [DECL] -> FORMULA -> FORMULA
Exists [DECL]
vs FORMULA
f

-- parser for negations
negP :: AnnoState.AParser st FORMULA
negP :: AParser st FORMULA
negP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.negS AParser st Token -> AParser st Token -> AParser st Token
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
AnnoState.asKey String
Keywords.notS
          FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
formula3P
          FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> AParser st FORMULA) -> FORMULA -> AParser st FORMULA
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA
Negation FORMULA
f

-- parser for true
trueP :: AnnoState.AParser st FORMULA
trueP :: AParser st FORMULA
trueP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.trueS
           FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
T

-- parser for false
falseP :: AnnoState.AParser st FORMULA
falseP :: AParser st FORMULA
falseP = do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.falseS
            FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
F

-- parser for symbol items
symbItems :: AnnoState.AParser st SYMB_ITEMS
symbItems :: AParser st SYMB_ITEMS
symbItems = ([Token] -> SYMB_ITEMS)
-> ParsecT String (AnnoState st) Identity [Token]
-> AParser st SYMB_ITEMS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Token] -> SYMB_ITEMS
Symb_items ParsecT String (AnnoState st) Identity [Token]
forall st. AParser st [Token]
namesP

-- parser for symbol map items
symbMapItems :: AnnoState.AParser st SYMB_MAP_ITEMS
symbMapItems :: AParser st SYMB_MAP_ITEMS
symbMapItems = do (xs :: [SYMB_OR_MAP]
xs, _) <- AParser st SYMB_OR_MAP
forall st. AParser st SYMB_OR_MAP
symbOrMap AParser st SYMB_OR_MAP
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([SYMB_OR_MAP], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`Lexer.separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
AnnoState.anComma
                  SYMB_MAP_ITEMS -> AParser st SYMB_MAP_ITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB_MAP_ITEMS -> AParser st SYMB_MAP_ITEMS)
-> SYMB_MAP_ITEMS -> AParser st SYMB_MAP_ITEMS
forall a b. (a -> b) -> a -> b
$ [SYMB_OR_MAP] -> SYMB_MAP_ITEMS
Symb_map_items [SYMB_OR_MAP]
xs

-- parser for symbols or symbol maps
symbOrMap :: AnnoState.AParser st SYMB_OR_MAP
symbOrMap :: AParser st SYMB_OR_MAP
symbOrMap = do Token
s <- AParser st Token
forall st. AParser st Token
nameP
               (do String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.mapsTo
                   Token
t <- AParser st Token
forall st. AParser st Token
nameP
                   SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB_OR_MAP -> AParser st SYMB_OR_MAP)
-> SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ Token -> Token -> SYMB_OR_MAP
Symb_map Token
s Token
t)
                AParser st SYMB_OR_MAP
-> AParser st SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> SYMB_OR_MAP
Symb Token
s)