{-# LANGUAGE DeriveFunctor #-}

module Language.Fixpoint.Horn.SMTParse (
    hornP
  , hCstrP
  , hPredP
  , hQualifierP
  , hVarP
  , exprP
  , sortP
) where

import qualified Language.Fixpoint.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon)
import qualified Language.Fixpoint.Types        as F
import qualified Language.Fixpoint.Horn.Types   as H
import           Text.Megaparsec                hiding (State)
import           Text.Megaparsec.Char           (space1, string, char)
import qualified Data.HashMap.Strict            as M
import qualified Data.Text as T
import qualified Text.Megaparsec.Char.Lexer  as L

type FParser = FP.Parser

fAddNumTyCon :: F.Symbol -> FP.Parser ()
fAddNumTyCon :: Symbol -> Parser ()
fAddNumTyCon = Symbol -> Parser ()
FP.addNumTyCon

lexeme :: FParser a -> FParser a
lexeme :: forall a. FParser a -> FParser a
lexeme = Parser () -> ParserV Symbol a -> ParserV Symbol a
forall v a. ParserV v () -> ParserV v a -> ParserV v a
FP.lexeme' Parser ()
spaces

locLexeme :: FP.Parser a -> FP.Parser (F.Located a)
locLexeme :: forall a. Parser a -> Parser (Located a)
locLexeme = Parser () -> ParserV Symbol a -> ParserV Symbol (Located a)
forall v a. ParserV v () -> ParserV v a -> ParserV v (Located a)
FP.locLexeme' Parser ()
spaces

-- | Consumes all whitespace, including LH comments.
--
-- Should not be used directly, but primarily via 'lexeme'.
--
-- The only "valid" use case for spaces is in top-level parsing
-- function, to consume initial spaces.
--
spaces :: FParser ()
spaces :: Parser ()
spaces =
  Parser () -> Parser () -> Parser () -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space
    Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1
    Parser ()
lineComment
    Parser ()
blockComment

lineComment :: FParser ()
lineComment :: Parser ()
lineComment = Tokens [Char] -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment [Char]
Tokens [Char]
";"

blockComment :: FParser ()
blockComment :: Parser ()
blockComment = Tokens [Char] -> Tokens [Char] -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> Tokens s -> m ()
L.skipBlockComment [Char]
Tokens [Char]
"/* " [Char]
Tokens [Char]
"*/"

reserved :: String -> FParser ()
reserved :: [Char] -> Parser ()
reserved = Parser () -> [Char] -> Parser ()
FP.reserved' Parser ()
spaces

reservedOp :: String -> FParser ()
reservedOp :: [Char] -> Parser ()
reservedOp = Parser () -> [Char] -> Parser ()
FP.reservedOp' Parser ()
spaces

sym :: String -> FParser String
sym :: [Char] -> FParser [Char]
sym [Char]
x = FParser [Char] -> FParser [Char]
forall a. FParser a -> FParser a
lexeme (Tokens [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
x)

parens :: FParser a -> FParser a
parens :: forall a. FParser a -> FParser a
parens = FParser [Char]
-> FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> FParser [Char]
sym [Char]
"(") ([Char] -> FParser [Char]
sym [Char]
")")

stringLiteral :: FParser String
stringLiteral :: FParser [Char]
stringLiteral = FParser [Char] -> FParser [Char]
forall a. FParser a -> FParser a
lexeme FParser [Char]
forall v. ParserV v [Char]
FP.stringR FParser [Char] -> [Char] -> FParser [Char]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"string literal"

symbolP :: FParser F.Symbol
symbolP :: FParser Symbol
symbolP = FParser Symbol -> FParser Symbol
forall a. FParser a -> FParser a
lexeme FParser Symbol
forall v. ParserV v Symbol
FP.symbolR FParser Symbol -> [Char] -> FParser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"identifier"

fIntP :: FParser Int
fIntP :: FParser Int
fIntP = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
-> FParser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
natural

natural :: FParser Integer
natural :: StateT (PStateV Symbol) (Parsec Void [Char]) Integer
natural = StateT (PStateV Symbol) (Parsec Void [Char]) Integer
-> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
forall a. FParser a -> FParser a
lexeme StateT (PStateV Symbol) (Parsec Void [Char]) Integer
forall v. ParserV v Integer
FP.naturalR StateT (PStateV Symbol) (Parsec Void [Char]) Integer
-> [Char] -> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"nat literal"

double :: FParser Double
double :: FParser Double
double = FParser Double -> FParser Double
forall a. FParser a -> FParser a
lexeme FParser Double
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, RealFloat a) =>
m a
L.float FParser Double -> [Char] -> FParser Double
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"float literal"


locUpperIdP, locSymbolP :: FParser F.LocSymbol
locUpperIdP :: FParser LocSymbol
locUpperIdP = FParser Symbol -> FParser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme FParser Symbol
forall v. ParserV v Symbol
FP.upperIdR
locSymbolP :: FParser LocSymbol
locSymbolP  = FParser Symbol -> FParser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme FParser Symbol
forall v. ParserV v Symbol
FP.symbolR

upperIdP :: FP.Parser F.Symbol
upperIdP :: FParser Symbol
upperIdP = FParser Symbol -> FParser Symbol
forall a. FParser a -> FParser a
lexeme FParser Symbol
forall v. ParserV v Symbol
FP.upperIdR FParser Symbol -> [Char] -> FParser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"upperIdP"

lowerIdP :: FP.Parser F.Symbol
lowerIdP :: FParser Symbol
lowerIdP = FParser Symbol -> FParser Symbol
forall a. FParser a -> FParser a
lexeme FParser Symbol
forall v. ParserV v Symbol
FP.lowerIdR FParser Symbol -> [Char] -> FParser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"upperIdP"

fTyConP :: FParser F.FTycon
fTyConP :: FParser FTycon
fTyConP
  =   ([Char] -> Parser ()
reserved [Char]
"int"     Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.intFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Integer" Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.intFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Int"     Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.intFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"real"    Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.realFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"bool"    Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.boolFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"num"     Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.numFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Str"     Parser () -> FParser FTycon -> FParser FTycon
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> FParser FTycon
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
F.strFTyCon)
  FParser FTycon -> FParser FTycon -> FParser FTycon
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (LocSymbol -> FParser FTycon
forall v. LocSymbol -> ParserV v FTycon
FP.mkFTycon        (LocSymbol -> FParser FTycon)
-> FParser LocSymbol -> FParser FTycon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<  FParser LocSymbol
locUpperIdP)


fTrueP :: FP.Parser F.Expr
fTrueP :: Parser Expr
fTrueP = [Char] -> Parser ()
reserved [Char]
"true"  Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
F.PTrue

fFalseP :: FP.Parser F.Expr
fFalseP :: Parser Expr
fFalseP = [Char] -> Parser ()
reserved [Char]
"false" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
F.PFalse

fSymconstP :: FP.Parser F.SymConst
fSymconstP :: Parser SymConst
fSymconstP =  Text -> SymConst
F.SL (Text -> SymConst) -> ([Char] -> Text) -> [Char] -> SymConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
T.pack ([Char] -> SymConst) -> FParser [Char] -> Parser SymConst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser [Char]
stringLiteral

-- | Parser for literal numeric constants: floats or integers without sign.
constantP :: FParser F.Constant
constantP :: FParser Constant
constantP =
     FParser Constant -> FParser Constant
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Double -> Constant
F.R (Double -> Constant) -> FParser Double -> FParser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Double
double)   -- float literal
 FParser Constant -> FParser Constant -> FParser Constant
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Constant
F.I (Integer -> Constant)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
-> FParser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Integer
natural        -- nat literal

-------------------------------------------------------------------------------
hornP :: FParser H.TagQuery
-------------------------------------------------------------------------------
hornP :: FParser TagQuery
hornP = do
  Parser ()
spaces
  [HThing Tag]
hThings <- StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [HThing Tag]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
hThingP
  TagQuery -> FParser TagQuery
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([HThing Tag] -> TagQuery
forall a. [HThing a] -> Query a
mkQuery [HThing Tag]
hThings)

mkQuery :: [HThing a] -> H.Query a
mkQuery :: forall a. [HThing a] -> Query a
mkQuery [HThing a]
things = H.Query
  { qQuals :: [Qualifier]
H.qQuals =            [ Qualifier
q     | HQual Qualifier
q  <- [HThing a]
things ]
  , qVars :: [Var a]
H.qVars  =            [ Var a
k     | HVar  Var a
k  <- [HThing a]
things ]
  , qCstr :: Cstr a
H.qCstr  = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
H.CAnd     [ Cstr a
c     | HCstr Cstr a
c  <- [HThing a]
things ]
  , qCon :: HashMap Symbol Sort
H.qCon   = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x,Sort
t) | HCon Symbol
x Sort
t <- [HThing a]
things ]
  , qDis :: HashMap Symbol Sort
H.qDis   = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x,Sort
t) | HDis Symbol
x Sort
t <- [HThing a]
things ]
  , qEqns :: [Equation]
H.qEqns  =            [ Equation
e     | HDef Equation
e   <- [HThing a]
things ]
  , qMats :: [Rewrite]
H.qMats  =            [ Rewrite
m     | HMat Rewrite
m   <- [HThing a]
things ]
  , qData :: [DataDecl]
H.qData  =            [ DataDecl
dd    | HDat DataDecl
dd  <- [HThing a]
things ]
  , qOpts :: [[Char]]
H.qOpts  =            [ [Char]
o     | HOpt [Char]
o   <- [HThing a]
things ]
  , qNums :: [Symbol]
H.qNums  =            [ Symbol
s     | HNum Symbol
s   <- [HThing a]
things ]
  }

-- | A @HThing@ describes the kinds of things we may see, in no particular order
--   in a .smt2 query file.

data HThing a
  = HQual !F.Qualifier
  | HVar  !(H.Var a)
  | HCstr !(H.Cstr a)

  -- for uninterpred functions and ADT constructors
  | HCon  F.Symbol F.Sort
  | HDis  F.Symbol F.Sort
  | HDef  F.Equation
  | HMat  F.Rewrite
  | HDat !F.DataDecl
  | HOpt !String
  | HNum  F.Symbol
  deriving ((forall a b. (a -> b) -> HThing a -> HThing b)
-> (forall a b. a -> HThing b -> HThing a) -> Functor HThing
forall a b. a -> HThing b -> HThing a
forall a b. (a -> b) -> HThing a -> HThing b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> HThing a -> HThing b
fmap :: forall a b. (a -> b) -> HThing a -> HThing b
$c<$ :: forall a b. a -> HThing b -> HThing a
<$ :: forall a b. a -> HThing b -> HThing a
Functor)

hThingP :: FParser (HThing H.Tag)
hThingP :: StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
hThingP  = Parser ()
spaces Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a. FParser a -> FParser a
parens StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
body
  where
    body :: StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
body =  Qualifier -> HThing Tag
forall a. Qualifier -> HThing a
HQual (Qualifier -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"qualif"     Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
-> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
hQualifierP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Cstr Tag -> HThing Tag
forall a. Cstr a -> HThing a
HCstr (Cstr Tag -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"constraint" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
hCstrP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var Tag -> HThing Tag
forall a. Var a -> HThing a
HVar  (Var Tag -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"var"        Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
hVarP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> HThing Tag
forall a. [Char] -> HThing a
HOpt  ([Char] -> HThing Tag)
-> FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"fixpoint"   Parser () -> FParser [Char] -> FParser [Char]
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> FParser [Char]
stringLiteral)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> HThing Tag
forall a. Symbol -> Sort -> HThing a
HCon  (Symbol -> Sort -> HThing Tag)
-> FParser Symbol
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Sort -> HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"constant"   Parser () -> FParser Symbol -> FParser Symbol
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> FParser Symbol
symbolP) StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> HThing Tag
forall a. Symbol -> Sort -> HThing a
HDis  (Symbol -> Sort -> HThing Tag)
-> FParser Symbol
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Sort -> HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"distinct"   Parser () -> FParser Symbol -> FParser Symbol
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> FParser Symbol
symbolP) StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Equation -> HThing Tag
forall a. Equation -> HThing a
HDef  (Equation -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"define"     Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
-> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
defineP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rewrite -> HThing Tag
forall a. Rewrite -> HThing a
HMat  (Rewrite -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"match"      Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
-> StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
matchP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DataDecl -> HThing Tag
forall a. DataDecl -> HThing a
HDat  (DataDecl -> HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"datatype"   Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
-> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
dataDeclP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> HThing Tag
forall a. Symbol -> HThing a
HNum  (Symbol -> HThing Tag)
-> FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"numeric"    Parser () -> FParser Symbol -> FParser Symbol
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> FParser Symbol
numericDeclP)

numericDeclP :: FParser F.Symbol
numericDeclP :: FParser Symbol
numericDeclP = do
  Symbol
x <- LocSymbol -> Symbol
forall a. Located a -> a
F.val (LocSymbol -> Symbol) -> FParser LocSymbol -> FParser Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser LocSymbol
locUpperIdP
  Symbol -> Parser ()
fAddNumTyCon Symbol
x
  Symbol -> FParser Symbol
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbol
x

-------------------------------------------------------------------------------
hCstrP :: FParser (H.Cstr H.Tag)
-------------------------------------------------------------------------------
hCstrP :: StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
hCstrP =  StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a. FParser a -> FParser a
parens StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
body)
      StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Pred -> Tag -> Cstr Tag
forall a. Pred -> a -> Cstr a
H.Head (Pred -> Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
hPredP                            StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag
  where
    body :: StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
body =  [Cstr Tag] -> Cstr Tag
forall a. [Cstr a] -> Cstr a
H.CAnd ([Cstr Tag] -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Cstr Tag]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"and"    Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Cstr Tag]
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Cstr Tag]
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Cstr Tag]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
hCstrP)
        StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind Tag -> Cstr Tag -> Cstr Tag
forall a. Bind a -> Cstr a -> Cstr a
H.All  (Bind Tag -> Cstr Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"forall" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
hBindP)  StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
hCstrP
        StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind Tag -> Cstr Tag -> Cstr Tag
forall a. Bind a -> Cstr a -> Cstr a
H.Any  (Bind Tag -> Cstr Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"exists" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
hBindP)  StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
hCstrP
        StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Pred -> Tag -> Cstr Tag
forall a. Pred -> a -> Cstr a
H.Head (Pred -> Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"tag"    Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
hPredP)  StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Cstr Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Cstr Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Char] -> Tag
H.Tag ([Char] -> Tag)
-> FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser [Char]
stringLiteral)

hBindP :: FParser (H.Bind H.Tag)
hBindP :: StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
hBindP   = StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
forall a. FParser a -> FParser a
parens (StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
 -> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag))
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
forall a b. (a -> b) -> a -> b
$ do
  (Symbol
x, Sort
t) <- FParser (Symbol, Sort)
symSortP
  Symbol -> Sort -> Pred -> Tag -> Bind Tag
forall a. Symbol -> Sort -> Pred -> a -> Bind a
H.Bind Symbol
x Sort
t (Pred -> Tag -> Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Bind Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
hPredP StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Bind Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Bind Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

-------------------------------------------------------------------------------
hPredP :: FParser H.Pred
-------------------------------------------------------------------------------
hPredP :: StateT (PStateV Symbol) (Parsec Void [Char]) Pred
hPredP = StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall a. FParser a -> FParser a
parens StateT (PStateV Symbol) (Parsec Void [Char]) Pred
body
  where
    body :: StateT (PStateV Symbol) (Parsec Void [Char]) Pred
body =  Symbol -> [Symbol] -> Pred
H.Var  (Symbol -> [Symbol] -> Pred)
-> FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) ([Symbol] -> Pred)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Symbol
kvSymP StateT (PStateV Symbol) (Parsec Void [Char]) ([Symbol] -> Pred)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Symbol]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Symbol]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some FParser Symbol
symbolP
        StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Pred] -> Pred
H.PAnd ([Pred] -> Pred)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Pred]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> Parser ()
reserved [Char]
"and" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Pred]
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Pred]
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Pred]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT (PStateV Symbol) (Parsec Void [Char]) Pred
hPredP)
        StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
-> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr -> Pred
H.Reft (Expr -> Pred)
-> Parser Expr -> StateT (PStateV Symbol) (Parsec Void [Char]) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP

kvSymP :: FParser F.Symbol
kvSymP :: FParser Symbol
kvSymP = Token [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'$' StateT (PStateV Symbol) (Parsec Void [Char]) Char
-> FParser Symbol -> FParser Symbol
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> FParser Symbol
symbolP

-------------------------------------------------------------------------------
-- | Qualifiers
-------------------------------------------------------------------------------
hQualifierP :: FParser F.Qualifier
hQualifierP :: StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
hQualifierP = do
  SourcePos
pos    <- StateT (PStateV Symbol) (Parsec Void [Char]) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
  Symbol
n      <- FParser Symbol
upperIdP
  [(Symbol, Sort)]
params <- FParser [(Symbol, Sort)] -> FParser [(Symbol, Sort)]
forall a. FParser a -> FParser a
parens (FParser (Symbol, Sort) -> FParser [(Symbol, Sort)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some FParser (Symbol, Sort)
symSortP)
  Expr
body   <- Parser Expr
exprP
  Qualifier -> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return  (Qualifier
 -> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier)
-> Qualifier
-> StateT (PStateV Symbol) (Parsec Void [Char]) Qualifier
forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
forall v.
Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v
F.mkQual Symbol
n ((Symbol, Sort) -> QualParam
mkParam ((Symbol, Sort) -> QualParam) -> [(Symbol, Sort)] -> [QualParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
params) Expr
body SourcePos
pos

mkParam :: (F.Symbol, F.Sort) -> F.QualParam
mkParam :: (Symbol, Sort) -> QualParam
mkParam (Symbol
x, Sort
t) = Symbol -> QualPattern -> Sort -> QualParam
F.QP Symbol
x QualPattern
F.PatNone Sort
t

-------------------------------------------------------------------------------
-- | Horn Variables
-------------------------------------------------------------------------------

hVarP :: FParser (H.Var H.Tag)
hVarP :: StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
hVarP = Symbol -> [Sort] -> Tag -> Var Tag
forall a. Symbol -> [Sort] -> a -> Var a
H.HVar (Symbol -> [Sort] -> Tag -> Var Tag)
-> FParser Symbol
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Tag -> Var Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Symbol
kvSymP StateT
  (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Tag -> Var Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Var Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
forall a. FParser a -> FParser a
parens (StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP) StateT (PStateV Symbol) (Parsec Void [Char]) (Tag -> Var Tag)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Var Tag)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT (PStateV Symbol) (Parsec Void [Char]) Tag
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

-------------------------------------------------------------------------------
-- | Helpers
-------------------------------------------------------------------------------
sPairP :: FParser a -> FParser b -> FParser (a, b)
sPairP :: forall a b. FParser a -> FParser b -> FParser (a, b)
sPairP FParser a
aP FParser b
bP = FParser (a, b) -> FParser (a, b)
forall a. FParser a -> FParser a
parens ((,) (a -> b -> (a, b))
-> FParser a
-> StateT (PStateV Symbol) (Parsec Void [Char]) (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser a
aP StateT (PStateV Symbol) (Parsec Void [Char]) (b -> (a, b))
-> FParser b -> FParser (a, b)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FParser b
bP)

sMany :: FParser a -> FParser [a]
sMany :: forall a. FParser a -> FParser [a]
sMany FParser a
p = FParser [a] -> FParser [a]
forall a. FParser a -> FParser a
parens (FParser a -> FParser [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many FParser a
p)


symSortP :: FParser (F.Symbol, F.Sort)
symSortP :: FParser (Symbol, Sort)
symSortP = FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> FParser (Symbol, Sort)
forall a b. FParser a -> FParser b -> FParser (a, b)
sPairP  FParser Symbol
symbolP StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP
-- symSortP = fParens ((,) <$> fSymbolP <*> sortP)

dataDeclP :: FParser F.DataDecl
dataDeclP :: StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
dataDeclP = do
  (FTycon
tc, Int
n) <- FParser FTycon -> FParser Int -> FParser (FTycon, Int)
forall a b. FParser a -> FParser b -> FParser (a, b)
sPairP FParser FTycon
fTyConP FParser Int
fIntP
  [DataCtor]
ctors   <- FParser DataCtor -> FParser [DataCtor]
forall a. FParser a -> FParser [a]
sMany FParser DataCtor
dataCtorP
  DataDecl -> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure     (DataDecl -> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl)
-> DataDecl
-> StateT (PStateV Symbol) (Parsec Void [Char]) DataDecl
forall a b. (a -> b) -> a -> b
$ FTycon -> Int -> [DataCtor] -> DataDecl
F.DDecl FTycon
tc Int
n [DataCtor]
ctors

dataCtorP :: FParser F.DataCtor
dataCtorP :: FParser DataCtor
dataCtorP = FParser DataCtor -> FParser DataCtor
forall a. FParser a -> FParser a
parens (LocSymbol -> [DataField] -> DataCtor
F.DCtor (LocSymbol -> [DataField] -> DataCtor)
-> FParser LocSymbol
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) ([DataField] -> DataCtor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser LocSymbol
locSymbolP StateT
  (PStateV Symbol) (Parsec Void [Char]) ([DataField] -> DataCtor)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [DataField]
-> FParser DataCtor
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FParser DataField
-> StateT (PStateV Symbol) (Parsec Void [Char]) [DataField]
forall a. FParser a -> FParser [a]
sMany FParser DataField
dataFieldP)

dataFieldP :: FParser F.DataField
dataFieldP :: FParser DataField
dataFieldP = (LocSymbol -> Sort -> DataField) -> (LocSymbol, Sort) -> DataField
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry LocSymbol -> Sort -> DataField
F.DField ((LocSymbol, Sort) -> DataField)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (LocSymbol, Sort)
-> FParser DataField
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser LocSymbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) (LocSymbol, Sort)
forall a b. FParser a -> FParser b -> FParser (a, b)
sPairP FParser LocSymbol
locSymbolP StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP

bindsP :: FParser [(F.Symbol, F.Sort)]
bindsP :: FParser [(Symbol, Sort)]
bindsP = FParser (Symbol, Sort) -> FParser [(Symbol, Sort)]
forall a. FParser a -> FParser [a]
sMany FParser (Symbol, Sort)
bindP

bindP :: FParser (F.Symbol, F.Sort)
bindP :: FParser (Symbol, Sort)
bindP = FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> FParser (Symbol, Sort)
forall a b. FParser a -> FParser b -> FParser (a, b)
sPairP FParser Symbol
symbolP StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP

defineP :: FParser F.Equation
defineP :: StateT (PStateV Symbol) (Parsec Void [Char]) Equation
defineP = do
  Symbol
name   <- FParser Symbol
symbolP
  [(Symbol, Sort)]
xts    <- FParser [(Symbol, Sort)]
bindsP
  Sort
s      <- StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP
  Expr
body   <- Parser Expr
exprP
  Equation -> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return  (Equation -> StateT (PStateV Symbol) (Parsec Void [Char]) Equation)
-> Equation
-> StateT (PStateV Symbol) (Parsec Void [Char]) Equation
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation Symbol
name [(Symbol, Sort)]
xts Expr
body Sort
s

matchP :: FParser F.Rewrite
matchP :: StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
matchP = do
  Symbol
f    <- FParser Symbol
symbolP
  Symbol
d:[Symbol]
xs <- StateT (PStateV Symbol) (Parsec Void [Char]) [Symbol]
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Symbol]
forall a. FParser a -> FParser a
parens (FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Symbol]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some FParser Symbol
symbolP)
  Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite
F.SMeasure Symbol
f Symbol
d [Symbol]
xs (Expr -> Rewrite)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) Rewrite
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP

sortP :: FParser F.Sort
sortP :: StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP =  (Tokens [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
"@" StateT (PStateV Symbol) (Parsec Void [Char]) (Tokens [Char])
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Int -> Sort
F.FVar (Int -> Sort)
-> FParser Int -> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Int -> FParser Int
forall a. FParser a -> FParser a
parens FParser Int
fIntP))
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Int"  Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
F.FInt)
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Real" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
F.FReal)
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"Frac" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
F.FFrac)
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved [Char]
"num" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sort -> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return  Sort
F.FNum)
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (FTycon -> [Sort] -> Sort
F.fAppTC (FTycon -> [Sort] -> Sort)
-> FParser FTycon
-> StateT (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser FTycon
fTyConP StateT (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Sort] -> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> Sort
F.FObj (Symbol -> Sort) -> (Symbol -> Symbol) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Symbol -> Sort)
-> FParser Symbol
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Symbol
lowerIdP)
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. FParser a -> FParser a
parens ([Char] -> Parser ()
reserved [Char]
"func" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Int -> [Sort] -> Sort -> Sort
mkFunc (Int -> [Sort] -> Sort -> Sort)
-> FParser Int
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Int
fIntP StateT
  (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort -> Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Sort)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
forall a. FParser a -> FParser [a]
sMany StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP)))
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. FParser a -> FParser a
parens ([Char] -> Parser ()
reserved [Char]
"list" Parser ()
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Sort -> Sort
mkList (Sort -> Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP)))
     StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a. FParser a -> FParser a
parens (FTycon -> [Sort] -> Sort
F.fAppTC (FTycon -> [Sort] -> Sort)
-> FParser FTycon
-> StateT (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser FTycon
fTyConP StateT (PStateV Symbol) (Parsec Void [Char]) ([Sort] -> Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP)

mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort
mkFunc :: Int -> [Sort] -> Sort -> Sort
mkFunc Int
n [Sort]
ss Sort
s = Int -> [Sort] -> Sort
F.mkFFunc Int
n ([Sort]
ss [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort
s])

mkList :: F.Sort -> F.Sort
mkList :: Sort -> Sort
mkList Sort
s = FTycon -> [Sort] -> Sort
F.fAppTC FTycon
F.listFTyCon [Sort
s]

exprP :: FParser F.Expr
exprP :: Parser Expr
exprP
  =   Parser Expr
fTrueP
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
fFalseP
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (SymConst -> Expr
forall v. SymConst -> ExprV v
F.ESym (SymConst -> Expr) -> Parser SymConst -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SymConst
fSymconstP)
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Constant -> Expr
forall v. Constant -> ExprV v
F.ECon (Constant -> Expr) -> FParser Constant -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Constant
constantP)
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> FParser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser Symbol
symbolP)
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. FParser a -> FParser a
parens Parser Expr
pExprP

pExprP :: FParser F.Expr
pExprP :: Parser Expr
pExprP
  =   ([Char] -> Parser ()
reserved   [Char]
"if"     Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
F.EIte   (Expr -> Expr -> Expr -> Expr)
-> Parser Expr
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"lit"    Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Char] -> Sort -> Expr
mkLit    ([Char] -> Sort -> Expr)
-> FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser [Char]
stringLiteral StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"cast"   Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
F.ECst   (Expr -> Sort -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"not"    Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr
forall v. ExprV v -> ExprV v
F.PNot   (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reservedOp [Char]
"=>"     Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp   (Expr -> Expr -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reservedOp [Char]
"<=>"    Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff   (Expr -> Expr -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"and"    Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.PAnd   ([Expr] -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
-> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"or"     Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.POr    ([Expr] -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
-> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"forall" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PAll   ([(Symbol, Sort)] -> Expr -> Expr)
-> FParser [(Symbol, Sort)]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser [(Symbol, Sort)]
bindsP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"exists" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PExist ([(Symbol, Sort)] -> Expr -> Expr)
-> FParser [(Symbol, Sort)]
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser [(Symbol, Sort)]
bindsP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"lam"    Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
F.ELam   ((Symbol, Sort) -> Expr -> Expr)
-> FParser (Symbol, Sort)
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FParser (Symbol, Sort)
bindP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"coerce" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
F.ECoerc (Sort -> Sort -> Expr -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"ETApp"  Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
F.ETApp  (Expr -> Sort -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Sort -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Sort -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (PStateV Symbol) (Parsec Void [Char]) Sort
sortP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> Parser ()
reserved   [Char]
"ETAbs"  Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
F.ETAbs  (Expr -> Symbol -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Symbol -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Symbol -> Expr)
-> FParser Symbol -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FParser Symbol
symbolP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin  (Bop -> Expr -> Expr -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
bopP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP)
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom (Brel -> Expr -> Expr -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT
     (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
brelP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr -> Expr)
-> Parser Expr
-> StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP StateT (PStateV Symbol) (Parsec Void [Char]) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) (a -> b)
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP)
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. FParser a -> FParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ([Char] -> FParser [Char]
sym [Char]
"-" FParser [Char] -> Parser Expr -> Parser Expr
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr
forall v. ExprV v -> ExprV v
F.ENeg (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP))
  Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Expr] -> Expr
mkApp ([Expr] -> Expr)
-> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
-> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> StateT (PStateV Symbol) (Parsec Void [Char]) [Expr]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Expr
exprP)

mkLit :: String -> F.Sort -> F.Expr
mkLit :: [Char] -> Sort -> Expr
mkLit [Char]
l Sort
t = Constant -> Expr
forall v. Constant -> ExprV v
F.ECon (Text -> Sort -> Constant
F.L ([Char] -> Text
T.pack [Char]
l) Sort
t)

mkApp :: [F.Expr] -> F.Expr
mkApp :: [Expr] -> Expr
mkApp (Expr
e:[Expr]
es) = Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps Expr
e [Expr]
es
mkApp [Expr]
_      = [Char] -> Expr
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

bopP :: FParser F.Bop
bopP :: StateT (PStateV Symbol) (Parsec Void [Char]) Bop
bopP
  =  ([Char] -> FParser [Char]
sym [Char]
"+"   FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.Plus)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"-"   FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.Minus)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"*"   FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.Times)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"/"   FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.Div)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"mod" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.Mod)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"*."  FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.RTimes)
 StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"/."  FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
-> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bop -> StateT (PStateV Symbol) (Parsec Void [Char]) Bop
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bop
F.RDiv)

brelP :: FParser F.Brel
brelP :: StateT (PStateV Symbol) (Parsec Void [Char]) Brel
brelP
  =  ([Char] -> FParser [Char]
sym [Char]
"="  FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Eq)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"!=" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Ne)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"~~" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Ueq)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"!~" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Une)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
">=" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Ge)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
">"  FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Gt)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"<=" FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Le)
 StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> FParser [Char]
sym [Char]
"<"  FParser [Char]
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
-> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a b.
StateT (PStateV Symbol) (Parsec Void [Char]) a
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
-> StateT (PStateV Symbol) (Parsec Void [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Brel -> StateT (PStateV Symbol) (Parsec Void [Char]) Brel
forall a. a -> StateT (PStateV Symbol) (Parsec Void [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Brel
F.Lt)