aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml18
-rw-r--r--kernel/csymtable.ml2
-rw-r--r--kernel/reduction.ml12
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/term.ml6
-rw-r--r--kernel/term.mli12
-rw-r--r--kernel/term_typing.ml3
-rw-r--r--kernel/univ.ml37
-rw-r--r--kernel/univ.mli7
-rw-r--r--kernel/vmvalues.ml11
10 files changed, 82 insertions, 32 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5dab2932d7..4a34dbcffe 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont =
of the structured constant, while the later (if any) will be applied as
arguments. *)
let open Univ in begin
- let levels = Universe.levels u in
- let global_levels =
- LSet.filter (fun x -> Level.var_index x = None) levels
- in
- let local_levels =
- List.map_filter (fun x -> Level.var_index x)
- (LSet.elements levels)
- in
+ let u,s = Universe.compact u in
(* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
- let uglob =
- LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
- in
- if local_levels = [] then
- compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont
+ if List.is_empty s then
+ compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont
else
let compile_get_univ reloc idx sz cont =
set_max_stack_size sz;
compile_fv_elem reloc (FVuniv_var idx) sz cont
in
comp_app compile_str_cst compile_get_univ reloc
- (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+ (Bstrconst (Const_type u)) (Array.of_list s) sz cont
end
| LetIn(_,xb,_,body) ->
compile_constr reloc xb sz
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 2bbb867cd4..bbd284bc1d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_bn _, _ -> false
| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
| Const_univ_level _ , _ -> false
-| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2
| Const_type _ , _ -> false
let rec hash_structured_constant c =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 159d2ea665..da7042713f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -882,6 +882,18 @@ let hnf_prod_app env t n =
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
+let hnf_prod_applist_assum env n c l =
+ let rec app n subst t l =
+ if Int.equal n 0 then
+ if l == [] then substl subst t
+ else anomaly (Pp.str "Too many arguments.")
+ else match kind (whd_allnolet env t), l with
+ | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+ | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
+ | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+ app n [] c l
+
(* Dealing with arities *)
let dest_prod env =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0e6a2b8199..6f7e3f8f8f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -105,6 +105,12 @@ val beta_app : constr -> constr -> constr
(** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
val hnf_prod_applist : env -> types -> constr list -> types
+(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to
+ the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it
+ returns [t] with the assumptions of [Γ] instantiated by [args] and
+ the local definitions of [Γ] expanded. *)
+val hnf_prod_applist_assum : env -> int -> types -> constr list -> types
+
(** Compatibility alias for Term.lambda_appvect_assum *)
val betazeta_appvect : int -> constr -> constr array -> constr
diff --git a/kernel/term.ml b/kernel/term.ml
index fae990d45f..a4c92bd333 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -352,10 +352,11 @@ let lambda_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough lambda/let's.") in
app n [] c l
@@ -377,10 +378,11 @@ let prod_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a8cf6e1e..b4597676a3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr
val lambda_appvect : constr -> constr array -> constr
(** In [lambda_applist_assum n c args], [c] is supposed to have the
- form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
val lambda_applist_assum : int -> constr -> constr list -> constr
@@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr
(** pseudo-reduction rule *)
(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
-val prod_appvect : constr -> constr array -> constr
-val prod_applist : constr -> constr list -> constr
+val prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
(** In [prod_appvect_assum n c args], [c] is supposed to have the
- form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
-val prod_appvect_assum : int -> constr -> constr array -> constr
-val prod_applist_assum : int -> constr -> constr list -> constr
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
(** {5 Other term destructors. } *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 5f501bff10..9b864440d1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -223,9 +223,8 @@ let rec unzip ctx j =
unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
let feedback_completion_typecheck =
- let open Feedback in
Option.iter (fun state_id ->
- feedback ~id:state_id Feedback.Complete)
+ Feedback.feedback ~id:state_id Feedback.Complete)
let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 080bb7ad48..fbb0473644 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -266,7 +266,7 @@ struct
module Expr =
struct
type t = Level.t * int
-
+
(* Hashing of expressions *)
module ExprHash =
struct
@@ -487,7 +487,40 @@ struct
| [] -> cons a l
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
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 77ebf5a11b..c45ebe21cc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -125,6 +125,13 @@ sig
val for_all : (Level.t * int -> bool) -> t -> bool
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
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec18..2d8a1d9761 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,6 +8,7 @@
open Names
open Sorts
open Cbytecodes
+open Univ
(*******************************************)
(* Initalization of the abstract machine ***)
@@ -189,11 +190,11 @@ let rec whd_accu a stk =
| i when Int.equal i type_atom_tag ->
begin match stk with
| [Zapp args] ->
- let u = ref (Obj.obj (Obj.field at 0)) in
- for i = 0 to nargs args - 1 do
- u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
- done;
- Vsort (Type !u)
+ let args = Array.init (nargs args) (arg args) in
+ let u = Obj.obj (Obj.field at 0) in
+ let inst = Instance.of_array (Array.map uni_lvl_val args) in
+ let u = Univ.subst_instance_universe inst u in
+ Vsort (Type u)
| _ -> assert false
end
| i when i <= max_atom_tag ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 10:11:55 +0000