aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cPrimitives.mli1
-rw-r--r--kernel/primred.ml77
-rw-r--r--kernel/primred.mli7
-rw-r--r--kernel/term_typing.ml16
4 files changed, 61 insertions, 40 deletions
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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:23:39 +0000