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

1 files changed, 20 insertions, 22 deletions

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