(* This file is autogenerated from Defaults.v by remake_packages.py *)
Require Import Crypto.Specific.Framework.CurveParametersPackage.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Defaults.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.

Module TAG.
  Inductive tags := carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
End TAG.

Ltac add_carry_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.carry_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 s := Tag.get pkg TAG.s in
                   let c := Tag.get pkg TAG.c in
                   let carry_chains := Tag.get pkg TAG.carry_chains in
                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let wt_divides_chains := Tag.get pkg TAG.wt_divides_chains in
                   let carry_sig := fresh "carry_sig" in
                   let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in
                   constr:(carry_sig)).
Ltac add_zero_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.zero_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 zero_sig := fresh "zero_sig" in
                   let zero_sig := pose_zero_sig sz m wt zero_sig in
                   constr:(zero_sig)).
Ltac add_one_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.one_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 one_sig := fresh "one_sig" in
                   let one_sig := pose_one_sig sz m wt one_sig in
                   constr:(one_sig)).
Ltac add_a24_sig pkg :=
  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 add_add_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.add_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 wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let add_sig := fresh "add_sig" in
                   let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in
                   constr:(add_sig)).
Ltac add_sub_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.sub_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 wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let coef := Tag.get pkg TAG.coef in
                   let sub_sig := fresh "sub_sig" in
                   let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in
                   constr:(sub_sig)).
Ltac add_opp_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.opp_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 wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let coef := Tag.get pkg TAG.coef in
                   let opp_sig := fresh "opp_sig" in
                   let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in
                   constr:(opp_sig)).
Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.mul_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 s := Tag.get pkg TAG.s in
                   let c := Tag.get pkg TAG.c in
                   let sz2 := Tag.get pkg TAG.sz2 in
                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let mul_sig := fresh "mul_sig" in
                   let mul_sig := pose_mul_sig P_default_mul P_extra_prove_mul_eq sz m wt s c sz2 wt_nonzero mul_sig in
                   constr:(mul_sig)).
Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.square_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 s := Tag.get pkg TAG.s in
                   let c := Tag.get pkg TAG.c in
                   let sz2 := Tag.get pkg TAG.sz2 in
                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let square_sig := fresh "square_sig" in
                   let square_sig := pose_square_sig P_default_square P_extra_prove_square_eq sz m wt s c sz2 wt_nonzero square_sig in
                   constr:(square_sig)).
Ltac add_ring pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.ring
    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 wt_divides' := Tag.get pkg TAG.wt_divides' in
                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                   let wt_nonzero := Tag.get pkg TAG.wt_nonzero in
                   let zero_sig := Tag.get pkg TAG.zero_sig in
                   let one_sig := Tag.get pkg TAG.one_sig in
                   let opp_sig := Tag.get pkg TAG.opp_sig 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 ring := fresh "ring" in
                   let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in
                   constr:(ring)).
Ltac add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq :=
  let pkg := add_carry_sig pkg in
  let pkg := add_zero_sig pkg in
  let pkg := add_one_sig pkg in
  let pkg := add_a24_sig pkg in
  let pkg := add_add_sig pkg in
  let pkg := add_sub_sig pkg in
  let pkg := add_opp_sig pkg in
  let pkg := add_mul_sig pkg P_default_mul P_extra_prove_mul_eq in
  let pkg := add_square_sig pkg P_default_square P_extra_prove_square_eq in
  let pkg := add_ring pkg in
  Tag.strip_local pkg.


Module MakeDefaultsPackage (PKG : PrePackage).
  Module Import MakeDefaultsPackageInternal := MakePackageBase PKG.

  Ltac get_carry_sig _ := get TAG.carry_sig.
  Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing).
  Ltac get_zero_sig _ := get TAG.zero_sig.
  Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing).
  Ltac get_one_sig _ := get TAG.one_sig.
  Notation one_sig := (ltac:(let v := get_one_sig () 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_add_sig _ := get TAG.add_sig.
  Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing).
  Ltac get_sub_sig _ := get TAG.sub_sig.
  Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing).
  Ltac get_opp_sig _ := get TAG.opp_sig.
  Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing).
  Ltac get_mul_sig _ := get TAG.mul_sig.
  Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing).
  Ltac get_square_sig _ := get TAG.square_sig.
  Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing).
  Ltac get_ring _ := get TAG.ring.
  Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing).
End MakeDefaultsPackage.