aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/vm_printers.ml3
-rw-r--r--kernel/cbytecodes.ml23
-rw-r--r--kernel/cbytecodes.mli3
-rw-r--r--kernel/cbytegen.ml22
-rw-r--r--kernel/cemitcodes.ml2
-rw-r--r--kernel/vconv.ml8
-rw-r--r--kernel/vm.ml2
-rw-r--r--kernel/vmvalues.ml30
-rw-r--r--kernel/vmvalues.mli3
-rw-r--r--pretyping/vnorm.ml4
10 files changed, 45 insertions, 55 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index f819d2e6a..bb7a963aa 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,7 @@ and ppstack s =
and ppatom a =
match a with
| Aid idk -> print_idkey idk
- | Atype u -> print_string "Type(...)"
+ | Asort u -> print_string "Sort(...)"
| Aind(sp,i) -> print_string "Ind(";
print_string (MutInd.to_string sp);
print_string ","; print_int i;
@@ -69,7 +69,6 @@ and ppatom a =
and ppwhd whd =
match whd with
- | Vsort s -> ppsort s
| Vprod _ -> print_string "product"
| Vfun _ -> print_string "function"
| Vfix _ -> print_vfix()
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index aa6c49bc7..586ef1709 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -32,13 +32,12 @@ let cofix_evaluated_tag = 7
let last_variant_tag = 245
type structured_constant =
- | Const_sorts of Sorts.t
+ | Const_sort of Sorts.t
| Const_ind of inductive
| Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
| Const_univ_level of Univ.Level.t
- | Const_type of Univ.Universe.t
type reloc_table = (tag * int) array
@@ -46,8 +45,8 @@ type annot_switch =
{ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
let rec eq_structured_constant c1 c2 = match c1, c2 with
-| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_sorts _, _ -> false
+| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2
+| Const_sort _, _ -> false
| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
| Const_ind _, _ -> false
| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
@@ -59,13 +58,11 @@ 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 _ , _ -> false
let rec hash_structured_constant c =
let open Hashset.Combine in
match c with
- | Const_sorts s -> combinesmall 1 (Sorts.hash s)
+ | Const_sort s -> combinesmall 1 (Sorts.hash s)
| Const_ind i -> combinesmall 2 (ind_hash i)
| Const_proj p -> combinesmall 3 (Constant.hash p)
| Const_b0 t -> combinesmall 4 (Int.hash t)
@@ -74,7 +71,6 @@ let rec hash_structured_constant c =
let h = Array.fold_left fold 0 a in
combinesmall 5 (combine (Int.hash t) h)
| Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
- | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
let eq_annot_switch asw1 asw2 =
let eq_ci ci1 ci2 =
@@ -236,20 +232,19 @@ open Util
let pp_sort s =
let open Sorts in
- match family s with
- | InSet -> str "Set"
- | InProp -> str "Prop"
- | InType -> str "Type"
+ match s with
+ | Prop Null -> str "Prop"
+ | Prop Pos -> str "Set"
+ | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
let rec pp_struct_const = function
- | Const_sorts s -> pp_sort s
+ | Const_sort s -> pp_sort s
| Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
| Const_proj p -> Constant.print p
| Const_b0 i -> int i
| Const_bn (i,t) ->
int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
| Const_univ_level l -> Univ.Level.pr l
- | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
let pp_lbl lbl = str "L" ++ int lbl
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index c8fbb27a9..71dd65186 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -26,13 +26,12 @@ val cofix_evaluated_tag : tag
val last_variant_tag : tag
type structured_constant =
- | Const_sorts of Sorts.t
+ | Const_sort of Sorts.t
| Const_ind of inductive
| Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
| Const_univ_level of Univ.Level.t
- | Const_type of Univ.Universe.t
val pp_struct_const : structured_constant -> Pp.t
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 3104d5751..0d7619e9f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -480,23 +480,23 @@ let rec compile_lam env reloc lam sz cont =
(Const_ind ind) (Univ.Instance.to_array u) sz cont
| Lsort (Sorts.Prop _ as s) ->
- compile_structured_constant reloc (Const_sorts s) sz cont
+ 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
+ (* 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_sorts (Sorts.Type u)) sz cont
+ compile_structured_constant reloc (Const_sort (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_structured_constant compile_get_univ reloc
- (Const_type u) (Array.of_list s) sz cont
+ (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
end
| Llet (id,def,body) ->
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 856b0b465..32d5387b2 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -350,7 +350,7 @@ type to_patch = emitcodes * patches * fv
(* Substitution *)
let rec subst_strcst s sc =
match sc with
- | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc
+ | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
| Const_proj p -> Const_proj (subst_constant s p)
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8c7658147..ad9aa4267 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -44,7 +44,6 @@ let rec conv_val env pb k v1 v2 cu =
and conv_whd env pb k whd1 whd2 cu =
(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
match whd1, whd2 with
- | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
| Vuniv_level _ , _
| _ , Vuniv_level _ ->
(** Both of these are invalid since universes are handled via
@@ -81,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu =
(* on the fly eta expansion *)
conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
- | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
+ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
| Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
@@ -119,8 +118,9 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
- | Atype _ , _ | _, Atype _ -> assert false
- | Aind _, _ | Aid _, _ -> raise NotConvertible
+ | Asort s1, Asort s2 ->
+ sort_cmp_universes env pb s1 s2 cu
+ | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible
and conv_stack env k stk1 stk2 cu =
match stk1, stk2 with
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 352ea74a4..f0bae98dc 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -168,7 +168,7 @@ let rec apply_stack a stk v =
let apply_whd k whd =
let v = val_of_rel k in
match whd with
- | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
+ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
| Vfun f -> reduce_fun k f
| Vfix(f, None) ->
push_ra stop;
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 2d8a1d976..2a784fdf4 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -121,7 +121,7 @@ type vswitch = {
type atom =
| Aid of Vars.id_key
| Aind of inductive
- | Atype of Univ.Universe.t
+ | Asort of Sorts.t
(* Zippers *)
@@ -136,7 +136,6 @@ type stack = zipper list
type to_update = values
type whd =
- | Vsort of Sorts.t
| Vprod of vprod
| Vfun of vfun
| Vfix of vfix * arguments option
@@ -167,7 +166,6 @@ let uni_lvl_val (v : values) : Univ.Level.t =
let pr =
let open Pp in
match whd with
- | Vsort _ -> str "Vsort"
| Vprod _ -> str "Vprod"
| Vfun _ -> str "Vfun"
| Vfix _ -> str "Vfix"
@@ -189,12 +187,17 @@ let rec whd_accu a stk =
match Obj.tag at with
| i when Int.equal i type_atom_tag ->
begin match stk with
+ | [] -> Vatom_stk(Obj.magic at, stk)
| [Zapp args] ->
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)
+ let s = Obj.obj (Obj.field at 0) in
+ begin match s with
+ | Type u ->
+ let inst = Instance.of_array (Array.map uni_lvl_val args) in
+ let u = Univ.subst_instance_universe inst u in
+ Vatom_stk (Asort (Type u), [])
+ | _ -> assert false
+ end
| _ -> assert false
end
| i when i <= max_atom_tag ->
@@ -243,11 +246,8 @@ let whd_val : values -> whd =
else
let tag = Obj.tag o in
if tag = accu_tag then
- (
- if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
- else
- if is_accumulate (fun_code o) then whd_accu o []
- else Vprod(Obj.obj o))
+ if is_accumulate (fun_code o) then whd_accu o []
+ else Vprod(Obj.obj o)
else
if tag = Obj.closure_tag || tag = Obj.infix_tag then
(match kind_of_closure o with
@@ -273,7 +273,7 @@ let obj_of_atom : atom -> Obj.t =
(* obj_of_str_const : structured_constant -> Obj.t *)
let rec obj_of_str_const str =
match str with
- | Const_sorts s -> Obj.repr (Vsort s)
+ | Const_sort s -> obj_of_atom (Asort s)
| Const_ind ind -> obj_of_atom (Aind ind)
| Const_proj p -> Obj.repr p
| Const_b0 tag -> Obj.repr tag
@@ -285,7 +285,6 @@ let rec obj_of_str_const str =
done;
res
| Const_univ_level l -> Obj.repr (Vuniv_level l)
- | Const_type u -> obj_of_atom (Atype u)
let val_of_obj o = ((Obj.obj o) : values)
@@ -502,10 +501,9 @@ let rec pr_atom a =
| RelKey i -> str "#" ++ int i
| _ -> str "...") ++ str ")"
| Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")"
- | Atype _ -> str "Atype(")
+ | Asort _ -> str "Asort(")
and pr_whd w =
Pp.(match w with
- | Vsort _ -> str "Vsort"
| Vprod _ -> str "Vprod"
| Vfun _ -> str "Vfun"
| Vfix _ -> str "Vfix"
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 350f71372..570e3606a 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -57,7 +57,7 @@ val cofix_upd_code : to_update -> tcode
type atom =
| Aid of Vars.id_key
| Aind of inductive
- | Atype of Univ.Universe.t
+ | Asort of Sorts.t
(** Zippers *)
@@ -70,7 +70,6 @@ type zipper =
type stack = zipper list
type whd =
- | Vsort of Sorts.t
| Vprod of vprod
| Vfun of vfun
| Vfix of vfix * arguments option
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c93b41786..6b7ea2996 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -141,7 +141,6 @@ and nf_vtype env sigma v = nf_val env sigma v crazy_type
and nf_whd env sigma whd typ =
match whd with
- | Vsort s -> mkSort s
| Vprod p ->
let dom = nf_vtype env sigma (dom p) in
let name = Name (Id.of_string "x") in
@@ -182,7 +181,8 @@ and nf_whd env sigma whd typ =
let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
in
nf_univ_args ~nb_univs mk env sigma stk
- | Vatom_stk(Atype u, stk) -> assert false
+ | Vatom_stk(Asort s, stk) ->
+ assert (List.is_empty stk); mkSort s
| Vuniv_level lvl ->
assert false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:53:21 +0000