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 =
+let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps =
noprint (lazy "indexing equations");
let eq_cache,lemmas =
match lemmas with
eq_cache lemmas
;;
-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 =
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 =
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 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
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
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
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
Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
])
-let auto_lowtac ~params:(univ,flags as params) status goal =
+let auto_lowtac ~params:(univ,flags) status goal =
let gty = get_goalty status goal in
let ctx = ctx_of gty in
let candidates = candidates_from_ctx univ ctx status in
projects / helm.git / blobdiff