dk_obj.sk 5.83 KB
Newer Older
1
#NAME dk_obj.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
2

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
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
(;

Copyright Raphaël Cauderlier (2014)

<raphael.cauderlier@inria.fr>

This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.

This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software.  You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".

As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.

In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.

The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.

37
 ;)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
38

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
39
(; Labels ;)
40
def label := string.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
41
42

(; Object types ;)
43
def type := dk_type.type.  (; type := list (label * type) ;)
44
45
def Ot_nil := dk_type.tnil.
def Ot_cons := dk_type.tcons.
46
47
def Ot_st := dk_type.st.
def Ot_domain_subtype := dk_type.domain_subtype.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
48

49
def pos := dk_type.pos.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
50

51
52
53
54
55
56
57
58
59
60
61
62
(; Expressions, methods and objects ;)
PreObj : type -> type -> Type.
def Expr : type -> Type.
[A] Expr A --> PreObj A A.

Po_nil : A : type ->
         PreObj A Ot_nil.
Po_cons : A : type ->
          D : type ->
          l : label ->
          B : type ->
          (Expr A -> Expr B) ->
63
          PreObj A D ->
64
          PreObj A (Ot_cons l B D).
65

66
67
def preselect : A : type ->
                D : type ->
68
                o : PreObj A D ->
69
70
71
                l : label ->
                B : type ->
                pos l B D ->
72
                Expr A ->
73
                Expr B.
74

75
[m] preselect _ _ (Po_cons _ _ _ _ m _) _ _ (dk_type.at_head _ _ _) --> m.
76
77

[A,D,l,l2,o,H,Htl]
78
    preselect
79
80
81
    _
    _
    (Po_cons A D _ _ _ o)
82
83
    l
      H
84
      (dk_type.in_tail _ _ _ _ _ Htl)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
85
      -->
86
    preselect A D o l H Htl.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
87

88
89
def preupdate : A : type ->
                D : type ->
90
                o : PreObj A D ->
91
92
93
94
                l : label ->
                B : type ->
                H : pos l B D ->
                (Expr A -> Expr B) ->
95
                PreObj A D.
96
[A,D,l,B,o,m2]
97
    preupdate
98
99
    _
    _
100
101
    (Po_cons A D l B _ o)
    _
102
    _
103
      (dk_type.at_head _ _ _)
104
      m2
105
      -->
106
    Po_cons A D l B m2 o
107

108
[A,D,l,l2,B,m1,m2,o,p,C]
109
    preupdate
110
111
112
      _
      _
      (Po_cons A D l2 B m1 o)
113
      l
114
115
        C
        (dk_type.in_tail _ _ _ _ _ p)
116
        m2
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
117
      -->
118
    Po_cons A D l2 B m1 (preupdate A D o l C p m2).
119

120
def obj_select : A : type ->
121
                 eA : Expr A ->
122
123
124
125
126
127
                 l : label ->
                 B : type ->
                 pos l B A ->
                 Expr B.
[A,o,l,B,p]
    obj_select A o l B p
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
128
129
130
      -->
    preselect
      A
131
      A
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
132
133
      o
        l
134
135
        B
        p
136
          o.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
137

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
138
139
140
141
(; The definitions of select and update
   are limited to objects so that selection
   and updating other expressions is still definable. ;)

142
def select : A : type ->
143
             eA : Expr A ->
144
145
146
147
148
149
             l : label ->
             B : type ->
             pos l B A ->
             Expr B.
[A,D,l,B,m,po]
    select _ (Po_cons A D l B m po)
150
      -->
151
    obj_select A (Po_cons A D l B m po).
152

153
def obj_update : A : type ->
154
                 eA : Expr A ->
155
156
157
158
                 l : label ->
                 B : type ->
                 pos l B A ->
                 (Expr A -> Expr B) ->
159
                 Expr A.
160
[A] obj_update A --> preupdate A A.
161

162
def update : A : type ->
163
             eA : Expr A ->
164
165
166
167
             l : label ->
             B : type ->
             pos l B A ->
             (Expr A -> Expr B) ->
168
             Expr A.
169
170
[A,D,l,B,m,po]
    update _ (Po_cons A D l B m po)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
171
      -->
172
    obj_update A (Po_cons A D l B m po).
173

174
175
176
def preinit : A : type ->
              C : type ->
              (l : label -> B : type -> pos l B C -> pos l B A) ->
177
              PreObj A C.
178
179
180
[A] preinit A dk_type.tnil _ --> Po_nil A
[A,l,B,C,Hsub]
    preinit A (dk_type.tcons l B C) Hsub
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
181
182
183
184
      -->
    Po_cons
      A
      C
185
      l
186
187
      B
      (self : Expr A => select A self l B (Hsub l B (dk_type.at_head l B C)))
188
      (preinit A C
189
190
               (l2 : label => B' : type => p : pos l2 B' C =>
                Hsub l2 B' (dk_type.in_tail l2 B' l B C p))).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
191

192
193
def init : A : type -> Expr A.
[A] init A --> preinit A A (l : label => B : type => p : pos l B A => p).
194

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
195
196
(; Subtyping ;)

197
198
def coerce : A : type ->
             B : type ->
199
200
201
202
             Ot_st A B ->
             Expr A ->
             Expr B.

203
204
[A,B,st,a]
    select _ (coerce A B st a)
205
      -->
206
207
      (l : label => C : type => p : pos l C B =>
    select A a l C (dk_type.domain_subtype A B st l C p)).
208

209
210
[A,B,st,a]
    update _ (coerce A B st a)
211
      -->
212
    (l : label => C : type => p : pos l C B => m : (Expr B -> Expr C) =>
213
    coerce A B st
214
215
216
             (update A a l C (dk_type.domain_subtype A B st l C p)
                             (self : Expr A =>
                              m (coerce A B st self)))).
217
[A,B,C,stAB,stBC,a]
218
    coerce B C stBC (coerce A _ stAB a)
219
220
      -->
    coerce A C (dk_type.st_trans A B C stAB stBC) a.