[Kernel] Simpler generation of opcode files

Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.

3 files changed, 5 insertions, 72 deletions

diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
deleted file mode 100644
index c7abedaed6..0000000000
--- a/kernel/byterun/coq_instruct.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Coq Compiler                              */
-/*                                                                     */
-/*        Benjamin Gregoire, projets Logical and Cristal               */
-/*                        INRIA Rocquencourt                           */
-/*                                                                     */
-/*                                                                     */
-/***********************************************************************/
-
-#ifndef _COQ_INSTRUCT_
-#define _COQ_INSTRUCT_
-
-/* Nota: this list of instructions is parsed to produce derived files */
-/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase    */
-/* and alone on lines starting by two spaces.                         */
-/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c    */
-/* with the arity of the instruction and maybe coq_tcode_of_code.     */
-
-enum instructions {
-  ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
-  PUSH, 
-  PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
-  PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, 
-  POP,
-  ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
-  PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
-  PUSH_RETADDR,
-  APPLY, APPLY1, APPLY2, APPLY3, APPLY4,
-  APPTERM, APPTERM1, APPTERM2, APPTERM3,
-  RETURN, RESTART, GRAB, GRABREC, 
-  CLOSURE, CLOSUREREC, CLOSURECOFIX,
-  OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
-  PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, 
-  PUSHOFFSETCLOSURE,
-  GETGLOBAL, PUSHGETGLOBAL,
-  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4,
-  SWITCH, PUSHFIELDS, 
-  GETFIELD0, GETFIELD1, GETFIELD, 
-  SETFIELD0, SETFIELD1, SETFIELD,
-  PROJ,
-  ENSURESTACKCAPACITY,
-  CONST0, CONST1, CONST2, CONST3, CONSTINT,
-  PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
-  ACCUMULATE,
-  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
-/* spiwack: */
-  BRANCH,
-  CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63,
-  CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63,
-  CHECKMULINT63, CHECKMULCINT63,
-  CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63,
-  CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63,
-  CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63,
-  CHECKLSLINT63CONST1, CHECKLSRINT63CONST1,
-
-  CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63,
-  CHECKCOMPAREINT63,
-
-  CHECKHEAD0INT63, CHECKTAIL0INT63,
-
-  ISINT, AREINT2,
-
-  STOP
-};
-
-#endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index c3c44670be..20bdf28e54 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -5,6 +5,9 @@
  (c_names coq_fix_code coq_memory coq_values coq_interp))
 
 (rule
+ (targets coq_instruct.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))
+
+(rule
  (targets coq_jumptbl.h)
- (deps (:h-file coq_instruct.h) make_jumptbl.sh)
- (action (bash "./make_jumptbl.sh %{h-file} %{targets}")))
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh
deleted file mode 100755
index eacd4daac8..0000000000
--- a/kernel/byterun/make_jumptbl.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-
-sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2}