vm.fail
Alpha equivalence checker for arbitrary lambda terms
1import std/[algorithm, os, json, monotimes, strutils]
2import ego/named, ego/debruijn, ego/locally_nameless, ego/explicit_subst,
3 ego/syntax, ego/jsonio
4
5type Rep = enum rNamed, rDebruijn, rLn, rSubst
6
7const repNames = ["named", "debruijn", "ln", "subst"]
8
9proc 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
18proc 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
31proc 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
45proc 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
76proc nowUs(): int64 =
77 let m = getMonoTime()
78 m.ticks div 1000
79
80proc median(xs: var seq[int64]): int64 =
81 xs.sort()
82 xs[xs.len div 2]
83
84proc 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
153proc 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
172proc 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
222quit(main())