{- |
Module      :  ./CommonLogic/Parse_KIF.hs
Description :  Parser of the Knowledge Interchange Format
Copyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011, Soeren Schulze 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  s.schulze@uni-bremen.de
Stability   :  provisional
Portability :  portable
-}

module CommonLogic.Parse_KIF 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.Keywords
import Common.Lexer (notFollowedWith)
import Common.Parsec (reserved)
import Common.Token
import Common.GlobalAnnotations (PrefixMap)

import CommonLogic.Lexer_KIF

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

boolop_nary :: [(String, [SENTENCE] -> BOOL_SENT, String)]
boolop_nary :: [(String, [SENTENCE] -> BOOL_SENT, String)]
boolop_nary = [(String
andS, AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction, "conjunction"),
               (String
orS, AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction, "disjunction")]

boolop_binary :: [(String, SENTENCE -> SENTENCE -> BOOL_SENT, String)]
boolop_binary :: [(String, SENTENCE -> SENTENCE -> BOOL_SENT, String)]
boolop_binary = [(String
equivS, ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional, "equivalence"),
                 (String
implS, ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication, "implication")]

boolop_quant :: [(String, QUANT, String)]
boolop_quant :: [(String, QUANT, String)]
boolop_quant = [(String
forallS, QUANT
Universal, "universal quantifier"),
                (String
existsS, QUANT
Existential, "existiantial quantifier")]

parse_keys :: [(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys :: [(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys = [CharParser st (Token, op_t, String)]
-> CharParser st (Token, op_t, String)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([CharParser st (Token, op_t, String)]
 -> CharParser st (Token, op_t, String))
-> ([(String, op_t, String)]
    -> [CharParser st (Token, op_t, String)])
-> [(String, op_t, String)]
-> CharParser st (Token, op_t, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, op_t, String) -> CharParser st (Token, op_t, String))
-> [(String, op_t, String)]
-> [CharParser st (Token, op_t, String)]
forall a b. (a -> b) -> [a] -> [b]
map
             (\ (ident :: String
ident, con :: op_t
con, desc :: String
desc) ->
               (Token -> (Token, op_t, String))
-> ParsecT String st Identity Token
-> CharParser st (Token, op_t, String)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\ ch :: Token
ch -> (Token
ch, op_t
con, String
ident)) (String -> ParsecT String st Identity Token
forall st. String -> CharParser st Token
key String
ident ParsecT String st Identity Token
-> String -> ParsecT String st Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
desc))

logsent :: CharParser st SENTENCE
logsent :: CharParser st SENTENCE
logsent = do Token
ch <- String -> CharParser st Token
forall st. String -> CharParser st Token
key String
notS CharParser st Token -> String -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "negation"
             SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> String -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "sentence after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
notS String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
             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
ch, 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 (ch :: Token
ch, con :: [SENTENCE] -> BOOL_SENT
con, ident :: String
ident) <- [(String, [SENTENCE] -> BOOL_SENT, String)]
-> CharParser st (Token, [SENTENCE] -> BOOL_SENT, String)
forall op_t st.
[(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys [(String, [SENTENCE] -> BOOL_SENT, String)]
boolop_nary
             [SENTENCE]
s <- CharParser st SENTENCE -> ParsecT String 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 ParsecT String st Identity [SENTENCE]
-> String -> ParsecT String st Identity [SENTENCE]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "sentences after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
             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
con [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
ch, [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 (ch :: Token
ch, con :: SENTENCE -> SENTENCE -> BOOL_SENT
con, ident :: String
ident) <- [(String, SENTENCE -> SENTENCE -> BOOL_SENT, String)]
-> CharParser st (Token, SENTENCE -> SENTENCE -> BOOL_SENT, String)
forall op_t st.
[(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys [(String, SENTENCE -> SENTENCE -> BOOL_SENT, String)]
boolop_binary
             SENTENCE
s1 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> String -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "first sentence after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
             SENTENCE
s2 <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> String -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "second sentence after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
             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 -> SENTENCE -> BOOL_SENT
con 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
ch, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s1, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s2]
      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 (ch :: Token
ch, q :: QUANT
q, ident :: String
ident) <- [(String, QUANT, String)] -> CharParser st (Token, QUANT, String)
forall op_t st.
[(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys [(String, QUANT, String)]
boolop_quant
             [NAME_OR_SEQMARK]
vars <- CharParser st [NAME_OR_SEQMARK] -> CharParser st [NAME_OR_SEQMARK]
forall st a. CharParser st a -> CharParser st a
parens (ParsecT String st Identity NAME_OR_SEQMARK
-> CharParser st [NAME_OR_SEQMARK]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ((Token -> NAME_OR_SEQMARK)
-> CharParser st Token
-> ParsecT String st Identity NAME_OR_SEQMARK
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> NAME_OR_SEQMARK
Name (CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
variable)
                                    ParsecT String st Identity NAME_OR_SEQMARK
-> ParsecT String st Identity NAME_OR_SEQMARK
-> ParsecT String st Identity NAME_OR_SEQMARK
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> NAME_OR_SEQMARK)
-> CharParser st Token
-> ParsecT String st Identity NAME_OR_SEQMARK
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> NAME_OR_SEQMARK
SeqMark (CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
rowvar)))
                     CharParser st [NAME_OR_SEQMARK]
-> String -> CharParser st [NAME_OR_SEQMARK]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "quantified variables"
             SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence CharParser st SENTENCE -> String -> CharParser st SENTENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "sentence after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
             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
$ QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
q [NAME_OR_SEQMARK]
vars 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
ch, [NAME_OR_SEQMARK] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [NAME_OR_SEQMARK]
vars, SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s]

plainAtom :: CharParser st ATOM
plainAtom :: CharParser st ATOM
plainAtom = do
  Token
t <- CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String
forall st. CharParser st String
word CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st String
forall st. CharParser st String
variable) CharParser st Token -> String -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "word"
  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 (Token -> TERM
Name_term Token
t) []

atomsent :: CharParser st ATOM -> CharParser st SENTENCE
atomsent :: CharParser st ATOM -> CharParser st SENTENCE
atomsent = (ATOM -> SENTENCE) -> CharParser st ATOM -> CharParser st SENTENCE
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\ a :: ATOM
a -> ATOM -> Range -> SENTENCE
Atom_sent ATOM
a (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
a)

plainsent :: CharParser st SENTENCE
plainsent :: CharParser st SENTENCE
plainsent = CharParser st ATOM -> CharParser st SENTENCE
forall st. CharParser st ATOM -> CharParser st SENTENCE
atomsent CharParser st ATOM
forall st. CharParser st ATOM
plainAtom

parensent :: CharParser st SENTENCE
parensent :: CharParser st SENTENCE
parensent = CharParser st SENTENCE -> CharParser st SENTENCE
forall st a. CharParser st a -> CharParser st a
parens (CharParser st SENTENCE -> CharParser st SENTENCE)
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ CharParser st SENTENCE
forall st. CharParser st SENTENCE
logsent 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
<|> CharParser st SENTENCE
forall st. CharParser st SENTENCE
relsent 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
<|> CharParser st SENTENCE
forall st. CharParser st SENTENCE
eqsent

funterm :: CharParser st TERM
funterm :: CharParser st TERM
funterm = CharParser st TERM -> CharParser st TERM
forall st a. CharParser st a -> CharParser st a
parens CharParser st TERM
forall st. CharParser st TERM
funterm
      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
relword <- CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken ([String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved
               [String
equalS, String
neqS, String
andS, String
orS, String
equivS, String
implS, String
forallS, String
existsS, String
notS]
               (CharParser st String
forall st. CharParser st String
word CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st String
forall st. CharParser st String
variable)) CharParser st Token -> String -> CharParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "funword"
             let nt :: TERM
nt = Token -> TERM
Name_term Token
relword
             [TERM_SEQ]
t <- ParsecT String st Identity TERM_SEQ
-> ParsecT String st Identity [TERM_SEQ]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ((Token -> TERM_SEQ)
-> CharParser st Token -> ParsecT String st Identity TERM_SEQ
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM_SEQ
Seq_marks (CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
rowvar)
                        ParsecT String st Identity TERM_SEQ
-> ParsecT String st Identity TERM_SEQ
-> ParsecT String st Identity TERM_SEQ
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (TERM -> TERM_SEQ)
-> CharParser st TERM -> ParsecT String st Identity TERM_SEQ
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM TERM -> TERM_SEQ
Term_seq CharParser st TERM
forall st. CharParser st TERM
term) ParsecT String st Identity [TERM_SEQ]
-> String -> ParsecT String st Identity [TERM_SEQ]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "arguments"
             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
$ if [TERM_SEQ] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM_SEQ]
t
               then TERM
nt
               else TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
nt [TERM_SEQ]
t
                    ([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
relword, [TERM_SEQ] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [TERM_SEQ]
t])

relsent :: CharParser st SENTENCE
relsent :: CharParser st SENTENCE
relsent = do
  TERM
ft <- CharParser st TERM
forall st. CharParser st TERM
funterm
  let a :: ATOM
a = case TERM
ft of
        p :: TERM
p@(Name_term _) -> TERM -> [TERM_SEQ] -> ATOM
Atom TERM
p []
        Funct_term p :: TERM
p args :: [TERM_SEQ]
args _ -> TERM -> [TERM_SEQ] -> ATOM
Atom TERM
p [TERM_SEQ]
args
        _ -> String -> ATOM
forall a. HasCallStack => String -> a
error "unknown TERM in relsent"
  CharParser st ATOM -> CharParser st SENTENCE
forall st. CharParser st ATOM -> CharParser st SENTENCE
atomsent (CharParser st ATOM -> CharParser st SENTENCE)
-> CharParser st ATOM -> CharParser st SENTENCE
forall a b. (a -> b) -> a -> b
$ ATOM -> CharParser st ATOM
forall (m :: * -> *) a. Monad m => a -> m a
return ATOM
a

neqS :: String
neqS :: String
neqS = "/="

eq_ops :: [(String, SENTENCE -> Id.Range -> SENTENCE, String)]
eq_ops :: [(String, SENTENCE -> Range -> SENTENCE, String)]
eq_ops = [(String
equalS, SENTENCE -> Range -> SENTENCE
forall a b. a -> b -> a
const, "equation"),
          (String
neqS, \ e :: SENTENCE
e rn :: Range
rn -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
e) Range
rn, "inequality")]

eqsent :: CharParser st SENTENCE
eqsent :: CharParser st SENTENCE
eqsent = do
  (ch :: Token
ch, con :: SENTENCE -> Range -> SENTENCE
con, ident :: String
ident) <- [(String, SENTENCE -> Range -> SENTENCE, String)]
-> CharParser st (Token, SENTENCE -> Range -> SENTENCE, String)
forall op_t st.
[(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys [(String, SENTENCE -> Range -> SENTENCE, String)]
eq_ops
  TERM
t1 <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> String -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "term after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
  TERM
t2 <- CharParser st TERM
forall st. CharParser st TERM
term CharParser st TERM -> String -> CharParser st TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "second term after \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
  let rn :: Range
rn = [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
ch, TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t1, TERM -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM
t2]
  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
$ SENTENCE -> Range -> SENTENCE
con (ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation TERM
t1 TERM
t2) Range
rn) Range
rn

term :: CharParser st TERM
term :: CharParser st TERM
term = (Token -> TERM)
-> ParsecT String st Identity Token -> CharParser st TERM
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM
Name_term (CharParser st String -> ParsecT String st Identity Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
variable)
   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
<|> (Token -> TERM)
-> ParsecT String st Identity Token -> CharParser st TERM
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM
Name_term (CharParser st String -> ParsecT String st Identity Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
word)
   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
<|> (Token -> TERM)
-> ParsecT String st Identity Token -> CharParser st TERM
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM
Name_term (CharParser st String -> ParsecT String st Identity Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
quotedString)
   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
<|> (Token -> TERM)
-> ParsecT String st Identity Token -> CharParser st TERM
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> TERM
Name_term (CharParser st String -> ParsecT String st Identity Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser st String
forall st. CharParser st String
number)
   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 -> CharParser st TERM
forall st a. CharParser st a -> CharParser st a
parens (CharParser st TERM
forall st. CharParser st TERM
funterm 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
               SENTENCE
s <- CharParser st SENTENCE
forall st. CharParser st SENTENCE
logsent 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
<|> CharParser st SENTENCE
forall st. CharParser st SENTENCE
eqsent
               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
$ SENTENCE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SENTENCE
s)

sentence :: CharParser st SENTENCE
sentence :: CharParser st SENTENCE
sentence = CharParser st SENTENCE
forall st. CharParser st SENTENCE
parensent 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
<|> CharParser st SENTENCE
forall st. CharParser st SENTENCE
plainsent

topLevelSentence :: CharParser st SENTENCE
topLevelSentence :: CharParser st SENTENCE
topLevelSentence = GenParser Char st ()
-> GenParser Char st Token -> GenParser Char st ()
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
notFollowedWith (() -> GenParser Char st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                   ([GenParser Char st Token] -> GenParser Char st Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> GenParser Char st Token)
-> [String] -> [GenParser Char st Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> GenParser Char st Token
forall st. String -> CharParser st Token
key [String]
terminatingKeywords))
                   GenParser Char st ()
-> CharParser st SENTENCE -> CharParser st SENTENCE
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser st SENTENCE
forall st. CharParser st SENTENCE
sentence

basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec :: PrefixMap -> AParser st BASIC_SPEC
basicSpec _ = do
  ParsecT String (AnnoState st) Identity String
-> ParsecT String (AnnoState st) Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String (AnnoState st) Identity String
forall st. CharParser st String
white
  [SENTENCE]
sentences <- ParsecT String (AnnoState st) Identity SENTENCE
-> ParsecT String (AnnoState st) Identity [SENTENCE]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String (AnnoState st) Identity SENTENCE
forall st. CharParser st SENTENCE
topLevelSentence
  let phrases :: [PHRASE]
phrases = (SENTENCE -> PHRASE) -> [SENTENCE] -> [PHRASE]
forall a b. (a -> b) -> [a] -> [b]
map SENTENCE -> PHRASE
Sentence [SENTENCE]
sentences
  let text :: TEXT
text = [PHRASE] -> Range -> TEXT
Text [PHRASE]
phrases (Range -> TEXT) -> Range -> TEXT
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges ([[Pos]] -> [Pos]) -> [[Pos]] -> [Pos]
forall a b. (a -> b) -> a -> b
$ (PHRASE -> [Pos]) -> [PHRASE] -> [[Pos]]
forall a b. (a -> b) -> [a] -> [b]
map PHRASE -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [PHRASE]
phrases
  let text_meta :: TEXT_META
text_meta = TEXT
-> Maybe IRI -> Maybe (Set Token) -> [PrefixMapping] -> TEXT_META
Text_meta TEXT
text Maybe IRI
forall a. Maybe a
Nothing Maybe (Set Token)
forall a. Maybe a
Nothing []
  let basic_items :: BASIC_ITEMS
basic_items = [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items [TEXT_META -> Annoted TEXT_META
forall a. a -> Annoted a
Annotation.emptyAnno TEXT_META
text_meta]
  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 [BASIC_ITEMS -> Annoted BASIC_ITEMS
forall a. a -> Annoted a
Annotation.emptyAnno BASIC_ITEMS
basic_items]