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
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
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
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;
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"));
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) =
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}.
∀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.
}.
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.
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.
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.
projects / helm.git / commitdiff