the next generation of the in-browser educational proof assistant
functorise sexp subst and unify
+27
-28
+7
-1
src/SExp.res
+7
-1
src/SExp.res
···
1
1
module ConstSymbol: SExpFunc.SYMBOL = {
2
2
type t = string
3
-
let match = (nameA, nameB) => nameA == nameB
3
+
type subst = Map.t<int, string>
4
+
let unify = (a, b) =>
5
+
if a == b {
6
+
Seq.once(Map.make())
7
+
} else {
8
+
Seq.empty
9
+
}
4
10
let prettyPrint = (name, ~scope as _: array<string>) => name
5
11
let parse = (string, ~scope as _: array<string>) => Ok((string, ""))
6
12
}
+20
-27
src/SExpFunc.res
+20
-27
src/SExpFunc.res
···
1
1
module type SYMBOL = {
2
2
type t
3
-
let match: (t, t) => bool
3
+
type subst = Map.t<int, t>
4
+
let unify: (t, t) => Seq.t<subst>
4
5
let prettyPrint: (t, ~scope: array<string>) => string
5
6
let parse: (string, ~scope: array<string>) => result<(t, string), string>
6
7
}
···
94
95
s->Map.set(schematic, term)
95
96
s
96
97
}
97
-
let rec unifyTerm = (a: t, b: t) =>
98
+
let rec unifyTerm = (a: t, b: t): Seq.t<subst> =>
98
99
switch (a, b) {
99
-
| (Symbol(na), Symbol(nb)) if na->Symbol.match(nb) => Some(emptySubst)
100
-
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst)
101
-
| (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => Some(emptySubst)
100
+
| (Symbol(na), Symbol(nb)) =>
101
+
Symbol.unify(na, nb)->Seq.map(subst => subst->Util.mapMapValues(v => Symbol(v)))
102
102
| (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
103
103
unifyArray(Belt.Array.zip(xa, xb))
104
+
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Seq.once(emptySubst)
105
+
| (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb =>
106
+
Seq.once(emptySubst)
104
107
| (Schematic({schematic, allowed}), t)
105
108
if !Belt.Set.has(schematicsIn(t), schematic) &&
106
109
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
107
-
Some(singletonSubst(schematic, t))
110
+
Seq.once(singletonSubst(schematic, t))
108
111
| (t, Schematic({schematic, allowed}))
109
112
if !Belt.Set.has(schematicsIn(t), schematic) &&
110
113
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
111
-
Some(singletonSubst(schematic, t))
112
-
| (_, _) => None
114
+
Seq.once(singletonSubst(schematic, t))
115
+
| (_, _) => Seq.empty
113
116
}
114
-
and unifyArray = (a: array<(t, t)>) => {
117
+
and unifyArray = (a: array<(t, t)>): Seq.t<subst> => {
115
118
if Array.length(a) == 0 {
116
-
Some(emptySubst)
119
+
Seq.once(emptySubst)
117
120
} else {
118
121
let (x, y) = a[0]->Option.getUnsafe
119
-
switch unifyTerm(x, y) {
120
-
| None => None
121
-
| Some(s1) =>
122
-
switch a
122
+
unifyTerm(x, y)->Seq.flatMap(s1 =>
123
+
a
123
124
->Array.sliceToEnd(~start=1)
124
125
->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
125
-
->unifyArray {
126
-
| None => None
127
-
| Some(s2) => Some(combineSubst(s1, s2))
128
-
}
129
-
}
126
+
->unifyArray
127
+
->Seq.map(s2 => combineSubst(s1, s2))
128
+
)
130
129
}
131
130
}
132
-
let unify = (a: t, b: t, ~gen as _=?) => {
133
-
Seq.fromArray(
134
-
switch unifyTerm(a, b) {
135
-
| None => []
136
-
| Some(s) => [s]
137
-
},
138
-
)
139
-
}
131
+
let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b)
132
+
140
133
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
141
134
switch term {
142
135
| Symbol(_) => term