(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** List of opcodes.

    It is used to generate the files [coq_instruct.h], [coq_jumptbl.h],
    [coq_arity.h], and [vmopcodes.ml].

    [STOP] needs to be the last opcode.

    Arity -1 designates opcodes that need special handling in [coq_fix_code.c].
*)
let opcodes =
  [|
    "ACC0", 0;
    "ACC1", 0;
    "ACC2", 0;
    "ACC3", 0;
    "ACC4", 0;
    "ACC5", 0;
    "ACC6", 0;
    "ACC7", 0;
    "ACC", 1;
    "PUSH", 0;
    "PUSHACC1", 0;
    "PUSHACC2", 0;
    "PUSHACC3", 0;
    "PUSHACC4", 0;
    "PUSHACC5", 0;
    "PUSHACC6", 0;
    "PUSHACC7", 0;
    "PUSHACC", 1;
    "POP", 1;
    "ENVACC0", 0;
    "ENVACC1", 0;
    "ENVACC2", 0;
    "ENVACC3", 0;
    "ENVACC", 1;
    "PUSHENVACC0", 0;
    "PUSHENVACC1", 0;
    "PUSHENVACC2", 0;
    "PUSHENVACC3", 0;
    "PUSHENVACC", 1;
    "PUSH_RETADDR", 1;
    "APPLY", 1;
    "APPLY1", 0;
    "APPLY2", 0;
    "APPLY3", 0;
    "APPLY4", 0;
    "APPTERM", 2;
    "APPTERM1", 1;
    "APPTERM2", 1;
    "APPTERM3", 1;
    "RETURN", 1;
    "RESTART", 0;
    "GRAB", 1;
    "GRABREC", 1;
    "CLOSURE", 2;
    "CLOSUREREC", -1;
    "CLOSURECOFIX", -1;
    "OFFSETCLOSURE0", 0;
    "OFFSETCLOSURE1", 0;
    "OFFSETCLOSURE", 1;
    "PUSHOFFSETCLOSURE0", 0;
    "PUSHOFFSETCLOSURE1", 0;
    "PUSHOFFSETCLOSURE", 1;
    "GETGLOBAL", 1;
    "PUSHGETGLOBAL", 1;
    "MAKEBLOCK", 2;
    "MAKEBLOCK1", 1;
    "MAKEBLOCK2", 1;
    "MAKEBLOCK3", 1;
    "MAKEBLOCK4", 1;
    "SWITCH", -1;
    "PUSHFIELDS", 1;
    "GETFIELD0", 0;
    "GETFIELD1", 0;
    "GETFIELD", 1;
    "SETFIELD", 1;
    "PROJ", 2;
    "ENSURESTACKCAPACITY", 1;
    "CONST0", 0;
    "CONST1", 0;
    "CONST2", 0;
    "CONST3", 0;
    "CONSTINT", 1;
    "PUSHCONST0", 0;
    "PUSHCONST1", 0;
    "PUSHCONST2", 0;
    "PUSHCONST3", 0;
    "PUSHCONSTINT", 1;
    "ACCUMULATE", 0;
    "MAKESWITCHBLOCK", 4;
    "MAKEACCU", 1;
    "BRANCH", 1;
    "CHECKADDINT63", 1;
    "CHECKADDCINT63", 1;
    "CHECKADDCARRYCINT63", 1;
    "CHECKSUBINT63", 1;
    "CHECKSUBCINT63", 1;
    "CHECKSUBCARRYCINT63", 1;
    "CHECKMULINT63", 1;
    "CHECKMULCINT63", 1;
    "CHECKDIVINT63", 1;
    "CHECKMODINT63", 1;
    "CHECKDIVEUCLINT63", 1;
    "CHECKDIV21INT63", 1;
    "CHECKLXORINT63", 1;
    "CHECKLORINT63", 1;
    "CHECKLANDINT63", 1;
    "CHECKLSLINT63", 1;
    "CHECKLSRINT63", 1;
    "CHECKADDMULDIVINT63", 1;
    "CHECKEQINT63", 1;
    "CHECKLTINT63", 1;
    "CHECKLEINT63", 1;
    "CHECKCOMPAREINT63", 1;
    "CHECKHEAD0INT63", 1;
    "CHECKTAIL0INT63", 1;
    "CHECKOPPFLOAT", 1;
    "CHECKABSFLOAT", 1;
    "CHECKEQFLOAT", 1;
    "CHECKLTFLOAT", 1;
    "CHECKLEFLOAT", 1;
    "CHECKCOMPAREFLOAT", 1;
    "CHECKCLASSIFYFLOAT", 1;
    "CHECKADDFLOAT", 1;
    "CHECKSUBFLOAT", 1;
    "CHECKMULFLOAT", 1;
    "CHECKDIVFLOAT", 1;
    "CHECKSQRTFLOAT", 1;
    "CHECKFLOATOFINT63", 1;
    "CHECKFLOATNORMFRMANTISSA", 1;
    "CHECKFRSHIFTEXP", 1;
    "CHECKLDSHIFTEXP", 1;
    "CHECKNEXTUPFLOAT", 1;
    "CHECKNEXTDOWNFLOAT", 1;
    "CHECKNEXTUPFLOATINPLACE", 1;
    "CHECKNEXTDOWNFLOATINPLACE", 1;
    "CHECKCAMLCALL2_1", 2;
    "CHECKCAMLCALL1", 2;
    "CHECKCAMLCALL2", 2;
    "CHECKCAMLCALL3_1", 2;
    "STOP", 0
  |]

let pp_c_comment fmt =
  Format.fprintf fmt "/* %s */"

let pp_ocaml_comment fmt =
  Format.fprintf fmt "(* %s *)"

let pp_header isOcaml fmt =
  Format.fprintf fmt "%a"
    (if isOcaml then pp_ocaml_comment else pp_c_comment)
    "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml"

let pp_coq_instruct_h fmt =
  pp_header false fmt;
  Format.fprintf fmt "#pragma once@.enum instructions {@.";
  Array.iter (fun (name, _) ->
      Format.fprintf fmt "  %s,@." name
    ) opcodes;
  Format.fprintf fmt "};@."

let pp_coq_jumptbl_h fmt =
  pp_header false fmt;
  Array.iter (fun (name, _) ->
      Format.fprintf fmt "  &&coq_lbl_%s,@." name
    ) opcodes

let pp_coq_arity_h fmt =
  pp_header false fmt;
  Format.fprintf fmt "static signed char arity2[] = {@.";
  Array.iter (fun (_, arity) ->
      Format.fprintf fmt "  %d,@." arity
    ) opcodes;
  Format.fprintf fmt "};@."

let pp_vmopcodes_ml fmt =
  pp_header true fmt;
  Array.iteri (fun n s ->
      Format.fprintf fmt "let op%s = %d@.@." s n
    ) (Array.map fst opcodes)

let usage () =
  Format.eprintf "usage: %s [enum|jump|arity|copml]@." Sys.argv.(0);
  exit 1

let main () =
  match Sys.argv.(1) with
  | "enum" -> pp_coq_instruct_h Format.std_formatter
  | "jump" -> pp_coq_jumptbl_h Format.std_formatter
  | "arity" -> pp_coq_arity_h Format.std_formatter
  | "copml" -> pp_vmopcodes_ml Format.std_formatter
  | _ -> usage ()
  | exception Invalid_argument _ -> usage ()

let () = main ()