Experimenting with backtracking and stepping on "all" possible subterms

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 4a69c6e84b5ba2f046deac6281630a5b866f9897..bac3ddf98a532784a587fa90cd9cbd67ca1f1e0a 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -157,19 +157,16 @@ print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);
   sigma=sub::p.sigma}\r
 ;;\r
 \r
-let get_subterm_with_head_and_args hd_var n_args =\r
- let rec aux lev = function\r
- | C | V _ | B -> None\r
- | L t -> aux (lev+1) t\r
+let get_subterms_with_head hd_var =\r
+ let rec aux lev inert_done = function\r
+ | C | V _ | B -> []\r
+ | L t -> aux (lev+1) false t\r
  | A(t1,t2) as t ->\r
    let hd_var', n_args' = get_inert t1 in\r
-   if hd_var' = V (hd_var + lev) && n_args <= 1 + n_args'\r
-    (* the `+1` above is because of t2 *)\r
-    then Some (lift ~-lev t)\r
-    else match aux lev t2 with\r
-    | None -> aux lev t1\r
-    | Some _ as res -> res\r
- in aux 0\r
+   if not inert_done && hd_var' = V (hd_var + lev)\r
+    then lift ~-lev t :: aux lev true t1 @ aux lev false t2\r
+    else aux lev true t1 @ aux lev false t2\r
+ in aux 0 false\r
 ;;\r
 \r
 let rec purify = function\r
@@ -310,28 +307,36 @@ let auto p =
  match hd with\r
  | C | L _ | B | A _  -> assert false\r
  | V hd_var ->\r
- match get_subterm_with_head_and_args hd_var n_args p.conv with\r
- | None ->\r
-    let phase = p.phase in\r
+ let tms = get_subterms_with_head hd_var p.conv in\r
+ if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
+  then (\r
+    (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)\r
+    List.iter (fun t -> try\r
+      let js = find_eta_difference p t n_args in\r
+      (* print_endline (String.concat ", " (List.map string_of_int js)); *)\r
+      if js = [] then problem_fail p "no eta difference found (div subterm of conv?)";\r
+      let js = List.rev js in\r
+       List.iter\r
+        (fun j ->\r
+         try\r
+          let k = 1 + max\r
+           (compute_max_lambdas_at hd_var j p.div)\r
+            (compute_max_lambdas_at hd_var j p.conv) in\r
+          ignore (aux (step j k p))\r
+         with Fail(_, s) ->\r
+          print_endline ("Backtracking (eta_diff) because: " ^ s)) js;\r
+       raise (Fail(-1, "no eta difference"))\r
+      with Fail(_, s) ->\r
+       print_endline ("Backtracking (get_subterms) because: " ^ s)) tms;\r
+     raise (Fail(-1, "no similar terms"))\r
+   )\r
+  else\r
+    (let phase = p.phase in\r
      let p = eat p in\r
      if phase = `Two\r
       then problem_fail p "Auto.2 did not complete the problem"\r
-      else aux p\r
- | Some t ->\r
-  let js = find_eta_difference p t n_args in\r
-  (* print_endline (String.concat ", " (List.map string_of_int js)); *)\r
-  if js = [] then problem_fail p "no eta difference found (div subterm of conv?)";\r
-  let js = List.rev js in\r
-   List.iter\r
-    (fun j ->\r
-     try\r
-      let k = 1 + max\r
-       (compute_max_lambdas_at hd_var j p.div)\r
-        (compute_max_lambdas_at hd_var j p.conv) in\r
-      ignore (aux (step j k p))\r
-     with Fail(_, s) ->\r
-      print_endline ("Backtracking because: " ^ s)) js;\r
-   raise (Fail(-1, "no eta difference")) in\r
+      else aux p)\r
+  in\r
   try\r
    aux p\r
   with Done sigma -> sigma\r