blob: a83adb29c227328128619b1e1b8b8feaeef48439 (
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
|
(* This file is autogenerated from Defaults.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Defaults.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
End TAG.
Ltac add_carry_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.carry_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let carry_chains := Tag.get pkg TAG.carry_chains in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let wt_divides_chains := Tag.get pkg TAG.wt_divides_chains in
let carry_sig := fresh "carry_sig" in
let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in
constr:(carry_sig)).
Ltac add_zero_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.zero_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let zero_sig := fresh "zero_sig" in
let zero_sig := pose_zero_sig sz m wt zero_sig in
constr:(zero_sig)).
Ltac add_one_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.one_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let one_sig := fresh "one_sig" in
let one_sig := pose_one_sig sz m wt one_sig in
constr:(one_sig)).
Ltac add_a24_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.a24_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let a24 := Tag.get pkg TAG.a24 in
let a24_sig := fresh "a24_sig" in
let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
constr:(a24_sig)).
Ltac add_add_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.add_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let add_sig := fresh "add_sig" in
let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in
constr:(add_sig)).
Ltac add_sub_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.sub_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let coef := Tag.get pkg TAG.coef in
let sub_sig := fresh "sub_sig" in
let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in
constr:(sub_sig)).
Ltac add_opp_sig pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.opp_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let coef := Tag.get pkg TAG.coef in
let opp_sig := fresh "opp_sig" in
let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in
constr:(opp_sig)).
Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq :=
Tag.update_by_tac_if_not_exists
pkg
TAG.mul_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let sz2 := Tag.get pkg TAG.sz2 in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let mul_sig := fresh "mul_sig" in
let mul_sig := pose_mul_sig P_default_mul P_extra_prove_mul_eq sz m wt s c sz2 wt_nonzero mul_sig in
constr:(mul_sig)).
Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq :=
Tag.update_by_tac_if_not_exists
pkg
TAG.square_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let s := Tag.get pkg TAG.s in
let c := Tag.get pkg TAG.c in
let sz2 := Tag.get pkg TAG.sz2 in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let square_sig := fresh "square_sig" in
let square_sig := pose_square_sig P_default_square P_extra_prove_square_eq sz m wt s c sz2 wt_nonzero square_sig in
constr:(square_sig)).
Ltac add_ring pkg :=
Tag.update_by_tac_if_not_exists
pkg
TAG.ring
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let m := Tag.get pkg TAG.m in
let wt := Tag.get pkg TAG.wt in
let wt_divides' := Tag.get pkg TAG.wt_divides' in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
let zero_sig := Tag.get pkg TAG.zero_sig in
let one_sig := Tag.get pkg TAG.one_sig in
let opp_sig := Tag.get pkg TAG.opp_sig in
let add_sig := Tag.get pkg TAG.add_sig in
let sub_sig := Tag.get pkg TAG.sub_sig in
let mul_sig := Tag.get pkg TAG.mul_sig in
let ring := fresh "ring" in
let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in
constr:(ring)).
Ltac add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq :=
let pkg := add_carry_sig pkg in
let pkg := add_zero_sig pkg in
let pkg := add_one_sig pkg in
let pkg := add_a24_sig pkg in
let pkg := add_add_sig pkg in
let pkg := add_sub_sig pkg in
let pkg := add_opp_sig pkg in
let pkg := add_mul_sig pkg P_default_mul P_extra_prove_mul_eq in
let pkg := add_square_sig pkg P_default_square P_extra_prove_square_eq in
let pkg := add_ring pkg in
Tag.strip_local pkg.
Module MakeDefaultsPackage (PKG : PrePackage).
Module Import MakeDefaultsPackageInternal := MakePackageBase PKG.
Ltac get_carry_sig _ := get TAG.carry_sig.
Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing).
Ltac get_zero_sig _ := get TAG.zero_sig.
Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
Ltac get_one_sig _ := get TAG.one_sig.
Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing).
Ltac get_a24_sig _ := get TAG.a24_sig.
Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
Ltac get_add_sig _ := get TAG.add_sig.
Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
Ltac get_sub_sig _ := get TAG.sub_sig.
Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing).
Ltac get_opp_sig _ := get TAG.opp_sig.
Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing).
Ltac get_mul_sig _ := get TAG.mul_sig.
Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing).
Ltac get_square_sig _ := get TAG.square_sig.
Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing).
Ltac get_ring _ := get TAG.ring.
Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing).
End MakeDefaultsPackage.
|
