blob: d10d722020423602230d5b824dbb27292f231004 (
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
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
|
(* This file is autogenerated from ReificationTypes.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ReificationTypes.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := limb_widths | bounds_exp | bounds_tight | bounds_loose | bounds_limbwidths | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_tight_bounded | feW_loose_bounded | feW_limbwidths_bounded | feBW_tight | feBW_loose | feBW_limbwidths | feBW_relax | feBW_relax_limbwidths_to_tight | feBW_relax_limbwidths_to_loose | feBW_tight_bounded | feBW_limbwidths_bounded | phiW | phiBW_tight | phiBW_loose | phiBW_limbwidths.
End TAG.
Ltac add_limb_widths pkg :=
let wt := Tag.get pkg TAG.wt in
let sz := Tag.get pkg TAG.sz in
let limb_widths := fresh "limb_widths" in
let limb_widths := pose_local_limb_widths wt sz limb_widths in
Tag.local_update pkg TAG.limb_widths limb_widths.
Ltac add_bounds_exp pkg :=
let sz := Tag.get pkg TAG.sz in
let limb_widths := Tag.get pkg TAG.limb_widths in
let bounds_exp := fresh "bounds_exp" in
let bounds_exp := pose_local_bounds_exp sz limb_widths bounds_exp in
Tag.local_update pkg TAG.bounds_exp bounds_exp.
Ltac add_bounds_tight pkg :=
let sz := Tag.get pkg TAG.sz in
let upper_bound_of_exponent_tight := Tag.get pkg TAG.upper_bound_of_exponent_tight in
let bounds_exp := Tag.get pkg TAG.bounds_exp in
let bounds_tight := fresh "bounds_tight" in
let bounds_tight := pose_local_bounds_tight sz upper_bound_of_exponent_tight bounds_exp bounds_tight in
Tag.local_update pkg TAG.bounds_tight bounds_tight.
Ltac add_bounds_loose pkg :=
let sz := Tag.get pkg TAG.sz in
let upper_bound_of_exponent_loose := Tag.get pkg TAG.upper_bound_of_exponent_loose in
let bounds_exp := Tag.get pkg TAG.bounds_exp in
let bounds_loose := fresh "bounds_loose" in
let bounds_loose := pose_local_bounds_loose sz upper_bound_of_exponent_loose bounds_exp bounds_loose in
Tag.local_update pkg TAG.bounds_loose bounds_loose.
Ltac add_bounds_limbwidths pkg :=
let sz := Tag.get pkg TAG.sz in
let bounds_exp := Tag.get pkg TAG.bounds_exp in
let bounds_limbwidths := fresh "bounds_limbwidths" in
let bounds_limbwidths := pose_local_bounds_limbwidths sz bounds_exp bounds_limbwidths in
Tag.local_update pkg TAG.bounds_limbwidths bounds_limbwidths.
Ltac add_bound1 pkg :=
let r := Tag.get pkg TAG.r in
let bound1 := fresh "bound1" in
let bound1 := pose_bound1 r bound1 in
Tag.update pkg TAG.bound1 bound1.
Ltac add_lgbitwidth pkg :=
let bitwidth := Tag.get pkg TAG.bitwidth in
let lgbitwidth := fresh "lgbitwidth" in
let lgbitwidth := pose_local_lgbitwidth bitwidth lgbitwidth in
Tag.local_update pkg TAG.lgbitwidth lgbitwidth.
Ltac add_adjusted_bitwidth' pkg :=
let lgbitwidth := Tag.get pkg TAG.lgbitwidth in
let adjusted_bitwidth' := fresh "adjusted_bitwidth'" in
let adjusted_bitwidth' := pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' in
Tag.local_update pkg TAG.adjusted_bitwidth' adjusted_bitwidth'.
Ltac add_adjusted_bitwidth pkg :=
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let adjusted_bitwidth := fresh "adjusted_bitwidth" in
let adjusted_bitwidth := pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth in
Tag.update pkg TAG.adjusted_bitwidth adjusted_bitwidth.
Ltac add_feZ pkg :=
let sz := Tag.get pkg TAG.sz in
let feZ := fresh "feZ" in
let feZ := pose_local_feZ sz feZ in
Tag.local_update pkg TAG.feZ feZ.
Ltac add_feW pkg :=
let sz := Tag.get pkg TAG.sz in
let lgbitwidth := Tag.get pkg TAG.lgbitwidth in
let feW := fresh "feW" in
let feW := pose_feW sz lgbitwidth feW in
Tag.update pkg TAG.feW feW.
Ltac add_feW_tight_bounded pkg :=
let feW := Tag.get pkg TAG.feW in
let bounds_tight := Tag.get pkg TAG.bounds_tight in
let feW_tight_bounded := fresh "feW_tight_bounded" in
let feW_tight_bounded := pose_feW_tight_bounded feW bounds_tight feW_tight_bounded in
Tag.update pkg TAG.feW_tight_bounded feW_tight_bounded.
Ltac add_feW_loose_bounded pkg :=
let feW := Tag.get pkg TAG.feW in
let bounds_loose := Tag.get pkg TAG.bounds_loose in
let feW_loose_bounded := fresh "feW_loose_bounded" in
let feW_loose_bounded := pose_feW_loose_bounded feW bounds_loose feW_loose_bounded in
Tag.update pkg TAG.feW_loose_bounded feW_loose_bounded.
Ltac add_feW_limbwidths_bounded pkg :=
let feW := Tag.get pkg TAG.feW in
let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
let feW_limbwidths_bounded := fresh "feW_limbwidths_bounded" in
let feW_limbwidths_bounded := pose_feW_limbwidths_bounded feW bounds_limbwidths feW_limbwidths_bounded in
Tag.update pkg TAG.feW_limbwidths_bounded feW_limbwidths_bounded.
Ltac add_feBW_tight pkg :=
let sz := Tag.get pkg TAG.sz in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds_tight := Tag.get pkg TAG.bounds_tight in
let feBW_tight := fresh "feBW_tight" in
let feBW_tight := pose_feBW_tight sz adjusted_bitwidth' bounds_tight feBW_tight in
Tag.update pkg TAG.feBW_tight feBW_tight.
Ltac add_feBW_loose pkg :=
let sz := Tag.get pkg TAG.sz in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds_loose := Tag.get pkg TAG.bounds_loose in
let feBW_loose := fresh "feBW_loose" in
let feBW_loose := pose_feBW_loose sz adjusted_bitwidth' bounds_loose feBW_loose in
Tag.update pkg TAG.feBW_loose feBW_loose.
Ltac add_feBW_limbwidths pkg :=
let sz := Tag.get pkg TAG.sz in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
let feBW_limbwidths := fresh "feBW_limbwidths" in
let feBW_limbwidths := pose_feBW_limbwidths sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths in
Tag.update pkg TAG.feBW_limbwidths feBW_limbwidths.
Ltac add_feBW_relax pkg :=
let sz := Tag.get pkg TAG.sz in
let feBW_tight := Tag.get pkg TAG.feBW_tight in
let feBW_loose := Tag.get pkg TAG.feBW_loose in
let feBW_relax := fresh "feBW_relax" in
let feBW_relax := pose_feBW_relax sz feBW_tight feBW_loose feBW_relax in
Tag.update pkg TAG.feBW_relax feBW_relax.
Ltac add_feBW_relax_limbwidths_to_tight pkg :=
let sz := Tag.get pkg TAG.sz in
let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
let feBW_tight := Tag.get pkg TAG.feBW_tight in
let feBW_relax_limbwidths_to_tight := fresh "feBW_relax_limbwidths_to_tight" in
let feBW_relax_limbwidths_to_tight := pose_feBW_relax_limbwidths_to_tight sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight in
Tag.update pkg TAG.feBW_relax_limbwidths_to_tight feBW_relax_limbwidths_to_tight.
Ltac add_feBW_relax_limbwidths_to_loose pkg :=
let sz := Tag.get pkg TAG.sz in
let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
let feBW_loose := Tag.get pkg TAG.feBW_loose in
let feBW_relax_limbwidths_to_loose := fresh "feBW_relax_limbwidths_to_loose" in
let feBW_relax_limbwidths_to_loose := pose_feBW_relax_limbwidths_to_loose sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose in
Tag.update pkg TAG.feBW_relax_limbwidths_to_loose feBW_relax_limbwidths_to_loose.
Ltac add_feBW_tight_bounded pkg :=
let freeze := Tag.get pkg TAG.freeze in
let wt := Tag.get pkg TAG.wt in
let sz := Tag.get pkg TAG.sz in
let feBW_tight := Tag.get pkg TAG.feBW_tight in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds_tight := Tag.get pkg TAG.bounds_tight in
let m := Tag.get pkg TAG.m in
let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
let feBW_tight_bounded := fresh "feBW_tight_bounded" in
let feBW_tight_bounded := pose_feBW_tight_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded in
Tag.update pkg TAG.feBW_tight_bounded feBW_tight_bounded.
Ltac add_feBW_limbwidths_bounded pkg :=
let freeze := Tag.get pkg TAG.freeze in
let wt := Tag.get pkg TAG.wt in
let sz := Tag.get pkg TAG.sz in
let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds_limbwidths := Tag.get pkg TAG.bounds_limbwidths in
let m := Tag.get pkg TAG.m in
let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
let feBW_limbwidths_bounded := fresh "feBW_limbwidths_bounded" in
let feBW_limbwidths_bounded := pose_feBW_limbwidths_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded in
Tag.update pkg TAG.feBW_limbwidths_bounded feBW_limbwidths_bounded.
Ltac add_phiW pkg :=
let feW := Tag.get pkg TAG.feW in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let phiW := fresh "phiW" in
let phiW := pose_phiW feW m wt phiW in
Tag.update pkg TAG.phiW phiW.
Ltac add_phiBW_tight pkg :=
let feBW_tight := Tag.get pkg TAG.feBW_tight in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let phiBW_tight := fresh "phiBW_tight" in
let phiBW_tight := pose_phiBW_tight feBW_tight m wt phiBW_tight in
Tag.update pkg TAG.phiBW_tight phiBW_tight.
Ltac add_phiBW_loose pkg :=
let feBW_loose := Tag.get pkg TAG.feBW_loose in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let phiBW_loose := fresh "phiBW_loose" in
let phiBW_loose := pose_phiBW_loose feBW_loose m wt phiBW_loose in
Tag.update pkg TAG.phiBW_loose phiBW_loose.
Ltac add_phiBW_limbwidths pkg :=
let feBW_limbwidths := Tag.get pkg TAG.feBW_limbwidths in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let phiBW_limbwidths := fresh "phiBW_limbwidths" in
let phiBW_limbwidths := pose_phiBW_limbwidths feBW_limbwidths m wt phiBW_limbwidths in
Tag.update pkg TAG.phiBW_limbwidths phiBW_limbwidths.
Ltac add_ReificationTypes_package pkg :=
let pkg := add_limb_widths pkg in
let pkg := add_bounds_exp pkg in
let pkg := add_bounds_tight pkg in
let pkg := add_bounds_loose pkg in
let pkg := add_bounds_limbwidths pkg in
let pkg := add_bound1 pkg in
let pkg := add_lgbitwidth pkg in
let pkg := add_adjusted_bitwidth' pkg in
let pkg := add_adjusted_bitwidth pkg in
let pkg := add_feZ pkg in
let pkg := add_feW pkg in
let pkg := add_feW_tight_bounded pkg in
let pkg := add_feW_loose_bounded pkg in
let pkg := add_feW_limbwidths_bounded pkg in
let pkg := add_feBW_tight pkg in
let pkg := add_feBW_loose pkg in
let pkg := add_feBW_limbwidths pkg in
let pkg := add_feBW_relax pkg in
let pkg := add_feBW_relax_limbwidths_to_tight pkg in
let pkg := add_feBW_relax_limbwidths_to_loose pkg in
let pkg := add_feBW_tight_bounded pkg in
let pkg := add_feBW_limbwidths_bounded pkg in
let pkg := add_phiW pkg in
let pkg := add_phiBW_tight pkg in
let pkg := add_phiBW_loose pkg in
let pkg := add_phiBW_limbwidths pkg in
Tag.strip_subst_local pkg.
Module MakeReificationTypesPackage (PKG : PrePackage).
Module Import MakeReificationTypesPackageInternal := MakePackageBase PKG.
Ltac get_bound1 _ := get TAG.bound1.
Notation bound1 := (ltac:(let v := get_bound1 () in exact v)) (only parsing).
Ltac get_adjusted_bitwidth _ := get TAG.adjusted_bitwidth.
Notation adjusted_bitwidth := (ltac:(let v := get_adjusted_bitwidth () in exact v)) (only parsing).
Ltac get_feW _ := get TAG.feW.
Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing).
Ltac get_feW_tight_bounded _ := get TAG.feW_tight_bounded.
Notation feW_tight_bounded := (ltac:(let v := get_feW_tight_bounded () in exact v)) (only parsing).
Ltac get_feW_loose_bounded _ := get TAG.feW_loose_bounded.
Notation feW_loose_bounded := (ltac:(let v := get_feW_loose_bounded () in exact v)) (only parsing).
Ltac get_feW_limbwidths_bounded _ := get TAG.feW_limbwidths_bounded.
Notation feW_limbwidths_bounded := (ltac:(let v := get_feW_limbwidths_bounded () in exact v)) (only parsing).
Ltac get_feBW_tight _ := get TAG.feBW_tight.
Notation feBW_tight := (ltac:(let v := get_feBW_tight () in exact v)) (only parsing).
Ltac get_feBW_loose _ := get TAG.feBW_loose.
Notation feBW_loose := (ltac:(let v := get_feBW_loose () in exact v)) (only parsing).
Ltac get_feBW_limbwidths _ := get TAG.feBW_limbwidths.
Notation feBW_limbwidths := (ltac:(let v := get_feBW_limbwidths () in exact v)) (only parsing).
Ltac get_feBW_relax _ := get TAG.feBW_relax.
Notation feBW_relax := (ltac:(let v := get_feBW_relax () in exact v)) (only parsing).
Ltac get_feBW_relax_limbwidths_to_tight _ := get TAG.feBW_relax_limbwidths_to_tight.
Notation feBW_relax_limbwidths_to_tight := (ltac:(let v := get_feBW_relax_limbwidths_to_tight () in exact v)) (only parsing).
Ltac get_feBW_relax_limbwidths_to_loose _ := get TAG.feBW_relax_limbwidths_to_loose.
Notation feBW_relax_limbwidths_to_loose := (ltac:(let v := get_feBW_relax_limbwidths_to_loose () in exact v)) (only parsing).
Ltac get_feBW_tight_bounded _ := get TAG.feBW_tight_bounded.
Notation feBW_tight_bounded := (ltac:(let v := get_feBW_tight_bounded () in exact v)) (only parsing).
Ltac get_feBW_limbwidths_bounded _ := get TAG.feBW_limbwidths_bounded.
Notation feBW_limbwidths_bounded := (ltac:(let v := get_feBW_limbwidths_bounded () in exact v)) (only parsing).
Ltac get_phiW _ := get TAG.phiW.
Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing).
Ltac get_phiBW_tight _ := get TAG.phiBW_tight.
Notation phiBW_tight := (ltac:(let v := get_phiBW_tight () in exact v)) (only parsing).
Ltac get_phiBW_loose _ := get TAG.phiBW_loose.
Notation phiBW_loose := (ltac:(let v := get_phiBW_loose () in exact v)) (only parsing).
Ltac get_phiBW_limbwidths _ := get TAG.phiBW_limbwidths.
Notation phiBW_limbwidths := (ltac:(let v := get_phiBW_limbwidths () in exact v)) (only parsing).
End MakeReificationTypesPackage.
|
