{- |
Module      :  ./CASL/Formula.hs
Description :  Parser for CASL terms and formulae
Copyright   :  (c) Christian Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

parse terms and formulae
-}

{-
   http://www.cofi.info/Documents/CASL/Summary/
   from 25 March 2001
   C.2.1 Basic Specifications with Subsorts

   remarks:

   when-else-TERMs are non-mixfix,
   because when-else has lowest precedence.
   C.3.1 Precedence

   Sorted (or casted) terms are not directly recognized,
   because "u v : s" may be "u (v:s)" or "(u v):s"

   No term or formula may start with a parenthesized argument list that
   includes commas.

   The arguments of qualified ops or preds can only be given by a following
   parenthesized argument list.

   Braced or bracketed term-lists including commas stem from a possible
   %list-annotation or (for brackets) from compound lists.

   C.6.3 Literal syntax for lists

   `%list b1__b2, c, f'.
   b1 must contain at least one open brace or bracket ("{" or [")
   and all brackets must be balanced in "b1 b2" (the empty list).

   all parsers are paramterized with a String list containing additional
   keywords
-}

module CASL.Formula
    ( term
    , mixTerm
    , primFormula
    , genPrimFormula
    , formula
    , anColon
    , varDecl
    , varDecls
    , opSort
    , opFunSort
    , opType
    , predType
    , predUnitType
    , qualPredName
    , implKey
    , ifKey
    ) where

import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token

import CASL.AS_Basic_CASL

import Text.ParserCombinators.Parsec

simpleTerm :: [String] -> AParser st (TERM f)
simpleTerm :: [String] -> AParser st (TERM f)
simpleTerm k :: [String]
k = (Token -> TERM f)
-> ParsecT String (AnnoState st) Identity Token
-> AParser st (TERM f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> TERM f
forall f. Token -> TERM f
Mixfix_token (ParsecT String (AnnoState st) Identity Token
 -> AParser st (TERM f))
-> ParsecT String (AnnoState st) Identity Token
-> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall st. CharParser st String -> CharParser st Token
pToken
    ( CharParser (AnnoState st) String
forall st. CharParser st String
scanFloat
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanString
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanQuotedChar
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanDotWords
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st. [String] -> CharParser st String -> CharParser st String
reserved ([String]
k [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fwords) CharParser (AnnoState st) String
forall st. CharParser st String
scanAnyWords
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st. [String] -> CharParser st String -> CharParser st String
reserved ([String]
k [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fops) CharParser (AnnoState st) String
forall st. CharParser st String
scanAnySigns
  CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
placeS
  CharParser (AnnoState st) String
-> String -> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "id/literal" )

restTerms :: TermParser f => [String] -> AParser st [TERM f]
restTerms :: [String] -> AParser st [TERM f]
restTerms k :: [String]
k = ([String] -> AParser st ()
forall st. [String] -> AParser st ()
tryItemEnd [String]
startKeyword AParser st () -> AParser st [TERM f] -> AParser st [TERM f]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [TERM f] -> AParser st [TERM f]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  AParser st [TERM f] -> AParser st [TERM f] -> AParser st [TERM f]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
restTerm [String]
k AParser st (TERM f) -> AParser st [TERM f] -> AParser st [TERM f]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> [String] -> AParser st [TERM f]
forall f st. TermParser f => [String] -> AParser st [TERM f]
restTerms [String]
k
  AParser st [TERM f] -> AParser st [TERM f] -> AParser st [TERM f]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [TERM f] -> AParser st [TERM f]
forall (m :: * -> *) a. Monad m => a -> m a
return []

startTerm :: TermParser f => [String] -> AParser st (TERM f)
startTerm :: [String] -> AParser st (TERM f)
startTerm k :: [String]
k =
    AParser st (TERM f)
forall f st. TermParser f => AParser st (TERM f)
parenTerm AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (TERM f)
forall f st. TermParser f => AParser st (TERM f)
braceTerm AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (TERM f)
forall f st. TermParser f => AParser st (TERM f)
bracketTerm AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (TERM f) -> AParser st (TERM f)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st ()
forall st. AParser st ()
addAnnos AParser st () -> AParser st (TERM f) -> AParser st (TERM f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> AParser st (TERM f)
forall st f. [String] -> AParser st (TERM f)
simpleTerm [String]
k)

restTerm :: TermParser f => [String] -> AParser st (TERM f)
restTerm :: [String] -> AParser st (TERM f)
restTerm k :: [String]
k = [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
startTerm [String]
k AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (TERM f)
forall st f. [String] -> AParser st (TERM f)
typedTerm [String]
k AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (TERM f)
forall st f. [String] -> AParser st (TERM f)
castedTerm [String]
k

mixTerm :: TermParser f => [String] -> AParser st (TERM f)
mixTerm :: [String] -> AParser st (TERM f)
mixTerm k :: [String]
k = (f -> TERM f)
-> ParsecT String (AnnoState st) Identity f -> AParser st (TERM f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f -> TERM f
forall f. f -> TERM f
ExtTERM (Bool -> ParsecT String (AnnoState st) Identity f
forall a st. TermParser a => Bool -> AParser st a
termParser Bool
True) AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  [TERM f]
l <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
startTerm [String]
k AParser st (TERM f)
-> ParsecT String (AnnoState st) Identity [TERM f]
-> ParsecT String (AnnoState st) Identity [TERM f]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> [String] -> ParsecT String (AnnoState st) Identity [TERM f]
forall f st. TermParser f => [String] -> AParser st [TERM f]
restTerms [String]
k
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ if [TERM f] -> Bool
forall a. [a] -> Bool
isSingle [TERM f]
l then [TERM f] -> TERM f
forall a. [a] -> a
head [TERM f]
l else [TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term [TERM f]
l

-- | when-else terms
term :: TermParser f => [String] -> AParser st (TERM f)
term :: [String] -> AParser st (TERM f)
term k :: [String]
k = do
  TERM f
t <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
mixTerm [String]
k
  TERM f -> AParser st (TERM f) -> AParser st (TERM f)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option TERM f
t (AParser st (TERM f) -> AParser st (TERM f))
-> AParser st (TERM f) -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ do
    Token
w <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
whenS
    FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
k
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
elseS
    TERM f
r <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k
    TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
t FORMULA f
f TERM f
r (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
w [] Token
e

anColon :: AParser st Token
anColon :: AParser st Token
anColon = AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos AParser st Token
forall st. GenParser Char st Token
colonST

typedTerm :: [String] -> AParser st (TERM f)
typedTerm :: [String] -> AParser st (TERM f)
typedTerm k :: [String]
k = do
  Token
c <- AParser st Token
forall st. AParser st Token
colonT
  Id
t <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ Id -> Range -> TERM f
forall f. Id -> Range -> TERM f
Mixfix_sorted_term Id
t (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c

castedTerm :: [String] -> AParser st (TERM f)
castedTerm :: [String] -> AParser st (TERM f)
castedTerm k :: [String]
k = do
  Token
c <- AParser st Token
forall st. AParser st Token
asT
  Id
t <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ Id -> Range -> TERM f
forall f. Id -> Range -> TERM f
Mixfix_cast Id
t (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c

terms :: TermParser f => [String] -> AParser st ([TERM f], [Token])
terms :: [String] -> AParser st ([TERM f], [Token])
terms k :: [String]
k = [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k AParser st (TERM f)
-> GenParser Char (AnnoState st) Token
-> AParser st ([TERM f], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
anComma

qualVarName :: Token -> AParser st (TERM f)
qualVarName :: Token -> AParser st (TERM f)
qualVarName o :: Token
o = do
  Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
varS
  Token
i <- [String] -> AParser st Token
forall st. [String] -> GenParser Char st Token
varId []
  Token
c <- AParser st Token
forall st. AParser st Token
colonT
  Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [] GenParser Char (AnnoState st) Id
-> ParsecT String (AnnoState st) Identity ()
-> GenParser Char (AnnoState st) Id
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
  Token
p <- AParser st Token
forall st. GenParser Char st Token
cParenT
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ Token -> Id -> Range -> TERM f
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
i Id
s (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token
v, Token
c] Token
p

qualOpName :: Token -> AParser st (TERM f)
qualOpName :: Token -> AParser st (TERM f)
qualOpName = (OP_SYMB -> TERM f)
-> ParsecT String (AnnoState st) Identity OP_SYMB
-> AParser st (TERM f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
`mkAppl` []) (ParsecT String (AnnoState st) Identity OP_SYMB
 -> AParser st (TERM f))
-> (Token -> ParsecT String (AnnoState st) Identity OP_SYMB)
-> Token
-> AParser st (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> ParsecT String (AnnoState st) Identity OP_SYMB
forall st. Token -> AParser st OP_SYMB
qualOpSymb

qualOpSymb :: Token -> AParser st OP_SYMB
qualOpSymb :: Token -> AParser st OP_SYMB
qualOpSymb o :: Token
o = do
  Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
opS
  Id
i <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId []
  Token
c <- AParser st Token
forall st. AParser st Token
anColon
  OP_TYPE
t <- [String] -> AParser st OP_TYPE
forall st. [String] -> AParser st OP_TYPE
opType [] AParser st OP_TYPE
-> ParsecT String (AnnoState st) Identity () -> AParser st OP_TYPE
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
  Token
p <- AParser st Token
forall st. GenParser Char st Token
cParenT
  OP_SYMB -> AParser st OP_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_SYMB -> AParser st OP_SYMB) -> OP_SYMB -> AParser st OP_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
i OP_TYPE
t (Range -> OP_SYMB) -> Range -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token
v, Token
c] Token
p

opSort :: [String] -> GenParser Char st (Bool, Id, Range)
opSort :: [String] -> GenParser Char st (Bool, Id, Range)
opSort k :: [String]
k = (Id -> (Bool, Id, Range))
-> ParsecT String st Identity Id
-> GenParser Char st (Bool, Id, Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ s :: Id
s -> (Bool
False, Id
s, Range
nullRange)) ([String] -> ParsecT String st Identity Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k) GenParser Char st (Bool, Id, Range)
-> GenParser Char st (Bool, Id, Range)
-> GenParser Char st (Bool, Id, Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  Token
q <- GenParser Char st Token
forall st. GenParser Char st Token
quMarkT
  Id
s <- [String] -> ParsecT String st Identity Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k
  (Bool, Id, Range) -> GenParser Char st (Bool, Id, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Id
s, Token -> Range
tokPos Token
q)

opFunSort :: [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE
opFunSort :: [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE
opFunSort k :: [String]
k ts :: [Id]
ts ps :: [Token]
ps = do
  Token
a <- CharParser st String -> CharParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (String -> CharParser st String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
funS)
  (b :: Bool
b, s :: Id
s, qs :: Range
qs) <- [String] -> GenParser Char st (Bool, Id, Range)
forall st. [String] -> GenParser Char st (Bool, Id, Range)
opSort [String]
k
  OP_TYPE -> GenParser Char st OP_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_TYPE -> GenParser Char st OP_TYPE)
-> OP_TYPE -> GenParser Char st OP_TYPE
forall a b. (a -> b) -> a -> b
$ OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type (if Bool
b then OpKind
Partial else OpKind
Total) [Id]
ts Id
s
             (Range -> OP_TYPE) -> Range -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange ([Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
a]) Range
qs

opType :: [String] -> AParser st OP_TYPE
opType :: [String] -> AParser st OP_TYPE
opType k :: [String]
k = do
  (b :: Bool
b, s :: Id
s, p :: Range
p) <- [String] -> GenParser Char (AnnoState st) (Bool, Id, Range)
forall st. [String] -> GenParser Char st (Bool, Id, Range)
opSort [String]
k
  if Bool
b then OP_TYPE -> AParser st OP_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_TYPE -> AParser st OP_TYPE) -> OP_TYPE -> AParser st OP_TYPE
forall a b. (a -> b) -> a -> b
$ OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [] Id
s Range
p else do
      Token
c <- GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
crossT
      (ts :: [Id]
ts, ps :: [Token]
ps) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k GenParser Char (AnnoState st) Id
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
crossT
      [String] -> [Id] -> [Token] -> AParser st OP_TYPE
forall st. [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE
opFunSort [String]
k (Id
s Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
ts) (Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
    AParser st OP_TYPE -> AParser st OP_TYPE -> AParser st OP_TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> [Id] -> [Token] -> AParser st OP_TYPE
forall st. [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE
opFunSort [String]
k [Id
s] []
    AParser st OP_TYPE -> AParser st OP_TYPE -> AParser st OP_TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> OP_TYPE -> AParser st OP_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [] Id
s Range
nullRange)

parenTerm :: TermParser f => AParser st (TERM f)
parenTerm :: AParser st (TERM f)
parenTerm = do
  Token
o <- AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos AParser st Token
forall st. GenParser Char st Token
oParenT
  Token -> AParser st (TERM f)
forall st f. Token -> AParser st (TERM f)
qualVarName Token
o AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Token -> AParser st (TERM f)
forall st f. Token -> AParser st (TERM f)
qualOpName Token
o AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> Token -> AParser st (TERM f)
forall st f. [String] -> Token -> AParser st (TERM f)
qualPredName [] Token
o AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (ts :: [TERM f]
ts, ps :: [Token]
ps) <- [String] -> AParser st ([TERM f], [Token])
forall f st.
TermParser f =>
[String] -> AParser st ([TERM f], [Token])
terms []
    Token
c <- AParser st ()
forall st. AParser st ()
addAnnos AParser st () -> AParser st Token -> AParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Token
forall st. GenParser Char st Token
cParenT
    TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f]
ts (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c)

braceTerm :: TermParser f => AParser st (TERM f)
braceTerm :: AParser st (TERM f)
braceTerm = do
  Token
o <- AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos AParser st Token
forall st. GenParser Char st Token
oBraceT
  (ts :: [TERM f]
ts, ps :: [Token]
ps) <- ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT String (AnnoState st) Identity ([TERM f], [Token])
 -> ParsecT String (AnnoState st) Identity ([TERM f], [Token]))
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall a b. (a -> b) -> a -> b
$ [String]
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall f st.
TermParser f =>
[String] -> AParser st ([TERM f], [Token])
terms []
  Token
c <- AParser st ()
forall st. AParser st ()
addAnnos AParser st () -> AParser st Token -> AParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Token
forall st. GenParser Char st Token
cBraceT
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_braced [TERM f]
ts (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c

bracketTerm :: TermParser f => AParser st (TERM f)
bracketTerm :: AParser st (TERM f)
bracketTerm = do
  Token
o <- AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos AParser st Token
forall st. GenParser Char st Token
oBracketT
  (ts :: [TERM f]
ts, ps :: [Token]
ps) <- ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT String (AnnoState st) Identity ([TERM f], [Token])
 -> ParsecT String (AnnoState st) Identity ([TERM f], [Token]))
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall a b. (a -> b) -> a -> b
$ [String]
-> ParsecT String (AnnoState st) Identity ([TERM f], [Token])
forall f st.
TermParser f =>
[String] -> AParser st ([TERM f], [Token])
terms []
  Token
c <- AParser st ()
forall st. AParser st ()
addAnnos AParser st () -> AParser st Token -> AParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Token
forall st. GenParser Char st Token
cBracketT
  TERM f -> AParser st (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> AParser st (TERM f)) -> TERM f -> AParser st (TERM f)
forall a b. (a -> b) -> a -> b
$ [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_bracketed [TERM f]
ts (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c

quant :: AParser st (QUANTIFIER, Token)
quant :: AParser st (QUANTIFIER, Token)
quant = [AParser st (QUANTIFIER, Token)] -> AParser st (QUANTIFIER, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice (((QUANTIFIER, String) -> AParser st (QUANTIFIER, Token))
-> [(QUANTIFIER, String)] -> [AParser st (QUANTIFIER, Token)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (q :: QUANTIFIER
q, s :: String
s) -> do
    Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
s
    (QUANTIFIER, Token) -> AParser st (QUANTIFIER, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (QUANTIFIER
q, Token
t))
  [ (QUANTIFIER
Unique_existential, String
existsS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
exMark)
  , (QUANTIFIER
Existential, String
existsS)
  , (QUANTIFIER
Universal, String
forallS) ])
  AParser st (QUANTIFIER, Token)
-> String -> AParser st (QUANTIFIER, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "quantifier"

varDecls :: [String] -> AParser st ([VAR_DECL], [Token])
varDecls :: [String] -> AParser st ([VAR_DECL], [Token])
varDecls ks :: [String]
ks = GenParser Char (AnnoState st) VAR_DECL
-> GenParser Char (AnnoState st) Token
-> AParser st ([VAR_DECL], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy ([String] -> GenParser Char (AnnoState st) VAR_DECL
forall st. [String] -> AParser st VAR_DECL
varDecl [String]
ks) GenParser Char (AnnoState st) Token
forall st. AParser st Token
anSemiOrComma

data VarsQualOpOrPred =
    VarDecls [VAR_DECL] [Token]
  | BoundOp OP_NAME OP_TYPE
  | BoundPred PRED_NAME PRED_TYPE

varDeclsOrQual :: [String] -> AParser st VarsQualOpOrPred
varDeclsOrQual :: [String] -> AParser st VarsQualOpOrPred
varDeclsOrQual k :: [String]
k =
  (([VAR_DECL], [Token]) -> VarsQualOpOrPred)
-> ParsecT String (AnnoState st) Identity ([VAR_DECL], [Token])
-> AParser st VarsQualOpOrPred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([VAR_DECL] -> [Token] -> VarsQualOpOrPred)
-> ([VAR_DECL], [Token]) -> VarsQualOpOrPred
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [VAR_DECL] -> [Token] -> VarsQualOpOrPred
VarDecls) ([String]
-> ParsecT String (AnnoState st) Identity ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varDecls [String]
k)
  AParser st VarsQualOpOrPred
-> AParser st VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
o <- CharParser (AnnoState st) Token
forall st. GenParser Char st Token
oParenT
    do Qual_op_name i :: Id
i t :: OP_TYPE
t _ <- Token -> AParser st OP_SYMB
forall st. Token -> AParser st OP_SYMB
qualOpSymb Token
o
       VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall (m :: * -> *) a. Monad m => a -> m a
return (VarsQualOpOrPred -> AParser st VarsQualOpOrPred)
-> VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall a b. (a -> b) -> a -> b
$ Id -> OP_TYPE -> VarsQualOpOrPred
BoundOp Id
i OP_TYPE
t
     AParser st VarsQualOpOrPred
-> AParser st VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
       Qual_pred_name i :: Id
i t :: PRED_TYPE
t _ <- [String] -> Token -> AParser st PRED_SYMB
forall st. [String] -> Token -> AParser st PRED_SYMB
qualPredSymb [String]
k Token
o
       VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall (m :: * -> *) a. Monad m => a -> m a
return (VarsQualOpOrPred -> AParser st VarsQualOpOrPred)
-> VarsQualOpOrPred -> AParser st VarsQualOpOrPred
forall a b. (a -> b) -> a -> b
$ Id -> PRED_TYPE -> VarsQualOpOrPred
BoundPred Id
i PRED_TYPE
t

quantFormula :: TermParser f => [String] -> AParser st (FORMULA f)
quantFormula :: [String] -> AParser st (FORMULA f)
quantFormula k :: [String]
k = do
  (q :: QUANTIFIER
q, p :: Token
p) <- AParser st (QUANTIFIER, Token)
forall st. AParser st (QUANTIFIER, Token)
quant
  VarsQualOpOrPred
vdq <- [String] -> AParser st VarsQualOpOrPred
forall st. [String] -> AParser st VarsQualOpOrPred
varDeclsOrQual [String]
k
  Token
d <- AParser st Token
forall st. AParser st Token
dotT
  FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
k
  FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ case VarsQualOpOrPred
vdq of
    VarDecls vs :: [VAR_DECL]
vs ps :: [Token]
ps -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs FORMULA f
f (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
p [Token]
ps Token
d
    BoundOp o :: Id
o t :: OP_TYPE
t -> Id -> OP_TYPE -> FORMULA f -> FORMULA f
forall f. Id -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp Id
o OP_TYPE
t FORMULA f
f
    BoundPred i :: Id
i t :: PRED_TYPE
t -> Id -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. Id -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred Id
i PRED_TYPE
t FORMULA f
f

varDecl :: [String] -> AParser st VAR_DECL
varDecl :: [String] -> AParser st VAR_DECL
varDecl k :: [String]
k = do
  (vs :: [Token]
vs, ps :: [Token]
ps) <- [String] -> GenParser Char (AnnoState st) Token
forall st. [String] -> GenParser Char st Token
varId [String]
k GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Token], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
anComma
  Token
c <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT
  Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k
  VAR_DECL -> AParser st VAR_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR_DECL -> AParser st VAR_DECL)
-> VAR_DECL -> AParser st VAR_DECL
forall a b. (a -> b) -> a -> b
$ [Token] -> Id -> Range -> VAR_DECL
Var_decl [Token]
vs Id
s ([Token] -> Range
catRange [Token]
ps Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
c)

predType :: [String] -> AParser st PRED_TYPE
predType :: [String] -> AParser st PRED_TYPE
predType k :: [String]
k = do
    (ts :: [Id]
ts, ps :: [Token]
ps) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k GenParser Char (AnnoState st) Id
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
crossT
    PRED_TYPE -> AParser st PRED_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
ts ([Token] -> Range
catRange [Token]
ps))
  AParser st PRED_TYPE
-> AParser st PRED_TYPE -> AParser st PRED_TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st PRED_TYPE
forall st. GenParser Char st PRED_TYPE
predUnitType

predUnitType :: GenParser Char st PRED_TYPE
predUnitType :: GenParser Char st PRED_TYPE
predUnitType = do
  Token
o <- CharParser st Token
forall st. GenParser Char st Token
oParenT
  Token
c <- CharParser st Token
forall st. GenParser Char st Token
cParenT
  PRED_TYPE -> GenParser Char st PRED_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_TYPE -> GenParser Char st PRED_TYPE)
-> PRED_TYPE -> GenParser Char st PRED_TYPE
forall a b. (a -> b) -> a -> b
$ [Id] -> Range -> PRED_TYPE
Pred_type [] (Token -> Range
tokPos Token
o Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
c)

qualPredName :: [String] -> Token -> AParser st (TERM f)
qualPredName :: [String] -> Token -> AParser st (TERM f)
qualPredName k :: [String]
k = (PRED_SYMB -> TERM f)
-> ParsecT String (AnnoState st) Identity PRED_SYMB
-> AParser st (TERM f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PRED_SYMB -> TERM f
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred (ParsecT String (AnnoState st) Identity PRED_SYMB
 -> AParser st (TERM f))
-> (Token -> ParsecT String (AnnoState st) Identity PRED_SYMB)
-> Token
-> AParser st (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String]
-> Token -> ParsecT String (AnnoState st) Identity PRED_SYMB
forall st. [String] -> Token -> AParser st PRED_SYMB
qualPredSymb [String]
k

qualPredSymb :: [String] -> Token -> AParser st PRED_SYMB
qualPredSymb :: [String] -> Token -> AParser st PRED_SYMB
qualPredSymb k :: [String]
k o :: Token
o = do
  Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
predS
  Id
i <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
k
  Token
c <- AParser st Token
forall st. AParser st Token
colonT
  PRED_TYPE
s <- [String] -> AParser st PRED_TYPE
forall st. [String] -> AParser st PRED_TYPE
predType [String]
k AParser st PRED_TYPE
-> ParsecT String (AnnoState st) Identity ()
-> AParser st PRED_TYPE
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
  Token
p <- AParser st Token
forall st. GenParser Char st Token
cParenT
  PRED_SYMB -> AParser st PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_SYMB -> AParser st PRED_SYMB)
-> PRED_SYMB -> AParser st PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
i PRED_TYPE
s (Range -> PRED_SYMB) -> Range -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token
v, Token
c] Token
p

parenFormula :: TermParser f => [String] -> AParser st (FORMULA f)
parenFormula :: [String] -> AParser st (FORMULA f)
parenFormula k :: [String]
k = CharParser (AnnoState st) Token
forall st. GenParser Char st Token
oParenT CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos CharParser (AnnoState st) Token
-> (Token -> AParser st (FORMULA f)) -> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> Token -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> Token -> AParser st (FORMULA f)
clParenFormula [String]
k

clParenFormula :: TermParser f => [String] -> Token -> AParser st (FORMULA f)
clParenFormula :: [String] -> Token -> AParser st (FORMULA f)
clParenFormula k :: [String]
k o :: Token
o = do
      TERM f
q <- [String] -> Token -> AParser st (TERM f)
forall st f. [String] -> Token -> AParser st (TERM f)
qualPredName [] Token
o AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Token -> AParser st (TERM f)
forall st f. Token -> AParser st (TERM f)
qualVarName Token
o AParser st (TERM f) -> AParser st (TERM f) -> AParser st (TERM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Token -> AParser st (TERM f)
forall st f. Token -> AParser st (TERM f)
qualOpName Token
o
      [TERM f]
l <- [String] -> AParser st [TERM f]
forall f st. TermParser f => [String] -> AParser st [TERM f]
restTerms []  -- optional arguments
      [String] -> TERM f -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> TERM f -> AParser st (FORMULA f)
termFormula [String]
k (TERM f -> AParser st (FORMULA f))
-> TERM f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
l then TERM f
q else [TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ TERM f
q TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
: [TERM f]
l
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
k AParser st (FORMULA f)
-> ParsecT String (AnnoState st) Identity ()
-> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
      case FORMULA f
f of
        Mixfix_formula t :: TERM f
t -> do
          Token
c <- CharParser (AnnoState st) Token
forall st. GenParser Char st Token
cParenT
          [TERM f]
l <- [String] -> AParser st [TERM f]
forall f st. TermParser f => [String] -> AParser st [TERM f]
restTerms [String]
k
          let tt :: TERM f
tt = [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f
t] (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c
              ft :: TERM f
ft = if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
l then TERM f
tt else [TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ TERM f
tt TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
: [TERM f]
l
          [String] -> TERM f -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> TERM f -> AParser st (FORMULA f)
termFormula [String]
k TERM f
ft -- commas are not allowed
        _ -> CharParser (AnnoState st) Token
forall st. GenParser Char st Token
cParenT CharParser (AnnoState st) Token
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f

termFormula :: TermParser f => [String] -> TERM f -> AParser st (FORMULA f)
termFormula :: [String] -> TERM f -> AParser st (FORMULA f)
termFormula k :: [String]
k t :: TERM f
t = do
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
exEqual
    TERM f
r <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t Equality
Existl TERM f
r (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> CharParser (AnnoState st) String
forall st. String -> CharParser st String
tryString String
exEqual
    String -> AParser st (FORMULA f)
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected (String -> AParser st (FORMULA f))
-> String -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ "sign following " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
exEqual
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
e <- AParser st Token
forall st. AParser st Token
equalT
    TERM f
r <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t Equality
Strong TERM f
r (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS
    Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
k
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Id -> Range -> FORMULA f
forall f. TERM f -> Id -> Range -> FORMULA f
Membership TERM f
t Id
s (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula TERM f
t)

primFormula :: TermParser f => [String] -> AParser st (FORMULA f)
primFormula :: [String] -> AParser st (FORMULA f)
primFormula = AParser st f -> [String] -> AParser st (FORMULA f)
forall f st.
TermParser f =>
AParser st f -> [String] -> AParser st (FORMULA f)
genPrimFormula (Bool -> AParser st f
forall a st. TermParser a => Bool -> AParser st a
termParser Bool
False)

genPrimFormula :: TermParser f => AParser st f -> [String]
  -> AParser st (FORMULA f)
genPrimFormula :: AParser st f -> [String] -> AParser st (FORMULA f)
genPrimFormula p :: AParser st f
p k :: [String]
k = do
    f
f <- AParser st f
p
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ f -> FORMULA f
forall f. f -> FORMULA f
ExtFORMULA f
f
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primCASLFormula [String]
k

primCASLFormula :: TermParser f => [String] -> AParser st (FORMULA f)
primCASLFormula :: [String] -> AParser st (FORMULA f)
primCASLFormula k :: [String]
k = do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
trueS
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> ([Pos] -> FORMULA f) -> [Pos] -> AParser st (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
True (Range -> FORMULA f) -> ([Pos] -> Range) -> [Pos] -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pos] -> Range
Range ([Pos] -> AParser st (FORMULA f))
-> [Pos] -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> [Pos]
tokenRange Token
c
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
falseS
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> ([Pos] -> FORMULA f) -> [Pos] -> AParser st (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
False (Range -> FORMULA f) -> ([Pos] -> Range) -> [Pos] -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pos] -> Range
Range ([Pos] -> AParser st (FORMULA f))
-> [Pos] -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> [Pos]
tokenRange Token
c
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
defS
    TERM f
t <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> (Range -> FORMULA f) -> Range -> AParser st (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
t (Range -> AParser st (FORMULA f))
-> Range -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
notS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
negS AParser st Token -> String -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "\"not\""
    FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
k
    FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA f
f (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
parenFormula [String]
k
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
quantFormula [String]
k
  AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
k AParser st (TERM f)
-> (TERM f -> AParser st (FORMULA f)) -> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> TERM f -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> TERM f -> AParser st (FORMULA f)
termFormula [String]
k)

andKey :: AParser st Token
andKey :: AParser st Token
andKey = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lAnd

orKey :: AParser st Token
orKey :: AParser st Token
orKey = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lOr

andOrFormula :: TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula :: [String] -> AParser st (FORMULA f)
andOrFormula k :: [String]
k = [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
k AParser st (FORMULA f)
-> (FORMULA f -> AParser st (FORMULA f)) -> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> FORMULA f -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> FORMULA f -> AParser st (FORMULA f)
optAndOr [String]
k

optAndOr :: TermParser f => [String] -> FORMULA f -> AParser st (FORMULA f)
optAndOr :: [String] -> FORMULA f -> AParser st (FORMULA f)
optAndOr k :: [String]
k f :: FORMULA f
f = do
      Token
c <- AParser st Token
forall st. AParser st Token
andKey
      (fs :: [FORMULA f]
fs, ps :: [Token]
ps) <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
k AParser st (FORMULA f)
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA f], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
andKey
      FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con (FORMULA f
f FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
fs) (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Token
c <- AParser st Token
forall st. AParser st Token
orKey
      (fs :: [FORMULA f]
fs, ps :: [Token]
ps) <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
primFormula [String]
k AParser st (FORMULA f)
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA f], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
orKey
      FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis (FORMULA f
f FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
fs) (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f

implKey :: AParser st Token
implKey :: AParser st Token
implKey = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
implS

ifKey :: AParser st Token
ifKey :: AParser st Token
ifKey = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ifS

formula :: TermParser f => [String] -> AParser st (FORMULA f)
formula :: [String] -> AParser st (FORMULA f)
formula k :: [String]
k = [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula [String]
k AParser st (FORMULA f)
-> (FORMULA f -> AParser st (FORMULA f)) -> AParser st (FORMULA f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> FORMULA f -> AParser st (FORMULA f)
forall f st.
TermParser f =>
[String] -> FORMULA f -> AParser st (FORMULA f)
optImplForm [String]
k

optImplForm :: TermParser f => [String] -> FORMULA f -> AParser st (FORMULA f)
optImplForm :: [String] -> FORMULA f -> AParser st (FORMULA f)
optImplForm k :: [String]
k f :: FORMULA f
f = do
      Token
c <- AParser st Token
forall st. AParser st Token
implKey
      (fs :: [FORMULA f]
fs, ps :: [Token]
ps) <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula [String]
k AParser st (FORMULA f)
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA f], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
implKey
      FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Relation -> [FORMULA f] -> [Pos] -> FORMULA f
forall f. Relation -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl Relation
Implication (FORMULA f
f FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
fs) ([Pos] -> FORMULA f) -> [Pos] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Token] -> [Pos]
catPosAux ([Token] -> [Pos]) -> [Token] -> [Pos]
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Token
c <- AParser st Token
forall st. AParser st Token
ifKey
      (fs :: [FORMULA f]
fs, ps :: [Token]
ps) <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula [String]
k AParser st (FORMULA f)
-> AParser st Token
-> GenParser Char (AnnoState st) ([FORMULA f], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
ifKey
      FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [FORMULA f] -> [Pos] -> FORMULA f
forall f. [FORMULA f] -> [Pos] -> FORMULA f
makeIf (FORMULA f
f FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
fs) ([Pos] -> FORMULA f) -> [Pos] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Token] -> [Pos]
catPosAux ([Token] -> [Pos]) -> [Token] -> [Pos]
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
equivS
      FORMULA f
g <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula [String]
k
      FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> AParser st (FORMULA f))
-> FORMULA f -> AParser st (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f Relation
Equivalence FORMULA f
g (Range -> FORMULA f) -> Range -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
    AParser st (FORMULA f)
-> AParser st (FORMULA f) -> AParser st (FORMULA f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> FORMULA f -> AParser st (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f

makeImpl :: Relation -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl :: Relation -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl b :: Relation
b l :: [FORMULA f]
l p :: [Pos]
p = case ([FORMULA f]
l, [Pos]
p) of
  ([f :: FORMULA f
f, g :: FORMULA f
g], _) -> FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f Relation
b FORMULA f
g ([Pos] -> Range
Range [Pos]
p)
  (f :: FORMULA f
f : r :: [FORMULA f]
r, c :: Pos
c : q :: [Pos]
q) -> FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f Relation
b (Relation -> [FORMULA f] -> [Pos] -> FORMULA f
forall f. Relation -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl Relation
b [FORMULA f]
r [Pos]
q) ([Pos] -> Range
Range [Pos
c])
  _ -> String -> FORMULA f
forall a. HasCallStack => String -> a
error "makeImpl got illegal argument"

makeIf :: [FORMULA f] -> [Pos] -> FORMULA f
makeIf :: [FORMULA f] -> [Pos] -> FORMULA f
makeIf l :: [FORMULA f]
l p :: [Pos]
p = Relation -> [FORMULA f] -> [Pos] -> FORMULA f
forall f. Relation -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl Relation
RevImpl ([FORMULA f] -> [FORMULA f]
forall a. [a] -> [a]
reverse [FORMULA f]
l) ([Pos] -> FORMULA f) -> [Pos] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Pos] -> [Pos]
forall a. [a] -> [a]
reverse [Pos]
p