From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 6 Mar 2018 21:11:44 +0000 (+0100)
Subject: Fixed bug where x occurs as its stepped argument. Is this linear anymore?
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0dd15aa7265036c77e788c2c215316ff02f91945;p=fireball-separation.git

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

diff --git a/ocaml/andrea9.ml b/ocaml/andrea9.ml
index 1326064..7771af9 100644
--- 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
       p, A(t, V (v + k + 1)) in
  let p, t = aux' p n (V 0) in
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (m+1)) in
+ let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in
  let rec aux m t =
   if m < 0
    then aux' (k-1) t
@@ -272,15 +272,15 @@ let cut_app n t =
  in snd (aux t)
 ;;
 
-let find_difference div conv n_args =
- let conv = cut_app n_args conv in
- let rec aux t1 t2 k = match t1, t2 with
+let find_difference p t n_args =
+ let t = cut_app n_args t in
+ let rec aux t u k = match t, u with
  | V _, V _ -> assert false (* div subterm of conv *)
  | A(t1,t2), A(u1,u2) ->
-    if not (eta_eq t2 u2) then k
+    if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)
     else aux t1 u1 (k-1)
  | _, _ -> assert false
- in aux div conv n_args
+ in aux p.div t n_args
 ;;
 
 let rec count_lams = function
@@ -288,11 +288,12 @@ let rec count_lams = function
  | _ -> 0
 ;;
 
-let compute_k_from_args hd_var n_args =
+let compute_k_from_args p hd_var j =
  let rec aux hd = function
  | A(t1,t2) -> max (
-    if hd_of t1 = hd && (nargs t1) = (n_args - 1) then count_lams t2 else 0)
-  (max (aux hd t1) (aux hd t2))
+    if hd_of t1 = hd && (nargs t1) = j
+     then (print_endline(string_of_t p t2);if t2 = V hd then j else count_lams t2)
+     else 0) (max (aux hd t1) (aux hd t2))
  | L t -> aux (hd+1) t
  | V _ -> 0
  | _ -> assert false
@@ -306,10 +307,10 @@ let rec auto p =
  | None ->
     (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())
  | Some t ->
-  let j = find_difference p.div p.conv n_args - 1 in
+  let j = find_difference p t n_args - 1 in
   let k = max
-   (compute_k_from_args hd_var n_args p.div)
-    (compute_k_from_args hd_var n_args p.conv) in
+   (compute_k_from_args p hd_var j p.div)
+    (compute_k_from_args p hd_var j p.conv) in
   let p = step j k p in
   auto p
 ;;
@@ -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"
 "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;
 
+auto (problem_of "x (y. x y y)" "x (y. x y x)");;
+
+let rec conv_join = function
+ | [] -> "@"
+ | x::xs -> conv_join xs ^ " ("^ x ^")"
+;;
+
+(* auto (problem_of "x a a a" (conv_join[
+ "x b a a";
+ "x a b a";
+ "x a a b";
+]));; *)
+
+auto (problem_of "x a a a a" (conv_join[
+ "x b a a a";
+ "x a b a a";
+ "x a a b a";
+ "x a a a b";
+]));
+
+(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)
+auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[
+ "x a a a a (_. a) b b b";
+ "x a a a a (_. _. _. _. x. y. x y)";
+]));
+
 (* let _ = exec
  "x y"
  [ "x x"; "y z"; "y x" ]