From 6ec8ad120e5b2dd2f054cbdf83845453a7be7bcc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Oct 2009 09:23:57 +0000 Subject: [PATCH] Smarter implementation of instantiate to avoid re-checking twice the same term. --- helm/software/components/ng_tactics/nAuto.ml | 2 +- .../components/ng_tactics/nTacStatus.ml | 30 ++++++++++++------- .../components/ng_tactics/nTacStatus.mli | 3 +- .../components/ng_tactics/nTactics.ml | 19 +++++------- 4 files changed, 29 insertions(+), 25 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index a80334d01..d3409bcbe 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -28,7 +28,7 @@ let auto_paramod ~params:(l,_) status goal = let status, l = List.fold_left (fun (status, l) t -> - let status, t = disambiguate status t None (ctx_of gty) in + let status, t = disambiguate status (ctx_of gty) t None in let status, ty = typeof status (ctx_of t) t in let status, t = term_of_cic_term status t (ctx_of gty) in let status, ty = term_of_cic_term status ty (ctx_of ty) in diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index f51f4d2d7..462501e66 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -49,6 +49,7 @@ let pp_status status = type cic_term = NCic.context * NCic.term let ctx_of (c,_) = c ;; +let mk_cic_term c t = c,t ;; let ppterm status t = let uri,height,metasenv,subst,obj = status#obj in @@ -138,7 +139,7 @@ let term_of_cic_term s t c = s, t ;; -let disambiguate status t ty context = +let disambiguate status context t ty = let status, expty = match ty with | None -> status, None @@ -225,17 +226,26 @@ let get_goalty status g = with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_goalty") ;; +let to_subst status i entry = + let name,height,metasenv,subst,obj = status#obj in + let metasenv = List.filter (fun j,_ -> j <> i) metasenv in + let subst = (i, entry) :: subst in + status#set_obj (name,height,metasenv,subst,obj) +;; + let instantiate status i t = let _,_,metasenv,_,_ = status#obj in let gname, context, gty = List.assoc i metasenv in - let status, (_,t), (_,ty) = - refine status context t (Some (context,gty)) - in + let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in + to_subst status i (gname,context,t,ty) +;; - let name,height,metasenv,subst,obj = status#obj in - let metasenv = List.filter (fun j,_ -> j <> i) metasenv in - let subst = (i, (gname, context, t, ty)) :: subst in - status#set_obj (name,height,metasenv,subst,obj) +let instantiate_with_ast status i t = + let _,_,metasenv,_,_ = status#obj in + let gname, context, gty = List.assoc i metasenv in + let ggty = mk_cic_term context gty in + let status, (_,t) = disambiguate status context t (Some ggty) in + to_subst status i (gname,context,t,gty) ;; let mk_meta status ?(attrs=[]) ctx bo_or_ty = @@ -356,7 +366,7 @@ let select_term | NCic.Implicit `Hole, t -> (match wanted with | Some wanted -> - let status', wanted = disambiguate status wanted None ctx in + let status', wanted = disambiguate status ctx wanted None in pp(lazy("wanted: "^ppterm status' wanted)); let (status',found), t' = match_term status' ctx wanted t in if found then status',t' else status,t @@ -391,8 +401,6 @@ let analyse_indty status ty = status, (ref, consno, left, right) ;; -let mk_cic_term c t = c,t ;; - let apply_subst status ctx t = let status, (_,t) = relocate status ctx t in let _,_,_,subst,_ = status#obj in diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index c7e3ea75e..fdad9f861 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -32,7 +32,7 @@ val term_of_cic_term : val mk_cic_term : NCic.context -> NCic.term -> cic_term val disambiguate: - #pstatus as 'status -> tactic_term -> cic_term option -> NCic.context -> + #pstatus as 'status -> NCic.context -> tactic_term -> cic_term option -> 'status * cic_term (* * cic_term XXX *) val analyse_indty: @@ -65,6 +65,7 @@ val mk_meta: [ `Decl of cic_term | `Def of cic_term ] -> 'status * cic_term val instantiate: #pstatus as 'status -> int -> cic_term -> 'status +val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status val select_term: #pstatus as 'status -> diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index a9b95339f..9834cce8a 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -277,9 +277,7 @@ let first_tac tacl status = ;; let exact_tac t : 's tactic = distribute_tac (fun status goal -> - let goalty = get_goalty status goal in - let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in - instantiate status goal t) + instantiate_with_ast status goal t) ;; let assumption_tac status = distribute_tac (fun status goal -> @@ -407,7 +405,7 @@ let generalize_tac ~where = _,_,(None,_,_) -> fail (lazy "No term to generalize") | txt,txtlen,(Some what,_,_) -> let status, what = - disambiguate status (txt,txtlen,what) None (ctx_of goalty) + disambiguate status (ctx_of goalty) (txt,txtlen,what) None in status,what,[] ) @@ -416,7 +414,6 @@ let generalize_tac ~where = List.fold_left (fun s t -> unify s (ctx_of goalty) canon t) status rest in let status, canon = term_of_cic_term status canon (ctx_of goalty) in - (* XXX embedding AST *) instantiate status goal (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) ) s) ] @@ -451,7 +448,7 @@ let reduce_tac ~reduction ~where = let change_tac ~where ~with_what = let change status t = - let status, ww = disambiguate status with_what None (ctx_of t) in + let status, ww = disambiguate status (ctx_of t) with_what None in let status = unify status (ctx_of t) t ww in status, ww in @@ -485,7 +482,7 @@ type indtyinfo = { let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal -> let goalty = get_goalty status goal in - let status, what = disambiguate status what None (ctx_of goalty) in + let status, what = disambiguate status (ctx_of goalty) what None in let status, ty_what = typeof status (ctx_of what) what in let status, (r,consno,lefts,rights) = analyse_indty status ty_what in let leftno = List.length lefts in @@ -559,7 +556,7 @@ let intro_tac name = let cases ~what status goal = let gty = get_goalty status goal in - let status, what = disambiguate status what None (ctx_of gty) in + let status, what = disambiguate status (ctx_of gty) what None in let status, ty = typeof status (ctx_of what) what in let status, (ref, consno, _, _) = analyse_indty status ty in let status, what = term_of_cic_term status what (ctx_of gty) in @@ -567,9 +564,7 @@ let cases ~what status goal = NCic.Match (ref,NCic.Implicit `Term, what, HExtlib.mk_list (NCic.Implicit `Term) consno) in - let ctx = ctx_of gty in - let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in - instantiate status goal t + instantiate status goal (mk_cic_term (ctx_of gty) t) ;; let cases_tac ~what:(txt,len,what) ~where = @@ -610,7 +605,7 @@ let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);; let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let gty = get_goalty status goal in let eq status ctx t1 t2 = - let status,t1 = disambiguate status t1 None ctx in + let status,t1 = disambiguate status ctx t1 None in let status,t1 = apply_subst status ctx t1 in let status,t1 = term_of_cic_term status t1 ctx in let t2 = mk_cic_term ctx t2 in -- 2.39.2