let print ?(depth=0) s =
prerr_endline (String.make (2*depth) ' '^Lazy.force s)
-let noprint ?(depth=0) _ = ()
+let noprint ?depth:(_=0) _ = ()
let debug_print = noprint
open Continuationals.Stack
else true
with Not_found -> true
-let print_stat status tbl =
+let print_stat _status tbl =
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) =
end
;;
-let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps =
- if flag then
- NCicParamod.empty_state
- else begin
+let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps =
noprint (lazy "indexing equations");
let eq_cache,lemmas =
match lemmas with
| NCicTypeChecker.TypeCheckerFailure _
| NCicTypeChecker.AssertFailure _ -> eq_cache)
eq_cache lemmas
- end
;;
-let fast_eq_check_tac ~params s =
+let fast_eq_check_tac ~params:_ s =
let unit_eq = index_local_equations s#eq_cache s in
dist_fast_eq_check unit_eq s
;;
| s::_ -> s
;;
-let paramod_tac ~params s =
+let paramod_tac ~params:_ s =
let unit_eq = index_local_equations s#eq_cache s in
NTactics.distribute_tac (paramod unit_eq) s
;;
(fun ty ctx_entry ->
match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
- | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
+ | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
;;
let args_for_context ?(k=1) ctx =
List.fold_left
(fun (n,l) ctx_entry ->
match ctx_entry with
- | 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)
(k,[]) ctx in
args
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
*)
let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
List.fold_left
- (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 (uri,_,_,_,obj) as okind =
+ let (uri,_,_,_,_obj) as okind =
constant_for_meta status ctx ty i in
try
NCicEnvironment.check_and_add_obj status okind;
| _ -> let args =
List.map (NCicSubstitution.subst_meta status lc) args in
NCic.Appl(NCic.Rel k::args))
- | NCic.Meta (j,lc) as m ->
+ | NCic.Meta (_j,lc) as m ->
(match lc with
_,NCic.Irl _ -> m
| n,NCic.Ctx l ->
let close_wrt_metasenv status subst =
List.fold_left
- (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
aux metasenv ty []
let smart_apply t unit_eq status g =
- 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
debug_print(lazy("ritorno da fast_eq_check"));
res
with
- | NCicEnvironment.ObjectNotFound s as e ->
+ | NCicEnvironment.ObjectNotFound _s as e ->
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 *)
unit_eq = unit_eq;
trace = trace}
-let only signature _context candidate = true
+let only _signature _context _candidate = true
(*
(* TASSI: nel trie ci mettiamo solo il body, non il ty *)
let candidate_ty =
if level = 0 then []
else match gs with
| [] -> assert false
- | (g,_,_,_)::s ->
+ | (g,_,_,_,_)::s ->
let is_open = function
| (_,Continuationals.Stack.Open i) -> Some i
| (_,Continuationals.Stack.Closed _) -> None
let open_goals level status = stack_goals level status#stack
;;
-let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
+let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
try
- let old_og_no = List.length (open_goals (depth+1) status) in
+ (*let old_og_no = List.length (open_goals (depth+1) status) in*)
debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
^ (NotationPp.pp_term status) t));
let status =
debug_print ~depth (lazy "strange application"); None)
else
*) (incr candidate_no; Some ((!candidate_no,t),status))
- with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
+ with Error _ -> debug_print ~depth (lazy "failed"); None
;;
let sort_of status subst metasenv ctx t =
cands, diff more_cands cands
;;
-let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
+let is_a_needed_uri s =
+ 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_f3.con" ||
+ s = "cic:/matita/basics/logic/eq_f2.con" ||
+ s = "cic:/matita/basics/logic/eq_f.con"
+
+let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty =
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 is_prod, is_eq =
+ let is_prod, _is_eq =
let status, t = term_of_cic_term status gty context in
let t = NCicReduction.whd status subst context t in
match t with
in
(* we now compute global candidates *)
let global_cands, smart_global_cands =
- if flags.local_candidates then
- let mapf s =
- let to_ast = function
- | NCic.Const r when true
- (*is_relevant statistics r*) -> Some (Ast.NRef r)
- (* | NCic.Const _ -> None *)
- | _ -> assert false in
- HExtlib.filter_map
- to_ast (NDiscriminationTree.TermSet.elements s) in
- let g,l =
- get_cands
- (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
- NDiscriminationTree.TermSet.diff
- NDiscriminationTree.TermSet.empty
- raw_gty raw_weak_gty in
- mapf g, mapf l
- else [],[] in
+ let mapf s =
+ let to_ast = function
+ | NCic.Const r when true
+ (*is_relevant statistics r*) -> Some (Ast.NRef r)
+ (* | NCic.Const _ -> None *)
+ | _ -> assert false in
+ HExtlib.filter_map
+ to_ast (NDiscriminationTree.TermSet.elements s) in
+ let g,l =
+ get_cands
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
+ NDiscriminationTree.TermSet.diff
+ NDiscriminationTree.TermSet.empty
+ raw_gty raw_weak_gty in
+ mapf g, mapf l
+ in
+ let global_cands,smart_global_cands =
+ 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
+ uri) | _ -> false)
+ in filter global_cands,filter smart_global_cands
+ in
(* we now compute local candidates *)
let local_cands,smart_local_cands =
- if flags.local_candidates then
let mapf s =
let to_ast t =
let _status, t = term_of_cic_term status t context
(fun ty -> search_in_th ty cache)
Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
mapf g, mapf l
- else [],[] in
+ in
+ let local_cands,smart_local_cands =
+ 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
+ uri) | _ -> false)
+ in filter local_cands,filter smart_local_cands
+ in
(* we now splits candidates in facts or not facts *)
let test = is_a_fact_ast status subst metasenv context in
let by,given_candidates =
flags status tcache signature gty
in
let sm = if is_eq || is_prod then 0 else 2 in
- let sm1 = if flags.last then 2 else 0 in
+ (*let sm1 = if flags.last then 2 else 0 in *)
let maxd = (depth + 1 = flags.maxdepth) in
let try_candidates only_one sm acc candidates =
List.fold_left
NCicMetaSubst.mk_meta
metasenv ctx ~with_type:implication `IsType in
let status = status#set_obj (n,h,metasenv,subst,obj) in
- let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
+ let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in
try
let status = NTactics.intro_tac "foo" status in
let status =
let intro ~depth status facts name =
let status = NTactics.intro_tac name status in
- let _, ctx, ngty = current_goal status in
+ let _, ctx, _ngty = current_goal status 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
let gstatus =
match status#stack with
| [] -> assert false
- | (goals, t, k, tag) :: s ->
+ | (goals, t, k, tag, p) :: s ->
let g = head_goals status#stack in
let sortedg =
(List.rev (MS.topological_sort g (deps status))) in
let sorted_goals =
List.map (fun i -> List.find (is_it i) goals) sortedg
in
- (sorted_goals, t, k, tag) :: s
+ (sorted_goals, t, k, tag, p) :: s
in
status#set_stack gstatus
;;
let gstatus =
match status#stack with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag, p) :: s ->
let is_open = function
| (_,Continuationals.Stack.Open _) -> true
| (_,Continuationals.Stack.Closed _) -> false
in
let g' = List.filter is_open g in
- (g', t, k, tag) :: s
+ (g', t, k, tag, p) :: s
in
status#set_stack gstatus
;;
if level = 0 then [],[],gs else
match gs with
| [] -> assert false
- | (g, t, k, tag) :: s ->
+ | (g, t, k, tag,p) :: s ->
let f,o,gs = slice (level-1) s in
let f1,o1 = List.partition in_focus g
in
- (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
+ (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs
in
let gstatus =
let f,o,s = slice level status#stack in f@o@s
let move_to_side level status =
match status#stack with
| [] -> assert false
- | (g,_,_,_)::tl ->
+ | (g,_,_,_,_)::tl ->
let is_open = function
| (_,Continuationals.Stack.Open i) -> Some i
| (_,Continuationals.Stack.Closed _) -> None
List.for_all (fun i -> IntSet.mem i others)
(HExtlib.filter_map is_open g)
-let top_cache ~depth top status ?(use_given_only=false) cache =
+let top_cache ~depth:_ top status ?(use_given_only=false) cache =
if top then
let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
{cache with unit_eq = unit_eq}
and
(* BRAND NEW VERSION *)
-auto_main flags signature cache depth status ?(use_given_only=false): unit=
+auto_main flags signature cache depth ?(use_given_only=false) status: unit=
debug_print ~depth (lazy "entering auto main");
debug_print ~depth (pptrace status cache.trace);
debug_print ~depth (lazy ("stack length = " ^
match goals with
| [] when depth = 0 -> raise (Proved (status,cache.trace))
| [] ->
- 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 _ = debug_print (pptrace status trace) in
let stack =
match s#stack with
- | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+ | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest
| _ -> assert false
in
let s = s#set_stack stack in
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)
+ 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_lowtac ~params:(univ,flags) status goal =
let gty = get_goalty status goal in
projects / helm.git / blobdiff