From 4d85faf22614fae57d4b0c45a5699258a9274272 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 7 Jun 2018 10:18:42 +0200 Subject: [PATCH] Replaced eat with andrea's finish (fixes examples failing for measure) --- ocaml/simple.ml | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 27d0119..4e93965 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -291,10 +291,42 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")") sanity p ;; +let finish p = + let compute_max_arity = + let rec aux n = function + | A(_,t1,t2) -> max (aux (n+1) t1) (aux 0 t2) + | L(_,t) -> max n (aux 0 t) + | V _ -> n + in aux 0 in +print_cmd "FINISH" ""; + let div_hd, div_nargs = get_inert p.div in + let j = div_nargs - 1 in + let arity = compute_max_arity p.conv in + let n = 1 + arity + max + (compute_max_lambdas_at div_hd j p.div) + (compute_max_lambdas_at div_hd j p.conv) in + let p = step j n p in + let div_hd, div_nargs = get_inert p.div in + let rec aux m = function + A(_,t1,t2) -> if is_var t2 then + (let delta_var, _ = get_inert t2 in + if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None + then m, delta_var + else aux (m-1) t1) else aux (m-1) t1 + | _ -> assert false in + let m, delta_var = aux div_nargs p.div in + let p = subst_in_problem (delta_var, delta) p in + let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in + sanity p +;; + let rec auto p = let hd_var, n_args = get_inert p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with | None -> + (try problem_fail (finish p) "Auto.2 did not complete the problem" + with Done sigma -> sigma) + (* (try let phase = p.phase in let p = eat p in @@ -302,6 +334,7 @@ let rec auto p = then problem_fail p "Auto.2 did not complete the problem" else auto p with Done sigma -> sigma) + *) | Some t -> let j = find_eta_difference p t n_args in let k = 1 + max -- 2.39.2