(* type var = (* unique name *) int * (int * term) option * (*level*) int *)
type term =
  | Tvar of int
  | Tapp of term * term * bool
  | Tlam of int * term
;;

let zero = Tvar 1010;;
let dummy = Tvar 333;;


(* mk_app & subst implementano la beta *)
let rec mk_app t1 t2 = match t1 with
  | Tlam(v, t1') -> subst v t2 t1'
  | _ -> Tapp(t1, t2, false)
and subst v tv =
  let rec aux = function
  | Tapp(t1, t2, _) -> mk_app (aux t1) (aux t2)
  | Tvar v' as t -> if v = v' then tv else t
  | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t')
  in aux
;;

(* PARSING AND PRINTING *)

let parse =
  let rec minus1 = function
    | Tvar n -> Tvar (n-1)
    | Tapp(t1, t2, b) -> Tapp(minus1 t1, minus1 t2, b)
    | Tlam(n, t) -> Tlam(n-1, minus1 t)
  (* in let open Parser *)
  in let rec myterm_of_term = function
    | Parser.Var n -> Tvar n
    | Parser.App(t1, t2) -> (*Tapp(myterm_of_term t1, myterm_of_term t2) WARNING! BETA DOWN HERE! *)
                            mk_app (myterm_of_term t1) (myterm_of_term t2)
    | Parser.Lam(t) -> minus1 (Tlam(0, myterm_of_term t))
  in fun strs -> (
    let (tms, free) = Parser.parse_many strs
    in List.map myterm_of_term tms
    )
;;

(* PRETTY PRINTING *)
open Console;;

let fancy_of_term t =
let rec string_of_term =
  let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"] in
  let bound = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in
  let string_of_int' n = if n >= 0 then "free" ^ string_of_int n else "bound" ^ string_of_int n  in
  let rec string_of_var t =
    if Tvar t = dummy then "_" else if Tvar t = zero then "ZZ" else match t with
    | n -> string_of_int' n
  and string_of_term_w_pars = function
    | Tvar v -> string_of_var v
    | Tapp(t1, t2, _) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"
    | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"
  and string_of_term_no_pars_app = function
    | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)
    | _ as t -> string_of_term_w_pars t
  and string_of_term_no_pars_lam = function
    | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)
    | _ as t -> string_of_term_no_pars t
  and string_of_term_no_pars = function
    | Tlam(_, _) as t -> string_of_term_no_pars_lam t
    | _ as t -> string_of_term_no_pars_app t
  in string_of_term_no_pars
in let rec html_of_term =
  let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in
  let bound = ["x"; "y"; "z"; "w"; "q"] in
  let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in
  let rec string_of_var t =
    if Tvar t = dummy then "#" else if Tvar t = zero then "Z" else string_of_int' t
  and string_of_term_w_pars = function
    | Tvar v -> string_of_var v
    | Tapp(t1, t2,_) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"
    | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"
  and string_of_term_no_pars_app = function
    | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)
    | _ as t -> string_of_term_w_pars t
  and string_of_term_no_pars_lam = function
    | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)
    | _ as t -> string_of_term_no_pars t
  and string_of_term_no_pars = function
    | Tlam(_, _) as t -> string_of_term_no_pars_lam t
    | _ as t -> string_of_term_no_pars_app t
  in string_of_term_no_pars
in
  string_of_term t / "html_of_term t"
;;

let fancy_of_nf t: Console.fancyobj =
let rec print ?(l=[]) =
 function
    `Var n -> Util.Vars.print_name l n
  | `N n -> string_of_int n
  | `Match(t,bs_lift,bs,args) ->
     "([" ^ print ~l (t :> Num.nf) ^
     " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Num.lift bs_lift t)) !bs) ^ "] " ^
     String.concat " " (List.map (print ~l) args) ^ ")"
  | `I(n,args) -> "(" ^ Util.Vars.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
  | `Lam(_,nf) ->
     let name = Util.Vars.string_of_var (List.length l) in
     "" ^ name ^ "." ^ print ~l:(name::l) (nf : Num.nf)

(* in let rec print_html ?(l=[]) =
 function
    `Var n -> Lambda3.print_name l n
  | `N n -> string_of_int n
  | `Match(t,bs_lift,bs,args) ->
     "(<b>match</b> " ^ print_html ~l (t :> Lambda3.nf) ^
     " <b>with</b> " ^ String.concat " <b>|</b> " (List.map (fun (n,t) -> string_of_int n ^ " <b>&rArr;</b> " ^ print_html ~l (Lambda3.lift bs_lift t)) !bs) ^ "..." (* Attenzion non sto stampando gli argomenti applicati! Perche' non ce ne sono mai *)
  | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")"
  | `Lam nf ->
     let name = Lambda3.string_of_var (List.length l) in
     "&lambda;" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf) *)
in
  print t / print t
;;

let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);;
(*  *)


let varcount = ref 11;;

let freshvar () = (
  varcount := (!varcount + 1);
  !varcount
);;

let find_applicative =
  let rec aux = function
  | Tapp(t1, Tlam _, _) -> Some t1
  | Tapp(t1, t2, _) ->
    (match aux t1 with
    | None -> aux t2
    | _ as r -> r)
  | _-> None
  in let rec aux2 = function
    | [] -> None
    | x::xs -> (match aux x with
      | None -> aux2 xs
      | _ as result -> result
    )
  in aux2
;;

let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)

let rec hd = function | Tvar _ as x -> x | Tapp(t, _, _) -> hd t | _ -> assert false;;

let rec set_applied =
  function
  | Tvar _ as v -> v
  | Tlam _ -> assert false
  | Tapp(t1,t2,_) -> Tapp(set_applied t1, set_applied t2, true)
;;

let rec constant a n =
  if n = 0 then [] else a:: (constant a (n-1))
;;

let rec mk_dummies k t =
  set_applied (mk_apps t (constant dummy (k+1)))
;;

let rec make_lambda_zero k =
  if k = 0 then mk_dummies (k+1) zero else Tlam(0, make_lambda_zero (k-1))
;;

let mk_vars n =
  let rec aux n =
    if n = 0
    then []
    else (Tvar (freshvar ())) :: (aux (n-1))
  in aux n @ [make_lambda_zero (n+1)]
;;

let apply a vars =
  let rec aux = function
  | Tapp(t1, t2, b) ->
    if t1 = a
    then (assert (not b); Tapp(aux t1, mk_apps' t2 vars, true))
    else Tapp(aux t1, aux t2, b)
  | _ as t -> t
  and mk_apps' t vars =
    if t = zero
    then mk_dummies (List.length vars - 1) t
    else aux (mk_apps t vars)
  in aux
;;

let round k (app_map, tms) =
  match find_applicative tms with
  | None -> raise Not_found
  | Some a ->
    let vars = mk_vars k in
    let f = apply a vars in
    let app_map = (a, vars) :: (List.map (fun (x,y) -> f x, y) app_map)
    in (app_map, List.map f tms)
;;

let ends_with t1 t2 = match t1 with
  | Tapp(_, t, _) -> t = t2
  | _ -> false
;;

let rec last_round k (app_map, forbidden, t) =
  let mk_apps' forbidden t vars =
    if List.mem t forbidden
    then mk_dummies (List.length vars - 1) t
    else mk_apps t vars
  (* in let rec already_applied = function
    | Tapp(_, t) -> t = zero || t = dummy || hd t = zero
    | _ -> false *)
  in if ends_with t dummy then (app_map, forbidden, t) else (match t with
  | Tapp(t1, t2, b) ->
    if b
    then
      let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)
      in let app_map, forbidden, t2 = last_round k (app_map, forbidden, t2)
      in app_map, forbidden, Tapp(t1, t2, b)
    else
      let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)
      in let app_map, forbidden, t2 =
        try
            let vars = List.assoc t1 app_map
            in last_round k (app_map, forbidden, (mk_apps' forbidden t2 vars))
          with Not_found ->
            let vars = mk_vars k in
            let app_map = (t1, vars) :: app_map in
            last_round k (app_map, (vars @ forbidden), (mk_apps' forbidden t2 vars))
      in app_map, forbidden, Tapp(t1, t2, true)
  | _ as t -> app_map, forbidden, t
  )
;;

let fixpoint f =
  let rec aux x = try
    let y = f x in aux y
  with Not_found -> x
  in aux
;;

(* lista di sottotermini applicativi *)
let rec subterms = function
  | Tlam _ -> assert false
  | Tvar _ as v -> [v]
  | Tapp(t1, t2, b) -> Tapp(t1, t2, b) :: ((subterms t1) @ (subterms t2))
;;

(* filtra dai sottotermini le variabili *)
let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;

let stupid_sort_uniq map l =
  let rec stupid_uniq = function
    | [] -> []
    | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)
  in let stupid_compare a b =
    let rec size = function
      | Tvar n as v -> if v = zero then 0 else (
        try
          let t, _ = List.find (fun (_,vars) -> List.mem v vars) map
          in 1 + size t
        with Not_found -> 1 + n)
      | Tapp(t1,t2,_) -> 1 + size t1 + size t2
      | Tlam _ -> assert false
    in compare (size a) (size b)
  in stupid_uniq (List.sort stupid_compare l)
;;

(* crea i match ricorsivamente.
  - k e' lo special-K
  - subs e' l'insieme dei sottotermini
  TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione
 *)
let crea_match subs map forbidden (acc : (term * Num.nf) list) : term -> Num.nf =
  let req t = try List.assoc t acc with Not_found -> `Var 9999 in
  let aux t1 = (
  if t1 = dummy then `Var 99999 else
  (* let _ = print_term t1 in *)
  let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2,true)) subs) subs
  in if cont = [] then
    try `N (Util.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else

    if List.mem (hd t1) forbidden then `Lam (true,req (Tapp(t1, dummy, true)))
    else (
      let vars = List.assoc t1 map
      (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))
      in let _ = print_term (mk_apps dummy vars) *)
      in let vars = List.map req vars
      in let vars = List.map (Num.lift 1) vars (* forse lift non necessario *)
      in let vars = Listx.from_list vars
      in let body = `I(0, vars)
      in let branches = List.map (fun t2 -> (Util.index_of t2 subs, req (Tapp(t1, t2, true)))) cont
      in let bs = ref(branches)
      in let lift = 1
      in let args = []
      in `Lam (true, `Match(body, lift, bs, args))
    )
  ) in aux
;;

(* filtra dai sottotermini le variabili *)
let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;

let mk_zeros k =
  let rec aux n prev =
    if n = 0 then [zero]
    else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev
  in aux (k+1) []
;;

let rec freevars = function
  | Tvar _ as v -> [v]
  | Tlam(v,t) -> List.filter (fun x-> x <> Tvar v) (freevars t)
  | Tapp(t1,t2,_) -> (freevars t1) @ (freevars t2)
;;

open Pure;;

let is_scott_n t n =
  let open Lambda4 in let open Pure in
  let rec aux n = function
  | L (L (A (V 1, L (V 0)))) -> n = 0
  | L (L (A (V 0, t))) -> aux (n-1) t
  | _ -> assert false
  in aux n t
;;
let is_scott =
  let open Lambda4 in let open Pure in
  let rec aux = function
  | L (L (A (V 1, L (V 0)))) -> 0
  | L (L (A (V 0, t))) -> 1 + aux t
  | _ -> assert false
  in aux
;;

let compute_special_k tms =
  let rec aux k t = match t with
    | Tvar _ -> 0
    | Tapp(t1,t2,_) -> Pervasives.max (aux 0 t1) (aux 0 t2)
    | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)
  in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms
;;

let magic strings =
  let rec map_helper_3 a b f =
    function
    | [] -> a, b, []
    | c::cs ->
      let a, b, d = f (a, b, c) in
      let a, b, ds = map_helper_3 a b f cs in
      a, b, (d::ds)
  in let _ = print_hline ()
  in let tms = parse strings
  in let k = compute_special_k tms
  in let zero' = make_lambda_zero (k+1)
  in let tms = List.map (fun x -> Tapp(x, zero', false)) tms
  in let fv = Util.sort_uniq (List.concat (List.map freevars tms))
  in let (map, tms') = fixpoint (round k) ([], tms)
  (* in let _ = print_string_endline "map1 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok1" *)
  in let _ = List.map print_term tms'

  in let map1 = List.map fst map
  in let map2 = List.map snd map
  in let map_new, forbidden, map1' = map_helper_3 [] [zero] (last_round k) map1

  in let map = map_new @ (List.combine map1' map2)
  (* in let _ = print_string_endline "map2 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok2" *)
  in let map, forbidden, tms' = map_helper_3 map forbidden (last_round k) tms'

  in let _ = List.map print_term tms'
  in let subs = List.concat (List.map subterms tms')
  in let subs = stupid_sort_uniq map subs
  (* metti gli zeri in testa, perche' vanno calcolati per primi *)
  in let zeros = mk_zeros k
  in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)

  (* in let _ = print_string_endline " subs"; List.iter print_term subs *)
  (* in let _ = print_string_endline "map "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok" *)

  in let f t acc = let res = crea_match subs map forbidden acc t in (t,res)::acc
  in let acc = List.fold_right f subs []

  in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc
  in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " &#8614; ") ^^ fancy_of_nf y)) sigma

  in let _ = print_string_endline "controllo di purezza";
  (* in let open Num *)
  in let ps, _ = Num.parse' strings
  in let ps = List.map (fun x -> Num.mk_app x (`Var 1010)) ps
  in let ps = List.map (fun t -> Num.ToScott.t_of_nf (t :> Num.nf)) ps
  in let sigma = List.map (
    function (Tvar n , inst) -> n, Num.ToScott.t_of_nf inst | _ -> assert false
    ) sigma
  (* in let ps =
    List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma
  in let _ = List.iteri (fun i n ->
    print_string_endline ("X " ^ Pure.print (Pure.whd n));
    (* assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs)) *)
    is_scott (Pure.whd n); ()
    ) ps *)
  in ()
;;


(* magic ["x (x x x)"; "x (y. y x)"; "x x (y. y y (x x y))"] ;; *)
magic ["((x x) (x. x))";"x x"];;

(*

let alive (_, _, n) = n;;
let rec setalive c = function
  | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v
  | Tapp(a,b) -> Tapp(setalive c a, setalive c b)
  | Tlam(n, t) -> Tlam(n, setalive c t)
;;

let mk_vars t lev =
  let rec aux n =
    if n = 0
    then []
    else Tvar(0, Some(n, t), lev) :: (aux (n-1))
  in aux
;;

let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)


let compute_special_k tms =
  let rec aux k t = match t with
    | Tvar _ -> 0
    | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2)
    | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)
  in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms
;;

let compute_special_h tms =
  let rec eat_lam = function
    | Tlam(_,t) -> eat_lam t
    | _ as t -> t
  in
  let rec aux t = match t with
    | Tvar _ -> 0
    | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2)
    | Tlam(v,t) -> 1 + (aux (eat_lam t))
  in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms
;;

(* funzione di traduzione brutta & cattiva *)
let translate k =
  let rec aux = function
  | Tlam _ -> assert false
  | Tvar _ as v -> v
  | Tapp(t1, t2) ->
    let v = hd t1 in
    let a = alive v in
    let t1' = aux t1 in
    let t2' = if a = 0
      then t2
      else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero])
    in Tapp(t1', aux t2')
  in aux
;;

(* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *)
let rec dummize = function
  | Tlam _ -> assert false
  | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c)
  | Tvar _ as v -> v
  | Tapp(t1, t2) ->
    if alive (hd t1) = 0
    then Tapp(dummize t1, dummy)
    else Tapp(dummize t1, dummize t2)
;;

(* lista di sottotermini applicativi *)
let rec subterms = function
  | Tlam _ -> assert false
  | Tvar _ as v -> [v]
  | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2))
;;

(* filtra dai sottotermini le variabili *)
let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;


let rec stupid_uniq = function
  | [] -> []
  | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)
;;
let stupid_compare a b =
  let rec size = function
    | Tvar(_,None,_) -> 0
    | Tvar(_,Some(_,t),_) -> 1 + size t
    | Tapp(t1,t2) -> 1 + size t1 + size t2
    | Tlam _ -> assert false
  in compare (size a) (size b)
;;
let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);;

(* crea i match ricorsivamente.
  - k e' lo special-K
  - subs e' l'insieme dei sottotermini
  TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione
 *)
let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf =
  let req t = try List.assoc t acc with Not_found -> `Var 9999 in
  let aux t1 = (
  if t1 = dummy then `Var 99999 else
  (* let _ = print_term t1 in *)
  let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs
  in if cont = [] then
    try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else
  let a = alive (hd t1) in
    if a = 0 then `Lam (req (Tapp(t1, dummy)))
    else (
      let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero]
      (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))
      in let _ = print_term (mk_apps dummy vars) *)
      in let vars = List.map req vars
      in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *)
      in let vars = Listx.from_list vars
      in let body = `I(0, vars)
      in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont
      in let bs = ref(branches)
      in let lift = 1
      in let args = []
      in `Lam (`Match(body, lift, bs, args))
    )
  ) in aux
;;

let mk_zeros k =
  let rec aux n prev =
    if n = 0 then [zero]
    else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev
  in aux (k+1) []
;;

let is_scott_n t n =
  let open Lambda3 in let open Pure in
  let rec aux n = function
  | L (L (A (V 1, L (V 0)))) -> n = 0
  | L (L (A (V 0, t))) -> aux (n-1) t
  | _ -> assert false
  in aux n t
;;

(* do the magic *)
let magic strings k h = (
  let tms = parse strings
  in let tms = List.map (fun x -> Tapp(x, zero)) tms
  in let tms' = List.map (setalive h) tms
  in let tms' = List.map (translate k) tms'
  in let tms' = List.map dummize tms'
  (* in let bullet = ">" / "&bullet;" *)
  (* in let progress s = print_endline (bullet ^^ fancy_of_string s) *)
  in let progress = print_h1
  in let _ = progress "traduzione completata"
  (* in let _ = List.map print_term tms' *)
  in let _ = progress "ordino i sottotermini"
  in let subs = List.concat (List.map subterms tms')
  in let subs = stupid_sort_uniq subs
  (* metti gli zeri in testa, perche' vanno calcolati per primi *)
  in let zeros = mk_zeros k
  in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)
  in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs))
  in let vars = vars subs
  (* in let _ = List.iter print_term subs *)
  (* in let _ = 0/0 *)
  in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars
  (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *)
  in let _ = progress "sto creando i match"
  (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *)
  in let f t acc = let res = crea_match k subs acc t in (t,res)::acc
  in let acc = List.fold_right f subs []
  in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc
  in let _ = progress "match creati"
  in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " &#8614; ") ^^ fancy_of_nf y)) sigma

  in let _ = progress "controllo di purezza";
  in let open Lambda3
  in let ps, _ = Lambda3.parse' strings
  in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps
  in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps
  in let sigma = List.map (
    function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false
    ) sigma
  in let ps =
    List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma
  in let _ = List.iteri (fun i n ->
    (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *)
    (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *)
    assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps
  in let _ = progress "fatto." in ()
);;

let do_everything tms =
let tms' = parse tms in
let k = compute_special_k tms' in
let h = compute_special_h tms' in
(* let _ = print_string_endline (string_of_int h) in *)
magic tms k h
;;

let _ =
  let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in
  (* 1 2 *)
  (* let tms = ["x c" ; "b (x c d e)"; "b"] in *)
  (* 0 1 *)
  (* let tms = ["x x x"] in *)
  let tms' = parse tms in
  let k = compute_special_k tms' in
  let h = compute_special_h tms' in
  (* let _ = print_string_endline (string_of_int h) in *)
  magic tms k h
;;

(* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option
and term' =
  | Tvar' of var'
  | Tapp' of term' * term' * (* active *) bool
  | Tlam' of int * term'
;;

let rec iter mustapply =
  let aux = function
  | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b)
  | Tvar' _ as v -> v
  | Tapp'(t1, t2, b) -> if b &&
  in aux
;; *)

*)