package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.kernel/Vmbytecodes/index.html
Module VmbytecodesSource
Source
type instruction = | Klabel of Label.t| Kacc of int(*accu = sp
*)n| Kenvacc of int(*accu = coq_env
*)n| Koffsetclosure of int(*accu = &coq_env
*)n| Kpush(*sp = accu :: sp
*)| Kpop of int(*sp = skipn n sp
*)| Kpush_retaddr of Label.t(*sp = pc :: coq_env :: coq_extra_args :: sp ; coq_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 Names.Constant.t| Kconst of Vmvalues.structured_constant| Kmakeblock of int * Vmvalues.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 * Vmvalues.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= sp0; sp = pop sp| Kstop| Ksequence of bytecodes| Kproj of Names.Projection.Repr.t| Kensurestackcapacity of int| Kbranch of Label.t(*jump to label, is it needed ?
*)| Kprim of CPrimitives.t * Constr.pconstant| Kcamlprim of caml_prim * Label.t