Replace curve-specific definitions with tactics

This requires Coq >= 8.7

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
11m15.52s | Total                                              | 11m14.53s || +0m00.99s
---------------------------------------------------------------------------------------
0m31.11s  | Specific/X25519/C32/Synthesis                      |    N/A    || +0m31.10s
   N/A    | Specific/X25519/C32/ArithmeticSynthesisTest        | 0m30.80s  || -0m30.80s
0m09.61s  | Specific/X25519/C64/Synthesis                      |    N/A    || +0m09.60s
   N/A    | Specific/X25519/C64/ArithmeticSynthesisTest        | 0m08.56s  || -0m08.56s
1m54.56s  | Specific/X25519/C64/ladderstep                     | 1m56.56s  || -0m02.00s
1m21.50s  | Specific/IntegrationTestKaratsubaMul               | 1m22.98s  || -0m01.48s
1m15.96s  | Specific/IntegrationTestLadderstep130              | 1m14.08s  || +0m01.88s
0m51.80s  | Specific/X25519/C32/femul                          | 0m53.79s  || -0m01.99s
1m51.81s  | Specific/NISTP256/AMD64/femul                      | 1m51.27s  || +0m00.53s
0m28.68s  | Specific/X25519/C32/fesquare                       | 0m28.30s  || +0m00.37s
0m25.45s  | Specific/IntegrationTestMontgomeryP256_128         | 0m25.60s  || -0m00.15s
0m18.81s  | Specific/NISTP256/AMD64/fesub                      | 0m18.32s  || +0m00.48s
0m16.01s  | Specific/NISTP256/AMD64/feadd                      | 0m15.86s  || +0m00.15s
0m15.15s  | Specific/NISTP256/AMD64/feopp                      | 0m14.95s  || +0m00.20s
0m12.42s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m12.15s  || +0m00.26s
0m12.41s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m12.31s  || +0m00.09s
0m11.10s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m11.31s  || -0m00.21s
0m10.70s  | Specific/X25519/C64/femul                          | 0m10.17s  || +0m00.52s
0m09.94s  | Specific/NISTP256/AMD64/fenz                       | 0m09.94s  || +0m00.00s
0m09.37s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.36s  || +0m00.00s
0m08.78s  | Specific/IntegrationTestSub                        | 0m08.84s  || -0m00.06s
0m07.98s  | Specific/IntegrationTestFreeze                     | 0m08.12s  || -0m00.13s
0m07.42s  | Specific/X25519/C64/fesquare                       | 0m07.22s  || +0m00.20s
0m00.99s  | Specific/SynthesisFramework                        |    N/A    || +0m00.99s
0m00.88s  | Specific/ReificationTypes                          | 0m00.91s  || -0m00.03s
0m00.85s  | Specific/ArithmeticSynthesisFramework              |    N/A    || +0m00.85s
   N/A    | Specific/X25519/C32/ReificationTypes               | 0m00.82s  || -0m00.82s
   N/A    | Specific/X25519/C64/ReificationTypes               | 0m00.77s  || -0m00.77s
0m00.77s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.79s  || -0m00.02s
0m00.72s  | Specific/LadderstepSynthesisFramework              |    N/A    || +0m00.72s
0m00.38s  | Specific/IntegrationTestDisplayCommon              | 0m00.40s  || -0m00.02s
0m00.36s  | Specific/IntegrationTestDisplayCommonTactics       | 0m00.35s  || +0m00.01s

1 files changed, 22 insertions, 16 deletions

diff --git a/src/Specific/ReificationTypes.v b/src/Specific/ReificationTypes.v
index cc705689b..3a160e04d 100644
--- a/src/Specific/ReificationTypes.v
+++ b/src/Specific/ReificationTypes.v
@@ -139,7 +139,7 @@ Ltac pose_phiBW feBW m wt phiBW :=
     ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
            phiBW.
 
-Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent :=
+Ltac get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent :=
   let limb_widths := fresh "limb_widths" in
   let bounds_exp := fresh "bounds_exp" in
   let bounds := fresh "bounds" in
@@ -166,12 +166,12 @@ Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_expone
   let phiW := pose_phiW feW m wt phiW in
   let phiBW := pose_phiBW feBW m wt phiBW in
   constr:((feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW)).
-Ltac make_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent :=
+Ltac make_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent :=
   lazymatch goal with
   | [ |- { T : _ & T } ] => eexists
   | [ |- _ ] => idtac
   end;
-  let pkg := get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent in
+  let pkg := get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent in
   exact pkg.
 
 Module Type ReificationTypesPrePackage.
@@ -180,22 +180,28 @@ Module Type ReificationTypesPrePackage.
 End ReificationTypesPrePackage.
 
 Module MakeReificationTypes (RP : ReificationTypesPrePackage).
-  Definition ReificationTypes_package := RP.ReificationTypes_package.
-  Ltac reduce_proj x :=
-    let RP_ReificationTypes_package := (eval cbv [ReificationTypes_package] in ReificationTypes_package) in
-    let v := (eval cbv [ReificationTypes_package RP_ReificationTypes_package] in x) in
-    exact v.
+  Ltac get_ReificationTypes_package _ := eval hnf in RP.ReificationTypes_package.
+  Ltac RT_reduce_proj x :=
+    eval cbv beta iota zeta in x.
   (**
 <<
 terms = 'feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW'
 for i in terms.split(', '):
-    print("  Notation %s := (ltac:(reduce_proj (let '(%s) := ReificationTypes_package in %s))) (only parsing)." % (i, terms, i))
+    print("  Ltac get_%s _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(%s) := pkg in %s)." % (i, terms, i))
+    print("  Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (i, i))
 >> *)
-  Notation feZ := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feZ))) (only parsing).
-  Notation feW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW))) (only parsing).
-  Notation feW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW_bounded))) (only parsing).
-  Notation feBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW))) (only parsing).
-  Notation feBW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW_bounded))) (only parsing).
-  Notation phiW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiW))) (only parsing).
-  Notation phiBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiBW))) (only parsing).
+  Ltac get_feZ _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feZ).
+  Notation feZ := (ltac:(let v := get_feZ () in exact v)) (only parsing).
+  Ltac get_feW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW).
+  Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing).
+  Ltac get_feW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW_bounded).
+  Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing).
+  Ltac get_feBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW).
+  Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing).
+  Ltac get_feBW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW_bounded).
+  Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing).
+  Ltac get_phiW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiW).
+  Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing).
+  Ltac get_phiBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiBW).
+  Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing).
 End MakeReificationTypes.