open Continuationals.Stack
open NTacStatus
module Ast = CicNotationPt
+
+(* ======================= statistics ========================= *)
+
let app_counter = ref 0
+module RHT = struct
+ type t = NReference.reference
+ let equal = (==)
+ let compare = Pervasives.compare
+ let hash = Hashtbl.hash
+end;;
+
+module RefHash = Hashtbl.Make(RHT);;
+
+type info = {
+ nominations : int ref;
+ uses: int ref;
+}
+
+let statistics: info RefHash.t = RefHash.create 503
+
+let incr_nominations tbl item =
+ try
+ let v = RefHash.find tbl item in incr v.nominations
+ with Not_found ->
+ RefHash.add tbl item {nominations = ref 1; uses = ref 0}
+
+let incr_uses tbl item =
+ try
+ let v = RefHash.find tbl item in incr v.uses
+ with Not_found -> assert false
+
+let toref f tbl t =
+ match t with
+ | Ast.NRef n ->
+ f tbl n
+ | Ast.NCic _ (* local candidate *)
+ | _ -> ()
+
+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
+ let vcompare (_,v1) (_,v2) =
+ 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 = " ^
+ (string_of_float (relevance v)) ^
+ "; uses = " ^ (string_of_int !(v.uses)) in
+ lazy (String.concat "\n" (List.map vstring l))
+
(* ======================= utility functions ========================= *)
module IntSet = Set.Make(struct type t = int let compare = compare end)
let is_a_fact_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
match obj with
- | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
+ | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
is_a_fact s (mk_cic_term [] ty)
(* aggiungere i costruttori *)
| _ -> false
with
NCicRefiner.RefineFailure msg
| NCicRefiner.Uncertain msg ->
- print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
snd (Lazy.force msg) ^
"\n in the environment\n" ^
NCicPp.ppmetasenv subst metasenv)); None
| NCicRefiner.AssertFailure msg ->
- print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
Lazy.force msg ^
"\n in the environment\n" ^
NCicPp.ppmetasenv subst metasenv)); None
type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
-let keys_of_term status t =
- let status, orig_ty = typeof status (ctx_of t) t in
+(* cartesian: term set list -> term list set *)
+let rec cartesian =
+ function
+ [] -> NDiscriminationTree.TermListSet.empty
+ | [l] ->
+ NDiscriminationTree.TermSet.fold
+ (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
+ | he::tl ->
+ let rest = cartesian tl in
+ NDiscriminationTree.TermSet.fold
+ (fun x acc ->
+ NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
+ ) he NDiscriminationTree.TermListSet.empty
+;;
+
+(* all_keys_of_cic_type: term -> term set *)
+let all_keys_of_cic_type metasenv subst context ty =
+ let saturate ty =
+ (* Here we are dropping the metasenv, but this should not raise any
+ exception (hopefully...) *)
+ let ty,_,hyps =
+ NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
+ in
+ ty,List.length hyps
+ in
+ let rec aux ty =
+ match ty with
+ NCic.Appl (he::tl) ->
+ let tl' =
+ List.map (fun ty ->
+ let wty = NCicReduction.whd ~delta:0 ~subst context ty in
+ if ty = wty then
+ NDiscriminationTree.TermSet.add ty (aux ty)
+ else
+ NDiscriminationTree.TermSet.union
+ (NDiscriminationTree.TermSet.add ty (aux ty))
+ (NDiscriminationTree.TermSet.add wty (aux wty))
+ ) tl
+ in
+ NDiscriminationTree.TermListSet.fold
+ (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
+ (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
+ NDiscriminationTree.TermSet.empty
+ | _ -> NDiscriminationTree.TermSet.empty
+ in
+ let ty,ity = saturate ty in
+ let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in
+ if ty = wty then
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
+ else
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
+ iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
+;;
+
+let all_keys_of_type status t =
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of t in
+ let keys =
+ all_keys_of_cic_type metasenv subst context
+ (snd (term_of_cic_term status t context))
+ in
+ status,
+ List.map
+ (fun (intros,keys) ->
+ intros,
+ NDiscriminationTree.TermSet.fold
+ (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
+ keys Ncic_termSet.empty
+ ) keys
+;;
+
+
+let keys_of_type status orig_ty =
+ (* 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 keys = [ty] in
+ let keys =
+(*
+ let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
+ if orig_ty' <> orig_ty then
+ let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
+ [ty;ty']
+ else
+ [ty]
+*)
+ [ty] in
+(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
let keys =
let _, ty = term_of_cic_term status ty (ctx_of ty) in
match ty with
status, keys
;;
+let all_keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ all_keys_of_type status orig_ty
+;;
+
+let keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ keys_of_type status orig_ty
+;;
+
let mk_th_cache status gl =
List.fold_left
(fun (status, acc) g ->
type flags = {
do_types : bool; (* solve goals in Type *)
last : bool; (* last goal: take first solution only *)
+ candidates: Ast.term list option;
maxwidth : int;
maxsize : int;
maxdepth : int;
trace: Ast.term list
}
-let add_to_trace cache t =
+let add_to_trace ~depth cache t =
match t with
- | Ast.NRef _ -> {cache with trace = t::cache.trace}
+ | Ast.NRef _ ->
+ debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t));
+ {cache with trace = t::cache.trace}
| Ast.NCic _ (* local candidate *)
| _ -> (*not an application *) cache
+let pptrace tr =
+ (lazy ("Proof Trace: " ^ (String.concat ";"
+ (List.map CicNotationPp.pp_term tr))))
(* not used
let remove_from_trace cache t =
match t with
aux t
;;
+let get_cands retrieve_for diff empty gty weak_gty =
+ let cands = retrieve_for gty in
+ match weak_gty with
+ | None -> cands, empty
+ | Some weak_gty ->
+ let more_cands = retrieve_for weak_gty in
+ cands, diff more_cands cands
+;;
+
+let get_candidates ?(smart=true) depth flags status cache signature gty =
+ let maxd = ((depth + 1) = flags.maxdepth) 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 raw_weak_gty, weak_gty =
+ if smart then
+ match raw_gty with
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak = perforate_small subst metasenv context raw_gty in
+ Some weak, Some (mk_cic_term context weak)
+ | _ -> None,None
+ else None,None
+ in
+ let global_cands, smart_global_cands =
+ match flags.candidates with
+ | Some l when (not maxd) -> l,[]
+ | Some _
+ | 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
+ 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 local_cands,smart_local_cands =
+ let mapf s =
+ let to_ast t =
+ let _status, t = term_of_cic_term status t context
+ in Ast.NCic t in
+ List.map to_ast (Ncic_termSet.elements s) in
+ let g,l =
+ get_cands
+ (fun ty -> search_in_th ty cache)
+ Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
+ mapf g, mapf l in
+ sort_candidates status context (global_cands@local_cands),
+ sort_candidates status context (smart_global_cands@smart_local_cands)
+;;
+
+(* old version
let get_candidates ?(smart=true) status cache signature gty =
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let c_ast = function
| NCic.Const r -> Ast.NRef r | _ -> assert false in
let _, raw_gty = term_of_cic_term status gty context in
+ let keys = all_keys_of_cic_term metasenv subst context raw_gty in
+ (* we only keep those keys that do not require any intros for now *)
+ let no_intros_keys = snd (List.hd keys) in
+ let cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ NDiscriminationTree.TermSet.union acc
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe ty)
+ ) no_intros_keys NDiscriminationTree.TermSet.empty in
+(* old code:
let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
universe raw_gty in
+*)
+ let local_cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
+ ) no_intros_keys Ncic_termSet.empty in
+(* old code:
let local_cands = search_in_th gty cache in
+*)
debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
let together global local =
NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
(List.length tl)) in *)
let more_cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe weak_gty in
+ NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe weak_gty
+ in
let smart_cands =
NDiscriminationTree.TermSet.diff more_cands cands in
- let cic_weak_gty = mk_cic_term context weak_gty in
+ let cic_weak_gty = mk_cic_term context weak_gty in
let more_local_cands = search_in_th cic_weak_gty cache in
let smart_local_cands =
Ncic_termSet.diff more_local_cands local_cands in
(* if smart then smart_candidates, []
else candidates, [] *)
candidates, smart_candidates
-;;
+;;
-let applicative_case depth signature status flags gty (cache:cache) =
+let get_candidates ?(smart=true) flags status cache signature gty =
+ match flags.candidates with
+ | None -> get_candidates ~smart status cache signature gty
+ | Some l -> l,[]
+;; *)
+
+let applicative_case depth signature status flags gty cache =
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
in
debug_print(lazy (string_of_bool is_eq));
let candidates, smart_candidates =
- get_candidates ~smart:(not is_eq) status tcache signature gty in
+ get_candidates ~smart:(not is_eq) depth
+ flags status tcache signature gty in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
debug_print ~depth
| _ -> status, facts
;;
-let rec intros ~depth status (cache:cache) =
+let rec intros ~depth status cache =
match is_prod status with
| Some _ ->
+ let trace = cache.trace in
let status,facts =
intros_facts ~depth status cache.facts
in
(* we reindex the equation from scratch *)
let unit_eq =
index_local_equations status#eq_cache status in
- status, init_cache ~facts ~unit_eq ()
+ status, init_cache ~facts ~unit_eq () ~trace
| _ -> status, cache
;;
-let reduce ~depth status g =
+let reduce ~whd ~depth status g =
let n,h,metasenv,subst,o = status#obj in
let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
let ty = NCicUntrusted.apply_subst subst ctx ty in
- let ty' = NCicReduction.whd ~subst ctx ty in
+ let ty' =
+ (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty
+ in
if ty = ty' then []
else
(debug_print ~depth
let do_something signature flags status g depth gty cache =
(* whd *)
- let l = reduce ~depth status g in
+ let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
(* if l <> [] then l,cache else *)
(* backward aplications *)
let l1 =
let l2 =
if ((l1 <> []) && flags.last) then [] else
applicative_case depth signature status flags gty cache
- (* fast paramodulation *)
in
+ (* statistics *)
+ List.iter
+ (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
(* states in l1 have have an empty set of subgoals: no point to sort them *)
debug_print ~depth
(lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
flags signature cache depth status : unit =
debug_print ~depth (lazy ("entering auto clusters at depth " ^
(string_of_int depth)));
+ debug_print ~depth (pptrace cache.trace);
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
and
(* BRAND NEW VERSION *)
-auto_main flags signature (cache:cache) depth status: unit =
+auto_main flags signature cache depth status: unit =
debug_print ~depth (lazy "entering auto main");
+ debug_print ~depth (pptrace cache.trace);
debug_print ~depth (lazy ("stack length = " ^
(string_of_int (List.length status#stack))));
(* ignore(Unix.select [] [] [] 0.01); *)
let depth,cache =
if t=Ast.Ident("__whd",None) then depth, cache
else depth+1,loop_cache in
- let cache = add_to_trace cache t in
+ let cache = add_to_trace ~depth cache t in
try
- auto_clusters flags signature (cache:cache) depth status
+ auto_clusters flags signature cache depth status
with Gaveup _ ->
debug_print ~depth (lazy "Failed");
())
| _ -> false) trace
;;
-let auto_tac ~params:(_univ,flags) status =
+let auto_tac ~params:(univ,flags) status =
let oldstatus = status in
let status = (status:> NTacStatus.tac_status) in
let goals = head_goals status#stack in
let status, facts = mk_th_cache status goals in
let unit_eq = index_local_equations status#eq_cache status in
- let cache = init_cache ~facts ~unit_eq () in
+ let cache = init_cache ~facts ~unit_eq () in
(* pp_th status facts; *)
(*
NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
(NDiscriminationTree.TermSet.elements t))
)));
*)
+ let candidates =
+ match univ with
+ | None -> None
+ | Some l ->
+ let to_Ast t =
+ let status, res = disambiguate status [] t None in
+ let _,res = term_of_cic_term status res (ctx_of res)
+ in Ast.NCic res
+ in Some (List.map to_Ast l)
+ in
let depth = int "depth" flags 3 in
let size = int "size" flags 10 in
let width = int "width" flags 4 (* (3+List.length goals)*) in
let signature = height_of_goals status in
let flags = {
last = true;
+ candidates = candidates;
maxwidth = width;
maxsize = size;
maxdepth = depth;
| Gaveup _ -> up_to (x+1) y
| Proved (s,trace) ->
debug_print (lazy ("proved at depth " ^ string_of_int x));
+ List.iter (toref incr_uses statistics) trace;
let trace = cleanup_trace s trace in
- let _ = print (lazy
- ("Proof Trace: " ^ (String.concat ";"
- (List.map CicNotationPp.pp_term trace)))) in
+ let _ = debug_print (pptrace trace) in
let stack =
match s#stack with
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
oldstatus#set_status s
in
let s = up_to depth depth in
+ debug_print (print_stat statistics);
debug_print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
debug_print(lazy