1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
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.
|
