{-# LANGUAGE TupleSections #-}

-- | Type checking and type inference
module L3.Core.Eval (evalExpr, evalExpr0) where

import Data.Char (isDigit)
import Data.List (intercalate)
import L3.Core.Expr
import L3.Core.Infer
import L3.Core.Normal
import L3.Log
import L3.Util

trace :: String -> a -> a
trace = String -> String -> a -> a
forall a. String -> String -> a -> a
traceU String
"Core::Eval"

-- | Evaluate an expression, returning its type and normalized form
evalExpr :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a, Expr a)
evalExpr :: Context a -> Expr a -> Result (Expr a, Expr a)
evalExpr (Ctx [(a, Expr a)]
τ) Expr a
e = String -> Result (Expr a, Expr a) -> Result (Expr a, Expr a)
forall a. String -> a -> a
trace (String
"evalExpr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(a, Expr a)] -> String
forall a. Show a => a -> String
show [(a, Expr a)]
τ String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e) (Context a -> Expr a -> Result (Expr a, Expr a)
forall a.
(Eq a, Enum a, Show a) =>
Context a -> Expr a -> Result (Expr a, Expr a)
evalExpr' ([(a, Expr a)] -> Context a
forall a. [(a, Expr a)] -> Context a
Ctx [(a, Expr a)]
τ) Expr a
e)

evalExpr' :: Context a -> Expr a -> Result (Expr a, Expr a)
evalExpr' Context a
τ Expr a
e = (Expr a -> (Expr a, Expr a))
-> Result (Expr a) -> Result (Expr a, Expr a)
forall a b. (a -> b) -> Result a -> Result b
mapR (,Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
e) (Context a -> Expr a -> Result (Expr a)
forall a.
(Eq a, Enum a, Show a) =>
Context a -> Expr a -> Result (Expr a)
inferType Context a
τ Expr a
e)

-- | `evalExpr0` is the same as `evalExpr` with an empty context, meaning that
-- the expression must be closed (i.e. no free variables), otherwise evaluation
-- will fail.
evalExpr0 :: (Eq a, Enum a, Show a) => Expr a -> Result (Expr a, Expr a)
evalExpr0 :: Expr a -> Result (Expr a, Expr a)
evalExpr0 Expr a
e = String -> Result (Expr a, Expr a) -> Result (Expr a, Expr a)
forall a. String -> a -> a
trace (String
"evalExpr0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e) (Expr a -> Result (Expr a, Expr a)
forall a.
(Eq a, Enum a, Show a) =>
Expr a -> Result (Expr a, Expr a)
evalExpr0' Expr a
e)

evalExpr0' :: (Eq a, Enum a, Show a) => Expr a -> Result (Expr a, Expr a)
evalExpr0' :: Expr a -> Result (Expr a, Expr a)
evalExpr0' = Context a -> Expr a -> Result (Expr a, Expr a)
forall a.
(Eq a, Enum a, Show a) =>
Context a -> Expr a -> Result (Expr a, Expr a)
evalExpr ([(a, Expr a)] -> Context a
forall a. [(a, Expr a)] -> Context a
Ctx [])