blob: 18fef6cc9734154cbba334665bff169268303b63 (
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
|
(* This file is autogenerated from Freeze.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Freeze.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
Module TAG.
Inductive tags := m_correct_wt | freeze_sig.
End TAG.
Ltac add_m_correct_wt pkg :=
if_freeze
pkg
ltac:(fun _ => Tag.update_by_tac_if_not_exists
pkg
TAG.m_correct_wt
ltac:(fun _ => let m := Tag.get pkg TAG.m in
let c := Tag.get pkg TAG.c in
let sz := Tag.get pkg TAG.sz in
let wt := Tag.get pkg TAG.wt in
let m_correct_wt := fresh "m_correct_wt" in
let m_correct_wt := pose_m_correct_wt m c sz wt m_correct_wt in
constr:(m_correct_wt)))
ltac:(fun _ => pkg)
().
Ltac add_freeze_sig pkg :=
if_freeze
pkg
ltac:(fun _ => Tag.update_by_tac_if_not_exists
pkg
TAG.freeze_sig
ltac:(fun _ => let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let base := Tag.get pkg TAG.base in
let sz := Tag.get pkg TAG.sz in
let c := Tag.get pkg TAG.c in
let bitwidth := Tag.get pkg TAG.bitwidth in
let m_enc := Tag.get pkg TAG.m_enc in
let base_pos := Tag.get pkg TAG.base_pos in
let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
let freeze_sig := fresh "freeze_sig" in
let freeze_sig := pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig in
constr:(freeze_sig)))
ltac:(fun _ => pkg)
().
Ltac add_Freeze_package pkg :=
let pkg := add_m_correct_wt pkg in
let pkg := add_freeze_sig pkg in
Tag.strip_subst_local pkg.
Module MakeFreezePackage (PKG : PrePackage).
Module Import MakeFreezePackageInternal := MakePackageBase PKG.
Ltac get_m_correct_wt _ := get TAG.m_correct_wt.
Notation m_correct_wt := (ltac:(let v := get_m_correct_wt () in exact v)) (only parsing).
Ltac get_freeze_sig _ := get TAG.freeze_sig.
Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
End MakeFreezePackage.
|
