diff options
Diffstat (limited to 'kernel/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 44 |
1 files changed, 21 insertions, 23 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index b8de7619..f87090c7 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,15 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Term +open Constr type tag = int @@ -26,21 +28,26 @@ val cofix_evaluated_tag : tag val last_variant_tag : tag type structured_constant = - | Const_sorts of sorts + | Const_sort of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.universe_level - | Const_type of Univ.universe + | Const_univ_level of Univ.Level.t -val pp_struct_const : structured_constant -> Pp.std_ppcmds +val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + module Label : sig type t = int @@ -69,7 +76,7 @@ type instruction = (** 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 + | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 ** is accu, all others are popped from @@ -132,6 +139,7 @@ type fv_elem = FVnamed of Id.t | FVrel of int | FVuniv_var of int +| FVevar of Evar.t type fv = fv_elem array @@ -152,6 +160,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) @@ -163,16 +172,5 @@ type comp_env = { in_env : vm_env ref (** the variables that are accessed *) } -val pp_bytecodes : bytecodes -> Pp.std_ppcmds -val pp_fv_elem : fv_elem -> Pp.std_ppcmds - -(*spiwack: moved this here because I needed it for retroknowledge *) -type block = - | Bconstr of constr - | Bstrconst of structured_constant - | Bmakeblock of int * block array - | Bconstruct_app of int * int * int * block array - (** tag , nparams, arity *) - | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array - (** compilation function (see get_vm_constant_dynamic_info in - retroknowledge.mli for more info) , argument array *) +val pp_bytecodes : bytecodes -> Pp.t +val pp_fv_elem : fv_elem -> Pp.t |