diff options
author | 2017-02-14 00:19:04 -0500 | |
---|---|---|
committer | 2017-02-14 00:19:04 -0500 | |
commit | 8a90b078ece6fac84bb45b0375aa65a8faa25466 (patch) | |
tree | 14f6b11c10aa75146f458ca712f570a9217c1898 | |
parent | 81364d2020f9e2218cfe0dfd274a9b82dc2d7d42 (diff) |
Add src/Reflection/BoundByCastWf.v
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/BoundByCastWf.v | 56 |
2 files changed, 57 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 7c06bba30..ec0cacb70 100644 --- a/_CoqProject +++ b/_CoqProject @@ -99,6 +99,7 @@ src/Reflection/Application.v src/Reflection/ApplicationLemmas.v src/Reflection/ApplicationRelations.v src/Reflection/BoundByCast.v +src/Reflection/BoundByCastWf.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Conversion.v src/Reflection/CountLets.v diff --git a/src/Reflection/BoundByCastWf.v b/src/Reflection/BoundByCastWf.v new file mode 100644 index 000000000..88e0169b8 --- /dev/null +++ b/src/Reflection/BoundByCastWf.v @@ -0,0 +1,56 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.BoundByCast. +Require Import Crypto.Reflection.EtaWf. +Require Import Crypto.Reflection.InlineCastWf. +Require Import Crypto.Reflection.LinearizeWf. +Require Import Crypto.Reflection.SmartBoundWf. + +(* +Require Import Crypto.Reflection.SmartBound. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Inline. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.MapCast. +Require Import Crypto.Reflection.Eta.*) + +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_bounds : base_type_code -> Type) + (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) + (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) + (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) + (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), + option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) + (failf : forall var t, @exprf base_type_code op var (Tbase t)) + (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 Expr := (@Expr base_type_code op). + + Lemma Wf_Boundify {t1} (e1 : Expr t1) args2 + (Hwf : Wf e1) + : Wf (@Boundify + _ op _ interp_op_bounds + bound_base_type + _ base_type_bl_transparent + base_type_leb + Cast + is_cast is_const genericize_op + failf t1 e1 args2). + Proof. + unfold Boundify. + apply Wf_ExprEta. + apply Wf_InlineCast; auto. + apply Wf_Linearize. + apply Wf_SmartBound; auto. + Admitted. +End language. |