Speed up reification a little bit

This helps a lot more in C32 ladderstep; we eliminate useless typeclass
unification against hypotheses by separating out the typeclass used for
external overloading and posing hypotheses, and the typeclass used for
recursion under binders.

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
12m49.58s | Total                                              | 13m04.75s || -0m15.16s
---------------------------------------------------------------------------------------
2m48.67s  | Specific/X25519/C64/ladderstep                     | 2m58.05s  || -0m09.37s
2m21.65s  | Specific/NISTP256/AMD64/femul                      | 2m16.64s  || +0m05.01s
1m25.60s  | Specific/IntegrationTestKaratsubaMul               | 1m30.00s  || -0m04.40s
1m08.01s  | Specific/X25519/C32/femul                          | 1m12.17s  || -0m04.15s
1m08.25s  | Specific/IntegrationTestLadderstep130              | 1m11.61s  || -0m03.35s
0m39.67s  | Specific/X25519/C32/fesquare                       | 0m39.16s  || +0m00.51s
0m27.09s  | Specific/IntegrationTestMontgomeryP256_128         | 0m27.02s  || +0m00.07s
0m17.74s  | Specific/NISTP256/AMD64/fesub                      | 0m18.34s  || -0m00.60s
0m17.21s  | Specific/IntegrationTestFreeze                     | 0m16.37s  || +0m00.83s
0m15.89s  | Specific/NISTP256/AMD64/feadd                      | 0m15.31s  || +0m00.58s
0m14.78s  | Specific/NISTP256/AMD64/feopp                      | 0m14.73s  || +0m00.04s
0m14.47s  | Specific/X25519/C64/femul                          | 0m14.39s  || +0m00.08s
0m12.07s  | Specific/IntegrationTestSub                        | 0m11.76s  || +0m00.31s
0m12.07s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m11.93s  || +0m00.14s
0m11.79s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m12.00s  || -0m00.21s
0m10.84s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m10.90s  || -0m00.06s
0m10.08s  | Specific/X25519/C64/fesquare                       | 0m10.61s  || -0m00.52s
0m09.66s  | Specific/NISTP256/AMD64/fenz                       | 0m09.68s  || -0m00.01s
0m09.27s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.28s  || -0m00.00s
0m03.51s  | Compilers/TestCase                                 | 0m03.49s  || +0m00.01s
0m03.08s  | Specific/NISTP256/FancyMachine256/Montgomery       | 0m03.23s  || -0m00.14s
0m02.99s  | Specific/NISTP256/FancyMachine256/Barrett          | 0m03.00s  || -0m00.00s
0m02.16s  | Specific/NISTP256/FancyMachine256/Core             | 0m02.15s  || +0m00.01s
0m00.86s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics      | 0m00.84s  || +0m00.02s
0m00.68s  | Compilers/Z/Bounds/Pipeline                        | 0m00.61s  || +0m00.07s
0m00.56s  | Compilers/Z/Bounds/Pipeline/Glue                   | 0m00.54s  || +0m00.02s
0m00.54s  | Compilers/Z/Reify                                  | 0m00.54s  || +0m00.00s
0m00.40s  | Compilers/Reify                                    | 0m00.41s  || -0m00.00s

1 files changed, 41 insertions, 8 deletions

diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index b986722f8..4943eca86 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -64,6 +64,7 @@ Tactic Notation "debug_reifyf_case" string(case)
   := debug3 ltac:(fun _ => idtac "reifyf:" case).
 Ltac debug_enter_reify_abs e := debug2 ltac:(fun _ => debug_enter_reify_idtac "reify_abs:" e).
 
+Class reify_internal {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_internal : T.
 Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T.
 Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False.
 Arguments reify_var_for_in_is _ {T} _ _ {eT} _.
@@ -172,7 +173,13 @@ Ltac reifyf base_type_code interp_base_type op var e :=
   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_reifyf e in
-  match constr:(Set) with
+  match goal with
+  | [ re := ?rev : reify reify_tag e |- _ ] =>
+    (* fast path *)
+    let dummy := debug_reifyf_case "hyp" in
+    let ret := rev in
+    let dummy := debug_leave_reifyf_success e ret in
+    ret
   | _ =>
     let ret :=
         lazymatch e with
@@ -202,7 +209,7 @@ Ltac reifyf base_type_code interp_base_type op var e :=
           let not_x := fresh x in
           let C' := match constr:(Set) with
                     | _ => constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
-                                     (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *)
+                                     (_ : reify_internal reify_tag C)) (* [C] here is an open term that references "x" by name *)
                     | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to reify by typeclasses:" e)
                     end in
           match constr:(Set) with
@@ -313,11 +320,24 @@ Ltac reifyf base_type_code interp_base_type op var e :=
   | _ => debug_leave_reifyf_failure e
   end.
 
+Ltac do_reifyf_goal _ :=
+  debug_enter_reify_rec;
+  let e := lazymatch goal with
+           | [ |- reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ]
+             => reifyf base_type_code interp_base_type op var e
+           | [ |- reify_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ]
+             => reifyf base_type_code interp_base_type op var e
+           end in
+  debug_leave_reify_rec e;
+  eexact e.
+
 Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
-=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e)
-   : typeclass_instances.
+=> do_reifyf_goal () : typeclass_instances.
+Hint Extern 0 (reify_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
+=> do_reifyf_goal () : typeclass_instances.
 
 (** For reification including [Abs] *)
+Class reify_abs_internal {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs_internal : T.
 Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T.
 Ltac reify_abs base_type_code interp_base_type op var e :=
   let reify_rec e := reify_abs base_type_code interp_base_type op var e in
@@ -347,7 +367,7 @@ Ltac reify_abs base_type_code interp_base_type op var e :=
       let not_x := fresh x in
       let C' := match constr:(Set) with
                 | _ => 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 *)
+                                 (_ : reify_abs_internal reify_tag C)) (* [C] here is an open term that references "x" by name *)
                 | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to reify by typeclasses:" e)
                 end in
       let C := match constr:(Set) with
@@ -362,11 +382,24 @@ Ltac reify_abs base_type_code interp_base_type op var e :=
     end
   end.
 
+Ltac do_reify_abs_goal _ :=
+  debug_enter_reify_rec;
+  let e := lazymatch goal with
+           | [ |- reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ]
+             => reify_abs base_type_code interp_base_type op var e
+           | [ |- reify_abs_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e ]
+             => reify_abs base_type_code interp_base_type op var e
+           end in
+  debug_leave_reify_rec e;
+  eexact e.
+
 Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
-=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances.
+=> do_reify_abs_goal () : typeclass_instances.
+Hint Extern 0 (reify_abs_internal (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e)
+=> do_reify_abs_goal () : typeclass_instances.
 
 Ltac Reify' base_type_code interp_base_type op e :=
-  lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with
+  lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs_internal (@exprf base_type_code interp_base_type op var) e)) with
     (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *)
   end.
 Ltac Reify base_type_code interp_base_type op make_const e :=
@@ -463,7 +496,7 @@ Ltac unique_reify_context_variable base_type_code interp_base_type op F Fbody rT
          => let maybe_x := fresh x in
             let not_x := fresh maybe_x in
             let rF := lazymatch constr:(fun var' (x : X) (not_x : var' src) (_ : reify_var_for_in_is base_type_code x src not_x)
-                                        => (_ : reify (reify_pretag var') Fbody'))
+                                        => (_ : reify_internal (reify_pretag var') Fbody'))
                       with
                       | fun (var' : ?VAR) (x : ?X) (v : ?V) _ => ?C
                         => constr:(fun (var' : VAR) (v : V) => C)