ocaml/lambda3.ml.ar

   1 open Util
   2 open Util.Vars
   3 open Pure
   4 open Num
   5
   6 type problem =
   7  { freshno: int
   8  ; ps: i_n_var list (* the n-th inert must become n *)
   9  ; sigma: (int * nf) list (* the computed substitution *)
  10  ; deltas: (int * nf) list ref list (* collection of all branches *)
  11  }
  12
  13 let print_problem {freshno; ps; deltas} =
  14  let deltas = String.concat "\n" (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
  15  let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
  16  deltas ^ (if deltas = "" then "" else "\n") ^
  17  String.concat "\n" (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps)
  18 ;;
  19
  20 let make_fresh_var freshno =
  21  freshno+1, freshno+1
  22
  23 let make_fresh_vars p m =
  24  let rec aux =
  25   function
  26      0 -> p.freshno,[]
  27    | n when n > 0 ->
  28       let freshno,vars = aux (n-1) in
  29       let freshno,v = make_fresh_var freshno in
  30       freshno,`Var (0,v)::vars
  31    | _ -> assert false in
  32  let freshno,vars = aux m in
  33  {p with freshno}, vars
  34
  35 let simple_expand_match ps =
  36   let rec aux level = function
  37   | #i_num_var as t -> aux_i_num_var level t
  38   | `Lam(b,t) -> `Lam(b, aux (level+1) t)
  39   and aux_i_num_var level = function
  40   | `Match(ar,u,bs_lift,bs,args) as torig ->
  41     let u = aux_i_num_var level u in
  42     bs := List.map (fun (n, x) -> n, aux 0 x) !bs;
  43     (try
  44        (match u with
  45          | #i_n_var as u ->
  46             let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *)
  47             in let t = mk_match ar (`N i) bs_lift bs args in
  48             if t <> torig then
  49             aux level (t :> nf)
  50            else raise Not_found
  51          | _ -> raise Not_found)
  52       with Not_found ->
  53        `Match(ar,cast_to_i_num_var u,bs_lift,bs,List.map (aux level) args))
  54   | `I(ar,k,args) -> `I(ar,k,Listx.map (aux level) args)
  55   | `N _ | `Var _ as t -> t
  56 in aux_i_num_var 0;;
  57
  58 let rec super_simplify_ps ps it =
  59   let it' = List.map (fun t -> cast_to_i_num_var (simple_expand_match ps t)) (it :> i_num_var list) in
  60   if it <> it' then super_simplify_ps ps it' else it'
  61
  62 let super_simplify ({ps} as p) =
  63   let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in
  64   {p with ps=List.map cast_to_i_n_var ps}
  65
  66 let subst_in_problem x inst ({freshno; ps; sigma} as p) =
  67  let len_ps = List.length ps in
  68 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
  69 prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
  70   let rec aux ((freshno,acc_ps,acc_new_ps) as acc) =
  71    function
  72       [] -> acc
  73     | t::todo_ps ->
  74 (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
  75        let t = subst false x inst (t :> nf) in
  76 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
  77        let freshno,new_t,acc_new_ps =
  78         expand_match (freshno,acc_ps@`Var(-1,max_int/3)::todo_ps,acc_new_ps) t
  79        in
  80         aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
  81
  82   and expand_match ((freshno,acc_ps, acc_new_ps) as acc) t =
  83    match t with
  84     | `Match(ar,u',bs_lift,bs,args) ->
  85         let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in
  86         let acc_new_ps,i =
  87          match u with
  88             `N i -> acc_new_ps,i
  89           | _ ->
  90             let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in
  91             let super_simplified_ps = super_simplify_ps ps ps in
  92 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
  93 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;
  94 List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*)
  95             match index_of_opt ~eq:eta_eq super_simplified_ps u with
  96                Some i -> acc_new_ps, i
  97              | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps
  98         in
  99          let freshno=
 100           if List.exists (fun (j,_) -> i=j) !bs then
 101            freshno
 102           else
 103            let freshno,v = make_fresh_var freshno in
 104            bs := !bs @ [i, `Var (ar - 1,v)] ;
 105            freshno in
 106 (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*)
 107          let t = mk_match ar (`N i) bs_lift bs args in
 108 (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
 109           expand_match (freshno,acc_ps,acc_new_ps) t
 110     | `Lam _ ->
 111          (* the cast will fail *)
 112          (* freshno,(cast_to_i_n_var t),acc_new_ps *)
 113          assert false
 114     | #i_n_var as x ->
 115        let x = simple_expand_match (acc_ps@acc_new_ps) x in
 116        freshno,cast_to_i_num_var x,acc_new_ps in
 117   let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in
 118   let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in
 119 (let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
 120 prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst));
 121   let p = {p with freshno; ps; sigma = sigma@[x,inst]} in
 122   let p = super_simplify p in
 123 prerr_endline (print_problem p); p
 124
 125 exception Dangerous
 126
 127 let rec dangerous arities showstoppers =
 128  function
 129     `N _
 130   | `Var _
 131   | `Lam _ -> ()
 132   | `Match(_,t,liftno,bs,args) ->
 133       (* CSC: XXX partial dependency on the encoding *)
 134       (match t with
 135           `N _ -> List.iter (dangerous arities showstoppers) args
 136         | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args
 137         | `Var (_,x) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *)
 138         | `I(_,x,args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *)
 139       )
 140   | `I(_,k,args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0
 141
 142 and dangerous_inert arities showstoppers k args more_args =
 143  List.iter (dangerous arities showstoppers) args ;
 144  if List.mem k showstoppers then raise Dangerous else
 145  try
 146   let _,_,y = List.find (fun (v,_,_) -> v=k) arities in
 147   let arity = match y with `Var _ -> 0 | `I(_,_,args) -> Listx.length args | _ -> assert false in
 148   if List.length args + more_args > arity then raise Dangerous else ()
 149  with
 150   Not_found -> ()
 151
 152 (* inefficient algorithm *)
 153 let edible arities showstoppers ps =
 154  let rec aux showstoppers =
 155   function
 156      [] -> showstoppers
 157    | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers ->
 158       (* se la testa di x e' uno show-stopper *)
 159       let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in
 160       (* aggiungi tutte le variabili libere di x *)
 161       if List.length showstoppers <> List.length new_showstoppers then
 162        aux new_showstoppers ps
 163       else
 164        aux showstoppers xs
 165    | x::xs ->
 166       match hd_of x with
 167          None -> aux showstoppers xs
 168        | Some h ->
 169           try
 170            dangerous arities showstoppers (x : i_n_var :> nf) ;
 171            aux showstoppers xs
 172           with
 173            Dangerous ->
 174             aux (sort_uniq (h::showstoppers)) ps
 175  in
 176   aux showstoppers ps
 177
 178 let precompute_edible_data {ps} xs =
 179  List.map (fun x ->
 180   let y = List.find (fun y -> hd_of y = Some x) ps in
 181   x, index_of ~eq:eta_eq y ps, y) xs
 182 ;;
 183
 184 let critical_showstoppers p =
 185   let p = super_simplify p in
 186   let showstoppers_step =
 187   List.concat (List.map (fun bs ->
 188     let heads = List.map (fun (i,_) -> List.nth p.ps i) !bs in
 189     let heads = List.sort compare (filter_map hd_of heads) in
 190     snd (split_duplicates heads)
 191     ) p.deltas) in
 192   let showstoppers_step = sort_uniq showstoppers_step in
 193   let showstoppers_eat =
 194    let heads_and_arities =
 195     List.sort (fun (k,_) (h,_) -> compare k h)
 196      (filter_map (function `Var (_,k) -> Some (k,0) | `I(_,k,args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in
 197    let rec multiple_arities =
 198     function
 199        []
 200      | [_] -> []
 201      | (x,i)::(y,j)::tl when x = y && i <> j ->
 202          x::multiple_arities tl
 203      | _::tl -> multiple_arities tl in
 204    multiple_arities heads_and_arities in
 205
 206   let showstoppers_eat = sort_uniq showstoppers_eat in
 207   let showstoppers_eat = List.filter
 208     (fun x -> not (List.mem x showstoppers_step))
 209     showstoppers_eat in
 210   List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ string_of_var v)) showstoppers_step;
 211   List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ string_of_var v)) showstoppers_eat;
 212   p, showstoppers_step, showstoppers_eat
 213   ;;
 214
 215 let eat p =
 216   let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
 217   let showstoppers = showstoppers_step @ showstoppers_eat in
 218   let heads = List.sort compare (filter_map hd_of ps) in
 219   let arities = precompute_edible_data p (uniq heads) in
 220   let showstoppers = edible arities showstoppers ps in
 221   let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
 222   let p =
 223   List.fold_left (fun p (x,pos,(xx : i_n_var)) ->
 224    let n = match xx with `I(_,_,args) -> Listx.length args | _ -> 0 in
 225    let v = `N(pos) in
 226    let inst = make_lams v n in
 227 (let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in
 228  prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst));
 229    (* CSC: XXX to avoid applied numbers in safe positions that
 230       trigger assert failures subst_in_problem x inst p*)
 231    { p with sigma = p.sigma @ [x,inst] }
 232   ) p l in
 233  let ps =
 234   List.map (fun t ->
 235    try
 236     let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in
 237     `N j
 238    with Not_found -> t
 239   ) ps in
 240  List.iter
 241   (fun bs ->
 242     bs :=
 243      List.map
 244       (fun (n,t as res) ->
 245         match List.nth ps n with
 246            `N m -> m,t
 247          | _ -> res
 248       ) !bs
 249   ) p.deltas ;
 250  let p = { p with ps } in
 251  if l <> [] then prerr_endline (print_problem p);
 252  if List.for_all (function `N _ -> true | _ -> false) ps then
 253   `Finished p
 254  else
 255   `Continue p
 256
 257 let instantiate p x n =
 258   let p,vars = make_fresh_vars p n in
 259   let freshno,zero = make_fresh_var p.freshno in
 260   let p = {p with freshno} in
 261   let zero = Listx.Nil (`Var (0,zero)) in
 262   let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in
 263   let bs = ref [] in
 264   let inst = `Lam(false,`Match(-1,`I(-1,0,Listx.map (lift 1) args),1,bs,[])) in
 265   let p = {p with deltas=bs::p.deltas} in
 266   subst_in_problem x inst p
 267 ;;
 268
 269 let compute_special_k tms =
 270   let rec aux k (t: nf) = Pervasives.max k (match t with
 271     | `Lam(b,t) -> aux (k + if b then 1 else 0) t
 272     | `I(_, n, tms) -> Listx.max (Listx.map (aux 0) tms)
 273     | `Match(_, t, liftno, bs, args) ->
 274         List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
 275     | `N _ -> 0
 276     | `Var _ -> 0
 277   ) in Listx.max (Listx.map (aux 0) tms)
 278 ;;
 279
 280 let auto_instantiate (n,p) =
 281   let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
 282  let x =
 283   match showstoppers_step, showstoppers_eat with
 284     | [], y::_ ->
 285       prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
 286     | [], [] ->
 287      let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ps) in
 288      (match heads with
 289          [] -> assert false
 290        | x::_ ->
 291           prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
 292           x)
 293   | x::_, _ ->
 294       prerr_endline ("INSTANTIATING " ^ string_of_var x);
 295       x in
 296 (* Strategy that decreases the special_k to 0 first (round robin)
 297 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
 298 let x =
 299  try
 300   (match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0) ps) with
 301       None -> assert false
 302     | Some x ->
 303        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
 304        x)
 305  with
 306   Not_found -> x
 307 in
 308 (* Instantiate in decreasing order of compute_special_k
 309 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
 310 let x =
 311  try
 312   (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) ps)))) with
 313       None -> assert false
 314     | Some x ->
 315        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
 316        x)
 317  with
 318   Not_found -> x
 319 in*)
 320  let special_k =
 321      compute_special_k (Listx.from_list (p.ps :> nf list) )in
 322  if special_k < n then
 323   prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@");
 324  let p = instantiate p x special_k in
 325  special_k,p
 326
 327 let problem_measure {ps} =
 328   (* let rec term_size_i_n_var =
 329     function
 330     | `I(v,nfs) ->
 331       (Listx.length nfs) *
 332       (List.fold_right (fun (a,b) c -> 10 + ((a+1) * term_size b) + c) (List.mapi (fun x y -> (x,y)) (Listx.to_list nfs)) 0)
 333     | `Var _ -> 1
 334     | `N _ -> 0
 335   and term_size =
 336     function
 337     | #i_n_var as t -> term_size_i_n_var t
 338     | `Match(t,lift,bs,args) -> 1 + (term_size (t :> nf)) + 1 + (List.fold_right ((+) ++ term_size) args 0)
 339     | `Lam(b,t) -> (if b then 0 else 1) + term_size t
 340   (* in List.fold_right ((+) ++ term_size_i_n_var) ps 0;; *)
 341   in ... *)
 342   0
 343
 344 let rec auto_eat (n,({ps} as p)) =
 345  match eat p with
 346     `Finished p -> p
 347   | `Continue p ->
 348     let p' = auto_instantiate (n,p) in
 349     let m' = problem_measure (snd p') in
 350     let delta = m' - problem_measure p in
 351     (if delta >= 0
 352     then print_endline ("$$$$ MEASURE DID NOT DECREASE (after inst) delta=" ^ string_of_int delta));
 353     let p'' = auto_eat p' in
 354     (if m' <= problem_measure p''
 355     then print_endline ("$$$$ MEASURE DID NOT DECREASE (after eat) $$$"));
 356     p''
 357 ;;
 358
 359 let auto p n =
 360  prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@");
 361  auto_eat (n,p)
 362 ;;
 363
 364 (*
 365 0 = snd
 366
 367       x y = y 0    a y = k  k z = z 0  c y = k   y u = u h1 h2 0          h2 a = h3
 368 1 x a c    1 a 0 c  1 k c    1 c 0      1 k        1 k                     1 k
 369 2 x a y    2 a 0 y  2 k y    2 y 0      2 y 0      2 h2 0                  2 h3
 370 3 x b y    3 b 0 y  3 b 0 y  3 b 0 y    3 b 0 y    3 b 0 (\u. u h1 h2 0)   3 b 0 (\u. u h1 (\w.h3) 0)
 371 4 x b c    4 b 0 c  4 b 0 c  4 b 0 c    4 b 0 c    4 b 0 c                 4 b 0 c
 372 5 x (b e)  5 b e 0  5 b e 0  5 b e 0    5 b e 0    5 b e 0                 5 b e 0
 373 6 y y      6 y y    6 y y    6 y y      6 y y      6 h1 h1 h2 0 h2 0       6 h1 h1 (\w. h3) 0 (\w. h3) 0
 374
 375                                 l2 _ = l3
 376 b u = u l1 l2 0                 e _ _ _ _ = f                         l3 n = n j 0
 377 1 k                             1 k                                  1 k
 378 2 h3                            2 h3                                 2 h3
 379 3 l2 0 (\u. u h1 (\w. h3) 0)    3 l3 (\u. u h1 (\w. h3) 0)           3 j h1 (\w. h3) 0 0
 380 4 l2 0 c                        4 l3 c                               4 c j 0
 381 5 e l1 l2 0 0                   5 f                                  5 f
 382 6 h1 h1 (\w. h3) 0 (\w. h3) 0   6 h1 h1 (\w. h3) 0 (\w. h3) 0        6 h1 h1 (\w. h3) 0 (\w. h3) 0
 383 *)
 384
 385 (*
 386                 x n = n 0 ?
 387 x a (b (a c))   a 0 = 1 ? (b (a c))   8
 388 x a (b d')      a 0 = 1 ? (b d')      7
 389 x b (a c)       b 0 = 1 ? (a c)       4
 390 x b (a c')      b 0 = 1 ? (a c')      5
 391
 392 c = 2
 393 c' = 3
 394 a 2 = 4  (* a c *)
 395 a 3 = 5  (* a c' *)
 396 d' = 6
 397 b 6 = 7  (* b d' *)
 398 b 4 = 8  (* b (a c) *)
 399 b 0 = 1
 400 a 0 = 1
 401 *)
 402
 403 (************** Tests ************************)
 404
 405 let optimize_numerals p =
 406   let replace_in_sigma perm =
 407     let rec aux = function
 408     | `N n -> `N (List.nth perm n)
 409     | `I _ | `Var _ -> assert false
 410     | `Lam(v,t) -> `Lam(v, aux t)
 411     | `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
 412     in List.map (fun (n,t) -> (n,aux t))
 413   in
 414   let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in
 415   let maxs = Array.to_list (Array.init (List.length deltas') (fun _ -> 0)) in
 416   let max = Listx.max (Listx.from_list (
 417     List.concat (List.map snd deltas')
 418   )) in
 419   let perm,_ = List.fold_left (fun (perm, maxs) (curr_n:int) ->
 420       let containing = filter_map (fun (i, bs) -> if List.mem curr_n bs then Some i else None) deltas' in
 421       (* (prerr_endline (string_of_int curr_n ^ " occurs in: " ^ (String.concat " " (List.map string_of_int containing)))); *)
 422       let neww = Listx.max (Listx.from_list (List.mapi (fun n max -> if List.mem n containing then max else 0) maxs)) in
 423       let maxs = List.mapi (fun i m -> if List.mem i containing then neww+1 else m) maxs in
 424       (neww::perm, maxs)
 425     ) ([],maxs) (Array.to_list (Array.init (max+1) (fun x -> x))) in
 426   replace_in_sigma (List.rev perm) p.sigma
 427 ;;
 428
 429 prerr_endline "########## main ##########";;
 430
 431 (* Commands:
 432     v ==> v := \a. a k1 .. kn \^m.0
 433     + ==> v := \^k. numero  for every v such that ...
 434     * ==> tries v as long as possible and then +v as long as possible
 435 *)
 436 let main problems =
 437  let rec aux ({ps} as p) n l =
 438   if List.for_all (function `N _ -> true | _ -> false) ps then begin
 439    assert (l = []);
 440    p
 441   end else
 442    let _ = prerr_endline (print_problem p) in
 443    let x,l =
 444     match l with
 445      | cmd::l -> cmd,l
 446      | [] -> read_line (),[] in
 447    let cmd =
 448     if x = "+" then
 449      `DoneWith
 450     else if x = "*" then
 451      `Auto
 452     else
 453      `Step x in
 454    match cmd with
 455     | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *)
 456     | `Step x ->
 457         let x = var_of_string x in
 458         aux (instantiate p x n) n l
 459     | `Auto -> aux (auto p n) n l
 460  in
 461   List.iter
 462    (fun (p,n,cmds) ->
 463      let p_finale = aux p n cmds in
 464      let freshno,sigma = p_finale.freshno, p_finale.sigma in
 465      prerr_endline "------- <DONE> ------";
 466      prerr_endline (print_problem p);
 467      prerr_endline "---------------------";
 468      let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
 469      List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
 470 (*
 471      prerr_endline "----------------------";
 472      let ps =
 473       List.fold_left (fun ps (x,inst) ->
 474        (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *)
 475        (* In this non-recursive version, the intermediate states may containt Matchs *)
 476        List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps)
 477        (p.ps :> i_num_var list) sigma in
 478      prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
 479      List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ;
 480 *)
 481      prerr_endline "---------<OPT>----------";
 482      let sigma = optimize_numerals p_finale in (* optimize numerals *)
 483      let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
 484      List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
 485      prerr_endline "---------<PURE>---------";
 486      let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in
 487      let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
 488      (*let ps_ok = List.fold_left (fun ps (x,inst) ->
 489        List.map (Pure.subst false x inst) ps) ps sigma in*)
 490      let e =
 491       let rec aux n =
 492        if n > freshno then
 493         []
 494        else
 495         let e = aux (n+1) in
 496         (try
 497          e,Pure.lift (-n-1) (let t = (snd (List.find (fun (i,_) -> i = n) sigma)) in prerr_endline (string_of_var n ^ " := " ^ Pure.print t); t),[]
 498         with
 499          Not_found -> [],Pure.V n,[])::e
 500       in
 501        aux 0 in
 502 (*
 503      prerr_endline "---------<PPP>---------";
 504 let rec print_e e =
 505  "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]"
 506 in
 507      prerr_endline (print_e e);
 508      List.iter (fun (t,t_ok) ->
 509       prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok);
 510       (*assert (Pure.unwind (e,t,[]) = t_ok)*)
 511      ) (List.combine ps ps_ok);
 512 *)
 513      prerr_endline "--------<REDUCE>---------";
 514      List.iteri (fun i n ->
 515        (*prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));*)
 516        let t = Pure.mwhd (e,n,[]) in
 517        prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t));
 518        assert (t = Scott.mk_n i)
 519      ) ps ;
 520      prerr_endline "-------- </DONE> --------"
 521    ) problems
 522
 523 (********************** problems *******************)
 524
 525 let zero = `Var (0,0);;
 526
 527 let append_zero =
 528  function
 529   | `I _
 530   | `Var _ as i ->  cast_to_i_n_var (mk_app i zero)
 531   | _ -> assert false
 532 ;;
 533
 534 type t = problem * int * string list;;
 535
 536 let magic strings cmds =
 537   let tms, _ = parse' strings in (*  *)
 538   let tms = sort_uniq ~compare:eta_compare tms in
 539   let special_k = compute_special_k (Listx.from_list tms) in (* compute special K *)
 540   let fv = sort_uniq (List.concat (List.map free_vars tms)) in (* free variables *)
 541   let tms = List.map cast_to_i_n_var tms in (* cast nf list -> i_n_var list *)
 542   let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *)
 543   (*let _ =  prerr_endline ("Free vars: " ^ String.concat ", " (List.map string_of_var fv)) in*)
 544   let freshno = Listx.max (Listx.from_list fv) in
 545   let dummy = `Var (-1,max_int / 2) in
 546   let deltas = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
 547   {freshno; ps; sigma=[] ; deltas}, special_k, cmds
 548 ;;
 549
 550 let magic_conv ~div:_ ~conv:_ ~nums:_ _ = assert false;;