(* 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 := mul_code_correct | square_code_correct | carry_sig | zero_sig | one_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring.
End TAG.

Ltac add_mul_code_correct pkg P_extra_prove_mul_eq :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.mul_code_correct
    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
                   let sz2 := Tag.get pkg TAG.sz2 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 mul_code := Tag.get pkg TAG.mul_code in
                   let mul_code_correct := fresh "mul_code_correct" in
                   let mul_code_correct := pose_mul_code_correct P_extra_prove_mul_eq sz sz2 wt s c mul_code mul_code_correct in
                   constr:(mul_code_correct)).
Ltac add_square_code_correct pkg P_extra_prove_square_eq :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.square_code_correct
    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
                   let sz2 := Tag.get pkg TAG.sz2 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 square_code := Tag.get pkg TAG.square_code in
                   let square_code_correct := fresh "square_code_correct" in
                   let square_code_correct := pose_square_code_correct P_extra_prove_square_eq sz sz2 wt s c square_code square_code_correct in
                   constr:(square_code_correct)).
Ltac add_carry_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.carry_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 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 carry_sig := fresh "carry_sig" in
                   let carry_sig := pose_carry_sig wt m base sz s c carry_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 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 sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                   let base_pos := Tag.get pkg TAG.base_pos in
                   let zero_sig := fresh "zero_sig" in
                   let zero_sig := pose_zero_sig wt m base sz sz_nonzero base_pos 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 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 sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                   let base_pos := Tag.get pkg TAG.base_pos in
                   let one_sig := fresh "one_sig" in
                   let one_sig := pose_one_sig wt m base sz sz_nonzero base_pos one_sig in
                   constr:(one_sig)).
Ltac add_add_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.add_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 add_sig := fresh "add_sig" in
                   let add_sig := pose_add_sig wt m base sz 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 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 coef := Tag.get pkg TAG.coef in
                   let sub_sig := fresh "sub_sig" in
                   let sub_sig := pose_sub_sig wt m base sz 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 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 coef := Tag.get pkg TAG.coef in
                   let opp_sig := fresh "opp_sig" in
                   let opp_sig := pose_opp_sig wt m base sz coef opp_sig in
                   constr:(opp_sig)).
Ltac add_mul_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.mul_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 s := Tag.get pkg TAG.s in
                   let c := Tag.get pkg TAG.c in
                   let mul_code := Tag.get pkg TAG.mul_code in
                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                   let s_nonzero := Tag.get pkg TAG.s_nonzero in
                   let base_pos := Tag.get pkg TAG.base_pos in
                   let mul_code_correct := Tag.get pkg TAG.mul_code_correct in
                   let mul_sig := fresh "mul_sig" in
                   let mul_sig := pose_mul_sig wt m base sz s c mul_code sz_nonzero s_nonzero base_pos mul_code_correct mul_sig in
                   constr:(mul_sig)).
Ltac add_square_sig pkg :=
  Tag.update_by_tac_if_not_exists
    pkg
    TAG.square_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 s := Tag.get pkg TAG.s in
                   let c := Tag.get pkg TAG.c in
                   let square_code := Tag.get pkg TAG.square_code in
                   let sz_nonzero := Tag.get pkg TAG.sz_nonzero in
                   let s_nonzero := Tag.get pkg TAG.s_nonzero in
                   let base_pos := Tag.get pkg TAG.base_pos in
                   let square_code_correct := Tag.get pkg TAG.square_code_correct in
                   let square_sig := fresh "square_sig" in
                   let square_sig := pose_square_sig wt m base sz s c square_code sz_nonzero s_nonzero base_pos square_code_correct 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_extra_prove_mul_eq P_extra_prove_square_eq :=
  let pkg := add_mul_code_correct pkg P_extra_prove_mul_eq in
  let pkg := add_square_code_correct pkg P_extra_prove_square_eq in
  let pkg := add_carry_sig pkg in
  let pkg := add_zero_sig pkg in
  let pkg := add_one_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 in
  let pkg := add_square_sig pkg in
  let pkg := add_ring pkg in
  Tag.strip_subst_local pkg.


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

  Ltac get_mul_code_correct _ := get TAG.mul_code_correct.
  Notation mul_code_correct := (ltac:(let v := get_mul_code_correct () in exact v)) (only parsing).
  Ltac get_square_code_correct _ := get TAG.square_code_correct.
  Notation square_code_correct := (ltac:(let v := get_square_code_correct () in exact v)) (only parsing).
  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_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.