module Minilang.Lambda.DeBruijn where

import Data.List (elemIndex)
import Data.Text (Text)
import Minilang.Lambda.Eval (Term)
import qualified Minilang.Lambda.Eval as Eval

data DeBruijn
  = FV Text
  | Var Int
  | Lam DeBruijn
  | App DeBruijn DeBruijn
  deriving (Show, Read, Eq)

-- Convert a term with named variables to De Bruijn indices
toDeBruijn :: Term -> DeBruijn
toDeBruijn term = go term []
  where
    go (Eval.Var x) env =
      case elemIndex x env of
        Just idx -> Var idx
        Nothing -> FV x
    go (Eval.Lam x body) env =
      Lam (go body (x : env))
    go (Eval.App f a) env =
      App (go f env) (go a env)

eval :: DeBruijn -> DeBruijn
eval (App f a) =
  case eval f of
    Lam body -> eval (substitute 0 a body)
    f' -> App f' a
eval term = term

substitute :: Int -> DeBruijn -> DeBruijn -> DeBruijn
substitute n arg term = case term of
  FV x -> FV x
  Var x
    | x == n -> arg
    | otherwise -> Var x
  Lam body -> Lam (substitute (n + 1) arg body)
  App f a -> App (substitute n arg f) (substitute n arg a)