{-|
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, 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
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 = forall a. Parser a -> Parser a
token forall a b. (a -> b) -> a -> b
$ forall (st :: ZeroBitType) e a. ParserT st e a -> ParserT st e Name
byteStringOf forall a b. (a -> b) -> a -> b
$
  forall (st :: ZeroBitType) e a b.
ParserT st e a -> (a -> Span -> ParserT st e b) -> ParserT st e b
withSpan (Parser Char
identStartChar forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (st :: ZeroBitType) e a. ParserT st e a -> ParserT st e ()
skipMany Parser Char
identChar) (\()
_ Span
span -> forall (st :: ZeroBitType) e a. ParserT st e a -> ParserT st e ()
fails (Span -> ParserT PureMode Error ()
isKeyword Span
span))

-- | Parse an identifier, throw a precise error on failure.
ident' :: Parser Name
ident' :: Parser Name
ident' = Parser Name
ident 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 forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (st :: ZeroBitType) e. (Char -> Bool) -> ParserT st e Char
satisfyAscii Char -> Bool
isDigit

int :: Parser Int
int :: Parser Int
int = forall a. Parser a -> Parser a
token do
  (Int
place, Int
n) <- forall a b (st :: ZeroBitType) e.
(a -> b -> b) -> ParserT st e a -> ParserT st e b -> ParserT st e b
chainr (\Int
n (!Int
place, !Int
acc) -> (Int
placeforall a. Num a => a -> a -> a
*Int
10,Int
accforall a. Num a => a -> a -> a
+Int
placeforall a. Num a => a -> a -> a
*Int
n)) Parser Int
digit (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, Int
0))
  case Int
place of
    Int
1 -> forall (f :: * -> *) a. Alternative f => f a
empty
    Int
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n

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

atom' :: Parser Tm
atom' :: Parser Tm
atom' = Parser Tm
atom
  forall a. Parser a -> [Expected] -> Parser a
`cut` [String -> Expected
Msg String
"identifier", Expected
"true", Expected
"false", String -> Expected
Msg String
"parenthesized expression", String -> Expected
Msg String
"integer literal"]

-- | Parse an `App`-level expression.
app' :: Parser Tm
app' :: Parser Tm
app' = forall b a (st :: ZeroBitType) e.
(b -> a -> b) -> ParserT st e b -> ParserT st e a -> ParserT st e b
chainl Tm -> Tm -> Tm
App Parser Tm
atom' Parser Tm
atom

-- | Parse a `Mul`-level expression.
mul' :: Parser Tm
mul' :: Parser Tm
mul' = forall b a (st :: ZeroBitType) e.
(b -> a -> b) -> ParserT st e b -> ParserT st e a -> ParserT st e b
chainl Tm -> Tm -> Tm
Mul Parser Tm
app' ($(symbol "*") 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' = forall b a (st :: ZeroBitType) e.
(b -> a -> b) -> ParserT st e b -> ParserT st e a -> ParserT st e b
chainl Tm -> Tm -> Tm
Add Parser Tm
mul' ($(symbol "+") forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
mul')

-- | Parse an `FlatParse.Examples.BasicLambda.Parser.Eq` or `Lt`-level expression.
eqLt' :: Parser Tm
eqLt' :: Parser Tm
eqLt' =
  Parser Tm
add' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Tm
e1 ->
  forall (st :: ZeroBitType) e a b.
ParserT st e a
-> ParserT st e b -> ParserT st e b -> ParserT st e b
branch $(symbol "==") (Tm -> Tm -> Tm
Eq Tm
e1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Tm
add') forall a b. (a -> b) -> a -> b
$
  forall (st :: ZeroBitType) e a b.
ParserT st e a
-> ParserT st e b -> ParserT st e b -> ParserT st e b
branch $(symbol "<")  (Tm -> Tm -> Tm
Lt Tm
e1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Tm
add') forall a b. (a -> b) -> a -> b
$
  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
ident'
  $(symbol' "=")
  Tm
t <- Parser Tm
tm'
  $(keyword' "in")
  Tm
u <- Parser Tm
tm'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
ident'
  $(symbol' ".")
  Tm
t <- Parser Tm
tm'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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'
  $(keyword' "then")
  Tm
u <- Parser Tm
tm'
  $(keyword' "else")
  Tm
v <- Parser Tm
tm'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall (st :: ZeroBitType) e a.
ParserT st e a -> ParserT st e a -> ParserT st e a
<|> Parser Tm
lam forall (st :: ZeroBitType) e a.
ParserT st e a -> ParserT st e a -> ParserT st e a
<|> Parser Tm
pIf forall (st :: ZeroBitType) e a.
ParserT st e a -> ParserT st e a -> ParserT st e a
<|> Parser Tm
eqLt') forall a. Parser a -> [Expected] -> Parser a
`cut` [Expected
"let", Expected
"lam", Expected
"if"]

-- | Parse a complete source file.
src' :: Parser Tm
src' :: Parser Tm
src' = ParserT PureMode Error ()
ws forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Tm
tm' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (st :: ZeroBitType) e. ParserT st e ()
eof forall a. Parser a -> [Expected] -> Parser a
`cut` [String -> Expected
Msg String
"end of input (lexical error)"]


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

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