{-|
This module contains a simple lambda calculus parser. This parser is not optimized for maximum
performance; instead it's written in a style which emulates the look and feel of conventional
monadic parsers. An optimized implementation would use low-level `switch` expressions more often.
-}

{-# language StrictData #-}

module FlatParse.Examples.BasicLambda.Parser where

import Data.Char (ord)
import qualified Data.ByteString as B

import FlatParse.Basic hiding (Parser, runParser, string, char, err, cut)
import FlatParse.Examples.BasicLambda.Lexer

--------------------------------------------------------------------------------

type Name = B.ByteString

{-|
A term in the language. The precedences of different constructs are the following, in decreasing
order of strength:

* Identifiers, literals and parenthesized expressions
* Function application (left assoc)
* Multiplication (left assoc)
* Addition (left assoc)
* Equality, less-than (non-assoc)
* @lam@, @let@, @if@ (right assoc)

-}
data Tm
  = Var Name        -- ^ @x@
  | App Tm Tm       -- ^ @t u@
  | Lam Name Tm     -- ^ @lam x. t@
  | Let Name Tm Tm  -- ^ @let x = t in u@
  | BoolLit Bool    -- ^ @true@ or @false@.
  | IntLit Int      -- ^ A positive `Int` literal.
  | If Tm Tm Tm     -- ^ @if t then u else v@
  | Add Tm Tm       -- ^ @t + u@
  | Mul Tm Tm       -- ^ @t * u@
  | Eq Tm Tm        -- ^ @t == u@
  | Lt Tm Tm        -- ^ @t < u@
  deriving Int -> Tm -> ShowS
[Tm] -> ShowS
Tm -> String
(Int -> Tm -> ShowS)
-> (Tm -> String) -> ([Tm] -> ShowS) -> Show Tm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tm] -> ShowS
$cshowList :: [Tm] -> ShowS
show :: Tm -> String
$cshow :: Tm -> String
showsPrec :: Int -> Tm -> ShowS
$cshowsPrec :: Int -> Tm -> ShowS
Show


-- | Parse an identifier. This parser uses `isKeyword` to check that an identifier is not a
--   keyword.
ident :: Parser Name
ident :: Parser Name
ident = Parser Name -> Parser Name
forall a. Parser a -> Parser a
token (Parser Name -> Parser Name) -> Parser Name -> Parser Name
forall a b. (a -> b) -> a -> b
$ Parser () Error () -> Parser Name
forall r e a. Parser r e a -> Parser r e Name
byteStringOf (Parser () Error () -> Parser Name)
-> Parser () Error () -> Parser Name
forall a b. (a -> b) -> a -> b
$
  Parser () Error ()
-> (() -> Span -> Parser () Error ()) -> Parser () Error ()
forall r e a b.
Parser r e a -> (a -> Span -> Parser r e b) -> Parser r e b
spanned (Parser Char
identStartChar Parser Char -> Parser () Error () -> Parser () Error ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser () Error ()
forall r e a. Parser r e a -> Parser r e ()
many_ Parser Char
identChar) (\()
_ -> Parser () Error () -> Parser () Error ()
forall r e a. Parser r e a -> Parser r e ()
fails (Parser () Error () -> Parser () Error ())
-> (Span -> Parser () Error ()) -> Span -> Parser () Error ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Span -> Parser () Error ()
isKeyword)

-- | Parse an identifier, throw a precise error on failure.
cutIdent :: Parser Name
cutIdent :: Parser Name
cutIdent = Parser Name
ident Parser Name -> Expected -> Parser Name
forall a. Parser a -> Expected -> Parser a
`cut'` (String -> Expected
Msg String
"identifier")

digit :: Parser Int
digit :: Parser Int
digit = (\Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') (Char -> Int) -> Parser Char -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Char
forall r e. (Char -> Bool) -> Parser r e Char
satisfyASCII Char -> Bool
isDigit

int :: Parser Int
int :: Parser Int
int = Parser Int -> Parser Int
forall a. Parser a -> Parser a
token (Parser Int -> Parser Int) -> Parser Int -> Parser Int
forall a b. (a -> b) -> a -> b
$
  (Int, Int) -> Int
forall a b. (a, b) -> b
snd ((Int, Int) -> Int) -> Parser () Error (Int, Int) -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> (Int, Int) -> (Int, Int))
-> Parser Int
-> Parser () Error (Int, Int)
-> Parser () Error (Int, Int)
forall a b r e.
(a -> b -> b) -> Parser r e a -> Parser r e b -> Parser r e b
chainr (\Int
n (!Int
place, !Int
acc) -> (Int
placeInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
10,Int
accInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
placeInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n)) Parser Int
digit ((Int
10,) (Int -> (Int, Int)) -> Parser Int -> Parser () Error (Int, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
digit)

-- | Parse a literal, identifier or parenthsized expression.
atom :: Parser Tm
atom :: Parser Tm
atom =
       (Name -> Tm
Var           (Name -> Tm) -> Parser Name -> Parser Tm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Name
ident)
   Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> (Bool -> Tm
BoolLit Bool
True  Tm -> Parser () Error () -> Parser Tm
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$  $(keyword "true"))
   Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> (Bool -> Tm
BoolLit Bool
False Tm -> Parser () Error () -> Parser Tm
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$  $(keyword "false"))
   Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> (Int -> Tm
IntLit        (Int -> Tm) -> Parser Int -> Parser Tm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
int)
   Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> ($(symbol "(") Parser () Error () -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
tm Parser Tm -> Parser () Error () -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* $(cutSymbol ")"))

-- | Parse an `App`-level expression.
app :: Parser Tm
app :: Parser Tm
app = (Tm -> Tm -> Tm) -> Parser Tm -> Parser Tm -> Parser Tm
forall b a r e.
(b -> a -> b) -> Parser r e b -> Parser r e a -> Parser r e b
chainl Tm -> Tm -> Tm
App (Parser Tm
atom Parser Tm -> [Expected] -> Parser Tm
forall a. Parser a -> [Expected] -> Parser a
`cut` [String -> Expected
Msg String
"identifier", String -> Expected
Lit String
"true", String -> Expected
Lit String
"false"]) Parser Tm
atom

-- | Parse a `Mul`-level expression.
mul :: Parser Tm
mul :: Parser Tm
mul = (Tm -> Tm -> Tm) -> Parser Tm -> Parser Tm -> Parser Tm
forall b a r e.
(b -> a -> b) -> Parser r e b -> Parser r e a -> Parser r e b
chainl Tm -> Tm -> Tm
Mul Parser Tm
app ($(symbol "*") Parser () Error () -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
app)

-- | Parse an `Add`-level expression.
add :: Parser Tm
add :: Parser Tm
add = (Tm -> Tm -> Tm) -> Parser Tm -> Parser Tm -> Parser Tm
forall b a r e.
(b -> a -> b) -> Parser r e b -> Parser r e a -> Parser r e b
chainl Tm -> Tm -> Tm
Add Parser Tm
mul ($(symbol "+") Parser () Error () -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
mul)

-- | Parse an `Eq` or `Lt`-level expression.
eqLt :: Parser Tm
eqLt :: Parser Tm
eqLt =
  Parser Tm
add Parser Tm -> (Tm -> Parser Tm) -> Parser Tm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Tm
e1 ->
  Parser () Error () -> Parser Tm -> Parser Tm -> Parser Tm
forall r e a b.
Parser r e a -> Parser r e b -> Parser r e b -> Parser r e b
branch $(symbol "==") (Tm -> Tm -> Tm
Eq Tm
e1 (Tm -> Tm) -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Tm
add) (Parser Tm -> Parser Tm) -> Parser Tm -> Parser Tm
forall a b. (a -> b) -> a -> b
$
  Parser () Error () -> Parser Tm -> Parser Tm -> Parser Tm
forall r e a b.
Parser r e a -> Parser r e b -> Parser r e b -> Parser r e b
branch $(symbol "<")  (Tm -> Tm -> Tm
Lt Tm
e1 (Tm -> Tm) -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Tm
add) (Parser Tm -> Parser Tm) -> Parser Tm -> Parser Tm
forall a b. (a -> b) -> a -> b
$
  Tm -> Parser Tm
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tm
e1

-- | Parse a `Let`.
pLet :: Parser Tm
pLet :: Parser Tm
pLet = do
  $(keyword "let")
  Name
x <- Parser Name
cutIdent
  $(cutSymbol "=")
  Tm
t <- Parser Tm
tm
  $(cutKeyword "in")
  Tm
u <- Parser Tm
tm
  Tm -> Parser Tm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tm -> Parser Tm) -> Tm -> Parser Tm
forall a b. (a -> b) -> a -> b
$ Name -> Tm -> Tm -> Tm
Let Name
x Tm
t Tm
u

-- | Parse a `Lam`.
lam :: Parser Tm
lam :: Parser Tm
lam = do
  $(keyword "lam")
  Name
x <- Parser Name
cutIdent
  $(cutSymbol ".")
  Tm
t <- Parser Tm
tm
  Tm -> Parser Tm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tm -> Parser Tm) -> Tm -> Parser Tm
forall a b. (a -> b) -> a -> b
$ Name -> Tm -> Tm
Lam Name
x Tm
t

-- | Parse an `If`.
pIf :: Parser Tm
pIf :: Parser Tm
pIf = do
  $(keyword "if")
  Tm
t <- Parser Tm
tm
  $(cutKeyword "then")
  Tm
u <- Parser Tm
tm
  $(cutKeyword "else")
  Tm
v <- Parser Tm
tm
  Tm -> Parser Tm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tm -> Parser Tm) -> Tm -> Parser Tm
forall a b. (a -> b) -> a -> b
$ Tm -> Tm -> Tm -> Tm
If Tm
t Tm
u Tm
v

-- | Parse any `Tm`.
tm :: Parser Tm
tm :: Parser Tm
tm = Parser Tm
pLet Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> Parser Tm
lam Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> Parser Tm
pIf Parser Tm -> Parser Tm -> Parser Tm
forall r e a. Parser r e a -> Parser r e a -> Parser r e a
<|> Parser Tm
eqLt

-- | Parse a complete source file.
src :: Parser Tm
src :: Parser Tm
src = Parser () Error ()
ws Parser () Error () -> Parser Tm -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
tm Parser Tm -> Parser () Error () -> Parser Tm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser () Error ()
forall r e. Parser r e ()
eof Parser () Error () -> [Expected] -> Parser () Error ()
forall a. Parser a -> [Expected] -> Parser a
`cut`
  [String -> Expected
Msg String
"end of input", String -> Expected
Msg String
"identifier", String -> Expected
Lit String
"true", String -> Expected
Lit String
"false",
   String -> Expected
Msg String
"integer literal", String -> Expected
Msg String
"parenthesized expression"]


-- Examples
--------------------------------------------------------------------------------

-- testParser src p1
-- p1 = unlines [
--   "let f = lam x. lam y. x (x (x y)) in",
--   "let g = if f true then false else true in",
--   "f g g h"
--   ]