Finish ignores rigid arguments; auto tries to diverge the arguments of an inert

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 5c158b3b0b400c09b6dca7ff3bf0d1916fb8afe1..185c54ef2f025afeea14d38d6bfa74d2423722de 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -1,5 +1,4 @@
 let (++) f g x = f (g x);;\r
-let id x = x;;\r
 let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;\r
 \r
 let print_hline = Console.print_hline;;\r
@@ -93,9 +92,12 @@ exception Unseparable of string;;
 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
+ | x::xs -> (try f x with Backtrack s -> (if s <> "" then print_endline ("\n<< BACKTRACK: "^s)); try_all label f xs)\r
  | [] -> raise (Backtrack label)\r
 ;;\r
+let try_both label f x g y =\r
+ try_all label (function `L x -> f x | `R y -> g y) [`L x ; `R y]\r
+;;\r
 \r
 let problem_fail p reason =\r
  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
@@ -222,7 +224,7 @@ let purify =
 ;;\r
 \r
 let check p sigma =\r
- print_endline "Checking...";\r
+ print_endline "\nChecking...";\r
  let div = purify p.div in\r
  let conv = purify p.conv in\r
  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
@@ -238,13 +240,7 @@ let check p sigma =
 ;;\r
 \r
 let sanity p =\r
- print_endline (string_of_problem p); (* non cancellare *)\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
- | _ as t -> t in\r
- let p = {p with div=remove_trailing_constant_args p.div} in\r
- p\r
+ print_endline (string_of_problem p) (* non cancellare *); p\r
 ;;\r
 \r
 (* drops the arguments of t after the n-th *)\r
@@ -289,7 +285,7 @@ let compute_max_lambdas_at hd_var j =
  in aux hd_var\r
 ;;\r
 \r
-let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
+let print_cmd s1 s2 = print_endline ("\n>> " ^ s1 ^ " " ^ s2);;\r
 \r
 (* returns Some i if i is the smallest integer s.t. p holds for the i-th\r
    element of the list in input *)\r
@@ -297,7 +293,7 @@ let smallest_such_that p =
  let rec aux i =\r
   function\r
      [] -> None\r
-   | hd::_ when (print_endline (string_of_t hd) ; p hd) -> Some i\r
+   | hd::_ when p i hd -> Some i\r
    | _::tl -> aux (i+1) tl\r
  in\r
   aux 0\r
@@ -320,10 +316,10 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^
  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
  let subst = var, t in\r
  let divs, p = subst_in_problem subst p in\r
- divs, sanity p\r
+ divs, p\r
 ;;\r
 \r
-let finish p =\r
+let finish p arity =\r
  (* one-step version of eat *)\r
  let compute_max_arity =\r
    let rec aux n = function\r
@@ -331,12 +327,14 @@ let finish p =
    | L(t,g) -> List.fold_right (max ++ (aux 0)) (t::g) 0\r
    | _ -> n\r
  in aux 0 in\r
-print_cmd "FINISH" "";\r
  (* First, a step on the last argument of the divergent.\r
     Because of the sanity check, it will never be a constant term. *)\r
  let div_hd, div_nargs = get_inert p.div in\r
- let div_hd = match div_hd with V n -> n | _ -> assert false in\r
- let j = div_nargs - 1 in\r
+ let div_hd = match div_hd with V n -> n | _ -> raise (Backtrack "Cannot finish on constant tm") in\r
+ let j = match\r
+  smallest_such_that (fun i t -> i >= arity && not (is_constant t)) (args_of_inert p.div)\r
+  with Some j -> j | None -> raise (Backtrack "") in\r
+ print_endline "\n>> FINISHING";\r
  let arity = compute_max_arity p.conv in\r
  let n = 1 + arity + max\r
   (compute_max_lambdas_at div_hd j p.div)\r
@@ -356,48 +354,47 @@ print_cmd "FINISH" "";
  | _ -> 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
- sanity p\r
+ ignore (subst_in_problem (div_hd, mk_lams delta (m-1)) p);\r
+ assert false\r
 ;;\r
 \r
 let auto p =\r
  let rec aux p =\r
+ if eta_subterm p.div p.conv\r
+ then raise (Backtrack "div is subterm of conv");\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
+ | L _ as t -> (* case p.div is an abstraction *)\r
+    print_endline "\nSOTTO UN LAMBDA";\r
+    let t, g = mk_app t C in\r
+    aux ({p with div=mk_apps C (t::g)})\r
+ | V _ | C -> raise (Backtrack "V | C")\r
+ | A _ -> (\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
+   then (print_endline "\nSOTTO UN C"; try_all "auto.C"\r
+    (fun div -> aux (sanity {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
+   let arity = List.fold_right (max ++ (snd ++ get_inert)) tms 0 in\r
+   try_both "???" (finish p) arity\r
+    (fun _ ->\r
+      let jss = List.concat (List.map (find_eta_difference p) tms) in\r
+      let jss = List.sort_uniq compare jss in\r
+      let f = try_all "no differences"\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\r
+       try_both "step, then diverge arguments"\r
+        f jss\r
+        (try_all "tried p.div arguments" (fun div -> aux {p with div})) (args_of_inert p.div)\r
+      ) ()\r
  ) in try\r
   aux p\r
  with Done sigma -> sigma\r
@@ -440,33 +437,3 @@ let solve p =
 ;;\r
 \r
 Problems.main (solve ++ problem_of);\r
-\r
-(* Example usage of interactive: *)\r
-\r
-(* let interactive div conv cmds =\r
- let p = problem_of div conv in\r
- try (\r
- let p = List.fold_left (|>) p cmds in\r
- let rec f p cmds =\r
-  let nth spl n = int_of_string (List.nth spl n) in\r
-  let read_cmd () =\r
-   let s = read_line () in\r
-   let spl = Str.split (Str.regexp " +") s in\r
-   s, let uno = List.hd spl in\r
-    try if uno = "eat" then eat\r
-    else if uno = "step" then step (nth spl 1) (nth spl 2)\r
-    else failwith "Wrong input."\r
-    with Failure s -> print_endline s; (fun x -> x) in\r
-  let str, cmd = read_cmd () in\r
-  let cmds = (" " ^ str ^ ";")::cmds in\r
-  try\r
-   let p = cmd p in f p cmds\r
-  with\r
-  | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
- in f p []\r
- ) with Done _ -> ()\r
-;; *)\r
-\r
-(* interactive "x y"\r
- "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
-;; *)\r