aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_interp.c18
-rw-r--r--kernel/genOpcodeFiles.ml6
-rw-r--r--kernel/vmbytecodes.ml4
-rw-r--r--kernel/vmbytecodes.mli2
-rw-r--r--kernel/vmbytegen.ml2
-rw-r--r--kernel/vmemitcodes.ml13
-rw-r--r--kernel/vmlambda.ml12
-rw-r--r--kernel/vmlambda.mli3
9 files changed, 9 insertions, 53 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 9118410549..cd431dbf2e 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -43,8 +43,6 @@ void init_arity () {
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
- arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
- arity[LTFLOAT]=arity[LEFLOAT]=
arity[ISINT]=arity[AREINT2]=0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 3bee36b667..74eb4973d0 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1271,11 +1271,8 @@ value coq_interprete
Instruct(CHECKADDINT63){
print_instr("CHECKADDINT63");
CheckInt2();
- }
- Instruct(ADDINT63) {
/* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
- print_instr("ADDINT63");
Uint63_add(accu, *sp++);
Next;
}
@@ -1309,9 +1306,6 @@ value coq_interprete
Instruct (CHECKSUBINT63) {
print_instr("CHECKSUBINT63");
CheckInt2();
- }
- Instruct (SUBINT63) {
- print_instr("SUBINT63");
/* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
@@ -1517,9 +1511,6 @@ value coq_interprete
Instruct (CHECKLTINT63) {
print_instr("CHECKLTINT63");
CheckInt2();
- }
- Instruct (LTINT63) {
- print_instr("LTINT63");
int b;
Uint63_lt(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1529,9 +1520,6 @@ value coq_interprete
Instruct (CHECKLEINT63) {
print_instr("CHECKLEINT63");
CheckInt2();
- }
- Instruct (LEINT63) {
- print_instr("LEINT63");
int b;
Uint63_leq(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1608,9 +1596,6 @@ value coq_interprete
Instruct (CHECKLTFLOAT) {
print_instr("CHECKLTFLOAT");
CheckFloat2();
- }
- Instruct (LTFLOAT) {
- print_instr("LTFLOAT");
accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
Next;
}
@@ -1618,9 +1603,6 @@ value coq_interprete
Instruct (CHECKLEFLOAT) {
print_instr("CHECKLEFLOAT");
CheckFloat2();
- }
- Instruct (LEFLOAT) {
- print_instr("LEFLOAT");
accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
Next;
}
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index f052e03cde..b48084109b 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -104,11 +104,9 @@ let opcodes =
"MAKEPROD";
"BRANCH";
"CHECKADDINT63";
- "ADDINT63";
"CHECKADDCINT63";
"CHECKADDCARRYCINT63";
"CHECKSUBINT63";
- "SUBINT63";
"CHECKSUBCINT63";
"CHECKSUBCARRYCINT63";
"CHECKMULINT63";
@@ -127,9 +125,7 @@ let opcodes =
"CHECKLSRINT63CONST1";
"CHECKEQINT63";
"CHECKLTINT63";
- "LTINT63";
"CHECKLEINT63";
- "LEINT63";
"CHECKCOMPAREINT63";
"CHECKHEAD0INT63";
"CHECKTAIL0INT63";
@@ -139,9 +135,7 @@ let opcodes =
"CHECKABSFLOAT";
"CHECKEQFLOAT";
"CHECKLTFLOAT";
- "LTFLOAT";
"CHECKLEFLOAT";
- "LEFLOAT";
"CHECKCOMPAREFLOAT";
"CHECKCLASSIFYFLOAT";
"CHECKADDFLOAT";
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c156a21c86..a1dea977cd 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -60,7 +60,7 @@ type instruction =
| Kproj of Projection.Repr.t
| Kensurestackcapacity of int
| Kbranch of Label.t (* jump to label *)
- | Kprim of CPrimitives.t * pconstant option
+ | Kprim of CPrimitives.t * pconstant
| Kcamlprim of CPrimitives.t * Label.t
| Kareint of int
@@ -146,7 +146,7 @@ let rec pp_instr i =
| Kensurestackcapacity size -> str "growstack " ++ int size
| Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++
- (match id with Some (id,_u) -> Constant.print id | None -> str "")
+ (Constant.print (fst id))
| Kcamlprim (op, lbl) ->
str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index b703058fb7..33071b917b 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -59,7 +59,7 @@ type instruction =
| Kensurestackcapacity of int
| Kbranch of Label.t (** jump to label, is it needed ? *)
- | Kprim of CPrimitives.t * pconstant option
+ | Kprim of CPrimitives.t * pconstant
| Kcamlprim of CPrimitives.t * Label.t
| Kareint of int
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 16a0f42664..6899ebe1a6 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -770,7 +770,7 @@ let rec compile_lam env cenv lam sz cont =
let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
comp_args (compile_lam env) cenv args sz cont
- | Lprim (Some (kn,u), op, args) when is_caml_prim op ->
+ | Lprim ((kn,u), op, args) when is_caml_prim op ->
let arity = CPrimitives.arity op in
let nparams = CPrimitives.nparams op in
let nargs = arity - nparams in
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index babc57794b..d0422dd324 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -208,14 +208,6 @@ let slot_for_caml_prim env op =
(* Emission of one instruction *)
-let nocheck_prim_op = function
- | Int63add -> opADDINT63
- | Int63sub -> opSUBINT63
- | Int63lt -> opLTINT63
- | Int63le -> opLEINT63
- | _ -> assert false
-
-
let check_prim_op = function
| Int63head0 -> opCHECKHEAD0INT63
| Int63tail0 -> opCHECKTAIL0INT63
@@ -354,10 +346,7 @@ let emit_instr env = function
| Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
| Kbranch lbl -> out env opBRANCH; out_label env lbl
- | Kprim (op,None) ->
- out env (nocheck_prim_op op)
-
- | Kprim(op,Some (q,_u)) ->
+ | Kprim (op, (q,_u)) ->
out env (check_prim_op op);
slot_for_getglobal env q
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 332a331a7a..cd7c9b015f 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -19,8 +19,7 @@ type lambda =
| Llet of Name.t Context.binder_annot * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of pconstant
- | Lprim of pconstant option * CPrimitives.t * lambda array
- (* No check if None *)
+ | Lprim of pconstant * CPrimitives.t * lambda array
| Lcase of case_info * reloc_table * lambda * lambda * lam_branches
| Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
@@ -148,16 +147,11 @@ let rec pp_lam lam =
| Lval _ -> str "values"
| Lsort s -> pp_sort s
| Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
- | Lprim(Some (kn,_u),_op,args) ->
+ | Lprim ((kn,_u),_op,args) ->
hov 1
(str "(PRIM " ++ pr_con kn ++ spc() ++
prlist_with_sep spc pp_lam (Array.to_list args) ++
str")")
- | Lprim(None,op,args) ->
- hov 1
- (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++
- prlist_with_sep spc pp_lam (Array.to_list args) ++
- str")")
| Lproj(p,arg) ->
hov 1
(str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
@@ -566,7 +560,7 @@ let rec get_alias env kn =
(* Compilation of primitive *)
let prim kn p args =
- Lprim(Some kn, p, args)
+ Lprim (kn, p, args)
let expand_prim kn op arity =
(* primitives are always Relevant *)
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
index bd11c2667f..8ae7e05f72 100644
--- a/kernel/vmlambda.mli
+++ b/kernel/vmlambda.mli
@@ -12,8 +12,7 @@ type lambda =
| Llet of Name.t Context.binder_annot * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of pconstant
- | Lprim of pconstant option * CPrimitives.t * lambda array
- (* No check if None *)
+ | Lprim of pconstant * CPrimitives.t * lambda array
| Lcase of case_info * reloc_table * lambda * lambda * lam_branches
| Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:30:02 +0000