blob: f0703b4accd75b8ab51d6c9c41038d0b3591aa1d (
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
|
(* 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 | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_bounded | feBW | feBW_bounded | phiW | phiBW.
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 pkg :=
let sz := Tag.get pkg TAG.sz in
let upper_bound_of_exponent := Tag.get pkg TAG.upper_bound_of_exponent in
let bounds_exp := Tag.get pkg TAG.bounds_exp in
let bounds := fresh "bounds" in
let bounds := pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds in
Tag.local_update pkg TAG.bounds bounds.
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_bounded pkg :=
let feW := Tag.get pkg TAG.feW in
let bounds := Tag.get pkg TAG.bounds in
let feW_bounded := fresh "feW_bounded" in
let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
Tag.update pkg TAG.feW_bounded feW_bounded.
Ltac add_feBW pkg :=
let sz := Tag.get pkg TAG.sz in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds := Tag.get pkg TAG.bounds in
let feBW := fresh "feBW" in
let feBW := pose_feBW sz adjusted_bitwidth' bounds feBW in
Tag.update pkg TAG.feBW feBW.
Ltac add_feBW_bounded pkg :=
let wt := Tag.get pkg TAG.wt in
let sz := Tag.get pkg TAG.sz in
let feBW := Tag.get pkg TAG.feBW in
let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
let bounds := Tag.get pkg TAG.bounds in
let m := Tag.get pkg TAG.m in
let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
let feBW_bounded := fresh "feBW_bounded" in
let feBW_bounded := pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded in
Tag.update pkg TAG.feBW_bounded feBW_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 pkg :=
let feBW := Tag.get pkg TAG.feBW in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let phiBW := fresh "phiBW" in
let phiBW := pose_phiBW feBW m wt phiBW in
Tag.update pkg TAG.phiBW phiBW.
Ltac add_ReificationTypes_package pkg :=
let pkg := add_limb_widths pkg in
let pkg := add_bounds_exp pkg in
let pkg := add_bounds 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_bounded pkg in
let pkg := add_feBW pkg in
let pkg := add_feBW_bounded pkg in
let pkg := add_phiW pkg in
let pkg := add_phiBW 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_bounded _ := get TAG.feW_bounded.
Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
Ltac get_feBW _ := get TAG.feBW.
Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
Ltac get_feBW_bounded _ := get TAG.feBW_bounded.
Notation feBW_bounded := (ltac:(let v := get_feBW_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 _ := get TAG.phiBW.
Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
End MakeReificationTypesPackage.
|
