From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 11 Jun 2018 09:56:53 +0000 (+0200)
Subject: Finish ignores rigid arguments; auto tries to diverge the arguments of an inert
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47a9f6a73ecea5a2e60932ce324e21f4a90315c2;p=fireball-separation.git

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

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