pushed evar reduction in kernel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 57 insertions, 39 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index d29f8b08c..10ef06993 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -28,7 +28,8 @@ let iota = ref 0
 let prune = ref 0
 
 let reset () =
-  beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
+  beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0;
+  prune := 0
 
 let stop() =
   msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
@@ -83,7 +84,6 @@ module RedFlags = (struct
     r_delta : bool;
     r_const : transparent_state;
     r_zeta : bool;
-    r_evar : bool;
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
@@ -99,7 +99,6 @@ module RedFlags = (struct
     r_delta = false;
     r_const = all_opaque;
     r_zeta = false;
-    r_evar = false;
     r_iota = false }
 
   let red_add red = function
@@ -201,6 +200,7 @@ type 'a infos = {
   i_flags : reds;
   i_repr : 'a infos -> constr -> 'a;
   i_env : env;
+  i_sigma : existential -> constr option;
   i_rels : int * (int * constr) list;
   i_vars : (identifier * constr) list;
   i_tab : (table_key, 'a) Hashtbl.t }
@@ -227,6 +227,9 @@ let ref_value_cache info ref =
     | NotEvaluableConst _ (* Const *)
       -> None
 
+let evar_value info ev =
+  info.i_sigma ev
+
 let defined_vars flags env =
 (*  if red_local_const (snd flags) then*)
     Sign.fold_named_context 
@@ -259,10 +262,11 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) =
 
 let mind_equiv_infos info = mind_equiv info.i_env
 
-let create mk_cl flgs env =
+let create mk_cl flgs env evars =
   { i_flags = flgs;
     i_repr = mk_cl;
     i_env = env;
+    i_sigma = evars;
     i_rels = defined_rels flgs env;
     i_vars = defined_vars flgs env;
     i_tab = Hashtbl.create 17 }
@@ -314,7 +318,7 @@ and fterm =
   | FLambda of int * (name * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential_key * fconstr array
+  | FEvar of existential * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -581,8 +585,8 @@ let mk_clos_deep clos_fun env t =
     | LetIn (n,b,t,c) ->
         { norm = Red;
 	  term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) }
-    | Evar(ev,args) ->
-	{ norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) }
+    | Evar ev ->
+	{ norm = Red; term = FEvar(ev,env) }
 
 (* A better mk_clos? *)
 let mk_clos2 = mk_clos_deep mk_clos
@@ -632,7 +636,8 @@ let rec to_constr constr_fun lfts v =
 	mkLetIn (n, constr_fun lfts b,
 	            constr_fun lfts t,
 	            constr_fun (el_lift lfts) fc)
-    | FEvar (ev,args) -> mkEvar(ev,Array.map (constr_fun lfts) args)
+    | FEvar ((ev,args),env) ->
+        mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
     | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
     | FCLOS (t,env) ->
         let fr = mk_clos2 env t in
@@ -891,6 +896,10 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
       knit info (subs_cons([|v|],e)) bd stk
+  | FEvar(ev,env) ->
+      (match evar_value info ev with
+          Some c -> knit info env c stk
+        | None -> (m,stk))
   | _ -> (m,stk)
 
 (* Computes the weak head normal form of a term *)
@@ -959,7 +968,8 @@ and norm_head info m =
           let fbds =
             Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
           mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
-      | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args)
+      | FEvar((i,args),env) ->
+          mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
       | t -> term_of_fconstr m
 
 (* Initialization and then normalization *)
@@ -982,7 +992,7 @@ let whd_stack infos m stk =
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
-let create_clos_infos flgs env =
-  create (fun _ -> inject) flgs env
+let create_clos_infos ?(evars=fun _ -> None) flgs env =
+  create (fun _ -> inject) flgs env evars
 
 let unfold_reference = ref_value_cache
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 926e152e0..ede0d6379 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -85,7 +85,9 @@ type table_key = id_key
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
 val info_flags: 'a infos -> reds
-val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
+val create: ('a infos -> constr -> 'a) -> reds -> env ->
+  (existential -> constr option) -> 'a infos
+val evar_value : 'a infos -> existential -> constr option
 
 (************************************************************************)
 (*s Lazy reduction. *)
@@ -111,7 +113,7 @@ type fterm =
   | FLambda of int * (name * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential_key * fconstr array
+  | FEvar of existential * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -156,7 +158,8 @@ val destFLambda :
 
 (* Global and local constant cache *)
 type clos_infos
-val create_clos_infos : reds -> env -> clos_infos
+val create_clos_infos :
+  ?evars:(existential->constr option) -> reds -> env -> clos_infos
 
 (* Reduction function *)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3d2f3e9b9..f1a44b5ca 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -248,10 +248,12 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
 	       then convert_stacks infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
-    | (FEvar (ev1,args1), FEvar (ev2,args2)) ->
+    | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if ev1=ev2 then
           let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
-          convert_vect infos el1 el2 args1 args2 u1
+          convert_vect infos el1 el2
+            (Array.map (mk_clos env1) args1)
+            (Array.map (mk_clos env2) args2) u1
         else raise NotConvertible
 
     (* 2 index known to be bound to no constant *)
@@ -382,29 +384,29 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-let clos_fconv trans cv_pb env t1 t2 =
-  let infos = trans, create_clos_infos betaiotazeta env in
+let clos_fconv trans cv_pb evars env t1 t2 =
+  let infos = trans, create_clos_infos ~evars betaiotazeta env in
   ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
-let trans_fconv reds cv_pb env t1 t2 =
+let trans_fconv reds cv_pb evars env t1 t2 =
   if eq_constr t1 t2 then Constraint.empty
-  else clos_fconv reds cv_pb env t1 t2
+  else clos_fconv reds cv_pb evars env t1 t2
 
-let trans_conv_cmp conv reds = trans_fconv reds conv
-let trans_conv reds = trans_fconv reds CONV
-let trans_conv_leq reds = trans_fconv reds CUMUL
+let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
+let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
+let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
 
 let fconv = trans_fconv (Idpred.full, Cpred.full)
 
-let conv_cmp = fconv
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv_cmp cv_pb = fconv cv_pb (fun _->None)
+let conv ?(evars=fun _->None) = fconv CONV evars
+let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
 
-let conv_leq_vecti env v1 v2 =
+let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
   array_fold_left2_i 
     (fun i c t1 t2 ->
       let c' =
-        try conv_leq env t1 t2 
+        try conv_leq ~evars env t1 t2 
         with NotConvertible -> raise (NotConvertibleVect i) in
       Constraint.union c c')
     Constraint.empty
@@ -413,17 +415,17 @@ let conv_leq_vecti env v1 v2 =
 
 (* option for conversion *)
 
-let vm_conv = ref fconv
+let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 = 
   try 
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb env t1 t2
+      fconv cv_pb (fun _->None) env t1 t2
   
 
-let default_conv = ref fconv 
+let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 
 let set_default_conv f = default_conv := f
 
@@ -432,7 +434,7 @@ let default_conv cv_pb env t1 t2 =
     !default_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb env t1 t2
+      fconv cv_pb (fun _->None) env t1 t2
   
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ac1591bb..de926bd1d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -40,15 +40,18 @@ val conv_sort      : sorts conversion_function
 val conv_sort_leq  : sorts conversion_function
 
 val trans_conv_cmp       : conv_pb -> constr trans_conversion_function
-
-val trans_conv           : constr trans_conversion_function
-val trans_conv_leq       : types trans_conversion_function
+val trans_conv           :
+  ?evars:(existential->constr option) -> constr trans_conversion_function
+val trans_conv_leq       :
+  ?evars:(existential->constr option) -> types trans_conversion_function
 
 val conv_cmp       : conv_pb -> constr conversion_function
-
-val conv           : constr conversion_function
-val conv_leq       : types conversion_function
-val conv_leq_vecti : types array conversion_function
+val conv           :
+  ?evars:(existential->constr option) -> constr conversion_function
+val conv_leq       :
+  ?evars:(existential->constr option) -> types conversion_function
+val conv_leq_vecti :
+  ?evars:(existential->constr option) -> types array conversion_function
 
 (* option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit