From 5752247f917f06eda81a74cb0c8a960df097c9ab Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 2 Jun 2004 17:02:47 +0000
Subject: Fusion comparaison Const/Var; export is_opaque

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5796 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/conv_oracle.ml  | 18 +++++++-----------
 kernel/conv_oracle.mli |  3 +++
 2 files changed, 10 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ffa7735e7..527030fb4 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -19,10 +19,6 @@ let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp
 
 let is_opaque_cst kn = not (KNpred.mem kn !cst_transp)
 
-(* Unfold the first only if it is not opaque and the second is
-   opaque *)
-let const_order kn1 kn2 = is_opaque_cst kn2 & not (is_opaque_cst kn1)
-
 (* Opaque variables *)
 let var_transp = ref Idpred.full
 
@@ -31,14 +27,14 @@ let set_transparent_var kn = var_transp := Idpred.add kn !var_transp
 
 let is_opaque_var kn = not (Idpred.mem kn !var_transp)
 
-let var_order id1 id2 = is_opaque_var id2 & not (is_opaque_var id1)
+(* Opaque reference keys *)
+let is_opaque = function
+  | ConstKey cst -> is_opaque_cst cst
+  | VarKey id -> is_opaque_var id
+  | FarRelKey _ -> false
 
-(* *)
-let oracle_order k1 k2 =
-  match (k1,k2) with
-      (ConstKey kn1, ConstKey kn2) -> const_order kn1 kn2
-    | (VarKey id1, VarKey id2) -> var_order id1 id2
-    | _ -> false
+(* Unfold the first only if it is not opaque and the second is opaque *)
+let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1)
 
 (* summary operations *)
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index da2bbfa23..0eefb8711 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -24,6 +24,9 @@ val set_transparent_const : kernel_name -> unit
 val set_opaque_var      : identifier -> unit
 val set_transparent_var : identifier -> unit
 
+val is_opaque_cst : constant -> bool
+val is_opaque_var : identifier -> bool
+
 (*****************************)
 
 (* transparent state summary operations *)
-- 
cgit v1.2.3