X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hb=ec73d44deba0365d258df455b0bd04ae1764cf76;hp=1d4738d952029f98835a93fbefefe7af21516313;hpb=3dadfa509ace9184e5cf33a46d44c48c6fbed31b;p=helm.git diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 1d4738d95..7a9c20f0f 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -19,8 +19,67 @@ 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 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 + 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.NCic (NCic.Const a)) ^ ": rel = " ^ + (string_of_float (relevance v)) ^ + "; 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) @@ -74,7 +133,7 @@ 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 @@ -117,7 +176,7 @@ let fast_height_of_term t = | 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)); @@ -161,10 +220,12 @@ let height_of_goals status = ;; (* =============================== 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 @@ -193,19 +254,23 @@ let solve fast status eq_cache goal = 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 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) ;; -let fast_eq_check eq_cache status goal = - match solve true status eq_cache goal with +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 ;; @@ -219,16 +284,15 @@ let auto_eq_check eq_cache status = 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 _ -> @@ -254,7 +318,7 @@ let fast_eq_check_tac ~params 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 ;; @@ -264,6 +328,17 @@ let paramod_tac ~params 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 @@ -453,7 +528,7 @@ let saturate_to_ref metasenv subst ctx nref ty = | 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 @@ -468,6 +543,7 @@ let smart_apply t unit_eq status g = (* 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 @@ -478,9 +554,13 @@ let smart_apply t unit_eq status g = 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 @@ -498,6 +578,8 @@ let smart_apply t unit_eq status g = 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 = @@ -513,10 +595,95 @@ let smart_apply_auto t eq_cache = 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 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)) + 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 _, ty = apply_subst status (ctx_of ty) 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 @@ -530,6 +697,16 @@ let keys_of_term status t = 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 -> @@ -608,7 +785,7 @@ let search_in_th gty th = | [] -> (* 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 @@ -621,6 +798,7 @@ let search_in_th gty th = 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; @@ -630,9 +808,31 @@ type flags = { 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 @@ -640,7 +840,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *) 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;; *) @@ -650,11 +850,13 @@ exception Proved of NTacStatus.tac_status (* 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 = true (* @@ -708,7 +910,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = 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 (* @@ -759,6 +961,68 @@ let perforate_small subst metasenv context t = 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 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 + 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 @@ -769,9 +1033,28 @@ let get_candidates ?(smart=true) status cache signature gty = 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 = @@ -792,11 +1075,12 @@ let get_candidates ?(smart=true) status cache signature gty = 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 @@ -809,9 +1093,15 @@ let get_candidates ?(smart=true) status cache signature gty = (* 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 @@ -823,9 +1113,32 @@ let applicative_case depth signature status flags gty (cache:cache) = | 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 + (* 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:(not is_eq) status tcache signature gty in + 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 @@ -927,10 +1240,22 @@ let rec guess_name name ctx = 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 @@ -944,32 +1269,46 @@ let intro ~depth status facts name = ;; 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: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 () - | _ -> 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 ~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 @@ -986,8 +1325,11 @@ let reduce ~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 ~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 = @@ -1000,8 +1342,10 @@ let do_something signature flags status g depth gty cache = 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))))); @@ -1141,11 +1485,12 @@ 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 let cache = @@ -1183,9 +1528,10 @@ let rec auto_clusters ?(top=false) (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 @@ -1197,32 +1543,33 @@ let rec auto_clusters ?(top=false) 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 = @@ -1254,7 +1601,6 @@ auto_main flags signature (cache:cache) depth status: unit = 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 @@ -1282,12 +1628,16 @@ auto_main flags signature (cache:cache) depth status: unit = 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 - 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 (debug_print(lazy "no more candidates"); Gaveup IntSet.empty) ;; @@ -1297,13 +1647,30 @@ 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) ?(trace_ref=ref []) 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 -> @@ -1314,6 +1681,16 @@ let auto_tac ~params:(_univ,flags) status = (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 @@ -1322,6 +1699,7 @@ let auto_tac ~params:(_univ,flags) status = let signature = height_of_goals status in let flags = { last = true; + candidates = candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1347,17 +1725,22 @@ let auto_tac ~params:(_univ,flags) status = *) 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 | _ -> 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 + debug_print (print_stat statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy