blob: 0cba4cb87a8f3bea561ff8f5d4c56a0d3d44b069 (
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
|
(* $Id$ *)
(*i*)
open Pp
open Names
open Generic
open Term
open Evd
open Environ
(*i*)
(* Flags for profiling reductions. *)
val stats : bool ref
val share : bool ref
(*s The set of reduction kinds. *)
type red_kind = BETA | DELTA of sorts oper | IOTA
type reds = {
r_beta : bool;
r_delta : sorts oper -> bool;
r_iota : bool }
val no_red : reds
val beta_red : reds
val betaiota_red : reds
val betadeltaiota_red : reds
val red_set : reds -> red_kind -> bool
(*s Reduction function specification. *)
type red_mode = UNIFORM | SIMPL | WITHBACK
type flags = red_mode * reds
(* [(UNIFORM,r)] == [r]-reduce in any context.
[(SIMPL,r)] == bdi-reduce under cases or fix, [r] otherwise
(like hnf does).
[(WITHBACK,r)] == internal use: means we are under a case
or in rec. arg. of fix. *)
val flags_under : flags -> flags
val red_top : flags -> red_kind -> bool
val red_under : flags -> red_kind -> bool
val no_flag : flags
val beta : flags
val betaiota : flags
val betadeltaiota : flags
val hnf_flags : flags
(*s Call by value functions *)
type cbv_value =
| VAL of int * constr
| LAM of name * constr * constr * cbv_value subs
| FIXP of sorts oper * constr array * cbv_value subs * cbv_value list
| CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
val shift_value : int -> cbv_value -> cbv_value
val contract_fixp : cbv_value subs -> constr -> cbv_value subs * constr
type stack =
| TOP
| APP of cbv_value list * stack
| CASE of constr * constr array * case_info * cbv_value subs * stack
val stack_app : cbv_value list -> stack -> stack
val under_case_stack : stack -> bool
val strip_appl : cbv_value -> stack -> cbv_value * stack
val red_allowed : flags -> stack -> red_kind -> bool
val reduce_const_body :
(cbv_value -> cbv_value) -> cbv_value -> stack -> cbv_value * stack
val fixp_reducible :
(cbv_value -> cbv_value) -> flags -> sorts oper -> stack -> bool
(* normalization of a constr: the two functions to know... *)
type 'a cbv_infos
val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
val cbv_norm : 'a cbv_infos -> constr -> constr
(* recursive functions... *)
val cbv_stack_term : 'a cbv_infos ->
stack -> cbv_value subs -> constr -> cbv_value
val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr
val cbv_norm_more : 'a cbv_infos -> cbv_value -> cbv_value
val norm_head : 'a cbv_infos ->
cbv_value subs -> constr -> stack -> cbv_value * stack
val apply_stack : 'a cbv_infos -> constr -> stack -> constr
val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
(*s Lazy reduction. *)
type 'a freeze
type 'a frterm =
| FRel of int
| FVAR of identifier
| FOP0 of 'a
| FOP1 of 'a * 'a freeze
| FOP2 of 'a * 'a freeze * 'a freeze
| FOPN of 'a * 'a freeze array
| FOPL of 'a * 'a freeze list
| FLAM of name * 'a freeze * 'a term * 'a freeze subs
| FLAMV of name * 'a freeze array * 'a term array * 'a freeze subs
| FLIFT of int * 'a freeze
| FFROZEN of 'a term * 'a freeze subs
val frterm_of : 'a freeze -> 'a frterm
val is_val : 'a freeze -> bool
val lift_frterm : int -> 'a freeze -> 'a freeze
val lift_freeze : int -> 'a freeze -> 'a freeze
val freeze : 'a freeze subs -> 'a term -> 'a freeze
val freeze_vect : 'a freeze subs -> 'a term array -> 'a freeze array
val freeze_list : 'a freeze subs -> 'a term list -> 'a freeze list
val traverse_term : 'a freeze subs -> 'a term -> 'a freeze
val lift_term_of_freeze : lift_spec -> 'a freeze -> 'a term
(* Back to constr *)
val fstrong : ('a freeze -> 'a freeze) -> lift_spec -> 'a freeze -> 'a term
val term_of_freeze : 'a freeze -> 'a term
val applist_of_freeze : 'a freeze array -> 'a term list
(* contract a substitution *)
val contract_subst : int -> 'a freeze -> 'a freeze -> 'a freeze
(* Calculus of Constructions *)
type fconstr = sorts oper freeze
val inject : constr -> fconstr
val strip_frterm :
int -> fconstr -> fconstr array list -> int * fconstr * fconstr array
val strip_freeze : fconstr -> int * fconstr * fconstr array
(* Auxiliary functions for (co)fixpoint reduction *)
val contract_fix_vect : (fconstr -> fconstr) -> sorts oper frterm -> fconstr
val copy_case : case_info -> fconstr array -> fconstr -> fconstr
(* Iota analysis: reducible ? *)
type case_status =
| CONSTRUCTOR of int * fconstr array
| COFIX of int * int * fconstr array * fconstr array
| IRREDUCTIBLE
(* Constant cache *)
type 'a clos_infos
val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
val clos_infos_env : 'a clos_infos -> env
(* Reduction function *)
val norm_val : 'a clos_infos -> fconstr -> constr
val whd_val : 'a clos_infos -> fconstr -> constr
val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr array
val fhnf_apply : 'a clos_infos ->
int -> fconstr -> fconstr array -> int * fconstr * fconstr array
val search_frozen_cst : 'a clos_infos ->
sorts oper -> fconstr array -> fconstr option
(* recursive functions... *)
val unfreeze : 'a clos_infos -> fconstr -> fconstr
val whnf_frterm : 'a clos_infos -> fconstr -> fconstr
val whnf_term : 'a clos_infos -> fconstr subs -> constr -> fconstr
val whnf_apply : 'a clos_infos -> fconstr -> fconstr array -> fconstr
|
