Fixed bug with x stepping on itself applied to args; refactoring

diff --git a/ocaml/andrea9.ml b/ocaml/andrea9.ml
index 7771af93d68dcb9eece179e1ecd37a877db43917..788cc49dc45792cb0e13ca12fef6ffee177dd3a3 100644 (file)
--- a/ocaml/andrea9.ml
+++ b/ocaml/andrea9.ml
@@ -1,4 +1,5 @@
 let (++) f g x = f (g x);;\r
+let id x = x;;\r
 \r
 let print_hline = Console.print_hline;;\r
 \r
@@ -11,6 +12,17 @@ type t =
  | P (* pacman *)\r
 ;;\r
 \r
+let eta_eq =\r
+ let rec aux l1 l2 t1 t2 = match t1, t2 with\r
+  | L t1, L t2 -> aux l1 l2 t1 t2\r
+  | L t1, t2 -> aux l1 (l2+1) t1 t2\r
+  | t1, L t2 -> aux (l1+1) l2 t1 t2\r
+  | V a, V b -> a + l1 = b + l2\r
+  | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
+  | _, _ -> false\r
+ in aux 0 0\r
+;;\r
+\r
 type problem = {\r
    orig_freshno: int\r
  ; freshno : int\r
@@ -20,8 +32,6 @@ type problem = {
  ; stepped : var list\r
 }\r
 \r
-let all_terms p = [p.div; p.conv];;\r
-\r
 exception Done of (var * t) list (* substitution *);;\r
 exception Fail of int * string;;\r
 \r
@@ -66,16 +76,27 @@ let freshvar ({freshno} as p) =
  {p with freshno=freshno+1}, freshno+1\r
 ;;\r
 \r
-let rec is_inert p =\r
+let rec is_inert =\r
  function\r
- | A(t,_) -> is_inert p t\r
+ | A(t,_) -> is_inert t\r
  | V _ -> true\r
  | L _ | B | P -> false\r
 ;;\r
 \r
 let is_var = function V _ -> true | _ -> false;;\r
 let is_lambda = function L _ -> true | _ -> false;;\r
-let is_pacman = function P -> true | _ -> false;;\r
+\r
+let rec head_of_inert = function\r
+ | V n -> n\r
+ | A(t, _) -> head_of_inert t\r
+ | _ -> assert false\r
+;;\r
+\r
+let rec args_no = function\r
+ | V _ -> 0\r
+ | A(t, _) -> 1 + args_no t\r
+ | _ -> assert false\r
+;;\r
 \r
 let rec subst level delift fromdiv sub =\r
  function\r
@@ -104,7 +125,7 @@ and lift n =
 let subst = subst 0 false;;\r
 \r
 let subst_in_problem (sub: var * t) (p: problem) =\r
-print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
+print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
  let p = {p with stepped=(fst sub)::p.stepped} in\r
  let conv = subst false sub p.conv in\r
  let div = subst true sub p.div in\r
@@ -113,84 +134,42 @@ print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ st
  {p with sigma=sub::p.sigma}\r
 ;;\r
 \r
-let free_vars p t =\r
- let rec aux level = function\r
- | V v -> if v >= level then [v] else []\r
- | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
- | L t -> aux (level+1) t\r
- | B | P -> []\r
- in Util.sort_uniq (aux 0 t)\r
-;;\r
-\r
-let visible_vars p t =\r
- let rec aux = function\r
- | V v -> [v]\r
- | A(t1,t2) -> (aux t1) @ (aux t2)\r
- | B | P\r
- | L _ -> []\r
- (* | Ptr n -> aux (get_conv p n) *)\r
- in Util.sort_uniq (aux t)\r
-;;\r
-\r
-let rec hd_of = function\r
- | V n -> n\r
- | A(t, _) -> hd_of t\r
- | _ -> assert false\r
-;;\r
-\r
-let rec nargs = function\r
- | V _ -> 0\r
- | A(t, _) -> 1 + nargs t\r
- | _ -> assert false\r
-;;\r
-\r
 let get_subterm_with_head_and_args hd_var n_args =\r
  let rec aux = function\r
  | V _ | L _ | B | P -> None\r
  | A(t1,t2) as t ->\r
-   if hd_of t1 = hd_var && n_args <= 1 + nargs t1\r
+   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1\r
     then Some t\r
-     else match aux t2 with\r
-     | None -> aux t1\r
-     | Some _ as res -> res\r
+    else match aux t2 with\r
+    | None -> aux t1\r
+    | Some _ as res -> res\r
  in aux\r
 ;;\r
 \r
-let rec eta_eq l1 l2 t1 t2 = match t1, t2 with\r
- | L t1, L t2 -> eta_eq l1 l2 t1 t2\r
- | L t1, t2 -> eta_eq l1 (l2+1) t1 t2\r
- | t1, L t2 -> eta_eq (l1+1) l2 t1 t2\r
- | V a, V b -> a + l1 = b + l2\r
- | A(t1,t2), A(u1,u2) -> eta_eq l1 l2 t1 u1 && eta_eq l1 l2 t2 u2\r
- | _, _ -> false\r
-;;\r
-let eta_eq = eta_eq 0 0;;\r
-\r
-\r
-let rec simple_explode p =\r
+(* let rec simple_explode p =\r
  match p.div with\r
  | V var ->\r
   let subst = var, B in\r
   sanity (subst_in_problem subst p)\r
- | _ -> p\r
-\r
-and sanity p =\r
- (* Sanity checks: *)\r
- if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";\r
- if p.conv = B then problem_fail p "p.conv diverged";\r
+ | _ -> p *)\r
 \r
+let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\r
  if p.div = B then raise (Done p.sigma);\r
- let p = if is_var p.div then simple_explode p else p in\r
+ if not (is_inert p.div) then problem_fail p "p.div converged";\r
+ if p.conv = B then problem_fail p "p.conv diverged";\r
+ (* let p = if is_var p.div then simple_explode p else p in *)\r
  p\r
 ;;\r
 \r
 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 \r
+(* eat the arguments of the divergent and explode.\r
+ It does NOT perform any check, may fail if done unsafely *)\r
 let eat p =\r
 print_cmd "EAT" "";\r
- let var = hd_of p.div in\r
- let n = nargs p.div in\r
+ let var = head_of_inert p.div in\r
+ let n = args_no p.div in\r
  let rec aux m t =\r
   if m = 0\r
    then lift n t\r
@@ -199,8 +178,9 @@ print_cmd "EAT" "";
  sanity (subst_in_problem subst p)\r
 ;;\r
 \r
+(* step on the head of div, on the k-th argument, with n fresh vars *)\r
 let step k n p =\r
- let var = hd_of p.div in\r
+ let var = head_of_inert p.div in\r
  print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
  let rec aux' p m t =\r
   if m < 0\r
@@ -260,7 +240,7 @@ let exec div conv cmds =
  | Done _ -> ()\r
 ;;\r
 \r
-let cut_app n t =\r
+let inert_cut_at n t =\r
  let rec aux t =\r
   match t with\r
   | V _ as t -> 0, t\r
@@ -272,8 +252,8 @@ let cut_app n t =
  in snd (aux t)\r
 ;;\r
 \r
-let find_difference p t n_args =\r
- let t = cut_app n_args t in\r
+let find_eta_difference p t n_args =\r
+ let t = inert_cut_at n_args t in\r
  let rec aux t u k = match t, u with\r
  | V _, V _ -> assert false (* div subterm of conv *)\r
  | A(t1,t2), A(u1,u2) ->\r
@@ -283,17 +263,20 @@ let find_difference p t n_args =
  in aux p.div t n_args\r
 ;;\r
 \r
-let rec count_lams = function\r
- | L t -> 1 + count_lams t\r
+let rec no_leading_lambdas = function\r
+ | L t -> 1 + no_leading_lambdas t\r
  | _ -> 0\r
 ;;\r
 \r
-let compute_k_from_args p hd_var j =\r
+let compute_max_lambdas_at hd_var j =\r
  let rec aux hd = function\r
- | A(t1,t2) -> max (\r
-    if hd_of t1 = hd && (nargs t1) = j\r
-     then (print_endline(string_of_t p t2);if t2 = V hd then j else count_lams t2)\r
-     else 0) (max (aux hd t1) (aux hd t2))\r
+ | A(t1,t2) ->\r
+    (if head_of_inert t1 = hd && args_no t1 = j\r
+      then max (\r
+       if is_inert t2 && head_of_inert t2 = hd\r
+        then j - args_no t2\r
+        else no_leading_lambdas t2)\r
+      else id) (max (aux hd t1) (aux hd t2))\r
  | L t -> aux (hd+1) t\r
  | V _ -> 0\r
  | _ -> assert false\r
@@ -301,16 +284,16 @@ let compute_k_from_args p hd_var j =
 ;;\r
 \r
 let rec auto p =\r
- let hd_var = hd_of p.div in\r
- let n_args = nargs p.div in\r
+ let hd_var = head_of_inert p.div in\r
+ let n_args = args_no p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
  | None ->\r
     (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())\r
  | Some t ->\r
-  let j = find_difference p t n_args - 1 in\r
+  let j = find_eta_difference p t n_args - 1 in\r
   let k = max\r
-   (compute_k_from_args p hd_var j p.div)\r
-    (compute_k_from_args p hd_var j p.conv) in\r
+   (compute_max_lambdas_at hd_var j p.div)\r
+    (compute_max_lambdas_at hd_var j p.conv) in\r
   let p = step j k p in\r
   auto p\r
 ;;\r