{- |
Module      :  ./QBF/Parse_AS_Basic.hs
Description :  Parser for basic specs
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <jonathan.von_schroeder@dfki.de>
Stability   :  experimental
Portability :  portable

Parser for abstract syntax for propositional logic

  Ref.
  <http://en.wikipedia.org/wiki/Propositional_logic>
-}

module QBF.Parse_AS_Basic
  ( basicSpec                      -- Parser for basic specs
  , symbItems
  , symbMapItems
  ) where

import qualified Common.AnnoState as AnnoState
import qualified Common.AS_Annotation as Annotation
import Common.Id as Id
import Common.Keywords as Keywords
import Common.Lexer as Lexer
import Common.Token
import Common.Parsec
import Common.GlobalAnnotations (PrefixMap)

import QBF.AS_BASIC_QBF as AS_BASIC
import Text.ParserCombinators.Parsec

propKeywords :: [String]
propKeywords :: [String]
propKeywords = [String]
criticalKeywords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
Keywords.propS
  , String
Keywords.notS
  , String
Keywords.trueS
  , String
Keywords.falseS
  , String
Keywords.forallS
  , String
Keywords.existsS ]

-- | Toplevel parser for basic specs
basicSpec :: PrefixMap -> AnnoState.AParser st AS_BASIC.BASICSPEC
basicSpec :: PrefixMap -> AParser st BASICSPEC
basicSpec _ =
  ([Annoted BASICITEMS] -> BASICSPEC)
-> ParsecT String (AnnoState st) Identity [Annoted BASICITEMS]
-> AParser st BASICSPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted BASICITEMS] -> BASICSPEC
AS_BASIC.BasicSpec (AParser st BASICITEMS
-> ParsecT String (AnnoState st) Identity [Annoted BASICITEMS]
forall st a. AParser st a -> AParser st [Annoted a]
AnnoState.annosParser AParser st BASICITEMS
forall st. AParser st BASICITEMS
parseBasicItems)
  AParser st BASICSPEC
-> AParser st BASICSPEC -> AParser st BASICSPEC
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 BASICSPEC -> AParser st BASICSPEC
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BASICSPEC -> AParser st BASICSPEC
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted BASICITEMS] -> BASICSPEC
AS_BASIC.BasicSpec []))

-- | Parser for basic items
parseBasicItems :: AnnoState.AParser st AS_BASIC.BASICITEMS
parseBasicItems :: AParser st BASICITEMS
parseBasicItems = AParser st BASICITEMS
forall st. AParser st BASICITEMS
parsePredDecl AParser st BASICITEMS
-> AParser st BASICITEMS -> AParser st BASICITEMS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BASICITEMS
forall st. AParser st BASICITEMS
parseAxItems

-- | parser for predicate declarations
parsePredDecl :: AnnoState.AParser st AS_BASIC.BASICITEMS
parsePredDecl :: AParser st BASICITEMS
parsePredDecl = (PREDITEM -> BASICITEMS)
-> ParsecT String (AnnoState st) Identity PREDITEM
-> AParser st BASICITEMS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PREDITEM -> BASICITEMS
AS_BASIC.PredDecl ParsecT String (AnnoState st) Identity PREDITEM
forall st. AParser st PREDITEM
predItem

-- | parser for AxiomItems
parseAxItems :: AnnoState.AParser st AS_BASIC.BASICITEMS
parseAxItems :: AParser st BASICITEMS
parseAxItems = do
       Token
d <- AParser st Token
forall st. AParser st Token
AnnoState.dotT
       (fs :: [Annoted FORMULA]
fs, ds :: [Token]
ds) <- AParser st (Annoted FORMULA)
forall st. AParser st (Annoted FORMULA)
aFormula AParser st (Annoted FORMULA)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted FORMULA], [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.dotT
       (_, an :: [Annotation]
an) <- AParser st ([Token], [Annotation])
forall st. AParser st ([Token], [Annotation])
AnnoState.optSemi
       let Range
_ = [Token] -> Range
Id.catRange (Token
d Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ds)
           ns :: [Annoted FORMULA]
ns = [Annoted FORMULA] -> [Annoted FORMULA]
forall a. [a] -> [a]
init [Annoted FORMULA]
fs [Annoted FORMULA] -> [Annoted FORMULA] -> [Annoted FORMULA]
forall a. [a] -> [a] -> [a]
++ [Annoted FORMULA -> [Annotation] -> Annoted FORMULA
forall a. Annoted a -> [Annotation] -> Annoted a
Annotation.appendAnno ([Annoted FORMULA] -> Annoted FORMULA
forall a. [a] -> a
last [Annoted FORMULA]
fs) [Annotation]
an]
       BASICITEMS -> AParser st BASICITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return (BASICITEMS -> AParser st BASICITEMS)
-> BASICITEMS -> AParser st BASICITEMS
forall a b. (a -> b) -> a -> b
$ [Annoted FORMULA] -> BASICITEMS
AS_BASIC.AxiomItems [Annoted FORMULA]
ns

-- | Any word to token
propId :: GenParser Char st Id.Token
propId :: GenParser Char st Token
propId = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
Lexer.pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ [String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
propKeywords CharParser st String
forall st. CharParser st String
Lexer.scanAnyWords

-- | parser for predicates = propositions
predItem :: AnnoState.AParser st AS_BASIC.PREDITEM
predItem :: AParser st PREDITEM
predItem = do
      Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey (String
Keywords.propS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
Keywords.sS) 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.propS
      (ps :: [Token]
ps, cs :: [Token]
cs) <- AParser st Token
forall st. CharParser st Token
propId AParser st Token
-> AParser st Token
-> GenParser Char (AnnoState st) ([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
      PREDITEM -> AParser st PREDITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (PREDITEM -> AParser st PREDITEM)
-> PREDITEM -> AParser st PREDITEM
forall a b. (a -> b) -> a -> b
$ [Token] -> Range -> PREDITEM
AS_BASIC.PredItem [Token]
ps (Range -> PREDITEM) -> Range -> PREDITEM
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
Id.catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
v Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs

-- | Parser for implies @=>@
implKey :: AnnoState.AParser st Id.Token
implKey :: AParser st Token
implKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.implS

-- | Parser for and @\/\ @
andKey :: AnnoState.AParser st Id.Token
andKey :: AParser st Token
andKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lAnd

-- | Parser for or @\\\/@
orKey :: AnnoState.AParser st Id.Token
orKey :: AParser st Token
orKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.lOr

-- | Parser for true
trueKey :: AnnoState.AParser st Id.Token
trueKey :: AParser st Token
trueKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.trueS

-- | Parser for false
falseKey :: AnnoState.AParser st Id.Token
falseKey :: AParser st Token
falseKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.falseS

-- | Parser for not
notKey :: AnnoState.AParser st Id.Token
notKey :: AParser st Token
notKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.notS

-- | Parser for negation
negKey :: AnnoState.AParser st Id.Token
negKey :: AParser st Token
negKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.negS

-- | Parser for equivalence @<=>@
equivKey :: AnnoState.AParser st Id.Token
equivKey :: AParser st Token
equivKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.equivS

-- | Parser for quantifier forall
forallKey :: AnnoState.AParser st Id.Token
forallKey :: AParser st Token
forallKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.forallS

-- | Parser for quantifier forall
existsKey :: AnnoState.AParser st Id.Token
existsKey :: AParser st Token
existsKey = String -> AParser st Token
forall st. String -> AParser st Token
AnnoState.asKey String
Keywords.existsS

-- | Parser for primitive formulae
primFormula :: AnnoState.AParser st AS_BASIC.FORMULA
primFormula :: AParser st FORMULA
primFormula = do
       Token
c <- AParser st Token
forall st. AParser st Token
trueKey
       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
$ Range -> FORMULA
AS_BASIC.TrueAtom (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
Id.tokPos Token
c
    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
<|> do
       Token
c <- AParser st Token
forall st. AParser st Token
falseKey
       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
$ Range -> FORMULA
AS_BASIC.FalseAtom (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
Id.tokPos Token
c
    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
<|> do
       Token
c <- AParser st Token
forall st. AParser st Token
notKey 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
<|> AParser st Token
forall st. AParser st Token
negKey AParser st Token -> String -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "\"not\""
       FORMULA
k <- AParser st FORMULA
forall st. AParser st FORMULA
primFormula
       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 -> Range -> FORMULA
AS_BASIC.Negation FORMULA
k (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
Id.tokPos Token
c
    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
parenFormula
    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
<|> do
           (c :: Token
c, q :: [Token] -> FORMULA -> Range -> FORMULA
q) <- AParser st Token
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token, [Token] -> FORMULA -> Range -> FORMULA)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair AParser st Token
forall st. AParser st Token
forallKey (([Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([Token] -> FORMULA -> Range -> FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return [Token] -> FORMULA -> Range -> FORMULA
AS_BASIC.ForAll)
                 ParsecT
  String
  (AnnoState st)
  Identity
  (Token, [Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token, [Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token, [Token] -> FORMULA -> Range -> FORMULA)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Token
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token, [Token] -> FORMULA -> Range -> FORMULA)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair AParser st Token
forall st. AParser st Token
existsKey (([Token] -> FORMULA -> Range -> FORMULA)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([Token] -> FORMULA -> Range -> FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return [Token] -> FORMULA -> Range -> FORMULA
AS_BASIC.Exists)
           (l :: [Token]
l, _) <- AParser st Token
forall st. CharParser st Token
propId AParser st Token
-> AParser st Token
-> GenParser Char (AnnoState st) ([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
           Token
_ <- AParser st Token
forall st. AParser st Token
AnnoState.dotT
           FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
impFormula
           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
$ if [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then String -> FORMULA
forall a. HasCallStack => String -> a
error "nothing quantified"
                   else [Token] -> FORMULA -> Range -> FORMULA
q [Token]
l FORMULA
f (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
Id.tokPos Token
c
    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
<|> (Token -> FORMULA) -> AParser st Token -> AParser st FORMULA
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> FORMULA
AS_BASIC.Predication AParser st Token
forall st. CharParser st Token
propId

-- | Parser for formulae containing 'and' and 'or'
andOrFormula :: AnnoState.AParser st AS_BASIC.FORMULA
andOrFormula :: AParser st FORMULA
andOrFormula = do
                  FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
primFormula
                  do Token
c <- AParser st Token
forall st. AParser st Token
andKey
                     (fs :: [FORMULA]
fs, ps :: [Token]
ps) <- AParser st FORMULA
forall st. AParser st FORMULA
primFormula 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` AParser st Token
forall st. AParser st Token
andKey
                     FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([FORMULA] -> Range -> FORMULA
AS_BASIC.Conjunction (FORMULA
f FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
fs)
                                        ([Token] -> Range
Id.catRange (Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)))
                    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
<|>
                    do Token
c <- AParser st Token
forall st. AParser st Token
orKey
                       (fs :: [FORMULA]
fs, ps :: [Token]
ps) <- AParser st FORMULA
forall st. AParser st FORMULA
primFormula 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` AParser st Token
forall st. AParser st Token
orKey
                       FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([FORMULA] -> Range -> FORMULA
AS_BASIC.Disjunction (FORMULA
f FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
fs)
                                          ([Token] -> Range
Id.catRange (Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)))
                    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

-- | Parser for formulae with implications
impFormula :: AnnoState.AParser st AS_BASIC.FORMULA
impFormula :: AParser st FORMULA
impFormula = do
                FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
andOrFormula
                do Token
c <- AParser st Token
forall st. AParser st Token
implKey
                   (fs :: [FORMULA]
fs, ps :: [Token]
ps) <- AParser st FORMULA
forall st. AParser st FORMULA
andOrFormula 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` AParser st Token
forall st. AParser st Token
implKey
                   FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([FORMULA] -> [Pos] -> FORMULA
makeImpl (FORMULA
f FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
fs) ([Token] -> [Pos]
Id.catPosAux (Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)))
                  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
<|>
                  do Token
c <- AParser st Token
forall st. AParser st Token
equivKey
                     FORMULA
g <- AParser st FORMULA
forall st. AParser st FORMULA
andOrFormula
                     FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA -> FORMULA -> Range -> FORMULA
AS_BASIC.Equivalence FORMULA
f FORMULA
g (Range -> FORMULA) -> Range -> FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> Range
Id.tokPos Token
c)
                  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
                    where makeImpl :: [FORMULA] -> [Pos] -> FORMULA
makeImpl [f :: FORMULA
f, g :: FORMULA
g] p :: [Pos]
p =
                              FORMULA -> FORMULA -> Range -> FORMULA
AS_BASIC.Implication FORMULA
f FORMULA
g ([Pos] -> Range
Id.Range [Pos]
p)
                          makeImpl (f :: FORMULA
f : r :: [FORMULA]
r) (c :: Pos
c : p :: [Pos]
p) = FORMULA -> FORMULA -> Range -> FORMULA
AS_BASIC.Implication FORMULA
f
                              ([FORMULA] -> [Pos] -> FORMULA
makeImpl [FORMULA]
r [Pos]
p) ([Pos] -> Range
Id.Range [Pos
c])
                          makeImpl _ _ =
                              String -> FORMULA
forall a. HasCallStack => String -> a
error "makeImpl got illegal argument"

-- | Parser for formulae with parentheses
parenFormula :: AnnoState.AParser st AS_BASIC.FORMULA
parenFormula :: AParser st FORMULA
parenFormula = do
       CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.oParenT CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
AnnoState.addAnnos
       FORMULA
f <- AParser st FORMULA
forall st. AParser st FORMULA
impFormula AParser st FORMULA
-> ParsecT String (AnnoState st) Identity () -> AParser st FORMULA
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
AnnoState.addAnnos
       CharParser (AnnoState st) Token
forall st. CharParser st Token
Lexer.cParenT CharParser (AnnoState st) Token
-> AParser st FORMULA -> AParser st FORMULA
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FORMULA -> AParser st FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA
f

-- | Toplevel parser for formulae
aFormula :: AnnoState.AParser st (Annotation.Annoted AS_BASIC.FORMULA)
aFormula :: AParser st (Annoted FORMULA)
aFormula = AParser st FORMULA -> AParser st (Annoted FORMULA)
forall st a. AParser st a -> AParser st (Annoted a)
AnnoState.allAnnoParser AParser st FORMULA
forall st. AParser st FORMULA
impFormula

-- | parsing a prop symbol
symb :: GenParser Char st SYMB
symb :: GenParser Char st SYMB
symb = (Token -> SYMB)
-> ParsecT String st Identity Token -> GenParser Char st SYMB
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> SYMB
SymbId ParsecT String st Identity Token
forall st. CharParser st Token
propId

-- | parsing one symbol or a mapping of one to a second symbol
symbMap :: GenParser Char st SYMBORMAP
symbMap :: GenParser Char st SYMBORMAP
symbMap = do
  SYMB
s <- GenParser Char st SYMB
forall st. GenParser Char st SYMB
symb
  do Token
f <- CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> CharParser st Token)
-> CharParser st String -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
mapsTo
     SYMB
t <- GenParser Char st SYMB
forall st. GenParser Char st SYMB
symb
     SYMBORMAP -> GenParser Char st SYMBORMAP
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB -> SYMB -> Range -> SYMBORMAP
SymbMap SYMB
s SYMB
t (Range -> SYMBORMAP) -> Range -> SYMBORMAP
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
f)
    GenParser Char st SYMBORMAP
-> GenParser Char st SYMBORMAP -> GenParser Char st SYMBORMAP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SYMBORMAP -> GenParser Char st SYMBORMAP
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB -> SYMBORMAP
Symb SYMB
s)

-- | Parse a list of comma separated symbols.
symbItems :: GenParser Char st SYMBITEMS
symbItems :: GenParser Char st SYMBITEMS
symbItems = do
  (is :: [SYMB]
is, ps :: [Token]
ps) <- GenParser Char st ([SYMB], [Token])
forall st. GenParser Char st ([SYMB], [Token])
symbs
  SYMBITEMS -> GenParser Char st SYMBITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return ([SYMB] -> Range -> SYMBITEMS
SymbItems [SYMB]
is (Range -> SYMBITEMS) -> Range -> SYMBITEMS
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps)

-- | parse a comma separated list of symbols
symbs :: GenParser Char st ([SYMB], [Token])
symbs :: GenParser Char st ([SYMB], [Token])
symbs = do
       SYMB
s <- GenParser Char st SYMB
forall st. GenParser Char st SYMB
symb
       do Token
c <- CharParser st Token
forall st. CharParser st Token
commaT CharParser st Token
-> GenParser Char st SYMB -> CharParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` GenParser Char st SYMB
forall st. GenParser Char st SYMB
symb
          (is :: [SYMB]
is, ps :: [Token]
ps) <- GenParser Char st ([SYMB], [Token])
forall st. GenParser Char st ([SYMB], [Token])
symbs
          ([SYMB], [Token]) -> GenParser Char st ([SYMB], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB
s SYMB -> [SYMB] -> [SYMB]
forall a. a -> [a] -> [a]
: [SYMB]
is, Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
         GenParser Char st ([SYMB], [Token])
-> GenParser Char st ([SYMB], [Token])
-> GenParser Char st ([SYMB], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([SYMB], [Token]) -> GenParser Char st ([SYMB], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SYMB
s], [])

-- | parse a list of symbol mappings
symbMapItems :: GenParser Char st SYMBMAPITEMS
symbMapItems :: GenParser Char st SYMBMAPITEMS
symbMapItems = do
  (is :: [SYMBORMAP]
is, ps :: [Token]
ps) <- GenParser Char st ([SYMBORMAP], [Token])
forall st. GenParser Char st ([SYMBORMAP], [Token])
symbMaps
  SYMBMAPITEMS -> GenParser Char st SYMBMAPITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return ([SYMBORMAP] -> Range -> SYMBMAPITEMS
SymbMapItems [SYMBORMAP]
is (Range -> SYMBMAPITEMS) -> Range -> SYMBMAPITEMS
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps)

-- | parse a comma separated list of symbol mappings
symbMaps :: GenParser Char st ([SYMBORMAP], [Token])
symbMaps :: GenParser Char st ([SYMBORMAP], [Token])
symbMaps = do
  SYMBORMAP
s <- GenParser Char st SYMBORMAP
forall st. GenParser Char st SYMBORMAP
symbMap
  do Token
c <- CharParser st Token
forall st. CharParser st Token
commaT CharParser st Token
-> GenParser Char st SYMB -> CharParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` GenParser Char st SYMB
forall st. GenParser Char st SYMB
symb
     (is :: [SYMBORMAP]
is, ps :: [Token]
ps) <- GenParser Char st ([SYMBORMAP], [Token])
forall st. GenParser Char st ([SYMBORMAP], [Token])
symbMaps
     ([SYMBORMAP], [Token]) -> GenParser Char st ([SYMBORMAP], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMBORMAP
s SYMBORMAP -> [SYMBORMAP] -> [SYMBORMAP]
forall a. a -> [a] -> [a]
: [SYMBORMAP]
is, Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
    GenParser Char st ([SYMBORMAP], [Token])
-> GenParser Char st ([SYMBORMAP], [Token])
-> GenParser Char st ([SYMBORMAP], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([SYMBORMAP], [Token]) -> GenParser Char st ([SYMBORMAP], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SYMBORMAP
s], [])