open Subst;;
open Terms;;


type red_state = Norm | Whnf | Red;;

(* Mutable terms with explicit shifts *)
type mterm =
  { mutable norm: red_state; mutable term: fterm }

 and fterm =
  Frel of int
| Fapp of mterm * mterm
| Flam of mterm * mterm subs * lambda
| Flift of int * mterm
| Fclos of mterm subs * lambda
;;

let is_val v = v.norm = Norm;;
let is_whnf v = v.norm <> Red;;
let set_norm v = v.norm <- Norm;;
let set_whnf v = if v.norm = Red then v.norm <- Whnf;; 

let rec lift_fterm n ft =
  match ft.term with
    Flift(k,m) -> lift_fterm (n+k) m
  | _ -> (ft.norm, Flift(n,ft));;

let new_mterm ft = { norm = Red; term = ft };;

(* Lookup in the context *)
let clos_rel e i =
  match expand_rel e i with
      Inl(0,mt) -> mt
    | Inl(n,mt) ->
        let (no,ft) = lift_fterm n mt in { norm=no; term=ft }
    | Inr n -> {norm=Norm; term= Frel n}
;;

(* Optimization: do not enclose variables in a closure.
   Makes variable access much faster *)
let mk_clos e = function
    Rel i -> clos_rel e i
  | t -> new_mterm (Fclos(e,t))
;;

let update v1 (no,t) =
  v1.norm <- no;
  v1.term <- t;
  v1 (* purely functional version: {norm=no; term=t}*)
;;