From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 2 Dec 2010 16:17:52 +0000 (+0000)
Subject: [ porting from CerCo's Matita ]
X-Git-Tag: make_still_working~2668
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=751af6075f28fb2abe052de73630ce114e761dee;p=helm.git

[ 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
---

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 =