{- |
Module      :  ./CommonLogic/Parse_CLIF.hs
Description :  Parser of common logic interchange format
Copyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Parser of common logic interchange format
-}

-- Ref. Common Logic ISO/IEC IS 24707:2007(E)

module CommonLogic.Parse_CLIF where

import qualified Common.AnnoState as AnnoState
import qualified Common.AS_Annotation as Annotation
import CommonLogic.AS_CommonLogic as AS
import Common.Id as Id
import Common.IRI
import Common.Lexer as Lexer hiding (oParenT, cParenT, pToken, parens)
import Common.Keywords (colonS, mapsTo)
import Common.GlobalAnnotations (PrefixMap)
import Common.Parsec
import Common.Token

import Data.Either (lefts, rights)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified CommonLogic.Tools as Tools

import CommonLogic.Lexer_CLIF

import Text.ParserCombinators.Parsec as Parsec
import Control.Monad (liftM)

-- | parser for getText
cltext :: PrefixMap -> CharParser st TEXT_META
cltext :: PrefixMap -> CharParser st TEXT_META
cltext pm :: PrefixMap
pm = ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [[Char]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
white ParsecT [Char] st Identity [[Char]]
-> CharParser st TEXT_META -> CharParser st TEXT_META
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token -> GenParser Char st Token)
-> GenParser Char st Token -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clTextKey
    (nt :: TEXT
nt, prfxs :: [PrefixMapping]
prfxs) <- CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
namedtext
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    TEXT_META -> CharParser st TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> CharParser st TEXT_META)
-> TEXT_META -> CharParser st TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT -> [PrefixMapping] -> TEXT_META
tm TEXT
nt [PrefixMapping]
prfxs
  CharParser st TEXT_META
-> CharParser st TEXT_META -> CharParser st TEXT_META
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (t :: TEXT
t, prfxs :: [PrefixMapping]
prfxs) <- CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
text CharParser st (TEXT, [PrefixMapping])
-> [Char] -> CharParser st (TEXT, [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "text"
    TEXT_META -> CharParser st TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> CharParser st TEXT_META)
-> TEXT_META -> CharParser st TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT -> [PrefixMapping] -> TEXT_META
tm TEXT
t [PrefixMapping]
prfxs
  )
  where tm :: TEXT -> [PrefixMapping] -> TEXT_META
        tm :: TEXT -> [PrefixMapping] -> TEXT_META
tm t :: TEXT
t prfxs :: [PrefixMapping]
prfxs = TEXT_META
emptyTextMeta { getText :: TEXT
AS.getText = TEXT
t
                                   , prefix_map :: [PrefixMapping]
prefix_map = PrefixMap -> [PrefixMapping]
forall k a. Map k a -> [(k, a)]
Map.toList PrefixMap
pm [PrefixMapping] -> [PrefixMapping] -> [PrefixMapping]
forall a. [a] -> [a] -> [a]
++ [PrefixMapping]
prfxs
                                   }

namedtext :: CharParser st (TEXT, [PrefixMapping])
namedtext :: CharParser st (TEXT, [PrefixMapping])
namedtext = do
    Token
n <- CharParser st Token
forall st. CharParser st Token
identifier CharParser st Token -> [Char] -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "name after \"cl-text\""
    (t :: TEXT
t, prfxs :: [PrefixMapping]
prfxs) <- (TEXT, [PrefixMapping])
-> CharParser st (TEXT, [PrefixMapping])
-> CharParser st (TEXT, [PrefixMapping])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([PHRASE] -> Range -> TEXT
Text [] Range
nullRange, []) CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
text
    (TEXT, [PrefixMapping]) -> CharParser st (TEXT, [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> TEXT -> Range -> TEXT
Named_text Token
n TEXT
t Range
nullRange, [PrefixMapping]
prfxs)

text :: CharParser st (TEXT, [PrefixMapping])
text :: CharParser st (TEXT, [PrefixMapping])
text = do
    [([PHRASE], [PrefixMapping])]
phrPrfxs <- ParsecT [Char] st Identity ([PHRASE], [PrefixMapping])
-> ParsecT [Char] st Identity [([PHRASE], [PrefixMapping])]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT [Char] st Identity ([PHRASE], [PrefixMapping])
forall st. CharParser st ([PHRASE], [PrefixMapping])
phrase
    let (phr :: [[PHRASE]]
phr, prfxs :: [[PrefixMapping]]
prfxs) = [([PHRASE], [PrefixMapping])] -> ([[PHRASE]], [[PrefixMapping]])
forall a b. [(a, b)] -> ([a], [b])
unzip [([PHRASE], [PrefixMapping])]
phrPrfxs
    (TEXT, [PrefixMapping]) -> CharParser st (TEXT, [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([PHRASE] -> Range -> TEXT
Text ([[PHRASE]] -> [PHRASE]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PHRASE]]
phr) Range
nullRange, [[PrefixMapping]] -> [PrefixMapping]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PrefixMapping]]
prfxs)

{- remove the try
keys set here to prevent try in more complex parser to get the right
error message in ex. the following text -}
phrase :: CharParser st ([PHRASE], [PrefixMapping])
phrase :: CharParser st ([PHRASE], [PrefixMapping])
phrase = ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [[Char]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
white ParsecT [Char] st Identity [[Char]]
-> CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clModuleKey)
    (m :: MODULE
m, prfxs :: [PrefixMapping]
prfxs) <- CharParser st (MODULE, [PrefixMapping])
forall st. CharParser st (MODULE, [PrefixMapping])
pModule
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([MODULE -> PHRASE
Module MODULE
m], [PrefixMapping]
prfxs)
  CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clImportsKey)
    IMPORTATION
i <- CharParser st IMPORTATION
forall st. CharParser st IMPORTATION
importation
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([IMPORTATION -> PHRASE
Importation IMPORTATION
i], [])
  CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clCommentKey)
    [Char]
c <- (ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
quotedstring ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
enclosedname) ParsecT [Char] st Identity [Char]
-> [Char] -> ParsecT [Char] st Identity [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "comment after \"cl-comment\""
    (t :: TEXT
t, prfxs :: [PrefixMapping]
prfxs) <- CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
comment_txt CharParser st (TEXT, [PrefixMapping])
-> [Char] -> CharParser st (TEXT, [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "text after \"cl-comment <comment>\""
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([COMMENT -> TEXT -> Range -> PHRASE
Comment_text ([Char] -> Range -> COMMENT
Comment [Char]
c Range
nullRange) TEXT
t Range
nullRange], [PrefixMapping]
prfxs)
  CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clPrefixKey)
    [PrefixMapping]
pm <- CharParser st [PrefixMapping]
forall st. CharParser st [PrefixMapping]
prefix
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [PrefixMapping]
pm)
  CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "sentence"
    ([PHRASE], [PrefixMapping])
-> CharParser st ([PHRASE], [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SENTENCE -> PHRASE
Sentence SENTENCE
s], [])
  )

prefix :: CharParser st [PrefixMapping]
prefix :: CharParser st [PrefixMapping]
prefix = do
  [Char]
p <- do
      [Char] -> ParsecT [Char] st Identity [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string [Char]
colonS
      [Char] -> ParsecT [Char] st Identity [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
colonS
    ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      [Char]
x <- ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
ncname
      [Char] -> ParsecT [Char] st Identity [Char]
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m [Char]
string [Char]
colonS
      [Char] -> ParsecT [Char] st Identity [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> ParsecT [Char] st Identity [Char])
-> [Char] -> ParsecT [Char] st Identity [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
colonS
  ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [[Char]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
white
  IRI
i <- IRIParser st IRI
forall st. IRIParser st IRI
iriCurie
  ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [[Char]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
white
  [PrefixMapping] -> CharParser st [PrefixMapping]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Char]
p, IRI
i)]

comment_txt :: CharParser st (TEXT, [PrefixMapping])
comment_txt :: CharParser st (TEXT, [PrefixMapping])
comment_txt = CharParser st (TEXT, [PrefixMapping])
-> CharParser st (TEXT, [PrefixMapping])
forall tok st a. GenParser tok st a -> GenParser tok st a
try CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
text CharParser st (TEXT, [PrefixMapping])
-> CharParser st (TEXT, [PrefixMapping])
-> CharParser st (TEXT, [PrefixMapping])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (TEXT, [PrefixMapping]) -> CharParser st (TEXT, [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return ([PHRASE] -> Range -> TEXT
Text [] Range
nullRange, [])

-- | parser for module
pModule :: CharParser st (MODULE, [PrefixMapping])
pModule :: CharParser st (MODULE, [PrefixMapping])
pModule = do
    Token
t <- CharParser st Token
forall st. CharParser st Token
identifier CharParser st Token -> [Char] -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "module name after \"cl-module\""
    (exs :: [Token]
exs, (txt :: TEXT
txt, prfxs :: [PrefixMapping]
prfxs)) <- CharParser st ([Token], (TEXT, [PrefixMapping]))
forall st. CharParser st ([Token], (TEXT, [PrefixMapping]))
pModExcl CharParser st ([Token], (TEXT, [PrefixMapping]))
-> [Char] -> CharParser st ([Token], (TEXT, [PrefixMapping]))
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "text in module"
    case [Token]
exs of
         [] -> (MODULE, [PrefixMapping])
-> CharParser st (MODULE, [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> TEXT -> Range -> MODULE
Mod Token
t TEXT
txt Range
nullRange, [PrefixMapping]
prfxs)
         _ -> (MODULE, [PrefixMapping])
-> CharParser st (MODULE, [PrefixMapping])
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> [Token] -> TEXT -> Range -> MODULE
Mod_ex Token
t [Token]
exs TEXT
txt Range
nullRange, [PrefixMapping]
prfxs)

-- | parser for
pModExcl :: CharParser st ([NAME], (TEXT, [PrefixMapping]))
pModExcl :: CharParser st ([Token], (TEXT, [PrefixMapping]))
pModExcl = ParsecT [Char] st Identity [Char]
-> ParsecT [Char] st Identity [[Char]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity [Char]
forall st. CharParser st [Char]
white ParsecT [Char] st Identity [[Char]]
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (do
    GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st Token
forall st. CharParser st Token
oParenT GenParser Char st Token
-> GenParser Char st Token -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char st Token
forall st. CharParser st Token
clExcludesKey)
    [Token]
exs <- GenParser Char st Token -> ParsecT [Char] st Identity [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many GenParser Char st Token
forall st. CharParser st Token
identifier ParsecT [Char] st Identity [Token]
-> [Char] -> ParsecT [Char] st Identity [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "only names in module-exclusion list"
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    (TEXT, [PrefixMapping])
tp <- CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
text
    ([Token], (TEXT, [PrefixMapping]))
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token]
exs, (TEXT, [PrefixMapping])
tp)
  CharParser st ([Token], (TEXT, [PrefixMapping]))
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (TEXT, [PrefixMapping])
tp <- CharParser st (TEXT, [PrefixMapping])
forall st. CharParser st (TEXT, [PrefixMapping])
text
    ([Token], (TEXT, [PrefixMapping]))
-> CharParser st ([Token], (TEXT, [PrefixMapping]))
forall (m :: * -> *) a. Monad m => a -> m a
return ([], (TEXT, [PrefixMapping])
tp)
  )

importation :: CharParser st IMPORTATION
importation :: CharParser st IMPORTATION
importation = do
     -- clImportsKey
     Token
n <- CharParser st Token
forall st. CharParser st Token
identifier CharParser st Token -> [Char] -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "importation name after \"cl-imports\""
     IMPORTATION -> CharParser st IMPORTATION
forall (m :: * -> *) a. Monad m => a -> m a
return (IMPORTATION -> CharParser st IMPORTATION)
-> IMPORTATION -> CharParser st IMPORTATION
forall a b. (a -> b) -> a -> b
$ Token -> IMPORTATION
Imp_name Token
n

-- | parser for sentences
sentence :: CharParser st SENTENCE
sentence :: CharParser st SENTENCE
sentence = CharParser st SENTENCE -> CharParser st SENTENCE
forall st a. CharParser st a -> CharParser st a
parens (do
    Token
ck <- GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st Token
forall st. CharParser st Token
clCommentKey
    [Char]
c <- (CharParser st [Char]
forall st. CharParser st [Char]
quotedstring CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
enclosedname) CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "comment after \"cl-comment\""
    SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "sentence after \"cl-comment <comment>\""
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ COMMENT -> SENTENCE -> Range -> SENTENCE
Comment_sent ([Char] -> Range -> COMMENT
Comment [Char]
c (Range -> COMMENT) -> Range -> COMMENT
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [Char] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Char]
c) SENTENCE
s
           (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
ck, [Char] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Char]
c, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    TERM
t0 <- GenParser Char st TERM -> GenParser Char st TERM
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st TERM
forall st. CharParser st TERM
rolesetTerm
    [(Token, TERM)]
nts <- ParsecT [Char] st Identity (Token, TERM)
-> ParsecT [Char] st Identity [(Token, TERM)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity (Token, TERM)
forall st. CharParser st (Token, TERM)
rolesetNT
    GenParser Char st Token
forall st. CharParser st Token
cParenT
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ TERM -> [(Token, TERM)] -> SENTENCE
rolesetSentence TERM
t0 [(Token, TERM)]
nts
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    ATOM
at <- CharParser st ATOM
forall st. CharParser st ATOM
atom
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ ATOM -> Range -> SENTENCE
Atom_sent ATOM
at (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ ATOM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan ATOM
at
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
andKey
    [SENTENCE]
s <- CharParser st SENTENCE -> ParsecT [Char] st Identity [SENTENCE]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence -- joinRanges with s = []?
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [SENTENCE]
s)
      (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, [SENTENCE] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [SENTENCE]
s]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
orKey
    [SENTENCE]
s <- CharParser st SENTENCE -> ParsecT [Char] st Identity [SENTENCE]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction [SENTENCE]
s)
      (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, [SENTENCE] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [SENTENCE]
s]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
notKey
    SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "sentence after \"not\""
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
s) (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c,
               SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st Token
forall st. CharParser st Token
iffKey
    SENTENCE
s1 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "sentence after \"iff\""
    SENTENCE
s2 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "second sentence after \"iff\""
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional SENTENCE
s1 SENTENCE
s2)
      (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s1, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s1]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
ifKey
    SENTENCE
s1 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "sentence after \"if\""
    SENTENCE
s2 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> [Char] -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "second sentence after \"if\""
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication SENTENCE
s1 SENTENCE
s2)
      (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s1, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s1]
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
forallKey
    Bool -> Token -> CharParser st SENTENCE
forall st. Bool -> Token -> CharParser st SENTENCE
quantsent1 Bool
True Token
c
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token
forall st. CharParser st Token
existsKey
    Bool -> Token -> CharParser st SENTENCE
forall st. Bool -> Token -> CharParser st SENTENCE
quantsent1 Bool
False Token
c
  )

quantsent1 :: Bool -> Token -> CharParser st SENTENCE
quantsent1 :: Bool -> Token -> CharParser st SENTENCE
quantsent1 t :: Bool
t c :: Token
c = do
    Token
g <- CharParser st Token
forall st. CharParser st Token
identifier CharParser st Token -> [Char] -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "predicate after quantifier"
    Bool -> Token -> Maybe Token -> CharParser st SENTENCE
forall st. Bool -> Token -> Maybe Token -> CharParser st SENTENCE
quantsent2 Bool
t Token
c (Maybe Token -> CharParser st SENTENCE)
-> Maybe Token -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ Token -> Maybe Token
forall a. a -> Maybe a
Just Token
g -- Quant_sent using syntactic sugar
  CharParser st SENTENCE
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    Bool -> Token -> Maybe Token -> CharParser st SENTENCE
forall st. Bool -> Token -> Maybe Token -> CharParser st SENTENCE
quantsent2 Bool
t Token
c Maybe Token
forall a. Maybe a
Nothing -- normal Quant_sent

quantsent2 :: Bool -> Token -> Maybe NAME -> CharParser st SENTENCE
quantsent2 :: Bool -> Token -> Maybe Token -> CharParser st SENTENCE
quantsent2 t :: Bool
t c :: Token
c mg :: Maybe Token
mg = do
    [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
bl <- CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
-> CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
forall st a. CharParser st a -> CharParser st a
parens CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
forall st.
CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
boundlist
    SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence
    SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (SENTENCE -> CharParser st SENTENCE)
-> SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ Bool
-> Maybe Token
-> [NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)]
-> SENTENCE
-> Range
-> SENTENCE
quantsent3 Bool
t Maybe Token
mg ([Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
-> [NAME_OR_SEQMARK]
forall a b. [Either a b] -> [b]
rights [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
bl) ([Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)]
forall a b. [Either a b] -> [a]
lefts [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
bl) SENTENCE
s
           (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s]

quantsent3 :: Bool -> Maybe NAME -> [NAME_OR_SEQMARK]
                   -> [(NAME_OR_SEQMARK, TERM)] -> SENTENCE -> Range -> SENTENCE
quantsent3 :: Bool
-> Maybe Token
-> [NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)]
-> SENTENCE
-> Range
-> SENTENCE
quantsent3 t :: Bool
t mg :: Maybe Token
mg bs :: [NAME_OR_SEQMARK]
bs ((n :: NAME_OR_SEQMARK
n, trm :: TERM
trm) : nts :: [(NAME_OR_SEQMARK, TERM)]
nts) s :: SENTENCE
s rn :: Range
rn = -- Quant_sent using syntactic sugar
  let functerm :: ATOM
functerm = case NAME_OR_SEQMARK
n of
       Name nm :: Token
nm -> TERM -> [TERM_SEQ] -> ATOM
Atom (TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
trm [TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
nm] Range
nullRange) []
       SeqMark sqm :: Token
sqm -> TERM -> [TERM_SEQ] -> ATOM
Atom (TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
trm [Token -> TERM_SEQ
Seq_marks Token
sqm] Range
nullRange) []
  in if Bool
t
        then QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [NAME_OR_SEQMARK
n] (Bool
-> Maybe Token
-> [NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)]
-> SENTENCE
-> Range
-> SENTENCE
quantsent3 Bool
t Maybe Token
mg [NAME_OR_SEQMARK]
bs [(NAME_OR_SEQMARK, TERM)]
nts (
                  BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication (ATOM -> Range -> SENTENCE
Atom_sent ATOM
functerm Range
rn) SENTENCE
s) Range
rn
                ) Range
rn) Range
rn
        else QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [NAME_OR_SEQMARK
n] (Bool
-> Maybe Token
-> [NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)]
-> SENTENCE
-> Range
-> SENTENCE
quantsent3 Bool
t Maybe Token
mg [NAME_OR_SEQMARK]
bs [(NAME_OR_SEQMARK, TERM)]
nts (
                  BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction [ATOM -> Range -> SENTENCE
Atom_sent ATOM
functerm Range
rn, SENTENCE
s]) Range
rn
                ) Range
rn) Range
rn
quantsent3 t :: Bool
t mg :: Maybe Token
mg bs :: [NAME_OR_SEQMARK]
bs [] s :: SENTENCE
s rn :: Range
rn =
  let quantType :: QUANT
quantType = if Bool
t then QUANT
Universal else QUANT
Existential
  in case Maybe Token
mg of
    Nothing -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
quantType [NAME_OR_SEQMARK]
bs SENTENCE
s Range
rn -- normal Quant_sent
    Just g :: Token
g ->                                -- Quant_sent using syntactic sugar
      let functerm :: ATOM
functerm = TERM -> [TERM_SEQ] -> ATOM
Atom (TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term (Token -> TERM
Name_term Token
g) ((Token -> TERM_SEQ) -> [Token] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> (Token -> TERM) -> Token -> TERM_SEQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> TERM
Name_term)
                      ([Token] -> [TERM_SEQ]) -> [Token] -> [TERM_SEQ]
forall a b. (a -> b) -> a -> b
$ Set Token -> [Token]
forall a. Set a -> [a]
Set.elems (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ SENTENCE -> Set Token
Tools.indvC_sen SENTENCE
s) Range
nullRange) []
      in if Bool
t
          then QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [NAME_OR_SEQMARK]
bs (BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication
              (ATOM -> Range -> SENTENCE
Atom_sent ATOM
functerm Range
nullRange) SENTENCE
s) Range
rn) Range
rn
          else
            QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Existential [NAME_OR_SEQMARK]
bs (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction
              [ATOM -> Range -> SENTENCE
Atom_sent ATOM
functerm Range
nullRange, SENTENCE
s]) Range
rn) Range
rn

boundlist :: CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
boundlist :: CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
boundlist = ParsecT
  [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
-> CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (do
    NAME_OR_SEQMARK
nos <- CharParser st NAME_OR_SEQMARK
forall st. CharParser st NAME_OR_SEQMARK
intNameOrSeqMark
    Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
 -> ParsecT
      [Char]
      st
      Identity
      (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK))
-> Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall a b. (a -> b) -> a -> b
$ NAME_OR_SEQMARK -> Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
forall a b. b -> Either a b
Right NAME_OR_SEQMARK
nos
  ParsecT
  [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT
  [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall st a. CharParser st a -> CharParser st a
parens (do
    NAME_OR_SEQMARK
nos <- CharParser st NAME_OR_SEQMARK
forall st. CharParser st NAME_OR_SEQMARK
intNameOrSeqMark
    TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term
    Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
 -> ParsecT
      [Char]
      st
      Identity
      (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK))
-> Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
-> ParsecT
     [Char] st Identity (Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK)
forall a b. (a -> b) -> a -> b
$ (NAME_OR_SEQMARK, TERM)
-> Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK
forall a b. a -> Either a b
Left (NAME_OR_SEQMARK
nos, TERM
t)
    )
  )

atom :: CharParser st ATOM
atom :: CharParser st ATOM
atom = do
    CharParser st Token
forall st. CharParser st Token
clEqualsKey
    TERM
t1 <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> [Char] -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "term after \"=\""
    TERM
t2 <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> [Char] -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "second term after \"=\""
    ATOM -> CharParser st ATOM
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOM -> CharParser st ATOM) -> ATOM -> CharParser st ATOM
forall a b. (a -> b) -> a -> b
$ TERM -> TERM -> ATOM
Equation TERM
t1 TERM
t2
  CharParser st ATOM -> CharParser st ATOM -> CharParser st ATOM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> [Char] -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "term"
    [TERM_SEQ]
ts <- ParsecT [Char] st Identity TERM_SEQ
-> ParsecT [Char] st Identity [TERM_SEQ]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity TERM_SEQ
forall st. CharParser st TERM_SEQ
termseq
    ATOM -> CharParser st ATOM
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOM -> CharParser st ATOM) -> ATOM -> CharParser st ATOM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> ATOM
Atom TERM
t [TERM_SEQ]
ts

term :: CharParser st TERM
term :: CharParser st TERM
term = do
     Token
t <- CharParser st Token
forall st. CharParser st Token
identifier
     TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> CharParser st TERM) -> TERM -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
t
   CharParser st TERM -> CharParser st TERM -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st TERM
forall st. CharParser st TERM
term_fun_cmt

term_fun_cmt :: CharParser st TERM
term_fun_cmt :: CharParser st TERM
term_fun_cmt = CharParser st TERM -> CharParser st TERM
forall st a. CharParser st a -> CharParser st a
parens (do
    Token
ck <- GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st Token
forall st. CharParser st Token
clCommentKey
    [Char]
c <- (CharParser st [Char]
forall st. CharParser st [Char]
quotedstring CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
enclosedname) CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "comment after \"cl-comment\""
    TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> [Char] -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "term after \"cl-comment <comment>\""
    TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> CharParser st TERM) -> TERM -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ TERM -> COMMENT -> Range -> TERM
Comment_term TERM
t ([Char] -> Range -> COMMENT
Comment [Char]
c (Range -> COMMENT) -> Range -> COMMENT
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [Char] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Char]
c)
           (Range -> TERM) -> Range -> TERM
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
ck, [Char] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Char]
c, TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t]
  CharParser st TERM -> CharParser st TERM -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- GenParser Char st Token -> GenParser Char st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char st Token
forall st. CharParser st Token
thatKey
    SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence
    TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> CharParser st TERM) -> TERM -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ SENTENCE -> Range -> TERM
That_term SENTENCE
s (Range -> TERM) -> Range -> TERM
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Token -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Token
c, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s]
  CharParser st TERM -> CharParser st TERM -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    TERM
t <- (Token -> TERM) -> GenParser Char st Token -> CharParser st TERM
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM
Name_term (GenParser Char st Token -> CharParser st TERM)
-> GenParser Char st Token -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ CharParser st [Char] -> GenParser Char st Token
forall st. CharParser st [Char] -> CharParser st Token
pToken CharParser st [Char]
forall st. CharParser st [Char]
quotedstring
    TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> CharParser st TERM) -> TERM -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
t [] (Range -> TERM) -> Range -> TERM
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t
  CharParser st TERM -> CharParser st TERM -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term
    [TERM_SEQ]
ts <- ParsecT [Char] st Identity TERM_SEQ
-> ParsecT [Char] st Identity [TERM_SEQ]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity TERM_SEQ
forall st. CharParser st TERM_SEQ
termseq
    TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM -> CharParser st TERM) -> TERM -> CharParser st TERM
forall a b. (a -> b) -> a -> b
$ TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
t [TERM_SEQ]
ts (Range -> TERM) -> Range -> TERM
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t, [TERM_SEQ] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [TERM_SEQ]
ts]
 )

termseq :: CharParser st TERM_SEQ
termseq :: CharParser st TERM_SEQ
termseq = do
   Token
x <- CharParser st Token
forall st. CharParser st Token
seqmark
   TERM_SEQ -> CharParser st TERM_SEQ
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM_SEQ -> CharParser st TERM_SEQ)
-> TERM_SEQ -> CharParser st TERM_SEQ
forall a b. (a -> b) -> a -> b
$ Token -> TERM_SEQ
Seq_marks Token
x
  CharParser st TERM_SEQ
-> CharParser st TERM_SEQ -> CharParser st TERM_SEQ
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
   TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term
   TERM_SEQ -> CharParser st TERM_SEQ
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM_SEQ -> CharParser st TERM_SEQ)
-> TERM_SEQ -> CharParser st TERM_SEQ
forall a b. (a -> b) -> a -> b
$ TERM -> TERM_SEQ
Term_seq TERM
t
  CharParser st TERM_SEQ -> [Char] -> CharParser st TERM_SEQ
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "term or sequence marker in term sequence"

rolesetTerm :: CharParser st TERM
rolesetTerm :: CharParser st TERM
rolesetTerm = do
  TERM
t0 <- CharParser st TERM
forall st. CharParser st TERM
term
  CharParser st Token
forall st. CharParser st Token
oParenT
  CharParser st Token
forall st. CharParser st Token
clRolesetKey
  TERM -> CharParser st TERM
forall (m :: * -> *) a. Monad m => a -> m a
return TERM
t0

rolesetNT :: CharParser st (NAME, TERM)
rolesetNT :: CharParser st (Token, TERM)
rolesetNT = CharParser st (Token, TERM) -> CharParser st (Token, TERM)
forall st a. CharParser st a -> CharParser st a
parens (CharParser st (Token, TERM) -> CharParser st (Token, TERM))
-> CharParser st (Token, TERM) -> CharParser st (Token, TERM)
forall a b. (a -> b) -> a -> b
$ do
  Token
n <- CharParser st Token
forall st. CharParser st Token
identifier
  TERM
t <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> [Char] -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "term"
  (Token, TERM) -> CharParser st (Token, TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
n, TERM
t)

rolesetSentence :: TERM -> [(NAME, TERM)] -> SENTENCE
rolesetSentence :: TERM -> [(Token, TERM)] -> SENTENCE
rolesetSentence t0 :: TERM
t0 nts :: [(Token, TERM)]
nts =
  let x :: Token
x = TERM -> [(Token, TERM)] -> Token
rolesetFreeName TERM
t0 [(Token, TERM)]
nts
  in QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Existential [Token -> NAME_OR_SEQMARK
Name Token
x] (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$
          Token -> TERM -> SENTENCE
rolesetAddToTerm Token
x TERM
t0 SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: ((Token, TERM) -> SENTENCE) -> [(Token, TERM)] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> (Token, TERM) -> SENTENCE
rolesetMixTerm Token
x) [(Token, TERM)]
nts
        ) Range
nullRange) (Range -> SENTENCE) -> Range -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t0

rolesetFreeName :: TERM -> [(NAME, TERM)] -> NAME
rolesetFreeName :: TERM -> [(Token, TERM)] -> Token
rolesetFreeName trm :: TERM
trm nts :: [(Token, TERM)]
nts =
  let usedNames :: Set Token
usedNames = Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union (((Token, TERM) -> Set Token) -> [(Token, TERM)] -> Set Token
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
Tools.setUnion_list
                    (\ (n :: Token
n, t :: TERM
t) -> Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM -> Set Token
Tools.indvC_term TERM
t)
                                           (Token -> Set Token
forall a. a -> Set a
Set.singleton Token
n))
                    [(Token, TERM)]
nts) (TERM -> Set Token
Tools.indvC_term TERM
trm)
  in (Token, Int) -> Token
forall a b. (a, b) -> a
fst ((Token, Int) -> Token) -> (Token, Int) -> Token
forall a b. (a -> b) -> a -> b
$ ([Char], Int) -> Set Token -> (Token, Int)
Tools.freeName ("x", 0) Set Token
usedNames


rolesetAddToTerm :: NAME -> TERM -> SENTENCE
rolesetAddToTerm :: Token -> TERM -> SENTENCE
rolesetAddToTerm x :: Token
x trm :: TERM
trm = ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom TERM
trm [TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
x]) Range
nullRange

rolesetMixTerm :: NAME -> (NAME, TERM) -> SENTENCE
rolesetMixTerm :: Token -> (Token, TERM) -> SENTENCE
rolesetMixTerm x :: Token
x (n :: Token
n, t :: TERM
t) =
  ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (Token -> TERM
Name_term Token
n) [TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ Token -> TERM
Name_term Token
x, TERM -> TERM_SEQ
Term_seq TERM
t]) Range
nullRange

symbIdentifier :: CharParser st Token
symbIdentifier :: CharParser st Token
symbIdentifier =
  CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
pToken ([[Char]] -> CharParser st [Char] -> CharParser st [Char]
forall st. [[Char]] -> CharParser st [Char] -> CharParser st [Char]
reserved ([[Char]]
reservedelement [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
casl_reserved_words) CharParser st [Char]
forall st. CharParser st [Char]
scanClSymbol)
  CharParser st Token -> [Char] -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "symbol"

scanClSymbol :: CharParser st String
scanClSymbol :: CharParser st [Char]
scanClSymbol = CharParser st [Char]
forall st. CharParser st [Char]
quotedstring CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st [Char]
forall st. CharParser st [Char]
enclosedname CharParser st [Char]
-> CharParser st [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
 ((Char -> Bool) -> ParsecT [Char] st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (\ c :: Char
c -> Char -> Bool
clLetters Char
c Bool -> Bool -> Bool
&& Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Char
c "%{}[],;=")
  ParsecT [Char] st Identity Char
-> CharParser st [Char] -> CharParser st [Char]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> ParsecT [Char] st Identity Char -> CharParser st [Char]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT [Char] st Identity Char
forall st. CharParser st Char
clLetter CharParser st [Char] -> [Char] -> CharParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> [Char] -> ParsecT s u m a
<?> "words")

intNameOrSeqMark :: CharParser st NAME_OR_SEQMARK
intNameOrSeqMark :: CharParser st NAME_OR_SEQMARK
intNameOrSeqMark = do
    Token
s <- CharParser st Token
forall st. CharParser st Token
seqmark -- fix seqmark parser for one
    NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK
forall (m :: * -> *) a. Monad m => a -> m a
return (NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK)
-> NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ Token -> NAME_OR_SEQMARK
SeqMark Token
s
  CharParser st NAME_OR_SEQMARK
-> CharParser st NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
n <- CharParser st Token
forall st. CharParser st Token
symbIdentifier
    NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK
forall (m :: * -> *) a. Monad m => a -> m a
return (NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK)
-> NAME_OR_SEQMARK -> CharParser st NAME_OR_SEQMARK
forall a b. (a -> b) -> a -> b
$ Token -> NAME_OR_SEQMARK
Name Token
n

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

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

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

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

-- | parsing one symbol or a mapping of one to a second symbol
symbMap :: GenParser Char st SYMB_OR_MAP
symbMap :: GenParser Char st SYMB_OR_MAP
symbMap = GenParser Char st SYMB_OR_MAP
forall st. GenParser Char st SYMB_OR_MAP
symbMapS GenParser Char st SYMB_OR_MAP
-> GenParser Char st SYMB_OR_MAP -> GenParser Char st SYMB_OR_MAP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char st SYMB_OR_MAP
forall st. GenParser Char st SYMB_OR_MAP
symbMapN

symbMapS :: GenParser Char st SYMB_OR_MAP
symbMapS :: GenParser Char st SYMB_OR_MAP
symbMapS = do
  Token
s <- CharParser st Token
forall st. CharParser st Token
seqmark
  do Token
f <- CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
pToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
toKey [Char]
mapsTo
     Token
t <- CharParser st Token
forall st. CharParser st Token
seqmark
     SYMB_OR_MAP -> GenParser Char st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Token -> Range -> SYMB_OR_MAP
Symb_mapS Token
s Token
t (Range -> SYMB_OR_MAP) -> Range -> SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
f)
   GenParser Char st SYMB_OR_MAP
-> GenParser Char st SYMB_OR_MAP -> GenParser Char 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 -> GenParser Char st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (NAME_OR_SEQMARK -> SYMB_OR_MAP
Symb (NAME_OR_SEQMARK -> SYMB_OR_MAP) -> NAME_OR_SEQMARK -> SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ Token -> NAME_OR_SEQMARK
SeqMark Token
s)

symbMapN :: GenParser Char st SYMB_OR_MAP
symbMapN :: GenParser Char st SYMB_OR_MAP
symbMapN = do
  Token
s <- CharParser st Token
forall st. CharParser st Token
symbIdentifier
  do Token
f <- CharParser st [Char] -> CharParser st Token
forall st. CharParser st [Char] -> CharParser st Token
pToken (CharParser st [Char] -> CharParser st Token)
-> CharParser st [Char] -> CharParser st Token
forall a b. (a -> b) -> a -> b
$ [Char] -> CharParser st [Char]
forall st. [Char] -> CharParser st [Char]
toKey [Char]
mapsTo
     Token
t <- CharParser st Token
forall st. CharParser st Token
symbIdentifier
     SYMB_OR_MAP -> GenParser Char st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Token -> Range -> SYMB_OR_MAP
Symb_mapN Token
s Token
t (Range -> SYMB_OR_MAP) -> Range -> SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
f)
   GenParser Char st SYMB_OR_MAP
-> GenParser Char st SYMB_OR_MAP -> GenParser Char 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 -> GenParser Char st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (NAME_OR_SEQMARK -> SYMB_OR_MAP
Symb (NAME_OR_SEQMARK -> SYMB_OR_MAP) -> NAME_OR_SEQMARK -> SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ Token -> NAME_OR_SEQMARK
Name Token
s)


-- | Toplevel parser for basic specs
basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec :: PrefixMap -> AParser st BASIC_SPEC
basicSpec pm :: PrefixMap
pm = PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
parseAxItems PrefixMap
pm
  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
<|> do
    Annoted BASIC_ITEMS
bi <- AParser st BASIC_ITEMS -> AParser st (Annoted BASIC_ITEMS)
forall st a. AParser st a -> AParser st (Annoted a)
AnnoState.allAnnoParser (AParser st BASIC_ITEMS -> AParser st (Annoted BASIC_ITEMS))
-> AParser st BASIC_ITEMS -> AParser st (Annoted BASIC_ITEMS)
forall a b. (a -> b) -> a -> b
$ PrefixMap -> AParser st BASIC_ITEMS
forall st. PrefixMap -> AParser st BASIC_ITEMS
parseBasicItems PrefixMap
pm
    BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC -> AParser st BASIC_SPEC)
-> BASIC_SPEC -> AParser st BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec [Annoted BASIC_ITEMS
bi]

{- function to parse different syntaxes
parsing: axiom items with dots, clif sentences, clif text
first getting only the sentences -}
parseBasicItems :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
parseBasicItems :: PrefixMap -> AParser st BASIC_ITEMS
parseBasicItems pm :: PrefixMap
pm = AParser st BASIC_ITEMS -> AParser st BASIC_ITEMS
forall tok st a. GenParser tok st a -> GenParser tok st a
try (PrefixMap -> AParser st BASIC_ITEMS
forall st. PrefixMap -> AParser st BASIC_ITEMS
parseSentences PrefixMap
pm)
              AParser st BASIC_ITEMS
-> AParser st BASIC_ITEMS -> AParser st BASIC_ITEMS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PrefixMap -> AParser st BASIC_ITEMS
forall st. PrefixMap -> AParser st BASIC_ITEMS
parseClText PrefixMap
pm
              -- parseClText

parseSentences :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
parseSentences :: PrefixMap -> AParser st BASIC_ITEMS
parseSentences pm :: PrefixMap
pm = do
    [Annoted TEXT_META]
xs <- ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
-> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
 -> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META])
-> ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
-> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META]
forall a b. (a -> b) -> a -> b
$ PrefixMap
-> ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
forall st. PrefixMap -> AParser st (Annoted TEXT_META)
aFormula PrefixMap
pm
    BASIC_ITEMS -> AParser st BASIC_ITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS -> AParser st BASIC_ITEMS)
-> BASIC_ITEMS -> AParser st BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items [Annoted TEXT_META]
xs

-- FIX
parseClText :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
parseClText :: PrefixMap -> AParser st BASIC_ITEMS
parseClText pm :: PrefixMap
pm = do
  TEXT_META
tx <- PrefixMap -> CharParser (AnnoState st) TEXT_META
forall st. PrefixMap -> CharParser st TEXT_META
cltext PrefixMap
pm
  BASIC_ITEMS -> AParser st BASIC_ITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS -> AParser st BASIC_ITEMS)
-> BASIC_ITEMS -> AParser st BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items ([TEXT_META] -> [Annoted TEXT_META]
textToAn [TEXT_META
tx])

textToAn :: [TEXT_META] -> [Annotation.Annoted TEXT_META]
textToAn :: [TEXT_META] -> [Annoted TEXT_META]
textToAn = (TEXT_META -> Annoted TEXT_META)
-> [TEXT_META] -> [Annoted TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map TEXT_META -> Annoted TEXT_META
forall a. a -> Annoted a
Annotation.emptyAnno

-- | parser for Axiom_items
parseAxItems :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
parseAxItems :: PrefixMap -> AParser st BASIC_SPEC
parseAxItems pm :: PrefixMap
pm = do
       Token
d <- AParser st Token
forall st. AParser st Token
AnnoState.dotT
       (fs :: [Annoted BASIC_ITEMS]
fs, ds :: [Token]
ds) <- AParser st BASIC_ITEMS -> AParser st (Annoted BASIC_ITEMS)
forall st a. AParser st a -> AParser st (Annoted a)
AnnoState.allAnnoParser (PrefixMap -> AParser st BASIC_ITEMS
forall st. PrefixMap -> AParser st BASIC_ITEMS
parseAx PrefixMap
pm) AParser st (Annoted BASIC_ITEMS)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted BASIC_ITEMS], [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 BASIC_ITEMS]
ns = [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a. [a] -> [a]
init [Annoted BASIC_ITEMS]
fs [Annoted BASIC_ITEMS]
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEMS -> [Annotation] -> Annoted BASIC_ITEMS
forall a. Annoted a -> [Annotation] -> Annoted a
Annotation.appendAnno ([Annoted BASIC_ITEMS] -> Annoted BASIC_ITEMS
forall a. [a] -> a
last [Annoted BASIC_ITEMS]
fs) [Annotation]
an]
       BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC -> AParser st BASIC_SPEC)
-> BASIC_SPEC -> AParser st BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec [Annoted BASIC_ITEMS]
ns

-- | Toplevel parser for formulae
parseAx :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
parseAx :: PrefixMap -> AParser st BASIC_ITEMS
parseAx pm :: PrefixMap
pm = do
  [Annoted TEXT_META]
t <- ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
-> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
 -> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META])
-> ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
-> ParsecT [Char] (AnnoState st) Identity [Annoted TEXT_META]
forall a b. (a -> b) -> a -> b
$ PrefixMap
-> ParsecT [Char] (AnnoState st) Identity (Annoted TEXT_META)
forall st. PrefixMap -> AParser st (Annoted TEXT_META)
aFormula PrefixMap
pm
  BASIC_ITEMS -> AParser st BASIC_ITEMS
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS -> AParser st BASIC_ITEMS)
-> BASIC_ITEMS -> AParser st BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items [Annoted TEXT_META]
t

-- | Toplevel parser for formulae
aFormula :: PrefixMap -> AnnoState.AParser st (Annotation.Annoted TEXT_META)
aFormula :: PrefixMap -> AParser st (Annoted TEXT_META)
aFormula pm :: PrefixMap
pm = AParser st TEXT_META -> AParser st (Annoted TEXT_META)
forall st a. AParser st a -> AParser st (Annoted a)
AnnoState.allAnnoParser (PrefixMap -> AParser st TEXT_META
forall st. PrefixMap -> CharParser st TEXT_META
cltext PrefixMap
pm)