Alpha equivalence checker for arbitrary lambda terms
Initial commit
author
vm.fail
date
(Jul 26, 2026, 12:37 AM UTC)
commit
29a2d74b
29a2d74bb09f7dbcb810795480dafd7b740be14e
vm.fail
date
(Jul 26, 2026, 12:37 AM UTC)
commit
29a2d74b
29a2d74bb09f7dbcb810795480dafd7b740be14e
+9591
+5
.gitignore
+5
.gitignore
+68
README.md
+68
README.md
···
1
+
# ego
2
+
3
+
Analyzes alpha equivalence in untyped lambda calculus terms. The OCaml
4
+
and Nim implementations keep the 4 binding representations independent:
5
+
6
+
- named variables
7
+
- de bruijn indices
8
+
- locally nameless terms
9
+
- explicit substitutions
10
+
11
+
each representation implements parsing conversion, pretty printing, free
12
+
variable analysis, alpha equivalence, capture avoiding substitution and
13
+
normalisation according to its own binding semantics
14
+
15
+
## Surface syntax
16
+
17
+
```text
18
+
x variable
19
+
\x. x abstraction
20
+
\x. \y. x y nested abstraction
21
+
(\x. x) y application
22
+
[x := y] t explicit substitution
23
+
```
24
+
25
+
Application is left associative and abstraction bodies extend to the right while names
26
+
match `[a-zA-Z][a-zA-Z0-9_'-]*` accordingly
27
+
28
+
## Representation contracts
29
+
30
+
Named terms store textual binders and resolve references through explicit
31
+
environments whereas substitution performs freshness generation and capture checks
32
+
33
+
De Bruijn terms encode bound references as lexical indices and retain free
34
+
variables separately and shifting is required when terms cross binder boundaries.
35
+
36
+
Locally nameless terms encode bound references as indices and free references as
37
+
names. Opening and closing enforce scope transitions; conversion and operations
38
+
reject terms that are not locally closed.
39
+
40
+
Explicit substitution terms retain substitutions in the syntax tree and reduction
41
+
propagates substitutions through variables, applications as well abstractions while
42
+
preserving alpha equivalence and delayed capture avoidance
43
+
44
+
## interfaces
45
+
46
+
All 4 implementations expose the same semantic operations:
47
+
48
+
```text
49
+
parse
50
+
pretty_print
51
+
free_variables
52
+
alpha_equivalent
53
+
substitute
54
+
normalize
55
+
convert_from_named
56
+
convert_to_named
57
+
```
58
+
59
+
The OCaml modules are `Named`, `Debruijn`, `Locally_nameless`, and
60
+
`Explicit_subst`. The Nim modules use distinct variant types for each term
61
+
representation and expose equivalent operations
62
+
63
+
## Automata renderer
64
+
65
+
This will convert automaton and transducer JSON into Graphviz
66
+
DOT, SVG, PNG, or PDF. Input states may be plain identifiers or objects with
67
+
labels and accepting state metadata. Transitions also accept explicit labels or
68
+
`read`, `write` and `action`
+26
examples/matcher.json
+26
examples/matcher.json
···
1
+
{
2
+
"name": "matcher",
3
+
"rankdir": "LR",
4
+
"start": "scan",
5
+
"accepting": ["found"],
6
+
"states": [
7
+
{"id": "scan", "label": "scan"},
8
+
{"id": "l", "label": "l"},
9
+
{"id": "la", "label": "la"},
10
+
{"id": "lam", "label": "lam"},
11
+
{"id": "lamb", "label": "lamb"},
12
+
{"id": "lambda", "label": "lambda"},
13
+
{"id": "found", "label": "found", "accepting": true}
14
+
],
15
+
"transitions": [
16
+
{"from": "scan", "to": "scan", "label": "Σ"},
17
+
{"from": "scan", "to": "l", "label": "l"},
18
+
{"from": "l", "to": "l", "label": "l"},
19
+
{"from": "l", "to": "la", "label": "a"},
20
+
{"from": "la", "to": "lam", "label": "m"},
21
+
{"from": "lam", "to": "lamb", "label": "b"},
22
+
{"from": "lamb", "to": "lambda", "label": "d"},
23
+
{"from": "lambda", "to": "found", "label": "a"},
24
+
{"from": "found", "to": "found", "label": "Σ"}
25
+
]
26
+
}
+131
examples/matcher.svg
+131
examples/matcher.svg
···
1
+
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2
+
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
3
+
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
4
+
<!-- Generated by graphviz version 14.1.5 (0)
5
+
-->
6
+
<!-- Title: matcher Pages: 1 -->
7
+
<svg width="1075pt" height="204pt"
8
+
viewBox="0.00 0.00 1075.00 204.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
9
+
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(18 185.72)">
10
+
<title>matcher</title>
11
+
<polygon fill="white" stroke="none" points="-18,18 -18,-185.72 1057.23,-185.72 1057.23,18 -18,18"/>
12
+
<!-- __start -->
13
+
<g id="node1" class="node">
14
+
<title>__start</title>
15
+
<ellipse fill="black" stroke="black" cx="2.88" cy="-51.62" rx="2.88" ry="2.88"/>
16
+
</g>
17
+
<!-- scan -->
18
+
<g id="node2" class="node">
19
+
<title>scan</title>
20
+
<ellipse fill="none" stroke="black" cx="137.69" cy="-51.62" rx="35.18" ry="35.18"/>
21
+
<text xml:space="preserve" text-anchor="middle" x="137.69" y="-47.67" font-family="Times New Roman" font-size="16.00">scan</text>
22
+
</g>
23
+
<!-- __start->scan -->
24
+
<g id="edge1" class="edge">
25
+
<title>__start->scan</title>
26
+
<path fill="none" stroke="black" d="M6.19,-51.62C16.48,-51.62 59.23,-51.62 93.04,-51.62"/>
27
+
<polygon fill="black" stroke="black" points="92.78,-54.42 100.78,-51.62 92.78,-48.82 92.78,-54.42"/>
28
+
<text xml:space="preserve" text-anchor="middle" x="54.14" y="-57.82" font-family="Times New Roman" font-size="14.00">start</text>
29
+
</g>
30
+
<!-- scan->scan -->
31
+
<g id="edge2" class="edge">
32
+
<title>scan->scan</title>
33
+
<path fill="none" stroke="black" d="M126.18,-85.29C122.02,-110.86 125.85,-136.8 137.69,-136.8 148.09,-136.8 152.31,-116.76 150.36,-94.55"/>
34
+
<polygon fill="black" stroke="black" points="153.16,-94.38 149.39,-86.79 147.6,-95.07 153.16,-94.38"/>
35
+
<text xml:space="preserve" text-anchor="middle" x="137.69" y="-143" font-family="Times New Roman" font-size="14.00">Σ</text>
36
+
</g>
37
+
<!-- l -->
38
+
<g id="node3" class="node">
39
+
<title>l</title>
40
+
<ellipse fill="none" stroke="black" cx="264.18" cy="-51.62" rx="21.57" ry="21.57"/>
41
+
<text xml:space="preserve" text-anchor="middle" x="264.18" y="-47.67" font-family="Times New Roman" font-size="16.00">l</text>
42
+
</g>
43
+
<!-- scan->l -->
44
+
<g id="edge3" class="edge">
45
+
<title>scan->l</title>
46
+
<path fill="none" stroke="black" d="M173.04,-51.62C191.74,-51.62 214.68,-51.62 232.74,-51.62"/>
47
+
<polygon fill="black" stroke="black" points="232.7,-54.42 240.7,-51.62 232.7,-48.82 232.7,-54.42"/>
48
+
<text xml:space="preserve" text-anchor="middle" x="207.74" y="-57.82" font-family="Times New Roman" font-size="14.00">l</text>
49
+
</g>
50
+
<!-- l->l -->
51
+
<g id="edge4" class="edge">
52
+
<title>l->l</title>
53
+
<path fill="none" stroke="black" d="M256.41,-72.13C250.9,-95.79 253.49,-123.19 264.18,-123.19 273.5,-123.19 276.66,-102.39 273.68,-81.4"/>
54
+
<polygon fill="black" stroke="black" points="276.45,-80.97 272.23,-73.62 270.94,-82 276.45,-80.97"/>
55
+
<text xml:space="preserve" text-anchor="middle" x="264.18" y="-129.39" font-family="Times New Roman" font-size="14.00">l</text>
56
+
</g>
57
+
<!-- la -->
58
+
<g id="node4" class="node">
59
+
<title>la</title>
60
+
<ellipse fill="none" stroke="black" cx="380.82" cy="-51.62" rx="21.57" ry="21.57"/>
61
+
<text xml:space="preserve" text-anchor="middle" x="380.82" y="-47.67" font-family="Times New Roman" font-size="16.00">la</text>
62
+
</g>
63
+
<!-- l->la -->
64
+
<g id="edge5" class="edge">
65
+
<title>l->la</title>
66
+
<path fill="none" stroke="black" d="M286.21,-51.62C303.98,-51.62 329.67,-51.62 349.64,-51.62"/>
67
+
<polygon fill="black" stroke="black" points="349.41,-54.42 357.41,-51.62 349.41,-48.82 349.41,-54.42"/>
68
+
<text xml:space="preserve" text-anchor="middle" x="322.5" y="-57.82" font-family="Times New Roman" font-size="14.00">a</text>
69
+
</g>
70
+
<!-- lam -->
71
+
<g id="node5" class="node">
72
+
<title>lam</title>
73
+
<ellipse fill="none" stroke="black" cx="512.6" cy="-51.62" rx="31.47" ry="31.47"/>
74
+
<text xml:space="preserve" text-anchor="middle" x="512.6" y="-47.67" font-family="Times New Roman" font-size="16.00">lam</text>
75
+
</g>
76
+
<!-- la->lam -->
77
+
<g id="edge6" class="edge">
78
+
<title>la->lam</title>
79
+
<path fill="none" stroke="black" d="M402.67,-51.62C421.23,-51.62 448.88,-51.62 471.69,-51.62"/>
80
+
<polygon fill="black" stroke="black" points="471.61,-54.42 479.61,-51.62 471.61,-48.82 471.61,-54.42"/>
81
+
<text xml:space="preserve" text-anchor="middle" x="441.76" y="-57.82" font-family="Times New Roman" font-size="14.00">m</text>
82
+
</g>
83
+
<!-- lamb -->
84
+
<g id="node6" class="node">
85
+
<title>lamb</title>
86
+
<ellipse fill="none" stroke="black" cx="656.68" cy="-51.62" rx="38.36" ry="38.36"/>
87
+
<text xml:space="preserve" text-anchor="middle" x="656.68" y="-47.67" font-family="Times New Roman" font-size="16.00">lamb</text>
88
+
</g>
89
+
<!-- lam->lamb -->
90
+
<g id="edge7" class="edge">
91
+
<title>lam->lamb</title>
92
+
<path fill="none" stroke="black" d="M544.43,-51.62C563.11,-51.62 587.33,-51.62 608.4,-51.62"/>
93
+
<polygon fill="black" stroke="black" points="608.31,-54.42 616.31,-51.62 608.31,-48.82 608.31,-54.42"/>
94
+
<text xml:space="preserve" text-anchor="middle" x="581.19" y="-57.82" font-family="Times New Roman" font-size="14.00">b</text>
95
+
</g>
96
+
<!-- lambda -->
97
+
<g id="node7" class="node">
98
+
<title>lambda</title>
99
+
<ellipse fill="none" stroke="black" cx="820.91" cy="-51.62" rx="51.62" ry="51.62"/>
100
+
<text xml:space="preserve" text-anchor="middle" x="820.91" y="-47.67" font-family="Times New Roman" font-size="16.00">lambda</text>
101
+
</g>
102
+
<!-- lamb->lambda -->
103
+
<g id="edge8" class="edge">
104
+
<title>lamb->lambda</title>
105
+
<path fill="none" stroke="black" d="M695.3,-51.62C714.38,-51.62 738.02,-51.62 759.56,-51.62"/>
106
+
<polygon fill="black" stroke="black" points="759.45,-54.42 767.45,-51.62 759.45,-48.82 759.45,-54.42"/>
107
+
<text xml:space="preserve" text-anchor="middle" x="732.16" y="-57.82" font-family="Times New Roman" font-size="14.00">d</text>
108
+
</g>
109
+
<!-- found -->
110
+
<g id="node8" class="node">
111
+
<title>found</title>
112
+
<ellipse fill="none" stroke="black" cx="992.63" cy="-51.62" rx="42.6" ry="42.6"/>
113
+
<ellipse fill="none" stroke="black" cx="992.63" cy="-51.62" rx="46.6" ry="46.6"/>
114
+
<text xml:space="preserve" text-anchor="middle" x="992.63" y="-47.67" font-family="Times New Roman" font-size="16.00">found</text>
115
+
</g>
116
+
<!-- lambda->found -->
117
+
<g id="edge9" class="edge">
118
+
<title>lambda->found</title>
119
+
<path fill="none" stroke="black" d="M872.83,-51.62C892.81,-51.62 915.79,-51.62 936.18,-51.62"/>
120
+
<polygon fill="black" stroke="black" points="936.14,-54.42 944.14,-51.62 936.14,-48.82 936.14,-54.42"/>
121
+
<text xml:space="preserve" text-anchor="middle" x="909.28" y="-57.82" font-family="Times New Roman" font-size="14.00">a</text>
122
+
</g>
123
+
<!-- found->found -->
124
+
<g id="edge10" class="edge">
125
+
<title>found->found</title>
126
+
<path fill="none" stroke="black" d="M977.98,-96.34C974.72,-123.06 979.6,-148.22 992.63,-148.22 1004.13,-148.22 1009.28,-128.62 1008.09,-105.63"/>
127
+
<polygon fill="black" stroke="black" points="1010.9,-105.57 1007.41,-97.84 1005.32,-106.06 1010.9,-105.57"/>
128
+
<text xml:space="preserve" text-anchor="middle" x="992.63" y="-154.42" font-family="Times New Roman" font-size="14.00">Σ</text>
129
+
</g>
130
+
</g>
131
+
</svg>
+25
examples/modulo.json
+25
examples/modulo.json
···
1
+
{
2
+
"name": "modulo",
3
+
"rankdir": "LR",
4
+
"start": "r0",
5
+
"accepting": ["r0"],
6
+
"states": [
7
+
{"id": "r0", "label": "r₀", "accepting": true},
8
+
{"id": "r1", "label": "r₁"},
9
+
{"id": "r2", "label": "r₂"},
10
+
{"id": "r3", "label": "r₃"},
11
+
{"id": "r4", "label": "r₄"}
12
+
],
13
+
"transitions": [
14
+
{"from": "r0", "to": "r0", "label": "0"},
15
+
{"from": "r0", "to": "r1", "label": "1"},
16
+
{"from": "r1", "to": "r2", "label": "0"},
17
+
{"from": "r1", "to": "r3", "label": "1"},
18
+
{"from": "r2", "to": "r4", "label": "0"},
19
+
{"from": "r2", "to": "r0", "label": "1"},
20
+
{"from": "r3", "to": "r1", "label": "0"},
21
+
{"from": "r3", "to": "r2", "label": "1"},
22
+
{"from": "r4", "to": "r3", "label": "0"},
23
+
{"from": "r4", "to": "r4", "label": "1"}
24
+
]
25
+
}
+126
examples/modulo.svg
+126
examples/modulo.svg
···
1
+
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2
+
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
3
+
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
4
+
<!-- Generated by graphviz version 14.1.5 (0)
5
+
-->
6
+
<!-- Title: modulo Pages: 1 -->
7
+
<svg width="659pt" height="406pt"
8
+
viewBox="0.00 0.00 659.00 406.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
9
+
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(18 388.17)">
10
+
<title>modulo</title>
11
+
<polygon fill="white" stroke="none" points="-18,18 -18,-388.17 641.18,-388.17 641.18,18 -18,18"/>
12
+
<!-- __start -->
13
+
<g id="node1" class="node">
14
+
<title>__start</title>
15
+
<ellipse fill="black" stroke="black" cx="2.88" cy="-184.57" rx="2.88" ry="2.88"/>
16
+
</g>
17
+
<!-- r0 -->
18
+
<g id="node2" class="node">
19
+
<title>r0</title>
20
+
<ellipse fill="none" stroke="black" cx="128.08" cy="-184.57" rx="21.57" ry="21.57"/>
21
+
<ellipse fill="none" stroke="black" cx="128.08" cy="-184.57" rx="25.57" ry="25.57"/>
22
+
<text xml:space="preserve" text-anchor="middle" x="128.08" y="-180.62" font-family="Times New Roman" font-size="16.00">r₀</text>
23
+
</g>
24
+
<!-- __start->r0 -->
25
+
<g id="edge1" class="edge">
26
+
<title>__start->r0</title>
27
+
<path fill="none" stroke="black" d="M6.02,-184.57C16.18,-184.57 60.44,-184.57 92.51,-184.57"/>
28
+
<polygon fill="black" stroke="black" points="92.51,-187.37 100.51,-184.57 92.51,-181.77 92.51,-187.37"/>
29
+
<text xml:space="preserve" text-anchor="middle" x="54.13" y="-190.77" font-family="Times New Roman" font-size="14.00">start</text>
30
+
</g>
31
+
<!-- r0->r0 -->
32
+
<g id="edge2" class="edge">
33
+
<title>r0->r0</title>
34
+
<path fill="none" stroke="black" d="M118.9,-208.55C113.51,-232.96 116.57,-260.13 128.08,-260.13 138.15,-260.13 141.75,-239.33 138.88,-217.78"/>
35
+
<polygon fill="black" stroke="black" points="141.66,-217.44 137.51,-210.05 136.14,-218.41 141.66,-217.44"/>
36
+
<text xml:space="preserve" text-anchor="middle" x="128.08" y="-266.33" font-family="Times New Roman" font-size="14.00">0</text>
37
+
</g>
38
+
<!-- r1 -->
39
+
<g id="node3" class="node">
40
+
<title>r1</title>
41
+
<ellipse fill="none" stroke="black" cx="249.46" cy="-255.57" rx="21.57" ry="21.57"/>
42
+
<text xml:space="preserve" text-anchor="middle" x="249.46" y="-251.62" font-family="Times New Roman" font-size="16.00">r₁</text>
43
+
</g>
44
+
<!-- r0->r1 -->
45
+
<g id="edge3" class="edge">
46
+
<title>r0->r1</title>
47
+
<path fill="none" stroke="black" d="M150.7,-197.42C170.86,-209.42 200.99,-227.33 222.46,-240.1"/>
48
+
<polygon fill="black" stroke="black" points="220.9,-242.43 229.21,-244.12 223.76,-237.62 220.9,-242.43"/>
49
+
<text xml:space="preserve" text-anchor="middle" x="190.77" y="-228.4" font-family="Times New Roman" font-size="14.00">1</text>
50
+
</g>
51
+
<!-- r2 -->
52
+
<g id="node4" class="node">
53
+
<title>r2</title>
54
+
<ellipse fill="none" stroke="black" cx="366.84" cy="-161.57" rx="21.57" ry="21.57"/>
55
+
<text xml:space="preserve" text-anchor="middle" x="366.84" y="-157.62" font-family="Times New Roman" font-size="16.00">r₂</text>
56
+
</g>
57
+
<!-- r1->r2 -->
58
+
<g id="edge4" class="edge">
59
+
<title>r1->r2</title>
60
+
<path fill="none" stroke="black" d="M266.5,-242.5C286.2,-226.45 319.76,-199.11 342.36,-180.7"/>
61
+
<polygon fill="black" stroke="black" points="343.96,-183.01 348.39,-175.79 340.42,-178.67 343.96,-183.01"/>
62
+
<text xml:space="preserve" text-anchor="middle" x="308.15" y="-217.59" font-family="Times New Roman" font-size="14.00">0</text>
63
+
</g>
64
+
<!-- r3 -->
65
+
<g id="node5" class="node">
66
+
<title>r3</title>
67
+
<ellipse fill="none" stroke="black" cx="601.61" cy="-228.57" rx="21.57" ry="21.57"/>
68
+
<text xml:space="preserve" text-anchor="middle" x="601.61" y="-224.62" font-family="Times New Roman" font-size="16.00">r₃</text>
69
+
</g>
70
+
<!-- r1->r3 -->
71
+
<g id="edge5" class="edge">
72
+
<title>r1->r3</title>
73
+
<path fill="none" stroke="black" d="M261.21,-274.07C270.53,-288.1 285.43,-306.33 304.03,-314.57 402.79,-358.29 452.62,-367 547.04,-314.57 568.65,-302.57 582.67,-277.84 590.93,-257.97"/>
74
+
<polygon fill="black" stroke="black" points="593.49,-259.12 593.78,-250.65 588.27,-257.09 593.49,-259.12"/>
75
+
<text xml:space="preserve" text-anchor="middle" x="425.54" y="-356.87" font-family="Times New Roman" font-size="14.00">1</text>
76
+
</g>
77
+
<!-- r2->r0 -->
78
+
<g id="edge7" class="edge">
79
+
<title>r2->r0</title>
80
+
<path fill="none" stroke="black" d="M345.06,-163.59C304.23,-167.55 213.22,-176.39 163.36,-181.24"/>
81
+
<polygon fill="black" stroke="black" points="163.17,-178.44 155.47,-182 163.71,-184.02 163.17,-178.44"/>
82
+
<text xml:space="preserve" text-anchor="middle" x="249.46" y="-180.8" font-family="Times New Roman" font-size="14.00">1</text>
83
+
</g>
84
+
<!-- r4 -->
85
+
<g id="node6" class="node">
86
+
<title>r4</title>
87
+
<ellipse fill="none" stroke="black" cx="484.23" cy="-21.57" rx="21.57" ry="21.57"/>
88
+
<text xml:space="preserve" text-anchor="middle" x="484.23" y="-17.62" font-family="Times New Roman" font-size="16.00">r₄</text>
89
+
</g>
90
+
<!-- r2->r4 -->
91
+
<g id="edge6" class="edge">
92
+
<title>r2->r4</title>
93
+
<path fill="none" stroke="black" d="M381.31,-145.23C401.71,-120.47 440.58,-73.31 463.97,-44.93"/>
94
+
<polygon fill="black" stroke="black" points="465.96,-46.92 468.89,-38.96 461.64,-43.36 465.96,-46.92"/>
95
+
<text xml:space="preserve" text-anchor="middle" x="425.54" y="-101.96" font-family="Times New Roman" font-size="14.00">0</text>
96
+
</g>
97
+
<!-- r3->r1 -->
98
+
<g id="edge8" class="edge">
99
+
<title>r3->r1</title>
100
+
<path fill="none" stroke="black" d="M581.13,-236.65C571.13,-240.41 558.63,-244.49 547.04,-246.57 450.86,-263.8 334.37,-260.43 280.48,-257.54"/>
101
+
<polygon fill="black" stroke="black" points="280.83,-254.75 272.68,-257.09 280.51,-260.34 280.83,-254.75"/>
102
+
<text xml:space="preserve" text-anchor="middle" x="425.54" y="-265.09" font-family="Times New Roman" font-size="14.00">0</text>
103
+
</g>
104
+
<!-- r3->r2 -->
105
+
<g id="edge9" class="edge">
106
+
<title>r3->r2</title>
107
+
<path fill="none" stroke="black" d="M580.57,-222.8C539.38,-210.94 445.04,-183.79 397.04,-169.97"/>
108
+
<polygon fill="black" stroke="black" points="398.01,-167.34 389.55,-167.81 396.46,-172.72 398.01,-167.34"/>
109
+
<text xml:space="preserve" text-anchor="middle" x="484.23" y="-206.83" font-family="Times New Roman" font-size="14.00">1</text>
110
+
</g>
111
+
<!-- r4->r3 -->
112
+
<g id="edge10" class="edge">
113
+
<title>r4->r3</title>
114
+
<path fill="none" stroke="black" d="M496.83,-39.65C509.58,-59.76 530.47,-93.33 547.04,-123.07 561.55,-149.09 576.81,-179.48 587.31,-200.95"/>
115
+
<polygon fill="black" stroke="black" points="584.69,-201.95 590.71,-207.91 589.72,-199.5 584.69,-201.95"/>
116
+
<text xml:space="preserve" text-anchor="middle" x="542.92" y="-129.27" font-family="Times New Roman" font-size="14.00">0</text>
117
+
</g>
118
+
<!-- r4->r4 -->
119
+
<g id="edge11" class="edge">
120
+
<title>r4->r4</title>
121
+
<path fill="none" stroke="black" d="M476.15,-42.08C470.41,-65.73 473.11,-93.13 484.23,-93.13 493.91,-93.13 497.21,-72.34 494.1,-51.35"/>
122
+
<polygon fill="black" stroke="black" points="496.87,-50.89 492.59,-43.57 491.37,-51.95 496.87,-50.89"/>
123
+
<text xml:space="preserve" text-anchor="middle" x="484.23" y="-99.33" font-family="Times New Roman" font-size="14.00">1</text>
124
+
</g>
125
+
</g>
126
+
</svg>
+23
examples/parity.dot
+23
examples/parity.dot
···
1
+
digraph "parity" {
2
+
rankdir="LR";
3
+
graph [pad="0.25", nodesep="0.7", ranksep="0.9"];
4
+
node [shape=circle, fontname="Times New Roman", fontsize=16];
5
+
edge [fontname="Times New Roman", fontsize=14, arrowsize=0.8];
6
+
"__start" [shape=point, label="", width=0.08];
7
+
"start" [label="start", shape="circle"];
8
+
"even_0" [label="even / 0", shape="doublecircle"];
9
+
"even_1" [label="even / 1", shape="circle"];
10
+
"odd_0" [label="odd / 0", shape="circle"];
11
+
"odd_1" [label="odd / 1", shape="circle"];
12
+
"__start" -> "start" [label="input"];
13
+
"start" -> "even_0" [label="0"];
14
+
"start" -> "odd_1" [label="1"];
15
+
"even_0" -> "even_0" [label="0"];
16
+
"even_0" -> "odd_1" [label="1"];
17
+
"even_1" -> "even_0" [label="0"];
18
+
"even_1" -> "odd_1" [label="1"];
19
+
"odd_0" -> "odd_0" [label="0"];
20
+
"odd_0" -> "even_1" [label="1"];
21
+
"odd_1" -> "odd_0" [label="0"];
22
+
"odd_1" -> "even_1" [label="1"];
23
+
}
+26
examples/parity.json
+26
examples/parity.json
···
1
+
{
2
+
"name": "parity",
3
+
"rankdir": "LR",
4
+
"start": "start",
5
+
"start_label": "input",
6
+
"accepting": ["even_0"],
7
+
"states": [
8
+
{"id": "start", "label": "start"},
9
+
{"id": "even_0", "label": "even / 0", "accepting": true},
10
+
{"id": "even_1", "label": "even / 1"},
11
+
{"id": "odd_0", "label": "odd / 0"},
12
+
{"id": "odd_1", "label": "odd / 1"}
13
+
],
14
+
"transitions": [
15
+
{"from": "start", "to": "even_0", "label": "0"},
16
+
{"from": "start", "to": "odd_1", "label": "1"},
17
+
{"from": "even_0", "to": "even_0", "label": "0"},
18
+
{"from": "even_0", "to": "odd_1", "label": "1"},
19
+
{"from": "even_1", "to": "even_0", "label": "0"},
20
+
{"from": "even_1", "to": "odd_1", "label": "1"},
21
+
{"from": "odd_0", "to": "odd_0", "label": "0"},
22
+
{"from": "odd_0", "to": "even_1", "label": "1"},
23
+
{"from": "odd_1", "to": "odd_0", "label": "0"},
24
+
{"from": "odd_1", "to": "even_1", "label": "1"}
25
+
]
26
+
}
examples/parity.png
examples/parity.png
This is a binary file and will not be displayed.
+126
examples/parity.svg
+126
examples/parity.svg
···
1
+
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2
+
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
3
+
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
4
+
<!-- Generated by graphviz version 14.1.5 (0)
5
+
-->
6
+
<!-- Title: parity Pages: 1 -->
7
+
<svg width="931pt" height="556pt"
8
+
viewBox="0.00 0.00 931.00 556.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
9
+
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(18 538.21)">
10
+
<title>parity</title>
11
+
<polygon fill="white" stroke="none" points="-18,18 -18,-538.21 913.32,-538.21 913.32,18 -18,18"/>
12
+
<!-- __start -->
13
+
<g id="node1" class="node">
14
+
<title>__start</title>
15
+
<ellipse fill="black" stroke="black" cx="2.88" cy="-305.97" rx="2.88" ry="2.88"/>
16
+
</g>
17
+
<!-- start -->
18
+
<g id="node2" class="node">
19
+
<title>start</title>
20
+
<ellipse fill="none" stroke="black" cx="143.25" cy="-305.97" rx="36.24" ry="36.24"/>
21
+
<text xml:space="preserve" text-anchor="middle" x="143.25" y="-302.02" font-family="Times New Roman" font-size="16.00">start</text>
22
+
</g>
23
+
<!-- __start->start -->
24
+
<g id="edge1" class="edge">
25
+
<title>__start->start</title>
26
+
<path fill="none" stroke="black" d="M5.84,-305.97C15.76,-305.97 61.44,-305.97 97.24,-305.97"/>
27
+
<polygon fill="black" stroke="black" points="97.05,-308.77 105.05,-305.97 97.05,-303.17 97.05,-308.77"/>
28
+
<text xml:space="preserve" text-anchor="middle" x="56.38" y="-312.17" font-family="Times New Roman" font-size="14.00">input</text>
29
+
</g>
30
+
<!-- even_0 -->
31
+
<g id="node3" class="node">
32
+
<title>even_0</title>
33
+
<ellipse fill="none" stroke="black" cx="311.48" cy="-392.97" rx="53.74" ry="53.74"/>
34
+
<ellipse fill="none" stroke="black" cx="311.48" cy="-392.97" rx="57.74" ry="57.74"/>
35
+
<text xml:space="preserve" text-anchor="middle" x="311.48" y="-389.02" font-family="Times New Roman" font-size="16.00">even / 0</text>
36
+
</g>
37
+
<!-- start->even_0 -->
38
+
<g id="edge2" class="edge">
39
+
<title>start->even_0</title>
40
+
<path fill="none" stroke="black" d="M175.91,-322.54C197.33,-333.75 226.26,-348.89 251.82,-362.27"/>
41
+
<polygon fill="black" stroke="black" points="250.25,-364.61 258.64,-365.84 252.85,-359.65 250.25,-364.61"/>
42
+
<text xml:space="preserve" text-anchor="middle" x="216.61" y="-350.46" font-family="Times New Roman" font-size="14.00">0</text>
43
+
</g>
44
+
<!-- odd_1 -->
45
+
<g id="node6" class="node">
46
+
<title>odd_1</title>
47
+
<ellipse fill="none" stroke="black" cx="492.44" cy="-265.97" rx="48.97" ry="48.97"/>
48
+
<text xml:space="preserve" text-anchor="middle" x="492.44" y="-262.02" font-family="Times New Roman" font-size="16.00">odd / 1</text>
49
+
</g>
50
+
<!-- start->odd_1 -->
51
+
<g id="edge3" class="edge">
52
+
<title>start->odd_1</title>
53
+
<path fill="none" stroke="black" d="M179.21,-300.67C200.69,-297.51 228.77,-293.52 253.74,-290.47 315.31,-282.94 386.05,-275.85 434.24,-271.25"/>
54
+
<polygon fill="black" stroke="black" points="434.37,-274.05 442.06,-270.51 433.84,-268.47 434.37,-274.05"/>
55
+
<text xml:space="preserve" text-anchor="middle" x="311.48" y="-296.67" font-family="Times New Roman" font-size="14.00">1</text>
56
+
</g>
57
+
<!-- even_0->even_0 -->
58
+
<g id="edge4" class="edge">
59
+
<title>even_0->even_0</title>
60
+
<path fill="none" stroke="black" d="M294.22,-448.4C291.83,-476.05 297.58,-500.71 311.48,-500.71 323.8,-500.71 329.72,-481.32 329.24,-457.65"/>
61
+
<polygon fill="black" stroke="black" points="332.05,-457.75 328.82,-449.91 326.46,-458.05 332.05,-457.75"/>
62
+
<text xml:space="preserve" text-anchor="middle" x="311.48" y="-506.91" font-family="Times New Roman" font-size="14.00">0</text>
63
+
</g>
64
+
<!-- even_0->odd_1 -->
65
+
<g id="edge5" class="edge">
66
+
<title>even_0->odd_1</title>
67
+
<path fill="none" stroke="black" d="M359.03,-359.93C385.23,-341.33 417.87,-318.17 444.19,-299.5"/>
68
+
<polygon fill="black" stroke="black" points="445.65,-301.89 450.55,-294.98 442.41,-297.33 445.65,-301.89"/>
69
+
<text xml:space="preserve" text-anchor="middle" x="406.34" y="-331.86" font-family="Times New Roman" font-size="14.00">1</text>
70
+
</g>
71
+
<!-- even_1 -->
72
+
<g id="node4" class="node">
73
+
<title>even_1</title>
74
+
<ellipse fill="none" stroke="black" cx="841.58" cy="-294.97" rx="53.74" ry="53.74"/>
75
+
<text xml:space="preserve" text-anchor="middle" x="841.58" y="-291.02" font-family="Times New Roman" font-size="16.00">even / 1</text>
76
+
</g>
77
+
<!-- even_1->even_0 -->
78
+
<g id="edge6" class="edge">
79
+
<title>even_1->even_0</title>
80
+
<path fill="none" stroke="black" d="M799.79,-329.35C786.29,-338.94 770.65,-348.28 754.84,-353.97 627.62,-399.73 467.13,-401.1 378.64,-397.42"/>
81
+
<polygon fill="black" stroke="black" points="378.88,-394.63 370.77,-397.07 378.63,-400.22 378.88,-394.63"/>
82
+
<text xml:space="preserve" text-anchor="middle" x="578.53" y="-398.05" font-family="Times New Roman" font-size="14.00">0</text>
83
+
</g>
84
+
<!-- even_1->odd_1 -->
85
+
<g id="edge7" class="edge">
86
+
<title>even_1->odd_1</title>
87
+
<path fill="none" stroke="black" d="M788.58,-284.55C765.68,-280.38 738.39,-275.98 713.59,-273.47 658.64,-267.91 595.64,-266.23 551.14,-265.83"/>
88
+
<polygon fill="black" stroke="black" points="551.19,-263.03 543.17,-265.77 551.15,-268.63 551.19,-263.03"/>
89
+
<text xml:space="preserve" text-anchor="middle" x="664.62" y="-279.67" font-family="Times New Roman" font-size="14.00">1</text>
90
+
</g>
91
+
<!-- odd_0 -->
92
+
<g id="node5" class="node">
93
+
<title>odd_0</title>
94
+
<ellipse fill="none" stroke="black" cx="664.62" cy="-48.97" rx="48.97" ry="48.97"/>
95
+
<text xml:space="preserve" text-anchor="middle" x="664.62" y="-45.02" font-family="Times New Roman" font-size="16.00">odd / 0</text>
96
+
</g>
97
+
<!-- odd_0->even_1 -->
98
+
<g id="edge9" class="edge">
99
+
<title>odd_0->even_1</title>
100
+
<path fill="none" stroke="black" d="M693.92,-88.76C723.97,-131.02 771.56,-197.92 804.33,-244"/>
101
+
<polygon fill="black" stroke="black" points="801.86,-245.37 808.78,-250.26 806.43,-242.12 801.86,-245.37"/>
102
+
<text xml:space="preserve" text-anchor="middle" x="750.71" y="-178.17" font-family="Times New Roman" font-size="14.00">1</text>
103
+
</g>
104
+
<!-- odd_0->odd_0 -->
105
+
<g id="edge8" class="edge">
106
+
<title>odd_0->odd_0</title>
107
+
<path fill="none" stroke="black" d="M649.36,-95.8C646.25,-122.8 651.34,-147.93 664.62,-147.93 676.35,-147.93 681.68,-128.35 680.63,-105.18"/>
108
+
<polygon fill="black" stroke="black" points="683.43,-105.06 680,-97.31 677.85,-105.51 683.43,-105.06"/>
109
+
<text xml:space="preserve" text-anchor="middle" x="664.62" y="-154.13" font-family="Times New Roman" font-size="14.00">0</text>
110
+
</g>
111
+
<!-- odd_1->even_1 -->
112
+
<g id="edge11" class="edge">
113
+
<title>odd_1->even_1</title>
114
+
<path fill="none" stroke="black" d="M535.61,-289.34C547.79,-295.09 561.33,-300.57 574.4,-303.97 652.19,-324.18 675.05,-325.6 754.84,-315.97 763.22,-314.96 771.96,-313.41 780.52,-311.6"/>
115
+
<polygon fill="black" stroke="black" points="781.04,-314.35 788.24,-309.88 779.82,-308.89 781.04,-314.35"/>
116
+
<text xml:space="preserve" text-anchor="middle" x="664.62" y="-327.93" font-family="Times New Roman" font-size="14.00">1</text>
117
+
</g>
118
+
<!-- odd_1->odd_0 -->
119
+
<g id="edge10" class="edge">
120
+
<title>odd_1->odd_0</title>
121
+
<path fill="none" stroke="black" d="M523.47,-227.67C552.66,-190.44 597.01,-133.9 627.98,-94.41"/>
122
+
<polygon fill="black" stroke="black" points="629.93,-96.46 632.67,-88.44 625.53,-93 629.93,-96.46"/>
123
+
<text xml:space="preserve" text-anchor="middle" x="578.53" y="-163.67" font-family="Times New Roman" font-size="14.00">0</text>
124
+
</g>
125
+
</g>
126
+
</svg>
+12
nim/ego.nimble
+12
nim/ego.nimble
···
1
+
version = "0.1.0"
2
+
author = "ego"
3
+
description = "Alpha-equivalence analyser for untyped lambda calculus with explicit substitutions"
4
+
license = "MIT"
5
+
srcDir = "src"
6
+
bin = @["ego"]
7
+
binDir = "."
8
+
9
+
requires "nim >= 2.0.0"
10
+
11
+
task test, "Run the test suite":
12
+
exec "nim c -r --hints:off -d:release --path:src tests/test_ego.nim"
+852
nim/results_nim.json
+852
nim/results_nim.json
···
1
+
{
2
+
"nim": {
3
+
"named": {
4
+
"apps-small": {
5
+
"alpha_us": 54,
6
+
"norm_us": 23,
7
+
"traversals": 242,
8
+
"max_depth": 60,
9
+
"mem_delta_bytes": 20512
10
+
},
11
+
"bigsubst-large": {
12
+
"alpha_us": 16151,
13
+
"norm_us": 8118,
14
+
"traversals": 4042,
15
+
"max_depth": 1020,
16
+
"mem_delta_bytes": 57376
17
+
},
18
+
"allbinders-large-a": {
19
+
"alpha_us": 44668,
20
+
"norm_us": 3819,
21
+
"traversals": 2002,
22
+
"max_depth": 1000,
23
+
"mem_delta_bytes": 40992
24
+
},
25
+
"shadow-small": {
26
+
"alpha_us": 90,
27
+
"norm_us": 15,
28
+
"traversals": 122,
29
+
"max_depth": 60,
30
+
"mem_delta_bytes": 20512
31
+
},
32
+
"allbinders-medium-b": {
33
+
"alpha_us": 3185,
34
+
"norm_us": 224,
35
+
"traversals": 502,
36
+
"max_depth": 250,
37
+
"mem_delta_bytes": 20512
38
+
},
39
+
"shadow-large": {
40
+
"alpha_us": 10151,
41
+
"norm_us": 4082,
42
+
"traversals": 2002,
43
+
"max_depth": 1000,
44
+
"mem_delta_bytes": 40992
45
+
},
46
+
"shift-large": {
47
+
"alpha_us": 7705,
48
+
"norm_us": 4495,
49
+
"traversals": 242,
50
+
"max_depth": 120,
51
+
"mem_delta_bytes": 20512
52
+
},
53
+
"shift-small": {
54
+
"alpha_us": 149,
55
+
"norm_us": 60,
56
+
"traversals": 26,
57
+
"max_depth": 12,
58
+
"mem_delta_bytes": 20512
59
+
},
60
+
"bigsubst-small": {
61
+
"alpha_us": 469,
62
+
"norm_us": 215,
63
+
"traversals": 282,
64
+
"max_depth": 80,
65
+
"mem_delta_bytes": 20512
66
+
},
67
+
"allbinders-small-a": {
68
+
"alpha_us": 246,
69
+
"norm_us": 31,
70
+
"traversals": 122,
71
+
"max_depth": 60,
72
+
"mem_delta_bytes": 20512
73
+
},
74
+
"apps-large": {
75
+
"alpha_us": 14863,
76
+
"norm_us": 6174,
77
+
"traversals": 4002,
78
+
"max_depth": 1000,
79
+
"mem_delta_bytes": 57376
80
+
},
81
+
"chain-large": {
82
+
"alpha_us": 10487,
83
+
"norm_us": 3928,
84
+
"traversals": 2002,
85
+
"max_depth": 1000,
86
+
"mem_delta_bytes": 40992
87
+
},
88
+
"leaves-small-b": {
89
+
"alpha_us": 6122,
90
+
"norm_us": 2766,
91
+
"traversals": 5554,
92
+
"max_depth": 120,
93
+
"mem_delta_bytes": 20512
94
+
},
95
+
"leaves-medium-a": {
96
+
"alpha_us": 243702,
97
+
"norm_us": 124508,
98
+
"traversals": 94379,
99
+
"max_depth": 500,
100
+
"mem_delta_bytes": 28704
101
+
},
102
+
"leaves-large-a": {
103
+
"alpha_us": 12786392,
104
+
"norm_us": 6283347,
105
+
"traversals": 1502504,
106
+
"max_depth": 2000,
107
+
"mem_delta_bytes": 127008
108
+
},
109
+
"bigsubst-medium": {
110
+
"alpha_us": 1631,
111
+
"norm_us": 820,
112
+
"traversals": 1042,
113
+
"max_depth": 270,
114
+
"mem_delta_bytes": 20512
115
+
},
116
+
"fv-small": {
117
+
"alpha_us": 52,
118
+
"norm_us": 23,
119
+
"traversals": 242,
120
+
"max_depth": 60,
121
+
"mem_delta_bytes": 20512
122
+
},
123
+
"leaves-large-b": {
124
+
"alpha_us": 13076700,
125
+
"norm_us": 7037531,
126
+
"traversals": 1502504,
127
+
"max_depth": 2000,
128
+
"mem_delta_bytes": 86048
129
+
},
130
+
"chain-medium": {
131
+
"alpha_us": 1077,
132
+
"norm_us": 298,
133
+
"traversals": 502,
134
+
"max_depth": 250,
135
+
"mem_delta_bytes": 20512
136
+
},
137
+
"allbinders-small-b": {
138
+
"alpha_us": 177,
139
+
"norm_us": 17,
140
+
"traversals": 122,
141
+
"max_depth": 60,
142
+
"mem_delta_bytes": 20512
143
+
},
144
+
"leaves-small-a": {
145
+
"alpha_us": 5721,
146
+
"norm_us": 2990,
147
+
"traversals": 5554,
148
+
"max_depth": 120,
149
+
"mem_delta_bytes": 20512
150
+
},
151
+
"fv-medium": {
152
+
"alpha_us": 742,
153
+
"norm_us": 422,
154
+
"traversals": 1002,
155
+
"max_depth": 250,
156
+
"mem_delta_bytes": 20512
157
+
},
158
+
"apps-medium": {
159
+
"alpha_us": 713,
160
+
"norm_us": 346,
161
+
"traversals": 1002,
162
+
"max_depth": 250,
163
+
"mem_delta_bytes": 20512
164
+
},
165
+
"allbinders-medium-a": {
166
+
"alpha_us": 2232,
167
+
"norm_us": 252,
168
+
"traversals": 502,
169
+
"max_depth": 250,
170
+
"mem_delta_bytes": 20512
171
+
},
172
+
"shadow-medium": {
173
+
"alpha_us": 842,
174
+
"norm_us": 238,
175
+
"traversals": 502,
176
+
"max_depth": 250,
177
+
"mem_delta_bytes": 20512
178
+
},
179
+
"fv-large": {
180
+
"alpha_us": 14043,
181
+
"norm_us": 7361,
182
+
"traversals": 4002,
183
+
"max_depth": 1000,
184
+
"mem_delta_bytes": 57376
185
+
},
186
+
"shift-medium": {
187
+
"alpha_us": 998,
188
+
"norm_us": 446,
189
+
"traversals": 102,
190
+
"max_depth": 50,
191
+
"mem_delta_bytes": 20512
192
+
},
193
+
"leaves-medium-b": {
194
+
"alpha_us": 223423,
195
+
"norm_us": 106415,
196
+
"traversals": 94379,
197
+
"max_depth": 500,
198
+
"mem_delta_bytes": 28704
199
+
},
200
+
"chain-small": {
201
+
"alpha_us": 125,
202
+
"norm_us": 17,
203
+
"traversals": 122,
204
+
"max_depth": 60,
205
+
"mem_delta_bytes": 20512
206
+
},
207
+
"allbinders-large-b": {
208
+
"alpha_us": 73724,
209
+
"norm_us": 4901,
210
+
"traversals": 2002,
211
+
"max_depth": 1000,
212
+
"mem_delta_bytes": 40992
213
+
}
214
+
},
215
+
"debruijn": {
216
+
"apps-small": {
217
+
"alpha_us": 50,
218
+
"norm_us": 24,
219
+
"traversals": 242,
220
+
"max_depth": 60,
221
+
"mem_delta_bytes": 20512
222
+
},
223
+
"bigsubst-large": {
224
+
"alpha_us": 16816,
225
+
"norm_us": 8628,
226
+
"traversals": 4042,
227
+
"max_depth": 1020,
228
+
"mem_delta_bytes": 86048
229
+
},
230
+
"allbinders-large-a": {
231
+
"alpha_us": 36805,
232
+
"norm_us": 18262,
233
+
"traversals": 2002,
234
+
"max_depth": 1000,
235
+
"mem_delta_bytes": 40992
236
+
},
237
+
"shadow-small": {
238
+
"alpha_us": 132,
239
+
"norm_us": 57,
240
+
"traversals": 122,
241
+
"max_depth": 60,
242
+
"mem_delta_bytes": 20512
243
+
},
244
+
"allbinders-medium-b": {
245
+
"alpha_us": 2086,
246
+
"norm_us": 932,
247
+
"traversals": 502,
248
+
"max_depth": 250,
249
+
"mem_delta_bytes": 20512
250
+
},
251
+
"shadow-large": {
252
+
"alpha_us": 39568,
253
+
"norm_us": 19433,
254
+
"traversals": 2002,
255
+
"max_depth": 1000,
256
+
"mem_delta_bytes": 40992
257
+
},
258
+
"shift-large": {
259
+
"alpha_us": 3179,
260
+
"norm_us": 1717,
261
+
"traversals": 242,
262
+
"max_depth": 120,
263
+
"mem_delta_bytes": 20512
264
+
},
265
+
"shift-small": {
266
+
"alpha_us": 115,
267
+
"norm_us": 52,
268
+
"traversals": 26,
269
+
"max_depth": 12,
270
+
"mem_delta_bytes": 20512
271
+
},
272
+
"bigsubst-small": {
273
+
"alpha_us": 264,
274
+
"norm_us": 164,
275
+
"traversals": 282,
276
+
"max_depth": 80,
277
+
"mem_delta_bytes": 20512
278
+
},
279
+
"allbinders-small-a": {
280
+
"alpha_us": 121,
281
+
"norm_us": 58,
282
+
"traversals": 122,
283
+
"max_depth": 60,
284
+
"mem_delta_bytes": 20512
285
+
},
286
+
"apps-large": {
287
+
"alpha_us": 13560,
288
+
"norm_us": 7313,
289
+
"traversals": 4002,
290
+
"max_depth": 1000,
291
+
"mem_delta_bytes": 86048
292
+
},
293
+
"chain-large": {
294
+
"alpha_us": 49559,
295
+
"norm_us": 29578,
296
+
"traversals": 2002,
297
+
"max_depth": 1000,
298
+
"mem_delta_bytes": 40992
299
+
},
300
+
"leaves-small-b": {
301
+
"alpha_us": 803,
302
+
"norm_us": 473,
303
+
"traversals": 5554,
304
+
"max_depth": 120,
305
+
"mem_delta_bytes": 20512
306
+
},
307
+
"leaves-medium-a": {
308
+
"alpha_us": 17306,
309
+
"norm_us": 5516,
310
+
"traversals": 94379,
311
+
"max_depth": 500,
312
+
"mem_delta_bytes": 57376
313
+
},
314
+
"leaves-large-a": {
315
+
"alpha_us": 155351,
316
+
"norm_us": 84396,
317
+
"traversals": 1502504,
318
+
"max_depth": 2000,
319
+
"mem_delta_bytes": 188448
320
+
},
321
+
"bigsubst-medium": {
322
+
"alpha_us": 1882,
323
+
"norm_us": 906,
324
+
"traversals": 1042,
325
+
"max_depth": 270,
326
+
"mem_delta_bytes": 28704
327
+
},
328
+
"fv-small": {
329
+
"alpha_us": 54,
330
+
"norm_us": 26,
331
+
"traversals": 242,
332
+
"max_depth": 60,
333
+
"mem_delta_bytes": 20512
334
+
},
335
+
"leaves-large-b": {
336
+
"alpha_us": 181925,
337
+
"norm_us": 103156,
338
+
"traversals": 1502504,
339
+
"max_depth": 2000,
340
+
"mem_delta_bytes": 188448
341
+
},
342
+
"chain-medium": {
343
+
"alpha_us": 3107,
344
+
"norm_us": 1276,
345
+
"traversals": 502,
346
+
"max_depth": 250,
347
+
"mem_delta_bytes": 20512
348
+
},
349
+
"allbinders-small-b": {
350
+
"alpha_us": 238,
351
+
"norm_us": 117,
352
+
"traversals": 122,
353
+
"max_depth": 60,
354
+
"mem_delta_bytes": 20512
355
+
},
356
+
"leaves-small-a": {
357
+
"alpha_us": 519,
358
+
"norm_us": 299,
359
+
"traversals": 5554,
360
+
"max_depth": 120,
361
+
"mem_delta_bytes": 20512
362
+
},
363
+
"fv-medium": {
364
+
"alpha_us": 967,
365
+
"norm_us": 440,
366
+
"traversals": 1002,
367
+
"max_depth": 250,
368
+
"mem_delta_bytes": 20512
369
+
},
370
+
"apps-medium": {
371
+
"alpha_us": 800,
372
+
"norm_us": 388,
373
+
"traversals": 1002,
374
+
"max_depth": 250,
375
+
"mem_delta_bytes": 20512
376
+
},
377
+
"allbinders-medium-a": {
378
+
"alpha_us": 2361,
379
+
"norm_us": 1098,
380
+
"traversals": 502,
381
+
"max_depth": 250,
382
+
"mem_delta_bytes": 20512
383
+
},
384
+
"shadow-medium": {
385
+
"alpha_us": 2177,
386
+
"norm_us": 1086,
387
+
"traversals": 502,
388
+
"max_depth": 250,
389
+
"mem_delta_bytes": 20512
390
+
},
391
+
"fv-large": {
392
+
"alpha_us": 20497,
393
+
"norm_us": 9974,
394
+
"traversals": 4002,
395
+
"max_depth": 1000,
396
+
"mem_delta_bytes": 86048
397
+
},
398
+
"shift-medium": {
399
+
"alpha_us": 863,
400
+
"norm_us": 380,
401
+
"traversals": 102,
402
+
"max_depth": 50,
403
+
"mem_delta_bytes": 20512
404
+
},
405
+
"leaves-medium-b": {
406
+
"alpha_us": 12446,
407
+
"norm_us": 6590,
408
+
"traversals": 94379,
409
+
"max_depth": 500,
410
+
"mem_delta_bytes": 57376
411
+
},
412
+
"chain-small": {
413
+
"alpha_us": 350,
414
+
"norm_us": 86,
415
+
"traversals": 122,
416
+
"max_depth": 60,
417
+
"mem_delta_bytes": 20512
418
+
},
419
+
"allbinders-large-b": {
420
+
"alpha_us": 38270,
421
+
"norm_us": 19381,
422
+
"traversals": 2002,
423
+
"max_depth": 1000,
424
+
"mem_delta_bytes": 40992
425
+
}
426
+
},
427
+
"ln": {
428
+
"apps-small": {
429
+
"alpha_us": 64,
430
+
"norm_us": 37,
431
+
"traversals": 242,
432
+
"max_depth": 60,
433
+
"mem_delta_bytes": 20512
434
+
},
435
+
"bigsubst-large": {
436
+
"alpha_us": 26387,
437
+
"norm_us": 13213,
438
+
"traversals": 4042,
439
+
"max_depth": 1020,
440
+
"mem_delta_bytes": 86048
441
+
},
442
+
"allbinders-large-a": {
443
+
"alpha_us": 41773,
444
+
"norm_us": 20839,
445
+
"traversals": 2002,
446
+
"max_depth": 1000,
447
+
"mem_delta_bytes": 40992
448
+
},
449
+
"shadow-small": {
450
+
"alpha_us": 197,
451
+
"norm_us": 86,
452
+
"traversals": 122,
453
+
"max_depth": 60,
454
+
"mem_delta_bytes": 20512
455
+
},
456
+
"allbinders-medium-b": {
457
+
"alpha_us": 3047,
458
+
"norm_us": 2242,
459
+
"traversals": 502,
460
+
"max_depth": 250,
461
+
"mem_delta_bytes": 20512
462
+
},
463
+
"shadow-large": {
464
+
"alpha_us": 51818,
465
+
"norm_us": 27772,
466
+
"traversals": 2002,
467
+
"max_depth": 1000,
468
+
"mem_delta_bytes": 40992
469
+
},
470
+
"shift-large": {
471
+
"alpha_us": 6627,
472
+
"norm_us": 3174,
473
+
"traversals": 242,
474
+
"max_depth": 120,
475
+
"mem_delta_bytes": 20512
476
+
},
477
+
"shift-small": {
478
+
"alpha_us": 115,
479
+
"norm_us": 71,
480
+
"traversals": 26,
481
+
"max_depth": 12,
482
+
"mem_delta_bytes": 20512
483
+
},
484
+
"bigsubst-small": {
485
+
"alpha_us": 393,
486
+
"norm_us": 174,
487
+
"traversals": 282,
488
+
"max_depth": 80,
489
+
"mem_delta_bytes": 20512
490
+
},
491
+
"allbinders-small-a": {
492
+
"alpha_us": 330,
493
+
"norm_us": 121,
494
+
"traversals": 122,
495
+
"max_depth": 60,
496
+
"mem_delta_bytes": 20512
497
+
},
498
+
"apps-large": {
499
+
"alpha_us": 23713,
500
+
"norm_us": 10474,
501
+
"traversals": 4002,
502
+
"max_depth": 1000,
503
+
"mem_delta_bytes": 86048
504
+
},
505
+
"chain-large": {
506
+
"alpha_us": 39877,
507
+
"norm_us": 19771,
508
+
"traversals": 2002,
509
+
"max_depth": 1000,
510
+
"mem_delta_bytes": 40992
511
+
},
512
+
"leaves-small-b": {
513
+
"alpha_us": 536,
514
+
"norm_us": 270,
515
+
"traversals": 5554,
516
+
"max_depth": 120,
517
+
"mem_delta_bytes": 20512
518
+
},
519
+
"leaves-medium-a": {
520
+
"alpha_us": 10362,
521
+
"norm_us": 5878,
522
+
"traversals": 94379,
523
+
"max_depth": 500,
524
+
"mem_delta_bytes": 57376
525
+
},
526
+
"leaves-large-a": {
527
+
"alpha_us": 177485,
528
+
"norm_us": 107127,
529
+
"traversals": 1502504,
530
+
"max_depth": 2000,
531
+
"mem_delta_bytes": 188448
532
+
},
533
+
"bigsubst-medium": {
534
+
"alpha_us": 1932,
535
+
"norm_us": 1039,
536
+
"traversals": 1042,
537
+
"max_depth": 270,
538
+
"mem_delta_bytes": 28704
539
+
},
540
+
"fv-small": {
541
+
"alpha_us": 58,
542
+
"norm_us": 27,
543
+
"traversals": 242,
544
+
"max_depth": 60,
545
+
"mem_delta_bytes": 20512
546
+
},
547
+
"leaves-large-b": {
548
+
"alpha_us": 237058,
549
+
"norm_us": 134837,
550
+
"traversals": 1502504,
551
+
"max_depth": 2000,
552
+
"mem_delta_bytes": 188448
553
+
},
554
+
"chain-medium": {
555
+
"alpha_us": 3255,
556
+
"norm_us": 1795,
557
+
"traversals": 502,
558
+
"max_depth": 250,
559
+
"mem_delta_bytes": 20512
560
+
},
561
+
"allbinders-small-b": {
562
+
"alpha_us": 189,
563
+
"norm_us": 94,
564
+
"traversals": 122,
565
+
"max_depth": 60,
566
+
"mem_delta_bytes": 20512
567
+
},
568
+
"leaves-small-a": {
569
+
"alpha_us": 545,
570
+
"norm_us": 289,
571
+
"traversals": 5554,
572
+
"max_depth": 120,
573
+
"mem_delta_bytes": 20512
574
+
},
575
+
"fv-medium": {
576
+
"alpha_us": 1143,
577
+
"norm_us": 622,
578
+
"traversals": 1002,
579
+
"max_depth": 250,
580
+
"mem_delta_bytes": 20512
581
+
},
582
+
"apps-medium": {
583
+
"alpha_us": 912,
584
+
"norm_us": 421,
585
+
"traversals": 1002,
586
+
"max_depth": 250,
587
+
"mem_delta_bytes": 20512
588
+
},
589
+
"allbinders-medium-a": {
590
+
"alpha_us": 3413,
591
+
"norm_us": 1354,
592
+
"traversals": 502,
593
+
"max_depth": 250,
594
+
"mem_delta_bytes": 20512
595
+
},
596
+
"shadow-medium": {
597
+
"alpha_us": 3027,
598
+
"norm_us": 1354,
599
+
"traversals": 502,
600
+
"max_depth": 250,
601
+
"mem_delta_bytes": 20512
602
+
},
603
+
"fv-large": {
604
+
"alpha_us": 22761,
605
+
"norm_us": 10327,
606
+
"traversals": 4002,
607
+
"max_depth": 1000,
608
+
"mem_delta_bytes": 86048
609
+
},
610
+
"shift-medium": {
611
+
"alpha_us": 815,
612
+
"norm_us": 393,
613
+
"traversals": 102,
614
+
"max_depth": 50,
615
+
"mem_delta_bytes": 20512
616
+
},
617
+
"leaves-medium-b": {
618
+
"alpha_us": 12151,
619
+
"norm_us": 6571,
620
+
"traversals": 94379,
621
+
"max_depth": 500,
622
+
"mem_delta_bytes": 57376
623
+
},
624
+
"chain-small": {
625
+
"alpha_us": 265,
626
+
"norm_us": 80,
627
+
"traversals": 122,
628
+
"max_depth": 60,
629
+
"mem_delta_bytes": 20512
630
+
},
631
+
"allbinders-large-b": {
632
+
"alpha_us": 40879,
633
+
"norm_us": 22422,
634
+
"traversals": 2002,
635
+
"max_depth": 1000,
636
+
"mem_delta_bytes": 40992
637
+
}
638
+
},
639
+
"subst": {
640
+
"apps-small": {
641
+
"alpha_us": 130,
642
+
"norm_us": 7,
643
+
"traversals": 242,
644
+
"max_depth": 60,
645
+
"mem_delta_bytes": 20512
646
+
},
647
+
"bigsubst-large": {
648
+
"alpha_us": 21639,
649
+
"norm_us": 2008,
650
+
"traversals": 6065,
651
+
"max_depth": 1020,
652
+
"mem_delta_bytes": 286752
653
+
},
654
+
"allbinders-large-a": {
655
+
"alpha_us": 36450,
656
+
"norm_us": 214,
657
+
"traversals": 2002,
658
+
"max_depth": 1000,
659
+
"mem_delta_bytes": 127008
660
+
},
661
+
"shadow-small": {
662
+
"alpha_us": 115,
663
+
"norm_us": 5,
664
+
"traversals": 122,
665
+
"max_depth": 60,
666
+
"mem_delta_bytes": 20512
667
+
},
668
+
"allbinders-medium-b": {
669
+
"alpha_us": 4194,
670
+
"norm_us": 37,
671
+
"traversals": 502,
672
+
"max_depth": 250,
673
+
"mem_delta_bytes": 28704
674
+
},
675
+
"shadow-large": {
676
+
"alpha_us": 12594,
677
+
"norm_us": 180,
678
+
"traversals": 2002,
679
+
"max_depth": 1000,
680
+
"mem_delta_bytes": 127008
681
+
},
682
+
"shift-large": {
683
+
"alpha_us": 1684,
684
+
"norm_us": 506,
685
+
"traversals": 603,
686
+
"max_depth": 240,
687
+
"mem_delta_bytes": 28704
688
+
},
689
+
"shift-small": {
690
+
"alpha_us": 74,
691
+
"norm_us": 41,
692
+
"traversals": 63,
693
+
"max_depth": 24,
694
+
"mem_delta_bytes": 20512
695
+
},
696
+
"bigsubst-small": {
697
+
"alpha_us": 344,
698
+
"norm_us": 93,
699
+
"traversals": 425,
700
+
"max_depth": 80,
701
+
"mem_delta_bytes": 20512
702
+
},
703
+
"allbinders-small-a": {
704
+
"alpha_us": 314,
705
+
"norm_us": 7,
706
+
"traversals": 122,
707
+
"max_depth": 60,
708
+
"mem_delta_bytes": 20512
709
+
},
710
+
"apps-large": {
711
+
"alpha_us": 18811,
712
+
"norm_us": 170,
713
+
"traversals": 4002,
714
+
"max_depth": 1000,
715
+
"mem_delta_bytes": 188448
716
+
},
717
+
"chain-large": {
718
+
"alpha_us": 14905,
719
+
"norm_us": 204,
720
+
"traversals": 2002,
721
+
"max_depth": 1000,
722
+
"mem_delta_bytes": 127008
723
+
},
724
+
"leaves-small-b": {
725
+
"alpha_us": 75,
726
+
"norm_us": 32,
727
+
"traversals": 189,
728
+
"max_depth": 120,
729
+
"mem_delta_bytes": 20512
730
+
},
731
+
"leaves-medium-a": {
732
+
"alpha_us": 293,
733
+
"norm_us": 158,
734
+
"traversals": 759,
735
+
"max_depth": 500,
736
+
"mem_delta_bytes": 28704
737
+
},
738
+
"leaves-large-a": {
739
+
"alpha_us": 2307,
740
+
"norm_us": 758,
741
+
"traversals": 3009,
742
+
"max_depth": 2000,
743
+
"mem_delta_bytes": 127008
744
+
},
745
+
"bigsubst-medium": {
746
+
"alpha_us": 2550,
747
+
"norm_us": 440,
748
+
"traversals": 1565,
749
+
"max_depth": 270,
750
+
"mem_delta_bytes": 57376
751
+
},
752
+
"fv-small": {
753
+
"alpha_us": 93,
754
+
"norm_us": 21,
755
+
"traversals": 242,
756
+
"max_depth": 60,
757
+
"mem_delta_bytes": 20512
758
+
},
759
+
"leaves-large-b": {
760
+
"alpha_us": 3229,
761
+
"norm_us": 1089,
762
+
"traversals": 3009,
763
+
"max_depth": 2000,
764
+
"mem_delta_bytes": 127008
765
+
},
766
+
"chain-medium": {
767
+
"alpha_us": 4177,
768
+
"norm_us": 65,
769
+
"traversals": 502,
770
+
"max_depth": 250,
771
+
"mem_delta_bytes": 28704
772
+
},
773
+
"allbinders-small-b": {
774
+
"alpha_us": 909,
775
+
"norm_us": 14,
776
+
"traversals": 122,
777
+
"max_depth": 60,
778
+
"mem_delta_bytes": 20512
779
+
},
780
+
"leaves-small-a": {
781
+
"alpha_us": 137,
782
+
"norm_us": 86,
783
+
"traversals": 189,
784
+
"max_depth": 120,
785
+
"mem_delta_bytes": 20512
786
+
},
787
+
"fv-medium": {
788
+
"alpha_us": 2312,
789
+
"norm_us": 75,
790
+
"traversals": 1002,
791
+
"max_depth": 250,
792
+
"mem_delta_bytes": 57376
793
+
},
794
+
"apps-medium": {
795
+
"alpha_us": 2159,
796
+
"norm_us": 80,
797
+
"traversals": 1002,
798
+
"max_depth": 250,
799
+
"mem_delta_bytes": 57376
800
+
},
801
+
"allbinders-medium-a": {
802
+
"alpha_us": 6288,
803
+
"norm_us": 62,
804
+
"traversals": 502,
805
+
"max_depth": 250,
806
+
"mem_delta_bytes": 28704
807
+
},
808
+
"shadow-medium": {
809
+
"alpha_us": 1478,
810
+
"norm_us": 34,
811
+
"traversals": 502,
812
+
"max_depth": 250,
813
+
"mem_delta_bytes": 28704
814
+
},
815
+
"fv-large": {
816
+
"alpha_us": 35673,
817
+
"norm_us": 444,
818
+
"traversals": 4002,
819
+
"max_depth": 1000,
820
+
"mem_delta_bytes": 188448
821
+
},
822
+
"shift-medium": {
823
+
"alpha_us": 897,
824
+
"norm_us": 282,
825
+
"traversals": 253,
826
+
"max_depth": 100,
827
+
"mem_delta_bytes": 20512
828
+
},
829
+
"leaves-medium-b": {
830
+
"alpha_us": 760,
831
+
"norm_us": 303,
832
+
"traversals": 759,
833
+
"max_depth": 500,
834
+
"mem_delta_bytes": 28704
835
+
},
836
+
"chain-small": {
837
+
"alpha_us": 905,
838
+
"norm_us": 67,
839
+
"traversals": 122,
840
+
"max_depth": 60,
841
+
"mem_delta_bytes": 20512
842
+
},
843
+
"allbinders-large-b": {
844
+
"alpha_us": 92922,
845
+
"norm_us": 173,
846
+
"traversals": 2002,
847
+
"max_depth": 1000,
848
+
"mem_delta_bytes": 127008
849
+
}
850
+
}
851
+
}
852
+
}
+222
nim/src/ego.nim
+222
nim/src/ego.nim
···
1
+
import std/[algorithm, os, json, monotimes, strutils]
2
+
import ego/named, ego/debruijn, ego/locally_nameless, ego/explicit_subst,
3
+
ego/syntax, ego/jsonio
4
+
5
+
type Rep = enum rNamed, rDebruijn, rLn, rSubst
6
+
7
+
const repNames = ["named", "debruijn", "ln", "subst"]
8
+
9
+
proc repsOf(s: string): seq[Rep] =
10
+
case s
11
+
of "named": @[rNamed]
12
+
of "debruijn": @[rDebruijn]
13
+
of "ln": @[rLn]
14
+
of "subst": @[rSubst]
15
+
of "all": @[rNamed, rDebruijn, rLn, rSubst]
16
+
else: raise newException(ValueError, "unknown representation: " & s)
17
+
18
+
proc checkWith(rep: Rep, t1, t2: Named): bool =
19
+
case rep
20
+
of rNamed: named.alphaEquivalent(t1, t2)
21
+
of rDebruijn:
22
+
debruijn.alphaEquivalent(debruijn.convertFromNamed(t1),
23
+
debruijn.convertFromNamed(t2))
24
+
of rLn:
25
+
locally_nameless.alphaEquivalent(locally_nameless.convertFromNamed(t1),
26
+
locally_nameless.convertFromNamed(t2))
27
+
of rSubst:
28
+
explicit_subst.alphaEquivalent(explicit_subst.convertFromNamed(t1),
29
+
explicit_subst.convertFromNamed(t2))
30
+
31
+
proc cmdCheck(args: seq[string], repSel: string): int =
32
+
let r1 = parseResult(args[0])
33
+
let r2 = parseResult(args[1])
34
+
if not r1.ok:
35
+
echo "PARSE-ERROR: ", r1.err
36
+
return 2
37
+
if not r2.ok:
38
+
echo "PARSE-ERROR: ", r2.err
39
+
return 2
40
+
for rep in repsOf(repSel):
41
+
let eq = checkWith(rep, r1.term, r2.term)
42
+
echo repNames[rep.ord], ": ", (if eq: "EQUIV" else: "NOT-EQUIV")
43
+
0
44
+
45
+
proc cmdCorpus(path: string): int =
46
+
let entries = loadCorpus(path)
47
+
var failures = 0
48
+
let reps = [rNamed, rDebruijn, rLn, rSubst]
49
+
for e in entries:
50
+
var results: seq[(Rep, bool)]
51
+
for rep in reps:
52
+
results.add((rep, checkWith(rep, e.t1, e.t2)))
53
+
for (rep, got) in results:
54
+
if e.expected != 2 and got != (e.expected == 1):
55
+
inc failures
56
+
echo "FAIL ", e.name, " [", repNames[rep.ord], "]: expected ",
57
+
(if e.expected == 1: "EQUIV" else: "NOT-EQUIV"), " got ",
58
+
(if got: "EQUIV" else: "NOT-EQUIV")
59
+
let first = results[0][1]
60
+
var agree = true
61
+
for (_, g) in results:
62
+
if g != first: agree = false
63
+
if not agree:
64
+
inc failures
65
+
var parts: seq[string]
66
+
for (rep, g) in results:
67
+
parts.add(repNames[rep.ord] & "=" & $g)
68
+
echo "DISAGREE ", e.name, ": ", parts.join(", ")
69
+
if failures > 0:
70
+
echo failures, " failure(s)"
71
+
1
72
+
else:
73
+
echo "corpus: ", entries.len, " entries, 0 failures"
74
+
0
75
+
76
+
proc nowUs(): int64 =
77
+
let m = getMonoTime()
78
+
m.ticks div 1000
79
+
80
+
proc median(xs: var seq[int64]): int64 =
81
+
xs.sort()
82
+
xs[xs.len div 2]
83
+
84
+
proc benchRep(rep: Rep, t1, t2: Named, iters: int): JsonNode =
85
+
var alphaTs: seq[int64]
86
+
var normTs: seq[int64]
87
+
var trav = 0
88
+
var depth = 0
89
+
var memBefore = getOccupiedMem()
90
+
for _ in 0 ..< iters:
91
+
GC_fullCollect()
92
+
memBefore = getOccupiedMem()
93
+
let t0 = nowUs()
94
+
case rep
95
+
of rNamed:
96
+
let (r, c) = named.alphaEquivalentCounted(t1, t2)
97
+
alphaTs.add(nowUs() - t0)
98
+
trav = max(trav, c.traversals)
99
+
depth = max(depth, c.maxDepth)
100
+
if r: discard
101
+
of rDebruijn:
102
+
let (r, c) = debruijn.alphaEquivalentCounted(
103
+
debruijn.convertFromNamed(t1), debruijn.convertFromNamed(t2))
104
+
alphaTs.add(nowUs() - t0)
105
+
trav = max(trav, c.traversals)
106
+
depth = max(depth, c.maxDepth)
107
+
if r: discard
108
+
of rLn:
109
+
let (r, c) = locally_nameless.alphaEquivalentCounted(
110
+
locally_nameless.convertFromNamed(t1),
111
+
locally_nameless.convertFromNamed(t2))
112
+
alphaTs.add(nowUs() - t0)
113
+
trav = max(trav, c.traversals)
114
+
depth = max(depth, c.maxDepth)
115
+
if r: discard
116
+
of rSubst:
117
+
let (r, c) = explicit_subst.alphaEquivalentCounted(
118
+
explicit_subst.convertFromNamed(t1),
119
+
explicit_subst.convertFromNamed(t2))
120
+
alphaTs.add(nowUs() - t0)
121
+
trav = max(trav, c.traversals)
122
+
depth = max(depth, c.maxDepth)
123
+
if r: discard
124
+
let t1n = nowUs()
125
+
case rep
126
+
of rNamed:
127
+
let (_, c) = named.normaliseCounted(t1)
128
+
normTs.add(nowUs() - t1n)
129
+
trav = max(trav, c.traversals)
130
+
depth = max(depth, c.maxDepth)
131
+
of rDebruijn:
132
+
let (_, c) = debruijn.normaliseCounted(debruijn.convertFromNamed(t1))
133
+
normTs.add(nowUs() - t1n)
134
+
trav = max(trav, c.traversals)
135
+
depth = max(depth, c.maxDepth)
136
+
of rLn:
137
+
let (_, c) = locally_nameless.normaliseCounted(
138
+
locally_nameless.convertFromNamed(t1))
139
+
normTs.add(nowUs() - t1n)
140
+
trav = max(trav, c.traversals)
141
+
depth = max(depth, c.maxDepth)
142
+
of rSubst:
143
+
let (_, c) = explicit_subst.normaliseCounted(
144
+
explicit_subst.convertFromNamed(t1))
145
+
normTs.add(nowUs() - t1n)
146
+
trav = max(trav, c.traversals)
147
+
depth = max(depth, c.maxDepth)
148
+
let memAfter = getOccupiedMem()
149
+
%* {"alpha_us": median(alphaTs), "norm_us": median(normTs),
150
+
"traversals": trav, "max_depth": depth,
151
+
"mem_delta_bytes": memAfter - memBefore}
152
+
153
+
proc cmdBench(path: string, iters: int, outPath: string): int =
154
+
let benches = loadBench(path)
155
+
var repJson = newJObject()
156
+
let reps = [rNamed, rDebruijn, rLn, rSubst]
157
+
for rep in reps:
158
+
var benchJson = newJObject()
159
+
for (name, t) in benches:
160
+
var other = t
161
+
if name.endsWith("-a"):
162
+
let base = name[0 ..< name.len - 2]
163
+
for (n2, t2) in benches:
164
+
if n2 == base & "-b": other = t2
165
+
benchJson[name] = benchRep(rep, t, other, iters)
166
+
repJson[repNames[rep.ord]] = benchJson
167
+
let outDoc = %* {"nim": repJson}
168
+
writeFile(outPath, outDoc.pretty)
169
+
echo "bench: wrote ", outPath
170
+
0
171
+
172
+
proc main(): int =
173
+
let args = commandLineParams()
174
+
if args.len < 1:
175
+
stderr.writeLine("usage: ego check <t1> <t2> [-r rep] | ego corpus <file> | ego bench <file> [--iters N] [--out file]")
176
+
return 2
177
+
case args[0]
178
+
of "check":
179
+
var rep = "named"
180
+
var terms: seq[string]
181
+
var i = 1
182
+
while i < args.len:
183
+
if args[i] == "-r":
184
+
inc i
185
+
rep = args[i]
186
+
else:
187
+
terms.add(args[i])
188
+
inc i
189
+
if terms.len != 2:
190
+
stderr.writeLine("check requires exactly two terms")
191
+
return 2
192
+
cmdCheck(terms, rep)
193
+
of "corpus":
194
+
if args.len < 2:
195
+
stderr.writeLine("corpus requires a file")
196
+
return 2
197
+
cmdCorpus(args[1])
198
+
of "bench":
199
+
var iters = 5
200
+
var outPath = "results.json"
201
+
var file = ""
202
+
var i = 1
203
+
while i < args.len:
204
+
if args[i] == "--iters":
205
+
inc i
206
+
iters = parseInt(args[i])
207
+
elif args[i] == "--out":
208
+
inc i
209
+
outPath = args[i]
210
+
else:
211
+
file = args[i]
212
+
inc i
213
+
if file == "":
214
+
stderr.writeLine("bench requires a file")
215
+
return 2
216
+
cmdBench(file, iters, outPath)
217
+
else:
218
+
stderr.writeLine("unknown command")
219
+
2
220
+
221
+
222
+
quit(main())
+186
nim/src/ego/debruijn.nim
+186
nim/src/ego/debruijn.nim
···
1
+
import std/sets
2
+
import named
3
+
4
+
type
5
+
DbKind* = enum dkVar, dkFree, dkLam, dkApp
6
+
DeBruijn* = ref DeBruijnObj
7
+
DeBruijnObj = object
8
+
case kind: DbKind
9
+
of dkVar:
10
+
idx: int
11
+
of dkFree:
12
+
name: string
13
+
of dkLam:
14
+
body: DeBruijn
15
+
of dkApp:
16
+
fun, arg: DeBruijn
17
+
18
+
proc dVar*(i: int): DeBruijn = (ref DeBruijnObj)(kind: dkVar, idx: i)
19
+
proc dFree*(n: string): DeBruijn = (ref DeBruijnObj)(kind: dkFree, name: n)
20
+
proc dLam*(b: DeBruijn): DeBruijn = (ref DeBruijnObj)(kind: dkLam, body: b)
21
+
proc dApp*(f, a: DeBruijn): DeBruijn = (ref DeBruijnObj)(kind: dkApp, fun: f, arg: a)
22
+
23
+
proc kind*(t: DeBruijn): DbKind = t.kind
24
+
proc idx*(t: DeBruijn): int = t.idx
25
+
proc name*(t: DeBruijn): string = t.name
26
+
proc body*(t: DeBruijn): DeBruijn = t.body
27
+
proc fun*(t: DeBruijn): DeBruijn = t.fun
28
+
proc arg*(t: DeBruijn): DeBruijn = t.arg
29
+
30
+
type UnboundIndex* = object of CatchableError
31
+
32
+
type Ctx* = object
33
+
traversals*: int
34
+
maxDepth*: int
35
+
36
+
proc tick*(c: var Ctx, depth: int) {.inline.} =
37
+
inc c.traversals
38
+
if depth > c.maxDepth: c.maxDepth = depth
39
+
40
+
proc freeVars*(t: DeBruijn): HashSet[string] =
41
+
case t.kind
42
+
of dkVar: discard
43
+
of dkFree: result.incl(t.name)
44
+
of dkLam: result = freeVars(t.body)
45
+
of dkApp:
46
+
result = freeVars(t.fun)
47
+
result = result + freeVars(t.arg)
48
+
49
+
proc eqDb(a, b: DeBruijn): bool =
50
+
if a.kind != b.kind: return false
51
+
case a.kind
52
+
of dkVar: a.idx == b.idx
53
+
of dkFree: a.name == b.name
54
+
of dkLam: eqDb(a.body, b.body)
55
+
of dkApp: eqDb(a.fun, b.fun) and eqDb(a.arg, b.arg)
56
+
57
+
proc shift(t: DeBruijn, cutoff, amount: int): DeBruijn =
58
+
case t.kind
59
+
of dkVar: (if t.idx >= cutoff: dVar(t.idx + amount) else: t)
60
+
of dkFree: t
61
+
of dkLam: dLam(shift(t.body, cutoff + 1, amount))
62
+
of dkApp: dApp(shift(t.fun, cutoff, amount), shift(t.arg, cutoff, amount))
63
+
64
+
proc subst(t: DeBruijn, j: int, s: DeBruijn): DeBruijn =
65
+
case t.kind
66
+
of dkVar:
67
+
if t.idx == j: s
68
+
elif t.idx > j: dVar(t.idx - 1)
69
+
else: t
70
+
of dkFree: t
71
+
of dkLam: dLam(subst(t.body, j + 1, shift(s, 0, 1)))
72
+
of dkApp: dApp(subst(t.fun, j, s), subst(t.arg, j, s))
73
+
74
+
proc substitute*(t: DeBruijn, j: int, s: DeBruijn): DeBruijn = subst(t, j, s)
75
+
76
+
proc step(t: DeBruijn): DeBruijn =
77
+
case t.kind
78
+
of dkApp:
79
+
if t.fun.kind == dkLam:
80
+
return subst(t.fun.body, 0, t.arg)
81
+
let f = step(t.fun)
82
+
if not eqDb(f, t.fun): return dApp(f, t.arg)
83
+
let a = step(t.arg)
84
+
if not eqDb(a, t.arg): return dApp(t.fun, a)
85
+
t
86
+
of dkLam:
87
+
let b = step(t.body)
88
+
if not eqDb(b, t.body): dLam(b) else: t
89
+
else: t
90
+
91
+
const stepLimit = 100000
92
+
93
+
proc normalise*(t: DeBruijn): DeBruijn =
94
+
result = t
95
+
var n = 0
96
+
while n < stepLimit:
97
+
let t2 = step(result)
98
+
if eqDb(t2, result): break
99
+
result = t2
100
+
inc n
101
+
102
+
proc convertFromNamed*(t: named.Named): DeBruijn =
103
+
proc go(t: named.Named, env: seq[(string, int)]): DeBruijn =
104
+
case t.kind
105
+
of named.nkVar:
106
+
for (v, i) in env:
107
+
if v == t.name: return dVar(i)
108
+
dFree(t.name)
109
+
of named.nkLam:
110
+
var env2 = @[(t.param, 0)]
111
+
for (v, i) in env: env2.add((v, i + 1))
112
+
dLam(go(t.body, env2))
113
+
of named.nkApp: dApp(go(t.fun, env), go(t.arg, env))
114
+
of named.nkSubst:
115
+
go(named.substitute(t.svar, t.repl, t.sbody), env)
116
+
go(t, @[])
117
+
118
+
proc convertToNamed*(t: DeBruijn): named.Named =
119
+
let fv = freeVars(t)
120
+
proc go(t: DeBruijn, env: seq[string]): named.Named =
121
+
case t.kind
122
+
of dkVar:
123
+
if t.idx >= env.len:
124
+
raise newException(UnboundIndex, "unbound index " & $t.idx)
125
+
named.nVar(env[t.idx])
126
+
of dkFree: named.nVar(t.name)
127
+
of dkLam:
128
+
var avoid = fv
129
+
for x in env: avoid.incl(x)
130
+
var base = "v"
131
+
var cand = base
132
+
var i = 0
133
+
while cand in avoid:
134
+
cand = base & $i
135
+
inc i
136
+
named.nLam(cand, go(t.body, @[cand] & env))
137
+
of dkApp: named.nApp(go(t.fun, env), go(t.arg, env))
138
+
go(t, @[])
139
+
140
+
proc wellScoped*(t: DeBruijn, depth: int = 0): bool =
141
+
case t.kind
142
+
of dkVar: t.idx < depth
143
+
of dkFree: true
144
+
of dkLam: wellScoped(t.body, depth + 1)
145
+
of dkApp: wellScoped(t.fun, depth) and wellScoped(t.arg, depth)
146
+
147
+
proc alphaEquivalent*(a, b: DeBruijn): bool =
148
+
eqDb(normalise(a), normalise(b))
149
+
150
+
proc alphaEquivalentCounted*(a, b: DeBruijn): tuple[r: bool, c: Ctx] =
151
+
var c: Ctx
152
+
proc go(a, b: DeBruijn, d: int): bool =
153
+
c.tick(d)
154
+
if a.kind != b.kind: return false
155
+
case a.kind
156
+
of dkVar: a.idx == b.idx
157
+
of dkFree: a.name == b.name
158
+
of dkLam: go(a.body, b.body, d + 1)
159
+
of dkApp: go(a.fun, b.fun, d + 1) and go(a.arg, b.arg, d + 1)
160
+
(go(normalise(a), normalise(b), 0), c)
161
+
162
+
proc normaliseCounted*(t: DeBruijn): tuple[r: DeBruijn, c: Ctx] =
163
+
var c: Ctx
164
+
proc walk(t: DeBruijn, d: int) =
165
+
c.tick(d)
166
+
case t.kind
167
+
of dkVar, dkFree: discard
168
+
of dkLam: walk(t.body, d + 1)
169
+
of dkApp: walk(t.fun, d + 1); walk(t.arg, d + 1)
170
+
var r = t
171
+
walk(r, 0)
172
+
var n = 0
173
+
while n < stepLimit:
174
+
let t2 = step(r)
175
+
walk(t2, 0)
176
+
if eqDb(t2, r): break
177
+
r = t2
178
+
inc n
179
+
(r, c)
180
+
181
+
proc prettyPrint*(t: DeBruijn): string =
182
+
case t.kind
183
+
of dkVar: "#" & $t.idx
184
+
of dkFree: t.name
185
+
of dkLam: "\\. " & prettyPrint(t.body)
186
+
of dkApp: prettyPrint(t.fun) & " " & prettyPrint(t.arg)
+227
nim/src/ego/explicit_subst.nim
+227
nim/src/ego/explicit_subst.nim
···
1
+
import std/[sets, tables]
2
+
import named
3
+
4
+
type
5
+
EsKind* = enum ekVar, ekLam, ekApp, ekSubst
6
+
ExplicitSubst* = ref EsObj
7
+
EsObj = object
8
+
case kind: EsKind
9
+
of ekVar:
10
+
name: string
11
+
of ekLam:
12
+
param: string
13
+
body: ExplicitSubst
14
+
of ekApp:
15
+
fun, arg: ExplicitSubst
16
+
of ekSubst:
17
+
svar: string
18
+
repl, sbody: ExplicitSubst
19
+
20
+
proc eVar*(n: string): ExplicitSubst = (ref EsObj)(kind: ekVar, name: n)
21
+
proc eLam*(p: string, b: ExplicitSubst): ExplicitSubst =
22
+
(ref EsObj)(kind: ekLam, param: p, body: b)
23
+
proc eApp*(f, a: ExplicitSubst): ExplicitSubst =
24
+
(ref EsObj)(kind: ekApp, fun: f, arg: a)
25
+
proc eSubst*(x: string, s, b: ExplicitSubst): ExplicitSubst =
26
+
(ref EsObj)(kind: ekSubst, svar: x, repl: s, sbody: b)
27
+
28
+
proc kind*(t: ExplicitSubst): EsKind = t.kind
29
+
proc name*(t: ExplicitSubst): string = t.name
30
+
proc param*(t: ExplicitSubst): string = t.param
31
+
proc body*(t: ExplicitSubst): ExplicitSubst = t.body
32
+
proc fun*(t: ExplicitSubst): ExplicitSubst = t.fun
33
+
proc arg*(t: ExplicitSubst): ExplicitSubst = t.arg
34
+
proc svar*(t: ExplicitSubst): string = t.svar
35
+
proc repl*(t: ExplicitSubst): ExplicitSubst = t.repl
36
+
proc sbody*(t: ExplicitSubst): ExplicitSubst = t.sbody
37
+
38
+
type Ctx* = object
39
+
traversals*: int
40
+
maxDepth*: int
41
+
42
+
proc tick*(c: var Ctx, depth: int) {.inline.} =
43
+
inc c.traversals
44
+
if depth > c.maxDepth: c.maxDepth = depth
45
+
46
+
proc freeVars*(t: ExplicitSubst): HashSet[string] =
47
+
case t.kind
48
+
of ekVar: result.incl(t.name)
49
+
of ekLam:
50
+
result = freeVars(t.body)
51
+
result.excl(t.param)
52
+
of ekApp:
53
+
result = freeVars(t.fun)
54
+
result = result + freeVars(t.arg)
55
+
of ekSubst:
56
+
var b = freeVars(t.sbody)
57
+
let used = t.svar in b
58
+
b.excl(t.svar)
59
+
result = b
60
+
if used:
61
+
result = result + freeVars(t.repl)
62
+
63
+
proc fresh(avoid: HashSet[string], base: string): string =
64
+
if base notin avoid: return base
65
+
var i = 0
66
+
while true:
67
+
let cand = base & $i
68
+
if cand notin avoid: return cand
69
+
inc i
70
+
71
+
proc rename(t: ExplicitSubst, old, nw: string): ExplicitSubst =
72
+
case t.kind
73
+
of ekVar: (if t.name == old: eVar(nw) else: t)
74
+
of ekApp: eApp(rename(t.fun, old, nw), rename(t.arg, old, nw))
75
+
of ekLam:
76
+
if t.param == old: t
77
+
else: eLam(t.param, rename(t.body, old, nw))
78
+
of ekSubst:
79
+
if t.svar == old: eSubst(t.svar, rename(t.repl, old, nw), t.sbody)
80
+
else: eSubst(t.svar, rename(t.repl, old, nw), rename(t.sbody, old, nw))
81
+
82
+
proc eqEs(a, b: ExplicitSubst): bool =
83
+
if a.kind != b.kind: return false
84
+
case a.kind
85
+
of ekVar: a.name == b.name
86
+
of ekLam: a.param == b.param and eqEs(a.body, b.body)
87
+
of ekApp: eqEs(a.fun, b.fun) and eqEs(a.arg, b.arg)
88
+
of ekSubst:
89
+
a.svar == b.svar and eqEs(a.repl, b.repl) and eqEs(a.sbody, b.sbody)
90
+
91
+
proc pushSubst(x: string, s, body: ExplicitSubst): ExplicitSubst =
92
+
let fvS = freeVars(s)
93
+
proc go(t: ExplicitSubst): ExplicitSubst =
94
+
case t.kind
95
+
of ekVar: (if t.name == x: s else: t)
96
+
of ekApp: eApp(go(t.fun), go(t.arg))
97
+
of ekLam:
98
+
if t.param == x: t
99
+
elif t.param notin fvS: eLam(t.param, go(t.body))
100
+
else:
101
+
let avoid = fvS + freeVars(t.body)
102
+
let y = fresh(avoid, t.param)
103
+
eLam(y, go(rename(t.body, t.param, y)))
104
+
of ekSubst:
105
+
if t.svar == x: eSubst(t.svar, go(t.repl), t.sbody)
106
+
elif t.svar notin fvS: eSubst(t.svar, go(t.repl), go(t.sbody))
107
+
else:
108
+
let avoid = fvS + freeVars(t.sbody)
109
+
let y = fresh(avoid, t.svar)
110
+
eSubst(y, go(t.repl), go(rename(t.sbody, t.svar, y)))
111
+
go(body)
112
+
113
+
const stepLimit = 100000
114
+
115
+
proc reduceEs(t: ExplicitSubst): ExplicitSubst =
116
+
case t.kind
117
+
of ekVar: t
118
+
of ekLam: eLam(t.param, reduceEs(t.body))
119
+
of ekApp:
120
+
let f = reduceEs(t.fun)
121
+
let a = reduceEs(t.arg)
122
+
if f.kind == ekLam: reduceEs(pushSubst(f.param, a, f.body))
123
+
else: eApp(f, a)
124
+
of ekSubst: reduceEs(pushSubst(t.svar, reduceEs(t.repl), t.sbody))
125
+
126
+
proc normalise*(t: ExplicitSubst): ExplicitSubst =
127
+
result = t
128
+
var n = 0
129
+
while n < stepLimit:
130
+
let t2 = reduceEs(result)
131
+
if eqEs(t2, result): break
132
+
result = t2
133
+
inc n
134
+
135
+
proc substitute*(x: string, s, body: ExplicitSubst): ExplicitSubst =
136
+
eSubst(x, s, body)
137
+
138
+
proc ofNamed*(t: named.Named): ExplicitSubst =
139
+
case t.kind
140
+
of named.nkVar: eVar(t.name)
141
+
of named.nkLam: eLam(t.param, ofNamed(t.body))
142
+
of named.nkApp: eApp(ofNamed(t.fun), ofNamed(t.arg))
143
+
of named.nkSubst: eSubst(t.svar, ofNamed(t.repl), ofNamed(t.sbody))
144
+
145
+
proc toNamed*(t: ExplicitSubst): named.Named =
146
+
case t.kind
147
+
of ekVar: named.nVar(t.name)
148
+
of ekLam: named.nLam(t.param, toNamed(t.body))
149
+
of ekApp: named.nApp(toNamed(t.fun), toNamed(t.arg))
150
+
of ekSubst: named.nSubst(t.svar, toNamed(t.repl), toNamed(t.sbody))
151
+
152
+
proc convertFromNamed*(t: named.Named): ExplicitSubst = ofNamed(t)
153
+
proc convertToNamed*(t: ExplicitSubst): named.Named = toNamed(normalise(t))
154
+
155
+
proc alphaEquivalent*(a, b: ExplicitSubst): bool =
156
+
named.alphaEquivalent(toNamed(normalise(a)), toNamed(normalise(b)))
157
+
158
+
proc addPair(e: Table[string, int], k: string, v: int): Table[string, int] =
159
+
result = e
160
+
result[k] = v
161
+
162
+
proc alphaEquivalentSusp*(a, b: ExplicitSubst): bool =
163
+
proc go(a, b: ExplicitSubst, ea, eb: Table[string, int], d: int): bool =
164
+
case a.kind
165
+
of ekSubst:
166
+
if b.kind == ekSubst:
167
+
return go(a.repl, b.repl, ea, eb, d) and
168
+
go(a.sbody, b.sbody, addPair(ea, a.svar, d), addPair(eb, b.svar, d), d + 1)
169
+
return go(normalise(a), b, ea, eb, d)
170
+
else:
171
+
if b.kind == ekSubst:
172
+
return go(a, normalise(b), ea, eb, d)
173
+
if a.kind != b.kind: return false
174
+
case a.kind
175
+
of ekVar:
176
+
let ia = ea.getOrDefault(a.name, -1)
177
+
let ib = eb.getOrDefault(b.name, -1)
178
+
if ia >= 0 or ib >= 0: ia == ib
179
+
else: a.name == b.name
180
+
of ekLam:
181
+
go(a.body, b.body, addPair(ea, a.param, d), addPair(eb, b.param, d), d + 1)
182
+
of ekApp:
183
+
go(a.fun, b.fun, ea, eb, d + 1) and go(a.arg, b.arg, ea, eb, d + 1)
184
+
of ekSubst: false
185
+
go(a, b, initTable[string, int](), initTable[string, int](), 0)
186
+
187
+
proc alphaEquivalentCounted*(a, b: ExplicitSubst): tuple[r: bool, c: Ctx] =
188
+
var c: Ctx
189
+
proc walk(t: ExplicitSubst, d: int) =
190
+
c.tick(d)
191
+
case t.kind
192
+
of ekVar: discard
193
+
of ekLam: walk(t.body, d + 1)
194
+
of ekApp: walk(t.fun, d + 1); walk(t.arg, d + 1)
195
+
of ekSubst: walk(t.repl, d + 1); walk(t.sbody, d + 1)
196
+
let na = normalise(a)
197
+
let nb = normalise(b)
198
+
walk(na, 0)
199
+
walk(nb, 0)
200
+
(named.alphaEquivalent(toNamed(na), toNamed(nb)), c)
201
+
202
+
proc normaliseCounted*(t: ExplicitSubst): tuple[r: ExplicitSubst, c: Ctx] =
203
+
var c: Ctx
204
+
proc walk(t: ExplicitSubst, d: int) =
205
+
c.tick(d)
206
+
case t.kind
207
+
of ekVar: discard
208
+
of ekLam: walk(t.body, d + 1)
209
+
of ekApp: walk(t.fun, d + 1); walk(t.arg, d + 1)
210
+
of ekSubst: walk(t.repl, d + 1); walk(t.sbody, d + 1)
211
+
var r = t
212
+
walk(r, 0)
213
+
var n = 0
214
+
while n < stepLimit:
215
+
let t2 = reduceEs(r)
216
+
walk(t2, 0)
217
+
if eqEs(t2, r): break
218
+
r = t2
219
+
inc n
220
+
(r, c)
221
+
222
+
proc prettyPrint*(t: ExplicitSubst): string =
223
+
case t.kind
224
+
of ekVar: t.name
225
+
of ekLam: "\\" & t.param & ". " & prettyPrint(t.body)
226
+
of ekApp: prettyPrint(t.fun) & " " & prettyPrint(t.arg)
227
+
of ekSubst: "[" & t.svar & " := " & prettyPrint(t.repl) & "] " & prettyPrint(t.sbody)
+187
nim/src/ego/jsonio.nim
+187
nim/src/ego/jsonio.nim
···
1
+
import std/tables
2
+
import named
3
+
4
+
type
5
+
JKind = enum jkObject, jkArray, jkString, jkBool, jkNull
6
+
JNode = ref object
7
+
case kind: JKind
8
+
of jkObject:
9
+
fields: Table[string, JNode]
10
+
of jkArray:
11
+
elems: seq[JNode]
12
+
of jkString:
13
+
str: string
14
+
of jkBool:
15
+
b: bool
16
+
of jkNull:
17
+
discard
18
+
19
+
Parser = object
20
+
src: string
21
+
pos: int
22
+
23
+
proc fail(p: Parser, msg: string) =
24
+
raise newException(ValueError, msg & " at byte " & $p.pos)
25
+
26
+
proc skipWs(p: var Parser) =
27
+
while p.pos < p.src.len and p.src[p.pos] in {' ', '\n', '\r', '\t'}:
28
+
inc p.pos
29
+
30
+
proc expect(p: var Parser, ch: char) =
31
+
p.skipWs()
32
+
if p.pos >= p.src.len or p.src[p.pos] != ch:
33
+
p.fail("expected " & $ch)
34
+
inc p.pos
35
+
36
+
proc parseString(p: var Parser): string =
37
+
p.expect('"')
38
+
while p.pos < p.src.len:
39
+
let ch = p.src[p.pos]
40
+
inc p.pos
41
+
case ch
42
+
of '"':
43
+
return
44
+
of '\\':
45
+
if p.pos >= p.src.len:
46
+
p.fail("unterminated escape")
47
+
let e = p.src[p.pos]
48
+
inc p.pos
49
+
case e
50
+
of '"': result.add('"')
51
+
of '\\': result.add('\\')
52
+
of '/': result.add('/')
53
+
of 'b': result.add('\b')
54
+
of 'f': result.add('\f')
55
+
of 'n': result.add('\n')
56
+
of 'r': result.add('\r')
57
+
of 't': result.add('\t')
58
+
else: p.fail("unsupported escape")
59
+
else:
60
+
result.add(ch)
61
+
p.fail("unterminated string")
62
+
63
+
proc lit(p: var Parser, s: string, n: JNode): JNode =
64
+
if p.pos + s.len <= p.src.len and p.src[p.pos ..< p.pos + s.len] == s:
65
+
p.pos += s.len
66
+
n
67
+
else:
68
+
p.fail("expected " & s)
69
+
nil
70
+
71
+
proc parseValue(p: var Parser): JNode
72
+
73
+
proc parseObject(p: var Parser): JNode =
74
+
p.expect('{')
75
+
result = JNode(kind: jkObject, fields: initTable[string, JNode]())
76
+
p.skipWs()
77
+
if p.pos < p.src.len and p.src[p.pos] == '}':
78
+
inc p.pos
79
+
return
80
+
while true:
81
+
let k = p.parseString()
82
+
p.expect(':')
83
+
result.fields[k] = p.parseValue()
84
+
p.skipWs()
85
+
if p.pos < p.src.len and p.src[p.pos] == ',':
86
+
inc p.pos
87
+
elif p.pos < p.src.len and p.src[p.pos] == '}':
88
+
inc p.pos
89
+
return
90
+
else:
91
+
p.fail("expected ',' or '}'")
92
+
93
+
proc parseArray(p: var Parser): JNode =
94
+
p.expect('[')
95
+
result = JNode(kind: jkArray)
96
+
p.skipWs()
97
+
if p.pos < p.src.len and p.src[p.pos] == ']':
98
+
inc p.pos
99
+
return
100
+
while true:
101
+
result.elems.add(p.parseValue())
102
+
p.skipWs()
103
+
if p.pos < p.src.len and p.src[p.pos] == ',':
104
+
inc p.pos
105
+
elif p.pos < p.src.len and p.src[p.pos] == ']':
106
+
inc p.pos
107
+
return
108
+
else:
109
+
p.fail("expected ',' or ']'")
110
+
111
+
proc parseValue(p: var Parser): JNode =
112
+
p.skipWs()
113
+
if p.pos >= p.src.len:
114
+
p.fail("expected value")
115
+
case p.src[p.pos]
116
+
of '{':
117
+
p.parseObject()
118
+
of '[':
119
+
p.parseArray()
120
+
of '"':
121
+
JNode(kind: jkString, str: p.parseString())
122
+
of 't':
123
+
p.lit("true", JNode(kind: jkBool, b: true))
124
+
of 'f':
125
+
p.lit("false", JNode(kind: jkBool, b: false))
126
+
of 'n':
127
+
p.lit("null", JNode(kind: jkNull))
128
+
else:
129
+
p.fail("unexpected value")
130
+
nil
131
+
132
+
proc parseJsonLocal(src: string): JNode =
133
+
var p = Parser(src: src, pos: 0)
134
+
result = p.parseValue()
135
+
p.skipWs()
136
+
if p.pos != p.src.len:
137
+
p.fail("trailing input")
138
+
139
+
proc field(n: JNode, k: string): JNode =
140
+
if n.kind != jkObject or k notin n.fields:
141
+
raise newException(ValueError, "missing field: " & k)
142
+
n.fields[k]
143
+
144
+
proc asString(n: JNode): string =
145
+
if n.kind != jkString:
146
+
raise newException(ValueError, "expected string")
147
+
n.str
148
+
149
+
proc termFromNode(n: JNode): Named =
150
+
let tag = n.field("tag").asString()
151
+
case tag
152
+
of "Var":
153
+
nVar(n.field("name").asString())
154
+
of "Lam":
155
+
nLam(n.field("param").asString(), termFromNode(n.field("body")))
156
+
of "App":
157
+
nApp(termFromNode(n.field("fun")), termFromNode(n.field("arg")))
158
+
of "Subst":
159
+
nSubst(n.field("var").asString(), termFromNode(n.field("repl")),
160
+
termFromNode(n.field("body")))
161
+
else:
162
+
raise newException(ValueError, "unknown tag: " & tag)
163
+
164
+
type CorpusEntry* = object
165
+
name*: string
166
+
t1*, t2*: Named
167
+
expected*: int
168
+
169
+
proc loadCorpus*(path: string): seq[CorpusEntry] =
170
+
let doc = parseJsonLocal(readFile(path))
171
+
if doc.kind != jkArray:
172
+
raise newException(ValueError, "corpus must be an array")
173
+
for e in doc.elems:
174
+
let exp = e.field("expected")
175
+
var ex = 2
176
+
if exp.kind == jkBool:
177
+
ex = if exp.b: 1 else: 0
178
+
result.add(CorpusEntry(name: e.field("name").asString(),
179
+
t1: termFromNode(e.field("t1")), t2: termFromNode(e.field("t2")),
180
+
expected: ex))
181
+
182
+
proc loadBench*(path: string): seq[(string, Named)] =
183
+
let doc = parseJsonLocal(readFile(path))
184
+
if doc.kind != jkObject:
185
+
raise newException(ValueError, "bench must be an object")
186
+
for k, v in doc.fields:
187
+
result.add((k, termFromNode(v)))
+207
nim/src/ego/named.nim
+207
nim/src/ego/named.nim
···
1
+
import std/[sets, tables]
2
+
3
+
type
4
+
NamedKind* = enum nkVar, nkLam, nkApp, nkSubst
5
+
Named* = ref object
6
+
case kind*: NamedKind
7
+
of nkVar: name*: string
8
+
of nkLam:
9
+
param*: string
10
+
body*: Named
11
+
of nkApp:
12
+
fun*, arg*: Named
13
+
of nkSubst:
14
+
svar*: string
15
+
repl*, sbody*: Named
16
+
17
+
proc nVar*(n: string): Named = Named(kind: nkVar, name: n)
18
+
proc nLam*(p: string, b: Named): Named = Named(kind: nkLam, param: p, body: b)
19
+
proc nApp*(f, a: Named): Named = Named(kind: nkApp, fun: f, arg: a)
20
+
proc nSubst*(x: string, s, b: Named): Named =
21
+
Named(kind: nkSubst, svar: x, repl: s, sbody: b)
22
+
23
+
proc freeVars*(t: Named): HashSet[string] =
24
+
case t.kind
25
+
of nkVar: result.incl(t.name)
26
+
of nkLam:
27
+
result = freeVars(t.body)
28
+
result.excl(t.param)
29
+
of nkApp:
30
+
result = freeVars(t.fun)
31
+
result = result + freeVars(t.arg)
32
+
of nkSubst:
33
+
var b = freeVars(t.sbody)
34
+
let used = t.svar in b
35
+
b.excl(t.svar)
36
+
result = b
37
+
if used:
38
+
result = result + freeVars(t.repl)
39
+
40
+
proc size*(t: Named): int =
41
+
case t.kind
42
+
of nkVar: 1
43
+
of nkLam: 1 + size(t.body)
44
+
of nkApp: 1 + size(t.fun) + size(t.arg)
45
+
of nkSubst: 1 + size(t.repl) + size(t.sbody)
46
+
47
+
type Ctx* = object
48
+
traversals*: int
49
+
maxDepth*: int
50
+
51
+
proc tick*(c: var Ctx, depth: int) {.inline.} =
52
+
inc c.traversals
53
+
if depth > c.maxDepth: c.maxDepth = depth
54
+
55
+
proc freshName(avoid: HashSet[string], base: string): string =
56
+
if base notin avoid: return base
57
+
var i = 0
58
+
while true:
59
+
let cand = base & $i
60
+
if cand notin avoid: return cand
61
+
inc i
62
+
63
+
proc rename(t: Named, old, nw: string): Named =
64
+
case t.kind
65
+
of nkVar: (if t.name == old: nVar(nw) else: t)
66
+
of nkApp: nApp(rename(t.fun, old, nw), rename(t.arg, old, nw))
67
+
of nkLam:
68
+
if t.param == old: t
69
+
else: nLam(t.param, rename(t.body, old, nw))
70
+
of nkSubst:
71
+
if t.svar == old: nSubst(t.svar, rename(t.repl, old, nw), t.sbody)
72
+
else: nSubst(t.svar, rename(t.repl, old, nw), rename(t.sbody, old, nw))
73
+
74
+
proc substitute*(x: string, s, body: Named): Named =
75
+
let fvS = freeVars(s)
76
+
let avoid0 = fvS + freeVars(body)
77
+
proc go(t: Named, avoid: HashSet[string]): Named =
78
+
case t.kind
79
+
of nkVar: (if t.name == x: s else: t)
80
+
of nkApp: nApp(go(t.fun, avoid), go(t.arg, avoid))
81
+
of nkLam:
82
+
if t.param == x: t
83
+
elif (t.param notin fvS) or (x notin freeVars(t.body)):
84
+
nLam(t.param, go(t.body, avoid))
85
+
else:
86
+
let y = freshName(avoid, t.param)
87
+
var avoid2 = avoid
88
+
avoid2.incl(y)
89
+
nLam(y, go(rename(t.body, t.param, y), avoid2))
90
+
of nkSubst:
91
+
if t.svar == x: nSubst(t.svar, go(t.repl, avoid), t.sbody)
92
+
elif (t.svar notin fvS) or (x notin freeVars(t.sbody)):
93
+
nSubst(t.svar, go(t.repl, avoid), go(t.sbody, avoid))
94
+
else:
95
+
let y = freshName(avoid, t.svar)
96
+
var avoid2 = avoid
97
+
avoid2.incl(y)
98
+
nSubst(y, go(t.repl, avoid), go(rename(t.sbody, t.svar, y), avoid2))
99
+
go(body, avoid0)
100
+
101
+
const stepLimit = 100000
102
+
103
+
proc elimSubst*(t: Named): Named =
104
+
case t.kind
105
+
of nkVar: t
106
+
of nkLam: nLam(t.param, elimSubst(t.body))
107
+
of nkApp: nApp(elimSubst(t.fun), elimSubst(t.arg))
108
+
of nkSubst: substitute(t.svar, elimSubst(t.repl), elimSubst(t.sbody))
109
+
110
+
proc eqTerm(a, b: Named): bool =
111
+
if a.kind != b.kind: return false
112
+
case a.kind
113
+
of nkVar: a.name == b.name
114
+
of nkLam: a.param == b.param and eqTerm(a.body, b.body)
115
+
of nkApp: eqTerm(a.fun, b.fun) and eqTerm(a.arg, b.arg)
116
+
of nkSubst:
117
+
a.svar == b.svar and eqTerm(a.repl, b.repl) and eqTerm(a.sbody, b.sbody)
118
+
119
+
proc step(t: Named): Named =
120
+
case t.kind
121
+
of nkApp:
122
+
if t.fun.kind == nkLam:
123
+
return substitute(t.fun.param, t.arg, t.fun.body)
124
+
let f = step(t.fun)
125
+
if not eqTerm(f, t.fun): return nApp(f, t.arg)
126
+
let a = step(t.arg)
127
+
if not eqTerm(a, t.arg): return nApp(t.fun, a)
128
+
t
129
+
of nkLam:
130
+
let b = step(t.body)
131
+
if not eqTerm(b, t.body): nLam(t.param, b) else: t
132
+
else: t
133
+
134
+
proc normalise*(t: Named): Named =
135
+
result = elimSubst(t)
136
+
var n = 0
137
+
while n < stepLimit:
138
+
let t2 = step(result)
139
+
if eqTerm(t2, result): break
140
+
result = t2
141
+
inc n
142
+
143
+
proc alphaEqNF(a, b: Named, c: var Ctx): bool =
144
+
proc go(a, b: Named, ea, eb: Table[string, int], d: int,
145
+
c: var Ctx): bool =
146
+
c.tick(d)
147
+
if a.kind != b.kind: return false
148
+
case a.kind
149
+
of nkVar:
150
+
let ia = ea.getOrDefault(a.name, -1)
151
+
let ib = eb.getOrDefault(b.name, -1)
152
+
if ia >= 0 or ib >= 0: ia == ib
153
+
else: a.name == b.name
154
+
of nkLam:
155
+
var ea2 = ea
156
+
var eb2 = eb
157
+
ea2[a.param] = d
158
+
eb2[b.param] = d
159
+
go(a.body, b.body, ea2, eb2, d + 1, c)
160
+
of nkApp:
161
+
go(a.fun, b.fun, ea, eb, d + 1, c) and
162
+
go(a.arg, b.arg, ea, eb, d + 1, c)
163
+
of nkSubst: false
164
+
go(a, b, initTable[string, int](), initTable[string, int](), 0, c)
165
+
166
+
proc alphaEquivalent*(a, b: Named): bool =
167
+
var c: Ctx
168
+
alphaEqNF(normalise(a), normalise(b), c)
169
+
170
+
proc alphaEquivalentCounted*(a, b: Named): tuple[r: bool, c: Ctx] =
171
+
var c: Ctx
172
+
let r = alphaEqNF(normalise(a), normalise(b), c)
173
+
(r, c)
174
+
175
+
proc normaliseCounted*(t: Named): tuple[r: Named, c: Ctx] =
176
+
var c: Ctx
177
+
proc walk(t: Named, d: int) =
178
+
c.tick(d)
179
+
case t.kind
180
+
of nkVar: discard
181
+
of nkLam: walk(t.body, d + 1)
182
+
of nkApp: walk(t.fun, d + 1); walk(t.arg, d + 1)
183
+
of nkSubst: walk(t.repl, d + 1); walk(t.sbody, d + 1)
184
+
var r = elimSubst(t)
185
+
walk(r, 0)
186
+
var n = 0
187
+
while n < stepLimit:
188
+
let t2 = step(r)
189
+
walk(t2, 0)
190
+
if eqTerm(t2, r): break
191
+
r = t2
192
+
inc n
193
+
(r, c)
194
+
195
+
proc `$`*(t: Named): string =
196
+
case t.kind
197
+
of nkVar: t.name
198
+
of nkLam: "\\" & t.param & ". " & $t.body
199
+
of nkApp:
200
+
let fs = if t.fun.kind in {nkLam, nkSubst}: "(" & $t.fun & ")" else: $t.fun
201
+
let argStr = if t.arg.kind == nkVar: $t.arg else: "(" & $t.arg & ")"
202
+
fs & " " & argStr
203
+
of nkSubst: "[" & t.svar & " := " & $t.repl & "] " & $t.sbody
204
+
205
+
proc prettyPrint*(t: Named): string = $t
206
+
proc convertFromNamed*(t: Named): Named = t
207
+
proc convertToNamed*(t: Named): Named = t
+224
nim/src/ego/nameless.nim
+224
nim/src/ego/nameless.nim
···
1
+
import std/sets
2
+
import named
3
+
4
+
type
5
+
LnKind* = enum lkBVar, lkFVar, lkLam, lkApp
6
+
LocallyNameless* = ref LnObj
7
+
LnObj = object
8
+
case kind: LnKind
9
+
of lkBVar:
10
+
idx: int
11
+
of lkFVar:
12
+
name: string
13
+
of lkLam:
14
+
body: LocallyNameless
15
+
of lkApp:
16
+
fun, arg: LocallyNameless
17
+
18
+
proc bVar*(i: int): LocallyNameless = (ref LnObj)(kind: lkBVar, idx: i)
19
+
proc fVar*(n: string): LocallyNameless = (ref LnObj)(kind: lkFVar, name: n)
20
+
proc lLam*(b: LocallyNameless): LocallyNameless = (ref LnObj)(kind: lkLam, body: b)
21
+
proc lApp*(f, a: LocallyNameless): LocallyNameless = (ref LnObj)(kind: lkApp, fun: f, arg: a)
22
+
23
+
proc kind*(t: LocallyNameless): LnKind = t.kind
24
+
proc idx*(t: LocallyNameless): int = t.idx
25
+
proc name*(t: LocallyNameless): string = t.name
26
+
proc body*(t: LocallyNameless): LocallyNameless = t.body
27
+
proc fun*(t: LocallyNameless): LocallyNameless = t.fun
28
+
proc arg*(t: LocallyNameless): LocallyNameless = t.arg
29
+
30
+
type NotLocallyClosed* = object of CatchableError
31
+
32
+
type Ctx* = object
33
+
traversals*: int
34
+
maxDepth*: int
35
+
36
+
proc tick*(c: var Ctx, depth: int) {.inline.} =
37
+
inc c.traversals
38
+
if depth > c.maxDepth: c.maxDepth = depth
39
+
40
+
proc freeVars*(t: LocallyNameless): HashSet[string] =
41
+
case t.kind
42
+
of lkBVar: discard
43
+
of lkFVar: result.incl(t.name)
44
+
of lkLam: result = freeVars(t.body)
45
+
of lkApp:
46
+
result = freeVars(t.fun)
47
+
result = result + freeVars(t.arg)
48
+
49
+
proc openAt(t: LocallyNameless, k: int, x: string): LocallyNameless =
50
+
case t.kind
51
+
of lkBVar: (if t.idx == k: fVar(x) else: t)
52
+
of lkFVar: t
53
+
of lkLam: lLam(openAt(t.body, k + 1, x))
54
+
of lkApp: lApp(openAt(t.fun, k, x), openAt(t.arg, k, x))
55
+
56
+
proc openTop*(t: LocallyNameless, x: string): LocallyNameless = openAt(t, 0, x)
57
+
58
+
proc closeAt(t: LocallyNameless, k: int, x: string): LocallyNameless =
59
+
case t.kind
60
+
of lkBVar: t
61
+
of lkFVar: (if t.name == x: bVar(k) else: t)
62
+
of lkLam: lLam(closeAt(t.body, k + 1, x))
63
+
of lkApp: lApp(closeAt(t.fun, k, x), closeAt(t.arg, k, x))
64
+
65
+
proc closeTop*(t: LocallyNameless, x: string): LocallyNameless = closeAt(t, 0, x)
66
+
67
+
proc lcAt(t: LocallyNameless, depth: int): bool =
68
+
case t.kind
69
+
of lkBVar: t.idx < depth
70
+
of lkFVar: true
71
+
of lkLam: lcAt(t.body, depth + 1)
72
+
of lkApp: lcAt(t.fun, depth) and lcAt(t.arg, depth)
73
+
74
+
proc lc*(t: LocallyNameless): bool = lcAt(t, 0)
75
+
76
+
proc requireLc(t: LocallyNameless) =
77
+
if not lc(t):
78
+
raise newException(NotLocallyClosed, "term is not locally closed")
79
+
80
+
proc eqLn(a, b: LocallyNameless): bool =
81
+
if a.kind != b.kind: return false
82
+
case a.kind
83
+
of lkBVar: a.idx == b.idx
84
+
of lkFVar: a.name == b.name
85
+
of lkLam: eqLn(a.body, b.body)
86
+
of lkApp: eqLn(a.fun, b.fun) and eqLn(a.arg, b.arg)
87
+
88
+
proc shift(t: LocallyNameless, cutoff: int): LocallyNameless =
89
+
case t.kind
90
+
of lkBVar: (if t.idx >= cutoff: bVar(t.idx + 1) else: t)
91
+
of lkFVar: t
92
+
of lkLam: lLam(shift(t.body, cutoff + 1))
93
+
of lkApp: lApp(shift(t.fun, cutoff), shift(t.arg, cutoff))
94
+
95
+
proc substBvar*(t: LocallyNameless, j: int, s: LocallyNameless): LocallyNameless =
96
+
case t.kind
97
+
of lkBVar:
98
+
if t.idx == j: s
99
+
elif t.idx > j: bVar(t.idx - 1)
100
+
else: t
101
+
of lkFVar: t
102
+
of lkLam: lLam(substBvar(t.body, j + 1, shift(s, 0)))
103
+
of lkApp: lApp(substBvar(t.fun, j, s), substBvar(t.arg, j, s))
104
+
105
+
proc substFvar*(t: LocallyNameless, x: string, s: LocallyNameless): LocallyNameless =
106
+
case t.kind
107
+
of lkBVar: t
108
+
of lkFVar: (if t.name == x: s else: t)
109
+
of lkLam: lLam(substFvar(t.body, x, s))
110
+
of lkApp: lApp(substFvar(t.fun, x, s), substFvar(t.arg, x, s))
111
+
112
+
proc substitute*(t: LocallyNameless, x: string, s: LocallyNameless): LocallyNameless =
113
+
substFvar(t, x, s)
114
+
115
+
proc step(t: LocallyNameless): LocallyNameless =
116
+
case t.kind
117
+
of lkApp:
118
+
if t.fun.kind == lkLam:
119
+
return substBvar(t.fun.body, 0, t.arg)
120
+
let f = step(t.fun)
121
+
if not eqLn(f, t.fun): return lApp(f, t.arg)
122
+
let a = step(t.arg)
123
+
if not eqLn(a, t.arg): return lApp(t.fun, a)
124
+
t
125
+
of lkLam:
126
+
let b = step(t.body)
127
+
if not eqLn(b, t.body): lLam(b) else: t
128
+
else: t
129
+
130
+
const stepLimit = 100000
131
+
132
+
proc normalise*(t: LocallyNameless): LocallyNameless =
133
+
requireLc(t)
134
+
result = t
135
+
var n = 0
136
+
while n < stepLimit:
137
+
let t2 = step(result)
138
+
if eqLn(t2, result): break
139
+
result = t2
140
+
inc n
141
+
142
+
proc convertFromNamed*(t: named.Named): LocallyNameless =
143
+
proc go(t: named.Named, env: seq[(string, int)]): LocallyNameless =
144
+
case t.kind
145
+
of named.nkVar:
146
+
for (v, i) in env:
147
+
if v == t.name: return bVar(i)
148
+
fVar(t.name)
149
+
of named.nkLam:
150
+
var env2 = @[(t.param, 0)]
151
+
for (v, i) in env: env2.add((v, i + 1))
152
+
lLam(go(t.body, env2))
153
+
of named.nkApp: lApp(go(t.fun, env), go(t.arg, env))
154
+
of named.nkSubst:
155
+
go(named.substitute(t.svar, t.repl, t.sbody), env)
156
+
go(t, @[])
157
+
158
+
proc convertToNamed*(t: LocallyNameless): named.Named =
159
+
requireLc(t)
160
+
let fv = freeVars(t)
161
+
proc go(t: LocallyNameless, env: seq[string]): named.Named =
162
+
case t.kind
163
+
of lkBVar:
164
+
if t.idx >= env.len:
165
+
raise newException(NotLocallyClosed, "unbound index " & $t.idx)
166
+
named.nVar(env[t.idx])
167
+
of lkFVar: named.nVar(t.name)
168
+
of lkLam:
169
+
var avoid = fv
170
+
for x in env: avoid.incl(x)
171
+
var cand = "v"
172
+
var i = 0
173
+
while cand in avoid:
174
+
cand = "v" & $i
175
+
inc i
176
+
named.nLam(cand, go(t.body, @[cand] & env))
177
+
of lkApp: named.nApp(go(t.fun, env), go(t.arg, env))
178
+
go(t, @[])
179
+
180
+
proc alphaEquivalent*(a, b: LocallyNameless): bool =
181
+
requireLc(a)
182
+
requireLc(b)
183
+
eqLn(normalise(a), normalise(b))
184
+
185
+
proc alphaEquivalentCounted*(a, b: LocallyNameless): tuple[r: bool, c: Ctx] =
186
+
requireLc(a)
187
+
requireLc(b)
188
+
var c: Ctx
189
+
proc go(a, b: LocallyNameless, d: int): bool =
190
+
c.tick(d)
191
+
if a.kind != b.kind: return false
192
+
case a.kind
193
+
of lkBVar: a.idx == b.idx
194
+
of lkFVar: a.name == b.name
195
+
of lkLam: go(a.body, b.body, d + 1)
196
+
of lkApp: go(a.fun, b.fun, d + 1) and go(a.arg, b.arg, d + 1)
197
+
(go(normalise(a), normalise(b), 0), c)
198
+
199
+
proc normaliseCounted*(t: LocallyNameless): tuple[r: LocallyNameless, c: Ctx] =
200
+
requireLc(t)
201
+
var c: Ctx
202
+
proc walk(t: LocallyNameless, d: int) =
203
+
c.tick(d)
204
+
case t.kind
205
+
of lkBVar, lkFVar: discard
206
+
of lkLam: walk(t.body, d + 1)
207
+
of lkApp: walk(t.fun, d + 1); walk(t.arg, d + 1)
208
+
var r = t
209
+
walk(r, 0)
210
+
var n = 0
211
+
while n < stepLimit:
212
+
let t2 = step(r)
213
+
walk(t2, 0)
214
+
if eqLn(t2, r): break
215
+
r = t2
216
+
inc n
217
+
(r, c)
218
+
219
+
proc prettyPrint*(t: LocallyNameless): string =
220
+
case t.kind
221
+
of lkBVar: "#" & $t.idx
222
+
of lkFVar: t.name
223
+
of lkLam: "\\. " & prettyPrint(t.body)
224
+
of lkApp: prettyPrint(t.fun) & " " & prettyPrint(t.arg)
+113
nim/src/ego/syntax.nim
+113
nim/src/ego/syntax.nim
···
1
+
import named
2
+
3
+
type
4
+
TokKind = enum tkVar, tkSlash, tkDot, tkLParen, tkRParen, tkLBrack, tkRBrack,
5
+
tkAssign, tkEnd
6
+
Tok = object
7
+
kind: TokKind
8
+
text: string
9
+
10
+
proc isNameStart(ch: char): bool = ch in {'a'..'z', 'A'..'Z'}
11
+
proc isNameChar(ch: char): bool =
12
+
ch in {'a'..'z', 'A'..'Z', '0'..'9', '_', '\'', '-'}
13
+
14
+
proc lex(src: string): seq[Tok] =
15
+
var i = 0
16
+
while i < src.len:
17
+
let ch = src[i]
18
+
if ch in {' ', '\t', '\n', '\r'}:
19
+
inc i
20
+
elif isNameStart(ch):
21
+
var j = i
22
+
while j < src.len and isNameChar(src[j]): inc j
23
+
result.add(Tok(kind: tkVar, text: src[i ..< j]))
24
+
i = j
25
+
elif ch == '\\' or ch == 0xCE.char:
26
+
if ch == 0xCE.char and i + 1 < src.len and src[i + 1] == 0xBB.char:
27
+
result.add(Tok(kind: tkSlash))
28
+
i += 2
29
+
else:
30
+
result.add(Tok(kind: tkSlash))
31
+
inc i
32
+
elif ch == '.':
33
+
result.add(Tok(kind: tkDot)); inc i
34
+
elif ch == '(':
35
+
result.add(Tok(kind: tkLParen)); inc i
36
+
elif ch == ')':
37
+
result.add(Tok(kind: tkRParen)); inc i
38
+
elif ch == '[':
39
+
result.add(Tok(kind: tkLBrack)); inc i
40
+
elif ch == ']':
41
+
result.add(Tok(kind: tkRBrack)); inc i
42
+
elif ch == ':' and i + 1 < src.len and src[i + 1] == '=':
43
+
result.add(Tok(kind: tkAssign)); i += 2
44
+
else:
45
+
raise newException(ValueError, "unexpected character: " & $ch)
46
+
result.add(Tok(kind: tkEnd))
47
+
48
+
type Parser = object
49
+
toks: seq[Tok]
50
+
pos: int
51
+
52
+
proc peek(p: Parser): Tok = p.toks[p.pos]
53
+
proc next(p: var Parser): Tok =
54
+
result = p.toks[p.pos]
55
+
inc p.pos
56
+
57
+
proc expect(p: var Parser, k: TokKind) =
58
+
if p.peek.kind != k:
59
+
raise newException(ValueError, "expected " & $k & " got " & $p.peek.kind)
60
+
discard p.next()
61
+
62
+
proc parseTerm(p: var Parser): Named
63
+
64
+
proc parseAtom(p: var Parser): Named =
65
+
let t = p.peek
66
+
case t.kind
67
+
of tkVar:
68
+
discard p.next()
69
+
nVar(t.text)
70
+
of tkSlash:
71
+
discard p.next()
72
+
let v = p.next()
73
+
if v.kind != tkVar:
74
+
raise newException(ValueError, "expected binder name")
75
+
p.expect(tkDot)
76
+
nLam(v.text, parseTerm(p))
77
+
of tkLParen:
78
+
discard p.next()
79
+
let t2 = parseTerm(p)
80
+
p.expect(tkRParen)
81
+
t2
82
+
of tkLBrack:
83
+
discard p.next()
84
+
let v = p.next()
85
+
if v.kind != tkVar:
86
+
raise newException(ValueError, "expected substitution variable")
87
+
p.expect(tkAssign)
88
+
let s = parseTerm(p)
89
+
p.expect(tkRBrack)
90
+
let b = parseTerm(p)
91
+
nSubst(v.text, s, b)
92
+
else:
93
+
raise newException(ValueError, "unexpected token: " & $t.kind)
94
+
95
+
proc startsAtom(p: Parser): bool =
96
+
p.peek.kind in {tkVar, tkSlash, tkLParen, tkLBrack}
97
+
98
+
proc parseTerm(p: var Parser): Named =
99
+
result = parseAtom(p)
100
+
while p.startsAtom():
101
+
result = nApp(result, parseAtom(p))
102
+
103
+
proc parse*(src: string): Named =
104
+
var p = Parser(toks: lex(src), pos: 0)
105
+
result = parseTerm(p)
106
+
if p.peek.kind != tkEnd:
107
+
raise newException(ValueError, "trailing input")
108
+
109
+
proc parseResult*(src: string): tuple[ok: bool, term: Named, err: string] =
110
+
try:
111
+
(true, parse(src), "")
112
+
except ValueError as e:
113
+
(false, nil, e.msg)
+183
nim/tests/test_ego.nim
+183
nim/tests/test_ego.nim
···
1
+
import std/[os, random, sets]
2
+
import ego/named, ego/debruijn, ego/locally_nameless, ego/explicit_subst,
3
+
ego/syntax, ego/jsonio
4
+
5
+
type Rep = enum rNamed, rDebruijn, rLn, rSubst
6
+
7
+
let reps = [rNamed, rDebruijn, rLn, rSubst]
8
+
9
+
proc check(cond: bool, msg: string) =
10
+
if not cond:
11
+
raise newException(AssertionDefect, msg)
12
+
13
+
proc expectRaises[T: CatchableError](msg: string, f: proc()) =
14
+
try:
15
+
f()
16
+
raise newException(AssertionDefect, msg & ": expected exception")
17
+
except T:
18
+
discard
19
+
20
+
proc findCorpus(): string =
21
+
for p in ["../shared/corpus.json", "shared/corpus.json",
22
+
"/home/bulg/projects/ego/shared/corpus.json"]:
23
+
if fileExists(p): return p
24
+
raise newException(IOError, "corpus.json not found")
25
+
26
+
proc checkWith(rep: Rep, t1, t2: Named): bool =
27
+
case rep
28
+
of rNamed:
29
+
named.alphaEquivalent(t1, t2)
30
+
of rDebruijn:
31
+
debruijn.alphaEquivalent(debruijn.convertFromNamed(t1),
32
+
debruijn.convertFromNamed(t2))
33
+
of rLn:
34
+
locally_nameless.alphaEquivalent(locally_nameless.convertFromNamed(t1),
35
+
locally_nameless.convertFromNamed(t2))
36
+
of rSubst:
37
+
explicit_subst.alphaEquivalent(explicit_subst.convertFromNamed(t1),
38
+
explicit_subst.convertFromNamed(t2))
39
+
40
+
proc pick(r: var Rand, xs: openArray[string]): string =
41
+
xs[r.rand(xs.len - 1)]
42
+
43
+
proc genLeaf(r: var Rand, scope: seq[string]): Named =
44
+
let fvs = ["p", "q", "g", "h"]
45
+
if scope.len > 0 and r.rand(99) < 75:
46
+
nVar(r.pick(scope))
47
+
else:
48
+
nVar(r.pick(fvs))
49
+
50
+
proc gen(r: var Rand, scope: seq[string], depth: int): Named =
51
+
let names = ["a", "b", "c", "d", "e", "f"]
52
+
if depth <= 0:
53
+
return genLeaf(r, scope)
54
+
let n = r.rand(99)
55
+
if n < 45:
56
+
let binder =
57
+
if scope.len > 0 and r.rand(99) < 35: r.pick(scope) else: r.pick(names)
58
+
return nLam(binder, gen(r, scope & @[binder], depth - 1))
59
+
if n < 75:
60
+
return nApp(genLeaf(r, scope), genLeaf(r, scope))
61
+
if n < 85:
62
+
let x = if scope.len == 0: "u" else: r.pick(scope)
63
+
return nSubst(x, gen(r, scope, depth - 1), gen(r, scope, depth - 1))
64
+
genLeaf(r, scope)
65
+
66
+
proc randomTerm(r: var Rand): Named =
67
+
gen(r, @[], 2 + r.rand(3))
68
+
69
+
proc testCorpus() =
70
+
for e in loadCorpus(findCorpus()):
71
+
var first = false
72
+
var haveFirst = false
73
+
for rep in reps:
74
+
let got = checkWith(rep, e.t1, e.t2)
75
+
if e.expected != 2:
76
+
check(got == (e.expected == 1), e.name & " expected mismatch")
77
+
if haveFirst:
78
+
check(got == first, e.name & " representation disagreement")
79
+
else:
80
+
first = got
81
+
haveFirst = true
82
+
83
+
proc testProperties() =
84
+
var r = initRand(42)
85
+
for _ in 0 ..< 200:
86
+
let t = randomTerm(r)
87
+
for rep in reps:
88
+
check(checkWith(rep, t, t), "reflexivity")
89
+
for _ in 0 ..< 200:
90
+
let t1 = randomTerm(r)
91
+
let t2 = randomTerm(r)
92
+
for rep in reps:
93
+
check(checkWith(rep, t1, t2) == checkWith(rep, t2, t1), "symmetry")
94
+
for _ in 0 ..< 100:
95
+
let t = randomTerm(r)
96
+
let n = named.normalise(t)
97
+
for rep in reps:
98
+
check(checkWith(rep, t, t) and checkWith(rep, n, n), "transitivity sample")
99
+
for _ in 0 ..< 200:
100
+
let t1 = randomTerm(r)
101
+
let t2 = randomTerm(r)
102
+
if named.alphaEquivalent(t1, t2):
103
+
check(freeVars(named.normalise(t1)) == freeVars(named.normalise(t2)),
104
+
"free variables preserved")
105
+
for _ in 0 ..< 200:
106
+
let t = randomTerm(r)
107
+
check(named.alphaEquivalent(debruijn.convertToNamed(debruijn.convertFromNamed(t)), t),
108
+
"debruijn roundtrip")
109
+
check(named.alphaEquivalent(locally_nameless.convertToNamed(
110
+
locally_nameless.convertFromNamed(t)), t), "ln roundtrip")
111
+
check(named.alphaEquivalent(explicit_subst.convertToNamed(
112
+
explicit_subst.convertFromNamed(t)), t), "subst roundtrip")
113
+
for _ in 0 ..< 100:
114
+
let t = randomTerm(r)
115
+
let n1 = named.normalise(t)
116
+
let n2 = debruijn.convertToNamed(debruijn.normalise(debruijn.convertFromNamed(t)))
117
+
let n3 = locally_nameless.convertToNamed(
118
+
locally_nameless.normalise(locally_nameless.convertFromNamed(t)))
119
+
let n4 = explicit_subst.convertToNamed(
120
+
explicit_subst.normalise(explicit_subst.convertFromNamed(t)))
121
+
check(named.alphaEquivalent(n1, n2), "named vs debruijn normalise")
122
+
check(named.alphaEquivalent(n1, n3), "named vs ln normalise")
123
+
check(named.alphaEquivalent(n1, n4), "named vs subst normalise")
124
+
125
+
proc testParseErrors() =
126
+
for s in ["", "\\", "\\x", "\\x.", "(\\x. x", "\\x. x)", "[x := ] x",
127
+
"[ := y] x", "((x", "[x := y]", ".", "\\. x"]:
128
+
let r = parseResult(s)
129
+
check(not r.ok, "parser accepted " & s)
130
+
131
+
proc testMalformed() =
132
+
check(not locally_nameless.lc(bVar(0)), "dangling bvar")
133
+
check(locally_nameless.lc(lLam(bVar(0))), "closed lambda")
134
+
check(not locally_nameless.lc(lLam(lLam(bVar(2)))), "dangling deep")
135
+
expectRaises[NotLocallyClosed]("ln convert", proc () =
136
+
discard locally_nameless.convertToNamed(bVar(3))
137
+
)
138
+
expectRaises[NotLocallyClosed]("ln alpha", proc () =
139
+
discard locally_nameless.alphaEquivalent(bVar(1), bVar(1))
140
+
)
141
+
check(debruijn.wellScoped(dLam(dVar(0))), "well scoped db")
142
+
check(not debruijn.wellScoped(dVar(0)), "ill scoped db")
143
+
expectRaises[UnboundIndex]("db convert", proc () =
144
+
discard debruijn.convertToNamed(dLam(dVar(2)))
145
+
)
146
+
147
+
proc parsed(s: string): Named =
148
+
let r = parseResult(s)
149
+
if not r.ok:
150
+
raise newException(ValueError, r.err)
151
+
r.term
152
+
153
+
proc testCapture() =
154
+
let cases = [
155
+
("[x := z] \\z. x", "\\w. z", true),
156
+
("[x := z] \\z. x", "\\z. z", false),
157
+
("[x := q] \\x. x", "\\x. x", true),
158
+
("[x := y] \\y. x y", "\\w. y w", true),
159
+
("[x := f y] \\y. \\z. x z", "\\a. \\b. f y b", true),
160
+
("[x := a] [y := b] x y", "a b", true)
161
+
]
162
+
for (a, b, exp) in cases:
163
+
let t1 = parsed(a)
164
+
let t2 = parsed(b)
165
+
for rep in reps:
166
+
check(checkWith(rep, t1, t2) == exp, a & " ~ " & b)
167
+
let t = explicit_subst.ofNamed(
168
+
nSubst("x", nVar("z"), nLam("z", nVar("x"))))
169
+
let n = explicit_subst.normalise(t)
170
+
check(n.kind == ekLam, "expected lambda after explicit normalise")
171
+
check(n.param != "z", "binder renamed")
172
+
check(n.body.kind == ekVar and n.body.name == "z", "body is free z")
173
+
check(explicit_subst.alphaEquivalentSusp(t, n), "susp agrees")
174
+
175
+
proc run(name: string, f: proc()) =
176
+
f()
177
+
echo "ok ", name
178
+
179
+
run("corpus", testCorpus)
180
+
run("properties", testProperties)
181
+
run("parse errors", testParseErrors)
182
+
run("malformed", testMalformed)
183
+
run("capture", testCapture)
+264
ocaml/bin/main.ml
+264
ocaml/bin/main.ml
···
1
+
open Ego
2
+
3
+
let reps_of_string = function
4
+
| "named" -> [ `Named ]
5
+
| "debruijn" -> [ `Debruijn ]
6
+
| "ln" -> [ `Ln ]
7
+
| "subst" -> [ `Subst ]
8
+
| "all" -> [ `Named; `Debruijn; `Ln; `Subst ]
9
+
| r -> failwith ("unknown representation: " ^ r)
10
+
11
+
let rep_name = function
12
+
| `Named -> "named"
13
+
| `Debruijn -> "debruijn"
14
+
| `Ln -> "ln"
15
+
| `Subst -> "subst"
16
+
17
+
let check_with rep t1 t2 =
18
+
match rep with
19
+
| `Named -> Named.alpha_equivalent t1 t2
20
+
| `Debruijn ->
21
+
Debruijn.alpha_equivalent
22
+
(Debruijn.convert_from_named t1)
23
+
(Debruijn.convert_from_named t2)
24
+
| `Ln ->
25
+
Locally_nameless.alpha_equivalent
26
+
(Locally_nameless.convert_from_named t1)
27
+
(Locally_nameless.convert_from_named t2)
28
+
| `Subst ->
29
+
Explicit_subst.alpha_equivalent
30
+
(Explicit_subst.convert_from_named t1)
31
+
(Explicit_subst.convert_from_named t2)
32
+
33
+
let cmd_check t1s t2s rep =
34
+
match (Syntax.parse_result t1s, Syntax.parse_result t2s) with
35
+
| Error m, _ | _, Error m ->
36
+
Printf.printf "PARSE-ERROR: %s\n" m;
37
+
exit 2
38
+
| Ok t1, Ok t2 ->
39
+
List.iter
40
+
(fun r ->
41
+
let eq = check_with r t1 t2 in
42
+
Printf.printf "%s: %s\n" (rep_name r) (if eq then "EQUIV" else "NOT-EQUIV"))
43
+
(reps_of_string rep)
44
+
45
+
let cmd_corpus path =
46
+
let entries = Json_io.load_corpus path in
47
+
let failures = ref 0 in
48
+
List.iter
49
+
(fun (e : Json_io.corpus_entry) ->
50
+
let results =
51
+
List.map (fun r -> (r, check_with r e.t1 e.t2))
52
+
[ `Named; `Debruijn; `Ln; `Subst ]
53
+
in
54
+
List.iter
55
+
(fun (r, got) ->
56
+
match e.expected with
57
+
| Some exp when got <> exp ->
58
+
incr failures;
59
+
Printf.printf "FAIL %s [%s]: expected %s got %s\n" e.name
60
+
(rep_name r)
61
+
(if exp then "EQUIV" else "NOT-EQUIV")
62
+
(if got then "EQUIV" else "NOT-EQUIV")
63
+
| _ -> ())
64
+
results;
65
+
let agree =
66
+
match results with
67
+
| (_, a) :: tl -> List.for_all (fun (_, b) -> b = a) tl
68
+
| [] -> true
69
+
in
70
+
if not agree then begin
71
+
incr failures;
72
+
let rs =
73
+
String.concat ", "
74
+
(List.map (fun (r, g) -> rep_name r ^ "=" ^ string_of_bool g) results)
75
+
in
76
+
Printf.printf "DISAGREE %s: %s\n" e.name rs
77
+
end)
78
+
entries;
79
+
if !failures > 0 then begin
80
+
Printf.printf "%d failure(s)\n" !failures;
81
+
exit 1
82
+
end
83
+
else Printf.printf "corpus: %d entries, 0 failures\n" (List.length entries)
84
+
85
+
let now_us () = int_of_float (Unix.gettimeofday () *. 1e6)
86
+
87
+
let median arr =
88
+
Array.sort compare arr;
89
+
arr.(Array.length arr / 2)
90
+
91
+
type bench_result = {
92
+
alpha_us : int;
93
+
norm_us : int;
94
+
traversals : int;
95
+
max_depth : int;
96
+
}
97
+
98
+
let json_escape s =
99
+
let b = Buffer.create (String.length s + 2) in
100
+
String.iter
101
+
(function
102
+
| '"' -> Buffer.add_string b "\\\""
103
+
| '\\' -> Buffer.add_string b "\\\\"
104
+
| '\n' -> Buffer.add_string b "\\n"
105
+
| '\r' -> Buffer.add_string b "\\r"
106
+
| '\t' -> Buffer.add_string b "\\t"
107
+
| c -> Buffer.add_char b c)
108
+
s;
109
+
Buffer.contents b
110
+
111
+
let write_results path impl reps =
112
+
let oc = open_out_bin path in
113
+
Fun.protect
114
+
~finally:(fun () -> close_out_noerr oc)
115
+
(fun () ->
116
+
Printf.fprintf oc "{\"%s\":{" (json_escape impl);
117
+
reps
118
+
|> List.iteri (fun ri (rep, benches) ->
119
+
if ri > 0 then output_char oc ',';
120
+
Printf.fprintf oc "\"%s\":{" (json_escape rep);
121
+
benches
122
+
|> List.iteri (fun bi (name, r) ->
123
+
if bi > 0 then output_char oc ',';
124
+
Printf.fprintf oc
125
+
"\"%s\":{\"alpha_us\":%d,\"norm_us\":%d,\"traversals\":%d,\"max_depth\":%d}"
126
+
(json_escape name) r.alpha_us r.norm_us r.traversals
127
+
r.max_depth);
128
+
output_char oc '}');
129
+
output_string oc "}}")
130
+
131
+
let bench_rep rep t1 t2 iters =
132
+
let alpha_ts = Array.make iters 0 in
133
+
let norm_ts = Array.make iters 0 in
134
+
let trav = ref 0 in
135
+
let depth = ref 0 in
136
+
for i = 0 to iters - 1 do
137
+
let t0 = now_us () in
138
+
let (r, c, d) =
139
+
match rep with
140
+
| `Named -> Named.alpha_equivalent_counted t1 t2
141
+
| `Debruijn ->
142
+
Debruijn.alpha_equivalent_counted
143
+
(Debruijn.convert_from_named t1)
144
+
(Debruijn.convert_from_named t2)
145
+
| `Ln ->
146
+
Locally_nameless.alpha_equivalent_counted
147
+
(Locally_nameless.convert_from_named t1)
148
+
(Locally_nameless.convert_from_named t2)
149
+
| `Subst ->
150
+
Explicit_subst.alpha_equivalent_counted
151
+
(Explicit_subst.convert_from_named t1)
152
+
(Explicit_subst.convert_from_named t2)
153
+
in
154
+
alpha_ts.(i) <- now_us () - t0;
155
+
ignore r;
156
+
if c > !trav then trav := c;
157
+
if d > !depth then depth := d;
158
+
let t0 = now_us () in
159
+
let (_, c, d) =
160
+
let drop (x, c, d) = (ignore x, c, d) in
161
+
match rep with
162
+
| `Named -> drop (Named.normalise_counted t1)
163
+
| `Debruijn ->
164
+
drop (Debruijn.normalise_counted (Debruijn.convert_from_named t1))
165
+
| `Ln ->
166
+
drop
167
+
(Locally_nameless.normalise_counted
168
+
(Locally_nameless.convert_from_named t1))
169
+
| `Subst ->
170
+
drop
171
+
(Explicit_subst.normalise_counted
172
+
(Explicit_subst.convert_from_named t1))
173
+
in
174
+
norm_ts.(i) <- now_us () - t0;
175
+
if c > !trav then trav := c;
176
+
if d > !depth then depth := d
177
+
done;
178
+
{
179
+
alpha_us = median alpha_ts;
180
+
norm_us = median norm_ts;
181
+
traversals = !trav;
182
+
max_depth = !depth;
183
+
}
184
+
185
+
let cmd_bench path iters out_path =
186
+
let benches = Json_io.load_bench path in
187
+
let reps = [ `Named; `Debruijn; `Ln; `Subst ] in
188
+
let pair_for name t =
189
+
if Filename.check_suffix name "-a" then
190
+
let base = String.sub name 0 (String.length name - 2) in
191
+
match List.assoc_opt (base ^ "-b") benches with Some other -> other | None -> t
192
+
else t
193
+
in
194
+
let rep_json =
195
+
List.map
196
+
(fun rep ->
197
+
let bench_json =
198
+
List.map
199
+
(fun (name, t) ->
200
+
let other = pair_for name t in
201
+
(name, bench_rep rep t other iters))
202
+
benches
203
+
in
204
+
(rep_name rep, bench_json))
205
+
reps
206
+
in
207
+
write_results out_path "ocaml" rep_json;
208
+
Printf.printf "bench: wrote %s\n" out_path
209
+
210
+
let () =
211
+
let argv = Sys.argv in
212
+
let argc = Array.length argv in
213
+
if argc < 2 then begin
214
+
prerr_endline "usage: ego check <t1> <t2> [-r rep] | ego corpus <file> | ego bench <file> [--iters N] [--out file]";
215
+
exit 2
216
+
end;
217
+
match argv.(1) with
218
+
| "check" ->
219
+
let rep = ref "named" in
220
+
let terms = ref [] in
221
+
let i = ref 2 in
222
+
while !i < argc do
223
+
(match argv.(!i) with
224
+
| "-r" ->
225
+
incr i;
226
+
rep := argv.(!i)
227
+
| s -> terms := s :: !terms);
228
+
incr i
229
+
done;
230
+
(match List.rev !terms with
231
+
| [ t1; t2 ] -> cmd_check t1 t2 !rep
232
+
| _ ->
233
+
prerr_endline "check requires exactly two terms";
234
+
exit 2)
235
+
| "corpus" ->
236
+
if argc < 3 then begin
237
+
prerr_endline "corpus requires a file";
238
+
exit 2
239
+
end;
240
+
cmd_corpus argv.(2)
241
+
| "bench" ->
242
+
let iters = ref 5 in
243
+
let out = ref "results.json" in
244
+
let file = ref None in
245
+
let i = ref 2 in
246
+
while !i < argc do
247
+
(match argv.(!i) with
248
+
| "--iters" ->
249
+
incr i;
250
+
iters := int_of_string argv.(!i)
251
+
| "--out" ->
252
+
incr i;
253
+
out := argv.(!i)
254
+
| s -> file := Some s);
255
+
incr i
256
+
done;
257
+
(match !file with
258
+
| Some f -> cmd_bench f !iters !out
259
+
| None ->
260
+
prerr_endline "bench requires a file";
261
+
exit 2)
262
+
| _ ->
263
+
prerr_endline "unknown command";
264
+
exit 2
+160
ocaml/lib/debruijn.ml
+160
ocaml/lib/debruijn.ml
···
1
+
type t =
2
+
| Var of int
3
+
| Free of string
4
+
| Lam of t
5
+
| App of t * t
6
+
7
+
module SSet = Set.Make (String)
8
+
9
+
exception Unbound_index of int
10
+
11
+
let rec free_variables = function
12
+
| Var _ -> SSet.empty
13
+
| Free x -> SSet.singleton x
14
+
| Lam b -> free_variables b
15
+
| App (f, a) -> SSet.union (free_variables f) (free_variables a)
16
+
17
+
let free_variable_list t = SSet.elements (free_variables t)
18
+
19
+
let rec pretty = function
20
+
| Var i -> "#" ^ string_of_int i
21
+
| Free x -> x
22
+
| Lam b -> "\\. " ^ pretty b
23
+
| App (f, a) ->
24
+
let pf =
25
+
match f with Var _ | Free _ | App _ -> pretty f | _ -> "(" ^ pretty f ^ ")"
26
+
in
27
+
let pa =
28
+
match a with Var _ | Free _ -> pretty a | _ -> "(" ^ pretty a ^ ")"
29
+
in
30
+
pf ^ " " ^ pa
31
+
32
+
let rec shift cutoff amount t =
33
+
match t with
34
+
| Var i -> if i >= cutoff then Var (i + amount) else Var i
35
+
| Free x -> Free x
36
+
| Lam b -> Lam (shift (cutoff + 1) amount b)
37
+
| App (f, a) -> App (shift cutoff amount f, shift cutoff amount a)
38
+
39
+
let rec subst j s = function
40
+
| Var i ->
41
+
if i = j then s else if i > j then Var (i - 1) else Var i
42
+
| Free x -> Free x
43
+
| Lam b -> Lam (subst (j + 1) (shift 0 1 s) b)
44
+
| App (f, a) -> App (subst j s f, subst j s a)
45
+
46
+
let substitute j s body = subst j s body
47
+
48
+
let rec convert_from_named_depth env = function
49
+
| Named.Var x -> begin
50
+
match List.assoc_opt x env with
51
+
| Some i -> Var i
52
+
| None -> Free x
53
+
end
54
+
| Named.Lam (x, b) -> Lam (convert_from_named_depth ((x, 0) :: List.map (fun (v, i) -> (v, i + 1)) env) b)
55
+
| Named.App (f, a) ->
56
+
App (convert_from_named_depth env f, convert_from_named_depth env a)
57
+
| Named.Subst (x, s, b) ->
58
+
let body = Named.substitute x s b in
59
+
convert_from_named_depth env body
60
+
61
+
let convert_from_named t = convert_from_named_depth [] t
62
+
63
+
let convert_to_named t =
64
+
let fv = free_variables t in
65
+
let fresh_avoid avoid base =
66
+
if not (List.mem base avoid) then base
67
+
else
68
+
let rec go i =
69
+
let cand = base ^ string_of_int i in
70
+
if List.mem cand avoid then go (i + 1) else cand
71
+
in
72
+
go 0
73
+
in
74
+
let rec go env = function
75
+
| Var i -> begin
76
+
match List.nth_opt env i with
77
+
| Some x -> Named.Var x
78
+
| None -> raise (Unbound_index i)
79
+
end
80
+
| Free x -> Named.Var x
81
+
| Lam b ->
82
+
let avoid = SSet.elements fv @ env in
83
+
let x = fresh_avoid avoid "v" in
84
+
Named.Lam (x, go (x :: env) b)
85
+
| App (f, a) -> Named.App (go env f, go env a)
86
+
in
87
+
go [] t
88
+
89
+
let is_value = function Lam _ -> true | _ -> false
90
+
91
+
let rec step = function
92
+
| App (Lam b, a) -> Some (subst 0 a b)
93
+
| App (f, a) when not (is_value f) -> begin
94
+
match step f with
95
+
| Some f' -> Some (App (f', a))
96
+
| None -> begin
97
+
match step a with Some a' -> Some (App (f, a')) | None -> None
98
+
end
99
+
end
100
+
| App (f, a) -> begin
101
+
match step a with Some a' -> Some (App (f, a')) | None -> None
102
+
end
103
+
| Lam b -> begin
104
+
match step b with Some b' -> Some (Lam b') | None -> None
105
+
end
106
+
| _ -> None
107
+
108
+
let step_limit = 10000
109
+
110
+
let normalise t =
111
+
let rec go n t =
112
+
if n >= step_limit then t
113
+
else match step t with Some t' -> go (n + 1) t' | None -> t
114
+
in
115
+
go 0 t
116
+
117
+
let normalise_counted t =
118
+
let count = ref 0 in
119
+
let maxd = ref 0 in
120
+
let rec walk d t =
121
+
incr count;
122
+
if d > !maxd then maxd := d;
123
+
match t with
124
+
| Var _ | Free _ -> ()
125
+
| Lam b -> walk (d + 1) b
126
+
| App (f, a) -> walk (d + 1) f; walk (d + 1) a
127
+
in
128
+
walk 0 t;
129
+
let rec go n t =
130
+
if n >= step_limit then t
131
+
else
132
+
match step t with
133
+
| Some t' -> walk 0 t'; go (n + 1) t'
134
+
| None -> t
135
+
in
136
+
(go 0 t, !count, !maxd)
137
+
138
+
let alpha_equivalent t1 t2 = normalise t1 = normalise t2
139
+
140
+
let rec well_scoped depth = function
141
+
| Var i -> i < depth
142
+
| Free _ -> true
143
+
| Lam b -> well_scoped (depth + 1) b
144
+
| App (f, a) -> well_scoped depth f && well_scoped depth a
145
+
146
+
let alpha_equivalent_counted t1 t2 =
147
+
let count = ref 0 in
148
+
let maxd = ref 0 in
149
+
let rec go d a b =
150
+
incr count;
151
+
if d > !maxd then maxd := d;
152
+
match (a, b) with
153
+
| Var i, Var j -> i = j
154
+
| Free x, Free y -> x = y
155
+
| Lam b1, Lam b2 -> go (d + 1) b1 b2
156
+
| App (f1, a1), App (f2, a2) -> go (d + 1) f1 f2 && go (d + 1) a1 a2
157
+
| _ -> false
158
+
in
159
+
let r = go 0 (normalise t1) (normalise t2) in
160
+
(r, !count, !maxd)
+23
ocaml/lib/debruijn.mli
+23
ocaml/lib/debruijn.mli
···
1
+
type t =
2
+
| Var of int
3
+
| Free of string
4
+
| Lam of t
5
+
| App of t * t
6
+
7
+
module SSet : Set.S with type elt = string
8
+
9
+
exception Unbound_index of int
10
+
11
+
val free_variables : t -> SSet.t
12
+
val free_variable_list : t -> string list
13
+
val pretty : t -> string
14
+
val shift : int -> int -> t -> t
15
+
val subst : int -> t -> t -> t
16
+
val substitute : int -> t -> t -> t
17
+
val convert_from_named : Named.t -> t
18
+
val convert_to_named : t -> Named.t
19
+
val alpha_equivalent : t -> t -> bool
20
+
val alpha_equivalent_counted : t -> t -> bool * int * int
21
+
val normalise : t -> t
22
+
val normalise_counted : t -> t * int * int
23
+
val well_scoped : int -> t -> bool
+186
ocaml/lib/explicit_subst.ml
+186
ocaml/lib/explicit_subst.ml
···
1
+
type t =
2
+
| Var of string
3
+
| Lam of string * t
4
+
| App of t * t
5
+
| Subst of string * t * t
6
+
7
+
module SSet = Set.Make (String)
8
+
9
+
let rec free_variables = function
10
+
| Var x -> SSet.singleton x
11
+
| Lam (x, b) -> SSet.remove x (free_variables b)
12
+
| App (f, a) -> SSet.union (free_variables f) (free_variables a)
13
+
| Subst (x, s, b) ->
14
+
let fv_b = free_variables b in
15
+
let fv_b' = SSet.remove x fv_b in
16
+
if SSet.mem x fv_b then SSet.union fv_b' (free_variables s) else fv_b'
17
+
18
+
let free_variable_list t = SSet.elements (free_variables t)
19
+
20
+
let rec pretty = function
21
+
| Var x -> x
22
+
| Lam (x, b) -> "\\" ^ x ^ ". " ^ pretty b
23
+
| App (f, a) ->
24
+
let pf =
25
+
match f with Var _ | App _ -> pretty f | _ -> "(" ^ pretty f ^ ")"
26
+
in
27
+
let pa = match a with Var _ -> pretty a | _ -> "(" ^ pretty a ^ ")" in
28
+
pf ^ " " ^ pa
29
+
| Subst (x, s, b) -> "[" ^ x ^ " := " ^ pretty s ^ "] " ^ pretty b
30
+
31
+
let fresh avoid base =
32
+
if not (SSet.mem base avoid) then base
33
+
else
34
+
let rec go i =
35
+
let cand = base ^ string_of_int i in
36
+
if SSet.mem cand avoid then go (i + 1) else cand
37
+
in
38
+
go 0
39
+
40
+
let rec rename old nw = function
41
+
| Var z -> if z = old then Var nw else Var z
42
+
| App (f, a) -> App (rename old nw f, rename old nw a)
43
+
| Lam (z, b) -> if z = old then Lam (z, b) else Lam (z, rename old nw b)
44
+
| Subst (z, u, b) ->
45
+
if z = old then Subst (z, rename old nw u, b)
46
+
else Subst (z, rename old nw u, rename old nw b)
47
+
48
+
let step_limit = 10000
49
+
50
+
let push_subst x s body =
51
+
let fv_s = free_variables s in
52
+
let rec go = function
53
+
| Var y -> if y = x then s else Var y
54
+
| App (t, u) -> App (go t, go u)
55
+
| Lam (y, b) ->
56
+
if y = x then Lam (y, b)
57
+
else if not (SSet.mem y fv_s) then Lam (y, go b)
58
+
else
59
+
let avoid =
60
+
SSet.union fv_s
61
+
(SSet.union (free_variables b) (free_variables s))
62
+
in
63
+
let y' = fresh avoid y in
64
+
Lam (y', go (rename y y' b))
65
+
| Subst (y, u, b) ->
66
+
if y = x then Subst (y, go u, b)
67
+
else if not (SSet.mem y fv_s) then Subst (y, go u, go b)
68
+
else
69
+
let avoid =
70
+
SSet.union fv_s
71
+
(SSet.union (free_variables b) (free_variables s))
72
+
in
73
+
let y' = fresh avoid y in
74
+
Subst (y', go u, go (rename y y' b))
75
+
in
76
+
go body
77
+
78
+
let rec reduce = function
79
+
| Var x -> Var x
80
+
| Lam (x, b) -> Lam (x, reduce b)
81
+
| App (f, a) -> begin
82
+
let f' = reduce f in
83
+
let a' = reduce a in
84
+
match f' with Lam (x, b) -> reduce (push_subst x a' b) | _ -> App (f', a')
85
+
end
86
+
| Subst (x, s, b) -> reduce (push_subst x (reduce s) b)
87
+
88
+
let normalise t =
89
+
let rec go n t =
90
+
if n >= step_limit then t
91
+
else
92
+
let t' = reduce t in
93
+
if t' = t then t else go (n + 1) t'
94
+
in
95
+
go 0 t
96
+
97
+
let rec to_named = function
98
+
| Var x -> Named.Var x
99
+
| Lam (x, b) -> Named.Lam (x, to_named b)
100
+
| App (f, a) -> Named.App (to_named f, to_named a)
101
+
| Subst (x, s, b) -> Named.Subst (x, to_named s, to_named b)
102
+
103
+
let rec of_named = function
104
+
| Named.Var x -> Var x
105
+
| Named.Lam (x, b) -> Lam (x, of_named b)
106
+
| Named.App (f, a) -> App (of_named f, of_named a)
107
+
| Named.Subst (x, s, b) -> Subst (x, of_named s, of_named b)
108
+
109
+
let alpha_equivalent t1 t2 =
110
+
Named.alpha_equivalent (to_named (normalise t1)) (to_named (normalise t2))
111
+
112
+
let alpha_equivalent_susp t1 t2 =
113
+
let rec go d e1 e2 a b =
114
+
match (a, b) with
115
+
| Var x, Var y -> begin
116
+
match (List.assoc_opt x e1, List.assoc_opt y e2) with
117
+
| Some i, Some j -> i = j
118
+
| None, None -> x = y
119
+
| _ -> false
120
+
end
121
+
| Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
122
+
| App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
123
+
| Subst (x, s1, b1), Subst (y, s2, b2) ->
124
+
go d e1 e2 s1 s2
125
+
&& go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
126
+
| Subst _, _ -> go d e1 e2 (normalise a) b
127
+
| _, Subst _ -> go d e1 e2 a (normalise b)
128
+
| _ -> false
129
+
in
130
+
go 0 [] [] t1 t2
131
+
132
+
let alpha_equivalent_counted t1 t2 =
133
+
let count = ref 0 in
134
+
let maxd = ref 0 in
135
+
let rec go d e1 e2 a b =
136
+
incr count;
137
+
if d > !maxd then maxd := d;
138
+
match (a, b) with
139
+
| Var x, Var y -> begin
140
+
match (List.assoc_opt x e1, List.assoc_opt y e2) with
141
+
| Some i, Some j -> i = j
142
+
| None, None -> x = y
143
+
| _ -> false
144
+
end
145
+
| Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
146
+
| App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
147
+
| Subst (x, s1, b1), Subst (y, s2, b2) ->
148
+
go d e1 e2 s1 s2
149
+
&& go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
150
+
| Subst _, _ ->
151
+
let a' = normalise a in
152
+
if a' = a then false else go d e1 e2 a' b
153
+
| _, Subst _ ->
154
+
let b' = normalise b in
155
+
if b' = b then false else go d e1 e2 a b'
156
+
| _ -> false
157
+
in
158
+
let r = go 0 [] [] t1 t2 in
159
+
(r, !count, !maxd)
160
+
161
+
let normalise_counted t =
162
+
let count = ref 0 in
163
+
let maxd = ref 0 in
164
+
let rec walk d t =
165
+
incr count;
166
+
if d > !maxd then maxd := d;
167
+
match t with
168
+
| Var _ -> ()
169
+
| Lam (_, b) -> walk (d + 1) b
170
+
| App (f, a) -> walk (d + 1) f; walk (d + 1) a
171
+
| Subst (_, s, b) -> walk (d + 1) s; walk (d + 1) b
172
+
in
173
+
walk 0 t;
174
+
let rec go n t =
175
+
if n >= step_limit then t
176
+
else
177
+
let t' = reduce t in
178
+
walk 0 t';
179
+
if t' = t then t else go (n + 1) t'
180
+
in
181
+
(go 0 t, !count, !maxd)
182
+
183
+
let substitute x s body = Subst (x, s, body)
184
+
185
+
let convert_from_named t = of_named t
186
+
let convert_to_named t = to_named (normalise t)
+22
ocaml/lib/explicit_subst.mli
+22
ocaml/lib/explicit_subst.mli
···
1
+
type t =
2
+
| Var of string
3
+
| Lam of string * t
4
+
| App of t * t
5
+
| Subst of string * t * t
6
+
7
+
module SSet : Set.S with type elt = string
8
+
9
+
val free_variables : t -> SSet.t
10
+
val free_variable_list : t -> string list
11
+
val pretty : t -> string
12
+
val push_subst : string -> t -> t -> t
13
+
val normalise : t -> t
14
+
val normalise_counted : t -> t * int * int
15
+
val to_named : t -> Named.t
16
+
val of_named : Named.t -> t
17
+
val alpha_equivalent : t -> t -> bool
18
+
val alpha_equivalent_susp : t -> t -> bool
19
+
val alpha_equivalent_counted : t -> t -> bool * int * int
20
+
val substitute : string -> t -> t -> t
21
+
val convert_from_named : Named.t -> t
22
+
val convert_to_named : t -> Named.t
+186
ocaml/lib/json_io.ml
+186
ocaml/lib/json_io.ml
···
1
+
exception Json_error of string
2
+
3
+
type json =
4
+
| JObject of (string * json) list
5
+
| JArray of json list
6
+
| JString of string
7
+
| JBool of bool
8
+
| JNull
9
+
10
+
let read_file path =
11
+
let ic = open_in_bin path in
12
+
Fun.protect
13
+
~finally:(fun () -> close_in_noerr ic)
14
+
(fun () ->
15
+
let n = in_channel_length ic in
16
+
really_input_string ic n)
17
+
18
+
let parse_json s =
19
+
let n = String.length s in
20
+
let i = ref 0 in
21
+
let error m = raise (Json_error (m ^ " at byte " ^ string_of_int !i)) in
22
+
let ws () =
23
+
while !i < n && match s.[!i] with ' ' | '\n' | '\r' | '\t' -> true | _ -> false do
24
+
incr i
25
+
done
26
+
in
27
+
let expect c =
28
+
ws ();
29
+
if !i >= n || s.[!i] <> c then error ("expected " ^ String.make 1 c);
30
+
incr i
31
+
in
32
+
let parse_lit lit v =
33
+
let len = String.length lit in
34
+
if !i + len <= n && String.sub s !i len = lit then (i := !i + len; v)
35
+
else error ("expected " ^ lit)
36
+
in
37
+
let parse_string () =
38
+
expect '"';
39
+
let b = Buffer.create 16 in
40
+
let rec loop () =
41
+
if !i >= n then error "unterminated string";
42
+
match s.[!i] with
43
+
| '"' -> incr i; JString (Buffer.contents b)
44
+
| '\\' ->
45
+
incr i;
46
+
if !i >= n then error "unterminated escape";
47
+
let c =
48
+
match s.[!i] with
49
+
| '"' -> '"'
50
+
| '\\' -> '\\'
51
+
| '/' -> '/'
52
+
| 'b' -> '\b'
53
+
| 'f' -> '\012'
54
+
| 'n' -> '\n'
55
+
| 'r' -> '\r'
56
+
| 't' -> '\t'
57
+
| _ -> error "unsupported string escape"
58
+
in
59
+
Buffer.add_char b c;
60
+
incr i;
61
+
loop ()
62
+
| c ->
63
+
Buffer.add_char b c;
64
+
incr i;
65
+
loop ()
66
+
in
67
+
loop ()
68
+
in
69
+
let rec value () =
70
+
ws ();
71
+
if !i >= n then error "expected value";
72
+
match s.[!i] with
73
+
| '{' -> obj ()
74
+
| '[' -> arr ()
75
+
| '"' -> parse_string ()
76
+
| 't' -> parse_lit "true" (JBool true)
77
+
| 'f' -> parse_lit "false" (JBool false)
78
+
| 'n' -> parse_lit "null" JNull
79
+
| _ -> error "unexpected value"
80
+
and obj () =
81
+
expect '{';
82
+
ws ();
83
+
if !i < n && s.[!i] = '}' then (incr i; JObject [])
84
+
else
85
+
let rec fields acc =
86
+
let key =
87
+
match parse_string () with JString k -> k | _ -> assert false
88
+
in
89
+
expect ':';
90
+
let v = value () in
91
+
ws ();
92
+
if !i < n && s.[!i] = ',' then (incr i; fields ((key, v) :: acc))
93
+
else if !i < n && s.[!i] = '}' then (incr i; JObject (List.rev ((key, v) :: acc)))
94
+
else error "expected ',' or '}'"
95
+
in
96
+
fields []
97
+
and arr () =
98
+
expect '[';
99
+
ws ();
100
+
if !i < n && s.[!i] = ']' then (incr i; JArray [])
101
+
else
102
+
let rec elems acc =
103
+
let v = value () in
104
+
ws ();
105
+
if !i < n && s.[!i] = ',' then (incr i; elems (v :: acc))
106
+
else if !i < n && s.[!i] = ']' then (incr i; JArray (List.rev (v :: acc)))
107
+
else error "expected ',' or ']'"
108
+
in
109
+
elems []
110
+
in
111
+
let v = value () in
112
+
ws ();
113
+
if !i <> n then error "trailing input";
114
+
v
115
+
116
+
let member k = function
117
+
| JObject xs -> begin
118
+
match List.assoc_opt k xs with
119
+
| Some v -> v
120
+
| None -> raise (Json_error ("missing field: " ^ k))
121
+
end
122
+
| _ -> raise (Json_error "expected object")
123
+
124
+
let to_string = function
125
+
| JString s -> s
126
+
| _ -> raise (Json_error "expected string")
127
+
128
+
let to_list = function
129
+
| JArray xs -> xs
130
+
| _ -> raise (Json_error "expected array")
131
+
132
+
let to_assoc = function
133
+
| JObject xs -> xs
134
+
| _ -> raise (Json_error "expected object")
135
+
136
+
let rec named_of_json j =
137
+
match member "tag" j |> to_string with
138
+
| "Var" -> Named.Var (member "name" j |> to_string)
139
+
| "Lam" ->
140
+
Named.Lam (member "param" j |> to_string, named_of_json (member "body" j))
141
+
| "App" ->
142
+
Named.App (named_of_json (member "fun" j), named_of_json (member "arg" j))
143
+
| "Subst" ->
144
+
Named.Subst
145
+
( member "var" j |> to_string,
146
+
named_of_json (member "repl" j),
147
+
named_of_json (member "body" j) )
148
+
| t -> raise (Json_error ("unknown tag: " ^ t))
149
+
150
+
let rec json_of_named = function
151
+
| Named.Var x -> JObject [ ("tag", JString "Var"); ("name", JString x) ]
152
+
| Named.Lam (x, b) ->
153
+
JObject [ ("tag", JString "Lam"); ("param", JString x); ("body", json_of_named b) ]
154
+
| Named.App (f, a) ->
155
+
JObject [ ("tag", JString "App"); ("fun", json_of_named f); ("arg", json_of_named a) ]
156
+
| Named.Subst (x, s, b) ->
157
+
JObject
158
+
[ ("tag", JString "Subst");
159
+
("var", JString x);
160
+
("repl", json_of_named s);
161
+
("body", json_of_named b) ]
162
+
163
+
type corpus_entry = {
164
+
name : string;
165
+
t1 : Named.t;
166
+
t2 : Named.t;
167
+
expected : bool option;
168
+
}
169
+
170
+
let load_corpus path =
171
+
parse_json (read_file path) |> to_list
172
+
|> List.map (fun e ->
173
+
{
174
+
name = member "name" e |> to_string;
175
+
t1 = named_of_json (member "t1" e);
176
+
t2 = named_of_json (member "t2" e);
177
+
expected =
178
+
(match member "expected" e with
179
+
| JNull -> None
180
+
| JBool b -> Some b
181
+
| _ -> raise (Json_error "expected must be bool or null"));
182
+
})
183
+
184
+
let load_bench path =
185
+
parse_json (read_file path) |> to_assoc
186
+
|> List.map (fun (k, v) -> (k, named_of_json v))
+196
ocaml/lib/locally_nameless.ml
+196
ocaml/lib/locally_nameless.ml
···
1
+
type t =
2
+
| BVar of int
3
+
| FVar of string
4
+
| Lam of t
5
+
| App of t * t
6
+
7
+
module SSet = Set.Make (String)
8
+
9
+
exception Not_locally_closed
10
+
11
+
let rec free_variables = function
12
+
| BVar _ -> SSet.empty
13
+
| FVar x -> SSet.singleton x
14
+
| Lam b -> free_variables b
15
+
| App (f, a) -> SSet.union (free_variables f) (free_variables a)
16
+
17
+
let free_variable_list t = SSet.elements (free_variables t)
18
+
19
+
let rec pretty = function
20
+
| BVar i -> "#" ^ string_of_int i
21
+
| FVar x -> x
22
+
| Lam b -> "\\. " ^ pretty b
23
+
| App (f, a) ->
24
+
let pf =
25
+
match f with
26
+
| BVar _ | FVar _ | App _ -> pretty f
27
+
| _ -> "(" ^ pretty f ^ ")"
28
+
in
29
+
let pa =
30
+
match a with BVar _ | FVar _ -> pretty a | _ -> "(" ^ pretty a ^ ")"
31
+
in
32
+
pf ^ " " ^ pa
33
+
34
+
let rec open_at k x = function
35
+
| BVar i -> if i = k then FVar x else BVar i
36
+
| FVar y -> FVar y
37
+
| Lam b -> Lam (open_at (k + 1) x b)
38
+
| App (f, a) -> App (open_at k x f, open_at k x a)
39
+
40
+
let open_top t x = open_at 0 x t
41
+
42
+
let rec close_at k x = function
43
+
| BVar i -> BVar i
44
+
| FVar y -> if y = x then BVar k else FVar y
45
+
| Lam b -> Lam (close_at (k + 1) x b)
46
+
| App (f, a) -> App (close_at k x f, close_at k x a)
47
+
48
+
let close_top t x = close_at 0 x t
49
+
50
+
let rec lc_at depth = function
51
+
| BVar i -> i < depth
52
+
| FVar _ -> true
53
+
| Lam b -> lc_at (depth + 1) b
54
+
| App (f, a) -> lc_at depth f && lc_at depth a
55
+
56
+
let lc t = lc_at 0 t
57
+
58
+
let require_lc t =
59
+
if not (lc t) then raise Not_locally_closed
60
+
61
+
let rec subst_bvar j s = function
62
+
| BVar i -> if i = j then s else if i > j then BVar (i - 1) else BVar i
63
+
| FVar x -> FVar x
64
+
| Lam b -> Lam (subst_bvar (j + 1) (shift s) b)
65
+
| App (f, a) -> App (subst_bvar j s f, subst_bvar j s a)
66
+
67
+
and shift t =
68
+
let rec go cutoff = function
69
+
| BVar i -> if i >= cutoff then BVar (i + 1) else BVar i
70
+
| FVar x -> FVar x
71
+
| Lam b -> Lam (go (cutoff + 1) b)
72
+
| App (f, a) -> App (go cutoff f, go cutoff a)
73
+
in
74
+
go 0 t
75
+
76
+
let rec subst_fvar x s = function
77
+
| BVar i -> BVar i
78
+
| FVar y -> if y = x then s else FVar y
79
+
| Lam b -> Lam (subst_fvar x s b)
80
+
| App (f, a) -> App (subst_fvar x s f, subst_fvar x s a)
81
+
82
+
let convert_from_named t =
83
+
let rec go env = function
84
+
| Named.Var x -> begin
85
+
match List.assoc_opt x env with
86
+
| Some i -> BVar i
87
+
| None -> FVar x
88
+
end
89
+
| Named.Lam (x, b) ->
90
+
Lam (go ((x, 0) :: List.map (fun (v, i) -> (v, i + 1)) env) b)
91
+
| Named.App (f, a) -> App (go env f, go env a)
92
+
| Named.Subst (x, s, b) ->
93
+
go env (Named.substitute x s b)
94
+
in
95
+
go [] t
96
+
97
+
let convert_to_named t =
98
+
require_lc t;
99
+
let fv = free_variables t in
100
+
let fresh_avoid avoid base =
101
+
if not (SSet.mem base avoid) then base
102
+
else
103
+
let rec go i =
104
+
let cand = base ^ string_of_int i in
105
+
if SSet.mem cand avoid then go (i + 1) else cand
106
+
in
107
+
go 0
108
+
in
109
+
let rec go env = function
110
+
| BVar i -> Named.Var (List.nth env i)
111
+
| FVar x -> Named.Var x
112
+
| Lam b ->
113
+
let avoid =
114
+
List.fold_left (fun a x -> SSet.add x a) fv env
115
+
in
116
+
let x = fresh_avoid avoid "v" in
117
+
Named.Lam (x, go (x :: env) b)
118
+
| App (f, a) -> Named.App (go env f, go env a)
119
+
in
120
+
go [] t
121
+
122
+
let is_value = function Lam _ -> true | _ -> false
123
+
124
+
let rec step = function
125
+
| App (Lam b, a) -> Some (subst_bvar 0 a b)
126
+
| App (f, a) when not (is_value f) -> begin
127
+
match step f with
128
+
| Some f' -> Some (App (f', a))
129
+
| None -> begin
130
+
match step a with Some a' -> Some (App (f, a')) | None -> None
131
+
end
132
+
end
133
+
| App (f, a) -> begin
134
+
match step a with Some a' -> Some (App (f, a')) | None -> None
135
+
end
136
+
| Lam b -> begin
137
+
match step b with Some b' -> Some (Lam b') | None -> None
138
+
end
139
+
| _ -> None
140
+
141
+
let step_limit = 10000
142
+
143
+
let normalise t =
144
+
require_lc t;
145
+
let rec go n t =
146
+
if n >= step_limit then t
147
+
else match step t with Some t' -> go (n + 1) t' | None -> t
148
+
in
149
+
go 0 t
150
+
151
+
let normalise_counted t =
152
+
require_lc t;
153
+
let count = ref 0 in
154
+
let maxd = ref 0 in
155
+
let rec walk d t =
156
+
incr count;
157
+
if d > !maxd then maxd := d;
158
+
match t with
159
+
| BVar _ | FVar _ -> ()
160
+
| Lam b -> walk (d + 1) b
161
+
| App (f, a) -> walk (d + 1) f; walk (d + 1) a
162
+
in
163
+
walk 0 t;
164
+
let rec go n t =
165
+
if n >= step_limit then t
166
+
else
167
+
match step t with
168
+
| Some t' -> walk 0 t'; go (n + 1) t'
169
+
| None -> t
170
+
in
171
+
(go 0 t, !count, !maxd)
172
+
173
+
let substitute x s body = subst_fvar x s body
174
+
175
+
let alpha_equivalent t1 t2 =
176
+
require_lc t1;
177
+
require_lc t2;
178
+
normalise t1 = normalise t2
179
+
180
+
let alpha_equivalent_counted t1 t2 =
181
+
require_lc t1;
182
+
require_lc t2;
183
+
let count = ref 0 in
184
+
let maxd = ref 0 in
185
+
let rec go d a b =
186
+
incr count;
187
+
if d > !maxd then maxd := d;
188
+
match (a, b) with
189
+
| BVar i, BVar j -> i = j
190
+
| FVar x, FVar y -> x = y
191
+
| Lam b1, Lam b2 -> go (d + 1) b1 b2
192
+
| App (f1, a1), App (f2, a2) -> go (d + 1) f1 f2 && go (d + 1) a1 a2
193
+
| _ -> false
194
+
in
195
+
let r = go 0 (normalise t1) (normalise t2) in
196
+
(r, !count, !maxd)
+28
ocaml/lib/locally_nameless.mli
+28
ocaml/lib/locally_nameless.mli
···
1
+
type t =
2
+
| BVar of int
3
+
| FVar of string
4
+
| Lam of t
5
+
| App of t * t
6
+
7
+
module SSet : Set.S with type elt = string
8
+
9
+
exception Not_locally_closed
10
+
11
+
val free_variables : t -> SSet.t
12
+
val free_variable_list : t -> string list
13
+
val pretty : t -> string
14
+
val open_at : int -> string -> t -> t
15
+
val open_top : t -> string -> t
16
+
val close_at : int -> string -> t -> t
17
+
val close_top : t -> string -> t
18
+
val lc : t -> bool
19
+
val require_lc : t -> unit
20
+
val subst_bvar : int -> t -> t -> t
21
+
val subst_fvar : string -> t -> t -> t
22
+
val substitute : string -> t -> t -> t
23
+
val convert_from_named : Named.t -> t
24
+
val convert_to_named : t -> Named.t
25
+
val alpha_equivalent : t -> t -> bool
26
+
val alpha_equivalent_counted : t -> t -> bool * int * int
27
+
val normalise : t -> t
28
+
val normalise_counted : t -> t * int * int
+168
ocaml/lib/named.ml
+168
ocaml/lib/named.ml
···
1
+
type t =
2
+
| Var of string
3
+
| Lam of string * t
4
+
| App of t * t
5
+
| Subst of string * t * t
6
+
7
+
module SSet = Set.Make (String)
8
+
9
+
let rec free_variables = function
10
+
| Var x -> SSet.singleton x
11
+
| Lam (x, b) -> SSet.remove x (free_variables b)
12
+
| App (f, a) -> SSet.union (free_variables f) (free_variables a)
13
+
| Subst (x, s, b) ->
14
+
let fv_b = free_variables b in
15
+
let fv_b' = SSet.remove x fv_b in
16
+
if SSet.mem x fv_b then SSet.union fv_b' (free_variables s) else fv_b'
17
+
18
+
let free_variable_list t = SSet.elements (free_variables t)
19
+
20
+
let rec pretty = function
21
+
| Var x -> x
22
+
| Lam (x, b) -> "\\" ^ x ^ ". " ^ pretty b
23
+
| App (f, a) ->
24
+
let pf =
25
+
match f with Var _ | App _ -> pretty f | _ -> "(" ^ pretty f ^ ")"
26
+
in
27
+
let pa = match a with Var _ -> pretty a | _ -> "(" ^ pretty a ^ ")" in
28
+
pf ^ " " ^ pa
29
+
| Subst (x, s, b) -> "[" ^ x ^ " := " ^ pretty s ^ "] " ^ pretty b
30
+
31
+
let fresh_name avoid base =
32
+
if not (SSet.mem base avoid) then base
33
+
else
34
+
let rec go i =
35
+
let cand = base ^ string_of_int i in
36
+
if SSet.mem cand avoid then go (i + 1) else cand
37
+
in
38
+
go 0
39
+
40
+
let rename old nw t =
41
+
let rec ren = function
42
+
| Var z -> if z = old then Var nw else Var z
43
+
| App (f, a) -> App (ren f, ren a)
44
+
| Lam (z, b) -> if z = old then Lam (z, b) else Lam (z, ren b)
45
+
| Subst (z, u, b) ->
46
+
if z = old then Subst (z, ren u, b) else Subst (z, ren u, ren b)
47
+
in
48
+
ren t
49
+
50
+
let substitute x s body =
51
+
let fv_s = free_variables s in
52
+
let fv_b = free_variables body in
53
+
let avoid0 = SSet.union fv_s fv_b in
54
+
let rec sub avoid = function
55
+
| Var y -> if y = x then s else Var y
56
+
| App (f, a) -> App (sub avoid f, sub avoid a)
57
+
| Lam (y, b) ->
58
+
if y = x then Lam (y, b)
59
+
else if (not (SSet.mem y fv_s)) || not (SSet.mem x (free_variables b)) then
60
+
Lam (y, sub avoid b)
61
+
else
62
+
let y' = fresh_name avoid y in
63
+
Lam (y', sub (SSet.add y' avoid) (rename y y' b))
64
+
| Subst (y, u, b) ->
65
+
if y = x then Subst (y, sub avoid u, b)
66
+
else if (not (SSet.mem y fv_s)) || not (SSet.mem x (free_variables b)) then
67
+
Subst (y, sub avoid u, sub avoid b)
68
+
else
69
+
let y' = fresh_name avoid y in
70
+
Subst (y', sub avoid u, sub (SSet.add y' avoid) (rename y y' b))
71
+
in
72
+
sub avoid0 body
73
+
74
+
let step_limit = 10000
75
+
76
+
let rec elim_subst = function
77
+
| Var x -> Var x
78
+
| Lam (x, b) -> Lam (x, elim_subst b)
79
+
| App (f, a) -> App (elim_subst f, elim_subst a)
80
+
| Subst (x, s, b) -> substitute x (elim_subst s) (elim_subst b)
81
+
82
+
let is_value = function Lam _ -> true | _ -> false
83
+
84
+
let rec step = function
85
+
| App (Lam (x, b), a) -> Some (substitute x a b)
86
+
| App (f, a) when not (is_value f) -> begin
87
+
match step f with
88
+
| Some f' -> Some (App (f', a))
89
+
| None -> begin
90
+
match step a with Some a' -> Some (App (f, a')) | None -> None
91
+
end
92
+
end
93
+
| App (f, a) -> begin
94
+
match step a with Some a' -> Some (App (f, a')) | None -> None
95
+
end
96
+
| Lam (x, b) -> begin
97
+
match step b with Some b' -> Some (Lam (x, b')) | None -> None
98
+
end
99
+
| _ -> None
100
+
101
+
let normalise t =
102
+
let t = elim_subst t in
103
+
let rec go n t =
104
+
if n >= step_limit then t
105
+
else match step t with Some t' -> go (n + 1) t' | None -> t
106
+
in
107
+
go 0 t
108
+
109
+
let normalise_counted t =
110
+
let count = ref 0 in
111
+
let maxd = ref 0 in
112
+
let rec walk d t =
113
+
incr count;
114
+
if d > !maxd then maxd := d;
115
+
match t with
116
+
| Var _ -> ()
117
+
| Lam (_, b) -> walk (d + 1) b
118
+
| App (f, a) -> walk (d + 1) f; walk (d + 1) a
119
+
| Subst (_, s, b) -> walk (d + 1) s; walk (d + 1) b
120
+
in
121
+
let t = elim_subst t in
122
+
walk 0 t;
123
+
let rec go n t =
124
+
if n >= step_limit then t
125
+
else
126
+
match step t with
127
+
| Some t' -> walk 0 t'; go (n + 1) t'
128
+
| None -> t
129
+
in
130
+
(go 0 t, !count, !maxd)
131
+
132
+
let convert_from_named t = t
133
+
let convert_to_named t = t
134
+
135
+
let alpha_equivalent t1 t2 =
136
+
let rec go d e1 e2 a b =
137
+
match (a, b) with
138
+
| Var x, Var y -> begin
139
+
match (List.assoc_opt x e1, List.assoc_opt y e2) with
140
+
| Some i, Some j -> i = j
141
+
| None, None -> x = y
142
+
| _ -> false
143
+
end
144
+
| Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
145
+
| App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
146
+
| _ -> false
147
+
in
148
+
go 0 [] [] (normalise t1) (normalise t2)
149
+
150
+
let alpha_equivalent_counted t1 t2 =
151
+
let count = ref 0 in
152
+
let maxd = ref 0 in
153
+
let rec go d e1 e2 a b =
154
+
incr count;
155
+
if d > !maxd then maxd := d;
156
+
match (a, b) with
157
+
| Var x, Var y -> begin
158
+
match (List.assoc_opt x e1, List.assoc_opt y e2) with
159
+
| Some i, Some j -> i = j
160
+
| None, None -> x = y
161
+
| _ -> false
162
+
end
163
+
| Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
164
+
| App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
165
+
| _ -> false
166
+
in
167
+
let r = go 0 [] [] (normalise t1) (normalise t2) in
168
+
(r, !count, !maxd)
+21
ocaml/lib/named.mli
+21
ocaml/lib/named.mli
···
1
+
type t =
2
+
| Var of string
3
+
| Lam of string * t
4
+
| App of t * t
5
+
| Subst of string * t * t
6
+
7
+
module SSet : Set.S with type elt = string
8
+
9
+
val free_variables : t -> SSet.t
10
+
val free_variable_list : t -> string list
11
+
val pretty : t -> string
12
+
val fresh_name : SSet.t -> string -> string
13
+
val substitute : string -> t -> t -> t
14
+
val alpha_equivalent : t -> t -> bool
15
+
val alpha_equivalent_counted : t -> t -> bool * int * int
16
+
val normalise : t -> t
17
+
val normalise_counted : t -> t * int * int
18
+
val elim_subst : t -> t
19
+
val convert_from_named : t -> t
20
+
val convert_to_named : t -> t
21
+
val step_limit : int
+125
ocaml/lib/syntax.ml
+125
ocaml/lib/syntax.ml
···
1
+
type token =
2
+
| TBackslash
3
+
| TDot
4
+
| TLParen
5
+
| TRParen
6
+
| TLBrack
7
+
| TRBrack
8
+
| TColonEq
9
+
| TVar of string
10
+
11
+
exception Parse_error of string
12
+
13
+
let is_var_start c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
14
+
15
+
let is_var_char c =
16
+
is_var_start c || (c >= '0' && c <= '9') || c = '_' || c = '\'' || c = '-'
17
+
18
+
let lex s =
19
+
let n = String.length s in
20
+
let rec go i acc =
21
+
if i >= n then List.rev acc
22
+
else
23
+
match s.[i] with
24
+
| ' ' | '\t' | '\n' | '\r' -> go (i + 1) acc
25
+
| '\\' -> go (i + 1) (TBackslash :: acc)
26
+
| '.' -> go (i + 1) (TDot :: acc)
27
+
| '(' -> go (i + 1) (TLParen :: acc)
28
+
| ')' -> go (i + 1) (TRParen :: acc)
29
+
| '[' -> go (i + 1) (TLBrack :: acc)
30
+
| ']' -> go (i + 1) (TRBrack :: acc)
31
+
| ':' ->
32
+
if i + 1 < n && s.[i + 1] = '=' then go (i + 2) (TColonEq :: acc)
33
+
else raise (Parse_error ("unexpected ':' at position " ^ string_of_int i))
34
+
| c when is_var_start c ->
35
+
let j = ref (i + 1) in
36
+
while !j < n && is_var_char s.[!j] do
37
+
incr j
38
+
done;
39
+
go !j (TVar (String.sub s i (!j - i)) :: acc)
40
+
| c ->
41
+
raise
42
+
(Parse_error
43
+
(Printf.sprintf "unexpected character %C at position %d" c i))
44
+
in
45
+
go 0 []
46
+
47
+
let parse s =
48
+
let toks = Array.of_list (lex s) in
49
+
let n = Array.length toks in
50
+
let pos = ref 0 in
51
+
let peek () = if !pos < n then Some toks.(!pos) else None in
52
+
let next () =
53
+
let t = peek () in
54
+
incr pos;
55
+
t
56
+
in
57
+
let expect tok what =
58
+
match next () with
59
+
| Some t when t = tok -> ()
60
+
| _ -> raise (Parse_error ("expected " ^ what))
61
+
in
62
+
let starts_atom = function
63
+
| Some (TVar _) | Some TLParen | Some TBackslash | Some TLBrack -> true
64
+
| _ -> false
65
+
in
66
+
let rec term () =
67
+
match peek () with
68
+
| Some TBackslash -> lam ()
69
+
| Some TLBrack -> subst ()
70
+
| _ -> app ()
71
+
and lam () =
72
+
ignore (next ());
73
+
match next () with
74
+
| Some (TVar v) ->
75
+
expect TDot "'.'";
76
+
let body = term () in
77
+
Named.Lam (v, body)
78
+
| _ -> raise (Parse_error "expected variable after '\\'")
79
+
and subst () =
80
+
ignore (next ());
81
+
match next () with
82
+
| Some (TVar v) ->
83
+
expect TColonEq "':='";
84
+
let s = term () in
85
+
expect TRBrack "']'";
86
+
let body = term () in
87
+
Named.Subst (v, s, body)
88
+
| _ -> raise (Parse_error "expected variable after '['")
89
+
and app () =
90
+
let lhs = atom () in
91
+
let rec args lhs =
92
+
if starts_atom (peek ()) then args (Named.App (lhs, atom ())) else lhs
93
+
in
94
+
args lhs
95
+
and atom () =
96
+
match next () with
97
+
| Some (TVar v) -> Named.Var v
98
+
| Some TLParen ->
99
+
let t = term () in
100
+
expect TRParen "')'";
101
+
t
102
+
| Some TBackslash -> begin
103
+
match next () with
104
+
| Some (TVar v) ->
105
+
expect TDot "'.'";
106
+
Named.Lam (v, term ())
107
+
| _ -> raise (Parse_error "expected variable after '\\'")
108
+
end
109
+
| Some TLBrack -> begin
110
+
match next () with
111
+
| Some (TVar v) ->
112
+
expect TColonEq "':='";
113
+
let s = term () in
114
+
expect TRBrack "']'";
115
+
Named.Subst (v, s, term ())
116
+
| _ -> raise (Parse_error "expected variable after '['")
117
+
end
118
+
| _ -> raise (Parse_error "expected a term")
119
+
in
120
+
let t = term () in
121
+
if !pos <> n then raise (Parse_error "trailing input");
122
+
t
123
+
124
+
let parse_result s =
125
+
match parse s with t -> Ok t | exception Parse_error m -> Error m
+1
ocaml/results_ocaml.json
+1
ocaml/results_ocaml.json
···
1
+
{"ocaml":{"named":{"chain-small":{"alpha_us":4,"norm_us":1,"traversals":61,"max_depth":60},"apps-small":{"alpha_us":3,"norm_us":1,"traversals":121,"max_depth":60},"shadow-small":{"alpha_us":2,"norm_us":1,"traversals":61,"max_depth":60},"fv-small":{"alpha_us":3,"norm_us":1,"traversals":121,"max_depth":60},"shift-small":{"alpha_us":11,"norm_us":6,"traversals":13,"max_depth":12},"bigsubst-small":{"alpha_us":75,"norm_us":8,"traversals":141,"max_depth":80},"leaves-small-a":{"alpha_us":800,"norm_us":390,"traversals":181,"max_depth":120},"leaves-small-b":{"alpha_us":762,"norm_us":411,"traversals":181,"max_depth":120},"allbinders-small-a":{"alpha_us":4,"norm_us":1,"traversals":61,"max_depth":60},"allbinders-small-b":{"alpha_us":4,"norm_us":0,"traversals":61,"max_depth":60},"chain-medium":{"alpha_us":18,"norm_us":3,"traversals":251,"max_depth":250},"apps-medium":{"alpha_us":11,"norm_us":5,"traversals":501,"max_depth":250},"shadow-medium":{"alpha_us":8,"norm_us":3,"traversals":251,"max_depth":250},"fv-medium":{"alpha_us":10,"norm_us":5,"traversals":501,"max_depth":250},"shift-medium":{"alpha_us":207,"norm_us":98,"traversals":51,"max_depth":50},"bigsubst-medium":{"alpha_us":282,"norm_us":25,"traversals":521,"max_depth":270},"leaves-medium-a":{"alpha_us":20542,"norm_us":10567,"traversals":751,"max_depth":500},"leaves-medium-b":{"alpha_us":19814,"norm_us":9974,"traversals":751,"max_depth":500},"allbinders-medium-a":{"alpha_us":17,"norm_us":3,"traversals":251,"max_depth":250},"allbinders-medium-b":{"alpha_us":17,"norm_us":3,"traversals":251,"max_depth":250},"chain-large":{"alpha_us":72,"norm_us":11,"traversals":1001,"max_depth":1000},"apps-large":{"alpha_us":43,"norm_us":21,"traversals":2001,"max_depth":1000},"shadow-large":{"alpha_us":34,"norm_us":11,"traversals":1001,"max_depth":1000},"fv-large":{"alpha_us":43,"norm_us":22,"traversals":2001,"max_depth":1000},"shift-large":{"alpha_us":1829,"norm_us":867,"traversals":121,"max_depth":120},"bigsubst-large":{"alpha_us":1071,"norm_us":89,"traversals":2021,"max_depth":1020},"leaves-large-a":{"alpha_us":512163,"norm_us":261612,"traversals":3001,"max_depth":2000},"leaves-large-b":{"alpha_us":544873,"norm_us":257322,"traversals":3001,"max_depth":2000},"allbinders-large-a":{"alpha_us":80,"norm_us":12,"traversals":1001,"max_depth":1000},"allbinders-large-b":{"alpha_us":71,"norm_us":12,"traversals":1001,"max_depth":1000}},"debruijn":{"chain-small":{"alpha_us":36,"norm_us":18,"traversals":61,"max_depth":60},"apps-small":{"alpha_us":3,"norm_us":1,"traversals":121,"max_depth":60},"shadow-small":{"alpha_us":34,"norm_us":17,"traversals":61,"max_depth":60},"fv-small":{"alpha_us":3,"norm_us":1,"traversals":121,"max_depth":60},"shift-small":{"alpha_us":11,"norm_us":6,"traversals":13,"max_depth":12},"bigsubst-small":{"alpha_us":73,"norm_us":33,"traversals":141,"max_depth":80},"leaves-small-a":{"alpha_us":165,"norm_us":94,"traversals":181,"max_depth":120},"leaves-small-b":{"alpha_us":158,"norm_us":91,"traversals":181,"max_depth":120},"allbinders-small-a":{"alpha_us":36,"norm_us":18,"traversals":61,"max_depth":60},"allbinders-small-b":{"alpha_us":36,"norm_us":18,"traversals":61,"max_depth":60},"chain-medium":{"alpha_us":619,"norm_us":309,"traversals":251,"max_depth":250},"apps-medium":{"alpha_us":10,"norm_us":5,"traversals":501,"max_depth":250},"shadow-medium":{"alpha_us":601,"norm_us":296,"traversals":251,"max_depth":250},"fv-medium":{"alpha_us":10,"norm_us":6,"traversals":501,"max_depth":250},"shift-medium":{"alpha_us":116,"norm_us":59,"traversals":51,"max_depth":50},"bigsubst-medium":{"alpha_us":243,"norm_us":120,"traversals":521,"max_depth":270},"leaves-medium-a":{"alpha_us":3042,"norm_us":1696,"traversals":751,"max_depth":500},"leaves-medium-b":{"alpha_us":2910,"norm_us":1601,"traversals":751,"max_depth":500},"allbinders-medium-a":{"alpha_us":604,"norm_us":324,"traversals":251,"max_depth":250},"allbinders-medium-b":{"alpha_us":594,"norm_us":298,"traversals":251,"max_depth":250},"chain-large":{"alpha_us":11955,"norm_us":5661,"traversals":1001,"max_depth":1000},"apps-large":{"alpha_us":41,"norm_us":22,"traversals":2001,"max_depth":1000},"shadow-large":{"alpha_us":11089,"norm_us":5834,"traversals":1001,"max_depth":1000},"fv-large":{"alpha_us":42,"norm_us":22,"traversals":2001,"max_depth":1000},"shift-large":{"alpha_us":592,"norm_us":280,"traversals":121,"max_depth":120},"bigsubst-large":{"alpha_us":1031,"norm_us":476,"traversals":2021,"max_depth":1020},"leaves-large-a":{"alpha_us":51610,"norm_us":31395,"traversals":3001,"max_depth":2000},"leaves-large-b":{"alpha_us":53974,"norm_us":30703,"traversals":3001,"max_depth":2000},"allbinders-large-a":{"alpha_us":11998,"norm_us":5861,"traversals":1001,"max_depth":1000},"allbinders-large-b":{"alpha_us":11272,"norm_us":5552,"traversals":1001,"max_depth":1000}},"ln":{"chain-small":{"alpha_us":35,"norm_us":18,"traversals":61,"max_depth":60},"apps-small":{"alpha_us":4,"norm_us":1,"traversals":121,"max_depth":60},"shadow-small":{"alpha_us":34,"norm_us":17,"traversals":61,"max_depth":60},"fv-small":{"alpha_us":4,"norm_us":2,"traversals":121,"max_depth":60},"shift-small":{"alpha_us":12,"norm_us":5,"traversals":13,"max_depth":12},"bigsubst-small":{"alpha_us":67,"norm_us":34,"traversals":141,"max_depth":80},"leaves-small-a":{"alpha_us":194,"norm_us":96,"traversals":181,"max_depth":120},"leaves-small-b":{"alpha_us":170,"norm_us":94,"traversals":181,"max_depth":120},"allbinders-small-a":{"alpha_us":36,"norm_us":18,"traversals":61,"max_depth":60},"allbinders-small-b":{"alpha_us":37,"norm_us":18,"traversals":61,"max_depth":60},"chain-medium":{"alpha_us":686,"norm_us":336,"traversals":251,"max_depth":250},"apps-medium":{"alpha_us":15,"norm_us":6,"traversals":501,"max_depth":250},"shadow-medium":{"alpha_us":676,"norm_us":347,"traversals":251,"max_depth":250},"fv-medium":{"alpha_us":15,"norm_us":6,"traversals":501,"max_depth":250},"shift-medium":{"alpha_us":118,"norm_us":55,"traversals":51,"max_depth":50},"bigsubst-medium":{"alpha_us":287,"norm_us":134,"traversals":521,"max_depth":270},"leaves-medium-a":{"alpha_us":3055,"norm_us":1730,"traversals":751,"max_depth":500},"leaves-medium-b":{"alpha_us":3196,"norm_us":1748,"traversals":751,"max_depth":500},"allbinders-medium-a":{"alpha_us":599,"norm_us":361,"traversals":251,"max_depth":250},"allbinders-medium-b":{"alpha_us":676,"norm_us":340,"traversals":251,"max_depth":250},"chain-large":{"alpha_us":11481,"norm_us":5908,"traversals":1001,"max_depth":1000},"apps-large":{"alpha_us":65,"norm_us":27,"traversals":2001,"max_depth":1000},"shadow-large":{"alpha_us":11654,"norm_us":5998,"traversals":1001,"max_depth":1000},"fv-large":{"alpha_us":60,"norm_us":27,"traversals":2001,"max_depth":1000},"shift-large":{"alpha_us":566,"norm_us":281,"traversals":121,"max_depth":120},"bigsubst-large":{"alpha_us":960,"norm_us":478,"traversals":2021,"max_depth":1020},"leaves-large-a":{"alpha_us":54645,"norm_us":30431,"traversals":3001,"max_depth":2000},"leaves-large-b":{"alpha_us":53205,"norm_us":30554,"traversals":3001,"max_depth":2000},"allbinders-large-a":{"alpha_us":13761,"norm_us":8571,"traversals":1001,"max_depth":1000},"allbinders-large-b":{"alpha_us":12006,"norm_us":6534,"traversals":1001,"max_depth":1000}},"subst":{"chain-small":{"alpha_us":4,"norm_us":2,"traversals":61,"max_depth":60},"apps-small":{"alpha_us":2,"norm_us":3,"traversals":121,"max_depth":60},"shadow-small":{"alpha_us":2,"norm_us":2,"traversals":61,"max_depth":60},"fv-small":{"alpha_us":2,"norm_us":3,"traversals":121,"max_depth":60},"shift-small":{"alpha_us":3,"norm_us":4,"traversals":37,"max_depth":24},"bigsubst-small":{"alpha_us":3,"norm_us":12,"traversals":143,"max_depth":61},"leaves-small-a":{"alpha_us":5,"norm_us":4,"traversals":181,"max_depth":120},"leaves-small-b":{"alpha_us":73,"norm_us":4,"traversals":181,"max_depth":120},"allbinders-small-a":{"alpha_us":5,"norm_us":1,"traversals":61,"max_depth":60},"allbinders-small-b":{"alpha_us":4,"norm_us":1,"traversals":61,"max_depth":60},"chain-medium":{"alpha_us":16,"norm_us":6,"traversals":251,"max_depth":250},"apps-medium":{"alpha_us":8,"norm_us":10,"traversals":501,"max_depth":250},"shadow-medium":{"alpha_us":7,"norm_us":6,"traversals":251,"max_depth":250},"fv-medium":{"alpha_us":8,"norm_us":10,"traversals":501,"max_depth":250},"shift-medium":{"alpha_us":13,"norm_us":23,"traversals":151,"max_depth":100},"bigsubst-medium":{"alpha_us":10,"norm_us":35,"traversals":523,"max_depth":251},"leaves-medium-a":{"alpha_us":22,"norm_us":16,"traversals":751,"max_depth":500},"leaves-medium-b":{"alpha_us":1240,"norm_us":17,"traversals":751,"max_depth":500},"allbinders-medium-a":{"alpha_us":16,"norm_us":6,"traversals":251,"max_depth":250},"allbinders-medium-b":{"alpha_us":15,"norm_us":6,"traversals":251,"max_depth":250},"chain-large":{"alpha_us":62,"norm_us":24,"traversals":1001,"max_depth":1000},"apps-large":{"alpha_us":38,"norm_us":48,"traversals":2001,"max_depth":1000},"shadow-large":{"alpha_us":29,"norm_us":25,"traversals":1001,"max_depth":1000},"fv-large":{"alpha_us":39,"norm_us":46,"traversals":2001,"max_depth":1000},"shift-large":{"alpha_us":32,"norm_us":81,"traversals":361,"max_depth":240},"bigsubst-large":{"alpha_us":36,"norm_us":145,"traversals":2023,"max_depth":1001},"leaves-large-a":{"alpha_us":116,"norm_us":70,"traversals":3001,"max_depth":2000},"leaves-large-b":{"alpha_us":19224,"norm_us":78,"traversals":3001,"max_depth":2000},"allbinders-large-a":{"alpha_us":66,"norm_us":27,"traversals":1001,"max_depth":1000},"allbinders-large-b":{"alpha_us":65,"norm_us":25,"traversals":1001,"max_depth":1000}}}}
+264
ocaml/test/test_ego.ml
+264
ocaml/test/test_ego.ml
···
1
+
open Ego
2
+
3
+
let find_corpus () =
4
+
let candidates =
5
+
[ "../shared/corpus.json"; "shared/corpus.json";
6
+
"/home/bulg/projects/ego/shared/corpus.json" ]
7
+
in
8
+
match List.find_opt Sys.file_exists candidates with
9
+
| Some p -> p
10
+
| None -> failwith "corpus.json not found"
11
+
12
+
let check_bool name exp got =
13
+
if got <> exp then
14
+
failwith
15
+
(Printf.sprintf "%s: expected %b got %b" name exp got)
16
+
17
+
let check_raises name f =
18
+
match f () with
19
+
| _ -> failwith (name ^ ": expected exception")
20
+
| exception _ -> ()
21
+
22
+
let check_with rep t1 t2 =
23
+
match rep with
24
+
| `Named -> Named.alpha_equivalent t1 t2
25
+
| `Debruijn ->
26
+
Debruijn.alpha_equivalent
27
+
(Debruijn.convert_from_named t1)
28
+
(Debruijn.convert_from_named t2)
29
+
| `Ln ->
30
+
Locally_nameless.alpha_equivalent
31
+
(Locally_nameless.convert_from_named t1)
32
+
(Locally_nameless.convert_from_named t2)
33
+
| `Subst ->
34
+
Explicit_subst.alpha_equivalent
35
+
(Explicit_subst.convert_from_named t1)
36
+
(Explicit_subst.convert_from_named t2)
37
+
38
+
let reps = [ `Named; `Debruijn; `Ln; `Subst ]
39
+
40
+
let test_corpus () =
41
+
let entries = Json_io.load_corpus (find_corpus ()) in
42
+
List.iter
43
+
(fun (e : Json_io.corpus_entry) ->
44
+
List.iter
45
+
(fun r ->
46
+
match e.Json_io.expected with
47
+
| Some exp ->
48
+
check_bool
49
+
(Printf.sprintf "%s [%s]" e.name
50
+
(match r with
51
+
| `Named -> "named" | `Debruijn -> "debruijn"
52
+
| `Ln -> "ln" | `Subst -> "subst"))
53
+
exp (check_with r e.t1 e.t2)
54
+
| None -> ())
55
+
reps)
56
+
entries
57
+
58
+
let rng = Random.State.make [| 42 |]
59
+
60
+
let names = [| "a"; "b"; "c"; "d"; "e"; "f" |]
61
+
let fvs = [| "p"; "q"; "g"; "h" |]
62
+
63
+
let rec gen scope depth =
64
+
let pick arr = arr.(Random.State.int rng (Array.length arr)) in
65
+
if depth <= 0 then
66
+
match scope with
67
+
| [] -> Named.Var (pick fvs)
68
+
| _ ->
69
+
if Random.State.float rng 1.0 < 0.75 then Named.Var (pick (Array.of_list scope))
70
+
else Named.Var (pick fvs)
71
+
else
72
+
let r = Random.State.float rng 1.0 in
73
+
if r < 0.45 then
74
+
let n =
75
+
if scope <> [] && Random.State.float rng 1.0 < 0.35
76
+
then pick (Array.of_list scope)
77
+
else pick names
78
+
in
79
+
Named.Lam (n, gen (n :: scope) (depth - 1))
80
+
else if r < 0.75 then
81
+
Named.App (gen scope (depth - 1), gen scope (depth - 1))
82
+
else if r < 0.85 then
83
+
let n = match scope with [] -> "u" | _ -> pick (Array.of_list scope) in
84
+
Named.Subst (n, gen scope (depth - 1), gen scope (depth - 1))
85
+
else
86
+
match scope with
87
+
| [] -> Named.Var (pick fvs)
88
+
| _ -> Named.Var (pick (Array.of_list scope))
89
+
90
+
let random_term () = gen [] (2 + Random.State.int rng 4)
91
+
92
+
let test_reflexivity () =
93
+
for _ = 1 to 200 do
94
+
let t = random_term () in
95
+
List.iter
96
+
(fun r ->
97
+
check_bool "reflexive" true (check_with r t t))
98
+
reps
99
+
done
100
+
101
+
let test_symmetry () =
102
+
for _ = 1 to 200 do
103
+
let t1 = random_term () in
104
+
let t2 = random_term () in
105
+
List.iter
106
+
(fun r ->
107
+
check_bool "symmetric"
108
+
(check_with r t1 t2) (check_with r t2 t1))
109
+
reps
110
+
done
111
+
112
+
let test_transitivity () =
113
+
for _ = 1 to 100 do
114
+
let t = random_term () in
115
+
List.iter
116
+
(fun r ->
117
+
let norm_named n =
118
+
match r with
119
+
| `Named -> Named.normalise n
120
+
| _ -> Named.normalise n
121
+
in
122
+
let a = check_with r t t in
123
+
let b = check_with r (norm_named t) (norm_named t) in
124
+
check_bool "transitive-self" a b)
125
+
reps
126
+
done
127
+
128
+
let test_fv_preserved () =
129
+
for _ = 1 to 200 do
130
+
let t1 = random_term () in
131
+
let t2 = random_term () in
132
+
if Named.alpha_equivalent t1 t2 then
133
+
check_bool "fv equal" true
134
+
(Named.SSet.equal (Named.free_variables (Named.normalise t1))
135
+
(Named.free_variables (Named.normalise t2)))
136
+
done
137
+
138
+
let test_roundtrip () =
139
+
for _ = 1 to 200 do
140
+
let t = random_term () in
141
+
let t' = Debruijn.convert_to_named (Debruijn.convert_from_named t) in
142
+
check_bool "roundtrip debruijn" true
143
+
(Named.alpha_equivalent t' t);
144
+
let t'' =
145
+
Locally_nameless.convert_to_named
146
+
(Locally_nameless.convert_from_named t)
147
+
in
148
+
check_bool "roundtrip ln" true
149
+
(Named.alpha_equivalent t'' t);
150
+
let t''' =
151
+
Explicit_subst.convert_to_named
152
+
(Explicit_subst.convert_from_named t)
153
+
in
154
+
check_bool "roundtrip subst" true
155
+
(Named.alpha_equivalent t''' t)
156
+
done
157
+
158
+
let test_cross_rep_normalise () =
159
+
for _ = 1 to 100 do
160
+
let t = random_term () in
161
+
let n1 = Named.normalise t in
162
+
let n2 =
163
+
Debruijn.convert_to_named
164
+
(Debruijn.normalise (Debruijn.convert_from_named t))
165
+
in
166
+
let n3 =
167
+
Locally_nameless.convert_to_named
168
+
(Locally_nameless.normalise (Locally_nameless.convert_from_named t))
169
+
in
170
+
let n4 =
171
+
Explicit_subst.convert_to_named
172
+
(Explicit_subst.normalise (Explicit_subst.convert_from_named t))
173
+
in
174
+
check_bool "named vs debruijn" true
175
+
(Named.alpha_equivalent n1 n2);
176
+
check_bool "named vs ln" true
177
+
(Named.alpha_equivalent n1 n3);
178
+
check_bool "named vs subst" true
179
+
(Named.alpha_equivalent n1 n4)
180
+
done
181
+
182
+
let test_parse_errors () =
183
+
List.iter
184
+
(fun s ->
185
+
match Syntax.parse_result s with
186
+
| Ok _ -> failwith ("should reject: " ^ s)
187
+
| Error _ -> ())
188
+
[ ""; "\\"; "\\x"; "\\x."; "(\\x. x"; "\\x. x)"; "[x := ] x"; "[ := y] x";
189
+
"((x"; "[x := y]"; "."; "\\. x" ]
190
+
191
+
let test_malformed () =
192
+
let open Locally_nameless in
193
+
check_bool "dangling bvar" false (lc (BVar 0));
194
+
check_bool "closed lam" true (lc (Lam (BVar 0)));
195
+
check_bool "dangling deep" false
196
+
(lc (Lam (Lam (BVar 2))));
197
+
check_raises "convert raises"
198
+
(fun () -> ignore (convert_to_named (BVar 3)));
199
+
check_raises "alpha raises"
200
+
(fun () -> ignore (alpha_equivalent (BVar 1) (BVar 1)))
201
+
202
+
let test_debruijn_scope () =
203
+
let open Debruijn in
204
+
check_bool "well scoped" true (well_scoped 0 (Lam (Var 0)));
205
+
check_bool "ill scoped" false (well_scoped 0 (Var 0));
206
+
check_raises "to_named raises"
207
+
(fun () -> ignore (convert_to_named (Lam (Var 2))))
208
+
209
+
let test_capture_avoidance () =
210
+
let parse s =
211
+
match Syntax.parse_result s with
212
+
| Ok t -> t
213
+
| Error m -> failwith m
214
+
in
215
+
let cases =
216
+
[ ("[x := z] \\z. x", "\\w. z", true);
217
+
("[x := z] \\z. x", "\\z. z", false);
218
+
("[x := q] \\x. x", "\\x. x", true);
219
+
("[x := y] \\y. x y", "\\w. y w", true);
220
+
("[x := f y] \\y. \\z. x z", "\\a. \\b. f y b", true);
221
+
("[x := a] [y := b] x y", "a b", true) ]
222
+
in
223
+
List.iter
224
+
(fun (s1, s2, exp) ->
225
+
let t1 = parse s1 in
226
+
let t2 = parse s2 in
227
+
List.iter
228
+
(fun r ->
229
+
check_bool (s1 ^ " ~ " ^ s2) exp (check_with r t1 t2))
230
+
reps)
231
+
cases
232
+
233
+
let test_explicit_susp () =
234
+
let open Explicit_subst in
235
+
let t = of_named (Named.Subst ("x", Named.Var "z", Named.Lam ("z", Named.Var "x"))) in
236
+
let n = normalise t in
237
+
(match n with
238
+
| Lam (y, Var z) ->
239
+
check_bool "binder renamed" true (y <> "z");
240
+
check_bool "body is free z" true (z = "z")
241
+
| _ -> failwith "expected renamed lambda");
242
+
check_bool "susp agrees with normal" true
243
+
(alpha_equivalent_susp t (normalise t))
244
+
245
+
let () =
246
+
let tests =
247
+
[ ("corpus", test_corpus);
248
+
("reflexivity", test_reflexivity);
249
+
("symmetry", test_symmetry);
250
+
("transitivity", test_transitivity);
251
+
("fv preserved", test_fv_preserved);
252
+
("roundtrip", test_roundtrip);
253
+
("cross-rep normalise", test_cross_rep_normalise);
254
+
("parse errors", test_parse_errors);
255
+
("local closure", test_malformed);
256
+
("de bruijn scope", test_debruijn_scope);
257
+
("capture avoidance", test_capture_avoidance);
258
+
("suspended subst", test_explicit_susp) ]
259
+
in
260
+
List.iter
261
+
(fun (name, f) ->
262
+
f ();
263
+
Printf.printf "ok %s\n" name)
264
+
tests
+149
tools/automata_viz.py
+149
tools/automata_viz.py
···
1
+
#!/usr/bin/env python3
2
+
import argparse
3
+
import json
4
+
import shutil
5
+
import subprocess
6
+
import sys
7
+
from pathlib import Path
8
+
9
+
10
+
def q(s):
11
+
return json.dumps(str(s), ensure_ascii=False)
12
+
13
+
14
+
def attrs(items):
15
+
xs = [(k, v) for k, v in items if v is not None]
16
+
if not xs:
17
+
return ""
18
+
return " [" + ", ".join(f"{k}={q(v)}" for k, v in xs) + "]"
19
+
20
+
21
+
def load(path):
22
+
with open(path, "r", encoding="utf-8") as f:
23
+
spec = json.load(f)
24
+
if "states" not in spec:
25
+
raise ValueError("missing required field: states")
26
+
if "transitions" not in spec:
27
+
raise ValueError("missing required field: transitions")
28
+
return spec
29
+
30
+
31
+
def transition_label(t):
32
+
if "label" in t:
33
+
return t["label"]
34
+
read = t.get("read")
35
+
write = t.get("write")
36
+
action = t.get("action")
37
+
parts = []
38
+
if read is not None:
39
+
parts.append(str(read))
40
+
if write is not None:
41
+
parts.append("→ " + str(write))
42
+
if action is not None:
43
+
parts.append(str(action))
44
+
return " ".join(parts)
45
+
46
+
47
+
def to_dot(spec):
48
+
name = spec.get("name", "automaton")
49
+
rankdir = spec.get("rankdir", "LR")
50
+
accepting = set(spec.get("accepting", []))
51
+
start = spec.get("start")
52
+
53
+
lines = [
54
+
f"digraph {q(name)} {{",
55
+
f" rankdir={q(rankdir)};",
56
+
' graph [pad="0.25", nodesep="0.7", ranksep="0.9"];',
57
+
' node [shape=circle, fontname="Times New Roman", fontsize=16];',
58
+
' edge [fontname="Times New Roman", fontsize=14, arrowsize=0.8];',
59
+
]
60
+
61
+
if start is not None:
62
+
lines.append(' "__start" [shape=point, label="", width=0.08];')
63
+
64
+
for state in spec["states"]:
65
+
if isinstance(state, str):
66
+
sid = state
67
+
label = state
68
+
final = sid in accepting
69
+
else:
70
+
sid = state["id"]
71
+
label = state.get("label", sid)
72
+
final = state.get("accepting", sid in accepting)
73
+
shape = "doublecircle" if final else "circle"
74
+
lines.append(f" {q(sid)}{attrs([('label', label), ('shape', shape)])};")
75
+
76
+
if start is not None:
77
+
lines.append(f" \"__start\" -> {q(start)}{attrs([('label', spec.get('start_label', 'start'))])};")
78
+
79
+
for t in spec["transitions"]:
80
+
src = t["from"]
81
+
dst = t["to"]
82
+
label = transition_label(t)
83
+
lines.append(
84
+
f" {q(src)} -> {q(dst)}"
85
+
f"{attrs([('label', label), ('xlabel', t.get('xlabel'))])};"
86
+
)
87
+
88
+
lines.append("}")
89
+
return "\n".join(lines) + "\n"
90
+
91
+
92
+
def render(dot_path, out_path, fmt):
93
+
dot = shutil.which("dot")
94
+
if dot is None:
95
+
raise RuntimeError("graphviz 'dot' executable not found")
96
+
subprocess.run([dot, f"-T{fmt}", str(dot_path), "-o", str(out_path)], check=True)
97
+
98
+
99
+
def main(argv):
100
+
parser = argparse.ArgumentParser(
101
+
description="Render finite automata/transducers from JSON using Graphviz."
102
+
)
103
+
parser.add_argument("input", help="automaton JSON file")
104
+
parser.add_argument("-o", "--output", help="output image path; extension selects format")
105
+
parser.add_argument("--dot", help="write DOT to this path")
106
+
parser.add_argument(
107
+
"--format",
108
+
choices=["svg", "png", "pdf", "dot"],
109
+
help="render format; defaults to output extension, or dot when no output is given",
110
+
)
111
+
args = parser.parse_args(argv)
112
+
113
+
spec = load(args.input)
114
+
dot_text = to_dot(spec)
115
+
fmt = args.format
116
+
if fmt is None:
117
+
fmt = Path(args.output).suffix.lstrip(".") if args.output else "dot"
118
+
if fmt == "":
119
+
raise ValueError("cannot infer output format from path without extension")
120
+
121
+
dot_path = Path(args.dot) if args.dot else None
122
+
if dot_path is not None:
123
+
dot_path.write_text(dot_text, encoding="utf-8")
124
+
125
+
if fmt == "dot" and args.output is None:
126
+
sys.stdout.write(dot_text)
127
+
return 0
128
+
129
+
if args.output is None:
130
+
raise ValueError("rendering requires --output unless --format dot is used")
131
+
132
+
out_path = Path(args.output)
133
+
if fmt == "dot":
134
+
out_path.write_text(dot_text, encoding="utf-8")
135
+
return 0
136
+
137
+
tmp_dot = dot_path if dot_path is not None else out_path.with_suffix(out_path.suffix + ".dot")
138
+
if dot_path is None:
139
+
tmp_dot.write_text(dot_text, encoding="utf-8")
140
+
try:
141
+
render(tmp_dot, out_path, fmt)
142
+
finally:
143
+
if dot_path is None:
144
+
tmp_dot.unlink(missing_ok=True)
145
+
return 0
146
+
147
+
148
+
if __name__ == "__main__":
149
+
raise SystemExit(main(sys.argv[1:]))