aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml4
-rw-r--r--kernel/cClosure.mli4
-rw-r--r--kernel/cbytegen.ml27
-rw-r--r--kernel/constr.ml2
-rw-r--r--kernel/constr.mli6
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/esubst.ml10
-rw-r--r--kernel/esubst.mli6
-rw-r--r--kernel/names.mli19
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli6
-rw-r--r--kernel/typeops.mli4
-rw-r--r--kernel/univ.ml47
-rw-r--r--kernel/univ.mli13
14 files changed, 70 insertions, 82 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5f683790c..08114abc4 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -96,7 +96,7 @@ module type RedFlagsSig = sig
val red_transparent : reds -> transparent_state
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
- val red_projection : reds -> projection -> bool
+ val red_projection : reds -> Projection.t -> bool
end
module RedFlags = (struct
@@ -364,7 +364,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of projection * fconstr
+ | FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 3a7f77d52..e2f5a3b82 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -74,7 +74,7 @@ module type RedFlagsSig = sig
(** This tests if the projection is in unfolded state already or
is unfodable due to delta. *)
- val red_projection : reds -> projection -> bool
+ val red_projection : reds -> Projection.t -> bool
end
module RedFlags : RedFlagsSig
@@ -132,7 +132,7 @@ type fterm =
| FInd of inductive Univ.puniverses
| FConstruct of constructor Univ.puniverses
| FApp of fconstr * fconstr array
- | FProj of projection * fconstr
+ | FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0766f49b3..70dc6867a 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -500,22 +500,19 @@ let rec compile_lam env reloc lam sz cont =
| Lsort (Sorts.Prop _ as s) ->
compile_structured_constant reloc (Const_sort s) sz cont
| Lsort (Sorts.Type u) ->
- (* We separate global and local universes in [u]. The former will be part
- of the structured constant, while the later (if any) will be applied as
- arguments. *)
- let open Univ in begin
- let u,s = Universe.compact u in
- (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
- let compile_get_univ reloc idx sz cont =
- set_max_stack_size sz;
- compile_fv_elem reloc (FVuniv_var idx) sz cont
- in
- if List.is_empty s then
- compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
- else
- comp_app compile_structured_constant compile_get_univ reloc
+ (* We represent universes as a global constant with local universes
+ "compacted", i.e. as [u arg0 ... argn] where we will substitute (after
+ evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *)
+ let u,s = Univ.compact_univ u in
+ let compile_get_univ reloc idx sz cont =
+ set_max_stack_size sz;
+ compile_fv_elem reloc (FVuniv_var idx) sz cont
+ in
+ if List.is_empty s then
+ compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
+ else
+ comp_app compile_structured_constant compile_get_univ reloc
(Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
- end
| Llet (id,def,body) ->
compile_lam env reloc def sz
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ba7fecadf..4f062d72f 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -100,7 +100,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
(* constr is the fixpoint of the previous type. Requires option
-rectypes of the Caml compiler to be set *)
type t = (t, t, Sorts.t, Instance.t) kind_of_term
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 98c0eaa28..0d464840c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr
val mkConstU : pconstant -> constr
(** Constructs a projection application *)
-val mkProj : (projection * constr) -> constr
+val mkProj : (Projection.t * constr) -> constr
(** Inductive types *)
@@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
(** User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
@@ -318,7 +318,7 @@ where [info] is pretty-printing information *)
val destCase : constr -> case_info * constr * constr * constr array
(** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
(** Destructs the {% $ %}i{% $ %}th function of the block
[Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e6ac1e72..fdd84b25b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -168,7 +168,7 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
(** {6 Primitive projections} *)
-val lookup_projection : Names.projection -> env -> projection_body
+val lookup_projection : Names.Projection.t -> env -> projection_body
val is_projection : Constant.t -> env -> bool
(** {5 Inductive types } *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index a11a0dc00..91cc64523 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -19,6 +19,8 @@ open Util
(*********************)
(* Explicit lifts and basic operations *)
+(* Invariant to preserve in this module: no lift contains two consecutive
+ [ELSHFT] nor two consecutive [ELLFT]. *)
type lift =
| ELID
| ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
@@ -28,15 +30,15 @@ type lift =
let el_id = ELID
(* compose a relocation of magnitude n *)
-let rec el_shft_rec n = function
- | ELSHFT(el,k) -> el_shft_rec (k+n) el
+let el_shft_rec n = function
+ | ELSHFT(el,k) -> ELSHFT(el,k+n)
| el -> ELSHFT(el,n)
let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
(* cross n binders *)
-let rec el_liftn_rec n = function
+let el_liftn_rec n = function
| ELID -> ELID
- | ELLFT(k,el) -> el_liftn_rec (n+k) el
+ | ELLFT(k,el) -> ELLFT(n+k, el)
| el -> ELLFT(n, el)
let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index b82d6fdf0..a674c425a 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
(** {6 Compact representation } *)
(** Compact representation of explicit relocations
- [ELSHFT(l,n)] == lift of [n], then apply [lift l].
- - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+ - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders.
+
+ Invariant ensured by the private flag: no lift contains two consecutive
+ [ELSHFT] nor two consecutive [ELLFT].
+*)
type lift = private
| ELID
| ELSHFT of lift * int
diff --git a/kernel/names.mli b/kernel/names.mli
index ffd96781b..96e020aed 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -547,6 +547,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool
(** equalities on constant and inductive names (for the checker) *)
val eq_con_chk : Constant.t -> Constant.t -> bool
+[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."]
+
val eq_ind_chk : inductive -> inductive -> bool
(** {6 Deprecated functions. For backward compatibility.} *)
@@ -633,27 +635,27 @@ val eq_label : Label.t -> Label.t -> bool
(** {5 Unique bound module names} *)
type mod_bound_id = MBId.t
-(** Alias type. *)
+[@@ocaml.deprecated "Same as [MBId.t]."]
-val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+val mod_bound_id_ord : MBId.t -> MBId.t -> int
[@@ocaml.deprecated "Same as [MBId.compare]."]
-val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
+val mod_bound_id_eq : MBId.t -> MBId.t -> bool
[@@ocaml.deprecated "Same as [MBId.equal]."]
-val make_mbid : DirPath.t -> Id.t -> mod_bound_id
+val make_mbid : DirPath.t -> Id.t -> MBId.t
[@@ocaml.deprecated "Same as [MBId.make]."]
-val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
+val repr_mbid : MBId.t -> int * Id.t * DirPath.t
[@@ocaml.deprecated "Same as [MBId.repr]."]
-val id_of_mbid : mod_bound_id -> Id.t
+val id_of_mbid : MBId.t -> Id.t
[@@ocaml.deprecated "Same as [MBId.to_id]."]
-val string_of_mbid : mod_bound_id -> string
+val string_of_mbid : MBId.t -> string
[@@ocaml.deprecated "Same as [MBId.to_string]."]
-val debug_string_of_mbid : mod_bound_id -> string
+val debug_string_of_mbid : MBId.t -> string
[@@ocaml.deprecated "Same as [MBId.debug_to_string]."]
(** {5 Names} *)
@@ -745,6 +747,7 @@ module Projection : sig
end
type projection = Projection.t
+[@@ocaml.deprecated "Alias for [Projection.t]"]
val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
[@@ocaml.deprecated "Same as [Constant.make]"]
diff --git a/kernel/term.ml b/kernel/term.ml
index 403ed881c..e1affb1c0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
type values = Vmvalues.values
diff --git a/kernel/term.mli b/kernel/term.mli
index 7cb3b662d..ee84dcb2b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -155,7 +155,7 @@ val destCase : constr -> case_info * constr * constr * constr array
[@@ocaml.deprecated "Alias for [Constr.destCase]"]
(** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
[@@ocaml.deprecated "Alias for [Constr.destProj]"]
(** Destructs the {% $ %}i{% $ %}th function of the block
@@ -403,7 +403,7 @@ val mkApp : constr * constr array -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkConst : Constant.t -> constr
[@@ocaml.deprecated "Alias for Constr"]
-val mkProj : projection * constr -> constr
+val mkProj : Projection.t * constr -> constr
[@@ocaml.deprecated "Alias for Constr"]
val mkInd : inductive -> constr
[@@ocaml.deprecated "Alias for Constr"]
@@ -571,7 +571,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Case of Constr.case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) Constr.pfixpoint
| CoFix of ('constr, 'types) Constr.pcofixpoint
- | Proj of projection * 'constr
+ | Proj of Projection.t * 'constr
[@@ocaml.deprecated "Alias for Constr.kind_of_term"]
type values = Vmvalues.values
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index bff40b017..85b2cfffd 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment
(** {6 type of an applied projection } *)
-val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
(** {6 Type of application. } *)
val judge_of_apply :
@@ -100,7 +100,7 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_projection_constant : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Projection.t puniverses -> types
val type_of_constant_in : env -> pconstant -> types
diff --git a/kernel/univ.ml b/kernel/univ.ml
index be21381b7..ea3a52295 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -490,39 +490,6 @@ struct
in
List.fold_right (fun a acc -> aux a acc) u []
- (** [max_var_pred p u] returns the maximum variable level in [u] satisfying
- [p], -1 if not found *)
- let rec max_var_pred p u =
- let open Level in
- match u with
- | [] -> -1
- | (v, _) :: u ->
- match var_index v with
- | Some i when p i -> max i (max_var_pred p u)
- | _ -> max_var_pred p u
-
- let rec remap_var u i j =
- let open Level in
- match u with
- | [] -> []
- | (v, incr) :: u when var_index v = Some i ->
- (Level.var j, incr) :: remap_var u i j
- | _ :: u -> remap_var u i j
-
- let rec compact u max_var i =
- if i >= max_var then (u,[]) else
- let j = max_var_pred (fun j -> j < i) u in
- if Int.equal i (j+1) then
- let (u,s) = compact u max_var (i+1) in
- (u, i :: s)
- else
- let (u,s) = compact (remap_var u i j) max_var (i+1) in
- (u, j+1 :: s)
-
- let compact u =
- let max_var = max_var_pred (fun _ -> true) u in
- compact u max_var 0
-
(* Returns the formal universe that is greater than the universes u and v.
Used to type the products. *)
let sup x y = merge_univs x y
@@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) =
let subst, univs = abstract_universes univs in
subst, (univs, variance)
+let rec compact_univ s vars i u =
+ match u with
+ | [] -> (s, List.rev vars)
+ | (lvl, _) :: u ->
+ match Level.var_index lvl with
+ | Some k when not (LMap.mem lvl s) ->
+ let lvl' = Level.var i in
+ compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u
+ | _ -> compact_univ s vars i u
+
+let compact_univ u =
+ let (s, s') = compact_univ LMap.empty [] 0 u in
+ (subst_univs_level_universe s u, s')
+
(** Pretty-printing *)
let pr_constraints prl = Constraint.pr prl
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 629d83fb8..aaed899bf 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -128,12 +128,6 @@ sig
val map : (Level.t * int -> 'a) -> t -> 'a list
- (** [compact u] remaps local variables in [u] such that their indices become
- consecutive. It returns the new universe and the mapping.
- Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] =
- [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
- *)
- val compact : t -> t * int list
end
type universe = Universe.t
@@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit
val make_abstract_instance : AUContext.t -> Instance.t
+(** [compact_univ u] remaps local variables in [u] such that their indices become
+ consecutive. It returns the new universe and the mapping.
+ Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] =
+ [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2]
+*)
+val compact_univ : Universe.t -> Universe.t * int list
+
(** {6 Pretty-printing of universes. } *)
val pr_constraint_type : constraint_type -> Pp.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 16:42:20 +0000