{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE CPP #-}

-- | Parser from Tokens into Expressions
module L3.Parse.ExprParser (parseExpr) where

import Control.Applicative
  ( Alternative (empty, (<|>)),
    Applicative (pure),
    optional,
    (<$>),
  )
import Data.Maybe
import L3.Core
import L3.Log
import L3.Parse.Lexer
import L3.Parse.Parsec
import L3.Parse.Parser
import L3.Parse.TokenParsec
import L3.Util
import Prelude hiding (pi)

trace :: String -> a -> a
trace = String -> String -> a -> a
forall a. String -> String -> a -> a
traceU String
"Parse::ExprParser"

traceIO :: (i -> String) -> Parser i o -> Parser i o
traceIO i -> String
msgFn Parser i o
parser = (i -> [(o, i)]) -> Parser i o
forall i o. (i -> [(o, i)]) -> Parser i o
Parser ((i -> [(o, i)]) -> Parser i o) -> (i -> [(o, i)]) -> Parser i o
forall a b. (a -> b) -> a -> b
$ \i
i -> String -> [(o, i)] -> [(o, i)]
forall a. String -> a -> a
trace (i -> String
msgFn i
i) (Parser i o -> i -> [(o, i)]
forall i o. Parser i o -> i -> [(o, i)]
unParser Parser i o
parser i
i)

-- | Parse a string to a named expression (using string labels)
--  Strip comments here, as they apply inside any context and are difficult to deal with otherwise
parseExpr :: [Token] -> Result ShowExpr
parseExpr :: [Token] -> Result ShowExpr
parseExpr [Token]
tks = String -> Result ShowExpr -> Result ShowExpr
forall a. String -> a -> a
trace (String
"parseExpr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
tks) ([Token] -> Result ShowExpr
parseExpr' [Token]
tks)

parseExpr' :: [Token] -> Result ShowExpr
parseExpr' [Token]
tks = Result ShowExpr
es
  where
    es :: Result ShowExpr
es = Parser [Token] ShowExpr -> [Token] -> Result ShowExpr
forall (f :: * -> *) i o.
(Alternative f, Show (f i), Show o, Eq (f i)) =>
Parser (f i) o -> f i -> Result o
runParser Parser [Token] ShowExpr
sugarE ([Token] -> Result ShowExpr)
-> ([Token] -> [Token]) -> [Token] -> Result ShowExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> Bool) -> [Token] -> [Token]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Token -> Bool) -> Token -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Bool
ann) ([Token] -> Result ShowExpr) -> [Token] -> Result ShowExpr
forall a b. (a -> b) -> a -> b
$ [Token]
tks
    ann :: Token -> Bool
ann (Comment String
c) = Bool
True
    ann Token
EOL = Bool
True
    ann Token
_ = Bool
False

-- | Sugared expression, injection point for additional syntax niceties
--  S :: A | [π(_:A)].S
sugarE :: Parser [Token] ShowExpr
sugarE :: Parser [Token] ShowExpr
sugarE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"sugarE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
sugarE'

#ifdef ANONYMOUSPI
sugarE' :: Parser [Token] ShowExpr
sugarE' = do
  ShowExpr
ex <- Parser [Token] ShowExpr
appE
  Maybe ShowExpr
anonPi <- Parser [Token] ShowExpr -> Parser [Token] (Maybe ShowExpr)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (ShowExpr -> Parser [Token] ShowExpr
anonPiE ShowExpr
ex)
  ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShowExpr -> Parser [Token] ShowExpr)
-> ShowExpr -> Parser [Token] ShowExpr
forall a b. (a -> b) -> a -> b
$ ShowExpr -> Maybe ShowExpr -> ShowExpr
forall a. a -> Maybe a -> a
fromMaybe ShowExpr
ex (Maybe ShowExpr -> ShowExpr) -> Maybe ShowExpr -> ShowExpr
forall a b. (a -> b) -> a -> b
$ Maybe ShowExpr
anonPi
#else
sugarE' = do appE
#endif

-- | Applicative expression, unknown and unbounded length
--  A :: F [app F ..]
appE :: Parser [Token] ShowExpr
appE :: Parser [Token] ShowExpr
appE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"appE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
appE'

appE' :: Parser [Token] ShowExpr
appE' = do
  [ShowExpr]
exprs <- Parser [Token] ShowExpr -> Parser [Token] [ShowExpr]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some Parser [Token] ShowExpr
funE
  ShowExpr -> Parser [Token] ShowExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (ShowExpr -> Parser [Token] ShowExpr)
-> ShowExpr -> Parser [Token] ShowExpr
forall a b. (a -> b) -> a -> b
$ (ShowExpr -> ShowExpr -> ShowExpr) -> [ShowExpr] -> ShowExpr
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 ShowExpr -> ShowExpr -> ShowExpr
forall a. Expr a -> Expr a -> Expr a
App [ShowExpr]
exprs

-- | Function expression
--  F :: λ(s:τ).E | π(s:τ).E | T | (S)
funE :: Parser [Token] ShowExpr
funE :: Parser [Token] ShowExpr
funE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"funE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
funE'

#ifdef STRICTPARENS
funE' =
  lamE
    <|> piE
    <|> termE
    <|> braces sugarE
#else
funE' :: Parser [Token] ShowExpr
funE' =
  Parser [Token] ShowExpr
lamE
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
piE
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
termE
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall a. Parser [Token] a -> Parser [Token] a
parens Parser [Token] ShowExpr
sugarE
#endif

-- | Terminal expression, bounded in length and with no children
--  T :: * | # | n@v | v
termE :: Parser [Token] ShowExpr
termE :: Parser [Token] ShowExpr
termE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"termE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
termE'

termE' :: Parser [Token] ShowExpr
termE' =
  Parser [Token] ShowExpr
star
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
box
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
nsVar
    Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
var

-- | Arrow expression, a component of functions
--  (->) :: (s:τ).
arrE :: Parser [Token] (Name, ShowExpr)
arrE :: Parser [Token] (Name, ShowExpr)
arrE = ([Token] -> String)
-> Parser [Token] (Name, ShowExpr)
-> Parser [Token] (Name, ShowExpr)
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"arrE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] (Name, ShowExpr)
arrE'

#ifdef STRICTPARENS
arrE' = do
  (i, τ) <- brackets typE
  _ <- one Arrow
  pure (i, τ)
#else 
arrE' :: Parser [Token] (Name, ShowExpr)
arrE' = do
  (Name
i, ShowExpr
τ) <- Parser [Token] (Name, ShowExpr) -> Parser [Token] (Name, ShowExpr)
forall a. Parser [Token] a -> Parser [Token] a
parens Parser [Token] (Name, ShowExpr)
typE
  Token
_ <- Token -> Parser [Token] Token
one Token
Arrow
  (Name, ShowExpr) -> Parser [Token] (Name, ShowExpr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
i, ShowExpr
τ)
#endif

-- | Type expression, a symbol has type expr
--  τ :: s:S
typE :: Parser [Token] (Name, ShowExpr)
typE :: Parser [Token] (Name, ShowExpr)
typE = ([Token] -> String)
-> Parser [Token] (Name, ShowExpr)
-> Parser [Token] (Name, ShowExpr)
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"typE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] (Name, ShowExpr)
typE'

typE' :: Parser [Token] (Name, ShowExpr)
typE' = do
  Token
t <- Parser [Token] Token
symbol
  case Token
t of
    (Symbol String
s) -> do
      Token -> Parser [Token] Token
one Token
HasType
      (String -> Name
Name String
s,) (ShowExpr -> (Name, ShowExpr))
-> Parser [Token] ShowExpr -> Parser [Token] (Name, ShowExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] ShowExpr
sugarE
    Token
_ -> Parser [Token] (Name, ShowExpr)
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Star axiom
--  * :: Star
star :: Parser [Token] ShowExpr
star :: Parser [Token] ShowExpr
star = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"star " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
forall a. Parser [Token] (Expr a)
star'

star' :: Parser [Token] (Expr a)
star' = do
  Token -> Parser [Token] Token
one Token
StarT
  Expr a -> Parser [Token] (Expr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
forall a. Expr a
Star

-- | Box axiom
--  # :: Box
box :: Parser [Token] ShowExpr
box :: Parser [Token] ShowExpr
box = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"box " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
forall a. Parser [Token] (Expr a)
box'

box' :: Parser [Token] (Expr a)
box' = do
  Token -> Parser [Token] Token
one Token
BoxT
  Expr a -> Parser [Token] (Expr a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
forall a. Expr a
Box

-- | Variable axiom
--  s :: Var s
var :: Parser [Token] ShowExpr
var :: Parser [Token] ShowExpr
var = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"var " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
var'

var' :: Parser [Token] ShowExpr
var' = do
  Token
t <- Parser [Token] Token
symbol
  case Token
t of
    (Symbol String
s) -> ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShowExpr -> Parser [Token] ShowExpr)
-> ShowExpr -> Parser [Token] ShowExpr
forall a b. (a -> b) -> a -> b
$ Name -> ShowExpr
forall a. a -> Expr a
Var (Name -> ShowExpr) -> Name -> ShowExpr
forall a b. (a -> b) -> a -> b
$ String -> Name
Name String
s
    Token
_ -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Namespaced-variable axiom
--  n@s :: Var n@s
nsVar :: Parser [Token] ShowExpr
nsVar :: Parser [Token] ShowExpr
nsVar = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"nsVar " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
nsVar'

nsVar' :: Parser [Token] ShowExpr
nsVar' = do
  Token
ns <- Parser [Token] Token
symbol
  Either Token Any
_ <- Token -> Either Token Any
forall a b. a -> Either a b
Left (Token -> Either Token Any)
-> Parser [Token] Token -> Parser [Token] (Either Token Any)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Token -> Parser [Token] Token
one Token
At
  ShowExpr
t <- Parser [Token] ShowExpr
var Parser [Token] ShowExpr
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Token] ShowExpr
nsVar
  case (Token
ns, ShowExpr
t) of
    (Symbol String
n, Var (Name String
s)) -> ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShowExpr -> Parser [Token] ShowExpr)
-> ShowExpr -> Parser [Token] ShowExpr
forall a b. (a -> b) -> a -> b
$ Name -> ShowExpr
forall a. a -> Expr a
Var (Name -> ShowExpr) -> Name -> ShowExpr
forall a b. (a -> b) -> a -> b
$ String -> Name
Name (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
    (Token, ShowExpr)
_ -> Parser [Token] ShowExpr
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Lambda function
--  λ(s:S).S :: Lam s S S
lamE :: Parser [Token] ShowExpr
lamE :: Parser [Token] ShowExpr
lamE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"lamE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
lamE'

lamE' :: Parser [Token] ShowExpr
lamE' = do
  Token
_ <- Token -> Parser [Token] Token
one Token
LambdaT
  (Name
i, ShowExpr
τ) <- Parser [Token] (Name, ShowExpr)
arrE
  Name -> ShowExpr -> ShowExpr -> ShowExpr
forall a. a -> Expr a -> Expr a -> Expr a
Lam Name
i ShowExpr
τ (ShowExpr -> ShowExpr)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] ShowExpr
sugarE

-- | Pi function
--  π(s:S).S :: Pi s S S
piE :: Parser [Token] ShowExpr
piE :: Parser [Token] ShowExpr
piE = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"piE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) Parser [Token] ShowExpr
piE'

piE' :: Parser [Token] ShowExpr
piE' = do
  Token
_ <- Token -> Parser [Token] Token
one Token
PiT
  (Name
i, ShowExpr
τ) <- Parser [Token] (Name, ShowExpr)
arrE
  Name -> ShowExpr -> ShowExpr -> ShowExpr
forall a. a -> Expr a -> Expr a -> Expr a
Pi Name
i ShowExpr
τ (ShowExpr -> ShowExpr)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] ShowExpr
sugarE

-- | Anonymous-pi function, where the name is unused and therefore not written
--  Note the implicit expression argument, as otherwise sugar = (app >> arrow >> sugar) <|> app
--  If this were not the case, all expressions are parsed as anonymous pis and will fail at the final arrow
--  This is an exponential slowdown
--  S :: π(_:S).S
anonPiE :: ShowExpr -> Parser [Token] ShowExpr
anonPiE :: ShowExpr -> Parser [Token] ShowExpr
anonPiE ShowExpr
τ = ([Token] -> String)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall i o. (i -> String) -> Parser i o -> Parser i o
traceIO (\[Token]
i -> String
"anonPiE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
i) (ShowExpr -> Parser [Token] ShowExpr
anonPiE' ShowExpr
τ)

anonPiE' :: ShowExpr -> Parser [Token] ShowExpr
anonPiE' ShowExpr
τ = do
  Token
_ <- Token -> Parser [Token] Token
one Token
Arrow
  Name -> ShowExpr -> ShowExpr -> ShowExpr
forall a. a -> Expr a -> Expr a -> Expr a
Pi (String -> Name
Name String
"_") ShowExpr
τ (ShowExpr -> ShowExpr)
-> Parser [Token] ShowExpr -> Parser [Token] ShowExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] ShowExpr
sugarE