Add Display files and targets

9 files changed, 105 insertions, 78 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index a04f3505c..15150eab1 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -181,7 +181,7 @@ Definition PipelineCorrect
             : e_final_newtype
               = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane))
            (** ** instantiation of original evar *)
-           (Hevar : final_e_evar = Interp (t:=Arrow _ _) Syntax.interp_op e_final_newtype v')
+           (Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v')
            (** ** side condition *)
            (Hv : Bounds.is_bounded_by input_bounds (cast_back_flat_const v'))
   : Bounds.is_bounded_by given_output_bounds (fZ (cast_back_flat_const v'))
@@ -196,7 +196,7 @@ Proof.
   clear Hwf He_unnatize_for_wf.
   symmetry in Hpost_correct.
   subst; cbv [proj1_sig] in *.
-  rewrite <- Hrexpr.
+  rewrite eq_InterpEta, <- Hrexpr.
   eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ].
   rewrite !@InterpPreWfPipeline in Hpost_correct.
   unshelve eapply relax_output_bounds; try eassumption; [].
diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v
new file mode 100644
index 000000000..a9955ad5b
--- /dev/null
+++ b/src/Specific/IntegrationTestDisplayCommon.v
@@ -0,0 +1,42 @@
+Require Import Crypto.Util.Sigma.Lift.
+Require Import Crypto.Util.Sigma.Associativity.
+Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Export Coq.ZArith.ZArith.
+Require Export Crypto.Util.LetIn.
+Require Export Crypto.Util.FixedWordSizes.
+Require Export Crypto.Compilers.Z.CNotations.
+
+Global Arguments Pos.to_nat !_ / .
+
+Ltac display_helper f :=
+  lazymatch type of f with
+  | forall _ : ?A, ?B
+    => let x := fresh "x" in
+       lazymatch (eval hnf in A) with
+       | @sig ?A ?P
+         => refine (fun x : A => _);
+            let f' := open_constr:(f (exist P x _)) in
+            display_helper f'
+       | prod ?A ?B
+         => let f' := open_constr:(fun (a : A) (b : B) => f (a, b)%core) in
+            display_helper f'
+       end
+  | _ => first [ refine (proj1_sig f)
+               | refine f ]
+  end.
+Tactic Notation "display" open_constr(f) :=
+  let do_red F := (eval cbv [proj1_sig f Lift.lift2_sig sig_eq_trans_exist1 MapProjections.proj2_sig_map Associativity.sig_sig_assoc Tuple.tuple Tuple.tuple' FixedWordSizes.wordT PeanoNat.Nat.log2 FixedWordSizes.word_case PeanoNat.Nat.log2_iter PeanoNat.Nat.pred FixedWordSizes.ZToWord FixedWordSizes.word_case_dep Bounds.bounds_to_base_type
+                                       Z.leb Z.compare Pos.compare Pos.compare_cont ZRange.lower ZRange.upper
+                            ] in F) in
+  let ret := open_constr:(ltac:(display_helper (proj1_sig f))) in
+  let ret := do_red ret in
+  let ret := lazymatch ret with
+             | context[match ?sz with O => _ | _ => _ end] => (eval cbv [sz] in ret)
+             | _ => ret
+             end in
+  let ret := (eval simpl @Z.to_nat in ret) in
+  let ret := (eval cbv beta iota zeta in ret) in
+  refine ret.
+Notation display f := (ltac:(let v := f in display v)) (only parsing).
diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v
index f7b6665c4..34eb10c46 100644
--- a/src/Specific/IntegrationTestLadderstep.v
+++ b/src/Specific/IntegrationTestLadderstep.v
@@ -16,6 +16,8 @@ Require Import Crypto.Util.Tactics.SubstEvars.
 Require Import Crypto.Curves.Montgomery.XZ.
 Import ListNotations.
 
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
 Section BoundedField25p5.
@@ -60,48 +62,6 @@ Section BoundedField25p5.
     reflexivity.
   Defined.
 
-  Definition adjust_tuple2_tuple2_sig {A P Q}
-             (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) }
-                  | Q (exist _ _ (proj1 (proj1 (proj2_sig a))),
-                       exist _ _ (proj2 (proj1 (proj2_sig a))),
-                       (exist _ _ (proj1 (proj2 (proj2_sig a))),
-                        exist _ _ (proj2 (proj2 (proj2_sig a))))) })
-    : { a : tuple (tuple (@sig A P) 2) 2 | Q a }.
-  Proof.
-    eexists.
-    exact (proj2_sig v).
-  Defined.
-
-  (** TODO MOVE ME *)
-  (** The [eexists_sig_etransitivity] tactic takes a goal of the form
-      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
-      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
-  Definition sig_eq_trans_exist1 {A B} (f : A -> B)
-             (b b' : B)
-             (pf : b' = b)
-             (y : { a : A | f a = b' })
-    : { a : A | f a = b }
-    := let 'exist a p := y in exist _ a (eq_trans p pf).
-  Ltac eexists_sig_etransitivity :=
-    lazymatch goal with
-    | [ |- { a : ?A | @?f a = ?b } ]
-      => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
-         simple refine (lem _ _)
-    end.
-  Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B)
-             (b : B)
-             (pf : forall a, f' a = f a)
-             (y : { a : A | f' a = b })
-    : { a : A | f a = b }
-    := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p).
-  Ltac eexists_sig_etransitivity_for_rewrite_fun :=
-    lazymatch goal with
-    | [ |- { a : ?A | @?f a = ?b } ]
-      => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in
-         simple refine (lem _ _); cbv beta
-    end.
-
-  (** TODO MOVE ME *)
   (* TODO : change this to field once field isomorphism happens *)
   Definition xzladderstep :
     { xzladderstep : feBW -> feBW -> feBW * feBW -> feBW * feBW -> feBW * feBW * (feBW * feBW)
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.v b/src/Specific/IntegrationTestLadderstepDisplay.v
new file mode 100644
index 000000000..ce551f580
--- /dev/null
+++ b/src/Specific/IntegrationTestLadderstepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.IntegrationTestLadderstep.
+Require Import Crypto.Specific.IntegrationTestDisplayCommon.
+
+(*Check display xzladderstep.*)
diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v
index ec9120246..0cbc3966e 100644
--- a/src/Specific/IntegrationTestMul.v
+++ b/src/Specific/IntegrationTestMul.v
@@ -11,6 +11,8 @@ Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Import ListNotations.
 
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
 Section BoundedField25p5.
@@ -39,23 +41,6 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  (** TODO MOVE ME *)
-  (** The [eexists_sig_etransitivity] tactic takes a goal of the form
-      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
-      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
-  Definition sig_eq_trans_exist1 {A B} (f : A -> B)
-             (b b' : B)
-             (pf : b' = b)
-             (y : { a : A | f a = b' })
-    : { a : A | f a = b }
-    := let 'exist a p := y in exist _ a (eq_trans p pf).
-  Ltac eexists_sig_etransitivity :=
-    lazymatch goal with
-    | [ |- { a : ?A | @?f a = ?b } ]
-      => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
-         simple refine (lem _ _)
-    end.
-
   (* TODO : change this to field once field isomorphism happens *)
   Definition mul :
     { mul : feBW -> feBW -> feBW
diff --git a/src/Specific/IntegrationTestMulDisplay.v b/src/Specific/IntegrationTestMulDisplay.v
new file mode 100644
index 000000000..bf6a3e1c4
--- /dev/null
+++ b/src/Specific/IntegrationTestMulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.IntegrationTestMul.
+Require Import Crypto.Specific.IntegrationTestDisplayCommon.
+
+Check display mul.
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
index a3a1e8613..3eadc371d 100644
--- a/src/Specific/IntegrationTestSub.v
+++ b/src/Specific/IntegrationTestSub.v
@@ -11,6 +11,8 @@ Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Import ListNotations.
 
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
 Section BoundedField25p5.
@@ -39,23 +41,6 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
 
-  (** TODO MOVE ME *)
-  (** The [eexists_sig_etransitivity] tactic takes a goal of the form
-      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
-      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
-  Definition sig_eq_trans_exist1 {A B} (f : A -> B)
-             (b b' : B)
-             (pf : b' = b)
-             (y : { a : A | f a = b' })
-    : { a : A | f a = b }
-    := let 'exist a p := y in exist _ a (eq_trans p pf).
-  Ltac eexists_sig_etransitivity :=
-    lazymatch goal with
-    | [ |- { a : ?A | @?f a = ?b } ]
-      => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
-         simple refine (lem _ _)
-    end.
-
   (* TODO : change this to field once field isomorphism happens *)
   Definition sub :
     { sub : feBW -> feBW -> feBW
diff --git a/src/Specific/IntegrationTestSubDisplay.v b/src/Specific/IntegrationTestSubDisplay.v
new file mode 100644
index 000000000..9f8e5eadc
--- /dev/null
+++ b/src/Specific/IntegrationTestSubDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.IntegrationTestSub.
+Require Import Crypto.Specific.IntegrationTestDisplayCommon.
+
+Check display sub.
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v
new file mode 100644
index 000000000..3bf18d4e7
--- /dev/null
+++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v
@@ -0,0 +1,43 @@
+(*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *)
+Require Import Crypto.Util.Tuple.
+
+Definition adjust_tuple2_tuple2_sig {A P Q}
+           (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) }
+                | Q (exist _ _ (proj1 (proj1 (proj2_sig a))),
+                     exist _ _ (proj2 (proj1 (proj2_sig a))),
+                     (exist _ _ (proj1 (proj2 (proj2_sig a))),
+                      exist _ _ (proj2 (proj2 (proj2_sig a))))) })
+  : { a : tuple (tuple (@sig A P) 2) 2 | Q a }.
+Proof.
+  eexists.
+  exact (proj2_sig v).
+Defined.
+
+(** TODO MOVE ME *)
+(** The [eexists_sig_etransitivity] tactic takes a goal of the form
+      [{ a | f a = b }], and splits it into two goals, [?b' = b] and
+      [{ a | f a = ?b' }], where [?b'] is a fresh evar. *)
+Definition sig_eq_trans_exist1 {A B} (f : A -> B)
+           (b b' : B)
+           (pf : b' = b)
+           (y : { a : A | f a = b' })
+  : { a : A | f a = b }
+  := let 'exist a p := y in exist _ a (eq_trans p pf).
+Ltac eexists_sig_etransitivity :=
+  lazymatch goal with
+  | [ |- { a : ?A | @?f a = ?b } ]
+    => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in
+       simple refine (lem _ _)
+  end.
+Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B)
+           (b : B)
+           (pf : forall a, f' a = f a)
+           (y : { a : A | f' a = b })
+  : { a : A | f a = b }
+  := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p).
+Ltac eexists_sig_etransitivity_for_rewrite_fun :=
+  lazymatch goal with
+  | [ |- { a : ?A | @?f a = ?b } ]
+    => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in
+       simple refine (lem _ _); cbv beta
+  end.