SSL vmbytecodes.mli
Interaktion und PortierbarkeitSML
(************************************************************************) (* * The Rocq Prover / The Rocq 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) *) (************************************************************************)
(* $Id$ *)
open Names open Vmvalues open Constr
module Label : sig type t = int val no : t val create : unit -> t val reset_label_counter : unit -> unit end
type instruction =
| Klabel of Label.t
| Kacc of int (** accu = sp[n] *)
| Kenvacc of int (** accu = rocq_env[n] *)
| Koffsetclosure of int (** accu = &rocq_env[n] *)
| Kpush (** sp = accu :: sp *)
| Kpop of int (** sp = skipn n sp *)
| Kpush_retaddr of Label.t (** sp = pc :: rocq_env :: rocq_extra_args :: sp ; rocq_extra_args = 0 *)
| Kshort_apply of int (** number of arguments (arguments on top of stack) *)
| Kapply of int (** number of arguments (arguments on top of stack) *)
| Kappterm of int * int (** number of arguments, slot size *)
| Kreturn of int (** slot size *)
| Kjump
| Krestart
| Kgrab of int (** number of arguments *)
| Kgrabrec of int (** rec arg *)
| Kclosure of Label.t * int (** label, number of free variables *)
| Kclosurerec of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *)
| Kgetglobal of Constant.t
| Ksubstinstance of UVars.Instance.t
| Kconst of structured_constant
| Kmakeblock of(* size: *) int * tag (** allocate an ocaml block. Index 0
** is accu, all others are popped from
** the top of the stack *)
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
| Kswitch of Label.t array * Label.t array (** consts,blocks *)
| Kpushfields of int
| Kfield of int (** accu = accu[n] *)
| Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *)
| Kstop
| Ksequence of bytecodes
| Kproj of int
| Kensurestackcapacity of int
| Kbranch of Label.t (** jump to label, is it needed ? *)
| Kprim of CPrimitives.t * pconstant
| Kcamlprim of caml_prim * Label.t
and bytecodes = instruction list
val pp_bytecodes : bytecodes -> Pp.t
type fv_elem =
FVnamed of Id.t
| FVrel of int
type fv = fv_elem array
val pp_fv_elem : fv_elem -> Pp.t
val caml_prim_to_prim : caml_prim -> CPrimitives.t
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
