From: acondolu Date: Tue, 18 Sep 2018 14:26:08 +0000 (+0200) Subject: New measure which looks promising X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=refs%2Fheads%2Fmeasure_tmp;p=fireball-separation.git New measure which looks promising - idea of nesting in paths - relies heavily on special k (behavior still not explained) - interactive mode to experiment with stepping Missing: - auto - finish - check / purification --- diff --git a/ocaml/simple.ml b/ocaml/simple.ml index b1b05ec..b76a654 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -6,13 +6,7 @@ let print_hline = Console.print_hline;; open Pure -type var_flag = [ - `Inherit | `Some of bool ref - (* bool: - true if original application and may determine a distinction - *) - | `Duplicate -] ;; +type var_flag = bool ;; type var = int;; type t = @@ -21,47 +15,19 @@ type t = | L of t ;; -let index_of x = - let rec aux n = - function - [] -> None - | x'::_ when x == x' -> Some n - | _::xs -> aux (n+1) xs - in aux 1 -;; - -let sep_of_app = - let apps = ref [] in - function - r when not !r -> " " - | r -> - let i = - match index_of r !apps with - Some i -> i - | None -> - apps := !apps @ [r]; - List.length !apps - in " " ^ string_of_int i ^ ":" -;; -let string_of_var_flag = function - | `Some b -> sep_of_app b - | `Inherit -> " ?" - | `Duplicate -> " !" - ;; - - let string_of_t = + let sep_of_app b = if b then " +" else " " in let string_of_bvar = let bound_vars = ["x"; "y"; "z"; "w"; "q"] in let bvarsno = List.length bound_vars in - fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in + fun nn -> if nn < bvarsno then List.nth bound_vars nn else "v" ^ (string_of_int (nn - bvarsno + 1)) in let rec string_of_term_w_pars level = function - | V v -> if v >= level then "`" ^ string_of_int (v-level) else + | V v -> if v >= level then string_of_int (v-level) else string_of_bvar (level - v-1) | A _ | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")" and string_of_term_no_pars_app level = function - | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ string_of_var_flag b ^ string_of_term_w_pars level t2 + | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ sep_of_app b ^ string_of_term_w_pars level t2 | _ as t -> string_of_term_w_pars level t and string_of_term_no_pars level = function | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t @@ -69,44 +35,32 @@ let string_of_t = in string_of_term_no_pars 0 ;; - -let delta = L(A(`Some (ref true),V 0, V 0));; - (* does NOT lift the argument *) let mk_lams = fold_nat (fun x _ -> L x) ;; let measure_of_t = - let rec aux acc = function - | V _ -> acc, 0 + let rec aux = function + | V _ -> 0 | A(b,t1,t2) -> - let acc, m1 = aux acc t1 in - let acc, m2 = aux acc t2 in - (match b with - | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2 - | _ -> acc, m1 + m2) - | L t -> aux acc t - in snd ++ (aux []) + (if b then 1 else 0) + aux t1 + aux t2 + | L t -> aux t + in aux ;; type problem = { orig_freshno: int ; freshno : int - ; div : t - ; conv : t + ; tms : t list ; sigma : (var * t) list (* substitutions *) - ; phase : [`One | `Two] (* :'( *) } let string_of_problem p = - let lines = [ - "[measure] " ^ string_of_int (measure_of_t p.div); - "[DV] " ^ string_of_t p.div; - "[CV] " ^ string_of_t p.conv; - ] in + let measure = List.fold_left (+) 0 (List.map measure_of_t p.tms) in + let lines = ("[measure] " ^ string_of_int measure) :: + List.map (fun x -> "[TM] " ^ string_of_t x) p.tms in String.concat "\n" lines ;; -exception B;; exception Done of (var * t) list (* substitution *);; exception Fail of int * string;; @@ -146,39 +100,43 @@ let rec no_leading_lambdas v n = function let rec erase = function | L t -> L (erase t) - | A(_,t1,t2) -> A(`Some(ref false), erase t1, erase t2) + | A(_,t1,t2) -> A(false, erase t1, erase t2) | V _ as t -> t ;; -let rec subst top level delift ((flag, var, tm) as sub) = +let explode = + let rec aux args = function + | L _ -> assert false + | V _ as x -> x, args + | A(b,t1,t2) -> aux ((b,t2)::args) t1 + in aux [] +;; + +let rec implode hd args = + match args with + | [] -> hd + | (f,a)::args -> implode (A(f,hd,a)) args +;; + +let get_head = + let rec aux lev = function + | L t -> aux (lev+1) t + | A(_,t,_) -> aux lev t + | V v -> v - lev + in aux 0 +;; + +let rec subst level delift ((var, tm) as sub) = function | V v -> if v = level + var then lift level tm else V (if delift && v > level then v-1 else v) - | L t -> L (subst top (level + 1) delift sub t) + | L t -> L (subst (level + 1) delift sub t) | A(b,t1,t2) -> - let special = b = `Duplicate && top && t2 = V (level + var) in - let t1' = subst (if special then false else top) level delift sub t1 in - let t2' = subst false level delift sub t2 in - match b with - | `Duplicate when special -> - assert (match t1' with L _ -> false | _ -> true) ; - (match flag with - | `Some b when !b -> b := false - | `Some b -> () - (*print_string "WARNING! Stepping on a useless argument!"; - ignore(read_line())*) - | `Inherit | `Duplicate -> assert false); - A(flag, t1', erase t2') - | `Inherit | `Duplicate -> - let b' = if t2 = V (level + var) - then (assert (flag <> `Inherit); flag) - else b in - assert (match t1' with L _ -> false | _ -> true) ; - A(b', t1', t2') - | `Some b' -> mk_app top b' t1' t2' -and mk_app top flag t1 t2 = if t1 = delta && t2 = delta then raise B - else match t1 with - | L t1 -> subst top 0 true (`Some flag, 0, t2) t1 - | _ -> A (`Some flag, t1, t2) + let t1' = subst level delift sub t1 in + let t2' = subst level delift sub t2 in + mk_app b t1' t2' +and mk_app flag t1 t2 = match t1 with + | L t1 -> subst 0 true (0, t2) t1 + | _ -> A (flag, t1, t2) and lift n = let rec aux lev = function @@ -187,14 +145,18 @@ and lift n = | A (b,t1, t2) -> A (b,aux lev t1, aux lev t2) in aux 0 ;; -let subst top = subst top 0 false;; -let mk_app = mk_app true;; +let subst = subst 0 false;; +(* let mk_app = mk_app true;; *) +let rec mk_apps t = function + | [] -> t + | (f,x)::xs -> mk_apps (mk_app f t x) xs +;; let eta_eq = let rec aux t1 t2 = match t1, t2 with | L t1, L t2 -> aux t1 t2 - | L t1, t2 -> aux t1 (A(`Some (ref true),lift 1 t2,V 0)) - | t1, L t2 -> aux (A(`Some (ref true),lift 1 t1,V 0)) t2 + | L t1, t2 -> aux t1 (A(false,lift 1 t2,V 0)) + | t1, L t2 -> aux (A(false,lift 1 t1,V 0)) t2 | V a, V b -> a = b | A(_,t1,t2), A(_,u1,u2) -> aux t1 u1 && aux t2 u2 | _, _ -> false @@ -212,25 +174,9 @@ let eta_subterm u = let subst_in_problem ?(top=true) ((v, t) as sub) p = print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t); let sigma = sub::p.sigma in - let sub = (`Inherit, v, t) in - let div = try subst top sub p.div with B -> raise (Done sigma) in - let conv = try subst false sub p.conv with B -> raise (Fail(-1,"p.conv diverged")) in - {p with div; conv; sigma} -;; - -let get_subterm_with_head_and_args hd_var n_args = - let rec aux lev = function - | V _ -> None - | L t -> aux (lev+1) t - | A(_,t1,t2) as t -> - let hd_var', n_args' = get_inert t1 in - if hd_var' = hd_var + lev && n_args <= 1 + n_args' - (* the `+1` above is because of t2 *) - then Some (lift ~-lev t) - else match aux lev t2 with - | None -> aux lev t1 - | Some _ as res -> res - in aux 0 + let sub = (v, t) in + let tms = List.map (subst sub) p.tms in + {p with tms; sigma} ;; let rec purify = function @@ -240,9 +186,9 @@ let rec purify = function ;; let check p sigma = - print_endline "Checking..."; - let div = purify p.div in - let conv = purify p.conv in + assert false (* FIXME *) + (* print_endline "Checking..."; + let tms = List.map purify p.tms in let sigma = List.map (fun (v,t) -> v, purify t) sigma in let freshno = List.fold_right (max ++ fst) sigma 0 in let env = Pure.env_of_sigma freshno sigma in @@ -250,207 +196,95 @@ let check p sigma = print_endline " D diverged."; assert (not (Pure.diverged (Pure.mwhd (env,conv,[])))); print_endline " C converged."; - () + () *) ;; let sanity p = print_endline (string_of_problem p); (* non cancellare *) - 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"; + let rec all_different = function + | [] -> true + | x::xs -> List.for_all ((<>) x) xs && all_different xs in + if List.for_all is_var p.tms && all_different p.tms + then raise (Done p.sigma); + if List.exists (not ++ is_inert) p.tms + then problem_fail p "used a non-effective path"; p ;; -(* drops the arguments of t after the n-th *) -(* FIXME! E' usato in modo improprio contando sul fatto - errato che ritorna un inerte lungo esattamente n *) -let inert_cut_at n t = - let rec aux t = - match t with - | V _ as t -> 0, t - | A(_,t1,_) as t -> - let k', t' = aux t1 in - if k' = n then n, t' - else k'+1, t - | _ -> assert false - in snd (aux t) -;; - -(* return the index of the first argument with a difference - (the first argument is 0) - precondition: p.div and t have n+1 arguments - *) -let find_eta_difference p t argsno = - let t = inert_cut_at argsno t in - let rec aux t u k = match t, u with - | V _, V _ -> None - | A(b1,t1,t2), A(b2,u1,u2) -> - (match aux t1 u1 (k-1) with - | None -> - if not (eta_eq t2 u2) then begin - let is_relevant = function `Some b -> !b | _ -> false in - if not (is_relevant b1 || is_relevant b2) then begin - print_string "WARNING! Stepping on a useless argument!"; -print_string (string_of_t t ^ " <==> " ^ string_of_t u); - ignore(read_line()) - end ; - Some (k-1) - end - else None - | Some j -> Some j) - | _, _ -> assert false - in match aux p.div t argsno with - | None -> problem_fail p "no eta difference found (div subterm of conv?)" - | Some j -> j -;; - -let compute_max_lambdas_at hd_var j = - let rec aux hd = function - | A(_,t1,t2) -> - (if get_inert t1 = (hd, j) - then max ( (*FIXME*) - if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd - then let hd', j' = get_inert t2 in j - j' - else no_leading_lambdas hd_var j t2) - else id) (max (aux hd t1) (aux hd t2)) - | L t -> aux (hd+1) t - | V _ -> 0 - in aux hd_var -;; - let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);; -(* step on the head of div, on the k-th argument, with n fresh vars *) -let step ?(isfinish=false) k n p = - let var, _ = get_inert p.div in -print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")"); - let p, t = (* apply fresh vars *) - fold_nat (fun (p, t) _ -> - let p, v = freshvar p in - p, A(`Some (ref false), t, V (v + k + 1)) - ) (p, V 0) n in - let t = (* apply bound variables V_k..V_0 *) - fold_nat (fun t m -> A((if m = k+1 then `Duplicate else `Inherit), t, V (k-m+1))) t (k+1) in - let t = mk_lams t (k+1) in (* make leading lambdas *) - let subst = var, t in - let p = subst_in_problem ~top:(not isfinish) subst p in - sanity p +let step var j n p = + let atsnd f (a,b) = (a, f b) in + let p, alphas = (* make fresh vars *) + fold_nat (fun (p, vs) _ -> + let p, v = freshvar p in + p, v::vs + ) (p, []) n in let alphas = List.rev alphas in + let rec aux lev (inside:bool) = function + | L t -> L (aux (lev+1) inside t) + | _ as x -> + let hd, args = explode x in + if hd = V (var+lev) then + (let nargs = List.length args in + let k = max 0 (j + 1 - nargs) in + let args = List.mapi + (fun i (f, t) -> f, lift k (aux lev (if i=j then true else inside) t)) args in + let bound = fold_nat (fun x n -> (false,V(n-1)) :: x) [] k in + let args = args @ bound in + let _, head = List.nth args j in + let args = List.mapi + (fun i (f, t) -> (if i=j && not inside then false else f), if i=j && not inside then erase t else t) args in + let head = (if inside then erase else id) head in + print_endline ("HEAD: " ^ string_of_t head); + let alphas = List.map (fun v -> false, V(lev+k+v)) alphas in + let t = mk_apps head (alphas @ args) in + let t = mk_lams t k in + t + ) else + (let args = List.map (atsnd (aux lev inside)) args in + implode hd args) in + let sigma = (var, aux 0 false (V var)) :: p.sigma in + {p with tms=List.map (aux 0 false) p.tms; sigma} ;; -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 ~isfinish:true 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 finish p = assert false ;; -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 - if phase = `Two - 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 - (compute_max_lambdas_at hd_var j p.div) - (compute_max_lambdas_at hd_var j p.conv) in - let m1 = measure_of_t p.div in - let p = step j k p in - let m2 = measure_of_t p.div in - (if m2 >= m1 then - (print_string ("WARNING! Measure did not decrease : " ^ string_of_int m2 ^ " >= " ^ string_of_int m1 ^ " (press )"); - ignore(read_line()))); - auto p -;; +let rec auto p = assert false ;; let problem_of (label, div, convs, ps, var_names) = print_hline (); let rec aux = function | `Lam(_,t) -> L (aux t) - | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app (ref true) x (aux y)) (V v) args + | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app true x (aux y)) (V v) args | `Var(v,_) -> V v | `N _ | `Match _ -> assert false in - assert (List.length ps = 0); let convs = (List.rev convs :> Num.nf list) in - let conv = aux - (if List.length convs = 1 - then List.hd convs - else `I((List.length var_names, min_int), Listx.from_list convs)) in - let var_names = "@" :: var_names in - let div = match div with - | Some div -> aux (div :> Num.nf) - | None -> assert false in + let tms = List.map aux (convs @ (ps :> Num.nf list)) in + let tms = match div with + | Some div -> aux (div :> Num.nf) :: tms + | None -> tms in let varno = List.length var_names in - let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; phase=`One} in + let p = {orig_freshno=varno; freshno=1+varno; tms; sigma=[]} in (* initial sanity check *) sanity p ;; +let rec interactive p = + print_string "[varno index alphano] "; + let s = read_line () in + let spl = Str.split (Str.regexp " +") s in + let nth n = int_of_string (List.nth spl n) in + let p = step (nth 0) (nth 1) (nth 2) p in + interactive (sanity p) +;; + let solve p = - if eta_subterm p.div p.conv - then print_endline "!!! div is subterm of conv. Problem was not run !!!" - else check p (auto p) + let rec aux = function + | [] -> false + | x::xs -> List.exists (eta_subterm x) xs || aux xs in + if aux p.tms + then print_endline "!!! Problem stopped: subterm problem !!!" + else check p (interactive p) ;; Problems.main (solve ++ problem_of); - -(* Example usage of interactive: *) - -(* let interactive div conv cmds = - let p = problem_of div conv in - try ( - let p = List.fold_left (|>) p cmds in - let rec f p cmds = - let nth spl n = int_of_string (List.nth spl n) in - let read_cmd () = - let s = read_line () in - let spl = Str.split (Str.regexp " +") s in - s, let uno = List.hd spl in - try if uno = "eat" then eat - else if uno = "step" then step (nth spl 1) (nth spl 2) - else failwith "Wrong input." - with Failure s -> print_endline s; (fun x -> x) in - let str, cmd = read_cmd () in - let cmds = (" " ^ str ^ ";")::cmds in - try - let p = cmd p in f p cmds - with - | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds) - in f p [] - ) with Done _ -> () -;; *) - -(* interactive "x y" - "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat] -;; *)