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
|
% The TAPL E-Rcd rule uses a slightly different indexing form,
% {li=vi ^{i IN 1..j-1}, lj=tj, lk=tk^{k IN j+1..n}
% which ott does not support, so that rule is slightly rephrased here.
grammar
T {{ hol Typ }}, S, U :: Ty ::= {{ com types: }}
| { </ li : Ti // , // i IN 1 .. n /> } :: :: Record {{ com type of records }}
t :: Tm ::= {{ com terms: }}
| { </ li = ti // , // i IN 1 .. n /> } :: :: Record {{ com record }}
| t . l :: :: Proj {{ com projection }}
v :: Va ::= {{ com values: }}
| { </ li = vi // , // i IN 1 .. n /> } :: :: Record {{ com record value }}
subrules
v <:: t
defns
Jop :: '' ::=
defn
t --> t' :: :: red :: E_ {{ com Evaluation }} by
---------------------------------- :: ProjRcd
{ </li=vi//i IN 1..n/> }.lj --> vj
t1 --> t1'
-------------- :: Proj
t1.l --> t1'.l
t --> t'
------------------------------------------------------------------------ :: Rcd
{ </li=vi//i IN 1..m/>,l=t,</lj'=tj//j IN 1..n/>} --> { </li=vi//i IN 1..m/>,l=t',</lj'=tj//j IN 1..n/>}
defns
Jtype :: '' ::=
defn
G |- t : T :: :: typing :: T_ {{ com Typing }} by
</ G|-ti:Ti // i IN 1..n />
DISTINCT </li // i IN 1..n />
----------------------------------------------------------- :: Rcd
G|- { </ li=ti // i IN 1..n /> }:{ </ li:Ti // i IN 1..n /> }
G|- t1:{ </ li:Ti // i IN 1..n /> }
----------------------------------- :: Proj
G|- t1.lj : Tj
|
