{-|
Module      : Language.Contract.Parser
Description : Parser for the contract language (STLC based).
Copyright   : (c) Xie Ruifeng, 2020
License     : AGPL-3
Maintainer  : krantz.xrf@outlook.com
Stability   : experimental
Portability : portable
-}
module Language.Contract.Parser
  ( parseTerm
  , parseFile
  ) where

import Text.Parsec
import Text.Parsec.Token

import Control.Monad.Reader

import Language.Contract.AST

type Parser = ParsecT String () (Reader [String])

langDef :: Monad m => GenLanguageDef String () m
langDef :: GenLanguageDef String () m
langDef = LanguageDef :: forall s u (m :: * -> *).
String
-> String
-> String
-> Bool
-> ParsecT s u m Char
-> ParsecT s u m Char
-> ParsecT s u m Char
-> ParsecT s u m Char
-> [String]
-> [String]
-> Bool
-> GenLanguageDef s u m
LanguageDef
  { commentStart :: String
commentStart    = "{-"
  , commentEnd :: String
commentEnd      = "-}"
  , commentLine :: String
commentLine     = "--"
  , nestedComments :: Bool
nestedComments  = Bool
True
  , identStart :: ParsecT String () m Char
identStart      = ParsecT String () m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter ParsecT String () m Char
-> ParsecT String () m Char -> ParsecT String () m Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_'
  , identLetter :: ParsecT String () m Char
identLetter     = ParsecT String () m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT String () m Char
-> ParsecT String () m Char -> ParsecT String () m Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String () m Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "_'"
  , opStart :: ParsecT String () m Char
opStart         = GenLanguageDef String () m -> ParsecT String () m Char
forall s u (m :: * -> *).
GenLanguageDef s u m -> ParsecT s u m Char
opLetter GenLanguageDef String () m
forall (m :: * -> *). Monad m => GenLanguageDef String () m
langDef
  , opLetter :: ParsecT String () m Char
opLetter        = String -> ParsecT String () m Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf ":!#$%&*+./<=>?@\\^|-~"
  , reservedOpNames :: [String]
reservedOpNames = ["\\", "->", ":", ".", "&", "|", "="]
  , reservedNames :: [String]
reservedNames   =
    [ "if", "then", "else", "let"
    , "unit", "true", "false"
    , "iszero", "pred", "succ", "not"
    , "Unit", "Nat", "Bool" ]
  , caseSensitive :: Bool
caseSensitive   = Bool
True
  }

lexer :: Monad m => GenTokenParser String () m
lexer :: GenTokenParser String () m
lexer = GenLanguageDef String () m -> GenTokenParser String () m
forall s (m :: * -> *) u.
Stream s m Char =>
GenLanguageDef s u m -> GenTokenParser s u m
makeTokenParser GenLanguageDef String () m
forall (m :: * -> *). Monad m => GenLanguageDef String () m
langDef

unit :: Parser Term
unit :: Parser Term
unit = Term
Unit Term -> ParsecT String () (Reader [String]) () -> Parser Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "unit"

nat :: Parser Term
nat :: Parser Term
nat = Natural -> Term
Natural (Natural -> Term) -> (Integer -> Natural) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Term)
-> ParsecT String () (Reader [String]) Integer -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) Integer
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m Integer
natural GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer

bool :: Parser Term
bool :: Parser Term
bool = Bool -> Term
Boolean Bool
True Term -> ParsecT String () (Reader [String]) () -> Parser Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "true"
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Bool -> Term
Boolean Bool
False Term -> ParsecT String () (Reader [String]) () -> Parser Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "false"

predict :: Parser Term
predict :: Parser Term
predict = GenTokenParser String () (Reader [String])
-> forall a.
   ParsecT String () (Reader [String]) a
   -> ParsecT String () (Reader [String]) a
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
braces GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer (Parser Term -> Parser Term) -> Parser Term -> Parser Term
forall a b. (a -> b) -> a -> b
$ do
  GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "\\"
  String
x <- GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer
  let env :: Parser Term -> Parser Term
env = if String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "_" then ([String] -> [String]) -> Parser Term -> Parser Term
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (String
xString -> [String] -> [String]
forall a. a -> [a] -> [a]
:) else Parser Term -> Parser Term
forall a. a -> a
id
  GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "."
  Parser Term -> Parser Term
env Parser Term
term

type_ :: Parser Type
type_ :: Parser Type
type_ = GenTokenParser String () (Reader [String])
-> Parser Type -> Parser Type
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer Parser Type
type_
  Parser Type -> Parser Type -> Parser Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Type
TNatural Type -> ParsecT String () (Reader [String]) () -> Parser Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "Nat"
  Parser Type -> Parser Type -> Parser Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Type
TBoolean Type -> ParsecT String () (Reader [String]) () -> Parser Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "Bool"
  Parser Type -> Parser Type -> Parser Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Type
TUnit Type -> ParsecT String () (Reader [String]) () -> Parser Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "Unit"
  Parser Type -> Parser Type -> Parser Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> Type -> Type -> Type
TArrow (Term -> Type -> Type -> Type)
-> Parser Term
-> ParsecT String () (Reader [String]) (Type -> Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
predict ParsecT String () (Reader [String]) (Type -> Type -> Type)
-> Parser Type
-> ParsecT String () (Reader [String]) (Type -> Type)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Type
type_ ParsecT String () (Reader [String]) (Type -> Type)
-> ParsecT String () (Reader [String]) ()
-> ParsecT String () (Reader [String]) (Type -> Type)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "->" ParsecT String () (Reader [String]) (Type -> Type)
-> Parser Type -> Parser Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Type
type_

atom :: Parser Term
atom :: Parser Term
atom = do
  String
x <- GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer
  Bool
-> ParsecT String () (Reader [String]) ()
-> ParsecT String () (Reader [String]) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_") (String -> ParsecT String () (Reader [String]) ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Unexpected wildcard '_'.")
  [(String, Natural)]
names <- ([String] -> [(String, Natural)])
-> ParsecT String () (Reader [String]) [(String, Natural)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([String] -> [Natural] -> [(String, Natural)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [0..])
  case String -> [(String, Natural)] -> Maybe Natural
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x [(String, Natural)]
names of
    Just n :: Natural
n -> Term -> Parser Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> Term
Atom Natural
n)
    Nothing -> String -> Parser Term
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "unbound variable."

lambda :: Parser Term
lambda :: Parser Term
lambda = do
  GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "\\"
  String
x <- GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer
  GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer ":"
  Type
t <- Parser Type
type_
  let env :: Parser Term -> Parser Term
env = if String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "_" then ([String] -> [String]) -> Parser Term -> Parser Term
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (String
xString -> [String] -> [String]
forall a. a -> [a] -> [a]
:) else Parser Term -> Parser Term
forall a. a -> a
id
  Term
p <- Term -> Parser Term -> Parser Term
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Bool -> Term
Boolean Bool
True) (Parser Term -> Parser Term) -> Parser Term -> Parser Term
forall a b. (a -> b) -> a -> b
$ Parser Term -> Parser Term
env (GenTokenParser String () (Reader [String])
-> Parser Term -> Parser Term
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
braces GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer Parser Term
term)
  GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "."
  Term
body <- Parser Term -> Parser Term
env Parser Term
term
  Term -> Parser Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Type -> Term -> Term
Lambda Term
p Type
t Term
body)

if_ :: Parser Term
if_ :: Parser Term
if_ = Term -> Term -> Term -> Term
If (Term -> Term -> Term -> Term)
-> Parser Term
-> ParsecT String () (Reader [String]) (Term -> Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "if" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
term)
  ParsecT String () (Reader [String]) (Term -> Term -> Term)
-> Parser Term
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "then" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
term)
  ParsecT String () (Reader [String]) (Term -> Term)
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "else" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
term)

assert_ :: Parser Term
assert_ :: Parser Term
assert_ = Term -> Term -> Term
Assert (Term -> Term -> Term)
-> Parser Term
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenTokenParser String () (Reader [String])
-> Parser Term -> Parser Term
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
braces GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer Parser Term
term ParsecT String () (Reader [String]) (Term -> Term)
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
term

atomTerm :: Parser Term
atomTerm :: Parser Term
atomTerm = GenTokenParser String () (Reader [String])
-> Parser Term -> Parser Term
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
parens GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer Parser Term
term
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
unit Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
nat Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
bool Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
lambda
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
atom Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
if_ Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term
assert_
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "iszero" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Term) -> Parser Term -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
IsZero Parser Term
term
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "pred" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Term) -> Parser Term -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
Pred Parser Term
term
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "succ" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Term) -> Parser Term -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
Succ Parser Term
term
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "not" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Term) -> Parser Term -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
Not Parser Term
term

term :: Parser Term
term :: Parser Term
term = Parser Term -> Parser Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Term -> Term -> Term
And (Term -> Term -> Term)
-> Parser Term
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
atomTerm ParsecT String () (Reader [String]) (Term -> Term)
-> ParsecT String () (Reader [String]) ()
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "&" ParsecT String () (Reader [String]) (Term -> Term)
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
atomTerm)
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Term -> Parser Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (Term -> Term -> Term
Or (Term -> Term -> Term)
-> Parser Term
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
atomTerm ParsecT String () (Reader [String]) (Term -> Term)
-> ParsecT String () (Reader [String]) ()
-> ParsecT String () (Reader [String]) (Term -> Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "|" ParsecT String () (Reader [String]) (Term -> Term)
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
atomTerm)
  Parser Term -> Parser Term -> Parser Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Term -> Term -> Term
App ([Term] -> Term)
-> ParsecT String () (Reader [String]) [Term] -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term -> ParsecT String () (Reader [String]) [Term]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Term
atomTerm

-- |Parse a term, for parsing many terms see 'parseFile'.
parseTerm :: String -> Either ParseError Term
parseTerm :: String -> Either ParseError Term
parseTerm s :: String
s =
  let prog :: Parser Term
prog = GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *). GenTokenParser s u m -> ParsecT s u m ()
whiteSpace GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
term Parser Term
-> ParsecT String () (Reader [String]) () -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () (Reader [String]) ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof
  in Reader [String] (Either ParseError Term)
-> [String] -> Either ParseError Term
forall r a. Reader r a -> r -> a
runReader (Parser Term
-> ()
-> String
-> String
-> Reader [String] (Either ParseError Term)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> u -> String -> s -> m (Either ParseError a)
runParserT Parser Term
prog () "<interactive>" String
s) []

binding :: Parser (String, Term)
binding :: Parser (String, Term)
binding = (,)
  (String -> Term -> (String, Term))
-> ParsecT String () (Reader [String]) String
-> ParsecT String () (Reader [String]) (Term -> (String, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reserved GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "let" ParsecT String () (Reader [String]) ()
-> ParsecT String () (Reader [String]) String
-> ParsecT String () (Reader [String]) String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) String
forall s u (m :: * -> *).
GenTokenParser s u m -> ParsecT s u m String
identifier GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer)
  ParsecT String () (Reader [String]) (Term -> (String, Term))
-> Parser Term -> Parser (String, Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (GenTokenParser String () (Reader [String])
-> String -> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *).
GenTokenParser s u m -> String -> ParsecT s u m ()
reservedOp GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer "=" ParsecT String () (Reader [String]) ()
-> Parser Term -> Parser Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
term)

file :: Parser [(String, Term)]
file :: Parser [(String, Term)]
file = Parser (String, Term)
binding Parser (String, Term)
-> ParsecT String () (Reader [String]) Char
-> Parser [(String, Term)]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
`endBy` GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) Char
-> ParsecT String () (Reader [String]) Char
forall s u (m :: * -> *).
GenTokenParser s u m
-> forall a. ParsecT s u m a -> ParsecT s u m a
lexeme GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer (Char -> ParsecT String () (Reader [String]) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ';')

-- |Parse a file, bindings in the form @let <name> = <term>;@.
parseFile :: String -> String -> Either ParseError [(String, Term)]
parseFile :: String -> String -> Either ParseError [(String, Term)]
parseFile nm :: String
nm s :: String
s =
  let prog :: Parser [(String, Term)]
prog = GenTokenParser String () (Reader [String])
-> ParsecT String () (Reader [String]) ()
forall s u (m :: * -> *). GenTokenParser s u m -> ParsecT s u m ()
whiteSpace GenTokenParser String () (Reader [String])
forall (m :: * -> *). Monad m => GenTokenParser String () m
lexer ParsecT String () (Reader [String]) ()
-> Parser [(String, Term)] -> Parser [(String, Term)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser [(String, Term)]
file Parser [(String, Term)]
-> ParsecT String () (Reader [String]) ()
-> Parser [(String, Term)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () (Reader [String]) ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof
  in Reader [String] (Either ParseError [(String, Term)])
-> [String] -> Either ParseError [(String, Term)]
forall r a. Reader r a -> r -> a
runReader (Parser [(String, Term)]
-> ()
-> String
-> String
-> Reader [String] (Either ParseError [(String, Term)])
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> u -> String -> s -> m (Either ParseError a)
runParserT Parser [(String, Term)]
prog () String
nm String
s) []