blob: 717f8de60eb6d113bbd447ecf2b2f0a1df43a909 (
plain)
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Wf.
Require Import Crypto.Reflection.SmartMap.
Require Import Crypto.Reflection.ExprInversion.
Require Import Crypto.Reflection.MapCast.
Require Import Crypto.Reflection.WfProofs.
Require Import Crypto.Reflection.WfInversion.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.
Section language.
Context {base_type_code : Type}
{interp_base_type : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst)
(failv : forall {var t}, @exprf base_type_code op var (Tbase t)).
Context (transfer_op : forall ovar src1 dst1 src2 dst2
(opc1 : op src1 dst1)
(opc2 : op src2 dst2)
(args1' : @exprf base_type_code op ovar src1)
(args2 : interp_flat_type interp_base_type src2),
@exprf base_type_code op ovar dst1).
Local Notation interp_flat_type_ivarf_wff G a b
:= (forall t x y,
List.In (existT _ t (x, y)%core) (flatten_binding_list a b)
-> wff G x y)
(only parsing).
Section with_var.
Context {ovar1 ovar2 : base_type_code -> Type}.
Context (wff_transfer_op
: forall G src1 dst1 src2 dst2 opc1 opc2 args1 args1' args2,
wff G (var1:=ovar1) (var2:=ovar2) args1 args1'
-> wff G
(@transfer_op ovar1 src1 dst1 src2 dst2 opc1 opc2 args1 args2)
(@transfer_op ovar2 src1 dst1 src2 dst2 opc1 opc2 args1' args2)).
Local Notation mapf_interp_cast
:= (@mapf_interp_cast
base_type_code base_type_code interp_base_type
op op interp_op2 failv
transfer_op).
Local Notation map_interp_cast
:= (@map_interp_cast
base_type_code base_type_code interp_base_type
op op interp_op2 failv
transfer_op).
Local Notation G1eTf
:= (fun t : base_type_code => interp_flat_type ovar1 (Tbase t) * interp_flat_type ovar2 (Tbase t))%type.
Local Notation G2eTf
:= (fun t : base_type_code => ovar1 t * ovar2 t)%type.
Local Notation GbeTf
:= (fun t : base_type_code => interp_flat_type ovar1 (Tbase t) * interp_base_type t)%type.
(* Definition Gse_related' {t} (G1e : G1eTf t) (Gbe : GbeTf t) (G2e G2eTf t) : Prop
:= fst G1e = fst Gbe /\
:= exists (pf1 : projT1 G1e = projT1 G2e
Definition Gse_related (G1e : sigT G1eTf) (G2e : sigT G2eTf) (G3e : sigT G3eTf) : Prop
:= exists (pf1 : projT1 G1e = projT1 G2e
/\
Local Notation G3eT
:= {t : base_type_code &
((interp_flat_type ivarf1 (Tbase t) * interp_flat_type ivarf2 (Tbase t))
* (ovar1 t * ovar2 t)
* interp_base_type t)%type }.
Local Notation G3T
:= (list G3eT).
Definition G3e_to_G1e
*)
(* Local *) Hint Resolve <- List.in_app_iff.
Local Ltac break_t
:= first [ progress subst
| progress inversion_wf
| progress invert_expr_subst
| progress inversion_sigma
| progress inversion_prod
| progress destruct_head sig
| progress destruct_head sigT
| progress destruct_head ex
| progress destruct_head and
| progress destruct_head prod
| progress break_match_hyps ].
Lemma wff_mapf_interp_cast
G1 Gbounds
{t1} e1 e2 ebounds
(Hwf_bounds : wff Gbounds e1 ebounds)
(Hwf : wff G1 e1 e2)
: wff G1
(@mapf_interp_cast ovar1 t1 e1 t1 ebounds)
(@mapf_interp_cast ovar2 t1 e2 t1 ebounds).
Proof.
revert dependent Gbounds; revert ebounds;
induction Hwf;
repeat match goal with
| _ => solve [ exfalso; assumption ]
| _ => intro
| _ => progress break_t
| _ => solve [ constructor; eauto
| eauto
| auto
| hnf; auto ]
| _ => progress simpl in *
| [ H : List.In _ (_ ++ _) |- _ ] => apply List.in_app_or in H
| _ => progress destruct_head or
| [ |- wff _ _ _ ] => constructor
| [ H : _ |- wff _ (mapf_interp_cast _ _ _ _) (mapf_interp_cast _ _ _ _) ]
=> eapply H; eauto; []; clear H
| _ => solve [ eauto using wff_SmartVarf, wff_in_impl_Proper ]
end.
Qed.
Lemma wf_map_interp_cast
{t1} e1 e2 ebounds
args2
(Hwf_bounds : wf e1 ebounds)
(Hwf : wf e1 e2)
: wf (@map_interp_cast ovar1 t1 e1 t1 ebounds args2)
(@map_interp_cast ovar2 t1 e2 t1 ebounds args2).
Proof.
destruct Hwf;
repeat match goal with
| _ => solve [ constructor; eauto
| eauto using wff_mapf_interp_cast
| exfalso; assumption ]
| _ => intro
| _ => progress break_t
| [ |- wf _ _ ] => constructor
| _ => solve [ eauto using wff_SmartVarf, wff_in_impl_Proper ]
end.
Qed.
End with_var.
Section gen.
Context (wff_transfer_op
: forall ovar1 ovar2 G src1 dst1 src2 dst2 opc1 opc2 e1 e2 args2,
wff G (var1:=ovar1) (var2:=ovar2) e1 e2
-> wff G
(@transfer_op ovar1 src1 dst1 src2 dst2 opc1 opc2 e1 args2)
(@transfer_op ovar2 src1 dst1 src2 dst2 opc1 opc2 e2 args2)).
Local Notation MapInterpCast
:= (@MapInterpCast
base_type_code interp_base_type
op interp_op2 failv
transfer_op).
Lemma Wf_MapInterpCast
{t} e
args
(Hwf : Wf e)
: Wf (@MapInterpCast t e args).
Proof.
intros ??; apply wf_map_interp_cast; auto.
Qed.
End gen.
End language.
Hint Resolve Wf_MapInterpCast : wf.
|
