blob: 821b2316855291d1daae818d32ec25b86650f418 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Term
open Names
(** This modules defines the representation of values internally used by
the native compiler. Be careful when removing apparently dead code from this
interface, as it may be used by programs generated at runtime. *)
type t = t -> t
type accumulator
type tag = int
type arity = int
type reloc_table = (tag * arity) array
type annot_sw = {
asw_ind : inductive;
asw_ci : case_info;
asw_reloc : reloc_table;
asw_finite : bool;
asw_prefix : string
}
val eq_annot_sw : annot_sw -> annot_sw -> bool
val hash_annot_sw : annot_sw -> int
type sort_annot = string * int
type rec_pos = int array
val eq_rec_pos : rec_pos -> rec_pos -> bool
type atom =
| Arel of int
| Aconstant of constant
| Aind of inductive
| Asort of sorts
| Avar of identifier
| Acase of annot_sw * accumulator * t * (t -> t)
| Afix of t array * t array * rec_pos * int
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
| Aprod of name * t * (t -> t)
| Ameta of metavariable * t
| Aevar of existential * t
(* Constructors *)
val mk_accu : atom -> t
val mk_rel_accu : int -> t
val mk_rels_accu : int -> int -> t array
val mk_constant_accu : constant -> t
val mk_ind_accu : inductive -> t
val mk_sort_accu : sorts -> t
val mk_var_accu : identifier -> t
val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
val mk_prod_accu : name -> t -> t -> t
val mk_fix_accu : rec_pos -> int -> t array -> t array -> t
val mk_cofix_accu : int -> t array -> t array -> t
val mk_meta_accu : metavariable -> t
val mk_evar_accu : existential -> t -> t
val upd_cofix : t -> t -> unit
val force_cofix : t -> t
val mk_const : tag -> t
val mk_block : tag -> t array -> t
val mk_int : int -> t
val mk_uint : Uint31.t -> t
val napply : t -> t array -> t
(* Functions over accumulators *)
val dummy_value : unit -> t
val atom_of_accu : accumulator -> atom
val args_of_accu : accumulator -> t list
val accu_nargs : accumulator -> int
val cast_accu : t -> accumulator
(* Functions over block: i.e constructors *)
type block
val block_size : block -> int
val block_field : block -> int -> t
val block_tag : block -> int
(* kind_of_value *)
type kind_of_value =
| Vaccu of accumulator
| Vfun of (t -> t)
| Vconst of int
| Vblock of block
val kind_of_value : t -> kind_of_value
(* *)
val is_accu : t -> bool
val str_encode : 'a -> string
val str_decode : string -> 'a
val mk_I31_accu : t
val decomp_uint : t -> t -> t
|
