Replace the python script with Ltac code

We now rely on Ltac rather than python to generate the raw identifiers.

After     | File Name                                       | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------
22m05.90s | Total                                           | 21m51.87s || +0m14.03s | +1.07%
-----------------------------------------------------------------------------------------------
0m49.25s  | GENERATEDIdentifiersWithoutTypesProofs.vo       | 0m55.23s  || -0m05.97s | -10.82%
0m19.14s  | GENERATEDIdentifiersWithoutTypes.vo             | 0m13.35s  || +0m05.79s | +43.37%
0m36.52s  | ExtractionHaskell/saturated_solinas             | 0m32.60s  || +0m03.92s | +12.02%
0m24.00s  | SlowPrimeSynthesisExamples.vo                   | 0m27.22s  || -0m03.21s | -11.82%
0m08.55s  | ExtractionOCaml/saturated_solinas.ml            | 0m05.49s  || +0m03.06s | +55.73%
3m24.98s  | p384_32.c                                       | 3m22.52s  || +0m02.45s | +1.21%
1m03.78s  | ExtractionHaskell/word_by_word_montgomery       | 1m01.13s  || +0m02.64s | +4.33%
0m47.85s  | p521_32.c                                       | 0m45.77s  || +0m02.07s | +4.54%
1m42.64s  | Fancy/Barrett256.vo                             | 1m41.49s  || +0m01.14s | +1.13%
0m40.30s  | p521_64.c                                       | 0m42.20s  || -0m01.90s | -4.50%
0m18.02s  | p256_32.c                                       | 0m19.03s  || -0m01.01s | -5.30%
0m14.70s  | ExtractionOCaml/unsaturated_solinas             | 0m13.33s  || +0m01.36s | +10.27%
0m14.28s  | p434_64.c                                       | 0m15.39s  || -0m01.11s | -7.21%
0m09.82s  | p224_32.c                                       | 0m08.77s  || +0m01.05s | +11.97%
0m08.59s  | p384_64.c                                       | 0m07.36s  || +0m01.22s | +16.71%
0m05.18s  | ExtractionHaskell/saturated_solinas.hs          | 0m06.59s  || -0m01.41s | -21.39%
1m34.02s  | RewriterWf2.vo                                  | 1m34.23s  || -0m00.20s | -0.22%
0m56.16s  | Rewriter/ToFancyWithCasts.vo                    | 0m55.41s  || +0m00.75s | +1.35%
0m45.85s  | Rewriter/NBE.vo                                 | 0m45.23s  || +0m00.62s | +1.37%
0m44.51s  | Rewriter/ArithWithCasts.vo                      | 0m44.12s  || +0m00.39s | +0.88%
0m44.10s  | RewriterInterpProofs1.vo                        | 0m43.89s  || +0m00.21s | +0.47%
0m43.66s  | ExtractionHaskell/unsaturated_solinas           | 0m43.25s  || +0m00.40s | +0.94%
0m36.46s  | PushButtonSynthesis/UnsaturatedSolinas.vo       | 0m36.36s  || +0m00.10s | +0.27%
0m36.09s  | RewriterWf1.vo                                  | 0m36.07s  || +0m00.02s | +0.05%
0m34.50s  | Fancy/Montgomery256.vo                          | 0m34.30s  || +0m00.20s | +0.58%
0m27.13s  | PushButtonSynthesis/WordByWordMontgomery.vo     | 0m26.99s  || +0m00.14s | +0.51%
0m24.70s  | Rewriter/Arith.vo                               | 0m24.26s  || +0m00.43s | +1.81%
0m22.75s  | ExtractionOCaml/word_by_word_montgomery         | 0m22.15s  || +0m00.60s | +2.70%
0m20.96s  | PushButtonSynthesis/BarrettReduction.vo         | 0m20.74s  || +0m00.22s | +1.06%
0m18.96s  | p448_solinas_64.c                               | 0m19.32s  || -0m00.35s | -1.86%
0m18.16s  | secp256k1_32.c                                  | 0m18.13s  || +0m00.03s | +0.16%
0m14.62s  | ExtractionOCaml/word_by_word_montgomery.ml      | 0m13.77s  || +0m00.84s | +6.17%
0m11.84s  | ExtractionOCaml/saturated_solinas               | 0m11.30s  || +0m00.53s | +4.77%
0m09.55s  | ExtractionOCaml/unsaturated_solinas.ml          | 0m09.14s  || +0m00.41s | +4.48%
0m08.42s  | ExtractionHaskell/word_by_word_montgomery.hs    | 0m08.16s  || +0m00.25s | +3.18%
0m06.96s  | BoundsPipeline.vo                               | 0m06.85s  || +0m00.11s | +1.60%
0m06.54s  | ExtractionHaskell/unsaturated_solinas.hs        | 0m07.17s  || -0m00.62s | -8.78%
0m03.57s  | PushButtonSynthesis/Primitives.vo               | 0m03.46s  || +0m00.10s | +3.17%
0m03.35s  | PushButtonSynthesis/SmallExamples.vo            | 0m03.34s  || +0m00.01s | +0.29%
0m03.30s  | PushButtonSynthesis/SaturatedSolinas.vo         | 0m03.22s  || +0m00.07s | +2.48%
0m02.83s  | curve25519_32.c                                 | 0m02.86s  || -0m00.02s | -1.04%
0m02.70s  | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s  || +0m00.07s | +2.66%
0m02.08s  | Rewriter.vo                                     | 0m02.02s  || +0m00.06s | +2.97%
0m01.60s  | curve25519_64.c                                 | 0m01.82s  || -0m00.21s | -12.08%
0m01.47s  | secp256k1_64.c                                  | 0m01.94s  || -0m00.47s | -24.22%
0m01.34s  | p224_64.c                                       | 0m01.71s  || -0m00.36s | -21.63%
0m01.33s  | CLI.vo                                          | 0m01.38s  || -0m00.04s | -3.62%
0m01.32s  | p256_64.c                                       | 0m01.77s  || -0m00.44s | -25.42%
0m01.28s  | Rewriter/ToFancy.vo                             | 0m01.36s  || -0m00.08s | -5.88%
0m01.23s  | Rewriter/StripLiteralCasts.vo                   | 0m01.08s  || +0m00.14s | +13.88%
0m01.16s  | StandaloneHaskellMain.vo                        | 0m01.18s  || -0m00.02s | -1.69%
0m01.13s  | CompilersTestCases.vo                           | 0m01.18s  || -0m00.05s | -4.23%
0m01.07s  | StandaloneOCamlMain.vo                          | 0m01.12s  || -0m00.05s | -4.46%
0m00.83s  | RewriterAll.vo                                  | 0m00.66s  || +0m00.16s | +25.75%
0m00.78s  | RewriterAllTactics.vo                           | 0m00.83s  || -0m00.04s | -6.02%

1 files changed, 7 insertions, 18 deletions

diff --git a/src/Rewriter.v b/src/Rewriter.v
index 34107b2c2..e1b537959 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -531,23 +531,6 @@ Module Compilers.
                (fun T Ts rec f1 f2 => forall x, rec (f1 x) (f2 x))
                ls.
 
-        Definition app_type_of_list {K} {ls : list Type} (f : type_of_list_cps K ls) (args : type_of_list ls) : K
-          := list_rect
-               (fun ls
-                => type_of_list_cps K ls -> type_of_list ls -> K)
-               (fun v _ => v)
-               (fun T Ts rec f x
-                => rec (f (fst x)) (snd x))
-               ls
-               f args.
-
-        Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
-          := list_rect
-               (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls)
-               (fun f => f tt)
-               (fun T Ts rec k t => rec (fun ts => k (t, ts)))
-               ls.
-
         Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope.
         Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope.
 
@@ -2154,6 +2137,12 @@ Module Compilers.
           := Eval cbv [pattern.ident.of_typed_ident] in
               pattern.Ident (pattern.ident.of_typed_ident (@ident.Literal t DefaultValue.type.base.default)).
 
+        Let pident_pair
+          := ltac:(let v := (eval cbv [pattern.ident.of_typed_ident] in
+                                (fun A B => pattern.ident.of_typed_ident (@ident.pair A B))) in
+                   let h := lazymatch v with fun A B => ?f _ _ => f end in
+                   exact h).
+
         Fixpoint make_Literal_pattern (t : pattern.base.type) : option (pattern t)
           := match t return option (pattern t) with
              | pattern.base.type.var _ => None
@@ -2161,7 +2150,7 @@ Module Compilers.
              | pattern.base.type.prod A B
                => (a <- make_Literal_pattern A;
                     b <- make_Literal_pattern B;
-                    Some ((#pattern.ident.pair @ a @ b)%pattern))
+                    Some ((#(pident_pair _ _) @ a @ b)%pattern))
              | pattern.base.type.list A => None
              | pattern.base.type.option A => None
              end%option%cps.