diff options
Diffstat (limited to 'src/Specific/Framework/ReificationTypesPackage.v')
| -rw-r--r-- | src/Specific/Framework/ReificationTypesPackage.v | 282 |
1 files changed, 0 insertions, 282 deletions
diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v deleted file mode 100644 index d10d72202..000000000 --- a/src/Specific/Framework/ReificationTypesPackage.v +++ /dev/null @@ -1,282 +0,0 @@ -(* 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. |