module V = Value
module T = Term

let rec index (env : V.env) (i : int) = 
  match env with
  | []      -> failwith "Can't happen"
  | x :: xs -> if i < 1 then x else index xs (i-1)

let rec eval (env : V.env) (tr : T.term) =
  match tr with
  | Var  (Ix i)               -> index env i
  | Mv   m                    -> V.Stuck (V.Meta m, ?)
  | Type                      -> V.Type
  | T0                        -> V.T0
  | Ind0 (B b, t)             -> begin
    match eval env t with
    | Stuck (s , T0) -> V.Stuck (V.Ind0 (V.C (env, b), s), V.T0)
    | _              -> failwith "eval Ind0 impossible error"
    end
  | T1                        -> V.T1
  | T1tr                      -> V.T1vl
  | TNat                      -> V.TNat
  | Zero                      -> V.Zero
  | Suc  n                    -> V.Suc (eval env n)
  | IndN (B b, tz, B B ts, n) -> indN env b (eval env tz) ts (eval env n)
  | TBool                     -> V.TBool
  | True                      -> V.True
  | False                     -> V.False
  | IndB (B b, t, f, bo)    -> begin
    match eval env bo with
    | True             -> eval env t
    | False            -> eval env f
    | Stuck (s, TBool) -> V.Stuck (V.IndB (V.C (env, b), eval env t, eval env f, s), V.TBool)
    | _                -> failwith "eval IndB impossible error"
    end
  | Pi   (dom, B cod)         -> V.Pi (eval env dom, V.C (env, cod))
  | Lam  (B scope)            -> V.Lam (C (env, scope))
  | App  (f, x)               -> app (eval env f) (eval env x)
  | Sg   (ty, B tr)           -> V.Sg (eval env ty, V.C (env, tr))
  | Pair (x, y)               -> V.Pair (eval env x, eval env y)
  | Fst  tr                   -> fst (eval env tr)
  | Snd  tr                   -> snd (eval env tr)
  | Let  (tr, _, B sc)        -> eval (eval env tr :: env) sc

(* B b, B B ts *)
and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) =
  match n with
  | Zero            -> tz
  | Suc m           -> eval (indN env b tz ts m :: m :: env) ts
  | Stuck (s, TNat) -> V.Stuck (V.IndN (V.C (env, b), tz, V.C2 (env, ts), s), V.TNat)
  | _               -> failwith "eval IndN impossible error"

and app (f : V.value) (x : V.value) =
  match f with
  | Lam (C (env, tr)) -> eval (x :: env) tr
  | Stuck (s, t)      -> begin
    match t with
    | Pi (_, C (env, tr)) -> V.Stuck (V.App (s, x, t), eval (x :: env) tr)
    | _                   -> failwith "eval app stuck f not of pi type"
    end
  | _                 -> failwith "eval app impossible error"

and fst (p : V.value) =
  match p with
  | Pair  (a, _) -> a
  | Stuck (s, Sg (a, _)) -> V.Stuck (V.Fst s, a)
  | _            -> failwith "eval fst impossible error"

and snd (p : V.value) =
  match p with
  | Pair  (_, b) -> b
  | Stuck (s, Sg (_, C (env, b))) -> V.Stuck (V.Snd s, (eval (fst p :: env) b))
  | _            -> failwith "eval fst impossible error"