diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cPrimitives.ml | 59 | ||||
| -rw-r--r-- | kernel/cPrimitives.mli | 13 | ||||
| -rw-r--r-- | kernel/conv_oracle.ml | 6 | ||||
| -rw-r--r-- | kernel/conv_oracle.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 6 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 6 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 10 |
9 files changed, 99 insertions, 9 deletions
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 3fa376a037..c4036e9677 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -52,6 +52,51 @@ type t = | Float64next_up | Float64next_down +let parse = function + | "int63_head0" -> Int63head0 + | "int63_tail0" -> Int63tail0 + | "int63_add" -> Int63add + | "int63_sub" -> Int63sub + | "int63_mul" -> Int63mul + | "int63_div" -> Int63div + | "int63_mod" -> Int63mod + | "int63_lsr" -> Int63lsr + | "int63_lsl" -> Int63lsl + | "int63_land" -> Int63land + | "int63_lor" -> Int63lor + | "int63_lxor" -> Int63lxor + | "int63_addc" -> Int63addc + | "int63_subc" -> Int63subc + | "int63_addcarryc" -> Int63addCarryC + | "int63_subcarryc" -> Int63subCarryC + | "int63_mulc" -> Int63mulc + | "int63_diveucl" -> Int63diveucl + | "int63_div21" -> Int63div21 + | "int63_addmuldiv" -> Int63addMulDiv + | "int63_eq" -> Int63eq + | "int63_lt" -> Int63lt + | "int63_le" -> Int63le + | "int63_compare" -> Int63compare + | "float64_opp" -> Float64opp + | "float64_abs" -> Float64abs + | "float64_eq" -> Float64eq + | "float64_lt" -> Float64lt + | "float64_le" -> Float64le + | "float64_compare" -> Float64compare + | "float64_classify" -> Float64classify + | "float64_add" -> Float64add + | "float64_sub" -> Float64sub + | "float64_mul" -> Float64mul + | "float64_div" -> Float64div + | "float64_sqrt" -> Float64sqrt + | "float64_of_int63" -> Float64ofInt63 + | "float64_normfr_mantissa" -> Float64normfr_mantissa + | "float64_frshiftexp" -> Float64frshiftexp + | "float64_ldshiftexp" -> Float64ldshiftexp + | "float64_next_up" -> Float64next_up + | "float64_next_down" -> Float64next_down + | _ -> raise Not_found + let equal (p1 : t) (p2 : t) = p1 == p2 @@ -229,3 +274,17 @@ let prim_type_to_string = function let op_or_type_to_string = function | OT_op op -> to_string op | OT_type t -> prim_type_to_string t + +let prim_type_of_string = function + | "int63_type" -> PT_int63 + | "float64_type" -> PT_float64 + | _ -> raise Not_found + +let op_or_type_of_string s = + try OT_type (prim_type_of_string s) + with Not_found -> OT_op (parse s) + +let parse_op_or_type ?loc s = + try op_or_type_of_string s + with Not_found -> + CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist.")) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 2a0399f1f7..a5db51111f 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -52,6 +52,10 @@ type t = | Float64next_up | Float64next_down +(** Can raise [Not_found]. + Beware that this is not exactly the reverse of [to_string] below. *) +val parse : string -> t + val equal : t -> t -> bool type arg_kind = @@ -75,6 +79,10 @@ type prim_type = | PT_int63 | PT_float64 +(** Can raise [Not_found] *) +val prim_type_of_string : string -> prim_type +val prim_type_to_string : prim_type -> string + type 'a prim_ind = | PIT_bool : unit prim_ind | PIT_carry : prim_type prim_ind @@ -90,8 +98,13 @@ type op_or_type = | OT_type of prim_type val prim_ind_to_string : 'a prim_ind -> string + +(** Can raise [Not_found] *) +val op_or_type_of_string : string -> op_or_type val op_or_type_to_string : op_or_type -> string +val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type + type ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type | PITT_type : prim_type -> ind_or_type diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 9b87c194c5..3ee1d2fb1f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,12 @@ open Names * The default value is [Level 100]. *) type level = Expand | Level of int | Opaque +let pr_level = function + | Expand -> Pp.str "expand" + | Level 0 -> Pp.str "transparent" + | Level n -> Pp.int n + | Opaque -> Pp.str "opaque" + let default = Level 0 let is_default = function | Level 0 -> true diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index b25488d94a..930edf6c49 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -27,6 +27,7 @@ val oracle_order : ('a -> Constant.t) -> oracle -> bool -> * The default value (transparent constants) is [Level 0]. *) type level = Expand | Level of int | Opaque +val pr_level : level -> Pp.t val transparent : level (** Check whether a level is transparent *) @@ -42,4 +43,3 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> TransparentState.t - diff --git a/kernel/environ.ml b/kernel/environ.ml index d6d52dbc2b..182ed55d0e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -67,7 +67,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -129,7 +129,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_sprop_allowed = true; - env_universes_lbound = Univ.Level.set; + env_universes_lbound = UGraph.Bound.Set; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; diff --git a/kernel/environ.mli b/kernel/environ.mli index 7a46538772..79e632daa0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -62,7 +62,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val universes_lbound : env -> Univ.Level.t -val set_universes_lbound : env -> Univ.Level.t -> env +val universes_lbound : env -> UGraph.Bound.t +val set_universes_lbound : env -> UGraph.Bound.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 8ac96a6481..e9687991c0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = if has_template_poly then (* For that particular case, we typecheck the inductive in an environment where the universes introduced by the definition are only [>= Prop] *) - let env = set_universes_lbound env Univ.Level.prop in + let env = set_universes_lbound env UGraph.Bound.Prop in push_context_set ~strict:false ctx env else (* In the regular case, all universes are [> Set] *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5f5f0ef8cd..927db9e9e6 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -148,8 +148,14 @@ let enforce_leq_alg u v g = assert (check_leq g u v); cg +module Bound = +struct + type t = Prop | Set +end + exception AlreadyDeclared = G.AlreadyDeclared let add_universe u ~lbound ~strict g = + let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in let graph = G.add u g.graph in let d = if strict then Lt else Le in enforce_constraint (lbound,d,u) {g with graph} diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8d9afb0990..c9fbd7f694 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t +module Bound : +sig + type t = Prop | Set + (** The [Prop] bound is only used for template polymorphic inductive types. *) +end + +val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : lbound:Level.t -> AUContext.t check_function +val check_subtype : lbound:Bound.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) |