-
Notifications
You must be signed in to change notification settings - Fork 0
/
classTable_orig.v
130 lines (100 loc) · 3.05 KB
/
classTable_orig.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
Require Import syntax.
Require Import partial.
Require Import namesAndTypes.
Import ConcreteEverything.
Section MethodsAndFields.
Variable P : Program.
Require Import Coq.Lists.List.
(* Module MethodsAndFields (ct: ClassTable). *)
(* Parameter CT : list ClassDecl. *)
(* Maybe change to method name? *)
Definition method : class -> MethodName_type -> MethDecl -> Prop :=
fun _ _ _ => classDecls P = nil.
Definition mtype C m md
(witn: method C m md) :=
retType md.
Definition mbody C m md
(witn: method C m md) :=
methodBody md.
Definition mparam C m md
(witn: method C m md) :=
argName md.
Definition class_name_methods : class -> list MethDecl :=
fun _ => match classDecls P with
| nil => nil
| _ => nil
end.
Definition fld : class -> FieldName_type -> Prop :=
fun _ _ => classDecls P = nil.
Definition ftype : forall C f,
fld C f -> class :=
fun C _ _ => C.
(* destruct (ant.fn.constructFresh nil). *)
(* auto. *)
(* Defined. *)
Definition fields : class -> list FieldName_type -> Prop.
Admitted.
Definition fieldsList : class -> list FieldName_type.
Admitted.
Theorem fieldsListIsFields :
forall C,
fields C (fieldsList C).
Admitted.
Theorem fld_in_flds C f fields_lst:
fld C f ->
fields C fields_lst ->
In f fields_lst.
Admitted.
Definition subclass : class -> class -> Prop :=
fun _ _ => classDecls P = nil.
Theorem method_subclass C D m md :
method D m md ->
subclass C D ->
method C m md.
admit.
Admitted.
Theorem subclass_refl C :
subclass C C.
admit.
Admitted.
Theorem subclass_trans C D E:
subclass C D -> subclass D E -> subclass C E.
admit.
Admitted.
Theorem field_subclass C D f :
fld D f ->
subclass C D ->
fld C f.
admit.
Admitted.
Theorem ftype_subclass C D f (f_witn: fld D f)
(sub_witn: subclass C D):
ftype D f f_witn = ftype C f (field_subclass C D f f_witn sub_witn).
admit.
Admitted.
Theorem unique_ftype C f (f_witn1 f_witn2: fld C f) :
ftype C f f_witn1 = ftype C f f_witn2.
admit.
Admitted.
Inductive subtype : typecheck_type -> typecheck_type -> Prop :=
| classSub : forall C D, subclass C D -> subtype (typt_class C) (typt_class D)
| boxSub : forall C D, subclass C D -> subtype (typt_box C) (typt_box D)
| allSub : forall sigma, subtype sigma typt_all.
Lemma subtype_and_subclass_lemma C' C :
subtype (typt_class C') (typt_class C) ->
subclass C' C.
Admitted.
Definition ocap : class -> Prop.
Admitted.
Theorem ocap_dec : forall C, ocap C \/ ~ (ocap C).
Admitted.
Fixpoint lookup_l (c: class) (l: list ClassDecl) : option ClassDecl :=
match l with
| nil => None
| cd :: cds => if class_eq_dec c (cls cd)
then (Some cd)
else (lookup_l c cds)
end.
Definition lookup (c: class) : option ClassDecl :=
lookup_l c (classDecls P).
End MethodsAndFields.