Factor Reify_rhs so that it's more reusable

1 files changed, 32 insertions, 22 deletions

diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v
index 2631a8a21..7b20f5efe 100644
--- a/src/Reflection/Reify.v
+++ b/src/Reflection/Reify.v
@@ -240,27 +240,37 @@ Ltac Reify base_type_code interp_base_type op e :=
 Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end.
 Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end.
 
-Ltac Reify_rhs base_type_code interp_base_type op interp_op :=
+Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op :=
   let rhs := rhs_of_goal in
-  let RHS := Reify base_type_code interp_base_type op rhs in
-  transitivity (Syntax.Interp interp_op RHS);
+  let RHS := Reify rhs in
+  let RHS' := (eval vm_compute in RHS) in
+  transitivity (Syntax.Interp interp_op RHS');
   [
-  | etransitivity; (* first we strip off the [InputSyntax.Compile]
-                      bit; Coq is bad at inferring the type, so we
-                      help it out by providing it *)
-    [ lazymatch goal with
-      | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ]
-        => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e)
-      end
-    | ((* now we unfold the interpretation function, including the
-          parameterized bits; we assume that [hnf] is enough to unfold
-          the interpretation functions that we're parameterized
-          over. *)
-      lazymatch goal with
-      | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ]
-        => let interp_base_type' := (eval hnf in interp_base_type) in
-           let interp_op' := (eval hnf in interp_op) in
-           change interp_base_type with interp_base_type';
-           change interp_op with interp_op'
-      end;
-      cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ].
+  | transitivity (Syntax.Interp interp_op RHS);
+    [ apply f_equal; vm_compute; reflexivity
+    | etransitivity; (* first we strip off the [InputSyntax.Compile]
+                        bit; Coq is bad at inferring the type, so we
+                        help it out by providing it *)
+      [ prove_interp_compile_correct ()
+      | ((* now we unfold the interpretation function, including the
+            parameterized bits; we assume that [hnf] is enough to unfold
+            the interpretation functions that we're parameterized
+            over. *)
+        lazymatch goal with
+        | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ]
+          => let interp_base_type' := (eval hnf in interp_base_type) in
+             let interp_op' := (eval hnf in interp_op) in
+             change interp_base_type with interp_base_type';
+             change interp_op with interp_op'
+        end;
+        cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ] ].
+
+Ltac Reify_rhs base_type_code interp_base_type op interp_op :=
+  Reify_rhs_gen
+    ltac:(Reify base_type_code interp_base_type op)
+           ltac:(fun _
+                 => lazymatch goal with
+                    | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ]
+                      => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e)
+                    end)
+                  interp_op.