From 751af6075f28fb2abe052de73630ce114e761dee Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Dec 2010 16:17:52 +0000 Subject: [PATCH] [ porting from CerCo's Matita ] 1. new implementation of normalize to have a speed up in case of fully applicative terms 2. all reduction tactics used to end with instatiate that re-checked the conversion using unification (!!!); added a new flag ?(refine=true) to instantiate to avoid this expensive check when we know it is useless --- matita/components/ng_kernel/nCicReduction.ml | 3 ++- matita/components/ng_kernel/nCicReduction.mli | 1 + .../components/ng_tactics/nCicTacReduction.ml | 23 +++++++++++++++---- matita/components/ng_tactics/nTacStatus.ml | 10 +++++--- matita/components/ng_tactics/nTacStatus.mli | 2 +- matita/components/ng_tactics/nTactics.ml | 2 +- 6 files changed, 31 insertions(+), 10 deletions(-) diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml index 8fc58f4c9..236f5778e 100644 --- a/matita/components/ng_kernel/nCicReduction.ml +++ b/matita/components/ng_kernel/nCicReduction.ml @@ -61,7 +61,7 @@ module CallByValueByNameForUnwind' : Strategy = struct lazy (fst (reduce ~delta:0 c)), (fun delta -> fst (reduce ~delta c)), lazy (unwind c) - let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta + let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta let from_stack_list_for_unwind ~unwind:_ l = List.map (fun (_,_,c) -> Lazy.force c) l let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta @@ -433,6 +433,7 @@ type machine = int * environment_item list * NCic.term * stack_item list let reduce_machine = R.reduce let from_stack = RS.from_stack +let from_env = RS.from_env let unwind = R.unwind let _ = diff --git a/matita/components/ng_kernel/nCicReduction.mli b/matita/components/ng_kernel/nCicReduction.mli index 713edd170..35159fc1c 100644 --- a/matita/components/ng_kernel/nCicReduction.mli +++ b/matita/components/ng_kernel/nCicReduction.mli @@ -44,6 +44,7 @@ val reduce_machine : delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine * bool val from_stack : delta:int -> stack_item -> machine +val from_env : delta:int -> environment_item -> machine val unwind : machine -> NCic.term val split_prods: diff --git a/matita/components/ng_tactics/nCicTacReduction.ml b/matita/components/ng_tactics/nCicTacReduction.ml index 3236956fd..bc756a9ff 100644 --- a/matita/components/ng_tactics/nCicTacReduction.ml +++ b/matita/components/ng_tactics/nCicTacReduction.ml @@ -12,13 +12,28 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) let rec normalize ?(delta=0) ~subst ctx t = - let aux = normalize ~delta ~subst in - match NCicReduction.whd ~delta ~subst ctx t with + normalize_machine ~delta ~subst ctx + (fst (NCicReduction.reduce_machine ~delta ~subst ctx (0,[],t,[]))) +and normalize_machine ?(delta=0) ~subst ctx (k,e,t,s) = + assert (delta=0); + let t = + if k = 0 then t + else + NCicSubstitution.psubst ~avoid_beta_redexes:true + (fun e -> normalize_machine ~delta ~subst ctx (NCicReduction.from_env ~delta e)) e t in + let t = + match t with NCic.Meta (n,(s,lc)) -> let l = NCicUtils.expand_local_context lc in - let l' = List.map (aux ctx) l in + let l' = List.map (normalize ~delta ~subst ctx) l in if l = l' then t else NCic.Meta (n,(s,NCic.Ctx l)) - | t -> NCicUtils.map (fun h ctx -> h::ctx) ctx aux t + | t -> NCicUtils.map (fun h ctx -> h::ctx) ctx (normalize ~delta ~subst) t + in + if s = [] then t + else + NCic.Appl + (t:: + (List.map (fun i -> normalize_machine ~delta ~subst ctx (NCicReduction.from_stack ~delta i)) s)) ;; diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 26e92add4..dd763c327 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -287,11 +287,15 @@ let to_subst status i entry = status#set_obj (name,height,metasenv,subst,obj) ;; -let instantiate status i t = +let instantiate status ?refine:(dorefine=true) 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 - to_subst status i (gname,context,t,ty) + if dorefine then + let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in + to_subst status i (gname,context,t,ty) + else + let status,(_,ty) = typeof status context t in + to_subst status i (gname,context,snd t,ty) ;; let instantiate_with_ast status i t = diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index f9eb1917c..30989faba 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -107,7 +107,7 @@ val mk_meta: #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context -> [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind -> 'status * cic_term -val instantiate: #pstatus as 'status -> int -> cic_term -> 'status +val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status val select_term: diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 9c9f0d73a..577edf9d9 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -371,7 +371,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job = let status, instance = mk_meta status newgoalctx (`Decl newgoalty) `IsTerm in - instantiate status goal instance) + instantiate ~refine:false status goal instance) ;; let select_tac ~where ~job move_down_hyps = -- 2.39.2