module Minilang.Lambda where

import Data.Bifunctor (second)
import Minilang.Lambda.DeBruijn (builtinDeBruijnEnv, eval', fromDeBruijn, toDeBruijn)
import Minilang.Lambda.Eval (Env, Term, builtinEnvValue)
import qualified Minilang.Lambda.Eval as Eval
import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer)
import Minilang.Lambda.Parser (AST (..), desugar)
import Minilang.Lambda.Unify (Type (..))
import Minilang.REPL.Types (Evaluator (..), Language (..))

-- | Top-level evaluator
-- Load a list of expressions into given `Env` and `Context`, returning an extended
-- `Env` and `Context` with declarations bound and the list of evaluated top-level
-- terms along with their types.
loadProgram ::
  Evaluator ->
  Language ->
  Env ->
  Context ->
  [AST] ->
  Either TypeError ([(Term, Type)], Env, Context)
loadProgram evaluator language env context exprs =
  fmap (\(res, e, c) -> (reverse res, e, c)) result
  where
    result =
      foldl
        ( \acc expr ->
            case acc of
              Left typeError -> Left typeError
              Right (results, env', context') ->
                case runExpr language expr env' context' of
                  Left typeError -> Left typeError
                  Right (Nothing, env'', context'') ->
                    Right (results, env'', context'')
                  Right (Just res, env'', context'') ->
                    Right (res : results, env'', context'')
        )
        (Right ([], env, context))
        exprs

    runExpr language (Def ident body) env context =
      let term = evalInEnvWith evaluator env body
       in case language of
            Typed ->
              case infer term of
                Left typeError -> Left typeError
                Right typ ->
                  Right (Nothing, (ident, term) : env, extendContext ident typ context)
            Untyped ->
              Right (Nothing, (ident, term) : env, context)
    runExpr language expr env context =
      let v = evalInEnvWith evaluator env expr
       in case language of
            Typed ->
              case infer v of
                Left typeError -> Left typeError
                Right typ ->
                  Right (Just (v, typ), env, context)
            Untyped ->
              Right (Just (v, TyVar "<?>"), env, context)

-- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator.
-- This is the default evaluator used by the server and REPL.
evalInEnv :: Env -> AST -> Term
evalInEnv = evalInEnvWith DeBruijn

-- | Evaluate an 'AST' using the selected 'Evaluator'.
evalInEnvWith :: Evaluator -> Env -> AST -> Term
evalInEnvWith DeBruijn env expr =
  let term = desugar expr
      -- User-defined bindings take precedence over builtins (rightmost wins
      -- in a left-to-right lookup, so put user env first).
      env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv
   in fromDeBruijn $ eval' env' (toDeBruijn term)
evalInEnvWith NbE env expr =
  let term  = desugar expr
      -- Build an EnvValue from the user Env by evaluating each binding's
      -- Term in the accumulated value env (builtins always available at the
      -- bottom).  foldl builds left-to-right so earlier bindings are visible
      -- when evaluating later ones.
      envV  = foldl addBinding builtinEnvValue env
      addBinding acc (name, t) = (name, Eval.eval acc t) : acc
   in Eval.readBack (Eval.eval envV term)