aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c11
-rw-r--r--kernel/byterun/coq_values.h6
-rw-r--r--kernel/cClosure.ml55
-rw-r--r--kernel/cPrimitives.ml6
-rw-r--r--kernel/cPrimitives.mli2
-rw-r--r--kernel/float64.ml10
-rw-r--r--kernel/float64.mli2
-rw-r--r--kernel/primred.ml30
-rw-r--r--kernel/primred.mli8
-rw-r--r--kernel/retroknowledge.ml6
-rw-r--r--kernel/retroknowledge.mli4
-rw-r--r--kernel/safe_typing.ml31
-rw-r--r--kernel/typeops.ml12
13 files changed, 95 insertions, 88 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 55b973dcdb..74edd79872 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1551,19 +1551,16 @@ value coq_interprete
x = Double_val(accu);
y = Double_val(*sp++);
if(x < y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Lt;
+ accu = coq_FLt;
}
else if(x > y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Gt;
+ accu = coq_FGt;
}
else if(x == y) {
- Alloc_small(accu, 1, coq_tag_Some);
- Field(accu, 0) = coq_Eq;
+ accu = coq_FEq;
}
else { // nan value
- accu = coq_None;
+ accu = coq_FNotComparable;
}
Next;
}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index fa51b2d31f..c79a8f1b4f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -42,8 +42,10 @@
#define coq_Eq Val_int(0)
#define coq_Lt Val_int(1)
#define coq_Gt Val_int(2)
-#define coq_tag_Some 1
-#define coq_None Val_int(0)
+#define coq_FEq Val_int(0)
+#define coq_FLt Val_int(1)
+#define coq_FGt Val_int(2)
+#define coq_FNotComparable Val_int(3)
#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5f0da5da65..77352595f1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1052,17 +1052,22 @@ module FNativeEntries =
fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
| None -> defined_cmp := false
- let defined_option = ref false
- let fSome = ref dummy
- let fNone = ref dummy
-
- let init_option retro =
- match retro.Retroknowledge.retro_option with
- | Some (cSome, cNone) ->
- defined_option := true;
- fSome := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cSome) };
- fNone := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNone) }
- | None -> defined_option := false
+ let defined_f_cmp = ref false
+ let fFEq = ref dummy
+ let fFLt = ref dummy
+ let fFGt = ref dummy
+ let fFNotComparable = ref dummy
+
+ let init_f_cmp retro =
+ match retro.Retroknowledge.retro_f_cmp with
+ | Some (cFEq, cFLt, cFGt, cFNotComparable) ->
+ defined_f_cmp := true;
+ fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) };
+ fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) };
+ fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) };
+ fFNotComparable :=
+ { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) };
+ | None -> defined_f_cmp := false
let defined_refl = ref false
@@ -1083,7 +1088,7 @@ module FNativeEntries =
init_carry !current_retro;
init_pair !current_retro;
init_cmp !current_retro;
- init_option !current_retro;
+ init_f_cmp !current_retro;
init_refl !current_retro
let check_env env =
@@ -1113,9 +1118,9 @@ module FNativeEntries =
check_env env;
assert (!defined_cmp)
- let check_option env =
+ let check_f_cmp env =
check_env env;
- assert (!defined_option)
+ assert (!defined_f_cmp)
let mkInt env i =
check_int env;
@@ -1155,15 +1160,21 @@ module FNativeEntries =
check_cmp env;
!fGt
- let mkSomeCmp env v =
- check_cmp env;
- check_option env;
- { mark = mark Cstr KnownR; term = FApp(!fSome, [|!fcmp;v|]) }
+ let mkFLt env =
+ check_f_cmp env;
+ !fFLt
- let mkNoneCmp env =
- check_cmp env;
- check_option env;
- { mark = mark Cstr KnownR; term = FApp(!fNone, [|!fcmp|]) }
+ let mkFEq env =
+ check_f_cmp env;
+ !fFEq
+
+ let mkFGt env =
+ check_f_cmp env;
+ !fFGt
+
+ let mkFNotComparable env =
+ check_f_cmp env;
+ !fFNotComparable
end
module FredNative = RedNative(FNativeEntries)
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 3154ee8c75..d5ed2c1a06 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -135,7 +135,7 @@ type 'a prim_ind =
| PIT_carry : prim_type prim_ind
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
- | PIT_option : unit prim_ind
+ | PIT_f_cmp : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
@@ -165,7 +165,7 @@ let types =
| Float64ofInt63 -> [int_ty; float_ty]
| Float64normfr_mantissa -> [float_ty; int_ty]
| Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))]
- | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())]
+ | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
| Float64add | Float64sub | Float64mul
| Float64div -> [float_ty; float_ty; float_ty]
| Float64ldshiftexp -> [float_ty; int_ty; float_ty]
@@ -197,7 +197,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with
| PIT_carry -> "carry"
| PIT_pair -> "pair"
| PIT_cmp -> "cmp"
- | PIT_option -> "option"
+ | PIT_f_cmp -> "f_cmp"
let prim_type_to_string = function
| PT_int63 -> "int63_type"
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index f9424fb09d..3e6ec8dbcc 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -74,7 +74,7 @@ type 'a prim_ind =
| PIT_carry : prim_type prim_ind
| PIT_pair : (prim_type * prim_type) prim_ind
| PIT_cmp : unit prim_ind
- | PIT_option : unit prim_ind
+ | PIT_f_cmp : unit prim_ind
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
diff --git a/kernel/float64.ml b/kernel/float64.ml
index a625c0f551..eebc8f35ef 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -24,17 +24,17 @@ let of_float f = f
let opp = ( ~-. )
let abs = abs_float
-type float_comparison = Eq | Lt | Gt | NotComparable
+type float_comparison = FEq | FLt | FGt | FNotComparable
let compare x y =
- if x < y then Lt
+ if x < y then FLt
else
(
- if x > y then Gt
+ if x > y then FGt
else
(
- if x = y then Eq
- else NotComparable (* NaN case *)
+ if x = y then FEq
+ else FNotComparable (* NaN case *)
)
)
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 7ced535dc0..c82f1d84da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -24,7 +24,7 @@ val of_float : float -> t
val opp : t -> t
val abs : t -> t
-type float_comparison = Eq | Lt | Gt | NotComparable
+type float_comparison = FEq | FLt | FGt | FNotComparable
(** The IEEE 754 float comparison.
* NotComparable is returned if there is a NaN in the arguments *)
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 1b9badfca9..5fe700cb9a 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -49,12 +49,12 @@ let add_retroknowledge env action =
| None -> ((ind,1), (ind,2), (ind,3))
| Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_cmp = Some r }
- | PIT_option ->
+ | PIT_f_cmp ->
let r =
- match retro.retro_option with
- | None -> ((ind,1), (ind,2))
- | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
- { retro with retro_option = Some 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
+ { retro with retro_f_cmp = Some r }
in
set_retroknowledge env retro
@@ -94,10 +94,10 @@ let get_cmp_constructors env =
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
-let get_option_constructors env =
- match env.retroknowledge.retro_option with
+let get_f_cmp_constructors env =
+ match env.retroknowledge.retro_f_cmp with
| Some r -> r
- | None -> anomaly Pp.(str"Reduction of primitive: option not registered")
+ | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
exception NativeDestKO
@@ -119,8 +119,10 @@ module type RedNativeEntries =
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
- val mkSomeCmp : env -> elem -> elem
- val mkNoneCmp : env -> elem
+ val mkFLt : env -> elem
+ val mkFEq : env -> elem
+ val mkFGt : env -> elem
+ val mkFNotComparable : env -> elem
end
module type RedNative =
@@ -239,10 +241,10 @@ struct
| Float64compare ->
let f1, f2 = get_float2 evd args in
(match Float64.compare f1 f2 with
- | Float64.Eq -> E.mkSomeCmp env (E.mkEq env)
- | Float64.Lt -> E.mkSomeCmp env (E.mkLt env)
- | Float64.Gt -> E.mkSomeCmp env (E.mkGt env)
- | Float64.NotComparable -> E.mkNoneCmp env)
+ | Float64.FEq -> E.mkFEq env
+ | Float64.FLt -> E.mkFLt env
+ | Float64.FGt -> E.mkFGt env
+ | Float64.FNotComparable -> E.mkFNotComparable env)
| Float64add ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
| Float64sub ->
diff --git a/kernel/primred.mli b/kernel/primred.mli
index b2c9ebc6ea..5531c81550 100644
--- a/kernel/primred.mli
+++ b/kernel/primred.mli
@@ -11,7 +11,7 @@ val get_bool_constructors : env -> constructor * constructor
val get_carry_constructors : env -> constructor * constructor
val get_pair_constructor : env -> constructor
val get_cmp_constructors : env -> constructor * constructor * constructor
-val get_option_constructors : env -> constructor * constructor
+val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
exception NativeDestKO (* Should be raised by get_* functions on failure *)
@@ -33,8 +33,10 @@ module type RedNativeEntries =
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
- val mkSomeCmp : env -> elem -> elem
- val mkNoneCmp : env -> elem
+ val mkFLt : env -> elem
+ val mkFEq : env -> elem
+ val mkFGt : env -> elem
+ val mkFNotComparable : env -> elem
end
module type RedNative =
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index a84353bdc6..e897be6141 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -24,7 +24,9 @@ type retroknowledge = {
retro_pair : constructor option;
retro_cmp : (constructor * constructor * constructor) option;
(* Eq, Lt, Gt *)
- retro_option : (constructor * constructor) option; (* Some, None *)
+ retro_f_cmp : (constructor * constructor * constructor * constructor)
+ option;
+ (* FEq, FLt, FGt, FNotComparable *)
retro_refl : constructor option;
}
@@ -35,7 +37,7 @@ let empty = {
retro_carry = None;
retro_pair = None;
retro_cmp = None;
- retro_option = None;
+ retro_f_cmp = None;
retro_refl = None;
}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0aca296d29..7aaf14e176 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -18,7 +18,9 @@ type retroknowledge = {
retro_pair : constructor option;
retro_cmp : (constructor * constructor * constructor) option;
(* Eq, Lt, Gt *)
- retro_option : (constructor * constructor) option; (* Some, None *)
+ retro_f_cmp : (constructor * constructor * constructor * constructor)
+ option;
+ (* FEq, FLt, FGt, FNotComparable *)
retro_refl : constructor option;
}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 000f6125a6..241ee8ada3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1403,27 +1403,16 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env =
check_type_cte 1;
check_name 2 "Gt";
check_type_cte 2
- | CPrimitives.PIT_option ->
- check_nconstr 2;
- check_name 0 "Some";
- let cSome = ob.mind_user_lc.(0) in
- let s = Pp.str "the first option constructor (Some) has a wrong type" in
- begin match Term.decompose_prod cSome with
- | ([_,v;_,_V], codom) ->
- check_if (is_Type _V) s;
- check_if (Constr.equal v (mkRel 1)) s;
- check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s
- | _ -> check_if false s
- end;
- check_name 1 "None";
- let cNone = ob.mind_user_lc.(1) in
- let s = Pp.str "the second option constructor (None) has a wrong type" in
- begin match Term.decompose_prod cNone with
- | ([_,_V], codom) ->
- check_if (is_Type _V) s;
- check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s
- | _ -> check_if false s
- end
+ | CPrimitives.PIT_f_cmp ->
+ check_nconstr 4;
+ check_name 0 "FEq";
+ check_type_cte 0;
+ check_name 1 "FLt";
+ check_type_cte 1;
+ check_name 2 "FGt";
+ check_type_cte 2;
+ check_name 3 "FNotComparable";
+ check_type_cte 3
let register_inductive ind prim senv =
check_register_ind ind prim senv.env;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9913772f2..3e79b174b8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -241,16 +241,16 @@ let type_of_prim env t =
| Some ((ind,_),_,_) -> Constr.mkInd ind
| None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.")
in
+ let f_compare_ty () =
+ match env.retroknowledge.Retroknowledge.retro_f_cmp with
+ | Some ((ind,_),_,_,_) -> Constr.mkInd ind
+ | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.")
+ in
let pair_ty fst_ty snd_ty =
match env.retroknowledge.Retroknowledge.retro_pair with
| Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|])
| None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.")
in
- let option_ty ty =
- match env.retroknowledge.Retroknowledge.retro_option with
- | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|])
- | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.")
- in
let carry_ty int_ty =
match env.retroknowledge.Retroknowledge.retro_carry with
| Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|])
@@ -265,7 +265,7 @@ let type_of_prim env t =
| PIT_carry, t -> carry_ty (tr_prim_type t)
| PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2)
| PIT_cmp, () -> compare_ty ()
- | PIT_option, () -> option_ty (compare_ty ()) in
+ | PIT_f_cmp, () -> f_compare_ty () in
let tr_type = function
| PITT_ind (i, a) -> tr_ind i a
| PITT_type t -> tr_prim_type t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:27:28 +0000