package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.kernel/Vmbytecodes/index.html

Module VmbytecodesSource

Sourcemodule Label : sig ... end
Sourcetype caml_prim =
  1. | CAML_Arraymake
  2. | CAML_Arrayget
  3. | CAML_Arraydefault
  4. | CAML_Arrayset
  5. | CAML_Arraycopy
  6. | CAML_Arraylength
  7. | CAML_Stringmake
  8. | CAML_Stringlength
  9. | CAML_Stringget
  10. | CAML_Stringsub
  11. | CAML_Stringcat
  12. | CAML_Stringcompare
Sourcetype instruction =
  1. | Klabel of Label.t
  2. | Kacc of int
    (*

    accu = spn

    *)
  3. | Kenvacc of int
    (*

    accu = rocq_envn

    *)
  4. | Koffsetclosure of int
    (*

    accu = &rocq_envn

    *)
  5. | Kpush
    (*

    sp = accu :: sp

    *)
  6. | Kpop of int
    (*

    sp = skipn n sp

    *)
  7. | Kpush_retaddr of Label.t
    (*

    sp = pc :: rocq_env :: rocq_extra_args :: sp ; rocq_extra_args = 0

    *)
  8. | Kshort_apply of int
    (*

    number of arguments (arguments on top of stack)

    *)
  9. | Kapply of int
    (*

    number of arguments (arguments on top of stack)

    *)
  10. | Kappterm of int * int
    (*

    number of arguments, slot size

    *)
  11. | Kreturn of int
    (*

    slot size

    *)
  12. | Kjump
  13. | Krestart
  14. | Kgrab of int
    (*

    number of arguments

    *)
  15. | Kgrabrec of int
    (*

    rec arg

    *)
  16. | Kclosure of Label.t * int
    (*

    label, number of free variables

    *)
  17. | Kclosurerec of int * int * Label.t array * Label.t array
    (*

    nb fv, init, lbl types, lbl bodies

    *)
  18. | Kclosurecofix of int * int * Label.t array * Label.t array
    (*

    nb fv, init, lbl types, lbl bodies

    *)
  19. | Kgetglobal of Names.Constant.t
  20. | Ksubstinstance of UVars.Instance.t
  21. | Kconst of Vmvalues.structured_constant
  22. | Kmakeblock of int * Vmvalues.tag
    (*

    allocate an ocaml block. Index 0 ** is accu, all others are popped from ** the top of the stack

    *)
  23. | Kmakeswitchblock of Label.t * Label.t * Vmvalues.annot_switch * int
  24. | Kswitch of Label.t array * Label.t array
    (*

    consts,blocks

    *)
  25. | Kpushfields of int
  26. | Kfield of int
    (*

    accu = accun

    *)
  27. | Ksetfield of int
    (*

    accun = sp0 ; sp = pop sp

    *)
  28. | Kstop
  29. | Ksequence of bytecodes
  30. | Kproj of int
  31. | Kensurestackcapacity of int
  32. | Kbranch of Label.t
    (*

    jump to label, is it needed ?

    *)
  33. | Kprim of CPrimitives.t * Constr.pconstant
  34. | Kcamlprim of caml_prim * Label.t
Sourceand bytecodes = instruction list
Sourceval pp_bytecodes : bytecodes -> Pp.t
Sourcetype fv_elem =
  1. | FVnamed of Names.Id.t
  2. | FVrel of int
Sourcetype fv = fv_elem array
Sourceval pp_fv_elem : fv_elem -> Pp.t
Sourceval caml_prim_to_prim : caml_prim -> CPrimitives.t