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, 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 = desugar body
       in case language of
            Typed ->
              case infer term of
                Left typeError -> Left typeError
                Right typ ->
                  Right (Nothing, (ident, term) : env, context)
            Untyped ->
              Right (Nothing, (ident, term) : env, context)
    runExpr language expr env context =
      let term = desugar expr
          env' = second toDeBruijn <$> env
          v = fromDeBruijn $ eval' env' (toDeBruijn term)
       in case language of
            Typed ->
              case infer term of
                Left typeError -> Left typeError
                Right typ ->
                  Right (Just (v, typ), env, context)
            Untyped ->
              Right (Just (v, TyVar "<?>"), env, context)