diff options
author | 2017-03-17 18:27:48 -0400 | |
---|---|---|
committer | 2017-03-17 18:27:48 -0400 | |
commit | 21eb6f96a4c9bba6aa185f402b0a9fdb4f10806f (patch) | |
tree | e6902798ed7e6a7ad4bc4a40e970539a9560a893 /src/Reflection/Named | |
parent | bcfcb5e91011ad0dda68e2b41f871058cf890a3c (diff) |
Revert "Have cast_op return exprf instead of op"
This reverts commit bcfcb5e91011ad0dda68e2b41f871058cf890a3c.
Doesn't actually build
Diffstat (limited to 'src/Reflection/Named')
-rw-r--r-- | src/Reflection/Named/MapCast.v | 8 | ||||
-rw-r--r-- | src/Reflection/Named/MapCastInterp.v | 96 |
2 files changed, 51 insertions, 53 deletions
diff --git a/src/Reflection/Named/MapCast.v b/src/Reflection/Named/MapCast.v index fc6698a09..a0b161a0a 100644 --- a/src/Reflection/Named/MapCast.v +++ b/src/Reflection/Named/MapCast.v @@ -12,10 +12,8 @@ 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 - (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))) + 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))) {BoundsContext : Context Name interp_base_type_bounds}. Fixpoint mapf_cast @@ -53,7 +51,7 @@ Section language. => let 'existT args_bounds argsv := args' in existT _ (interp_op_bounds _ _ _ args_bounds) - (cast_op t tR opc args_bounds argsv)) + (Op (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 ac8dfb32d..4cc88fe35 100644 --- a/src/Reflection/Named/MapCastInterp.v +++ b/src/Reflection/Named/MapCastInterp.v @@ -25,10 +25,8 @@ 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 - (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))) + 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))) {BoundsContext : Context Name interp_base_type_bounds} (BoundsContextOk : ContextOk BoundsContext) {interp_base_type : base_type_code -> Type} @@ -47,20 +45,13 @@ 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 (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) + (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)) (base_type_dec : DecidableRel (@eq base_type_code)) (Name_dec : DecidableRel (@eq Name)). @@ -179,32 +170,36 @@ Section language. | fin_inbounds_cast_back_t_step ]. Local Ltac t := repeat t_step. - 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. + 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. +*) Lemma mapf_cast_correct {t} (e:exprf base_type_code op Name t) @@ -231,10 +226,14 @@ Section language. pose proof (eq_trans (eq_sym G) H); clear G; inversion_option; subst end. auto. } - { do_specialize_IHe. - destruct_head and; subst; intuition eauto; symmetry; eauto. } + { 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. } { cbv [LetIn.Let_In] in *. - do_specialize_IHe. + do_specialize_IHe IHe1. + do_specialize_IHe IHe2. { apply IHe2; clear IHe2; try reflexivity. intros ??? H. let b := fresh "b" in @@ -242,7 +241,8 @@ Section language. 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. + { do_specialize_IHe IHe1. + do_specialize_IHe IHe2. t. } Qed. |