From 0f5bd8d764763ce97a981e81c266313da3ce41f5 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 10 Jun 2018 17:35:35 +0200
Subject: [PATCH] (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 :-(
---
 ocaml/simple.ml | 85 ++++++++++++++++++++++++++++++-------------------
 1 file changed, 52 insertions(+), 33 deletions(-)

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