Slightly faster reification

Be better at what we do and don't unfold for when proving interpretation
via [reflexivity].  This lets us handle the reification part of the
pipeline when we chose to have only one limb.

After    | File Name                                     | Before   || Change
--------------------------------------------------------------------------------
5m50.80s | Total                                         | 5m53.13s || -0m02.33s
--------------------------------------------------------------------------------
3m41.27s | Specific/IntegrationTestLadderstep            | 3m43.35s || -0m02.07s
1m30.39s | Specific/IntegrationTestLadderstep130         | 1m29.79s || +0m00.60s
0m13.60s | Specific/IntegrationTestMul                   | 0m13.52s || +0m00.08s
0m11.00s | Specific/IntegrationTestSub                   | 0m11.36s || -0m00.35s
0m03.50s | Compilers/TestCase                            | 0m03.64s || -0m00.14s
0m03.14s | Specific/FancyMachine256/Montgomery           | 0m03.26s || -0m00.11s
0m02.97s | Specific/FancyMachine256/Barrett              | 0m03.06s || -0m00.08s
0m01.88s | Specific/FancyMachine256/Core                 | 0m01.94s || -0m00.06s
0m00.68s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.78s || -0m00.09s
0m00.53s | Compilers/Z/Bounds/Pipeline                   | 0m00.54s || -0m00.01s
0m00.48s | Compilers/InputSyntax                         | 0m00.51s || -0m00.03s
0m00.46s | Compilers/Z/Reify                             | 0m00.50s || -0m00.03s
0m00.46s | Compilers/Z/Bounds/Pipeline/Glue              | 0m00.51s || -0m00.04s
0m00.44s | Compilers/Reify                               | 0m00.38s || +0m00.06s

2 files changed, 31 insertions, 17 deletions

diff --git a/src/Compilers/InputSyntax.v b/src/Compilers/InputSyntax.v
index 22f7cdd61..af2a6f277 100644
--- a/src/Compilers/InputSyntax.v
+++ b/src/Compilers/InputSyntax.v
@@ -5,6 +5,7 @@ Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Compilers.InterpProofs.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Notations.
 
@@ -60,7 +61,7 @@ Section language.
            | Const _ x => x
            | Var _ x => x
            | Op _ _ op args => @interp_op _ _ op (@interpf _ args)
-           | LetIn _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x)
+           | LetIn _ ex _ eC => dlet x := @interpf _ ex in @interpf _ (eC x)
            | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey)
            | MatchPair _ _ ex _ eC => match @interpf _ ex with pair x y => @interpf _ (eC x y) end
            end.
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index bfe94d857..5739d3096 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.DebugPrint.
 (*Require Import Crypto.Util.Tactics.PrintContext.*)
 Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.SubstLet.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.TransparentAssert.
@@ -329,23 +330,34 @@ Ltac reify_abs base_type_code interp_base_type op var e :=
   let reifyf_term e := reifyf base_type_code interp_base_type op var e in
   let mkReturn ef := constr:(Return (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ef) in
   let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in
-  let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in
+  let reify_pretag := constr:(@exprf base_type_code interp_base_type op) in
+  let reify_tag := constr:(reify_pretag var) in
   let dummy := debug_enter_reify_abs e in
-  lazymatch e with
-  | (fun x : ?T => ?C) =>
+  lazymatch goal with
+  | [ re := ?rev : forall var' (x : ?T) (not_x : var' _), reify (reify_pretag var') (e x) |- _ ] =>
+    (* fast path *)
     let t := reify_flat_type T in
-    (* Work around Coq 8.5 and 8.6 bug *)
-    (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
-    (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
-    (* even if its Gallina name matches a Ltac in this tactic. *)
-    let maybe_x := fresh x in
-    let not_x := fresh x in
-    lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
-                        (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *)
-    with fun _ v _ => @?C v => mkAbs t C end
-  | ?x =>
-    let xv := reifyf_term x in
-    mkReturn xv
+    let F := lazymatch (eval cbv beta in (rev var)) with
+             | fun _ => ?C => C
+             end in
+    mkAbs t F
+  | _ =>
+    lazymatch e with
+    | (fun x : ?T => ?C) =>
+      let t := reify_flat_type T in
+      (* Work around Coq 8.5 and 8.6 bug *)
+      (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
+      (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
+      (* even if its Gallina name matches a Ltac in this tactic. *)
+      let maybe_x := fresh x in
+      let not_x := fresh x in
+      lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
+                          (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *)
+      with fun _ v _ => @?C v => mkAbs t C end
+    | ?x =>
+      let xv := reifyf_term x in
+      mkReturn xv
+    end
   end.
 
 Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
@@ -410,7 +422,8 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac :=
                            change interp_base_type with interp_base_type';
                            change interp_op with interp_op'
                       end;
-                      cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_type_gen_hetero interp_flat_type interp interpf]; reflexivity)) ] ] ].
+                      subst_let;
+                      cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_type_gen_hetero interp_flat_type interp interpf InputSyntax.Fst InputSyntax.Snd]; reflexivity)) ] ] ].
 
 Ltac prove_compile_correct_using tac :=
   fun _ => intros;