-
Notifications
You must be signed in to change notification settings - Fork 0
/
wf_env.v
167 lines (129 loc) · 5.69 KB
/
wf_env.v
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
Require Import syntax.
Require Import partial.
Require Import heap.
Require Import classTable.
Require Import sframe.
Require Import reductions.
Require Import typing.
Require Import namesAndTypes.
Import ConcreteEverything.
Section WF_Env.
Import Coq.Lists.List.
Definition gamma_env_subset (gamma: Gamma_type) (L: Env_type) :=
forall x,
In x (p_Γ.domain gamma) ->
In x (p_env.domain L).
Theorem in_dec_equivalence (A: Type) (eq_dec: forall (x y: A),
{x = y} + {x <> y}
) :
forall x l1 l2,
(@In A x l1 <-> In x l2) <-> (~ In x l1 <-> ~ In x l2).
intros.
set (leml1 := in_dec eq_dec x l1).
set (leml2 := in_dec eq_dec x l2).
firstorder.
Defined.
Theorem subset_preserved gamma L x sigma envVal :
gamma_env_subset gamma L ->
gamma_env_subset (p_Γ.updatePartFunc gamma x sigma )
(p_env.updatePartFunc L x envVal).
intros subset x'.
intro.
set (lem_gamma := p_Γ.updatedFuncProp gamma x sigma x').
set (lem_env := p_env.updatedFuncProp L x envVal x').
elim (v_eq_dec x' x).
intro; rewrite a in *; clear a.
set (lem_env_x := (proj1 lem_env) (eq_refl x)).
set (lem_upd_env := proj1 (p_env.fDomainCompat (p_env.updatePartFunc L x envVal) x)).
set (in_or_not := in_dec v_eq_dec x (p_env.domain (p_env.updatePartFunc L x envVal))).
elim in_or_not.
auto.
intro.
set (not_in := lem_upd_env b).
rewrite not_in in lem_env_x; discriminate.
(* x != x'
* Proof structure:
* Then x' in dom(Gamma) <--> x' in dom(Gamma[x |-> sigma])
* x' in dom(L) <--> x' in dom(L[x |-> envVal])
*)
intro x_neq.
assert (In x' (p_Γ.domain gamma) <-> In x' (p_Γ.domain
(p_Γ.updatePartFunc gamma x sigma))).
apply (proj2 (in_dec_equivalence p_Γ.A v_eq_dec x' _ _)).
set (lem_gamma' := (proj2 lem_gamma) x_neq).
set (lem_gamma_upd_equiv
:= proj2 (p_Γ.fDomainCompat (p_Γ.updatePartFunc gamma x sigma) x')).
set (lem_gamma_equiv := proj2 (p_Γ.fDomainCompat gamma x')).
firstorder.
assert (In x' (p_env.domain L) <-> In x' (p_env.domain
(p_env.updatePartFunc L x envVal))).
apply (proj2 (in_dec_equivalence p_env.A v_eq_dec x' _ _)).
set (lem_env' := (proj2 lem_env) x_neq).
set (lem_env_upd_equiv
:= proj2 (p_env.fDomainCompat (p_env.updatePartFunc L x envVal) x')).
set (lem_env_equiv := proj2 (p_env.fDomainCompat L x')).
firstorder.
firstorder.
Qed.
Import Coq.Lists.List.
Variable P: Program.
Definition subtypeP := subtype P.
Definition TypeChecksP := TypeChecksTerm P.
Local Open Scope type_scope.
Definition WF_Var (H: Heap_type) (Gamma: Gamma_type) (L: Env_type) (x: VarName_type):=
(p_env.func L x = Some envNull) +
{C_o : _ &
match C_o with
| (C, o) => {witn : _&
(p_env.func L x = Some (envRef o)) *
(p_Γ.func Gamma x = Some (typt_class C)) *
(subtypeP (typt_class (heap_typeof H o witn)) (typt_class C))
}
end} +
{C_o : _ &
match C_o with
| (C, o) => {witn : _ &
(p_env.func L x = Some (envBox o)) *
(p_Γ.func Gamma x = Some (typt_box C)) *
(subtypeP (typt_class (heap_typeof H o witn)) (typt_class C))
}
end}.
Definition WF_Env H Gamma L :=
gamma_env_subset Gamma L *
forall x sigma,
p_Γ.func Gamma x = Some sigma ->
WF_Var H Gamma L x.
Inductive WF_Frame : Heap_type -> ann_frame_type -> typecheck_type -> Type :=
| t_frame1 : forall H Gamma eff t L ann sigma,
TypeChecksP Gamma eff t sigma ->
WF_Env H Gamma L ->
WF_Frame H (ann_frame (sframe L t) ann) sigma.
Inductive WF_Frame_ann : Heap_type -> ann_frame_type -> typecheck_type -> VarName_type ->
typecheck_type -> Type :=
| t_frame2 : forall H Gamma eff t L ann sigma x tau,
TypeChecksP (p_Γ.updatePartFunc Gamma x tau) eff t sigma ->
WF_Env H Gamma L ->
WF_Frame_ann H (ann_frame (sframe L t) ann) sigma x tau.
Notation "( H , x , tau ## F @@ sigma )" := (WF_Frame_ann H F sigma x tau).
Definition FS_ann_type := option (VarName_type * typecheck_type).
Inductive WF_FS : FS_ann_type -> Heap_type -> list (ann_frame_type) -> Type :=
| T_EmpFS : forall H, WF_FS None H nil
| T_FS_NA : forall H F FS sigma,
WF_Frame H (ann_frame F ann_epsilon) sigma ->
WF_FS None H FS ->
WF_FS None H ((ann_frame F ann_epsilon) :: FS)
| T_FS_NA2 : forall H F FS sigma x tau,
( H , x , tau ## (ann_frame F ann_epsilon) @@ sigma ) ->
WF_FS None H FS ->
WF_FS (Some (x, tau)) H ((ann_frame F ann_epsilon) :: FS)
| T_FS_A : forall H F FS x tau ,
WF_Frame H (ann_frame F (ann_var x)) tau ->
WF_FS (Some (x, tau)) H FS ->
WF_FS None H ((ann_frame F (ann_var x)) :: FS)
| T_FS_A2 : forall H F FS y sigma x tau,
( H, y, sigma ## (ann_frame F (ann_var x)) @@ tau) ->
WF_FS (Some (x, tau)) H FS ->
WF_FS (Some (y, sigma)) H ((ann_frame F (ann_var x)) :: FS).
(* Notation "[ ! H , x , tau ## FS ]" := (WF_FS (Some (x, tau)) H FS) (at level 0). *)
(* Notation "[ ! H ## FS ]" := (WF_FS None H FS) (at level 0). *)
End WF_Env.