Remove unchecked arithmetic operations from VM, as they are not used.

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]=

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,19 +1596,13 @@ 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;
       }
 
       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;
       }

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";

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 () ++

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
 

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

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
 

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 *)

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