diff options
Diffstat (limited to 'kernel/conv_oracle.mli')
| -rw-r--r-- | kernel/conv_oracle.mli | 31 |
1 files changed, 18 insertions, 13 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 966edd1d..6a774b4b 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -6,30 +6,35 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: conv_oracle.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id: conv_oracle.mli 10961 2008-05-21 23:26:23Z barras $ i*) 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 |