From: acondolu 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 ;;