From 21ee96d317a4f0e7abfe76f697defe78acc10b94 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Dec 2009 08:41:29 +0000 Subject: [PATCH] Trying to be faster. --- helm/software/components/ng_tactics/nAuto.ml | 2 +- helm/software/components/ng_tactics/nnAuto.ml | 139 ++++++++++++------ .../software/components/ng_tactics/nnAuto.mli | 3 + 3 files changed, 100 insertions(+), 44 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 25f4e0fc7..5c5bb471b 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -41,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal = NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l with | [] -> raise (Error (lazy "no proof found",None)) - | (pt, metasenv, subst)::_ -> + | (pt, _, metasenv, subst)::_ -> let status = status#set_obj (n,h,metasenv,subst,o) in instantiate status goal (mk_cic_term (ctx_of gty) pt) ;; diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index a2a76d4f5..07d08345c 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -14,9 +14,9 @@ open Printf let debug = ref false let debug_print ?(depth=0) s = if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () -let print= debug_print -(* let print ?(depth=0) s = - prerr_endline (String.make depth '\t'^Lazy.force s) *) +(* let print = debug_print *) +let print ?(depth=0) s = + prerr_endline (String.make depth '\t'^Lazy.force s) let debug_do f = if !debug then f () else () @@ -53,7 +53,7 @@ let menv_closure status gl = in closure IntSet.empty gl ;; -(* we call a "fact" an object whose hypothesis occurs in the goal +(* 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 status, ty, _ = saturate ~delta:max_int status ty in @@ -83,7 +83,6 @@ let current_goal status = open_goal, ctx, gty - (* =============================== paramod =========================== *) let auto_paramod ~params:(l,_) status goal = let gty = get_goalty status goal in @@ -103,7 +102,7 @@ let auto_paramod ~params:(l,_) status goal = NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l with | [] -> raise (Error (lazy "no proof found",None)) - | (pt, metasenv, subst)::_ -> + | (pt, _, metasenv, subst)::_ -> let status = status#set_obj (n,h,metasenv,subst,o) in instantiate status goal (mk_cic_term (ctx_of gty) pt) ;; @@ -113,18 +112,26 @@ let auto_paramod_tac ~params status = ;; let fast_eq_check_all status eq_cache goal = - let gty = get_goalty status goal in - let ctx = ctx_of gty in let n,h,metasenv,subst,o = status#obj in - let status,t = term_of_cic_term status gty ctx in - let build_status (pt, metasenv, subst) = - let status = status#set_obj (n,h,metasenv,subst,o) in - let gty = get_goalty status goal in - instantiate status goal (mk_cic_term ctx pt) + let gname, ctx, gty = List.assoc goal metasenv in + let gty = NCicUntrusted.apply_subst subst ctx gty in + let build_status (pt, _, metasenv, subst) = + (* let stamp = Unix.gettimeofday () in *) + let metasenv, subst, pt, pty = + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt (Some gty) + in +(* print (lazy (Printf.sprintf "Refined in %fs" + (Unix.gettimeofday() -. stamp))); *) + let status = status#set_obj (n,h,metasenv,subst,o) in + let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in + let subst = (goal,(gname,ctx,pt,pty)) :: subst in + status#set_obj (n,h,metasenv,subst,o) in List.map build_status (NCicParamod.fast_eq_check status metasenv subst ctx - eq_cache (NCic.Rel ~-1,t)) + eq_cache (NCic.Rel ~-1,gty)) ;; let fast_eq_check eq_cache status goal = @@ -133,19 +140,44 @@ let fast_eq_check eq_cache status goal = | s::_ -> s ;; -let fast_eq_check_tac ~params s = - NTactics.distribute_tac (fast_eq_check s#eq_cache) s +let dist_fast_eq_check eq_cache s = + NTactics.distribute_tac (fast_eq_check eq_cache) s ;; let auto_eq_check eq_cache status = try - let s = - NTactics.distribute_tac (fast_eq_check eq_cache) status in + let s = dist_fast_eq_check eq_cache status in [s] with | Error _ -> [] ;; +(* warning: ctx is supposed to be already instantiated w.r.t subst *) +let index_local_equations eq_cache status = + 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 c = ref 0 in + List.fold_left + (fun eq_cache _ -> + c:= !c+1; + let t = NCic.Rel !c in + try + let ty = NCicTypeChecker.typeof [] [] ctx t in + debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); + NCicParamod.forward_infer_step eq_cache t ty + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> eq_cache) + eq_cache ctx +;; + +let fast_eq_check_tac ~params s = + let unit_eq = index_local_equations s#eq_cache s in + dist_fast_eq_check unit_eq s +;; + (* let fast_eq_check_tac_all ~params eq_cache status = let g,_,_ = current_goal status in @@ -1179,6 +1211,47 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ;; *) +(****************** smart application ********************) + + +let smart_apply t unit_eq status g = + let n,h,metasenv,subst,o = status#obj in + let gname, ctx, gty = List.assoc g metasenv 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 ty = NCicTypeChecker.typeof subst metasenv ctx t in + let ty,metasenv,args = 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 + let eq_coerc = + let uri = + NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in + let ref = NReference.reference_of_spec uri (NReference.Def(2)) in + NCic.Const ref + in + let smart = + NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in + let smart = mk_cic_term ctx smart in + try + let status = instantiate status g smart in + let _,_,metasenv,subst,_ = status#obj in + let _,ctx,jty = List.assoc j metasenv in + let jty = NCicUntrusted.apply_subst subst ctx jty in + debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty))); + fast_eq_check unit_eq status j + with + | Error _ as e -> debug_print (lazy "error"); raise e + +let smart_apply_tac t s = + let unit_eq = index_local_equations s#eq_cache s in + NTactics.distribute_tac (smart_apply t unit_eq) s + +let smart_apply_auto t eq_cache = + NTactics.distribute_tac (smart_apply t eq_cache) + + (****************** types **************) @@ -1322,10 +1395,12 @@ let openg_no status = List.length (head_goals status#stack) let sort_new_elems l = List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l -let try_candidate flags depth status t = +let try_candidate flags depth status eq_cache t = try debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); - let status = NTactics.apply_tac ("",0,t) status in + let status = + smart_apply_auto ("",0,t) eq_cache status in + (* let status = NTactics.apply_tac ("",0,t) status in *) let og_no = openg_no status in if og_no > flags.maxwidth || (depth = flags.maxdepth && og_no <> 0) then @@ -1363,7 +1438,7 @@ let applicative_case depth signature status flags gty (cache:cache) = let elems = List.fold_left (fun elems cand -> - match try_candidate flags depth status cand with + match try_candidate flags depth status cache.unit_eq cand with | None -> elems | Some x -> x::elems) [] candidates @@ -1416,28 +1491,6 @@ let is_subsumed depth status gty cache = with Found -> debug_print ~depth (lazy "success");true) ;; -(* warning: ctx is supposed to be already instantiated w.r.t subst *) -let index_local_equations eq_cache status = - let open_goals = head_goals status#stack in -(* assert (List.length open_goals = 1); *) - let open_goal = List.hd open_goals in - let ngty = get_goalty status open_goal in - let ctx = ctx_of ngty in - let c = ref 0 in - List.fold_left - (fun eq_cache _ -> - c:= !c+1; - let t = NCic.Rel !c in - try - let ty = NCicTypeChecker.typeof [] [] ctx t in - debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); - NCicParamod.forward_infer_step eq_cache t ty - with - | NCicTypeChecker.TypeCheckerFailure _ - | NCicTypeChecker.AssertFailure _ -> eq_cache) - eq_cache ctx -;; - let rec guess_name name ctx = if name = "_" then guess_name "auto" ctx else if not (List.mem_assoc name ctx) then name else diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli index 7a381cbdc..e08d0456d 100644 --- a/helm/software/components/ng_tactics/nnAuto.mli +++ b/helm/software/components/ng_tactics/nnAuto.mli @@ -16,6 +16,9 @@ val fast_eq_check_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic +val smart_apply_tac: + NTacStatus.tactic_term -> 's NTacStatus.tactic + val auto_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic -- 2.39.2