coq 8.7.2 · OCaml Package

type retroknowledge

type entry = Constr.t

type nat_field =

| NatType
| NatPlus
| NatTimes

type n_field =

| NPositive
| NType
| NTwice
| NTwicePlusOne
| NPhi
| NPhiInv
| NPlus
| NTimes

type int31_field =

| Int31Bits
| Int31Type
| Int31Constructor
| Int31Twice
| Int31TwicePlusOne
| Int31Phi
| Int31PhiInv
| Int31Plus
| Int31PlusC
| Int31PlusCarryC
| Int31Minus
| Int31MinusC
| Int31MinusCarryC
| Int31Times
| Int31TimesC
| Int31Div21
| Int31Div
| Int31Diveucl
| Int31AddMulDiv
| Int31Compare
| Int31Head0
| Int31Tail0
| Int31Lor
| Int31Land
| Int31Lxor

type field =

| KInt31 of string * int31_field

type action =

| RKRegister of field * entry

val initial_retroknowledge : retroknowledge

val get_vm_compiling_info : 
  retroknowledge ->
  entry ->
  Cbytecodes.comp_env ->
  Term.constr array ->
  int ->
  Cbytecodes.bytecodes ->
  Cbytecodes.bytecodes

val get_vm_constant_static_info : 
  retroknowledge ->
  entry ->
  Term.constr array ->
  Cbytecodes.structured_constant

val get_vm_constant_dynamic_info : 
  retroknowledge ->
  entry ->
  Cbytecodes.comp_env ->
  Cbytecodes.block array ->
  int ->
  Cbytecodes.bytecodes ->
  Cbytecodes.bytecodes

val get_vm_before_match_info : 
  retroknowledge ->
  entry ->
  Cbytecodes.bytecodes ->
  Cbytecodes.bytecodes

val get_vm_decompile_constant_info : 
  retroknowledge ->
  entry ->
  int ->
  Term.constr

val get_native_compiling_info : 
  retroknowledge ->
  entry ->
  Nativeinstr.prefix ->
  Nativeinstr.lambda array ->
  Nativeinstr.lambda

val get_native_constant_static_info : 
  retroknowledge ->
  entry ->
  Term.constr array ->
  Nativeinstr.lambda

val get_native_constant_dynamic_info : 
  retroknowledge ->
  entry ->
  Nativeinstr.prefix ->
  Names.constructor ->
  Nativeinstr.lambda array ->
  Nativeinstr.lambda

val get_native_before_match_info : 
  retroknowledge ->
  entry ->
  Nativeinstr.prefix ->
  Names.constructor ->
  Nativeinstr.lambda ->
  Nativeinstr.lambda

val add_field : retroknowledge -> field -> entry -> retroknowledge

val mem : retroknowledge -> field -> bool

val find : retroknowledge -> field -> entry

type reactive_info = {

vm_compiling : (bool -> Cbytecodes.comp_env -> Term.constr array -> int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
vm_constant_static : (bool -> Term.constr array -> Cbytecodes.structured_constant) option;
vm_constant_dynamic : (bool -> Cbytecodes.comp_env -> Cbytecodes.block array -> int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
vm_decompile_const : (int -> Term.constr) option;
native_compiling : (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> Nativeinstr.lambda) option;
native_constant_static : (bool -> Term.constr array -> Nativeinstr.lambda) option;
native_constant_dynamic : (bool -> Nativeinstr.prefix -> Names.constructor -> Nativeinstr.lambda array -> Nativeinstr.lambda) option;
native_before_match : (bool -> Nativeinstr.prefix -> Names.constructor -> Nativeinstr.lambda -> Nativeinstr.lambda) option;

}

val empty_reactive_info : reactive_info

val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t

package coq