| 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)
(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 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 _ ->
let ty = NCicTypeChecker.typeof [] [] ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
(debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
- debug_print(lazy("riprovo " ^ (ppterm status (mk_cic_term ctx ty))));
NCicParamod.forward_infer_step eq_cache t ty)
else
(debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
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 =
| 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 _, raw_gty = term_of_cic_term status gty ctx in
match raw_gty with
| NCic.Prod (name,src,_) ->
- let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+ 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))
let rec intros_facts ~depth status facts =
if List.length (head_goals status#stack) <> 1 then status, facts else
match is_prod status with
+ | `Inductive name
| `Some(name) ->
let status,facts =
intro ~depth status facts name
- in intros_facts ~depth status facts
- | `Inductive name ->
+ in intros_facts ~depth status facts
+(* | `Inductive name ->
let status = NTactics.case1_tac name status in
- intros_facts ~depth status facts
+ intros_facts ~depth status facts *)
| _ -> status, facts
;;
| _ -> 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