From 2b941d27823cb7d06bbf83353c21779c866f3161 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 1 Jun 2018 17:45:48 +0200
Subject: [PATCH] Experimenting with backtracking and stepping on "all"
 possible subterms

---
 ocaml/simple.ml | 65 ++++++++++++++++++++++++++-----------------------
 1 file changed, 35 insertions(+), 30 deletions(-)

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