Add extract_Expr

1 files changed, 70 insertions, 7 deletions

diff --git a/src/Specific/IntegrationTestDisplayCommonTactics.v b/src/Specific/IntegrationTestDisplayCommonTactics.v
index 2e6c1f4bc..999fbe1ed 100644
--- a/src/Specific/IntegrationTestDisplayCommonTactics.v
+++ b/src/Specific/IntegrationTestDisplayCommonTactics.v
@@ -10,7 +10,15 @@ Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Compilers.Syntax.
 Require Export Crypto.Util.Notations.
 
-Ltac display_helper f :=
+Global Arguments Pos.to_nat !_ / .
+
+Ltac display_helper_gen f make_hole :=
+  let display_helper f := display_helper_gen f make_hole in
+  let do_make_hole _ :=
+      match goal with
+      | [ |- ?T ] => let h := make_hole T in
+                     refine h
+      end in
   let t := type of f in
   lazymatch (eval hnf in t) with
   | forall _ : ?A, ?B
@@ -19,21 +27,21 @@ Ltac display_helper f :=
        | @sig ?A ?P
          => lazymatch (eval hnf in A) with
             | sig _
-              => let f' := open_constr:(fun x : A => f (exist P x _)) in
+              => let f' := constr:(fun x : A => f (exist P x ltac:(do_make_hole ()))) in
                  display_helper f'
             | _
               => refine (fun x : A => _);
-                 let f' := open_constr:(f (exist P x _)) in
+                 let f' := constr:(f (exist P x ltac:(do_make_hole ()))) in
                  display_helper f'
             end
        | _
          => lazymatch A with
             | prod ?A ?B
-              => let f' := open_constr:(fun (a : A) (b : B) => f (a, b)%core) in
+              => let f' := constr:(fun (a : A) (b : B) => f (a, b)%core) in
                  display_helper f'
             | _
               => refine (fun x : A => _);
-                 let f' := open_constr:(f x) in
+                 let f' := constr:(f x) in
                  display_helper f'
             end
        end
@@ -53,7 +61,16 @@ Ltac display_helper f :=
        | _ => refine f
        end
   end.
-Tactic Notation "display" open_constr(f) :=
+Ltac display_helper f := display_helper_gen f ltac:(fun T => open_constr:(_)).
+Ltac display_helper_with_admit f :=
+  constr:(fun admit : forall T, T
+          => ltac:(display_helper_gen f ltac:(fun T => constr:(admit T)))).
+Ltac try_strip_admit f :=
+  lazymatch f with
+  | fun _ : forall T, T => ?P => P
+  | ?P => P
+  end.
+Ltac refine_display f :=
   let do_red F := (eval cbv [f
                                proj1_sig fst snd
                                Tuple.map Tuple.map'
@@ -73,8 +90,9 @@ Tactic Notation "display" open_constr(f) :=
                                interp_flat_type
                                Z.leb Z.compare Pos.compare Pos.compare_cont
                                ZRange.lower ZRange.upper
+                               BinPos.Pos.to_nat PeanoNat.Nat.pow
                             ] in F) in
-  let ret := open_constr:(ltac:(display_helper (proj1_sig f))) in
+  let ret := display_helper_with_admit (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)
@@ -82,5 +100,50 @@ Tactic Notation "display" open_constr(f) :=
              end in
   let ret := (eval simpl @Z.to_nat in ret) in
   let ret := (eval cbv [interp_flat_type] in ret) in
+  let ret := try_strip_admit ret in
   refine ret.
+Tactic Notation "display" open_constr(f) :=
+  refine_display f.
 Notation display f := (ltac:(let v := f in display v)) (only parsing).
+
+(** Some helper tactics for actually pulling out the expression *)
+Ltac strip_InterpEta term :=
+  let retype e :=
+      lazymatch type of e with
+      | forall var, @Syntax.expr ?base_type_code ?op var ?T
+        => constr:(e : @Syntax.Expr base_type_code op T)
+      | _ => e
+      end in
+  lazymatch term with
+  | fun x : ?T => ?P
+    => let maybe_x := fresh x in
+       let probably_not_x := fresh maybe_x in
+       let not_x := fresh probably_not_x in
+       lazymatch
+         constr:(fun x : T
+                 => match P with
+                    | not_x => ltac:(let v := (eval cbv delta [not_x] in not_x) in
+                                     let v' := strip_InterpEta v in
+                                     exact v')
+                    end)
+       with
+       | fun _ => ?P => retype P
+       | ?P => retype P
+       end
+  | @Eta.InterpEta _ _ _ _ _ ?e
+    => e
+  | @Eta.InterpEta _ _ _ _ _ ?e _
+    => e
+  | let (a, b) := ?f in _
+    => f
+  | _ => let dummy := match goal with
+                      | _ => fail 1 "strip_InterpEta:" term
+                      end in
+         I
+  end.
+
+Ltac extract_Expr f :=
+  let k := constr:(ltac:(refine_display f)) in
+  let k := strip_InterpEta k in
+  k.
+Notation extract_Expr f := (ltac:(let v := f in let v := extract_Expr v in refine v)) (only parsing).