aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c2
-rw-r--r--kernel/byterun/coq_values.h1
-rw-r--r--kernel/cPrimitives.mli1
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cemitcodes.ml8
-rw-r--r--kernel/primred.ml77
-rw-r--r--kernel/primred.mli7
-rw-r--r--kernel/term_typing.ml16
-rw-r--r--kernel/vmvalues.ml20
-rw-r--r--kernel/vmvalues.mli3
10 files changed, 75 insertions, 62 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9921208e04..15cc451ea8 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1187,7 +1187,7 @@ value coq_interprete
if (sz == 0) accu = Atom(0);
else {
Alloc_small(accu, sz, Default_tag);
- if (Field(*sp, 2) == Val_true) {
+ if (Is_tailrec_switch(*sp)) {
for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
}else{
for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 86ae6295fd..a19f9b56c1 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -32,6 +32,7 @@
#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#define Is_double(v) (Tag_val(v) == Double_tag)
+#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
/* coq array */
#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 5e5fad9f04..41b3bff465 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -128,6 +128,7 @@ 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
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7bff377238..bacc308e1f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont =
done;
let annot =
- {ci = ci; rtbl = rtbl; tailcall = is_tailcall;
+ {rtbl = rtbl; tailcall = is_tailcall;
max_stack_size = !max_stack_size - sz}
in
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6b4daabf0c..ed475dca7e 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -13,7 +13,6 @@
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
open Names
-open Constr
open Vmvalues
open Cbytecodes
open Copcodes
@@ -424,12 +423,11 @@ let subst_strcst s sc =
| Const_float _ -> sc
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
+let subst_annot _ (a : annot_switch) = a
+
let subst_reloc s ri =
match ri with
- | Reloc_annot a ->
- let (kn,i) = a.ci.ci_ind in
- let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
- Reloc_annot {a with ci = ci}
+ | Reloc_annot a -> Reloc_annot (subst_annot s a)
| Reloc_const sc -> Reloc_const (subst_strcst s sc)
| Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
| Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 10a8da8813..90eeeb9be7 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -5,62 +5,71 @@ open Retroknowledge
open Environ
open CErrors
-let add_retroknowledge env action =
+type _ action_kind =
+ | IncompatTypes : _ prim_type -> Constant.t action_kind
+ | IncompatInd : _ prim_ind -> inductive action_kind
+
+type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
+
+let check_same_types typ c1 c2 =
+ if not (Constant.equal c1 c2)
+ then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
+
+let check_same_inds ind i1 i2 =
+ if not (eq_ind i1 i2)
+ then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
+
+let add_retroknowledge retro action =
match action with
- | Register_type(PT_int63,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_int63 with
- | None -> { retro with retro_int63 = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
- | Register_type(PT_float64,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_float64 with
- | None -> { retro with retro_float64 = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
- | Register_type(PT_array,c) ->
- let retro = env.retroknowledge in
- let retro =
- match retro.retro_array with
- | None -> { retro with retro_array = Some c }
- | Some c' -> assert (Constant.equal c c'); retro in
- set_retroknowledge env retro
+ | Register_type(typ,c) ->
+ begin match typ with
+ | PT_int63 ->
+ (match retro.retro_int63 with
+ | None -> { retro with retro_int63 = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+
+ | PT_float64 ->
+ (match retro.retro_float64 with
+ | None -> { retro with retro_float64 = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+
+ | PT_array ->
+ (match retro.retro_array with
+ | None -> { retro with retro_array = Some c }
+ | Some c' -> check_same_types typ c c'; retro)
+ end
+
| Register_ind(pit,ind) ->
- let retro = env.retroknowledge in
- let retro =
- match pit with
+ begin match pit with
| PIT_bool ->
let r =
match retro.retro_bool with
| None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_bool = Some r }
| PIT_carry ->
let r =
match retro.retro_carry with
| None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_carry = Some r }
| PIT_pair ->
let r =
match retro.retro_pair with
| None -> (ind,1)
- | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in
+ | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_pair = Some r }
| PIT_cmp ->
let r =
match retro.retro_cmp with
| None -> ((ind,1), (ind,2), (ind,3))
- | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_cmp = Some r }
| PIT_f_cmp ->
let r =
match retro.retro_f_cmp with
| None -> ((ind,1), (ind,2), (ind,3), (ind,4))
- | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
+ | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_f_cmp = Some r }
| PIT_f_class ->
let r =
@@ -69,10 +78,12 @@ let add_retroknowledge env action =
(ind,5), (ind,6), (ind,7), (ind,8),
(ind,9))
| Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
- assert (eq_ind ind ind'); t in
+ check_same_inds pit ind ind'; t in
{ retro with retro_f_class = Some r }
- in
- set_retroknowledge env retro
+ end
+
+let add_retroknowledge env action =
+ set_retroknowledge env (add_retroknowledge env.retroknowledge action)
let get_int_type env =
match env.retroknowledge.retro_int63 with
diff --git a/kernel/primred.mli b/kernel/primred.mli
index 1bfaffaa44..6e9d4e297e 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -2,6 +2,13 @@ open Names
open Environ
(** {5 Reduction of primitives} *)
+type _ action_kind =
+ | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind
+ | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind
+
+type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
+
+(** May raise [IncomtibleDeclarations] *)
val add_retroknowledge : env -> Retroknowledge.action -> env
val get_int_type : env -> Constant.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 04e7a81697..48567aa564 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
univs, typ
| Some (typ,Monomorphic_entry uctx) ->
- assert (AUContext.is_empty auctx);
+ assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *)
let env = push_context_set ~strict:true uctx env in
let u = Instance.empty in
let typ =
@@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } =
Monomorphic uctx, typ
| Some (typ,Polymorphic_entry (unames,uctx)) ->
- assert (not (AUContext.is_empty auctx));
- (* push_context will check that the universes aren't repeated in the instance
- so comparing the sizes works *)
- assert (AUContext.size auctx = UContext.size uctx);
- (* No polymorphic primitive uses constraints currently *)
- assert (Constraint.is_empty (UContext.constraints uctx));
+ assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *)
+ (* [push_context] will check that the universes aren't repeated in
+ the instance so comparing the sizes works. No polymorphic
+ primitive uses constraints currently. *)
+ if not (AUContext.size auctx = UContext.size uctx
+ && Constraint.is_empty (UContext.constraints uctx))
+ then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++
+ str (op_or_type_to_string p));
let env = push_context ~strict:false uctx env in
(* Now we know that uctx matches the auctx *)
let typ = (Typeops.infer_type env typ).utj_val in
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index ec429d5f9e..de604176cb 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
open Univ
-open Constr
(********************************************)
(* Initialization of the abstract machine ***)
@@ -61,8 +60,9 @@ type structured_constant =
type reloc_table = (tag * int) array
+(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *)
type annot_switch =
- {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+ { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
let rec eq_structured_values v1 v2 =
v1 == v2 ||
@@ -123,22 +123,16 @@ let hash_structured_constant c =
| Const_float f -> combinesmall 7 (Float64.hash f)
let eq_annot_switch asw1 asw2 =
- let eq_ci ci1 ci2 =
- eq_ind ci1.ci_ind ci2.ci_ind &&
- Int.equal ci1.ci_npar ci2.ci_npar &&
- CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
- in
let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
- eq_ci asw1.ci asw2.ci &&
CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
- (asw1.tailcall : bool) == asw2.tailcall
+ (asw1.tailcall : bool) == asw2.tailcall &&
+ Int.equal asw1.max_stack_size asw2.max_stack_size
let hash_annot_switch asw =
let open Hashset.Combine in
- let h1 = Constr.case_info_hash asw.ci in
- let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
- let h3 = if asw.tailcall then 1 else 0 in
- combine3 h1 h2 h3
+ let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+ let h2 = if asw.tailcall then 1 else 0 in
+ combine3 h1 h2 asw.max_stack_size
let pp_sort s =
let open Sorts in
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f4070a02a3..f6efd49cfc 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Constr
(** Values *)
@@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t
type reloc_table = (tag * int) array
type annot_switch =
- {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+ { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
val eq_structured_constant : structured_constant -> structured_constant -> bool
val hash_structured_constant : structured_constant -> int
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 11:35:26 +0000