aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-21 23:26:23 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-21 23:26:23 +0000
commit85a223796514d98211c06593d7ec72e56ed21e33 (patch)
treeed71c16392b6b738787303df93f92d01091d4feb /kernel
parent82b959a8f6025f84a39efb67985e6fe1a338b94b (diff)
refined the conversion oracle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/conv_oracle.ml76
-rw-r--r--kernel/conv_oracle.mli29
2 files changed, 72 insertions, 33 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index d0f5cf63e..58668c014 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -10,33 +10,67 @@
open Names
-(* Opaque constants *)
-let cst_transp = ref Cpred.full
+(* Priority for the expansion of constant in the conversion test.
+ * Higher levels means that the expansion is less prioritary.
+ * (And Expand stands for -oo, and Opaque +oo.)
+ * The default value is [Level 100].
+ *)
+type level = Expand | Level of int | Opaque
+let default = Level 0
+let transparent = default
-let set_opaque_const kn = cst_transp := Cpred.remove kn !cst_transp
-let set_transparent_const kn = cst_transp := Cpred.add kn !cst_transp
+type oracle = level Idmap.t * level Cmap.t
-let is_opaque_cst kn = not (Cpred.mem kn !cst_transp)
+let var_opacity = ref Idmap.empty
+let cst_opacity = ref Cmap.empty
-(* Opaque variables *)
-let var_transp = ref Idpred.full
+let get_strategy = function
+ | VarKey id ->
+ (try Idmap.find id !var_opacity
+ with Not_found -> default)
+ | ConstKey c ->
+ (try Cmap.find c !cst_opacity
+ with Not_found -> default)
+ | RelKey _ -> Expand
-let set_opaque_var kn = var_transp := Idpred.remove kn !var_transp
-let set_transparent_var kn = var_transp := Idpred.add kn !var_transp
+let set_strategy k l =
+ match k with
+ | VarKey id ->
+ var_opacity :=
+ if l=default then Idmap.remove id !var_opacity
+ else Idmap.add id l !var_opacity
+ | ConstKey c ->
+ cst_opacity :=
+ if l=default then Cmap.remove c !cst_opacity
+ else Cmap.add c l !cst_opacity
+ | RelKey _ -> Util.error "set_strategy: RelKey"
-let is_opaque_var kn = not (Idpred.mem kn !var_transp)
+let set_transparent_const kn =
+ cst_opacity := Cmap.remove kn !cst_opacity
+let set_transparent_var id =
+ var_opacity := Idmap.remove id !var_opacity
-(* Opaque reference keys *)
-let is_opaque = function
- | ConstKey cst -> is_opaque_cst cst
- | VarKey id -> is_opaque_var id
- | RelKey _ -> false
+let set_opaque_const kn = set_strategy (ConstKey kn) Opaque
+let set_opaque_var id = set_strategy (VarKey id) Opaque
-(* 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)
+let get_transp_state () =
+ (Idmap.fold
+ (fun id l ts -> if l=Opaque then Idpred.remove id ts else ts)
+ !var_opacity Idpred.full,
+ Cmap.fold
+ (fun c l ts -> if l=Opaque then Cpred.remove c ts else ts)
+ !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 k1 k2 =
+ match get_strategy k1, get_strategy k2 with
+ | Expand, _ -> true
+ | Level n1, Opaque -> true
+ | Level n1, Level n2 -> n1 < n2
+ | _ -> false (* expand k2 *)
(* summary operations *)
-type transparent_state = Idpred.t * Cpred.t
-let init() = (cst_transp := Cpred.full; var_transp := Idpred.full)
-let freeze () = (!var_transp, !cst_transp)
-let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
+let init() = (cst_opacity := Cmap.empty; var_opacity := Idmap.empty)
+let freeze () = (!var_opacity, !cst_opacity)
+let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 6e09ce6f0..86e108c6f 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -10,26 +10,31 @@
open Names
-
(* 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 : 'a tableKey -> 'a tableKey -> bool
-(* Changing the oracle *)
-val set_opaque_const : constant -> unit
-val set_transparent_const : constant -> unit
+(* Priority for the expansion of constant in the conversion test.
+ * Higher levels means that the expansion is less prioritary.
+ * (And Expand stands for -oo, and Opaque +oo.)
+ * The default value (transparent constants) is [Level 0].
+ *)
+type level = Expand | Level of int | Opaque
+val transparent : level
-val set_opaque_var : identifier -> unit
-val set_transparent_var : identifier -> unit
+val get_strategy : 'a tableKey -> level
-val is_opaque_cst : constant -> bool
-val is_opaque_var : identifier -> bool
+(* Sets the level of a constant.
+ * Level of RelKey constant cannot be set. *)
+val set_strategy : 'a tableKey -> level -> unit
-(*****************************)
+val get_transp_state : unit -> transparent_state
-(* transparent state summary operations *)
+(*****************************)
+(* Summary operations *)
+type oracle
val init : unit -> unit
-val freeze : unit -> transparent_state
-val unfreeze : transparent_state -> unit
+val freeze : unit -> oracle
+val unfreeze : oracle -> unit