module Minilang.Lambda where

import Data.Bifunctor (second)
import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn)
import Minilang.Lambda.Eval (Env, Term)
import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer)
import Minilang.Lambda.Parser (AST (..), desugar)
import Minilang.Lambda.Unify (Type (..))
import Minilang.REPL.Types (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 ::
  Language ->
  Env ->
  Context ->
  [AST] ->
  Either TypeError ([(Term, Type)], Env, Context)
loadProgram 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 = evalInEnv 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 = evalInEnv 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)

evalInEnv :: Env -> AST -> Term
evalInEnv env expr =
  let term = desugar expr
      env' = second toDeBruijn <$> env
   in fromDeBruijn $ eval' env' (toDeBruijn term)