From 1e16d80cc7bf9b73cf5526934b17e2ba955a522a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 13:37:34 +0000 Subject: [PATCH] nauto: - fixed indexing (now always dome in the same way) - depth=x means: tray at depth=2 ... try at depth=x - run auto on set of goals that are linked by occurring in each others types, simply distribute if there is no dependency --- helm/software/components/ng_tactics/nAuto.ml | 184 +++++++++++++----- .../components/ng_tactics/nTacStatus.ml | 12 +- .../components/ng_tactics/nTacStatus.mli | 2 + .../matita/nlibrary/topology/cantor.ma | 27 +-- .../software/matita/nlibrary/topology/igft.ma | 1 + 5 files changed, 151 insertions(+), 75 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index d3409bcbe..8506c3adb 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -915,37 +915,50 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa type th_cache = (NCic.context * InvRelDiscriminationTree.t) list +let keys_of_term status t = + let status, orig_ty = typeof status (ctx_of t) t in + let _, ty, _ = saturate ~delta:max_int status orig_ty in + let keys = [ty] in + let keys = + let _, ty = term_of_cic_term status ty (ctx_of ty) in + match ty with + | NCic.Const (NReference.Ref (_,NReference.Def h)) + | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) + when h > 0 -> + let _,ty,_= saturate status ~delta:(h-1) orig_ty in + ty::keys + | _ -> keys + in + status, keys +;; + let mk_th_cache status gl = List.fold_left (fun (status, acc) g -> let gty = get_goalty status g in let ctx = ctx_of gty in + debug_print(lazy("th cache for: "^ppterm status gty)); + debug_print(lazy("th cache in: "^ppcontext status ctx)); if List.mem_assq ctx acc then status, acc else let idx = InvRelDiscriminationTree.empty in let status,_,idx = - List.fold_left (fun (status, i, idx) _ -> - let t = mk_cic_term ctx (NCic.Rel i) in - let status, orig_ty = typeof status ctx t in - let _, ty, _ = saturate ~delta:max_int status orig_ty in - let idx = InvRelDiscriminationTree.index idx ty t in - let idx = - let _, ty = term_of_cic_term status ty (ctx_of ty) in - match ty with - | NCic.Const (NReference.Ref (_,NReference.Def h)) - | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) - when h > 0 -> - let _,ty,_= saturate status ~delta:(h-1) orig_ty in - InvRelDiscriminationTree.index idx ty t - | _ -> idx - in - status, i+1, idx) + List.fold_left + (fun (status, i, idx) _ -> + let t = mk_cic_term ctx (NCic.Rel i) in + debug_print(lazy("indexing: "^ppterm status t)); + let status, keys = keys_of_term status t in + let idx = + List.fold_left (fun idx k -> + InvRelDiscriminationTree.index idx k t) idx keys + in + status, i+1, idx) (status, 1, idx) ctx in status, (ctx, idx) :: acc) (status,[]) gl ;; -let add_to_th t ty c = +let add_to_th t c ty = let key_c = ctx_of t in if not (List.mem_assq key_c c) then (key_c ,InvRelDiscriminationTree.index @@ -960,6 +973,25 @@ let add_to_th t ty c = replace c ;; +let pp_idx status idx = + InvRelDiscriminationTree.iter idx + (fun k set -> + debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k)); + Ncic_termSet.iter + (fun t -> debug_print(lazy("\t"^ppterm status t))) + set) +;; + +let pp_th status = + List.iter + (fun ctx, idx -> + debug_print(lazy( "-----------------------------------------------")); + debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx))); + debug_print(lazy( "||====> ")); + pp_idx status idx) +;; + + let search_in_th gty th = let c = ctx_of gty in let rec aux acc = function @@ -975,20 +1007,6 @@ let search_in_th gty th = in aux Ncic_termSet.empty c ;; - -let pp_th status = - List.iter - (fun ctx, idx -> - prerr_endline "-----------------------------------------------"; - prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx); - prerr_endline "||====> "; - InvRelDiscriminationTree.iter idx - (fun k set -> - prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k); - Ncic_termSet.iter - (fun t -> prerr_endline ("\t"^ppterm status t)) set)) -;; - type cache_examination_result = [ `Failed_in of int | `UnderInspection @@ -1163,14 +1181,11 @@ let intro_case status gno gty depth cache name = let open_goals = head_goals status#stack in assert (List.length open_goals = 1); let open_goal = List.hd open_goals in - let status, cache = - let ngty = get_goalty status open_goal in - let ctx = ctx_of ngty in - let t = mk_cic_term ctx (NCic.Rel 1) in - let status, ty = typeof status ctx t in - let _status, ty, _args = saturate status ty in - status, add_to_th t ty cache - in + let ngty = get_goalty status open_goal in + let ctx = ctx_of ngty in + let t = mk_cic_term ctx (NCic.Rel 1) in + let status, keys = keys_of_term status t in + let cache = List.fold_left (add_to_th t) cache keys in debug_print (lazy (" intro: "^ string_of_int open_goal)); (* pp_th status cache; *) incr candidate_no; @@ -1223,11 +1238,15 @@ let auto_main flags signature elems cache = aux ((s, size, don, todo, fl)::orlist, cache) | (s, size, don, todo, fl)::orlist when List.length(prop_only (d_goals todo)) > flags.maxwidth -> - debug_print (lazy ("FAIL: WIDTH")); + debug_print (lazy ("FAIL: WIDTH: " ^ + String.concat ", " + (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo)))); aux (orlist, cache) | (s, size, don, todo, fl)::orlist when size > flags.maxsize -> debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ - " > " ^ string_of_int flags.maxsize )); + " > " ^ string_of_int flags.maxsize ^ ": " ^ + String.concat ", " + (List.map (fun (x,_,_) -> string_of_int x) (d_goals todo)))); aux (orlist, cache) | _ when Unix.gettimeofday () > flags.timeout -> debug_print (lazy ("FAIL: TIMEOUT")); @@ -1315,28 +1334,85 @@ let int name l def = let auto_tac ~params:(_univ,flags) status = let goals = head_goals status#stack in let status, cache = mk_th_cache status goals in +(* pp_th status cache; *) let depth = int "depth" flags 3 in + let size = int "size" flags 10 in + let width = int "width" flags (3+List.length goals) in (* XXX fix sort *) - let goals = List.map (fun i -> D(i,depth,P)) goals in - let elems = [status,0,[],goals,[]] in + let goals depth = List.map (fun i -> D(i,depth,P)) goals in + let elems depth = [status,0,[],goals depth,[]] in let signature = () in let flags = { - maxwidth = 3 + List.length goals; - maxsize = 10; + maxwidth = width; + maxsize = size; timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in - match auto_main flags signature elems cache with - | Gaveup -> raise (Error (lazy "auto gave up", None)) - | Proved (s, (_orlist, _cache)) -> - let stack = - match s#stack with - | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest - | _ -> assert false - in - s#set_stack stack + let rec up_to x = + if x > depth then raise (Error (lazy "auto gave up", None)) + else + match auto_main flags signature (elems x) cache with + | Gaveup -> up_to (x+1) + | Proved (s, (_orlist, _cache)) -> + HLog.debug ("proved at depth " ^ string_of_int x); + let stack = + match s#stack with + | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | _ -> assert false + in + s#set_stack stack + in + up_to 2 +;; + +let group_by_tac eq_predicate tactic status = + let goals = head_goals status#stack in + if List.length goals < 2 then tactic status + else + let eq_predicate = eq_predicate status in + let rec aux classes = function + | [] -> classes + | g :: tl -> + try + let c = List.find (fun c -> eq_predicate c g) classes in + let classes = List.filter ((<>) c) classes in + aux ((g::c) :: classes) tl + with Not_found -> aux ([g] :: classes) tl + in + let classes = aux [] goals in + let pos_of l1 l2 = + let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in + List.map (fun x -> List.assoc x l2) l1 + in + NTactics.block_tac ([ NTactics.branch_tac ] + @ + HExtlib.list_concat ~sep:[NTactics.shift_tac] + (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes) + @ + [ NTactics.merge_tac ]) status +;; + +module IntSet = Set.Make(struct type t = int let compare = compare end) + +let type_dependency status gl g = + let rec closure acc = function + | [] -> acc + | x::l when IntSet.mem x acc -> closure acc l + | x::l -> + let acc = IntSet.add x acc in + let gty = get_goalty status x in + let deps = metas_of_term status gty in + closure acc (deps @ l) + in + not (IntSet.is_empty + (IntSet.inter + (closure IntSet.empty gl) + (closure IntSet.empty [g]))) ;; +let auto_tac ~params = + group_by_tac type_dependency (auto_tac ~params) +;; (* ========================= dispatching of auto/auto_paramod ============ *) let auto_tac ~params:(_,flags as params) = diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 462501e66..ed583fdaf 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -407,6 +407,11 @@ let apply_subst status ctx t = status, (ctx, NCicUntrusted.apply_subst subst ctx t) ;; +let metas_of_term status (context,t) = + let _,_,_,subst,_ = status#obj in + NCicUntrusted.metas_of_term subst context t +;; + (* ============= move this elsewhere ====================*) class ['stack] status = @@ -445,6 +450,8 @@ let ppelem = function | Dead -> "Dead" ;; +let string_of_path l = String.concat "." (List.map ppelem l) ;; + let path_string_of (ctx,t) = let len_ctx = List.length ctx in let rec aux arity = function @@ -463,7 +470,9 @@ let path_string_of (ctx,t) = | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)] | NCic.Match _ -> [Dead] in - aux 0 t + let path = aux 0 t in +(* prerr_endline (string_of_path path); *) + path ;; let compare e1 e2 = @@ -474,7 +483,6 @@ let compare e1 e2 = | e1,e2 -> Pervasives.compare e1 e2 ;; -let string_of_path l = String.concat "." (List.map ppelem l) ;; end diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index fdad9f861..f3bdd5aa1 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -40,6 +40,7 @@ val analyse_indty: 'status * (NReference.reference * int * NCic.term list * NCic.term list) val ppterm: #pstatus -> cic_term -> string +val ppcontext: #pstatus -> NCic.context -> string val whd: #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term -> 'status * cic_term @@ -58,6 +59,7 @@ val apply_subst: val fix_sorts: cic_term -> cic_term val saturate : #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list +val metas_of_term : #pstatus as 'status -> cic_term -> int list val get_goalty: #pstatus -> int -> cic_term val mk_meta: diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index 6ae8d36ad..f9655f4ca 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -14,11 +14,7 @@ alias symbol "covers" (instance 1) = "covers". alias symbol "covers" (instance 2) = "covers set". alias symbol "covers" (instance 3) = "covers". ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V. -#A; #a; #U; #V; #aU; #UV; -nelim aU; -##[ #c; #H; nauto; -##| #c; #i; #HCU; #H; @2 i; nauto; -##] +#A; #a; #U; #V; #aU; #UV; nelim aU; nauto depth=4; nqed. ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}. @@ -33,11 +29,7 @@ ntheorem th2_3 : ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i. #A; #a; #H; nelim H; ##[ #n; *; -##| #b; #i_star; #IH1; #IH2; - ncases (EM … b i_star); - ##[##2: (* nauto; *) #W; @i_star; napply W; - ##| nauto; - ##] +##| #b; #i_star; #IH1; #IH2; ncases (EM … b i_star); nauto; ##] nqed. @@ -57,7 +49,8 @@ nrecord uAx : Type[1] ≝ { }. ndefinition uax : uAx → Ax. -#A; @ (uax_ A) (λx.unit); #a; #_; napply (𝐂 a ?); nlapply one; ncases (with_ A a); nauto; +#A; @ (uax_ A) (λx.unit); #a; #_; +napply (𝐂 a ?); nlapply one; ncases (with_ A a); nauto; nqed. ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax. @@ -77,19 +70,17 @@ unification hint 0 ≔ ; ntheorem col2_4 : - ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##] + ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a one. #A; #a; #H; nelim H; ##[ #n; *; -##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); #H4; nauto; +##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); nauto; ##] nqed. ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }. ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V. -#A; #a; #U; #V; #HUV; #H; nelim H; -##[ nauto; -##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##] +#A; #a; #U; #V; #HUV; #H; nelim H; nauto depth=4; nqed. ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z. @@ -136,9 +127,7 @@ naxiom Ph : ∀x.h x = O \liff x ◃ ∅. nlemma replace_char: ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V. -#A; #U; #V; #a; #H1; #H2; #E; nelim E; -##[ #b; #Hb; @; nauto; -##| #b; #i; #H3; #H4; @2 i; #c; #Hc; nauto; ##] +#A; #U; #V; #UV; #VU; #a; #aU; nelim aU; nauto; nqed. ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x. diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index e5859f03a..06c492e86 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1168,6 +1168,7 @@ We now proceed with the proof of the infinity rule. D*) +alias symbol "covers" = "new covers set". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. #A; #U; #a; (** screenshot "n-cov-inf-1". *) -- 2.39.2