blob: 4108c8352d910a1c0e42b67d3ddb358ec28c96c2 (
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
|
(* This file is autogenerated from Ladderstep.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := a24' | a24_sig | Mxzladderstep_sig.
End TAG.
Ltac add_a24' pkg :=
if_ladderstep
pkg
ltac:(fun _ => Tag.update_by_tac_if_not_exists
pkg
TAG.a24'
ltac:(fun _ => let a24 := Tag.get pkg TAG.a24 in
let a24' := fresh "a24'" in
let a24' := pose_a24' a24 a24' in
constr:(a24')))
ltac:(fun _ => pkg)
().
Ltac add_a24_sig pkg :=
if_ladderstep
pkg
ltac:(fun _ => 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:(fun _ => pkg)
().
Ltac add_Mxzladderstep_sig pkg :=
if_ladderstep
pkg
ltac:(fun _ => Tag.update_by_tac_if_not_exists
pkg
TAG.Mxzladderstep_sig
ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m 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 square_sig := Tag.get pkg TAG.square_sig in
let carry_sig := Tag.get pkg TAG.carry_sig in
let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
constr:(Mxzladderstep_sig)))
ltac:(fun _ => pkg)
().
Ltac add_Ladderstep_package pkg :=
let pkg := add_a24' pkg in
let pkg := add_a24_sig pkg in
let pkg := add_Mxzladderstep_sig pkg in
Tag.strip_subst_local pkg.
Module MakeLadderstepPackage (PKG : PrePackage).
Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
Ltac get_a24' _ := get TAG.a24'.
Notation a24' := (ltac:(let v := get_a24' () 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_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
End MakeLadderstepPackage.
|
