vm.fail
Alpha equivalence checker for arbitrary lambda terms
1import std/[os, random, sets]
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
7let reps = [rNamed, rDebruijn, rLn, rSubst]
8
9proc check(cond: bool, msg: string) =
10 if not cond:
11 raise newException(AssertionDefect, msg)
12
13proc expectRaises[T: CatchableError](msg: string, f: proc()) =
14 try:
15 f()
16 raise newException(AssertionDefect, msg & ": expected exception")
17 except T:
18 discard
19
20proc 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
26proc 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
40proc pick(r: var Rand, xs: openArray[string]): string =
41 xs[r.rand(xs.len - 1)]
42
43proc 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
50proc 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
66proc randomTerm(r: var Rand): Named =
67 gen(r, @[], 2 + r.rand(3))
68
69proc 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
83proc 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
125proc 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
131proc 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
147proc parsed(s: string): Named =
148 let r = parseResult(s)
149 if not r.ok:
150 raise newException(ValueError, r.err)
151 r.term
152
153proc 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
175proc run(name: string, f: proc()) =
176 f()
177 echo "ok ", name
178
179run("corpus", testCorpus)
180run("properties", testProperties)
181run("parse errors", testParseErrors)
182run("malformed", testMalformed)
183run("capture", testCapture)