blob: 0882758576602b260e81d26cc8b94f2a336ae7bb (
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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Pp
open Names
open Term
open Environ
open Esubst
(*i*)
(* Flags for profiling reductions. *)
val stats : bool ref
val share : bool ref
val with_stats: 'a Lazy.t -> 'a
(*s Delta implies all consts (both global (= by
[kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
val all_opaque : transparent_state
val all_transparent : transparent_state
(* Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
type red_kind
(* The different kind of reduction *)
(* Const/Var means the reference as argument should be unfolded *)
(* Constbut/Varbut means all references except the ones as argument
of Constbut/Varbut should be unfolded (there may be several such
Constbut/Varbut *)
val fBETA : red_kind
val fDELTA : red_kind
val fIOTA : red_kind
val fZETA : red_kind
val fCONST : constant -> red_kind
val fVAR : identifier -> red_kind
(* No reduction at all *)
val no_red : reds
(* Adds a reduction kind to a set *)
val red_add : reds -> red_kind -> reds
(* Removes a reduction kind to a set *)
val red_sub : reds -> red_kind -> reds
(* Adds a reduction kind to a set *)
val red_add_transparent : reds -> transparent_state -> reds
(* Build a reduction set from scratch = iter [red_add] on [no_red] *)
val mkflags : red_kind list -> reds
(* Tests if a reduction kind is set *)
val red_set : reds -> red_kind -> bool
(* Gives the constant list *)
val red_get_const : reds -> bool * evaluable_global_reference list
end
module RedFlags : RedFlagsSig
open RedFlags
val beta : reds
val betaiota : reds
val betadeltaiota : reds
val betaiotazeta : reds
val betadeltaiotanolet : reds
val unfold_red : evaluable_global_reference -> reds
(***********************************************************************)
type table_key = id_key
type 'a infos
val ref_value_cache: 'a infos -> table_key -> 'a option
val info_flags: 'a infos -> reds
val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
(************************************************************************)
(*s A [stack] is a context of arguments, arguments are pushed by
[append_stack] one array at a time but popped with [decomp_stack]
one by one *)
type 'a stack_member =
| Zapp of 'a list
| Zcase of case_info * 'a * 'a array
| Zfix of 'a * 'a stack
| Zshift of int
| Zupdate of 'a
and 'a stack = 'a stack_member list
val empty_stack : 'a stack
val append_stack : 'a array -> 'a stack -> 'a stack
val decomp_stack : 'a stack -> ('a * 'a stack) option
val list_of_stack : 'a stack -> 'a list
val array_of_stack : 'a stack -> 'a array
val stack_assign : 'a stack -> int -> 'a -> 'a stack
val stack_args_size : 'a stack -> int
val app_stack : constr * constr stack -> constr
val stack_tail : int -> 'a stack -> 'a stack
val stack_nth : 'a stack -> int -> 'a
val zip_term : ('a -> constr) -> constr -> 'a stack -> constr
(************************************************************************)
(*s Lazy reduction. *)
(* [fconstr] is the type of frozen constr *)
type fconstr
(* [fconstr] can be accessed by using the function [fterm_of] and by
matching on type [fterm] *)
type fterm =
| FRel of int
| FAtom of constr (* Metas and Sorts *)
| FCast of fconstr * fconstr
| FFlex of table_key
| FInd of inductive
| FConstruct of constructor
| FApp of fconstr * fconstr array
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCases of case_info * fconstr * fconstr * fconstr array
| FLambda of int * (name * constr) list * constr * fconstr subs
| FProd of name * fconstr * fconstr
| FLetIn of name * fconstr * fconstr * constr * fconstr subs
| FEvar of existential_key * fconstr array
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
| FLOCKED
(* To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
val inject : constr -> fconstr
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> constr
val destFLambda :
(fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
(* prevents a term from being evaluated *)
val set_norm : fconstr -> unit
(* Global and local constant cache *)
type clos_infos
val create_clos_infos : reds -> env -> clos_infos
(* Reduction function *)
(* [norm_val] is for strong normalization *)
val norm_val : clos_infos -> fconstr -> constr
(* [whd_val] is for weak head normalization *)
val whd_val : clos_infos -> fconstr -> constr
(* [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
(* Conversion auxiliary functions to do step by step normalisation *)
(* [unfold_reference] unfolds references in a [fconstr] *)
val unfold_reference : clos_infos -> table_key -> fconstr option
(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
(************************************************************************)
(*i This is for lazy debug *)
val lift_fconstr : int -> fconstr -> fconstr
val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos : fconstr subs -> constr -> fconstr
val mk_clos_vect : fconstr subs -> constr array -> fconstr array
val mk_clos_deep :
(fconstr subs -> constr -> fconstr) ->
fconstr subs -> constr -> fconstr
val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
val kl : clos_infos -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
(* End of cbn debug section i*)
|
