-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMeta.v
155 lines (108 loc) · 2.89 KB
/
Meta.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
Require Coq.Bool.Sumbool.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Arith.EqNat.
Require Import Shared.
(*
====
IDs
====
*)
Class ID (A : Type) :=
{
id_eq_dec : forall (x y : A), {x = y} + {x <> y}
}.
Inductive svar : Type :=
| SVar : nat -> svar.
Instance ID_svar : ID svar := {}.
repeat decide equality.
Qed.
Definition this := SVar 0.
Inductive dvar : Type :=
| DVar : nat -> dvar.
Instance ID_dvar : ID dvar := {}.
repeat decide equality.
Qed.
Definition dthis := DVar 0.
Definition frame_id := nat.
Instance ID_frame_id : ID frame_id := {}.
repeat decide equality.
Qed.
Instance ID_dvar_frame : ID (dvar * frame_id) := {}.
repeat decide equality.
Qed.
Inductive field_id : Type :=
| Fid : nat -> field_id.
Definition field_id_eq (x y : field_id) : bool :=
match x, y with
| Fid n, Fid m => beq_nat n m
end.
Instance ID_field : ID field_id := {}.
repeat decide equality.
Qed.
Inductive region_id : Type :=
| Rid : nat -> region_id.
Definition region_id_eq (x y : region_id) : bool :=
match x, y with
| Rid n, Rid m => beq_nat n m
end.
Instance ID_region : ID region_id := {}.
repeat decide equality.
Qed.
Inductive method_id : Type :=
| Mid : nat -> method_id.
Definition method_id_eq (x y : method_id) : bool :=
match x, y with
| Mid n, Mid m => beq_nat n m
end.
Instance ID_method : ID method_id := {}.
repeat decide equality.
Qed.
Inductive class_id : Type :=
| Cid : nat -> class_id.
Definition class_id_eq (x y : class_id) : bool :=
match x, y with
| Cid n, Cid m => beq_nat n m
end.
Instance ID_class : ID class_id := {}.
repeat decide equality.
Qed.
Inductive interface_id : Type :=
| Iid : nat -> interface_id.
Definition interface_id_eq (x y : interface_id) : bool :=
match x, y with
| Iid n, Iid m => beq_nat n m
end.
Instance ID_interface : ID interface_id := {}.
repeat decide equality.
Qed.
Definition loc := nat.
Instance ID_loc : ID loc := {id_eq_dec := eq_nat_dec}.
Definition lock := (loc * region_id)%type.
Definition lock_eq (x y : lock) : bool :=
match x, y with
| (l1, r1), (l2, r2) => andb (beq_nat l1 l2) (region_id_eq r1 r2)
end.
Instance ID_lock : ID lock := {}.
repeat decide equality.
Qed.
(*
====
Map
====
*)
Definition partial_map (from:Type) {eqd : ID from} (to:Type) := from -> option to.
Definition empty {A B:Type} {eqd : ID A} : partial_map A B := (fun _ => None).
Definition extend {A B:Type} {eqd : ID A} (Gamma : partial_map A B) (a:A) (b:B) :=
fun a' => if id_eq_dec a a' then
Some b
else
Gamma a'.
Hint Unfold extend.
Definition drop {A B:Type} {eqd : ID A} (Gamma : partial_map A B) (a:A) :=
fun a' => if id_eq_dec a a' then
None
else
Gamma a'.
Hint Unfold drop.
Definition fresh {A B:Type} {eqd : ID A} (Gamma : partial_map A B) (a:A) := Gamma a = None.
Hint Unfold fresh.