Fixed bug where x occurs as its stepped argument. Is this linear anymore?

diff --git a/ocaml/andrea9.ml b/ocaml/andrea9.ml
index 1326064389be08912b9cc0ed0d34a80938b7ef69..7771af93d68dcb9eece179e1ecd37a877db43917 100644 (file)
--- a/ocaml/andrea9.ml
+++ b/ocaml/andrea9.ml
@@ -210,7 +210,7 @@ let step k n p =
      let p, t = aux' p (m-1) t in\r
       p, A(t, V (v + k + 1)) in\r
  let p, t = aux' p n (V 0) in\r
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (m+1)) in\r
+ let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in\r
  let rec aux m t =\r
   if m < 0\r
    then aux' (k-1) t\r
@@ -272,15 +272,15 @@ let cut_app n t =
  in snd (aux t)\r
 ;;\r
 \r
-let find_difference div conv n_args =\r
- let conv = cut_app n_args conv in\r
- let rec aux t1 t2 k = match t1, t2 with\r
+let find_difference p t n_args =\r
+ let t = cut_app 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
-    if not (eta_eq t2 u2) then k\r
+    if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)\r
     else aux t1 u1 (k-1)\r
  | _, _ -> assert false\r
- in aux div conv n_args\r
+ in aux p.div t n_args\r
 ;;\r
 \r
 let rec count_lams = function\r
@@ -288,11 +288,12 @@ let rec count_lams = function
  | _ -> 0\r
 ;;\r
 \r
-let compute_k_from_args hd_var n_args =\r
+let compute_k_from_args p hd_var j =\r
  let rec aux hd = function\r
  | A(t1,t2) -> max (\r
-    if hd_of t1 = hd && (nargs t1) = (n_args - 1) then count_lams t2 else 0)\r
-  (max (aux hd t1) (aux hd t2))\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
  | L t -> aux (hd+1) t\r
  | V _ -> 0\r
  | _ -> assert false\r
@@ -306,10 +307,10 @@ let rec auto p =
  | 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.div p.conv n_args - 1 in\r
+  let j = find_difference p t n_args - 1 in\r
   let k = max\r
-   (compute_k_from_args hd_var n_args p.div)\r
-    (compute_k_from_args hd_var n_args p.conv) in\r
+   (compute_k_from_args p hd_var j p.div)\r
+    (compute_k_from_args p hd_var j p.conv) in\r
   let p = step j k p in\r
   auto p\r
 ;;\r
@@ -351,6 +352,32 @@ auto (problem_of "a (x. x b) (x. x c)" "@ (a (x. b b) @) (a @ c) (a (x. x x) a)
 interactive "x y"\r
 "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;\r
 \r
+auto (problem_of "x (y. x y y)" "x (y. x y x)");;\r
+\r
+let rec conv_join = function\r
+ | [] -> "@"\r
+ | x::xs -> conv_join xs ^ " ("^ x ^")"\r
+;;\r
+\r
+(* auto (problem_of "x a a a" (conv_join[\r
+ "x b a a";\r
+ "x a b a";\r
+ "x a a b";\r
+]));; *)\r
+\r
+auto (problem_of "x a a a a" (conv_join[\r
+ "x b a a a";\r
+ "x a b a a";\r
+ "x a a b a";\r
+ "x a a a b";\r
+]));\r
+\r
+(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
+auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[\r
+ "x a a a a (_. a) b b b";\r
+ "x a a a a (_. _. _. _. x. y. x y)";\r
+]));\r
+\r
 (* let _ = exec\r
  "x y"\r
  [ "x x"; "y z"; "y x" ]\r