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
|
%% Some examples of usage of lists
%% (trying to gather the interesting cases from minicaml)
indexvar i, j, k, l, m, n ::=
metavar x ::=
grammar
t, term :: t_ ::=
| x :: :: x
| letrec lb1 and ... and lbn in t :: :: letrec
lb, letrec_binding :: lb_ ::=
| x = t :: :: simple
b, binding :: b_ ::=
| x :: :: x
E, environment :: E_ ::=
| b1 , .. , bn :: :: concrete
| nil :: M :: nil {{ ich wibble }}
| E1 , .... , En :: M :: concat {{ ich wibble }}
defns Typing :: Typing_ ::=
defn
E |- ok :: :: ok :: ok_ by
---------------------------------------------------------------- :: nil
nil |- ok
E |- ok
---------------------------------------------------------------- :: x
E, x |- ok
defn
E |- t :: :: term :: term_ by
E1, x, E2 |- ok
---------------------------------------------------------------- :: x
E1, x, E2 |- x
E, E1, ... , En |- lb1 gives E1 ... E, E1, ... , En |- lbn
E, E1, ... , En |- t
---------------------------------------------------------------- :: letrec
E |- letrec lb1 and ... and lbn in t
defn
E |- lb gives E' :: :: lb :: lb_ by
E |- t
---------------------------------------------------------------- :: simple
E |- x = t gives x
|
