Skip to content

Commit 51cfb62

Browse files
codedotcodedot
committed
Fork 'standard' from 'optimal'
1 parent e69b66f commit 51cfb62

3 files changed

Lines changed: 222 additions & 0 deletions

File tree

‎encoding/index.js‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ const generic = require("./generic");
44
const abstract = require("./abstract");
55
const closed = require("./closed");
66
const optimal = require("./optimal");
7+
const standard = require("./standard");
78

89
const expand = generic.expand;
910
const readback = generic.readback;
@@ -30,3 +31,4 @@ function addalgo(name, algo)
3031
addalgo("abstract", abstract);
3132
addalgo("closed", closed);
3233
addalgo("optimal", optimal);
34+
addalgo("standard", standard);

‎encoding/standard/index.js‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
"use strict";
2+
3+
const fs = require("fs");
4+
const path = require("path");
5+
6+
const template = fs.readFileSync(path.join(__dirname, "template.txt"), "utf8");
7+
8+
let mkwire, mktwins, getfv;
9+
10+
function psi(shared, list)
11+
{
12+
for (const atom in shared) {
13+
const twins = shared[atom];
14+
const wleft = twins.left;
15+
const wright = twins.right;
16+
const agent = `\\fan_{0}`;
17+
const tree = `${agent}(${wright}, ${wleft})`;
18+
19+
list.push(`${atom} = ${tree}`);
20+
}
21+
}
22+
23+
function mkscope(n, s)
24+
{
25+
for (let i = 0; i < n; i++)
26+
s = `\\scope_{0}(${s})`;
27+
28+
return s;
29+
}
30+
31+
function gamma(obj, root, list)
32+
{
33+
const node = obj.node;
34+
35+
if ("atom" == node) {
36+
if (obj.free) {
37+
const name = `this.mkid(${obj.name})`;
38+
const agent = `\\atom_{${name}}`;
39+
40+
list.push(`${root} = ${agent}`);
41+
} else {
42+
const agent = mkscope(obj.index, root);
43+
44+
list.push(`${obj.name} = ${agent}`);
45+
}
46+
} else if ("abst" == node) {
47+
const id = obj.var;
48+
const body = obj.body;
49+
const fv = getfv(body);
50+
const wire = mkwire();
51+
const agent = (id in fv) ? id : "\\erase";
52+
const tree = `\\lambda(${agent}, ${wire})`;
53+
54+
list.push(`${root} = ${tree}`);
55+
56+
gamma(body, wire, list);
57+
} else if ("appl" == node) {
58+
const wleft = mkwire();
59+
const wright = mkwire();
60+
const left = obj.left;
61+
const right = obj.right;
62+
const shared = mktwins(left, right);
63+
const agent = `\\apply(${wright}, ${root})`;
64+
65+
list.push(`${wleft} = ${agent}`);
66+
67+
gamma(left, wleft, list);
68+
gamma(right, wright, list);
69+
70+
psi(shared, list);
71+
}
72+
}
73+
74+
function encode(generic, term)
75+
{
76+
const inconfig = [
77+
"\\read_{this.mkhole()}(!print) = root"
78+
];
79+
80+
mkwire = generic.mkwire;
81+
mktwins = generic.mktwins;
82+
getfv = generic.getfv;
83+
84+
gamma(term, "root", inconfig);
85+
86+
inconfig.inet = template;
87+
return inconfig;
88+
}
89+
90+
module.exports = encode;

‎encoding/standard/template.txt‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
\fan_{i}[\scope_{j}(a), \scope_{j}(b)] {
2+
/* Duplicate higher delimiter. */
3+
if (i < j)
4+
++this.total;
5+
else
6+
return false;
7+
} \scope_{j}[\fan_{i}(a, b)];
8+
9+
\scope_{i}[\fan_{j + 1}(a, b)] {
10+
/* Level up higher or matching fan. */
11+
if (i <= j)
12+
++this.total;
13+
else
14+
return false;
15+
} \fan_{j}[\scope_{i}(a), \scope_{i}(b)];
16+
17+
\scope_{i}[\scope_{j + 1}(a)] {
18+
/* Level up higher delimiter. */
19+
if (i < j)
20+
++this.total;
21+
else
22+
return false;
23+
} \scope_{j}[\scope_{i}(a)];
24+
25+
\print {
26+
/* Ignore delimiter. */
27+
++this.total;
28+
} \scope_{i}[!print];
29+
30+
\read_{C}[\scope_{i}(a)] {
31+
/* Pass through context. */
32+
++this.total;
33+
} \scope_{i}[\read_{C}(a)];
34+
35+
\scope_{i}[a] {
36+
/* Annihilate matching delimiters. */
37+
if (i == j)
38+
++this.total;
39+
else
40+
return false;
41+
} \scope_{j}[a];
42+
43+
\scope_{i}[\apply(a, b)] {
44+
/* Pass through application. */
45+
++this.total;
46+
} \apply[\scope_{i}(a), \scope_{i}(b)];
47+
48+
\scope_{i}[\lambda(a, b)] {
49+
/* Level up delimiter. */
50+
++this.total;
51+
} \lambda[\scope_{i + 1}(a), \scope_{i + 1}(b)];
52+
53+
\scope_{i}[\atom_{M}] {
54+
/* Return an atom. */
55+
++this.total;
56+
} \atom_{M};
57+
58+
\read_{C}[\fan_{i}(a, b)] {
59+
/* Duplicate context. */
60+
++this.total;
61+
} \fan_{i}[\read_{C}(a), \read_{this.clone(C)}(b)];
62+
63+
\print {
64+
/* Output results of read-back. */
65+
this.nf = M;
66+
++this.total;
67+
} \atom_{M};
68+
69+
\read_{C}[a] {
70+
/* Read back abstraction. */
71+
++this.total;
72+
} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
73+
74+
\apply[\read_{this.appl(M)}(a), a] {
75+
/* Read back application. */
76+
++this.total;
77+
} \atom_{M};
78+
79+
\read_{C}[\atom_{this.atom(C, M)}] {
80+
/* Read back an atom. */
81+
++this.total;
82+
} \atom_{M};
83+
84+
\fan_{i}[\atom_{M}, \atom_{M}] {
85+
/* Duplicate an atom. */
86+
++this.total;
87+
} \atom_{M};
88+
89+
\apply[\scope_{0}(a), \scope_{0}(b)] {
90+
/* Apply beta reduction. */
91+
++this.beta;
92+
++this.total;
93+
} \lambda[a, b];
94+
95+
\fan_{i}[\apply(a, b), \apply(c, d)] {
96+
/* Duplicate application. */
97+
++this.total;
98+
} \apply[\fan_{i}(a, c), \fan_{i}(b, d)];
99+
100+
\fan_{i}[\lambda(a, b), \lambda(c, d)] {
101+
/* Level up fan. */
102+
++this.total;
103+
} \lambda[\fan_{i + 1}(a, c), \fan_{i + 1}(b, d)];
104+
105+
\fan_{i}[a, b] {
106+
/* Annihilate matching fans. */
107+
if (i == j)
108+
++this.total;
109+
else
110+
return false;
111+
} \fan_{j}[a, b];
112+
113+
\fan_{i}[\fan_{j}(a, b), \fan_{j}(c, d)] {
114+
/* Duplicate higher fan. */
115+
if (i < j)
116+
++this.total;
117+
else
118+
return false;
119+
} \fan_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
120+
121+
$$
122+
123+
INCONFIG
124+
125+
$$
126+
127+
READBACK
128+
129+
this.beta = 0;
130+
this.total = 0;

0 commit comments

Comments
 (0)