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