Add InlineCastWf

1 files changed, 131 insertions, 0 deletions

diff --git a/src/Reflection/InlineCastWf.v b/src/Reflection/InlineCastWf.v
new file mode 100644
index 000000000..ed295a3d4
--- /dev/null
+++ b/src/Reflection/InlineCastWf.v
@@ -0,0 +1,131 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.TypeInversion.
+Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Reflection.WfInversion.
+Require Import Crypto.Reflection.InlineCast.
+Require Import Crypto.Reflection.InlineWf.
+Require Import Crypto.Reflection.SmartCast.
+Require Import Crypto.Reflection.SmartCastWf.
+Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+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}
+          (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)
+          (base_type_leb : base_type_code -> base_type_code -> bool)
+          (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A'))
+          (is_cast : forall src dst, op src dst -> bool)
+          (is_const : forall src dst, op src dst -> bool)
+          (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 Infix "<=?" := base_type_leb : expr_scope.
+  Local Infix "=?" := base_type_beq : expr_scope.
+
+  Local Notation SmartCast_base := (@SmartCast_base _ op _ base_type_bl_transparent Cast).
+  Local Notation squash_cast := (@squash_cast _ op _ base_type_bl_transparent base_type_leb Cast).
+  Local Notation maybe_push_cast := (@maybe_push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const).
+  Local Notation push_cast := (@push_cast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const).
+  Local Notation InlineCast := (@InlineCast _ op _ base_type_bl_transparent base_type_leb Cast is_cast is_const).
+
+  Lemma wff_squash_cast var1 var2 a b c e1 e2 G
+        (Hwf : wff G e1 e2)
+    : wff G (@squash_cast var1 a b c e1) (@squash_cast var2 a b c e2).
+  Proof.
+    unfold squash_cast; break_innermost_match; auto with wf.
+  Qed.
+
+  Local Opaque InlineCast.squash_cast.
+
+  Lemma wff_maybe_push_cast_match {var1 var2 t e1 e2 G}
+        (Hwf : wff G e1 e2)
+    : match @maybe_push_cast var1 t e1, @maybe_push_cast var2 t e2 with
+      | Some e1', Some e2' => wff G e1' e2'
+      | None, None => True
+      | Some _, None | None, Some _ => False
+      end.
+  Proof.
+    induction Hwf;
+      repeat match goal with
+             | [ |- wff _ (squash_cast _ _ _ _) (squash_cast _ _ _ _) ]
+               => apply wff_squash_cast
+             | _ => progress subst
+             | _ => progress destruct_head' sig
+             | _ => progress destruct_head' and
+             | _ => progress inversion_option
+             | _ => progress simpl in *
+             | _ => congruence
+             | _ => progress break_innermost_match_step
+             | _ => intro
+             | [ H : forall e1 e2, Some _ = Some e1 -> _ |- _ ]
+               => specialize (fun e2 => H _ e2 eq_refl)
+             | [ H : forall e, Some _ = Some e -> _ |- _ ]
+               => specialize (H _ eq_refl)
+             | _ => solve [ auto with wf ]
+             | _ => progress inversion_wff_constr
+             | _ => progress inversion_type
+             | [ H : context[match ?e with _ => _ end] |- _ ] => invert_one_expr e
+             | [ |- context[match ?e with _ => _ end] ] => invert_one_expr e
+             end.
+  Qed.
+
+  Lemma wff_maybe_push_cast var1 var2 t e1 e2 G e1' e2'
+        (Hwf : wff G e1 e2)
+    : @maybe_push_cast var1 t e1 = Some e1'
+      -> @maybe_push_cast var2 t e2 = Some e2'
+      -> wff G e1' e2'.
+  Proof.
+    intros H0 H1; eapply wff_maybe_push_cast_match in Hwf.
+    rewrite H0, H1 in Hwf; assumption.
+  Qed.
+
+  Local Notation wff_inline_directive G x y :=
+    (wff G (exprf_of_inline_directive x) (exprf_of_inline_directive y)
+     /\ (fun x' y'
+         => match x', y' with
+            | default_inline _ _, default_inline _ _
+            | no_inline _ _, no_inline _ _
+            | inline _ _, inline _ _
+              => True
+            | default_inline _ _, _
+            | no_inline _ _, _
+            | inline _ _, _
+              => False
+            end) x y).
+
+  Lemma wff_push_cast var1 var2 t e1 e2 G
+        (Hwf : wff G e1 e2)
+    : wff_inline_directive G (@push_cast var1 t e1) (@push_cast var2 t e2).
+  Proof.
+    pose proof (wff_maybe_push_cast_match Hwf).
+    unfold push_cast; destruct t;
+      break_innermost_match;
+      repeat first [ apply conj
+                   | exact I
+                   | progress simpl in *
+                   | exfalso; assumption
+                   | assumption ].
+  Qed.
+
+  Lemma wff_exprf_of_push_cast var1 var2 t e1 e2 G
+        (Hwf : wff G e1 e2)
+    : wff G
+          (exprf_of_inline_directive (@push_cast var1 t e1))
+          (exprf_of_inline_directive (@push_cast var2 t e2)).
+  Proof. apply wff_push_cast; assumption. Qed.
+
+  Local Hint Resolve wff_push_cast.
+
+  Lemma Wf_InlineCast {t} e (Hwf : Wf e)
+    : Wf (@InlineCast t e).
+  Proof. apply Wf_InlineConstGen; auto. Qed.
+End language.
+
+Hint Resolve Wf_InlineCast : wf.