blob: bc38452d4f660d45989ab2cb8ea527a946a43deb (
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
117
118
119
120
121
122
123
124
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Constr
open Cbytecodes
(** Debug printing *)
val set_drawinstr : unit -> unit
(** Machine code *)
type tcode
(** Values *)
type vprod
type vfun
type vfix
type vcofix
type vblock
type vswitch
type arguments
type atom =
| Aid of Vars.id_key
| Aind of inductive
| Atype of Univ.Universe.t
(** Zippers *)
type zipper =
| Zapp of arguments
| Zfix of vfix * arguments (** might be empty *)
| Zswitch of vswitch
| Zproj of Constant.t (* name of the projection *)
type stack = zipper list
type to_up
type whd =
| Vsort of Sorts.t
| Vprod of vprod
| Vfun of vfun
| Vfix of vfix * arguments option
| Vcofix of vcofix * to_up * arguments option
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
| Vuniv_level of Univ.Level.t
(** For debugging purposes only *)
val pr_atom : atom -> Pp.t
val pr_whd : whd -> Pp.t
val pr_stack : stack -> Pp.t
(** Constructors *)
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
val val_of_named : Id.t -> values
val val_of_constant : Constant.t -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
(** Destructors *)
val whd_val : values -> whd
val uni_lvl_val : values -> Univ.Level.t
(** Arguments *)
val nargs : arguments -> int
val arg : arguments -> int -> values
(** Product *)
val dom : vprod -> values
val codom : vprod -> vfun
(** Function *)
val body_of_vfun : int -> vfun -> values
val decompose_vfun2 : int -> vfun -> vfun -> int * values * values
(** Fix *)
val current_fix : vfix -> int
val check_fix : vfix -> vfix -> bool
val rec_args : vfix -> int array
val reduce_fix : int -> vfix -> vfun array * values array
(** bodies , types *)
(** CoFix *)
val current_cofix : vcofix -> int
val check_cofix : vcofix -> vcofix -> bool
val reduce_cofix : int -> vcofix -> values array * values array
(** bodies , types *)
(** Block *)
val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> values
(** Switch *)
val check_switch : vswitch -> vswitch -> bool
val case_info : vswitch -> case_info
val type_of_switch : vswitch -> values
val branch_of_switch : int -> vswitch -> (int * values) array
(** Apply a value *)
val apply_whd : int -> whd -> values
|
