From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 7 Mar 2018 10:40:24 +0000 (+0100)
Subject: Fixed bug with x stepping on itself applied to args; refactoring
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c4cb7e061f1a545f2b3566067693adb6e5d3d1c;p=fireball-separation.git

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

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