open Terms;;
open Subst;;
open Mterms;;

(* Simplified version of the reduction functions of Coq V6.2 *)


(* Norm n'apporte rien dans la version actuelle.
   Il serait utile dans fstrong *)

let lift_freeze n mt =
  if n = 0 then mt else
    let (no,ft) = lift_fterm n mt in { norm=no; term=ft }
;;

let freeze_deeper e t =
  let rec unfreeze_mterm e t =
    match t with
      Rel i -> clos_rel e i
    | App(a,b) -> new_mterm (Fapp(unfreeze_mterm e a, unfreeze_mterm e b))
    | Lam u -> {norm=Whnf; term=Flam(mk_clos (subs_lift e) u, e, u)} in

  match t with
    Rel k -> lift_fterm 0 (clos_rel e k) (* cannot happen *)
  | App(a,b) ->
      let va = unfreeze_mterm e a in
      let vb = unfreeze_mterm e b in
        (Red, Fapp(va,vb))
  | Lam u ->  (Whnf, Flam(mk_clos (subs_lift e) u, e, u))
;;

let rec under_lifts ofun k v =
  match v.term with
    Flift(n,ft) -> under_lifts ofun (k+n) ft
  | Fclos(e,t) -> let uv = update v (freeze_deeper e t) in
                     under_lifts ofun k uv
  | _ -> (match ofun with
            Some f -> let uv = update v (f v) in under_lifts None k uv
          | None -> (k, v))
;;

let under_lfts f lfts v =
  let (k,uv) = under_lifts (Some f) 0 v in
    (lshift k lfts, uv)
;;

let rec fstrong hnf_fun lfts mt =
  let (klfts,umt) = under_lfts hnf_fun lfts mt in
  let nt =
    match umt.term with
      Frel i -> Rel (reloc_rel klfts i)
    | Fapp(a,b) -> App(fstrong hnf_fun klfts a, fstrong hnf_fun klfts b)
    | Flam(u,_,_) -> Lam(fstrong hnf_fun (llift klfts) u)
    | (Flift _ | Fclos _) -> failwith "fstrong" in
  let _ = update umt (Norm,umt.term) in
    nt
;;

let appl_state nh b =
  match nh.norm with
    Norm -> if is_val b then Norm else Whnf
  | s -> s;;


let rec whnf_fterm v =
  if is_whnf v then (v.norm, v.term)
  else
    match v.term with
      Fapp(a,b) -> whnf_apply a b
    | Frel _ -> (Norm, v.term)
    | Flam(u,_,_) -> ((if is_whnf u then u.norm else Whnf), v.term)
    | _ -> failwith "whnf_fterm"

and whnf_apply h b =
  let (depth,uh) = under_lifts (Some whnf_fterm) 0 h in
    match uh.term with
    | Flam (_,e,t) ->
        let sb = mk_clos (subs_shift_cons(depth,e, b)) t in
        let (depth',uh') = under_lifts (Some whnf_fterm) 0 sb
        in lift_fterm depth' uh' 
    | _ -> (appl_state uh b, Fapp(lift_freeze depth uh, b))
;;

let lz_norm t =
  let mt = mk_clos subs_id t in
    fstrong whnf_fterm lid mt;;