(Almost-)Correct handling of garbage in Simple

- subst_in_problem, step now return a list of terms from garbages
  that were activated, i.e. brought on toplevel after a reduction
- auto iterated on that garbage

TODO:
- remove sanity function
- problems/simple.constants.1 fails :-(

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 34b2a7f5168d34427d42b46e1d81de3b25219d9c..13400b7f8cb84cb94c36c65daae5bd3a3a0dcf42 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -179,16 +179,22 @@ and lift n =
   | C -> C\r
  in aux 0\r
 ;;\r
-let subst = subst 0 false;;\r
+let subst' = subst;;\r
+let subst = subst' 0 false;;\r
+\r
+let rec mk_apps t = function\r
+ | u::us -> mk_apps (A(t,u)) us\r
+ | [] -> t\r
+;;\r
 \r
 let subst_in_problem ((v, t) as sub) p =\r
 print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\r
  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 (Backtrack "p.conv diverged") in\r
- assert (g = []);\r
- {p with div; conv; sigma}\r
+ let divs = div :: g in\r
+ let conv, g = try subst sub p.conv with B -> raise (Backtrack "p.conv diverged") in\r
+ let conv = if g = [] then conv else mk_apps C (conv::g) in\r
+ divs, {p with div; conv; sigma}\r
 ;;\r
 \r
 let get_subterms_with_head hd_var =\r
@@ -233,7 +239,6 @@ let check p sigma =
 \r
 let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\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
@@ -316,8 +321,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^
   fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
  let subst = var, t in\r
- let p = subst_in_problem subst p in\r
- sanity p\r
+ let divs, p = subst_in_problem subst p in\r
+ divs, sanity p\r
 ;;\r
 \r
 let finish p =\r
@@ -338,7 +343,7 @@ print_cmd "FINISH" "";
  let n = 1 + arity + max\r
   (compute_max_lambdas_at div_hd j p.div)\r
   (compute_max_lambdas_at div_hd j p.conv) in\r
- let p = step j n p in\r
+ let _, p = step j n p in\r
  (* Now, find first argument of div that is a variable never applied anywhere.\r
  It must exist because of some invariant, since we just did a step,\r
  and because of the arity of the divergent *)\r
@@ -352,38 +357,52 @@ print_cmd "FINISH" "";
  | A(t,_) -> aux (m-1) t\r
  | _ -> assert false in\r
  let m, delta_var = aux div_nargs p.div in\r
- let p = subst_in_problem (delta_var, delta) p in\r
- let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
+ let _, p = subst_in_problem (delta_var, delta) p in\r
+ let _, p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
  sanity p\r
 ;;\r
 \r
 let auto p =\r
  let rec aux p =\r
- let hd, n_args = get_inert p.div in\r
- match hd with\r
- | C | L _ | A _  -> assert false\r
- | V hd_var ->\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
-    try_all "no similar terms" (fun t ->\r
+ match p.div with\r
+ | L(div,g) -> (* case p.div is an abstraction *)\r
+    let f l t = fst (subst' 0 true (0, C) t) :: l in\r
+    (* the `fst' above is because we can ignore the\r
+    garbage generated by the subst, because substituting\r
+    C does not create redexes and thus no new garbage is activated *)\r
+    let tms = List.fold_left f [] (div::g) in\r
+    try_all "auto.L"\r
+     (fun div -> aux {p with div}) tms\r
+ | _ -> (\r
+   if is_constant p.div (* case p.div is rigid inert *)\r
+   then try_all "auto.C"\r
+    (fun div -> aux {p with div}) (args_of_inert p.div)\r
+   else (* case p.div is flexible inert *)\r
+    let hd, n_args = get_inert p.div in\r
+   match hd with\r
+   | C | L _ | A _  -> assert false\r
+   | V hd_var ->\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
+     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
       let js = List.rev js in\r
-       try_all "no eta difference"\r
-        (fun j ->\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
-          aux (step j k p)) js) tms\r
-   )\r
-  else\r
-    problem_fail (finish p) "Finish did not complete the problem"\r
-  in\r
-  try\r
-   aux p\r
-  with Done sigma -> sigma\r
+      try_all "no eta difference"\r
+       (fun j ->\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
+         let divs, p = step j k p in\r
+         try_all "p.div" (fun div -> aux (sanity {p with div})) divs\r
+         ) js) tms)\r
+    else\r
+      problem_fail (finish p) "Finish did not complete the problem"\r
+ ) in try\r
+  aux p\r
+ with Done sigma -> sigma\r
 ;;\r
 \r
 let problem_of (label, div, convs, ps, var_names) =\r