From: acondolu Date: Sat, 9 Jun 2018 08:19:56 +0000 (+0200) Subject: Removed eat, p.stepped, p.phase and t.B X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69f44e4fb3d56f89adcc952514707914886fdd79;p=fireball-separation.git Removed eat, p.stepped, p.phase and t.B --- diff --git a/ocaml/simple.ml b/ocaml/simple.ml index c86796e..897d6b6 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -11,7 +11,6 @@ type t = | V of var | A of t * t | L of t - | B (* bottom *) | C (* constant *) ;; @@ -58,7 +57,6 @@ let string_of_t = | C -> "C" | A _ | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")" - | B -> "BOT" and string_of_term_no_pars_app level = function | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2 | _ as t -> string_of_term_w_pars level t @@ -74,19 +72,17 @@ type problem = { ; div : t ; conv : t ; sigma : (var * t) list (* substitutions *) - ; stepped : var list - ; phase : [`One | `Two] (* :'( *) } let string_of_problem p = let lines = [ - "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped); "[DV] " ^ string_of_t p.div; "[CV] " ^ string_of_t p.conv; ] in String.concat "\n" lines ;; +exception B;; exception Done of (var * t) list (* substitution *);; exception Fail of int * string;; @@ -107,14 +103,13 @@ let rec is_inert = | A(t,_) -> is_inert t | V _ -> true | C - | L _ | B -> false + | L _ -> false ;; let rec is_constant = function C -> true | V _ -> false - | B -> assert false | A(t,_) | L t -> is_constant t ;; @@ -141,7 +136,7 @@ let rec no_leading_lambdas v n = function | L t -> 1 + no_leading_lambdas (v+1) n t | A _ as t -> let v', m = get_inert t in if V v = v' then max 0 (n - m) else 0 | V v' -> if v = v' then n else 0 - | B | C -> 0 + | C -> 0 ;; let rec subst level delift sub = @@ -152,10 +147,9 @@ let rec subst level delift sub = let t1 = subst level delift sub t1 in let t2 = subst level delift sub t2 in mk_app t1 t2 - | C | B as t -> t -and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B + | C -> C +and mk_app t1 t2 = if t1 = delta && t2 = delta then raise B else match t1 with - | B -> B | L t1 -> subst 0 true (0, t2) t1 | _ -> A (t1, t2) and lift n = @@ -164,7 +158,7 @@ and lift n = | V m -> V (if m >= lev then m + n else m) | L t -> L (aux (lev+1) t) | A (t1, t2) -> A (aux lev t1, aux lev t2) - | C | B as t -> t + | C -> C in aux 0 ;; let subst = subst 0 false;; @@ -174,14 +168,13 @@ print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t); {p with div=subst sub p.div; conv=subst sub p.conv; - stepped=v::p.stepped; sigma=sub::p.sigma} ;; let get_subterms_with_head hd_var = let rec aux lev inert_done = function - | C | V _ | B -> [] | L t -> aux (lev+1) false t + | C | V _ -> [] | A(t1,t2) as t -> let hd_var', n_args' = get_inert t1 in if not inert_done && hd_var' = V (hd_var + lev) @@ -195,7 +188,6 @@ let rec purify = function | A (t1,t2) -> Pure.A (purify t1, purify t2) | V n -> Pure.V n | C -> Pure.V (min_int/2) - | B -> Pure.B ;; let check p sigma = @@ -214,9 +206,6 @@ let check p sigma = let sanity p = print_endline (string_of_problem p); (* non cancellare *) - if p.conv = B then problem_fail p "p.conv diverged"; - if p.div = B then raise (Done p.sigma); - if p.phase = `Two && p.div = delta then raise (Done p.sigma); if not (is_inert p.div) then problem_fail p "p.div converged"; (* Trailing constant args can be removed because do not contribute to eta-diff *) let rec remove_trailing_constant_args = function @@ -265,7 +254,6 @@ let compute_max_lambdas_at hd_var j = else id) (max (aux hd t1) (aux hd t2)) | L t -> aux (hd+1) t | V _ | C -> 0 - | _ -> assert false in aux hd_var ;; @@ -283,48 +271,11 @@ let smallest_such_that p = aux 0 ;; -(* 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, k = get_inert p.div in - match var with - | C | L _ | B | A _ -> assert false - | V var -> - let phase = p.phase in - let p = - match phase with - | `One -> - let i = - match smallest_such_that (fun x -> not (is_constant x)) (args_of_inert p.div) with - Some i -> i - | None -> assert false (*CSC: backtrack? *) in - let n = 1 + max - (compute_max_lambdas_at var (k-i-1) p.div) - (compute_max_lambdas_at var (k-i-1) p.conv) in - (* apply fresh vars *) - let p, t = fold_nat (fun (p, t) _ -> - let p, v = freshvar p in - p, A(t, V (v + k)) - ) (p, V (k-1-i)) n in - let p = {p with phase=`Two} in - let t = A(t, delta) in - let t = fold_nat (fun t m -> if k-m = i then t else A(t, V (k-m))) t k in - let subst = var, mk_lams t k in - let p = subst_in_problem subst p in - let _, args = get_inert p.div in - {p with div = inert_cut_at (args-k) p.div} - | `Two -> - let subst = var, mk_lams delta k in - subst_in_problem subst p in - sanity p -;; - (* step on the head of div, on the k-th argument, with n fresh vars *) let step k n p = let hd, _ = get_inert p.div in match hd with - | C | L _ | B | A _ -> assert false + | C | L _ | A _ -> assert false | V var -> print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^ "th)"); let p, t = (* apply fresh vars *) @@ -374,7 +325,6 @@ print_cmd "FINISH" ""; 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 - let p = {p with phase=`Two} in sanity p ;; @@ -382,7 +332,7 @@ let auto p = let rec aux p = let hd, n_args = get_inert p.div in match hd with - | C | L _ | B | A _ -> assert false + | C | L _ | A _ -> assert false | V hd_var -> let tms = get_subterms_with_head hd_var p.conv in if List.exists (fun t -> snd (get_inert t) >= n_args) tms @@ -408,13 +358,6 @@ let auto p = raise (Fail(-1, "no similar terms")) ) else - (* - (let phase = p.phase in - let p = eat p in - if phase = `Two - then problem_fail p "Auto.2 did not complete the problem" - else aux p) - *) problem_fail (finish p) "Finish did not complete the problem" in try @@ -425,19 +368,19 @@ let auto p = let problem_of (label, div, convs, ps, var_names) = print_hline (); let rec aux lev = function - | `Lam(_, t) -> L (aux (lev+1) t) - | `I (v, args) -> Listx.fold_left (fun x y -> mk_app x (aux lev y)) (aux lev (`Var v)) args + | `Lam(_, t) -> L (aux (lev+1) t, []) + | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else V v | `N _ | `Match _ -> assert false in assert (List.length ps = 0); let convs = List.rev convs in - let conv = List.fold_left (fun x y -> mk_app x (aux 0 (y :> Num.nf))) (V (List.length var_names)) convs in + let conv = List.fold_left (fun x y -> fst (mk_app x (aux 0 (y :> Num.nf)))) (V (List.length var_names)) convs in let var_names = "@" :: var_names in let div = match div with | Some div -> aux 0 (div :> Num.nf) | None -> assert false in let varno = List.length var_names in - {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} + {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]} ;; let solve p =