From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 13 Jul 2017 15:38:23 +0000 (+0200)
Subject: Tentative commit: tactics dropped and clean-up
X-Git-Tag: weak-reduction-separation~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=978648853f982a5e5755f084fb22342fdbb3534e;p=fireball-separation.git

Tentative commit: tactics dropped and clean-up

(cherry picked from commit 0991fc5486c3158fc361e84cbba5aefa67893ba4)

Include codice di pure.ml che implementa Pure.B da commit
 "Removed bomb variable"
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 715caf5..c376f01 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -11,6 +11,11 @@ let bomb = ref(`Var(-1,-666));;
  For Scott's encoding, two.
 *)
 let num_more_args = 2;;
+let _very_verbose = false;;
+
+let verbose s =
+ if _very_verbose then prerr_endline s
+;;
 
 let convergent_dummy = `N ~-1;
 
@@ -58,7 +63,7 @@ let string_of_measure (a,b) = "(fakevars="^string_of_int a^",sum_arities="^strin
 let problem_measure p = sum_arities p;;
 let string_of_measure = string_of_int;;
 
-let print_problem label ({freshno; div; conv; ps; deltas} as p) =
+let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
  Console.print_hline ();
  prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - ");
  let nl = "\n" in
@@ -79,7 +84,7 @@ let print_problem label ({freshno; div; conv; ps; deltas} as p) =
 
 
 let failwithProblem p reason =
- print_endline (print_problem "FAIL" p);
+ print_endline (string_of_problem "FAIL" p);
  failwith reason
 ;;
 
@@ -227,7 +232,7 @@ prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst));
  );
  let p = {p with sigma = sigma@[x,inst]} in
  let p = super_simplify p in
- prerr_endline (print_problem "instantiate" p);
+ prerr_endline (string_of_problem "instantiate" p);
  p
 ;;
 
@@ -450,7 +455,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
  let old_conv = p.conv in
  let p = { p with ps; conv } in
  if l <> [] || old_conv <> conv
-  then prerr_endline (print_problem "eat" p);
+  then prerr_endline (string_of_problem "eat" p);
  if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then
   `Finished p
  else
@@ -655,107 +660,80 @@ let env_of_sigma freshno sigma should_explode =
  in aux 0
 ;;
 
-prerr_endline "########## main ##########";;
-
-(* Commands:
-    v ==> v := \a. a k1 .. kn \^m.0
-    + ==> v := \^k. numero  for every v such that ...
-    * ==> tries v as long as possible and then +v as long as possible
-*)
-let main problems =
- let rec aux ({ps} as p) n l =
-  if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then begin
-   p
-  end else
-   let _ = prerr_endline (print_problem "main" p) in
-   let x,l =
-    match l with
-     | cmd::l -> cmd,l
-     | [] -> read_line (),[] in
-   let cmd =
-    if x = "+" then
-     `DoneWith
-    else if x = "*" then
-     `Auto
-    else
-     `Step x in
-   match cmd with
-    | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *)
-    | `Step x ->
-        let x = var_of_string x in
-        aux (instantiate p x n) n l
-    | `Auto -> aux (auto p n) n l
- in
-  List.iter
-   (fun (p,n,cmds) ->
-    Console.print_hline();
-    bomb := `Var (-1,-666);
-    let p_finale = aux p n cmds in
-    let freshno,sigma = p_finale.freshno, p_finale.sigma in
-    prerr_endline ("------- <DONE> ------\n ");
-    (* prerr_endline (print_problem "Original problem" p); *)
-    prerr_endline "---------------------";
-    let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
-    prerr_endline (" BOMB == " ^ print ~l !bomb);
-    prerr_endline "---------------------";
-    List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
+let solve p  =
+ bomb := `Var(-1,-666);
+ if List.for_all (function `N _ -> true | _ -> false) p.ps && p.div = None
+  then (prerr_endline "Initial problem is already completed, nothing to do")
+  else (
+  Console.print_hline();
+  prerr_endline (string_of_problem "main" p);
+  let p_finale = auto p p.initialSpecialK in
+  let freshno,sigma = p_finale.freshno, p_finale.sigma in
+  prerr_endline ("------- <DONE> ------ measure=. \n ");
+  (* prerr_endline (string_of_problem "Original problem" p); *)
+  (* prerr_endline "---------------------"; *)
+  let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
+  (* prerr_endline "---------------------"; *)
+  List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
 (*
-     prerr_endline "----------------------";
-     let ps =
-      List.fold_left (fun ps (x,inst) ->
-       (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *)
-       (* In this non-recursive version, the intermediate states may containt Matchs *)
-       List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps)
-       (p.ps :> i_num_var list) sigma in
-     prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
-     List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ;
+   prerr_endline "----------------------";
+   let ps =
+    List.fold_left (fun ps (x,inst) ->
+     (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *)
+     (* In this non-recursive version, the intermediate states may containt Matchs *)
+     List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps)
+     (p.ps :> i_num_var list) sigma in
+   prerr_endline (string_of_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
+   List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ;
 *)
-    prerr_endline "---------<OPT>----------";
-    let sigma = optimize_numerals p_finale in (* optimize numerals *)
-    let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
-    List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
-    prerr_endline "---------<PURE>---------";
-    let div = option_map (fun div -> ToScott.t_of_nf (div :> nf)) p.div in
-    let conv = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.conv in
-    let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in
-    let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
-    (*let ps_ok = List.fold_left (fun ps (x,inst) ->
-      List.map (Pure.subst false x inst) ps) ps sigma in*)
-    let e = env_of_sigma freshno sigma true in
-    let e' = env_of_sigma freshno sigma false in
+  prerr_endline "---------<OPT>----------";
+  let sigma = optimize_numerals p_finale in (* optimize numerals *)
+  let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
+  List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
+
+  prerr_endline "---------<PURE>---------";
+  let t_of_nf t = ToScott.t_of_nf (t :> nf) in
+  let div = option_map t_of_nf p.div in
+  let conv = List.map t_of_nf p.conv in
+  let ps = List.map t_of_nf p.ps in
+
+  let sigma' = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
+  let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in
 
 (*
-     prerr_endline "---------<PPP>---------";
+   prerr_endline "---------<PPP>---------";
 let rec print_e e =
- "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]"
+"[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]"
 in
-     prerr_endline (print_e e);
-     List.iter (fun (t,t_ok) ->
-      prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok);
-      (*assert (Pure.unwind (e,t,[]) = t_ok)*)
-     ) (List.combine ps ps_ok);
+   prerr_endline (print_e e);
+   List.iter (fun (t,t_ok) ->
+    prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok);
+    (*assert (Pure.unwind (e,t,[]) = t_ok)*)
+   ) (List.combine ps ps_ok);
 *)
-     prerr_endline "--------<REDUCE>---------";
-     (function Some div ->
-      print_endline (Pure.print div);
-      let t = Pure.mwhd (e',div,[]) in
-      prerr_endline ("*:: " ^ (Pure.print t));
-      prerr_endline (print !bomb);
-      assert (t = ToScott.t_of_nf (!bomb:>nf))
-     | None -> ()) div;
-     List.iter (fun n ->
-       prerr_endline ("_::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
-       prerr_endline ("_:: " ^ (Pure.print t))
-     ) conv ;
-     List.iteri (fun i n ->
-       prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
-       prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t));
-       assert (t = Scott.mk_n i)
-     ) ps ;
-     prerr_endline "-------- </DONE> --------"
-   ) problems
+  prerr_endline "--------<REDUCE>---------";
+  let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *)
+  (function Some div ->
+   print_endline (Pure.print div);
+   let t = Pure.mwhd (e',div,[]) in
+   prerr_endline ("*:: " ^ (Pure.print t));
+   assert (t = pure_bomb)
+  | None -> ()) div;
+  List.iter (fun n ->
+    verbose ("_::: " ^ (Pure.print n));
+    let t = Pure.mwhd (e',n,[]) in
+    verbose ("_:: " ^ (Pure.print t));
+    assert (t <> pure_bomb)
+  ) conv ;
+  List.iteri (fun i n ->
+    verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));
+    let t = Pure.mwhd (e',n,[]) in
+    verbose ((string_of_int i) ^ ":: " ^ (Pure.print t));
+    assert (t = Scott.mk_n i)
+  ) ps ;
+  prerr_endline "-------- </DONE> --------"
+ )
+;;
 
 (********************** problems *******************)
 
@@ -768,10 +746,8 @@ let append_zero =
   | _ -> assert false
 ;;
 
-type t = problem * int * string list;;
-
-let magic_conv ~div ~conv ~nums cmds =
- let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in
+let problem_of ~div ~conv ~nums =
+ let all_tms = (match div with None -> [] | Some div -> print_endline(div);[div]) @ nums @ conv in
   let all_tms, var_names = parse' all_tms in
   let div, (tms, conv) = match div with
     | None -> None, list_cut (List.length nums, all_tms)
@@ -780,22 +756,32 @@ let magic_conv ~div ~conv ~nums cmds =
  if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv)
  then (
   prerr_endline "--- TEST SKIPPED ---";
-  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}, 0, []
+  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}
  ) else
   let tms = sort_uniq ~compare:eta_compare tms in
   let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
   (* casts *)
-  let div = option_map cast_to_i_var div in
-  let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in
-  let tms = List.map cast_to_i_n_var tms in
+  let div =
+   match div with
+    | None -> None
+    | Some (`I _ as t) -> Some t
+    | _ -> raise (Failure "div is not an inert or BOT in the initial problem") in
+  let conv = Util.filter_map (
+   function
+   | #i_n_var as t -> Some t
+   | `Lam _ -> None
+   | _ -> raise (Failure "A term in conv is not i_n_var")
+   ) conv in
+  let tms = List.map (
+   function
+    | #i_n_var as y -> y
+    | _ -> raise (Failure "A term in num is not i_n_var")
+   ) tms in
 
   let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *)
   let freshno = List.length var_names in
   let deltas =
    let dummy = `Var (max_int / 2, -666) in
     [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
-
-  {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}, special_k, cmds
+  {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}
 ;;
-
-let magic strings cmds = magic_conv None [] strings cmds;;
diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index c8a571e..761bef6 100644
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -1,4 +1,3 @@
-type t
-val magic: string list -> string list -> t
-val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t
-val main: t list -> unit
+type problem
+val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem
+val solve: problem -> unit
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 2a99a5c..22b9d76 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,149 +1,150 @@
 open Lambda4;;
+let magic strings = problem_of None [] strings;;
+let solve_many = List.iter solve;;
 
-let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"]
+let p2 = magic [ "x y"; "x z" ; "x (y z)"]
 
 let p4 = magic
-  [ "x y"; "x (a. a x)" ; "y (y z)" ] ["*"]
+  [ "x y"; "x (a. a x)" ; "y (y z)" ]
 
 let p5 = magic
   ["a (x. x a) b"; "b (x. x b) a"]
-  ["*"]
 ;;
 
 let p6 = magic
   ["a (x. x a) b"; "b (x. x b) (c a)"]
-  ["*"]
+
 ;;
 
 let p7 = magic
   ["a (x. (x a)(a x x a)(x x) )"]
-  ["*"]
+
 ;;
 
 let p8 = magic
   ["x x (x x)"]
-  ["*"]
+
 ;;
 
 let p9 = magic
   ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]
-  ["*"]
+
 ;;
 
 let p10 = magic
   ["x (y (x a b c))"]
-  ["*"]
+
 ;;
 
 let p11 = magic
   ["x x"; "x (y.y)"]
-  ["*"]
+
 ;;
 
 let p12 = magic
   ["x x (x x)"; "x x (x (y.y))"]
-  ["*"]
+
 ;;
 
 let p13 = magic
   ["x x (x x (x x x x x (x x)))"]
-  ["*"]
+
 ;;
 
 let p14 = magic
   ["a (a a (a (a a)) (a (a a)))"]
-  ["*"]
+
 ;;
 
 let p15 = magic
   ["a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))"]
-  ["*"]
+
 ;;
 
 let p16 = magic
   ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]
-  ["*"]
+
 ;;
 
 let p17 = magic
   ["b a"; "b (c.a)"]
-  ["*"]
+
 ;;
 
 let p18 = magic
   ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]
-  ["*"]
+
 ;;
 
 let p19 = magic
   ["a (a a) (a a a (a (a (a a) a)) a)"]
-  ["*"]
+
 ;;
 
 let p20 = magic
-  ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"]["*"];;
+  ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"];;
 
 let p21 = magic
   ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))";
    "(((z z) x) (y z))";
    "((z (y z)) ((y z) (z z)))"
-] ["*"];;
+] ;;
 
 let p22 = magic
 ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
 "((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))";
-"(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ["*"];;
+"(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ;;
 
 (* diverging tests *)
 (* test p23 leads to test p24 *)
 let p23 = magic
-["z z z"; "z (z z) (x. x)"] ["*"];;
+["z z z"; "z (z z) (x. x)"] ;;
 
 (* because of the last term, the magic number is 1 and we diverge;
    but setting the magic number to 0 allows to solve the problem;
    thus our strategy is incomplete *)
 let p24 = magic
-["b b"; "b f"; "f b"; "a (x.x)"] ["*"];;
+["b b"; "b f"; "f b"; "a (x.x)"] ;;
 
 (* because of the last term, the magic number is 1 and we diverge;
    but setting the magic number to 0 allows to solve the problem;
    thus our strategy is incomplete *)
 let p25 = magic
-["b b"; "b f"; "f b"; "f (x.x)"] ["*"];;
+["b b"; "b f"; "f b"; "f (x.x)"] ;;
 
 (* BUG:
    0 (n (d (o.n) ...)))
    After instantiating n, the magic number (for d) should be 2, not 1! *)
 let p26 = magic
 ["(((x y) (z. (y. (y. z)))) (z. y))";
-"(((x y) x) (y y))"] ["*"];;
+"(((x y) x) (y y))"] ;;
 
 let p27 = magic
 ["(((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))";
 "((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))";
-"(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ["*"];;
+"(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ;;
 
 let p28 = magic
 ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
- "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ["*"];;
+ "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ;;
 
 let p29 = magic
 ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
-"(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ["*"];;
+"(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ;;
 
 let p30 = magic
 ["((b c) (b. (z a)))";
 "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
 "((v (v. c)) z)";
 "((v y) (v (a. (z v))))";
-"((y (b c)) ((z a) (v y)))"] ["*"];;
+"((y (b c)) ((z a) (v y)))"] ;;
 
 let p31 = magic
 [" (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))";
 "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
 "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
 "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
-"((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ["*"];;
+"((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ;;
 
 let p32 = magic
 ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
@@ -151,7 +152,7 @@ let p32 = magic
 "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
 "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
 "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
-] ["*"];;
+] ;;
 
 (* Shows an error when the strategy that minimizes special_k is NOT used *)
 let p33 = magic
@@ -161,7 +162,7 @@ let p33 = magic
 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))";
 (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
-] ["*"];;
+] ;;
 
 let p34 = magic [
 "b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a";
@@ -169,7 +170,7 @@ let p34 = magic [
 "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
 "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
 "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
-] ["*"];;
+] ;;
 (* 0: (b c (b c) (c (d j.e)) (b c (b c) j.(c f)) (b f j.k.d) (b j.k.l.(b c (b c)) (b g)) a)
 1: (d j.e e j.(c f) j.(c j) b a)
 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
@@ -180,59 +181,59 @@ let p35 = magic [
 "(((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))";
 "((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))";
 "((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))"
-] ["*"];;
+] ;;
 
 let p36 = magic
 [
 "(((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))";
 "(((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))";
 "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"
-] ["*"];;
+] ;;
 
 (* issue with eta-equality of terms in ps *)
 let p37 = magic
   ["x (a y) z"; "x (a z. y z) w"; "a c"]
-  ["*"];;
+  ;;
 
 (**********************)
 
-let q1 () = magic_conv
+let q1 () = problem_of
  None
  ["a d e"]
  ["a b"; "a c"]
- ["*"];;
+ ;;
 
-let q2 () = magic_conv
+let q2 () = problem_of
  None
  ["a d e"]
  ["a b" ]
- ["*"];;
+ ;;
 
-let q3 () = magic_conv
+let q3 () = problem_of
  (Some "x")
  ["a d e f"]
  ["a b" ]
- ["*"];;
+ ;;
 
-let q4 () = magic_conv
+let q4 () = problem_of
  None
  ["f (x.a b c d)"]
  ["a b" ]
- ["*"];;
+ ;;
 
-let q5 () = magic_conv
+let q5 () = problem_of
  (Some"x")
  ["(y. x)"]
  ["x"]
- ["*"];;
+ ;;
 
-let q6 () = magic_conv
+let q6 () = problem_of
  (Some"x")
  ["(y. x z)"]
  ["y"]
- ["*"];;
+ ;;
 
-let q7 () = magic_conv
+let q7 () = problem_of
  (Some "(b (c d (e f f k.(g e))) f)")
  ["(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))";
   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))";
@@ -240,25 +241,25 @@ let q7 () = magic_conv
  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
   "(f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)";
   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)"]
- ["*"];;
+ ;;
 
 (**********************)
 
-let q8 () = magic_conv
+let q8 () = problem_of
  (Some"x a")
- ["y (x b c)"] ["j"] ["*"]
+ ["y (x b c)"] ["j"]
 ;;
 
-let q9 () = magic_conv
+let q9 () = problem_of
  (Some"x a")
- ["y x"] ["a (y a b b b)"] ["*"]
+ ["y x"] ["a (y a b b b)"]
 ;;
 
-let q11 () = magic_conv
+let q11 () = problem_of
  (Some "x y")
- ["a (x z)"] [] ["*"];;
+ ["a (x z)"] [] ;;
 
-let q10 () = magic_conv
+let q10 () = problem_of
  (Some "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f)
 (k. e (f g))) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b
  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
@@ -273,20 +274,20 @@ let q10 () = magic_conv
 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)";
 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
 "e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))";
-] ["*"];;
+] ;;
 
-let m1 () = magic_conv None []
+let m1 () = problem_of None []
  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
- ["*"]
+
 ;;
 
-let m2 () = magic_conv None []
+let m2 () = problem_of None []
  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
- ["*"]
+
 ;;
 
 
-let n1 () = magic_conv (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)")
+let n1 () = problem_of (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)")
 [
 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. i))";
 "g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. l. g (m. c e) (m. i) (c b) (l c) b) (e c (d d (d c)) (c e (k. f)) (b (c b) (k. l. c b d) (c e) (k. l. m. f)))";
@@ -299,9 +300,9 @@ let n1 () = magic_conv (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e
 "d h (b (c b) (k. l. c b d) (c e)) (k. g (l. c e) (l. i) (c b) (k c) b) d b (b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (k. c)) a";
 "g (k. c e) (k. d d) (k. k k) (e c (d d (d c)) i) (k. g (l. k e) (l. d d)) (g i (b (c b) (k. l. c b d) (e c (d d (d c)) (k. c e (f c)) (k. k (c k) (l. m. c k d) (c e) k (g (l. c e) (l. i) (c k)) (l. c))))) (c b) a";
 "g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e) a"
-] ["*"];;
+] ;;
 
-let n2 () = magic_conv
+let n2 () = problem_of
 (Some"b b (c d) (k. d e) (k. k) (k. l. b)")
 [
 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))))) (d e (k. d e) g (i (k. k)))";
@@ -315,10 +316,10 @@ let n2 () = magic_conv
 "d e (k. d e) (k. b (l. h)) (k. l. d e) (d (g (d e) (g (k. e)) h) (g (d e) (k. l. l))) a";
 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (k. l. m. b b) a";
 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (b (b b) (d (g(d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k)))) (k. d e (l. d e) f) a";
-] ["*"]
+]
 ;;
 
-let n3 () = magic_conv
+let n3 () = problem_of
 (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
 [
 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
@@ -332,11 +333,11 @@ let n3 () = magic_conv
 "e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
-] ["*"];;
+] ;;
 
 (* main ([p34]);; *)
 
-main ([
+solve_many ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
  p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ;
  p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ;
@@ -346,7 +347,7 @@ main ([
  p37 ;
  p24 ; p25 ;
 ] @ List.map ((|>) ()) ([
- q1 ; q2; q3; q4 ; q5 ; q6 ;
+ q1 ; q2; (*q3;*) q4 ; q5 ; q6 ;
  q7 ;
  q8 ;
  q9 ;
diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 78c6c4c..95dae15 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -7,6 +7,7 @@ type t =
   | V of int
   | A of t * t
   | L of t
+  | B
 
 let rec print ?(l=[]) =
  function
@@ -15,6 +16,7 @@ let rec print ?(l=[]) =
   | L t ->
      let name = string_of_var (List.length l) in
      "λ" ^ name ^ "." ^ print ~l:(name::l) t
+  | B -> "B"
 
 let lift m =
  let rec aux l =
@@ -22,6 +24,7 @@ let lift m =
    | V n -> V (if n < l then n else n+m)
    | A (t1,t2) -> A (aux l t1, aux l t2)
    | L t -> L (aux (l+1) t)
+   | B -> B
  in
   aux 0
 
@@ -72,7 +75,8 @@ let unwind ?(tbl = Hashtbl.create 317) m =
        (try
          lift l (cache_unwind (List.nth e (n - l)))
         with Failure _ -> V (n - l))
-    | L t -> L (aux (l+1) t) in
+    | L t -> L (aux (l+1) t)
+    | B -> B in
   let t = aux 0 t in
   List.fold_left (fun f a -> A(f,a)) t s
 in
@@ -81,15 +85,19 @@ in
 let mwhd m =
  let rec aux =
   function
-     (e,A(t1,t2),s) ->
+   | (e,A(t1,t2),s) ->
        let t2' = aux (e,t2,[]) in
-       aux (e,t1,t2'::s)
+       let (_,t,_) = t2' in
+       if t = B
+        then t2'
+        else aux (e,t1,t2'::s)
    | (e,L t,x::s) -> aux (x::e,t,s)
    | (e,V n,s) as m ->
       (try
         let e,t,s' = List.nth e n in
         aux (e,t,s'@s)
        with Failure _ -> m)
+   | (e, B, _) -> (e, B, [])
    | (_,L _,[]) as m -> m
  in
   unwind (aux m)
diff --git a/ocaml/pure.mli b/ocaml/pure.mli
index f360074..a6b90ac 100644
--- a/ocaml/pure.mli
+++ b/ocaml/pure.mli
@@ -1,6 +1,6 @@
 module Pure :
   sig
-    type t = V of int | A of t * t | L of t
+    type t = V of int | A of t * t | L of t | B
     val print : ?l:string list -> t -> string
     val lift : int -> t -> t
     val unwind : ?tbl:('a list * t * 'a list as 'a, t) Hashtbl.t -> 'a -> t
diff --git a/ocaml/test.ml b/ocaml/test.ml
index 93240b9..f5bf55a 100644
--- a/ocaml/test.ml
+++ b/ocaml/test.ml
@@ -62,7 +62,7 @@ let call_main4 div convs nums =
   print_endline "CONV:"; List.iter prerr_endline convs;
   print_endline "NUMS:"; List.iter prerr_endline nums;
   prerr_newline ();
-  ) in Lambda4.main [Lambda4.magic_conv div convs nums ["*"]]
+  ) in Lambda4.solve (Lambda4.problem_of div convs nums)
 ;;
 
 let main =