the next generation of the in-browser educational proof assistant
unify add gen? parameter
+13
-13
+9
-9
src/HOTerm.res
+9
-9
src/HOTerm.res
···
170
170
| _ => {func: term, args: []}
171
171
}
172
172
}
173
-
let rec unifyTerm = (a: t, b: t) =>
173
+
let rec unifyTerm = (a: t, b: t, ~gen=?) =>
174
174
switch (reduce(a), reduce(b)) {
175
175
| (Symbol({name: na}), Symbol({name: nb})) if na == nb => Some(emptySubst)
176
176
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst)
···
178
178
| (Lam({name: _, body: ba}), Lam({name: _, body: bb})) => unifyTerm(ba, bb)
179
179
| (Lam({name: _, body: ba}), b) => unifyTerm(ba, App({func: upshift(b, 1), arg: Var({idx: 0})}))
180
180
| (a, Lam({name: _, body: bb})) => unifyTerm(App({func: upshift(a, 1), arg: Var({idx: 0})}), bb)
181
-
| (_, _) => cases(a, peelApp(a), b, peelApp(b))
181
+
| (_, _) => cases(a, peelApp(a), b, peelApp(b), ~gen?)
182
182
}
183
-
and unifyArray = (a: array<(t, t)>) => {
183
+
and unifyArray = (a: array<(t, t)>, ~gen=?) => {
184
184
if Array.length(a) == 0 {
185
185
Some(emptySubst)
186
186
} else {
187
187
let (x, y) = a[0]->Option.getUnsafe
188
-
switch unifyTerm(x, y) {
188
+
switch unifyTerm(x, y, ~gen?) {
189
189
| None => None
190
190
| Some(s1) =>
191
191
switch a
···
198
198
}
199
199
}
200
200
}
201
-
and cases = (at: t, a: peelAppT, bt: t, b: peelAppT) => {
201
+
and cases = (at: t, a: peelAppT, bt: t, b: peelAppT, ~gen=?) => {
202
202
switch (a.func, b.func) {
203
203
// rigid-rigid
204
204
| (Symbol(_) | Var(_), Symbol(_) | Var(_)) =>
205
205
if a.args->Array.length == b.args->Array.length && equivalent(a.func, b.func) {
206
-
unifyArray(Belt.Array.zip(a.args, b.args))
206
+
unifyArray(Belt.Array.zip(a.args, b.args), ~gen?)
207
207
} else {
208
208
None
209
209
}
···
228
228
schematic: raise(TODO("TODO")),
229
229
allowed,
230
230
}))
231
-
switch unifyArray(Belt.Array.zip(raise(TODO("TODO")), hs)) {
231
+
switch unifyArray(Belt.Array.zip(raise(TODO("TODO")), hs), ~gen?) {
232
232
| Some(s) => {
233
233
let term: t = raise(TODO("TODO"))
234
234
Some(singletonSubst(schematic, term))
···
245
245
| (_, _) => None
246
246
}
247
247
}
248
-
let unify = (a: t, b: t) => {
249
-
switch unifyTerm(a, b) {
248
+
let unify = (a: t, b: t, ~gen=?) => {
249
+
switch unifyTerm(a, b, ~gen?) {
250
250
| None => []
251
251
| Some(s) => [s]
252
252
}
+1
-1
src/SExp.res
+1
-1
src/SExp.res
+3
-3
src/Signatures.res
+3
-3
src/Signatures.res
···
3
3
type schematic
4
4
type meta
5
5
type subst = Map.t<schematic, t>
6
+
type gen
6
7
let substitute: (t, subst) => t
7
-
let unify: (t, t) => array<subst>
8
+
let unify: (t, t, ~gen: gen=?) => array<subst>
8
9
// law: unify(a,b) == [{}] iff equivalent(a,b)
9
10
let equivalent: (t, t) => bool
10
11
let substDeBruijn: (t, array<t>, ~from: int=?) => t
11
12
let upshift: (t, int, ~from: int=?) => t
12
-
type gen
13
13
let fresh: (gen, ~replacing: meta=?) => schematic
14
14
let seen: (gen, schematic) => unit
15
15
let place: (schematic, ~scope: array<meta>) => t
···
25
25
type t
26
26
let substitute: (t, Term.subst) => t
27
27
let equivalent: (t, t) => bool
28
-
let unify: (t, t) => array<Term.subst>
28
+
let unify: (t, t, ~gen: Term.gen=?) => array<Term.subst>
29
29
let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t
30
30
let upshift: (t, int, ~from: int=?) => t
31
31
let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>