package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Label : sig ... end
type instruction =
  1. | Klabel of Label.t
  2. | Kacc of int
  3. | Kenvacc of int
  4. | Koffsetclosure of int
  5. | Kpush
  6. | Kpop of int
  7. | Kpush_retaddr of Label.t
  8. | Kapply of int
  9. | Kappterm of int * int
  10. | Kreturn of int
  11. | Kjump
  12. | Krestart
  13. | Kgrab of int
  14. | Kgrabrec of int
  15. | Kclosure of Label.t * int
  16. | Kclosurerec of int * int * Label.t array * Label.t array
  17. | Kclosurecofix of int * int * Label.t array * Label.t array
  18. | Kgetglobal of Names.Constant.t
  19. | Kconst of Vmvalues.structured_constant
  20. | Kmakeblock of int * Vmvalues.tag
  21. | Kmakeprod
  22. | Kmakeswitchblock of Label.t * Label.t * Vmvalues.annot_switch * int
  23. | Kswitch of Label.t array * Label.t array
  24. | Kpushfields of int
  25. | Kfield of int
  26. | Ksetfield of int
  27. | Kstop
  28. | Ksequence of bytecodes * bytecodes
  29. | Kproj of Names.Projection.Repr.t
  30. | Kensurestackcapacity of int
  31. | Kbranch of Label.t
  32. | Kaddint31
  33. | Kaddcint31
  34. | Kaddcarrycint31
  35. | Ksubint31
  36. | Ksubcint31
  37. | Ksubcarrycint31
  38. | Kmulint31
  39. | Kmulcint31
  40. | Kdiv21int31
  41. | Kdivint31
  42. | Kaddmuldivint31
  43. | Kcompareint31
  44. | Khead0int31
  45. | Ktail0int31
  46. | Kisconst of Label.t
  47. | Kareconst of int * Label.t
  48. | Kcompint31
  49. | Kdecompint31
  50. | Klorint31
  51. | Klandint31
  52. | Klxorint31
and bytecodes = instruction list
type fv_elem =
  1. | FVnamed of Names.Id.t
  2. | FVrel of int
  3. | FVuniv_var of int
  4. | FVevar of Evar.t
type fv = fv_elem array
exception NotClosed
module FvMap : sig ... end
type vm_env = {
  1. size : int;
  2. fv_rev : fv_elem list;
  3. fv_fwd : int FvMap.t;
}
type comp_env = {
  1. arity : int;
  2. nb_uni_stack : int;
  3. nb_stack : int;
  4. in_stack : int list;
  5. nb_rec : int;
  6. pos_rec : instruction list;
  7. offset : int;
  8. in_env : vm_env ref;
}
val pp_bytecodes : bytecodes -> Pp.t
val pp_fv_elem : fv_elem -> Pp.t