1 files changed, 112 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/LegacySynthesisTactics.v b/src/PushButtonSynthesis/LegacySynthesisTactics.v
new file mode 100644
index 000000000..c2ae24f7c
--- /dev/null
+++ b/src/PushButtonSynthesis/LegacySynthesisTactics.v
@@ -0,0 +1,112 @@
+(** * Push-Button Synthesis: Legacy Synthesis Tactics *)
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.LanguageWf.
+Require Import Crypto.Language.
+Require Import Crypto.PushButtonSynthesis.ReificationCache.
+Require Import Crypto.Util.Equality. (* fg_equal_rel *)
+Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Crypto.Util.Tactics.GetGoal.
+
+Import
+  LanguageWf.Compilers
+  Language.Compilers.
+Import Compilers.defaults.
+
+(** TODO: Port Barrett and Montgomery to the new glue style, and remove these tactics.  These tactics are only needed for the old-glue-style derivations. *)
+Ltac peel_interp_app _ :=
+  lazymatch goal with
+  | [ |- ?R' (?InterpE ?arg) (?f ?arg) ]
+    => apply fg_equal_rel; [ | reflexivity ];
+       try peel_interp_app ()
+  | [ |- ?R' (Interp ?ev) (?f ?x) ]
+    => let sv := type of x in
+       let fx := constr:(f x) in
+       let dv := type of fx in
+       let rs := reify_type sv in
+       let rd := reify_type dv in
+       etransitivity;
+       [ apply @expr.Interp_APP_rel_reflexive with (s:=rs) (d:=rd) (R:=R');
+         typeclasses eauto
+       | apply fg_equal_rel;
+         [ try peel_interp_app ()
+         | try lazymatch goal with
+               | [ |- ?R (Interp ?ev) (Interp _) ]
+                 => reflexivity
+               | [ |- ?R (Interp ?ev) ?c ]
+                 => let rc := constr:(GallinaReify.Reify c) in
+                    unify ev rc; vm_compute; reflexivity
+               end ] ]
+  end.
+Ltac pre_cache_reify _ :=
+  let H' := fresh in
+  lazymatch goal with
+  | [ |- ?P /\ Wf ?e ]
+    => let P' := fresh in
+       evar (P' : Prop);
+       assert (H' : P' /\ Wf e); subst P'
+  end;
+  [
+      | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ];
+        cbv [type.app_curried];
+        let arg := fresh "arg" in
+        let arg2 := fresh in
+        intros arg arg2;
+        cbn [type.and_for_each_lhs_of_arrow type.eqv];
+        let H := fresh in
+        intro H;
+        repeat match type of H with
+               | and _ _ => let H' := fresh in
+                            destruct H as [H' H];
+                            rewrite <- H'
+               end;
+        clear dependent arg2; clear H;
+        intros _;
+        peel_interp_app ();
+        [ lazymatch goal with
+          | [ |- ?R (Interp ?ev) _ ]
+            => (tryif is_evar ev
+                 then let ev' := fresh "ev" in set (ev' := ev)
+                 else idtac)
+          end;
+          cbv [pointwise_relation];
+          repeat lazymatch goal with
+                 | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1
+                                           | revert H ]
+                 end;
+          eexact H'
+        | .. ] ];
+  [ intros; clear | .. ].
+Ltac do_inline_cache_reify do_if_not_cached :=
+  pre_cache_reify ();
+  [ try solve [
+          cbv beta zeta;
+          repeat match goal with H := ?e |- _ => is_evar e; subst H end;
+          try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ];
+          do_if_not_cached ()
+        ];
+    cache_reify ()
+  | .. ].
+
+(* TODO: MOVE ME *)
+Ltac vm_compute_lhs_reflexivity :=
+  lazymatch goal with
+  | [ |- ?LHS = ?RHS ]
+    => let x := (eval vm_compute in LHS) in
+       (* we cannot use the unify tactic, which just gives "not
+          unifiable" as the error message, because we want to see the
+          terms that were not unifable.  See also
+          COQBUG(https://github.com/coq/coq/issues/7291) *)
+       let _unify := constr:(ltac:(reflexivity) : RHS = x) in
+       vm_cast_no_check (eq_refl x)
+  end.
+
+Ltac solve_rop' rop_correct do_if_not_cached machine_wordsizev :=
+  eapply rop_correct with (machine_wordsize:=machine_wordsizev);
+  [ do_inline_cache_reify do_if_not_cached
+  | subst_evars; vm_compute_lhs_reflexivity (* lazy; reflexivity *) ].
+Ltac solve_rop_nocache rop_correct :=
+  solve_rop' rop_correct ltac:(fun _ => idtac).
+Ltac solve_rop rop_correct :=
+  solve_rop'
+    rop_correct
+    ltac:(fun _ => let G := get_goal in fail 2 "Could not find a solution in reify_gen_cache for" G).