From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 13:07:54 +0200
Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo

---
 kernel/cbytecodes.ml | 166 ---------------------------------------------------
 1 file changed, 166 deletions(-)
 delete mode 100644 kernel/cbytecodes.ml

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
deleted file mode 100644
index 74405a0105..0000000000
--- a/kernel/cbytecodes.ml
+++ /dev/null
@@ -1,166 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-(* Created by Bruno Barras for Benjamin Grégoire as part of the
-   bytecode-based reduction machine, Oct 2004 *)
-(* Support for native arithmetics by Arnaud Spiwack, May 2007 *)
-
-(* This file defines the type of bytecode instructions *)
-
-open Names
-open Vmvalues
-open Constr
-
-module Label =
-  struct
-    type t = int
-    let no = -1
-    let counter = ref no
-    let create () = incr counter; !counter
-    let reset_label_counter () = counter := no
-  end
-
-type instruction =
-  | Klabel of Label.t
-  | Kacc of int
-  | Kenvacc of int
-  | Koffsetclosure of int
-  | Kpush
-  | Kpop of int
-  | Kpush_retaddr of Label.t
-  | Kapply of int
-  | Kappterm of int * int
-  | Kreturn of int
-  | Kjump
-  | Krestart
-  | Kgrab of int
-  | Kgrabrec of int
-  | Kclosure of Label.t * int
-  | Kclosurerec of int * int * Label.t array * Label.t array
-  | Kclosurecofix of int * int * Label.t array * Label.t array
-                   (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of Constant.t
-  | Kconst of structured_constant
-  | Kmakeblock of int * tag
-  | Kmakeprod
-  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kswitch of Label.t array * Label.t array
-  | Kpushfields of int
-  | Kfield of int
-  | Ksetfield of int
-  | Kstop
-  | Ksequence of bytecodes * bytecodes
-  | Kproj of Projection.Repr.t
-  | Kensurestackcapacity of int
-  | Kbranch of Label.t                  (* jump to label *)
-  | Kprim of CPrimitives.t * pconstant option
-  | Kcamlprim of CPrimitives.t * Label.t
-  | Kareint of int
-
-and bytecodes = instruction list
-
-type fv_elem =
-  | FVnamed of Id.t
-  | FVrel of int
-  | FVuniv_var of int
-  | FVevar of Evar.t
-
-type fv = fv_elem array
-
-(* --- Pretty print *)
-open Pp
-open Util
-
-let pp_lbl lbl = str "L" ++ int lbl
-
-let pp_fv_elem = function
-  | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
-  | FVrel i -> str "Rel(" ++ int i ++ str ")"
-  | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
-  | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")"
-
-let rec pp_instr i =
-  match i with
-  | Klabel _   | Ksequence _ -> assert false
-  | Kacc n -> str "acc " ++ int n
-  | Kenvacc n -> str "envacc " ++ int n
-  | Koffsetclosure n -> str "offsetclosure " ++ int n
-  | Kpush -> str "push"
-  | Kpop n -> str "pop " ++ int n
-  | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
-  | Kapply n -> str "apply " ++ int n
-  | Kappterm(n, m) ->
-      str "appterm " ++ int n ++ str ", " ++ int m
-  | Kreturn n -> str "return " ++ int n
-  | Kjump -> str "jump"
-  | Krestart -> str "restart"
-  | Kgrab n -> str "grab " ++ int n
-  | Kgrabrec n -> str "grabrec " ++ int n
-  | Kclosure(lbl, n) ->
-      str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
-  | Kclosurerec(fv,init,lblt,lblb) ->
-      h 1 (str "closurerec " ++
-             int fv ++ str ", " ++ int init ++
-             str " types = " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
-             str " bodies = " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kclosurecofix (fv,init,lblt,lblb) ->
-      h 1 (str "closurecofix " ++
-             int fv ++ str ", " ++ int init ++
-             str " types = " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
-             str " bodies = " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kgetglobal idu -> str "getglobal " ++ Constant.print idu
-  | Kconst sc ->
-      str "const " ++ pp_struct_const sc
-  | Kmakeblock(n, m) ->
-      str "makeblock " ++ int n ++ str ", " ++ int m
-  | Kmakeprod -> str "makeprod"
-  | Kmakeswitchblock(lblt,lbls,_,sz) ->
-      str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
-        pp_lbl lbls ++ str ", " ++ int sz
-  | Kswitch(lblc,lblb) ->
-      h 1 (str "switch " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
-             str " | " ++
-             prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kpushfields n -> str "pushfields " ++ int n
-  | Kfield n -> str "field " ++ int n
-  | Ksetfield n -> str "setfield " ++ int n
-
-  | Kstop -> str "stop"
-
-  | Kbranch lbl -> str "branch " ++ pp_lbl lbl
-
-  | Kproj p -> str "proj " ++ Projection.Repr.print p
-
-  | 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 "")
-
-  | Kcamlprim (op, lbl) ->
-    str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
-    pp_lbl lbl
-
-  | Kareint n -> str "areint " ++ int n
-
-and pp_bytecodes c =
-  match c with
-  | [] -> str ""
-  | Klabel lbl :: c ->
-        str "L" ++ int lbl ++ str ":" ++ fnl () ++
-        pp_bytecodes c
-  | Ksequence (l1, l2) :: c ->
-      pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
-  | i :: c ->
-      pp_instr i ++ fnl () ++ pp_bytecodes c
-- 
cgit v1.2.3