let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
let relevance v = float !(v.uses) /. float !(v.nominations) in
let vcompare (_,v1) (_,v2) =
let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
let relevance v = float !(v.uses) /. float !(v.nominations) in
let vcompare (_,v1) (_,v2) =
(fun ty ctx_entry ->
match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
(fun ty ctx_entry ->
match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
- | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
- | name, NCic.Def(bo, _) -> n+1,l)
+ | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l
+ | _name, NCic.Def(_bo, _) -> n+1,l)
List.fold_left
(fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
let ikind = NCicUntrusted.kind_of_meta iattr in
List.fold_left
(fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
let ikind = NCicUntrusted.kind_of_meta iattr in
- let metasenv,j,instance,ty =
+ let metasenv,_j,instance,ty =
NCicMetaSubst.mk_meta ~attrs:iattr
metasenv ctx ~with_type:ty ikind in
let s_entry = i,(iattr, ctx, instance, ty) in
NCicMetaSubst.mk_meta ~attrs:iattr
metasenv ctx ~with_type:ty ikind in
let s_entry = i,(iattr, ctx, instance, ty) in
- (fun (subst,objs) (i,(iattr,ctx,ty)) ->
+ (fun (subst,objs) (i,(_iattr,ctx,ty)) ->
let ty = NCicUntrusted.apply_subst status subst ctx ty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
subst ctx in
let ty = NCicUntrusted.apply_subst status subst ctx ty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
subst ctx in
- let (uri,_,_,_,obj) as okind =
+ let (uri,_,_,_,_obj) as okind =
- (fun ty (i,(iattr,ctx,mty)) ->
+ (fun ty (i,(_iattr,ctx,mty)) ->
let mty = NCicUntrusted.apply_subst status subst ctx mty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
let mty = NCicUntrusted.apply_subst status subst ctx mty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
- let n,h,metasenv,subst,o = status#obj in
- let gname, ctx, gty = List.assoc g metasenv in
+ let n,h,metasenv,_subst,o = status#obj in
+ let _gname, ctx, gty = List.assoc g metasenv in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t `XTNone in
let status,t = term_of_cic_term status t ctx in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t `XTNone in
let status,t = term_of_cic_term status t ctx in
raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
(* FG: for now we catch TypeCheckerFailure; to be understood *)
raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
(* FG: for now we catch TypeCheckerFailure; to be understood *)
debug_print ~depth (lazy "strange application"); None)
else
*) (incr candidate_no; Some ((!candidate_no,t),status))
debug_print ~depth (lazy "strange application"); None)
else
*) (incr candidate_no; Some ((!candidate_no,t),status))
s = "cic:/matita/basics/logic/eq.ind" ||
s = "cic:/matita/basics/logic/sym_eq.con" ||
s = "cic:/matita/basics/logic/trans_eq.con" ||
s = "cic:/matita/basics/logic/eq.ind" ||
s = "cic:/matita/basics/logic/sym_eq.con" ||
s = "cic:/matita/basics/logic/trans_eq.con" ||
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let _, raw_gty = term_of_cic_term status gty context in
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let _, raw_gty = term_of_cic_term status gty context in
let status, t = term_of_cic_term status gty context in
let t = NCicReduction.whd status subst context t in
match t with
let status, t = term_of_cic_term status gty context in
let t = NCicReduction.whd status subst context t in
match t with
if flags.local_candidates then global_cands,smart_global_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
if flags.local_candidates then global_cands,smart_global_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
in filter global_cands,filter smart_global_cands
in
(* we now compute local candidates *)
in filter global_cands,filter smart_global_cands
in
(* we now compute local candidates *)
if flags.local_candidates then local_cands,smart_local_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
if flags.local_candidates then local_cands,smart_local_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
in filter local_cands,filter smart_local_cands
in
(* we now splits candidates in facts or not facts *)
in filter local_cands,filter smart_local_cands
in
(* we now splits candidates in facts or not facts *)
let t = mk_cic_term ctx (NCic.Rel 1) in
let status, keys = keys_of_term status t in
let facts = List.fold_left (add_to_th t) facts keys in
let t = mk_cic_term ctx (NCic.Rel 1) in
let status, keys = keys_of_term status t in
let facts = List.fold_left (add_to_th t) facts keys in
if top then
let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
{cache with unit_eq = unit_eq}
if top then
let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
{cache with unit_eq = unit_eq}
debug_print ~depth (lazy "entering auto main");
debug_print ~depth (pptrace status cache.trace);
debug_print ~depth (lazy ("stack length = " ^
debug_print ~depth (lazy "entering auto main");
debug_print ~depth (pptrace status cache.trace);
debug_print ~depth (lazy ("stack length = " ^
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache *)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- | orig::_ ->
- if depth > 0 && move_to_side depth status
- then
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache*)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- else
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache *)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ | _orig::_ ->
+ if depth > 0 && move_to_side depth status
+ then
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache*)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ else
let ng = List.length goals in
(* moved inside auto_clusters *)
if ng > flags.maxwidth then begin
let ng = List.length goals in
(* moved inside auto_clusters *)
if ng > flags.maxwidth then begin
let status, res = disambiguate status ctx t `XTNone in
let _,res = term_of_cic_term status res (ctx_of res)
in Ast.NCic res
let status, res = disambiguate status ctx t `XTNone in
let _,res = term_of_cic_term status res (ctx_of res)
in Ast.NCic res
- in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
- Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
- Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
- Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
- ])
+ in Some (List.map to_Ast l)
+(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases
+ @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+ Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+ Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+ Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+ ]
+*)
let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let candidates = candidates_from_ctx univ [] status in
let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let candidates = candidates_from_ctx univ [] status in