Have cast_op return exprf instead of op

cc @andres-erbsen

2 files changed, 53 insertions, 51 deletions

diff --git a/src/Reflection/Named/MapCast.v b/src/Reflection/Named/MapCast.v
index a0b161a0a..fc6698a09 100644
--- a/src/Reflection/Named/MapCast.v
+++ b/src/Reflection/Named/MapCast.v
@@ -12,8 +12,10 @@ Section language.
           (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
           (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code).
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
-  Context (cast_op : forall t tR (opc : op t tR) args_bs,
-              op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs)))
+  Context (cast_op
+           : forall t tR (opc : op t tR) args_bs
+                    (args : Named.exprf base_type_code op Name (pick_type args_bs)),
+              Named.exprf base_type_code op Name (pick_type (interp_op_bounds t tR opc args_bs)))
           {BoundsContext : Context Name interp_base_type_bounds}.
 
   Fixpoint mapf_cast
@@ -51,7 +53,7 @@ Section language.
                => let 'existT args_bounds argsv := args' in
                   existT _
                          (interp_op_bounds _ _ _ args_bounds)
-                         (Op (cast_op t tR opc args_bounds) argsv))
+                         (cast_op t tR opc args_bounds argsv))
               (@mapf_cast ctx _ args)
        end.
 
diff --git a/src/Reflection/Named/MapCastInterp.v b/src/Reflection/Named/MapCastInterp.v
index 4cc88fe35..ac8dfb32d 100644
--- a/src/Reflection/Named/MapCastInterp.v
+++ b/src/Reflection/Named/MapCastInterp.v
@@ -25,8 +25,10 @@ Section language.
           (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
           (pick_typeb : forall t, interp_base_type_bounds t -> base_type_code).
   Local Notation pick_type t v := (SmartFlatTypeMap pick_typeb (t:=t) v).
-  Context (cast_op : forall t tR (opc : op t tR) args_bs,
-              op (pick_type _ args_bs) (pick_type _ (interp_op_bounds t tR opc args_bs)))
+  Context (cast_op
+           : forall t tR (opc : op t tR) args_bs
+                    (args : Named.exprf base_type_code op Name (pick_type _ args_bs)),
+              Named.exprf base_type_code op Name (pick_type _ (interp_op_bounds t tR opc args_bs)))
           {BoundsContext : Context Name interp_base_type_bounds}
           (BoundsContextOk : ContextOk BoundsContext)
           {interp_base_type : base_type_code -> Type}
@@ -45,13 +47,20 @@ Section language.
                     (v : interp_flat_type interp_base_type t)
                     (H : inbounds t bs v),
                inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
-          (pull_cast_back:
-             forall t tR opc bs
-                    (v : interp_flat_type interp_base_type (pick_type t bs))
-                    (H : inbounds t bs (cast_back t bs v)),
-               interp_op t tR opc (cast_back t bs v)
-               =
-               cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v))
+          (pull_cast_back
+           : forall t tR opc bs (ctx : Context)
+                    (args : Named.exprf base_type_code op Name (pick_type t bs)) argsv
+                    (Hargs : interpf (interp_op:=interp_op) (ctx:=ctx) args = Some argsv)
+                    (H : inbounds t bs (cast_back t bs argsv))
+                    new_opv
+                    (Hnew : interpf (interp_op:=interp_op) (ctx:=ctx)
+                                    (cast_op _ _ opc bs args) = Some new_opv),
+              interp_op t tR opc (cast_back t bs argsv)
+              =
+              cast_back _ _ new_opv)
+          (cast_op_None : forall t tR opc bs args (ctx : Context),
+              interpf (interp_op:=interp_op) (ctx:=ctx) args = None
+              -> interpf (interp_op:=interp_op) (ctx:=ctx) (cast_op t tR opc bs args) = None)
           (base_type_dec : DecidableRel (@eq base_type_code))
           (Name_dec : DecidableRel (@eq Name)).
 
@@ -170,36 +179,32 @@ Section language.
           | fin_inbounds_cast_back_t_step ].
   Local Ltac t := repeat t_step.
 
-  Local Ltac do_specialize_IHe IH :=
-    let e := match type of IH with forall a b c x y, mapf_cast _ ?e = _ -> _ => e end in
-    let H0 := match goal with H : mapf_cast _ e = _ |- _ => H end in
-    specialize (fun oldValues newValues => IH oldValues newValues _ _ _ H0);
-    let H1 := match goal with H : interpf e = _ |- _ => H end in
-    specialize (fun newValues Hctx => IH _ newValues Hctx _ H1);
-    let e' := lazymatch type of IH with forall newValues, _ -> forall r', interpf ?e = _ -> _ => e end in
-    let H2 := lazymatch goal with H : interpf e' = _ |- _ => H end in
-    specialize (fun Hctx => IH _ Hctx _ H2).
-  (* alternate form:
-repeat match goal with
-             | [ IH : context[interpf ?e], H' : interpf (ctx:=?ctx) ?e = _ |- _ ]
-               => let check_tac _ := (rewrite H' in IH) in
-                  first [ specialize (IH ctx); check_tac ()
-                        | specialize (fun a => IH a ctx); check_tac ()
-                        | specialize (fun a b => IH a b ctx); check_tac () ]
-             | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ]
-               => let check_tac _ := (rewrite H' in IH) in
-                  first [ specialize (IH ctx); check_tac ()
-                        | specialize (fun a => IH a ctx); check_tac ()
-                        | specialize (fun a b => IH a b ctx); check_tac () ]
-             | [ H : forall x y z, Some _ = Some _ -> _ |- _ ]
-               => first [ specialize (H _ _ _ eq_refl)
-                        | specialize (fun x => H x _ _ eq_refl) ]
-             | [ H : forall x y, Some _ = Some _ -> _ |- _ ]
-               => first [ specialize (H _ _ eq_refl)
-                        | specialize (fun x => H x _ eq_refl) ]
-             | _ => progress specialize_by_assumption
-             end.
-*)
+  Local Ltac do_specialize_IHe :=
+    repeat match goal with
+           | [ IH : context[interpf ?e], H' : interpf (ctx:=?ctx) ?e = _ |- _ ]
+             => let check_tac _ := (rewrite H' in IH) in
+                first [ specialize (IH ctx); check_tac ()
+                      | specialize (fun a => IH a ctx); check_tac ()
+                      | specialize (fun a b => IH a b ctx); check_tac () ]
+           | [ IH : context[mapf_cast _ ?e], H' : mapf_cast ?ctx ?e = _ |- _ ]
+             => let check_tac _ := (rewrite H' in IH) in
+                first [ specialize (IH ctx); check_tac ()
+                      | specialize (fun a => IH a ctx); check_tac ()
+                      | specialize (fun a b => IH a b ctx); check_tac () ]
+           | [ H : forall x y z, Some _ = Some _ -> _ |- _ ]
+             => first [ specialize (H _ _ _ eq_refl)
+                      | specialize (fun x => H x _ _ eq_refl)
+                      | specialize (fun x y => H x y _ eq_refl) ]
+           | [ H : forall x y, Some _ = Some _ -> _ |- _ ]
+             => first [ specialize (H _ _ eq_refl)
+                      | specialize (fun x => H x _ eq_refl) ]
+           | [ H : context[interpf ?e], H' : interpf (interp_op:=?interp_op) (ctx:=?ctx) (cast_op ?t ?tR ?opc ?bs ?e) = _ |- _ ]
+             => let H2 := fresh in
+                destruct (interpf (interp_op:=interp_op) (ctx:=ctx) e) eqn:H2;
+                [ specialize (fun a => H ctx a _ H2)
+                | apply (@cast_op_None t tR opc bs e ctx) in H2; congruence ]
+           | _ => progress specialize_by_assumption
+           end.
 
   Lemma mapf_cast_correct
   {t} (e:exprf base_type_code op Name t)
@@ -226,14 +231,10 @@ repeat match goal with
                pose proof (eq_trans (eq_sym G) H); clear G; inversion_option; subst
              end.
       auto. }
-    { match goal with
-      | [ H0 : mapf_cast varBounds ?e = _, H1 : interpf ?e = _, H2 : interpf _ = _ |- _ ]
-        => specialize (IHe oldValues newValues varBounds _ _ H0 Hctx _ H1 _ H2)
-      end.
-      destruct_head and; subst; intuition eauto; symmetry; auto. }
+    { do_specialize_IHe.
+      destruct_head and; subst; intuition eauto; symmetry; eauto. }
     { cbv [LetIn.Let_In] in *.
-      do_specialize_IHe IHe1.
-      do_specialize_IHe IHe2.
+      do_specialize_IHe.
       { apply IHe2; clear IHe2; try reflexivity.
         intros ??? H.
         let b := fresh "b" in
@@ -241,8 +242,7 @@ repeat match goal with
         match goal with |- exists b0, ?v = Some b0 /\ _ => destruct v as [b|] eqn:H' end;
           [ exists b; split; [ reflexivity | ] | exfalso ];
           revert H H'; t. } }
-    { do_specialize_IHe IHe1.
-      do_specialize_IHe IHe2.
+    { do_specialize_IHe.
       t. }
   Qed.