diff options
Diffstat (limited to 'src/Reflection')
-rw-r--r-- | src/Reflection/SmartCastInterp.v | 35 | ||||
-rw-r--r-- | src/Reflection/SmartCastWf.v | 71 |
2 files changed, 106 insertions, 0 deletions
diff --git a/src/Reflection/SmartCastInterp.v b/src/Reflection/SmartCastInterp.v new file mode 100644 index 000000000..f7d1a1aef --- /dev/null +++ b/src/Reflection/SmartCastInterp.v @@ -0,0 +1,35 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.SmartMap. +Require Import Crypto.Reflection.TypeUtil. +Require Import Crypto.Reflection.SmartCast. +Require Import Crypto.Util.Notations. + +Local Open Scope expr_scope. +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {interp_base_type : base_type_code -> Type} + {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} + (base_type_beq : base_type_code -> base_type_code -> bool) + (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) + (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) + (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x) + (cast_val : forall A A', interp_base_type A -> interp_base_type A') + (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)). + + Local Notation exprf := (@exprf base_type_code op). + Local Notation SmartCast_base := (@SmartCast_base _ _ _ base_type_bl_transparent Cast). + Local Notation SmartCast := (@SmartCast _ _ _ base_type_bl_transparent Cast). + + Lemma interpf_SmartCast_base {A A'} (x : exprf (Tbase A)) + : interpf interp_op (SmartCast_base x) = interpf interp_op (Cast _ A A' x). + Proof. + clear dependent cast_val. + unfold SmartCast_base. + destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. + { destruct (base_type_bl_transparent A A' H). + rewrite interpf_Cast_id; reflexivity. } + { reflexivity. } + Qed. +End language. diff --git a/src/Reflection/SmartCastWf.v b/src/Reflection/SmartCastWf.v new file mode 100644 index 000000000..efc6da93c --- /dev/null +++ b/src/Reflection/SmartCastWf.v @@ -0,0 +1,71 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.WfProofs. +Require Import Crypto.Reflection.TypeUtil. +Require Import Crypto.Reflection.SmartCast. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Notations. + +Local Open Scope expr_scope. +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {interp_base_type : base_type_code -> Type} + {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst} + (base_type_beq : base_type_code -> base_type_code -> bool) + (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) + (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) + (wff_Cast : forall var1 var2 G A A' e1 e2, + wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)). + + Local Notation exprf := (@exprf base_type_code op). + Local Notation SmartCast_base := (@SmartCast_base _ _ _ base_type_bl_transparent Cast). + Local Notation SmartCast := (@SmartCast _ _ _ base_type_bl_transparent Cast). + + Lemma wff_SmartCast_base {var1 var2 A A'} G e1 e2 + (Hwf : wff (var1:=var1) (var2:=var2) G (t:=Tbase A) e1 e2) + : wff G (t:=Tbase A') (SmartCast_base e1) (SmartCast_base e2). + Proof. + unfold SmartCast_base; destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. + { destruct (base_type_bl_transparent A A' H); assumption. } + { auto. } + Qed. + + Local Hint Resolve List.in_or_app wff_in_impl_Proper. + Local Hint Extern 1 => progress simpl. + + Lemma wff_SmartCast {var1 var2} A B f1 f2 + : SmartCast A B = Some f1 -> SmartCast A B = Some f2 + -> forall e1 e2, + wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2) (f1 e1) (f2 e2). + Proof. + revert dependent B; induction A, B; + repeat match goal with + | _ => progress simpl in * + | _ => intro + | _ => progress subst + | _ => progress inversion_option + | [ |- wff _ (SmartCast_base _) (SmartCast_base _) ] + => apply wff_SmartCast_base + | _ => progress break_match_hyps + | _ => solve [ auto with wf ] + | [ H : forall B f1 f2, SmartCast ?A B = Some f1 -> SmartCast ?A B = Some f2 -> _, + H' : SmartCast ?A ?Bv = Some _, H'' : SmartCast ?A ?Bv = Some _ |- _ ] + => specialize (H _ _ _ H' H'') + | [ |- wff _ (Pair _ _) (Pair _ _) ] => constructor + | [ |- wff _ _ _ ] => solve [ eauto with wf ] + end. + Qed. + + Lemma wff_SmartCast_app {var1 var2} G A B f1 f2 + : SmartCast A B = Some f1 -> SmartCast A B = Some f2 + -> forall e1 e2, + wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2 ++ G) (f1 e1) (f2 e2). + Proof. + intros; eapply wff_in_impl_Proper; [ eapply wff_SmartCast; eassumption | auto ]. + Qed. +End language. + +Hint Resolve wff_SmartCast_base wff_SmartCast wff_SmartCast_app : wf. |