diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-19 18:54:39 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-19 18:54:39 -0400 |
commit | d4690fb9073f3d9d037acdf2b3655397af406974 (patch) | |
tree | 245ae9d838251bcbc942703a4e8033db4dffd64e /src/Reflection/MapCastByDeBruijnWf.v | |
parent | 8974f0676f16d583417e05413c51dc318f8de9f5 (diff) |
Add aborted MapCastByDeBruijnWf
I'm not sure exactly why the wf proof requires cast_backb in map_cast;
it seems to be used as a dumb way of instantiating the
context-extension on the input expression tree (since we're only given
the context-extension values on the output expression, which has a
different type).
Diffstat (limited to 'src/Reflection/MapCastByDeBruijnWf.v')
-rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v new file mode 100644 index 000000000..b4edb51c8 --- /dev/null +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -0,0 +1,94 @@ +Require Import Crypto.Reflection.SmartMap. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.Named.Syntax. +Require Import Crypto.Reflection.Named.ContextDefinitions. +Require Import Crypto.Reflection.Named.MapCastWf. +Require Import Crypto.Reflection.Named.InterpretToPHOASWf. +Require Import Crypto.Reflection.Named.CompileWf. +Require Import Crypto.Reflection.Named.PositiveContext. +Require Import Crypto.Reflection.Named.PositiveContext.Defaults. +Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties. +Require Import Crypto.Reflection.LinearizeWf. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapCastByDeBruijn. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.Tactics.BreakMatch. + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + (base_type_code_beq : base_type_code -> base_type_code -> bool) + (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y) + (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true) + (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)) + {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) + {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) + (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))) + (cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t). + Let cast_back : forall t b, interp_flat_type interp_base_type (pick_type b) -> interp_flat_type interp_base_type t + := fun t b => SmartFlatTypeMapUnInterp cast_backb. + Context (inboundsb : forall t, interp_base_type_bounds t -> interp_base_type t -> Prop). + Let inbounds : forall t, interp_flat_type interp_base_type_bounds t -> interp_flat_type interp_base_type t -> Prop + := fun t => interp_flat_type_rel_pointwise inboundsb (t:=t). + Context (interp_op_bounds_correct + : forall t tR opc bs + (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 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)). + + Local Notation MapCast + := (@MapCast + base_type_code op base_type_code_beq base_type_code_bl_transparent + failb interp_base_type_bounds interp_op_bounds pick_typeb cast_op). + + Local Notation PositiveContextOk := (@PositiveContextOk base_type_code _ base_type_code_beq base_type_code_bl_transparent base_type_code_lb). + + Local Instance dec_base_type_code_eq : DecidableRel (@eq base_type_code). + Proof. + refine (fun x y => (if base_type_code_beq x y as b return base_type_code_beq x y = b -> Decidable (x = y) + then fun pf => left (base_type_code_bl_transparent _ _ pf) + else fun pf => right _) eq_refl). + { clear -pf base_type_code_lb. + abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). } + Defined. + + Lemma MapCastCorrect + {t} (e : Expr base_type_code op t) + (Hwf : Wf e) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')), + Wf e'. + Proof. + unfold MapCastByDeBruijn.MapCast, option_map; intros b e'. + break_innermost_match; try congruence; intros ? v v'. + inversion_option; inversion_sigma; subst; simpl in *; intros. + unfold InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen. + eapply (@wf_interp_to_phoas + base_type_code op FMapPositive.PositiveMap.key _ _ _ _ + (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) + (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) + PositiveContextOk PositiveContextOk + (failb _) (failb _) _ e1); + (eapply wf_map_cast with (oldValues:=empty); eauto using PositiveContextOk with typeclass_instances); + try (eapply (wf_compile (ContextOk:=PositiveContextOk)); + [ apply wf_linearize; eauto | .. | eassumption ]); + try solve [ auto using name_list_unique_DefaultNamesFor + | intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence ]. + (* XXX why do we need cast_backb for arbitrary var ? *) + Abort. +End language. |