Conv_orable made functional and part of pre_env

But for vm, the kernel should be functional now

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

13 files changed, 49 insertions, 35 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index db57503f6..187ea4478 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1007,5 +1007,6 @@ type clos_infos = fconstr infos
 
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
   create (fun _ -> inject) flgs env evars
+let oracle_of_infos { i_env } = Environ.oracle i_env
 
 let unfold_reference = ref_value_cache
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 3a9603a37..161de91cf 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -163,6 +163,7 @@ val destFLambda :
 type clos_infos
 val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
+val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
 (** Reduction function *)
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 65efb4fd0..32aaacb62 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -26,48 +26,46 @@ let is_transparent = function
 | Level 0 -> true
 | _ -> false
 
-type oracle = level Id.Map.t * level Cmap.t
+type oracle = {
+  var_opacity : level Id.Map.t;
+  cst_opacity : level Cmap.t
+}
 
-let var_opacity = ref Id.Map.empty
-let cst_opacity = ref Cmap.empty
+let empty = { var_opacity = Id.Map.empty; cst_opacity = Cmap.empty }
 
-(* summary operations *)
-let freeze _ = (!var_opacity, !cst_opacity)
-let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
-
-let get_strategy = function
+let get_strategy { var_opacity; cst_opacity } = function
   | VarKey id ->
-      (try Id.Map.find id !var_opacity
+      (try Id.Map.find id var_opacity
       with Not_found -> default)
   | ConstKey c ->
-      (try Cmap.find c !cst_opacity
+      (try Cmap.find c cst_opacity
       with Not_found -> default)
   | RelKey _ -> Expand
 
-let set_strategy k l =
+let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
   match k with
   | VarKey id ->
-      var_opacity :=
-      if is_default l then Id.Map.remove id !var_opacity
-      else Id.Map.add id l !var_opacity
+      { oracle with var_opacity =
+          if is_default l then Id.Map.remove id var_opacity
+          else Id.Map.add id l var_opacity }
   | ConstKey c ->
-      cst_opacity :=
-      if is_default l then Cmap.remove c !cst_opacity
-      else Cmap.add c l !cst_opacity
+      { oracle with cst_opacity =
+          if is_default l then Cmap.remove c cst_opacity
+          else Cmap.add c l cst_opacity }
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
-let get_transp_state () =
+let get_transp_state { var_opacity; cst_opacity } =
   (Id.Map.fold
     (fun id l ts -> if  l=Opaque then Id.Pred.remove id ts else ts)
-    !var_opacity Id.Pred.full,
+    var_opacity Id.Pred.full,
    Cmap.fold
     (fun c l ts -> if  l=Opaque then Cpred.remove c ts else ts)
-    !cst_opacity Cpred.full)
+    cst_opacity Cpred.full)
 
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, expand the second one. *)
-let oracle_order l2r k1 k2 =
-  match get_strategy k1, get_strategy k2 with
+let oracle_order o l2r k1 k2 =
+  match get_strategy o k1, get_strategy o k2 with
     | Expand, _ -> true
     | Level n1, Opaque -> true
     | Level n1, Level n2 -> n1 < n2
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 7bb62112c..24797238d 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -8,11 +8,15 @@
 
 open Names
 
+type oracle
+
+val empty : oracle
+
 (** Order on section paths for unfolding.
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
+val oracle_order : oracle -> bool -> 'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
  * Higher levels means that the expansion is less prioritary.
@@ -25,16 +29,11 @@ val transparent : level
 (** Check whether a level is transparent *)
 val is_transparent : level -> bool
 
-val get_strategy : 'a tableKey -> level
+val get_strategy : oracle -> 'a tableKey -> level
 
 (** Sets the level of a constant.
  * Level of RelKey constant cannot be set. *)
-val set_strategy : 'a tableKey -> level -> unit
+val set_strategy : oracle -> 'a tableKey -> level -> oracle
 
-val get_transp_state : unit -> transparent_state
+val get_transp_state : oracle -> transparent_state
 
-(****************************
-   Summary operations *)
-type oracle
-val freeze   : [ `Yes | `No | `Shallow ] -> oracle
-val unfreeze : oracle -> unit
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ae6817a76..9f1868004 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -38,6 +38,8 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
+let oracle env = env.env_conv_oracle
+let set_oracle env o = { env with env_conv_oracle = o }
 
 let empty_named_context_val = empty_named_context_val
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d378501a0..38a1bf68a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -32,6 +32,8 @@ open Declarations
 type env
 val pre_env : env -> Pre_env.env
 val env_of_pre_env : Pre_env.env -> env
+val oracle : env -> Conv_oracle.oracle
+val set_oracle : env -> Conv_oracle.oracle -> env
 
 type named_context_val
 val eq_named_context_val : named_context_val -> named_context_val -> bool
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index cbc147e9e..7d318add5 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,13 +15,13 @@ Nativevalues
 Lazyconstr
 Declareops
 Retroknowledge
+Conv_oracle
 Pre_env
 Cbytegen
 Nativelambda
 Nativecode
 Nativelib
 Environ
-Conv_oracle
 Closure
 Reduction
 Nativeconv
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 9a2bb73d1..e543c4e68 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -54,6 +54,7 @@ type env = {
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification;
+  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
@@ -74,6 +75,7 @@ let empty_env = {
   env_stratification = {
     env_universes = initial_universes;
     env_engagement = None };
+  env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge }
 
 
@@ -118,6 +120,7 @@ let push_named d env =
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
     env_stratification = env.env_stratification;
+    env_conv_oracle = env.env_conv_oracle;
     retroknowledge = env.retroknowledge; }
 
 let lookup_named_val id env =
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 10c9c27cb..f634719f9 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -46,6 +46,7 @@ type env = {
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
+    env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 48c63ac96..194b223bb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -299,7 +299,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
-            if Conv_oracle.oracle_order l2r fl1 fl2 then
+            if Conv_oracle.oracle_order (Closure.oracle_of_infos (snd infos)) l2r fl1 fl2 then
               match unfold_reference infos fl1 with
                 | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
                 | None ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 40f16a6e6..3132d45e3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -777,3 +777,7 @@ environment, and store for the future (instead of just its type)
 loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
+
+let set_strategy e k l = { e with env =
+   (Environ.set_oracle e.env
+      (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b16d5b63d..dcdb866bf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -155,3 +155,6 @@ val register :
   field -> Retroknowledge.entry -> Term.constr -> safe_transformer0
 
 val register_inline : constant -> safe_transformer0
+
+val set_strategy :
+  safe_environment -> 'a Names.tableKey -> Conv_oracle.level -> safe_environment
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 7044b1372..4273596d9 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -99,7 +99,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
 	    conv_stack k stk1 stk2 cu
 	  else raise NotConvertible
 	with NotConvertible ->
-	  if oracle_order false ik1 ik2 then
+	  if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
             conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
           else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
@@ -219,10 +219,10 @@ and conv_eq_vect vt1 vt2 cu =
   else raise NotConvertible
 
 let vconv pb env t1 t2 =
+  infos := create_clos_infos betaiotazeta env;
   let cu =
     try conv_eq pb t1 t2 empty_constraint
     with NotConvertible ->
-      infos := create_clos_infos betaiotazeta env;
       let v1 = val_of_constr env t1 in
       let v2 = val_of_constr env t2 in
       let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in