← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/RefMan-modr.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/RefMan-modr.tex
 
1
\chapter[The Module System]{The Module System\label{chapter:Modules}}
 
2
 
 
3
The module system extends the Calculus of Inductive Constructions
 
4
providing a convenient way to structure large developments as well as
 
5
a mean of massive abstraction.
 
6
%It is described in details in Judicael's thesis and Jacek's thesis
 
7
 
 
8
\section{Modules and module types}
 
9
 
 
10
\paragraph{Access path.} It is denoted by $p$, it can be either a module 
 
11
variable $X$ or, if $p'$ is an access path and $id$ an identifier, then
 
12
$p'.id$ is an access path.
 
13
 
 
14
\paragraph{Structure element.} It is denoted by \elem\ and is either a
 
15
definition of a constant, an assumption, a definition of an inductive,
 
16
 a definition of a module, an alias of module or a module type abbreviation.
 
17
 
 
18
\paragraph{Structure expression.} It is denoted by $S$ and can be:
 
19
\begin{itemize}
 
20
\item an access path $p$
 
21
\item a plain structure $\struct{\nelist{\elem}{;}}$
 
22
\item a functor $\functor{X}{S}{S'}$, where $X$ is a module variable,
 
23
  $S$ and $S'$ are structure expression
 
24
\item an application $S\,p$, where $S$ is a structure expression and $p$ 
 
25
an access path 
 
26
\item a refined structure $\with{S}{p}{p'}$ or $\with{S}{p}{t:T}$ where $S$
 
27
is a structure expression, $p$ and $p'$ are access paths, $t$ is a term 
 
28
and $T$ is the type of $t$.
 
29
\end{itemize}
 
30
The symbol $W$ will be used to denote a plain structure or a functor.
 
31
\paragraph{Module definition,} is written $\Mod{X}{S}{S'}$ and
 
32
 consists of a module variable $X$, a module type
 
33
$S$ which can be any structure expression and optionally a module implementation $S'$ 
 
34
 which can be any structure expression except a refined structure.
 
35
 
 
36
\paragraph{Module alias,} is written $\ModA{X}{p}$ and
 
37
 consists of a module variable $X$ and a module path $p$. 
 
38
 
 
39
\paragraph{Module type abbreviation,} is written $\ModType{Y}{S}$, where
 
40
$Y$ is an identifier and $S$ is any structure expression .
 
41
 
 
42
 
 
43
\section{Typing Modules}
 
44
 
 
45
In order to introduce the typing system we first slightly extend
 
46
the syntactic class of terms and environments given in
 
47
section~\ref{Terms}. The environments, apart from definitions of
 
48
constants and inductive types now also hold any other structure elements.
 
49
Terms, apart from variables, constants and complex terms, 
 
50
include also access paths.
 
51
 
 
52
We also need additional typing judgments: 
 
53
\begin{itemize}
 
54
\item \WFT{E}{S}, denoting that a structure $S$ is well-formed, 
 
55
 
 
56
\item \WTM{E}{p}{S}, denoting that the module pointed by $p$ has type $S$ in
 
57
environment $E$.
 
58
 
 
59
\item \WEV{E}{S}{W}, denoting that a structure $S$ is evaluated to 
 
60
a structure $W$ in weak head normal form.
 
61
 
 
62
\item \WS{E}{S_1}{S_2}, denoting that a structure $S_1$ is a subtype of a
 
63
structure $S_2$.
 
64
 
 
65
\item \WS{E}{\elem_1}{\elem_2}, denoting that a structure element
 
66
  $\elem_1$ is more precise that a structure element $\elem_2$.
 
67
\end{itemize}
 
68
The rules for forming structures are the following:
 
69
\begin{description}
 
70
\item[WF-STR]
 
71
\inference{%
 
72
  \frac{
 
73
    \WF{E;E'}{}
 
74
  }{%%%%%%%%%%%%%%%%%%%%%
 
75
    \WFT{E}{\struct{E'}}
 
76
  }
 
77
}
 
78
\item[WF-FUN]
 
79
\inference{%
 
80
  \frac{
 
81
    \WEV{E;\ModS{X}{S}}{S'}{W}\qquad\WFT{E;\ModS{X}{S}}{W}
 
82
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%
 
83
    \WFT{E}{\functor{X}{S}{S'}}
 
84
  }
 
85
}
 
86
\end{description}
 
87
Evaluation of structures to weak head normal form:
 
88
\begin{description}
 
89
\item[WEVAL-APP]
 
90
\inference{%
 
91
  \frac{
 
92
    \begin{array}{c}
 
93
    \WEV{E}{S}{\functor{X}{S_1}{S_2}}~~~~~\WEV{E}{S_1}{W_1}\\
 
94
    \WTM{E}{p}{W_3}\qquad \WS{E}{W_3}{W_1}
 
95
    \end{array}
 
96
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
97
    \WEV{E}{S\,p}{S_2\{p/X,t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}}
 
98
  }
 
99
}
 
100
\end{description}
 
101
In the last rule, $\{t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}$ is the resulting
 
102
 substitution from the inlining mechanism. We substitute in $S$ the
 
103
 inlined fields $p_i.c_i$ form $\ModS{X}{S_1}$ by the corresponding delta-reduced term $t_i$ in~$p$.
 
104
\begin{description}
 
105
\item[WEVAL-WITH-MOD]
 
106
\inference{%
 
107
  \frac{
 
108
    \begin{array}{c}
 
109
    \WEV{E}{S}{\structe{\ModS{X}{S_1}}}~~~~~\WEV{E;\elem_1;\ldots;\elem_{i-1}}{S_1}{W_1}\\
 
110
    \WTM{E}{p}{W_2}\qquad \WS{E;\elem_1;\ldots;\elem_{i-1}}{W_2}{W_1}
 
111
    \end{array}
 
112
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
113
    \begin{array}{c}
 
114
    \WEVT{E}{\with{S}{x}{p}}{\structes{\ModA{X_1}{p}}{p/X}}
 
115
    \end{array}
 
116
  }
 
117
}
 
118
\item[WEVAL-WITH-MOD-REC]
 
119
\inference{%
 
120
  \frac{
 
121
    \begin{array}{c}
 
122
    \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
 
123
    \WEV{E;\elem_1;\ldots;\elem_{i-1}}{\with{S_1}{p}{p_1}}{W_1}
 
124
    \end{array}
 
125
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
126
    \begin{array}{c}
 
127
    \WEVT{E}{\with{S}{X_1.p}{p_1}}{\structes{\ModS{X_1}{W_1}}{p_1/X_1.p}}
 
128
    \end{array}
 
129
  }
 
130
}
 
131
\item[WEVAL-WITH-DEF]
 
132
\inference{%
 
133
  \frac{
 
134
    \begin{array}{c}
 
135
    \WEV{E}{S}{\structe{\Assum{}{c}{T_1}}}\\
 
136
    \WS{E;\elem_1;\ldots;\elem_{i-1}}{\Def{}{c}{t}{T}}{\Assum{}{c}{T_1}}
 
137
    \end{array}
 
138
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
139
    \begin{array}{c}
 
140
    \WEVT{E}{\with{S}{c}{t:T}}{\structe{\Def{}{c}{t}{T}}}
 
141
    \end{array}
 
142
  }
 
143
}
 
144
\item[WEVAL-WITH-DEF-REC]
 
145
\inference{%
 
146
  \frac{
 
147
    \begin{array}{c}
 
148
    \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
 
149
    \WEV{E;\elem_1;\ldots;\elem_{i_1}}{\with{S_1}{p}{p_1}}{W_1}
 
150
    \end{array}
 
151
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
152
    \begin{array}{c}
 
153
    \WEVT{E}{\with{S}{X_1.p}{t:T}}{\structe{\ModS{X}{W_1}}}
 
154
    \end{array}
 
155
  }
 
156
}
 
157
 
 
158
\item[WEVAL-PATH-MOD]
 
159
\inference{%
 
160
  \frac{
 
161
    \begin{array}{c}
 
162
    \WEV{E}{p}{\structe{ \Mod{X}{S}{S_1}}}\\
 
163
    \WEV{E;\elem_1;\ldots;\elem_{i-1}}{S}{W}
 
164
   \end{array}
 
165
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
166
    \WEV{E}{p.X}{W}
 
167
  }
 
168
}
 
169
\inference{%
 
170
  \frac{
 
171
    \begin{array}{c}
 
172
    \WF{E}{}~~~~~~\Mod{X}{S}{S_1}\in E\\
 
173
    \WEV{E}{S}{W}
 
174
   \end{array}
 
175
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
176
    \WEV{E}{X}{W}
 
177
  }
 
178
}
 
179
\item[WEVAL-PATH-ALIAS]
 
180
\inference{%
 
181
  \frac{
 
182
    \begin{array}{c}
 
183
    \WEV{E}{p}{\structe{\ModA{X}{p_1}}}\\
 
184
    \WEV{E;\elem_1;\ldots;\elem_{i-1}}{p_1}{W}
 
185
    \end{array}
 
186
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
187
    \WEV{E}{p.X}{W}
 
188
  }
 
189
}
 
190
\inference{%
 
191
  \frac{
 
192
    \begin{array}{c}
 
193
      \WF{E}{}~~~~~~~\ModA{X}{p_1}\in E\\
 
194
      \WEV{E}{p_1}{W}
 
195
    \end{array}
 
196
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
197
    \WEV{E}{X}{W}
 
198
  }
 
199
}
 
200
\item[WEVAL-PATH-TYPE]
 
201
\inference{%
 
202
  \frac{
 
203
    \begin{array}{c}
 
204
    \WEV{E}{p}{\structe{\ModType{Y}{S}}}\\
 
205
    \WEV{E;\elem_1;\ldots;\elem_{i-1}}{S}{W}
 
206
    \end{array}
 
207
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
208
    \WEV{E}{p.Y}{W}
 
209
  }
 
210
}
 
211
\item[WEVAL-PATH-TYPE]
 
212
\inference{%
 
213
  \frac{
 
214
    \begin{array}{c}
 
215
    \WF{E}{}~~~~~~~\ModType{Y}{S}\in E\\
 
216
    \WEV{E}{S}{W}
 
217
    \end{array}
 
218
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
219
    \WEV{E}{Y}{W}
 
220
  }
 
221
}
 
222
\end{description}
 
223
 Rules for typing module:
 
224
\begin{description}
 
225
\item[MT-EVAL-STR]
 
226
\inference{%
 
227
  \frac{
 
228
 \WEV{E}{p}{W}
 
229
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
230
    \WTM{E}{p}{W/p}
 
231
  }
 
232
}
 
233
 
 
234
\end{description}
 
235
The last rule, called strengthening is used to make all module fields
 
236
manifestly equal to themselves. The notation $W/p$ has the following
 
237
meaning:
 
238
\begin{itemize}
 
239
\item if $W\lra\struct{\elem_1;\dots;\elem_n}$ then
 
240
  $W/p=\struct{\elem_1/p;\dots;\elem_n/p}$ where $\elem/p$ is defined as
 
241
  follows:
 
242
  \begin{itemize}
 
243
  \item $\Def{}{c}{t}{T}/p\footnote{Opaque definitions are processed as assumptions.} ~=~ \Def{}{c}{t}{T}$
 
244
  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
 
245
  \item $\ModS{X}{S}/p ~=~ \ModA{X}{p.X}$
 
246
  \item $\ModA{X}{p'}/p ~=~ \ModA{X}{p'}$
 
247
  \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
 
248
  \item $\Indpstr{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}{p} ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
 
249
  \end{itemize}
 
250
\item if $W\lra\functor{X}{S'}{S''}$ then $W/p=W$
 
251
\end{itemize}
 
252
The notation $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ denotes an
 
253
inductive definition that is definitionally equal to the inductive
 
254
definition in the module denoted by the path $p$. All rules which have
 
255
$\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}$ as premises are also valid for 
 
256
$\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$. We give the formation rule
 
257
for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
 
258
the equality rules on inductive types and constructors. \\
 
259
 
 
260
The module subtyping rules:
 
261
\begin{description}
 
262
\item[MSUB-STR]
 
263
\inference{%
 
264
  \frac{
 
265
    \begin{array}{c}
 
266
      \WS{E;\elem_1;\dots;\elem_n}{\elem_{\sigma(i)}}{\elem'_i}
 
267
                                  \textrm{ \ for } i=1..m \\
 
268
      \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
 
269
    \end{array}
 
270
  }{
 
271
    \WS{E}{\struct{\elem_1;\dots;\elem_n}}{\struct{\elem'_1;\dots;\elem'_m}}
 
272
  }
 
273
}
 
274
\item[MSUB-FUN]
 
275
\inference{%       T_1 -> T_2 <: T_1' -> T_2'
 
276
  \frac{
 
277
\begin{array}{c}
 
278
  \WEV{E}{S_1}{W_1}\qquad\WEV{E}{S_1'}{W_1'}\\
 
279
  \WEV{E;\ModS{X}{S_1}}{S_2}{W_2}\qquad \WEV{E;\ModS{X}{S_1'}}{S_2'}{W_2'}\\
 
280
  \WS{E}{W_1'}{W_1}~~~~~~~~~~\WS{E;\ModS{X}{S_1'}}{W_2}{W_2'}
 
281
\end{array}
 
282
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
283
    \WS{E}{\functor{X}{S_1}{S_2}}{\functor{X}{S_1'}{S_2'}}
 
284
  }
 
285
}
 
286
% these are derived rules
 
287
% \item[MSUB-EQ]
 
288
% \inference{%
 
289
%   \frac{
 
290
%     \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
 
291
%   }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
292
%     \WS{E}{T_1'}{T_2'}
 
293
%   }
 
294
% }
 
295
% \item[MSUB-REFL]
 
296
% \inference{%
 
297
%   \frac{
 
298
%     \WFT{E}{T}
 
299
%   }{
 
300
%     \WS{E}{T}{T}
 
301
%   }
 
302
% }
 
303
\end{description}
 
304
Structure element subtyping rules:
 
305
\begin{description}
 
306
\item[ASSUM-ASSUM]
 
307
\inference{%
 
308
  \frac{
 
309
    \WTELECONV{}{T_1}{T_2}
 
310
  }{
 
311
    \WSE{\Assum{}{c}{T_1}}{\Assum{}{c}{T_2}}
 
312
  }
 
313
}
 
314
\item[DEF-ASSUM]
 
315
\inference{%
 
316
  \frac{
 
317
    \WTELECONV{}{T_1}{T_2}
 
318
  }{
 
319
    \WSE{\Def{}{c}{t}{T_1}}{\Assum{}{c}{T_2}}
 
320
  }
 
321
}
 
322
\item[ASSUM-DEF]
 
323
\inference{%
 
324
  \frac{
 
325
    \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{c}{t_2}
 
326
  }{
 
327
    \WSE{\Assum{}{c}{T_1}}{\Def{}{c}{t_2}{T_2}}
 
328
  }
 
329
}
 
330
\item[DEF-DEF]
 
331
\inference{%
 
332
  \frac{
 
333
    \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
 
334
  }{
 
335
    \WSE{\Def{}{c}{t_1}{T_1}}{\Def{}{c}{t_2}{T_2}}
 
336
  }
 
337
}
 
338
\item[IND-IND]
 
339
\inference{%
 
340
  \frac{
 
341
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
 
342
    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
 
343
    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
 
344
  }{
 
345
    \WSE{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}%
 
346
        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
 
347
  }
 
348
}
 
349
\item[INDP-IND]
 
350
\inference{%
 
351
  \frac{
 
352
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
 
353
    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
 
354
    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
 
355
  }{
 
356
    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
 
357
        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
 
358
  }
 
359
}
 
360
\item[INDP-INDP]
 
361
\inference{%
 
362
  \frac{
 
363
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
 
364
    ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
 
365
    ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
 
366
    ~~~~~~\WTECONV{}{p}{p'}
 
367
  }{
 
368
    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
 
369
        {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
 
370
  }
 
371
}
 
372
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
373
\item[MOD-MOD]
 
374
\inference{%
 
375
  \frac{
 
376
    \WSE{S_1}{S_2}
 
377
  }{
 
378
    \WSE{\ModS{X}{S_1}}{\ModS{X}{S_2}}
 
379
  }
 
380
}
 
381
\item[ALIAS-MOD]
 
382
\inference{%
 
383
  \frac{
 
384
    \WTM{E}{p}{S_1}~~~~~~~~\WSE{S_1}{S_2}
 
385
  }{
 
386
    \WSE{\ModA{X}{p}}{\ModS{X}{S_2}}
 
387
  }
 
388
}
 
389
\item[MOD-ALIAS]
 
390
\inference{%
 
391
  \frac{
 
392
      \WTM{E}{p}{S_2}~~~~~~~~
 
393
      \WSE{S_1}{S_2}~~~~~~~~\WTECONV{}{X}{p}
 
394
  }{
 
395
    \WSE{\ModS{X}{S_1}}{\ModA{X}{p}}
 
396
  }
 
397
}
 
398
\item[ALIAS-ALIAS]
 
399
\inference{%
 
400
  \frac{
 
401
    \WTECONV{}{p_1}{p_2}
 
402
  }{
 
403
    \WSE{\ModA{X}{p_1}}{\ModA{X}{p_2}}
 
404
  }
 
405
}
 
406
\item[MODTYPE-MODTYPE]
 
407
\inference{%
 
408
  \frac{
 
409
    \WSE{S_1}{S_2}~~~~~~~~\WSE{S_2}{S_1}
 
410
  }{
 
411
    \WSE{\ModType{Y}{S_1}}{\ModType{Y}{S_2}}
 
412
  }
 
413
}
 
414
\end{description}
 
415
New environment formation rules
 
416
\begin{description}
 
417
\item[WF-MOD]
 
418
\inference{%
 
419
  \frac{
 
420
    \WF{E}{}~~~~~~~~\WFT{E}{S}
 
421
  }{
 
422
    \WF{E;\ModS{X}{S}}{}
 
423
  }
 
424
}
 
425
\item[WF-MOD]
 
426
\inference{%
 
427
  \frac{
 
428
\begin{array}{c}
 
429
  \WS{E}{S_2}{S_1}\\
 
430
  \WF{E}{}~~~~~\WFT{E}{S_1}~~~~~\WFT{E}{S_2}
 
431
\end{array}
 
432
  }{
 
433
    \WF{E;\Mod{X}{S_1}{S_2}}{}
 
434
  }
 
435
}
 
436
 
 
437
\item[WF-ALIAS]
 
438
\inference{%
 
439
  \frac{
 
440
    \WF{E}{}~~~~~~~~~~~\WTE{}{p}{S}
 
441
  }{
 
442
    \WF{E,\ModA{X}{p}}{}
 
443
  }
 
444
}
 
445
\item[WF-MODTYPE]
 
446
\inference{%
 
447
  \frac{
 
448
    \WF{E}{}~~~~~~~~~~~\WFT{E}{S}
 
449
  }{
 
450
    \WF{E,\ModType{Y}{S}}{}
 
451
  }
 
452
}
 
453
\item[WF-IND]
 
454
\inference{%
 
455
  \frac{
 
456
    \begin{array}{c}
 
457
      \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
 
458
      \WT{E}{}{p:\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
 
459
      \WS{E}{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
 
460
    \end{array}
 
461
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
462
    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
 
463
  }
 
464
}
 
465
\end{description}
 
466
Component access rules
 
467
\begin{description}
 
468
\item[ACC-TYPE]
 
469
\inference{%
 
470
  \frac{
 
471
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Assum{}{c}{T};\dots}}
 
472
  }{
 
473
    \WTEG{p.c}{T}
 
474
  }
 
475
}
 
476
\\
 
477
\inference{%
 
478
  \frac{
 
479
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{T};\dots}}
 
480
  }{
 
481
    \WTEG{p.c}{T}
 
482
  }
 
483
}
 
484
\item[ACC-DELTA]
 
485
Notice that the following rule extends the delta rule defined in
 
486
section~\ref{delta}
 
487
\inference{%
 
488
  \frac{
 
489
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{U};\dots}}
 
490
  }{
 
491
    \WTEGRED{p.c}{\triangleright_\delta}{t}
 
492
  }
 
493
}
 
494
\\
 
495
In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
 
496
  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
 
497
  $[c_1:C_1;\ldots;c_n:C_n]$
 
498
\item[ACC-IND]
 
499
\inference{%
 
500
  \frac{
 
501
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
 
502
  }{
 
503
    \WTEG{p.I_j}{(p_1:P_1)\ldots(p_r:P_r)A_j}
 
504
  }
 
505
}
 
506
\inference{%
 
507
  \frac{
 
508
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
 
509
  }{
 
510
    \WTEG{p.c_m}{(p_1:P_1)\ldots(p_r:P_r){C_m}{I_j}{(I_j~p_1\ldots
 
511
       p_r)}_{j=1\ldots k}}
 
512
  }
 
513
}
 
514
\item[ACC-INDP]
 
515
\inference{%
 
516
  \frac{
 
517
    \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
 
518
  }{
 
519
    \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
 
520
  }
 
521
}
 
522
\inference{%
 
523
  \frac{
 
524
    \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
 
525
  }{
 
526
    \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
 
527
  }
 
528
}
 
529
 
 
530
\end{description}
 
531
 
 
532
% %%% replaced by \triangle_\delta
 
533
% Module path equality is a transitive and reflexive closure of the
 
534
% relation generated by ACC-MODEQ and ENV-MODEQ.
 
535
% \begin{itemize}
 
536
% \item []MP-EQ-REFL
 
537
% \inference{%
 
538
%   \frac{
 
539
%     \WTEG{p}{T}
 
540
%   }{
 
541
%     \WTEG{p}{p}
 
542
%   }
 
543
% }
 
544
% \item []MP-EQ-TRANS
 
545
% \inference{%
 
546
%   \frac{
 
547
%     \WTEGRED{p}{=}{p'}~~~~~~\WTEGRED{p'}{=}{p''}
 
548
%   }{
 
549
%     \WTEGRED{p'}{=}{p''}
 
550
%   }
 
551
% }
 
552
 
 
553
% \end{itemize}
 
554
 
 
555
 
 
556
% $Id: RefMan-modr.tex 11246 2008-07-22 15:10:05Z soubiran $
 
557
 
 
558
%%% Local Variables: 
 
559
%%% mode: latex
 
560
%%% TeX-master: "Reference-Manual"
 
561
%%% End: 
 
562