Display un-interped C code

3 files changed, 18 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index d12203026..7a61d0d71 100644
--- a/Makefile
+++ b/Makefile
@@ -89,11 +89,11 @@ 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/Compilers/Z/CNotations.vo
+$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Compilers/Z/CNotations.vo src/Specific/IntegrationTestDisplayCommon.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
+$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Compilers/Z/JavaNotations.vo src/Specific/IntegrationTestDisplayCommon.vo
 	$(SHOW)"COQC $*JavaDisplay > $@"
 	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@
 
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 15150eab1..147db3e54 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -82,7 +82,7 @@ Ltac handle_bounds_from_hyps :=
     vm_computed_reified_expression arguments]. *)
 Declare Reduction interp_red
   := cbv [fst snd
-              Interp InterpEta interp_op interp interp_eta interpf interpf_step
+              Interp (*InterpEta interp_op*) interp interp_eta interpf interpf_step
               interp_flat_type_eta interp_flat_type_eta_gen interp_flat_type
               interp_base_type interp_op
               SmartMap.SmartFlatTypeMap SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2
diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v
index a9955ad5b..64b7ff0d6 100644
--- a/src/Specific/IntegrationTestDisplayCommon.v
+++ b/src/Specific/IntegrationTestDisplayCommon.v
@@ -3,12 +3,14 @@ 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 Import Crypto.Compilers.Eta.
 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 !_ / .
+Global Arguments InterpEta {_ _ _ _ _}.
 
 Ltac display_helper f :=
   lazymatch type of f with
@@ -27,8 +29,18 @@ Ltac display_helper 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
+  let do_red F := (eval cbv [f
+                               proj1_sig
+                               Lift.lift2_sig Lift.lift4_sig
+                               MapProjections.proj2_sig_map Associativity.sig_sig_assoc
+                               sig_eq_trans_exist1
+                               Tuple.tuple Tuple.tuple'
+                               FixedWordSizes.wordT FixedWordSizes.word_case FixedWordSizes.ZToWord FixedWordSizes.word_case_dep
+                               PeanoNat.Nat.log2 PeanoNat.Nat.log2_iter PeanoNat.Nat.pred
+                               Bounds.bounds_to_base_type
+                               interp_flat_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
@@ -37,6 +49,6 @@ Tactic Notation "display" open_constr(f) :=
              | _ => ret
              end in
   let ret := (eval simpl @Z.to_nat in ret) in
-  let ret := (eval cbv beta iota zeta in ret) in
+  let ret := (eval cbv [interp_flat_type] in ret) in
   refine ret.
 Notation display f := (ltac:(let v := f in display v)) (only parsing).