open Printf
-let debug = ref false
let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
-let debug_print ?(depth=0) s =
- if !debug then print ~depth s else ()
-
-let debug_do f = if !debug then f () else ()
+let noprint ?(depth=0) _ = ()
+let debug_print = noprint
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)
(* we call a "fact" an object whose hypothesis occur in the goal
or in types of goal-variables *)
-let is_a_fact status ty =
+let branch status ty =
let status, ty, metas = saturate ~delta:0 status ty in
- debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
+ noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
let g_metas = metas_of_term status ty in
let clos = menv_closure status g_metas in
(* let _,_,metasenv,_,_ = status#obj in *)
| NCic.Meta(i,_) -> IntSet.add i acc
| _ -> assert false)
IntSet.empty metas
- in IntSet.subset menv clos;;
+ in
+ (* IntSet.subset menv clos *)
+ IntSet.cardinal(IntSet.diff menv clos)
+
+let is_a_fact status ty = branch status ty = 0
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
;;
(* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f status eq_cache goal =
+(*
let f =
if fast then NCicParamod.fast_eq_check
else NCicParamod.paramod in
+*)
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc goal metasenv in
let gty = NCicUntrusted.apply_subst subst ctx gty in
with
NCicRefiner.RefineFailure msg
| NCicRefiner.Uncertain msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- snd (Lazy.force msg))); None
+ 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 ->
debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- Lazy.force msg)); None
+ Lazy.force msg ^
+ "\n in the environment\n" ^
+ NCicPp.ppmetasenv subst metasenv)); None
| _ -> None
in
HExtlib.filter_map build_status
;;
let fast_eq_check eq_cache status goal =
- match solve true status eq_cache goal with
+ match solve NCicParamod.fast_eq_check status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
;;
let paramod eq_cache status goal =
- match solve false status eq_cache goal with
+ match solve NCicParamod.paramod status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
NTactics.distribute_tac (paramod unit_eq) s
;;
+let demod eq_cache status goal =
+ match solve NCicParamod.demod status eq_cache goal with
+ | [] -> raise (Error (lazy "no progress",None))
+ | s::_ -> s
+;;
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (demod unit_eq) s
+;;
+
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t None in
let status,t = term_of_cic_term status t ctx in
+ let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
let ty,metasenv,args =
match gty with
NCicMetaSubst.saturate metasenv subst ctx ty 0 in
let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
let status = status#set_obj (n,h,metasenv,subst,o) in
- let pterm = if args=[] then t else NCic.Appl(t::args) in
- debug_print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
- debug_print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
+ let pterm = if args=[] then t else
+ match t with
+ | NCic.Appl l -> NCic.Appl(l@args)
+ | _ -> NCic.Appl(t::args)
+ in
+ noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+ noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
let eq_coerc =
let uri =
NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
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;
type cache =
{facts : th_cache; (* positive results *)
under_inspection : cic_term list * th_cache; (* to prune looping *)
- unit_eq : NCicParamod.state
+ unit_eq : NCicParamod.state;
+ trace: Ast.term list
}
+let add_to_trace ~depth cache t =
+ match t with
+ | 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
+ | Ast.NRef _ ->
+ (match cache.trace with
+ | _::tl -> {cache with trace = tl}
+ | _ -> assert false)
+ | Ast.NCic _ (* local candidate *)
+ | _ -> (*not an application *) cache *)
+
type sort = T | P
type goal = int * sort (* goal, depth, sort *)
type fail = goal * cic_term
exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
atoms of the input goals *)
-exception Proved of NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status * Ast.term list
(* let close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
(* let cache_add_underinspection c _ _ = c;; *)
let init_cache ?(facts=[]) ?(under_inspection=[],[])
- ?(unit_eq=NCicParamod.empty_state) _ =
+ ?(unit_eq=NCicParamod.empty_state)
+ ?(trace=[])
+ _ =
{facts = facts;
under_inspection = under_inspection;
- unit_eq = unit_eq
- }
+ unit_eq = unit_eq;
+ trace = trace}
-let only signature _context candidate =
+let only signature _context candidate = true
+(*
(* TASSI: nel trie ci mettiamo solo il body, non il ty *)
let candidate_ty =
NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
~metasenv:[] candidate ^ ": " ^ string_of_int height));
- rc
+ rc *)
;;
let candidate_no = ref 0;;
let openg_no status = List.length (head_goals status#stack)
+let sort_candidates status ctx candidates =
+ let _,_,metasenv,subst,_ = status#obj in
+ let branch cand =
+ let status,ct = disambiguate status ctx ("",0,cand) None in
+ let status,t = term_of_cic_term status ct ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let res = branch status (mk_cic_term ctx ty) in
+ debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
+ ^ (string_of_int res)));
+ res
+ in
+ let candidates = List.map (fun t -> branch t,t) candidates in
+ let candidates =
+ List.sort (fun (a,_) (b,_) -> a - b) candidates in
+ let candidates = List.map snd candidates in
+ debug_print (lazy ("candidates =\n" ^ (String.concat "\n"
+ (List.map CicNotationPp.pp_term candidates))));
+ candidates
+
let sort_new_elems l =
List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
-let try_candidate ?(smart=0) flags depth status eq_cache t =
+let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
try
debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
let status =
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 _ ->
- smart_apply_auto ("",0,t) eq_cache status in
+ with Error _ as exc ->
+ smart_apply_auto ("",0,t) eq_cache status
+ in
+(*
let og_no = openg_no status in
if (* og_no > flags.maxwidth || *)
((depth + 1) = flags.maxdepth && og_no <> 0) then
(debug_print ~depth (lazy "pruned immediately"); None)
- else
- (incr candidate_no;
- Some ((!candidate_no,t),status))
+ else *)
+ (* useless
+ let status, cict = disambiguate status ctx ("",0,t) None in
+ let status,ct = term_of_cic_term status cict ctx in
+ let _,_,metasenv,subst,_ = status#obj in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
+ let res = branch status (mk_cic_term ctx ty) in
+ if smart=1 && og_no > res then
+ (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
+ ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
+ 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
;;
-let sort_of metasenv ctx t =
- let ty = NCicTypeChecker.typeof [] metasenv ctx t in
- NCicTypeChecker.typeof [] metasenv ctx ty
+let sort_of subst metasenv ctx t =
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let metasenv',ty = NCicUnification.fix_sorts metasenv subst ty in
+ assert (metasenv = metasenv');
+ NCicTypeChecker.typeof subst metasenv ctx ty
;;
let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
;;
-let perforate_small metasenv context t =
+let perforate_small subst metasenv context t =
let rec aux = function
| NCic.Appl (hd::tl) ->
let map t =
- let s = sort_of metasenv context t in
+ let s = sort_of subst metasenv context t in
match s with
| NCic.Sort(NCic.Type [`Type,u])
when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
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 raw_gty = NCicUntrusted.apply_subst subst context raw_gty 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
+ 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 =
+ let together global local =
List.map c_ast
(List.filter (only signature context)
(NDiscriminationTree.TermSet.elements global)) @
List.map t_ast (Ncic_termSet.elements local) in
- let candidates = together cands local_cands in
+ let candidates = together cands local_cands in
+ let candidates = sort_candidates status context candidates in
let smart_candidates =
if smart then
match raw_gty with
- | NCic.Appl _ ->
- let weak_gty = perforate_small metasenv context raw_gty in
+ | NCic.Appl _
+ | NCic.Const _
+ | NCic.Rel _ ->
+ let weak_gty = perforate_small subst metasenv context raw_gty in
(*
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
- together smart_cands smart_local_cands
+ together smart_cands smart_local_cands
+ (* together more_cands more_local_cands *)
| _ -> []
else []
in
- candidates, smart_candidates
-;;
+ let smart_candidates = sort_candidates status context smart_candidates in
+ (* if smart then smart_candidates, []
+ else candidates, [] *)
+ candidates, smart_candidates
+;;
+
+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:cache) =
+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
then (debug_print (lazy "pruned: not a fact"); elems)
else
match try_candidate (~smart:sm)
- flags depth status cache.unit_eq cand with
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] candidates
then (debug_print (lazy "pruned: not a fact"); elems)
else
match try_candidate (~smart:1)
- flags depth status cache.unit_eq cand with
+ flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
[] smart_candidates
| _ -> 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)))));
- l1 @ (sort_new_elems (l @ l2)), cache
+ (* l1 @ (sort_new_elems (l @ l2)), cache *)
+ l1 @ (List.rev l2) @ l, cache
;;
let pp_goal = function
status#set_stack gstatus
;;
-let open_goals level status =
- let rec aux level gs =
- if level = 0 then []
- else match gs with
- | [] -> assert false
- | (g, _, _, _) :: s ->
- let is_open = function
- | (_,Continuationals.Stack.Open i) -> Some i
- | (_,Continuationals.Stack.Closed _) -> None
- in
- HExtlib.filter_map is_open g @ aux (level-1) s
- in
- aux level status#stack
+let rec stack_goals level gs =
+ if level = 0 then []
+ else match gs with
+ | [] -> assert false
+ | (g,_,_,_)::s ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ HExtlib.filter_map is_open g @ stack_goals (level-1) s
;;
+let open_goals level status = stack_goals level status#stack
+;;
+
+let move_to_side level status =
+match status#stack with
+ | [] -> assert false
+ | (g,_,_,_)::tl ->
+ let is_open = function
+ | (_,Continuationals.Stack.Open i) -> Some i
+ | (_,Continuationals.Stack.Closed _) -> None
+ in
+ let others = menv_closure status (stack_goals (level-1) tl) in
+ List.for_all (fun i -> IntSet.mem i others)
+ (HExtlib.filter_map is_open g)
+
let rec auto_clusters ?(top=false)
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
if goals = [] then
- if depth = 0 then raise (Proved status)
+ if depth = 0 then raise (Proved (status, cache.trace))
else
let status = NTactics.merge_tac status in
- auto_clusters flags signature (cache:cache) (depth-1) status
+ 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
else if List.length goals < 2 then
auto_main flags signature cache depth status
else
List.iter
(fun gl ->
if List.length gl > flags.maxwidth then
- (debug_print (lazy "FAIL GLOBAL WIDTH");
+ (debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
raise (Gaveup IntSet.empty))
else ()) classes;
if List.length classes = 1 then
(fun l ->
("cluster:" ^ String.concat "," (List.map string_of_int l)))
classes)));
- let status,b =
+ let status,trace,b =
List.fold_left
- (fun (status,b) gl ->
+ (fun (status,trace,b) gl ->
+ let cache = {cache with trace = trace} in
let flags =
{flags with last = (List.length gl = 1)} in
let lold = List.length status#stack in
String.concat "," (List.map string_of_int gl)));
auto_main flags signature cache depth fstatus; assert false
with
- | Proved(status) ->
+ | Proved(status,trace) ->
let status = NTactics.merge_tac status in
let lnew = List.length status#stack in
assert (lold = lnew);
- (status,true)
- | Gaveup _ when top -> (status,b)
+ (status,trace,true)
+ | Gaveup _ when top -> (status,trace,b)
)
- (status,false) classes
+ (status,cache.trace,false) classes
in
let rec final_merge n s =
if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
in let status = final_merge depth status
- in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
+ in if b then raise (Proved(status,trace)) else raise (Gaveup IntSet.empty)
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 status = sort_tac (clean_up_tac status) in
let goals = head_goals status#stack in
match goals with
- | [] when depth = 0 -> raise (Proved status)
+ | [] 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
- | [] -> assert false
+ | [] -> 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:cache) (depth-1) status
+ auto_clusters flags signature cache (depth-1) status
| 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
+ else
let ng = List.length goals in
(* moved inside auto_clusters *)
if ng > flags.maxwidth then
- (debug_print (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
- else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
+ else if depth = flags.maxdepth then
+ raise (Gaveup IntSet.empty)
else
let status = NTactics.branch_tac ~force:true status in
let status, cache = intros ~depth status cache in
let depth,cache =
if t=Ast.Ident("__whd",None) then depth, cache
else depth+1,loop_cache 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");())
+ debug_print ~depth (lazy "Failed");
+ ())
alternatives;
- raise (Gaveup IntSet.empty)
+ raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
;;
let int name l def =
with Failure _ | Not_found -> def
;;
-let auto_tac ~params:(_univ,flags) status =
+module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
+
+let cleanup_trace s trace =
+ (* removing duplicates *)
+ let trace_set =
+ List.fold_left
+ (fun acc t -> AstSet.add t acc)
+ AstSet.empty trace in
+ let trace = AstSet.elements trace_set
+ (* filtering facts *)
+ in List.filter
+ (fun t ->
+ match t with
+ | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
+ | _ -> false) trace
+;;
+
+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;
*)
with
| Gaveup _ -> up_to (x+1) y
- | Proved s ->
+ | 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 _ = 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
projects / helm.git / blobdiff