aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml11
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml15
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/evd.ml19
-rw-r--r--engine/evd.mli56
-rw-r--r--engine/namegen.mli3
-rw-r--r--engine/termops.ml9
-rw-r--r--engine/termops.mli8
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli14
-rw-r--r--engine/universes.ml25
-rw-r--r--engine/universes.mli76
13 files changed, 126 insertions, 122 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index a54c082979..bcfbc8081e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -10,6 +10,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Context
open Evd
@@ -34,7 +35,7 @@ end
type t
val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
+val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : Evd.evar_map -> t -> t
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
@@ -84,16 +85,16 @@ let rec whd_evar sigma c =
| Some c -> whd_evar sigma c
| None -> c
end
- | App (f, args) when isEvar f ->
+ | App (f, args) when Term.isEvar f ->
(** Enforce smart constructor invariant on applications *)
- let ev = destEvar f in
+ let ev = Term.destEvar f in
begin match safe_evar_value sigma ev with
| None -> c
| Some f -> whd_evar sigma (mkApp (f, args))
end
- | Cast (c0, k, t) when isEvar c0 ->
+ | Cast (c0, k, t) when Term.isEvar c0 ->
(** Enforce smart constructor invariant on casts. *)
- let ev = destEvar c0 in
+ let ev = Term.destEvar c0 in
begin match safe_evar_value sigma ev with
| None -> c
| Some c -> whd_evar sigma (mkCast (c, k, t))
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index a4ad233b0b..e9ef302cf6 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -93,7 +93,7 @@ val mkEvar : t pexistential -> t
val mkSort : Sorts.t -> t
val mkProp : t
val mkSet : t
-val mkType : Univ.universe -> t
+val mkType : Univ.Universe.t -> t
val mkCast : t * cast_kind * t -> t
val mkProd : Name.t * t * t -> t
val mkLambda : Name.t * t * t -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 38efcca050..df4ef2ce71 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,6 +10,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Termops
open Namegen
open Pre_env
@@ -56,12 +57,12 @@ let new_global evd x =
exception Uninstantiated_evar of existential_key
let rec flush_and_check_evars sigma c =
- match kind_of_term c with
+ match kind c with
| Evar (evk,_ as ev) ->
(match existential_opt_value sigma ev with
| None -> raise (Uninstantiated_evar evk)
| Some c -> flush_and_check_evars sigma c)
- | _ -> map_constr (flush_and_check_evars sigma) c
+ | _ -> Constr.map (flush_and_check_evars sigma) c
let flush_and_check_evars sigma c =
flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
@@ -162,7 +163,7 @@ exception NoHeadEvar
let head_evar sigma c =
(** FIXME: this breaks if using evar-insensitive code *)
let c = EConstr.Unsafe.to_constr c in
- let rec hrec c = match kind_of_term c with
+ let rec hrec c = match kind c with
| Evar (evk,_) -> evk
| Case (_,_,c,_) -> hrec c
| App (c,_) -> hrec c
@@ -485,7 +486,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
(ie the hypotheses ids have been removed from the contexts of
evars). [global] should be true iff there is some variable of [ids] which
is a section variable *)
- match kind_of_term c with
+ match kind c with
| Var id' ->
if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
@@ -552,7 +553,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
evdref := evd;
Evd.existential_value !evdref ev
- | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
+ | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
let clear_hyps_in_evi_main env evdref hyps terms ids =
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
@@ -696,10 +697,10 @@ let undefined_evars_of_evar_info evd evi =
do not have this luxury, and need the more complete version. *)
let occur_evar_upto sigma n c =
let c = EConstr.Unsafe.to_constr c in
- let rec occur_rec c = match kind_of_term c with
+ let rec occur_rec c = match kind c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
| Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
- | _ -> iter_constr occur_rec c
+ | _ -> Constr.iter occur_rec c
in
try occur_rec c; false with Occur -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 2f85bc7335..62288ced46 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Evd
open Environ
open EConstr
@@ -54,11 +54,11 @@ val e_new_evar :
val new_type_evar :
env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
- evar_map * (constr * sorts)
+ evar_map * (constr * Sorts.t)
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
+ ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
diff --git a/engine/evd.ml b/engine/evd.ml
index 86ab2263f5..a1cb0ec68e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -8,10 +8,11 @@
open Pp
open CErrors
+open Sorts
open Util
open Names
open Nameops
-open Term
+open Constr
open Vars
open Environ
@@ -126,7 +127,7 @@ end
module Store = Store.Make ()
-type evar = Term.existential_key
+type evar = existential_key
let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
@@ -242,7 +243,7 @@ let evar_instance_array test_id info args =
instrec filter (evar_context info) 0
let make_evar_instance_array info args =
- evar_instance_array (NamedDecl.get_id %> isVarId) info args
+ evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
let instantiate_evar_array info c args =
let inst = make_evar_instance_array info args in
@@ -280,9 +281,9 @@ type 'a freelisted = {
(* Collects all metavars appearing in a constr *)
let metavars_of c =
let rec collrec acc c =
- match kind_of_term c with
+ match kind c with
| Meta mv -> Int.Set.add mv acc
- | _ -> Term.fold_constr collrec acc c
+ | _ -> Constr.fold collrec acc c
in
collrec Int.Set.empty c
@@ -706,10 +707,10 @@ let extract_all_conv_pbs evd =
extract_conv_pbs evd (fun _ -> true)
let loc_of_conv_pb evd (pbty,env,t1,t2) =
- match kind_of_term (fst (decompose_app t1)) with
+ match kind (fst (Term.decompose_app t1)) with
| Evar (evk1,_) -> fst (evar_source evk1 evd)
| _ ->
- match kind_of_term (fst (decompose_app t2)) with
+ match kind (fst (Term.decompose_app t2)) with
| Evar (evk2,_) -> fst (evar_source evk2 evd)
| _ -> None
@@ -720,9 +721,9 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
let evars_of_term c =
let rec evrec acc c =
- match kind_of_term c with
+ match kind c with
| Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
- | _ -> Term.fold_constr evrec acc c
+ | _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
diff --git a/engine/evd.mli b/engine/evd.mli
index 7576b3d5fc..45ca1a365a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -9,7 +9,7 @@
open Util
open Loc
open Names
-open Term
+open Constr
open Environ
(** This file defines the pervasive unification state used everywhere in Coq
@@ -488,10 +488,10 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * evar_universe_context
-val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : evar_universe_context -> Univ.ContextSet.t
val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
-val evar_context_universe_context : evar_universe_context -> Univ.universe_context
-val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
+val evar_context_universe_context : evar_universe_context -> Univ.UContext.t
+val evar_universe_context_of : Univ.ContextSet.t -> evar_universe_context
val empty_evar_universe_context : evar_universe_context
val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
evar_universe_context
@@ -503,10 +503,10 @@ val evar_universe_context_of_binders :
Universes.universe_binders -> evar_universe_context
val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
-val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map
+val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
-val universe_of_name : evar_map -> string -> Univ.universe_level
-val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
+val universe_of_name : evar_map -> string -> Univ.Level.t
+val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map
val add_constraints_context : evar_universe_context ->
Univ.constraints -> evar_universe_context
@@ -518,50 +518,50 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
val normalize_evar_universe_context : evar_universe_context ->
evar_universe_context
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t
val add_global_univ : evar_map -> Univ.Level.t -> evar_map
val universe_rigidity : evar_map -> Univ.Level.t -> rigid
-val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map
+val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map
(** See [UState.make_flexible_variable] *)
-val is_sort_variable : evar_map -> sorts -> Univ.universe_level option
+val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
not a local sort variable declared in [evm] *)
val is_flexible_level : evar_map -> Univ.Level.t -> bool
-(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
-val normalize_universe : evar_map -> Univ.universe -> Univ.universe
-val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
+(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
+val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t
+val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
-val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map
-val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map
-val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
-val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
-val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
+val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
+val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
+val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map
+val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
+val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
val set_eq_instances : ?flex:bool ->
- evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
+ evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
-val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool
-val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
+val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
+val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
val evar_universe_context : evar_map -> evar_universe_context
-val universe_context_set : evar_map -> Univ.universe_context_set
+val universe_context_set : evar_map -> Univ.ContextSet.t
val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
- (Id.t * Univ.Level.t) list * Univ.universe_context
+ (Id.t * Univ.Level.t) list * Univ.UContext.t
val universe_subst : evar_map -> Universes.universe_opt_subst
val universes : evar_map -> UGraph.t
val check_univ_decl : evar_map -> UState.universe_decl ->
- Universes.universe_binders * Univ.universe_context
+ Universes.universe_binders * Univ.UContext.t
val merge_universe_context : evar_map -> evar_universe_context -> evar_map
val set_universe_context : evar_map -> evar_universe_context -> evar_map
-val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
@@ -579,7 +579,7 @@ val update_sigma_env : evar_map -> env -> evar_map
(** Polymorphic universes *)
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t
val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
diff --git a/engine/namegen.mli b/engine/namegen.mli
index d29b69259f..abeed9f62d 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -9,7 +9,6 @@
(** This file features facilities to generate fresh names. *)
open Names
-open Term
open Environ
open Evd
open EConstr
@@ -27,7 +26,7 @@ val default_dependent_ident : Id.t (* "x" *)
Generating "intuitive" names from their type *)
val lowercase_first_char : Id.t -> string
-val sort_hdchar : sorts -> string
+val sort_hdchar : Sorts.t -> string
val hdchar : env -> evar_map -> types -> string
val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
val named_hd : env -> evar_map -> types -> Name.t -> Name.t
diff --git a/engine/termops.ml b/engine/termops.ml
index 67533cce42..78dbdb11aa 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -12,6 +12,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Vars
open Environ
@@ -46,7 +47,7 @@ let pr_puniverses p u =
if Univ.Instance.is_empty u then p
else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
-let rec pr_constr c = match kind_of_term c with
+let rec pr_constr c = match kind c with
| Rel n -> str "#"++int n
| Meta n -> str "Meta(" ++ int n ++ str ")"
| Var id -> pr_id id
@@ -798,7 +799,7 @@ let fold_constr_with_binders sigma g f n acc c =
let iter_constr_with_full_binders g f l c =
let open RelDecl in
- match kind_of_term c with
+ match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> ()
| Cast (c,_, t) -> f l c; f l t
@@ -983,9 +984,9 @@ let isMetaOf sigma mv c =
match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false
let rec subst_meta bl c =
- match kind_of_term c with
+ match kind c with
| Meta i -> (try Int.List.assoc i bl with Not_found -> c)
- | _ -> map_constr (subst_meta bl) c
+ | _ -> Constr.map (subst_meta bl) c
let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
| Cast (c,_,_) -> strip_outer_cast sigma c
diff --git a/engine/termops.mli b/engine/termops.mli
index ef2c52a455..2dab0685d6 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -10,13 +10,13 @@
needed in the kernel. *)
open Names
-open Term
+open Constr
open Environ
open EConstr
(** printers *)
-val print_sort : sorts -> Pp.t
-val pr_sort_family : sorts_family -> Pp.t
+val print_sort : Sorts.t -> Pp.t
+val pr_sort_family : Sorts.family -> Pp.t
val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
(** about contexts *)
@@ -147,7 +147,7 @@ val subst_term : Evd.evar_map -> constr -> constr -> constr
val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr
(** Alternative term equalities *)
-val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val base_sort_cmp : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool
val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) ->
Reduction.conv_pb -> constr -> constr -> bool
val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool
diff --git a/engine/uState.ml b/engine/uState.ml
index 13a9bb3732..77837fefcf 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -33,10 +33,10 @@ type uinfo = {
(* 2nd part used to check consistency on the fly. *)
type t =
{ uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
- uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ uctx_local : Univ.ContextSet.t; (** The local context of variables *)
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.universe_set;
+ uctx_univ_algebraic : Univ.LSet.t;
(** The subset of unification variables that can be instantiated with
algebraic universes as they appear in inferred types only. *)
uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
diff --git a/engine/uState.mli b/engine/uState.mli
index c44f2c1d74..b31e94b285 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -28,13 +28,13 @@ val is_empty : t -> bool
val union : t -> t -> t
-val of_context_set : Univ.universe_context_set -> t
+val of_context_set : Univ.ContextSet.t -> t
val of_binders : Universes.universe_binders -> t
(** {5 Projections} *)
-val context_set : t -> Univ.universe_context_set
+val context_set : t -> Univ.ContextSet.t
(** The local context of the state, i.e. a set of bound variables together
with their associated constraints. *)
@@ -54,7 +54,7 @@ val algebraics : t -> Univ.LSet.t
val constraints : t -> Univ.constraints
(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
-val context : t -> Univ.universe_context
+val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
(** {5 Constraints handling} *)
@@ -79,7 +79,7 @@ val universe_of_name : t -> string -> Univ.Level.t
(** {5 Unification} *)
-val restrict : t -> Univ.universe_set -> t
+val restrict : t -> Univ.LSet.t -> t
type rigid =
| UnivRigid
@@ -89,7 +89,7 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
@@ -130,12 +130,12 @@ val normalize : t -> t
Also return the association list of universe names and universes
(including those not in [names]). *)
val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
- (Id.t * Univ.Level.t) list * Univ.universe_context
+ (Id.t * Univ.Level.t) list * Univ.UContext.t
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t
(** {5 TODO: Document me} *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 0a2045a046..3136f805c8 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -6,10 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Sorts
open Util
open Pp
open Names
-open Term
+open Constr
open Environ
open Univ
open Globnames
@@ -20,7 +21,7 @@ let pr_with_global_universes l =
(** Local universe names of polymorphic references *)
-type universe_binders = (Id.t * Univ.universe_level) list
+type universe_binders = (Id.t * Univ.Level.t) list
let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
@@ -39,7 +40,7 @@ let is_set_minimization () = !set_minimization
type universe_constraint_type = ULe | UEq | ULub
-type universe_constraint = universe * universe_constraint_type * universe
+type universe_constraint = Universe.t * universe_constraint_type * Universe.t
module Constraints = struct
module S = Set.Make(
@@ -157,10 +158,10 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
if res then Some !cstrs else None
let compare_head_gen_proj env equ eqs eqc' m n =
- match kind_of_term m, kind_of_term n with
+ match kind m, kind n with
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
- (match kind_of_term f with
+ (match kind f with
| Const (p', u) when Constant.equal (Projection.constant p) p' ->
let pb = Environ.lookup_projection p env in
let npars = pb.Declarations.proj_npars in
@@ -328,7 +329,7 @@ let fresh_global_or_constr_instance env = function
| IsGlobal gr -> fresh_global_instance env gr
let global_of_constr c =
- match kind_of_term c with
+ match kind c with
| Const (c, u) -> ConstRef c, u
| Ind (i, u) -> IndRef i, u
| Construct (c, u) -> ConstructRef c, u
@@ -390,8 +391,8 @@ let type_of_reference env r =
let type_of_global t = type_of_reference (Global.env ()) t
let fresh_sort_in_family env = function
- | InProp -> prop_sort, ContextSet.empty
- | InSet -> set_sort, ContextSet.empty
+ | InProp -> Sorts.prop, ContextSet.empty
+ | InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
Type (Univ.Universe.make u), ContextSet.singleton u
@@ -449,7 +450,7 @@ let nf_evars_and_universes_opt_subst f subst =
let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
let lsubst = Univ.level_subst_of subst in
let rec aux c =
- match kind_of_term c with
+ match kind c with
| Evar (evk, args) ->
let args = Array.map aux args in
(match try f (evk, args) with Not_found -> None with
@@ -467,7 +468,7 @@ let nf_evars_and_universes_opt_subst f subst =
| Sort (Type u) ->
let u' = Univ.subst_univs_universe subst u in
if u' == u then c else mkSort (sort_of_univ u')
- | _ -> map_constr aux c
+ | _ -> Constr.map aux c
in aux
let fresh_universe_context_set_instance ctx =
@@ -526,7 +527,7 @@ let normalize_opt_subst ctx =
else try ignore(normalize u) with Not_found -> assert(false)) ctx
in !ectx
-type universe_opt_subst = universe option universe_map
+type universe_opt_subst = Universe.t option universe_map
let make_opt_subst s =
fun x ->
@@ -788,7 +789,7 @@ let normalize_context_set ctx us algs =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
- ctx UGraph.empty_universes
+ ctx UGraph.initial_universes
in
let g =
Univ.Constraint.fold
diff --git a/engine/universes.mli b/engine/universes.mli
index 3678ec94de..24613c4b91 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -8,7 +8,7 @@
open Util
open Names
-open Term
+open Constr
open Environ
open Univ
@@ -21,26 +21,26 @@ val pr_with_global_universes : Level.t -> Pp.t
(** Local universe name <-> level mapping *)
-type universe_binders = (Id.t * Univ.universe_level) list
-
+type universe_binders = (Id.t * Univ.Level.t) list
+
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
(** The global universe counter *)
-val set_remote_new_univ_level : universe_level RemoteCounter.installer
+val set_remote_new_univ_level : Level.t RemoteCounter.installer
(** Side-effecting functions creating new universe levels. *)
-val new_univ_level : DirPath.t -> universe_level
-val new_univ : DirPath.t -> universe
+val new_univ_level : DirPath.t -> Level.t
+val new_univ : DirPath.t -> Universe.t
val new_Type : DirPath.t -> types
-val new_Type_sort : DirPath.t -> sorts
+val new_Type_sort : DirPath.t -> Sorts.t
-val new_global_univ : unit -> universe in_universe_context_set
-val new_sort_in_family : sorts_family -> sorts
+val new_global_univ : unit -> Universe.t in_universe_context_set
+val new_sort_in_family : Sorts.family -> Sorts.t
(** {6 Constraints for type inference}
-
+
When doing conversion of universes, not only do we have =/<= constraints but
also Lub constraints which correspond to unification of two levels which might
not be necessary if unfolding is performed.
@@ -48,7 +48,7 @@ val new_sort_in_family : sorts_family -> sorts
type universe_constraint_type = ULe | UEq | ULub
-type universe_constraint = universe * universe_constraint_type * universe
+type universe_constraint = Universe.t * universe_constraint_type * Universe.t
module Constraints : sig
include Set.S with type elt = universe_constraint
@@ -63,7 +63,7 @@ type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> unive
val subst_univs_universe_constraints : universe_subst_fn ->
universe_constraints -> universe_constraints
-val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
+val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
val to_constraints : UGraph.t -> universe_constraints -> constraints
@@ -82,14 +82,14 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
-val fresh_instance_from_context : abstract_universe_context ->
- universe_instance constrained
+val fresh_instance_from_context : AUContext.t ->
+ Instance.t constrained
-val fresh_instance_from : abstract_universe_context -> universe_instance option ->
- universe_instance in_universe_context_set
+val fresh_instance_from : AUContext.t -> Instance.t option ->
+ Instance.t in_universe_context_set
-val fresh_sort_in_family : env -> sorts_family ->
- sorts in_universe_context_set
+val fresh_sort_in_family : env -> Sorts.family ->
+ Sorts.t in_universe_context_set
val fresh_constant_instance : env -> Constant.t ->
pconstant in_universe_context_set
val fresh_inductive_instance : env -> inductive ->
@@ -105,15 +105,15 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set ->
- universe_level_subst * universe_context_set
+val fresh_universe_context_set_instance : ContextSet.t ->
+ universe_level_subst * ContextSet.t
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> Globnames.global_reference puniverses
val constr_of_global_univ : Globnames.global_reference puniverses -> constr
-val extend_context : 'a in_universe_context_set -> universe_context_set ->
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
'a in_universe_context_set
(** Simplification and pruning of constraints:
@@ -127,38 +127,38 @@ val extend_context : 'a in_universe_context_set -> universe_context_set ->
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
-module UF : Unionfind.PartitionSig with type elt = universe_level
+module UF : Unionfind.PartitionSig with type elt = Level.t
-type universe_opt_subst = universe option universe_map
+type universe_opt_subst = Universe.t option universe_map
val make_opt_subst : universe_opt_subst -> universe_subst_fn
val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
-val normalize_context_set : universe_context_set ->
+val normalize_context_set : ContextSet.t ->
universe_opt_subst (* The defined and undefined variables *) ->
- universe_set (* univ variables that can be substituted by algebraics *) ->
- (universe_opt_subst * universe_set) in_universe_context_set
+ LSet.t (* univ variables that can be substituted by algebraics *) ->
+ (universe_opt_subst * LSet.t) in_universe_context_set
val normalize_univ_variables : universe_opt_subst ->
- universe_opt_subst * universe_set * universe_set * universe_subst
+ universe_opt_subst * LSet.t * LSet.t * universe_subst
val normalize_univ_variable :
- find:(universe_level -> universe) ->
- update:(universe_level -> universe -> universe) ->
- universe_level -> universe
+ find:(Level.t -> Universe.t) ->
+ update:(Level.t -> Universe.t -> Universe.t) ->
+ Level.t -> Universe.t
val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
- (universe_level -> universe)
+ (Level.t -> Universe.t)
val normalize_univ_variable_subst : universe_subst ref ->
- (universe_level -> universe)
+ (Level.t -> Universe.t)
val normalize_universe_opt_subst : universe_opt_subst ref ->
- (universe -> universe)
+ (Universe.t -> Universe.t)
val normalize_universe_subst : universe_subst ref ->
- (universe -> universe)
+ (Universe.t -> Universe.t)
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
@@ -180,7 +180,7 @@ val type_of_global : Globnames.global_reference -> types in_universe_context_set
val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
universe_opt_subst -> constr -> constr
-val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
+val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
(** Pretty-printing *)
@@ -188,11 +188,11 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
(** {6 Support for template polymorphism } *)
-val solve_constraints_system : universe option array -> universe array -> universe array ->
- universe array
+val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
+ Universe.t array
(** Operations for universe_info_ind *)
(** Given a universe context representing constraints of an inductive
this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info
+val univ_inf_ind_from_universe_context : UContext.t -> CumulativityInfo.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:09:02 +0000