the next generation of the in-browser educational proof assistant
Merge pull request #6 from mio-19/main
add a few tests
authored by
Liam O'Connor
and committed by
GitHub
38f80bbf
9c7d9851
+56
-9
+8
-7
src/HOTerm.res
+8
-7
src/HOTerm.res
···
133
133
subst->Array.map(((a, b)) => (upshift(a, amount), upshift(b, amount)))
134
134
}
135
135
// where pattern unification used mapbind we will need to use discharge for FCU
136
+
//
137
+
// When `prune` is true, it marks “dead” variables as Unallowed. Nipkow 1993 uses Var(-infinity) for this in the de Bruijn’s notation implementation.
138
+
// Nipkow 1993's non de Bruijn implementation handle this logic in `proj`. Similarly Makoto Hamana's paper uses `elem` and `subst` in `prune`
136
139
let rec discharge = (subst: array<(t, t)>, term: t, ~prune: bool): t => {
137
140
switch lookup(term, subst) {
138
141
| Some(found) => found
···
307
310
let rec proj_allowed = (subst: subst, term: t): bool => {
308
311
let term' = devar(subst, term)
309
312
switch term' {
310
-
| Lam(_) => false
311
-
| Unallowed => false
312
-
| Schematic(_) => false
313
-
| Symbol(_) => false
313
+
| Lam(_) | Unallowed | Schematic(_) | Symbol(_) => false
314
314
| Var(_) => true // pattern unification only allows this
315
-
// FCU allows this, right?
315
+
// FCU allows this:
316
316
| App(_) =>
317
317
switch strip(term') {
318
318
| (Symbol(_) | Var(_), args) => Array.every(args, x => proj_allowed(subst, x))
···
390
390
raise(UnifyFail("flexible schematic occurs in rigid term"))
391
391
}
392
392
// pattern unification
393
-
//let u = b->mapbind0(bind => idx2(xs, bind))
393
+
// let u = b->mapbind0(bind => idx2(xs, bind))
394
394
// FCU
395
395
let zn = mkvars(xs->Array.length)
396
-
let u = discharge(Belt.Array.zip(xs, zn), b, ~prune=true)
396
+
// we reversed it so that the last one will be picked if there are duplicates. This behaviour helps certain real world cases.
397
+
let u = discharge(Belt.Array.reverse(Belt.Array.zip(xs, zn)), b, ~prune=true)
397
398
proj(subst->substAdd(sa, lams(xs->Array.length, u)), u, ~gen)
398
399
}
399
400
let rec unifyTerm = (a: t, b: t, subst: subst, ~gen: option<gen>): subst =>
+33
-2
tests/HOTermTest.res
+33
-2
tests/HOTermTest.res
···
46
46
)
47
47
}
48
48
}
49
-
let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=true) => {
49
+
let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => {
50
50
testUnify0(t, at, bt, ~subst?, ~msg?, ~reduce)
51
51
testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce)
52
52
}
···
170
170
t->block("flex-rigid3", t => {
171
171
let x = "(?0 \\10)"
172
172
let y = "(fst \\10)"
173
-
t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"})))
173
+
t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"})))
174
174
})
175
175
t->block("flex-rigid", t => {
176
176
let x = "(?0 \\10)"
···
273
273
let a = "((x. ?0 x) (x. x x))"
274
274
// TODO: should it not unify or not?
275
275
t->Util.testNotUnify(a, divergent)
276
+
})
277
+
t->block("dup var", t => {
278
+
let a = "(?0 \\0 \\0)"
279
+
let b = "\\0"
280
+
t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. \\0)")))
281
+
})
282
+
// Yokoyama et al.'s example in A Functional Implementation of Function-as-Constructor Higher-Order Unification Makoto Hamana1
283
+
t->block("break global resctriction", t => {
284
+
t->testUnify(
285
+
"(x. y. ?0 (c x) (c y))",
286
+
"(x. y. c (?1 x y))",
287
+
~reduce=true,
288
+
~subst=emptySubst
289
+
->substAdd(0, t->Util.parse("(x. x. (c ?2))"))
290
+
->substAdd(1, t->Util.parse("(x. x. ?2)")),
291
+
)
292
+
})
293
+
t->block("violate global restriction only", t => {
294
+
t->testUnify(
295
+
"(l. (?0 (fst l)))",
296
+
"(l. (snd (?1 (cons (fst l) (snd l)))))",
297
+
~reduce=true,
298
+
~subst=emptySubst
299
+
->substAdd(0, t->Util.parse("(x. (snd ?2))"))
300
+
->substAdd(1, t->Util.parse("(x. ?2)")),
301
+
)
302
+
})
303
+
t->block("violate local restriction", t => {
304
+
let a = "(?0 (fst l) l)"
305
+
let b = "(cons l)"
306
+
t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. cons x)")))
276
307
})
277
308
})
+15
tests/TestUtil.res
+15
tests/TestUtil.res
···
1
1
open Signatures
2
2
open Zora
3
+
open Util
3
4
4
5
let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn
5
6
···
20
21
t->equal(res->fst, t2, ~msg?)
21
22
}
22
23
| Error(msg) => t->fail(~msg="parse failed: " ++ msg)
24
+
}
25
+
}
26
+
let parse = (t: Zora.t, input: string): Term.t => {
27
+
let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen())
28
+
switch res {
29
+
| Ok((term, "")) => term
30
+
| Ok((_, rest)) => {
31
+
t->fail(~msg="parse incomplete: " ++ rest)
32
+
raise(Unreachable(""))
33
+
}
34
+
| Error(msg) => {
35
+
t->fail(~msg="parse failed: " ++ msg)
36
+
raise(Unreachable(""))
37
+
}
23
38
}
24
39
}
25
40
let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?) => {