-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathtemplate.txt
More file actions
126 lines (103 loc) · 2.35 KB
/
template.txt
File metadata and controls
126 lines (103 loc) · 2.35 KB
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
\fan_{i}[\scope_{j}(a), \scope_{j}(b)] {
/* Duplicate higher delimiter. */
if (i < j)
this.debug.o();
else
return false;
} \scope_{j}[\fan_{i}(a, b)];
\scope_{i}[\fan_{j + 1}(a, b)] {
/* Level up higher or matching fan. */
if (i <= j)
this.debug.o();
else
return false;
} \fan_{j}[\scope_{i}(a), \scope_{i}(b)];
\scope_{i}[\scope_{j + 1}(a)] {
/* Level up higher delimiter. */
if (i < j)
this.debug.o();
else
return false;
} \scope_{j}[\scope_{i}(a)];
\print {
/* Ignore delimiter. */
this.debug.o();
} \scope_{i}[!print];
\read_{C}[\scope_{i}(a)] {
/* Pass through context. */
this.debug.o();
} \scope_{i}[\read_{C}(a)];
\scope_{i}[a] {
/* Annihilate matching delimiters. */
if (i == j)
this.debug.o();
else
return false;
} \scope_{j}[a];
\scope_{i}[\apply(a, b)] {
/* Pass through application. */
this.debug.o();
} \apply[\scope_{i}(a), \scope_{i}(b)];
\scope_{i}[\lambda(a, b)] {
/* Level up delimiter. */
this.debug.o();
} \lambda[\scope_{i + 1}(a), \scope_{i + 1}(b)];
\scope_{i}[\atom_{M}] {
/* Return an atom. */
this.debug.o();
} \atom_{M};
\read_{C}[\fan_{i}(a, b)] {
/* Duplicate context. */
this.debug.o();
} \fan_{i}[\read_{C}(a), \read_{this.clone(C)}(b)];
\print {
/* Output results of read-back. */
this.nf = M;
this.debug.o();
} \atom_{M};
\read_{C}[\scope_{0}(a)] {
/* Read back abstraction. */
this.debug.o();
} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
\apply[\read_{this.appl(M)}(a), a] {
/* Read back application. */
this.debug.o();
} \atom_{M};
\read_{C}[\atom_{this.atom(C, M)}] {
/* Read back an atom. */
this.debug.o();
} \atom_{M};
\fan_{i}[\atom_{M}, \atom_{M}] {
/* Duplicate an atom. */
this.debug.o();
} \atom_{M};
\apply[\scope_{0}(a), \scope_{0}(b)] {
/* Apply beta reduction. */
this.debug.b();
} \lambda[a, b];
\fan_{i}[\apply(a, b), \apply(c, d)] {
/* Duplicate application. */
this.debug.o();
} \apply[\fan_{i}(a, c), \fan_{i}(b, d)];
\fan_{i}[\lambda(a, b), \lambda(c, d)] {
/* Level up fan. */
this.debug.o();
} \lambda[\fan_{i + 1}(a, c), \fan_{i + 1}(b, d)];
\fan_{i}[a, b] {
/* Annihilate matching fans. */
if (i == j)
this.debug.a();
else
return false;
} \fan_{j}[a, b];
\fan_{i}[\fan_{j}(a, b), \fan_{j}(c, d)] {
/* Duplicate higher fan. */
if (i < j)
this.debug.d();
else
return false;
} \fan_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
$$
INCONFIG
$$
READBACK