Improved backtracking in Simple

- Removed Fail exception, replaced by combination
  of Failure, Backtrack, Unseparable
- Added label to problem

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 16b4e69c9f69e2ef02fea0d61545779657937492..60b4e8779f4aa41705dd8016fd3c2918599a74da 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -70,6 +70,7 @@ let string_of_t =
 type problem = {\r
    orig_freshno: int\r
  ; freshno : int\r
+ ; label : string\r
  ; div : t\r
  ; conv : t\r
  ; sigma : (var * t) list (* substitutions *)\r
@@ -85,12 +86,18 @@ let string_of_problem p =
 \r
 exception B;;\r
 exception Done of (var * t) list (* substitution *);;\r
-exception Fail of int * string;;\r
+exception Unseparable of string;;\r
+exception Backtrack of string;;\r
+\r
+let rec try_all label f = function\r
+ | x::xs -> (try f x with Backtrack _ -> try_all label f xs)\r
+ | [] -> raise (Backtrack label)\r
+;;\r
 \r
 let problem_fail p reason =\r
  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  print_endline (string_of_problem p);\r
- raise (Fail (-1, reason))\r
+ failwith reason\r
 ;;\r
 \r
 let freshvar ({freshno} as p) =\r
@@ -176,7 +183,7 @@ print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);
  let sigma = sub :: p.sigma in\r
  let div, g = try subst sub p.div with B -> raise (Done sigma) in\r
  assert (g = []);\r
- let conv, f = try subst sub p.conv with B -> raise (Fail(-1, "p.conv diverged")) in\r
+ let conv, f = try subst sub p.conv with B -> raise (Backtrack "p.conv diverged") in\r
  assert (g = []);\r
  {p with div; conv; sigma}\r
 ;;\r
@@ -212,16 +219,18 @@ let check p sigma =
  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
  let freshno = List.fold_right (max ++ fst) sigma 0 in\r
  let env = Pure.env_of_sigma freshno sigma in\r
- assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
- print_endline " D diverged.";\r
- assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
- print_endline " C converged.";\r
+ (if not (Pure.diverged (Pure.mwhd (env,div,[])))\r
+  then failwith "D converged in Pure");\r
+ print_endline "- D diverged.";\r
+ (if Pure.diverged (Pure.mwhd (env,conv,[]))\r
+  then failwith "C diverged in Pure");\r
+ print_endline "- C converged.";\r
  ()\r
 ;;\r
 \r
 let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\r
- if not (is_inert p.div) then problem_fail p "p.div converged";\r
+ if not (is_inert p.div) then raise (Backtrack "p.div converged");\r
  (* Trailing constant args can be removed because do not contribute to eta-diff *)\r
  let rec remove_trailing_constant_args = function\r
  | A(t1, t2) when is_constant t2 -> remove_trailing_constant_args t1\r
@@ -353,24 +362,16 @@ let auto p =
  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
+    try_all "no similar terms" (fun t ->\r
       let js = find_eta_difference p t 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
+       try_all "no eta difference"\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
+          aux (step j k p)) js) tms\r
    )\r
   else\r
     problem_fail (finish p) "Finish did not complete the problem"\r
@@ -395,15 +396,26 @@ let problem_of (label, div, convs, ps, var_names) =
  | Some div -> aux 0 (div :> Num.nf)\r
  | None -> assert false in\r
  let varno = List.length var_names in\r
- {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]}\r
+ {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; label}\r
 ;;\r
 \r
 let solve p =\r
- if is_constant p.div\r
-  then print_endline "!!! div is stuck. Problem was not run !!!"\r
- else if eta_subterm p.div p.conv\r
-  then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
-  else let p = sanity p (* initial sanity check *) in check p (auto p)\r
+ let c = if String.length p.label > 0 then String.sub (p.label) 0 1 else "" in\r
+ let module M = struct exception Okay end in\r
+ try\r
+  if eta_subterm p.div p.conv\r
+  then raise (Unseparable "div is subterm of conv")\r
+  else\r
+   let p = sanity p (* initial sanity check *) in\r
+   check p (auto p);\r
+   raise M.Okay\r
+ with\r
+  | M.Okay -> if c = "?" then\r
+    failwith "The problem succeeded, but was supposed to be unseparable"\r
+  | e when c = "!" ->\r
+    failwith ("The problem was supposed to be separable, but: "^Printexc.to_string e)\r
+  | e ->\r
+    print_endline ("The problem failed, as expected ("^Printexc.to_string e^")")\r
 ;;\r
 \r
 Problems.main (solve ++ problem_of);\r

diff --git a/ocaml/simple.mli b/ocaml/simple.mli
index fba247092a39b9074941eff9319e7c40038f67a7..67bee915c413aa424c50499cbd8c6d5bc675090c 100644 (file)
--- a/ocaml/simple.mli
+++ b/ocaml/simple.mli
@@ -1,5 +1,5 @@
 type problem\r
-exception Fail of int * string\r
+exception Unseparable of string\r
 val solve : problem -> unit\r
 val problem_of :\r
   string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *\r

diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index ed2c81c8e2325946ca5777b1ed1a151743f7f03a..9e79ee9e46adec9badb50c9b8432a497eb7ee8f2 100644 (file)
--- a/ocaml/simple_test.ml
+++ b/ocaml/simple_test.ml
@@ -58,9 +58,10 @@ let main =
     print_endline str;
     try
      (solve ++ problem_of ++ Parser.problem_of_string) ("$" ^ str)
-    with Simple.Fail _ as e ->
-     let str = "$ failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in
+    with Failure _ as e ->
+     let str = "$! failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in
      Printf.fprintf oc "%s\n" str
+    | Unseparable _ -> ()
   ) num ;
   close_out oc;
   print_endline ("\n\n---- </TESTS> " ^ file);