Add Display files and targets

11 files changed, 124 insertions, 85 deletions

diff --git a/Makefile b/Makefile
index 9ecc8674d..d12203026 100644
--- a/Makefile
+++ b/Makefile
@@ -12,6 +12,7 @@ HIDE := $(if $(VERBOSE),,@)
 
 .PHONY: coq clean update-_CoqProject cleanall install \
 	install-coqprime clean-coqprime coqprime \
+	specific-display display \
 	specific non-specific
 
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq
@@ -50,11 +51,17 @@ COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES))
 LITE_VOFILES := $(filter-out $(HEAVY_VOFILES),$(COQ_VOFILES))
 SPECIFIC_VO := $(filter src/Specific/%,$(VOFILES))
 NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES))
+SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(VOFILES))
+DISPLAY_VO := $(SPECIFIC_DISPLAY_VO)
+DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO))
+DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
 
 specific: $(SPECIFIC_VO) coqprime
 non-specific: $(NON_SPECIFIC_VO) coqprime
 coq: $(COQ_VOFILES) coqprime
 lite: $(LITE_VOFILES) coqprime
+specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log) coqprime
+display: $(DISPLAY_VO:.vo=.log) coqprime
 
 COQPRIME_FOLDER := coqprime
 ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5
@@ -82,13 +89,13 @@ Makefile.coq: Makefile _CoqProject
 	$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
 	$(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@
 
-#$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Reflection/Z/CNotations.vo
-#	$(SHOW)"COQC $*Display > $@"
-#	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@
-#
-#$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Reflection/Z/JavaNotations.vo
-#	$(SHOW)"COQC $*JavaDisplay > $@"
-#	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@
+$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Compilers/Z/CNotations.vo
+	$(SHOW)"COQC $*Display > $@"
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@
+
+$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Compilers/Z/JavaNotations.vo
+	$(SHOW)"COQC $*JavaDisplay > $@"
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@
 
 clean::
 	rm -f Makefile.coq
diff --git a/_CoqProject b/_CoqProject
index 8d25c02b3..0ecbfc92f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -191,9 +191,14 @@ src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
 src/Specific/ArithmeticSynthesisTest.v
+src/Specific/IntegrationTestDisplayCommon.v
 src/Specific/IntegrationTestLadderstep.v
+src/Specific/IntegrationTestLadderstepDisplay.v
 src/Specific/IntegrationTestMul.v
+src/Specific/IntegrationTestMulDisplay.v
 src/Specific/IntegrationTestSub.v
+src/Specific/IntegrationTestSubDisplay.v
+src/Specific/IntegrationTestTemporaryMiscCommon.v
 src/Specific/FancyMachine256/Barrett.v
 src/Specific/FancyMachine256/Core.v
 src/Specific/FancyMachine256/Montgomery.v
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.