(* 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.