diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 6 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 12 | ||||
| -rw-r--r-- | kernel/conv_oracle.mli | 2 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 1 | ||||
| -rw-r--r-- | kernel/names.ml | 7 | ||||
| -rw-r--r-- | kernel/names.mli | 8 | ||||
| -rw-r--r-- | kernel/reduction.ml | 8 | ||||
| -rw-r--r-- | kernel/reduction.mli | 8 | ||||
| -rw-r--r-- | kernel/transpState.ml | 18 | ||||
| -rw-r--r-- | kernel/transpState.mli | 26 | ||||
| -rw-r--r-- | kernel/vconv.ml | 4 |
11 files changed, 65 insertions, 35 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95546a83e1..c8028f713a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -93,8 +93,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> transparent_state -> reds - val red_transparent : reds -> transparent_state + val red_add_transparent : reds -> TranspState.t -> reds + val red_transparent : reds -> TranspState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -110,7 +110,7 @@ module RedFlags = (struct r_beta : bool; r_delta : bool; r_eta : bool; - r_const : transparent_state; + r_const : TranspState.t; r_zeta : bool; r_match : bool; r_fix : bool; diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1ee4bccc25..9d41ee0695 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -26,11 +26,11 @@ val with_stats: 'a Lazy.t -> 'a -val all_opaque : transparent_state -val all_transparent : transparent_state +val all_opaque : TranspState.t +val all_transparent : TranspState.t -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> Constant.t -> bool +val is_transparent_variable : TranspState.t -> variable -> bool +val is_transparent_constant : TranspState.t -> Constant.t -> bool (** Sets of reduction kinds. *) module type RedFlagsSig = sig @@ -60,10 +60,10 @@ module type RedFlagsSig = sig val red_sub : reds -> red_kind -> reds (** Adds a reduction kind to a set *) - val red_add_transparent : reds -> transparent_state -> reds + val red_add_transparent : reds -> TranspState.t -> reds (** Retrieve the transparent state of the reduction flags *) - val red_transparent : reds -> transparent_state + val red_transparent : reds -> TranspState.t (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 67add5dd35..3b51515352 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a -val get_transp_state : oracle -> transparent_state +val get_transp_state : oracle -> TranspState.t diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index a18c5d1e20..e716972ebe 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,4 +1,5 @@ Names +TranspState Uint31 Univ UGraph diff --git a/kernel/names.ml b/kernel/names.ml index 18560d5f8d..b2d6a489a6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons (*****************) -type transparent_state = Id.Pred.t * Cpred.t - -let empty_transparent_state = (Id.Pred.empty, Cpred.empty) -let full_transparent_state = (Id.Pred.full, Cpred.full) -let var_full_transparent_state = (Id.Pred.full, Cpred.empty) -let cst_full_transparent_state = (Id.Pred.empty, Cpred.full) - type 'a tableKey = | ConstKey of 'a | VarKey of Id.t diff --git a/kernel/names.mli b/kernel/names.mli index 98995752a2..350db871d5 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -510,14 +510,6 @@ type 'a tableKey = | VarKey of Id.t | RelKey of Int.t -(** Sets of names *) -type transparent_state = Id.Pred.t * Cpred.t - -val empty_transparent_state : transparent_state -val full_transparent_state : transparent_state -val var_full_transparent_state : transparent_state -val cst_full_transparent_state : transparent_state - type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5515ff9767..a45a5b3247 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = - ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?l2r:bool -> ?reds:TranspState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = +let gen_conv cv_pb ?(l2r=false) ?(reds=TranspState.full) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in @@ -792,11 +792,11 @@ let infer_conv_universes = CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes -let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) +let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) env univs t1 t2 = infer_conv_universes CONV l2r evars ts env univs t1 t2 -let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) +let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TranspState.full) env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 581e8bd88a..9b26e7b3dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = - ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?l2r:bool -> ?reds:TranspState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> constr infer_conversion_function + ?ts:TranspState.t -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> types infer_conversion_function + ?ts:TranspState.t -> types infer_conversion_function (** Depending on the universe state functions, this might raise [UniverseInconsistency] in addition to [NotConvertible] (for better error messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> - Names.transparent_state -> (constr,'a) generic_conversion_function + TranspState.t -> (constr,'a) generic_conversion_function val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function diff --git a/kernel/transpState.ml b/kernel/transpState.ml new file mode 100644 index 0000000000..9acb7244f7 --- /dev/null +++ b/kernel/transpState.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +type t = Id.Pred.t * Cpred.t + +let empty = (Id.Pred.empty, Cpred.empty) +let full = (Id.Pred.full, Cpred.full) +let var_full = (Id.Pred.full, Cpred.empty) +let cst_full = (Id.Pred.empty, Cpred.full) diff --git a/kernel/transpState.mli b/kernel/transpState.mli new file mode 100644 index 0000000000..a8d301549b --- /dev/null +++ b/kernel/transpState.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** Sets of names *) +type t = Id.Pred.t * Cpred.t + +val empty : t +(** Everything opaque *) + +val full : t +(** Everything transparent *) + +val var_full : t +(** All variables transparent *) + +val cst_full : t +(** All constant transparent *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c1130e62c9..46e52121c7 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed = let vm_conv_gen cv_pb env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 else try let v1 = val_of_constr env t1 in @@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 = with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2 + TranspState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in |