(* 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 | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_bounded | feBW | feBW_bounded | phiW | phiBW.
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 pkg :=
  let sz := Tag.get pkg TAG.sz in
  let upper_bound_of_exponent := Tag.get pkg TAG.upper_bound_of_exponent in
  let bounds_exp := Tag.get pkg TAG.bounds_exp in
  let bounds := fresh "bounds" in
  let bounds := pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds in
  Tag.local_update pkg TAG.bounds bounds.

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 limb_widths := Tag.get pkg TAG.limb_widths in
  let lgbitwidth := fresh "lgbitwidth" in
  let lgbitwidth := pose_local_lgbitwidth limb_widths 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_bounded pkg :=
  let feW := Tag.get pkg TAG.feW in
  let bounds := Tag.get pkg TAG.bounds in
  let feW_bounded := fresh "feW_bounded" in
  let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
  Tag.update pkg TAG.feW_bounded feW_bounded.

Ltac add_feBW pkg :=
  let sz := Tag.get pkg TAG.sz in
  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
  let bounds := Tag.get pkg TAG.bounds in
  let feBW := fresh "feBW" in
  let feBW := pose_feBW sz adjusted_bitwidth' bounds feBW in
  Tag.update pkg TAG.feBW feBW.

Ltac add_feBW_bounded pkg :=
  let wt := Tag.get pkg TAG.wt in
  let sz := Tag.get pkg TAG.sz in
  let feBW := Tag.get pkg TAG.feBW in
  let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in
  let bounds := Tag.get pkg TAG.bounds in
  let m := Tag.get pkg TAG.m in
  let wt_nonneg := Tag.get pkg TAG.wt_nonneg in
  let feBW_bounded := fresh "feBW_bounded" in
  let feBW_bounded := pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded in
  Tag.update pkg TAG.feBW_bounded feBW_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 pkg :=
  let feBW := Tag.get pkg TAG.feBW in
  let m := Tag.get pkg TAG.m in
  let wt := Tag.get pkg TAG.wt in
  let phiBW := fresh "phiBW" in
  let phiBW := pose_phiBW feBW m wt phiBW in
  Tag.update pkg TAG.phiBW phiBW.

Ltac add_ReificationTypes_package pkg :=
  let pkg := add_limb_widths pkg in
  let pkg := add_bounds_exp pkg in
  let pkg := add_bounds 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_bounded pkg in
  let pkg := add_feBW pkg in
  let pkg := add_feBW_bounded pkg in
  let pkg := add_phiW pkg in
  let pkg := add_phiBW pkg in
  Tag.strip_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_bounded _ := get TAG.feW_bounded.
  Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
  Ltac get_feBW _ := get TAG.feBW.
  Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
  Ltac get_feBW_bounded _ := get TAG.feBW_bounded.
  Notation feBW_bounded := (ltac:(let v := get_feBW_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 _ := get TAG.phiBW.
  Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
End MakeReificationTypesPackage.