| Ast.NCic _ (* local candidate *)
| _ -> ()
+let is_relevant tbl item =
+ try
+ let v = RefHash.find tbl item in
+ if !(v.nominations) < 60 then true (* not enough info *)
+ else if !(v.uses) = 0 then false
+ else true
+ with Not_found -> true
+
let print_stat tbl =
let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
let relevance v = float !(v.uses) /. float !(v.nominations) in
Pervasives.compare (relevance v1) (relevance v2) in
let l = List.sort vcompare l in
let vstring (a,v)=
- CicNotationPp.pp_term (Ast.NRef a) ^ ": rel = " ^
+ CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
(string_of_float (relevance v)) ^
- "; uses = " ^ (string_of_int !(v.uses)) in
- lazy (String.concat "\n" (List.map vstring l))
+ "; uses = " ^ (string_of_int !(v.uses)) ^
+ "; nom = " ^ (string_of_int !(v.nominations)) in
+ lazy ("\n\nSTATISTICS:\n" ^
+ String.concat "\n" (List.map vstring l))
(* ======================= utility functions ========================= *)
module IntSet = Set.Make(struct type t = int let compare = compare end)
| NCic.Rel _
| NCic.Sort _ -> ()
| NCic.Implicit _ -> assert false
- | NCic.Const nref as t ->
+ | NCic.Const nref ->
(*
prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
(f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
;;
-let fast_eq_check eq_cache status goal =
+let fast_eq_check eq_cache status (goal:int) =
match solve NCicParamod.fast_eq_check status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
let s = dist_fast_eq_check eq_cache status in
[s]
with
- | Error _ -> []
+ | Error _ -> debug_print (lazy ("no paramod proof found"));[]
;;
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
let index_local_equations eq_cache status =
debug_print (lazy "indexing equations");
let open_goals = head_goals status#stack in
let open_goal = List.hd open_goals in
let ngty = get_goalty status open_goal in
- let ctx = ctx_of ngty in
+ let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
let c = ref 0 in
List.fold_left
(fun eq_cache _ ->
| NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
when nre<>nref ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
- aux metasenv ty (args@moreargs)
+ aux metasenv bo (args@moreargs)
| NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
when nre<>nref ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
fast_eq_check unit_eq status j
with
+ | NCicEnvironment.ObjectNotFound s as e ->
+ raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
let smart_apply_tac t s =
let all_keys_of_type status t =
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of t in
+ let status, t = apply_subst status context t in
let keys =
all_keys_of_cic_type metasenv subst context
(snd (term_of_cic_term status t context))
(* Here we are dropping the metasenv (in the status), but this should not
raise any exception (hopefully...) *)
let _, ty, _ = saturate ~delta:max_int status orig_ty in
+ let _, ty = apply_subst status (ctx_of ty) ty in
let keys =
(*
let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
| [] -> (* Ncic_termSet.elements *) acc
| (_::tl) as k ->
try
- let idx = List.assq k th in
+ let idx = List.assoc(*q*) k th in
let acc = Ncic_termSet.union acc
(InvRelDiscriminationTree.retrieve_unifiables idx gty)
in
else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
else (* smart = 2: both *)
try NTactics.apply_tac ("",0,t) status
- with Error _ as exc ->
+ with Error _ ->
smart_apply_auto ("",0,t) eq_cache status
in
(*
| None ->
let mapf s =
let to_ast = function
- | NCic.Const r -> Ast.NRef r | _ -> assert false in
- List.map to_ast (NDiscriminationTree.TermSet.elements s) in
+ | 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
| NCic.Prod _ -> true, false
| _ -> false, NCicParamod.is_equation metasenv subst context t
in
- debug_print(lazy (string_of_bool is_eq));
+ debug_print~depth (lazy (string_of_bool is_eq));
+ (* old
let candidates, smart_candidates =
get_candidates ~smart:(not is_eq) depth
- flags status tcache signature gty in
+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates
+ else candidates in *)
+ (* new *)
+ let candidates, smart_candidates =
+ get_candidates ~smart:true depth
+ flags status tcache signature gty in
+ (* if the goal is an equation we avoid to apply unit equalities,
+ since superposition should take care of them; refl is an
+ exception since it prompts for convertibility *)
+ let candidates,smart_candidates =
+ let test x = not (is_a_fact_ast status subst metasenv context x) in
+ if is_eq then
+ Ast.Ident("refl",None) ::List.filter test candidates,
+ List.filter test smart_candidates
+ else candidates,smart_candidates in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
debug_print ~depth
let is_prod status =
let _, ctx, gty = current_goal status in
+ let status, gty = apply_subst status ctx gty in
let _, raw_gty = term_of_cic_term status gty ctx in
match raw_gty with
- | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
- | _ -> None
+ | NCic.Prod (name,src,_) ->
+ let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+ (match snd (term_of_cic_term status src ctx) with
+ | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
+ | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
+ let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
+ (match itys with
+ (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
+ | [_,_,_,[_]]
+ | [_,_,_,[]] -> `Inductive (guess_name name ctx)
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `None
let intro ~depth status facts name =
let status = NTactics.intro_tac name status in
;;
let rec intros_facts ~depth status facts =
+ if List.length (head_goals status#stack) <> 1 then status, facts else
match is_prod status with
- | Some(name) ->
+ | `Inductive name
+ | `Some(name) ->
let status,facts =
intro ~depth status facts name
- in intros_facts ~depth status facts
+ in intros_facts ~depth status facts
+(* | `Inductive name ->
+ let status = NTactics.case1_tac name status in
+ intros_facts ~depth status facts *)
| _ -> status, facts
;;
-let rec intros ~depth status cache =
+let intros ~depth status cache =
match is_prod status with
- | Some _ ->
+ | `Inductive _
+ | `Some _ ->
let trace = cache.trace in
let status,facts =
intros_facts ~depth status cache.facts
in
+ if head_goals status#stack = [] then
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status], cache
+ else
(* we reindex the equation from scratch *)
- let unit_eq =
- index_local_equations status#eq_cache status in
- status, init_cache ~facts ~unit_eq () ~trace
- | _ -> status, cache
+ let unit_eq = index_local_equations status#eq_cache status in
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status],
+ init_cache ~facts ~unit_eq () ~trace
+ | _ -> [],cache
;;
let reduce ~whd ~depth status g =
;;
let do_something signature flags status g depth gty cache =
+ let l0, cache = intros ~depth status cache in
+ if l0 <> [] then l0, cache
+ else
(* whd *)
let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
(* if l <> [] then l,cache else *)
raise (Gaveup IntSet.empty)
else
let status = NTactics.branch_tac ~force:true status in
- let status, cache = intros ~depth status cache in
let g,gctx, gty = current_goal status in
let ctx,ty = close status g in
let closegty = mk_cic_term ctx ty in
debug_print (~depth:depth)
(lazy ("Case: " ^ CicNotationPp.pp_term t));
let depth,cache =
- if t=Ast.Ident("__whd",None) then depth, cache
+ if t=Ast.Ident("__whd",None) ||
+ t=Ast.Ident("__intros",None)
+ then depth, cache
else depth+1,loop_cache in
let cache = add_to_trace ~depth cache t in
try
| _ -> false) trace
;;
-let auto_tac ~params:(univ,flags) status =
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let oldstatus = status in
let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
| _ -> assert false
in
let s = s#set_stack stack in
+ trace_ref := trace;
oldstatus#set_status s
in
let s = up_to depth depth in
projects / helm.git / blobdiff