the next generation of the in-browser educational proof assistant
1exception SubstNotCompatible(string)
2
3module type ATOM = AtomDef.ATOM
4
5module IntCmp = Belt.Id.MakeComparable({
6 type t = int
7 let cmp = Pervasives.compare
8})
9
10module Make = (Atom: AtomDef.ATOM): {
11 type rec t =
12 | Atom(Atom.t)
13 | Compound({subexps: array<t>})
14 | Var({idx: int})
15 | Schematic({schematic: int, allowed: array<int>})
16
17 include Signatures.TERM
18 with type t := t
19 and type meta = string
20 and type schematic = int
21 and type subst = Map.t<int, t>
22 let mapTerms: (t, t => t) => t
23} => {
24 type rec t =
25 | Atom(Atom.t)
26 | Compound({subexps: array<t>})
27 | Var({idx: int})
28 | Schematic({schematic: int, allowed: array<int>})
29 module Atom = Atom
30 type meta = string
31 type schematic = int
32 type subst = Map.t<schematic, t>
33 let substEqual = Util.mapEqual
34 let mapSubst = Util.mapMapValues
35 let makeSubst = () => {
36 Map.make()
37 }
38 let equivalent = (a: t, b: t) => {
39 a == b
40 }
41 let reduce = (term: t) => term
42 let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
43 switch it {
44 | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
45 | Compound({subexps}) =>
46 subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
47 Belt.Set.union(s, schematicsIn(x))
48 )
49 | _ => Belt.Set.make(~id=module(IntCmp))
50 }
51 let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
52 switch it {
53 | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
54 | Compound({subexps}) =>
55 subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
56 Belt.Set.union(s, freeVarsIn(x))
57 )
58 | _ => Belt.Set.make(~id=module(IntCmp))
59 }
60 let rec substitute = (term: t, subst: subst) =>
61 switch term {
62 | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))})
63 | Schematic({schematic, _}) =>
64 switch Map.get(subst, schematic) {
65 | None => term
66 | Some(found) => found
67 }
68 | Atom(name) => {
69 let symbolSubs =
70 subst
71 ->Map.entries
72 ->Iterator.toArray
73 ->Array.filterMap(((name, v)) =>
74 switch v {
75 | Atom(v) => Some((name, v))
76 | _ => None
77 }
78 )
79 ->Map.fromArray
80 Atom(name->Atom.substitute(symbolSubs))
81 }
82 | _ => term
83 }
84
85 let combineSubst = (s: subst, t: subst) => {
86 let nu = Map.make()
87 Map.entries(s)->Iterator.forEach(opt =>
88 switch opt {
89 | None => ()
90 | Some((key, term)) => nu->Map.set(key, term->substitute(t))
91 }
92 )
93 Map.entries(t)->Iterator.forEach(opt =>
94 switch opt {
95 | None => ()
96 | Some((key, term)) => nu->Map.set(key, term->substitute(s))
97 }
98 )
99 nu
100 }
101 let emptySubst: subst = Map.make()
102 let singletonSubst: (int, t) => subst = (schematic, term) => {
103 let s = Map.make()
104 s->Map.set(schematic, term)
105 s
106 }
107 let rec unifyTerm = (a: t, b: t): Seq.t<subst> =>
108 switch (a, b) {
109 | (Atom(na), Atom(nb)) =>
110 Atom.unify(na, nb)->Seq.map(subst => subst->Util.mapMapValues(v => Atom(v)))
111 | (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
112 unifyArray(Belt.Array.zip(xa, xb))
113 | (Var({idx: ia}), Var({idx: ib})) if ia == ib => Seq.once(emptySubst)
114 | (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb =>
115 Seq.once(emptySubst)
116 | (Schematic({schematic, allowed}), t)
117 if !Belt.Set.has(schematicsIn(t), schematic) &&
118 Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
119 Seq.once(singletonSubst(schematic, t))
120 | (t, Schematic({schematic, allowed}))
121 if !Belt.Set.has(schematicsIn(t), schematic) &&
122 Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
123 Seq.once(singletonSubst(schematic, t))
124 | (_, _) => Seq.empty
125 }
126 and unifyArray = (a: array<(t, t)>): Seq.t<subst> => {
127 if Array.length(a) == 0 {
128 Seq.once(emptySubst)
129 } else {
130 let (x, y) = a[0]->Option.getUnsafe
131 unifyTerm(x, y)->Seq.flatMap(s1 =>
132 a
133 ->Array.sliceToEnd(~start=1)
134 ->Array.filterMap(((t1, t2)) =>
135 try {Some((substitute(t1, s1), substitute(t2, s1)))} catch {
136 | SubstNotCompatible(_) => None
137 }
138 )
139 ->unifyArray
140 ->Seq.filterMap(s2 =>
141 try {Some(combineSubst(s1, s2))} catch {
142 | SubstNotCompatible(_) => None
143 }
144 )
145 )
146 }
147 }
148 let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b)
149
150 let rec lower = (term: t): option<Atom.t> =>
151 switch term {
152 | Atom(s) => Some(s)
153 | Var({idx}) => Atom.coerce(AtomDef.VarBase.wrap(Var({idx: idx})))
154 | Schematic({schematic, allowed}) =>
155 Atom.coerce(AtomDef.VarBase.wrap(Schematic({schematic, allowed})))
156 | Compound({subexps: [e1]}) => lower(e1)
157 | _ => None
158 }
159 let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
160 switch term {
161 | Atom(s) => Atom(Atom.substDeBruijn(s, Array.map(substs, lower), ~from))
162
163 | Compound({subexps}) =>
164 Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
165 | Var({idx: var}) =>
166 if var < from {
167 term
168 } else if var - from < Array.length(substs) && var - from >= 0 {
169 Option.getUnsafe(substs[var - from])
170 } else {
171 Var({idx: var - Array.length(substs)})
172 }
173 | Schematic({schematic, allowed}) =>
174 Schematic({
175 schematic,
176 allowed: Array.filterMap(allowed, i =>
177 if i < from + Array.length(substs) {
178 None
179 } else {
180 Some(i - (from + Array.length(substs)))
181 }
182 ),
183 })
184 }
185 let rec upshift = (term: t, amount: int, ~from: int=0) =>
186 switch term {
187 | Atom(s) => Atom(s->Atom.upshift(amount, ~from))
188 | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
189 | Var({idx}) =>
190 Var({
191 idx: if idx >= from {
192 idx + amount
193 } else {
194 idx
195 },
196 })
197 | Schematic({schematic, allowed}) =>
198 Schematic({
199 schematic,
200 allowed: Array.map(allowed, i =>
201 if i >= from {
202 i + amount
203 } else {
204 i
205 }
206 ),
207 })
208 }
209 let place = (x: int, ~scope: array<string>) => Schematic({
210 schematic: x,
211 allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
212 })
213 let mergeSubsts = Util.mapUnion
214
215 type gen = ref<int>
216 let seen = (g: gen, s: int) => {
217 if s >= g.contents {
218 g := s + 1
219 }
220 }
221 let fresh = (g: gen, ~replacing as _=?) => {
222 let v = g.contents
223 g := g.contents + 1
224 v
225 }
226 let prettyPrintVar = (idx: int, scope: array<string>) => {
227 switch scope[idx] {
228 | Some(n) if Array.indexOf(scope, n) == idx => n
229 | _ => "\\"->String.concat(String.make(idx))
230 }
231 }
232 let makeGen = () => {
233 ref(0)
234 }
235 let rec prettyPrint = (it: t, ~scope: array<string>) =>
236 switch it {
237 | Atom(name) => Atom.prettyPrint(name, ~scope)
238 | Var({idx}) => prettyPrintVar(idx, scope)
239 | Schematic({schematic, allowed}) =>
240 "?"
241 ->String.concat(String.make(schematic))
242 ->String.concat("(")
243 ->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " "))
244 ->String.concat(")")
245 | Compound({subexps}) =>
246 "("
247 ->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
248 ->String.concat(")")
249 }
250
251 let prettyPrintSubst = (sub, ~scope) =>
252 Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
253 let nameRES = "^([^\\s.\\[\\]()]+)\\."
254 let prettyPrintMeta = (str: string) => {
255 String.concat(str, ".")
256 }
257 let parseMeta = (str: string) => {
258 let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
259 switch re->RegExp.exec(str->String.trim) {
260 | None => Error("not a meta name")
261 | Some(res) =>
262 switch RegExp.Result.matches(res) {
263 | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
264 | _ => Error("impossible happened")
265 }
266 }
267 }
268 let mkParser = (~scope: array<string>, ~gen=?): Parser.t<t> => {
269 open Parser
270 let varLit = string("\\")->then(decimal)
271 let ident = regex1(/([^\s\(\)]+)/)
272 let varIdx =
273 varLit
274 ->or(
275 ident->bind(id =>
276 switch scope->Array.indexOfOpt(id) {
277 | Some(idx) => pure(idx)
278 | None => fail("expected variable")
279 }
280 ),
281 )
282 ->lexeme
283 let var = varIdx->map(idx => Var({idx: idx}))
284
285 let schemaLit =
286 string("?")
287 ->then(decimal)
288 ->bind(schematic =>
289 many(varIdx)
290 ->between(token("("), token(")"))
291 ->map(allowed => {
292 gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore
293 Schematic({schematic, allowed})
294 })
295 )
296 let inner = fix(f =>
297 choice([
298 schemaLit->label("schematic"),
299 var->label("variable"),
300 liftParse(Atom.parse, ~scope, ~gen?)->map(a => Atom(a))->label("atom"),
301 many(f)
302 ->between(token("(")->label("open expression"), token(")")->label("close expression"))
303 ->map(subexps => Compound({subexps: subexps})),
304 ])->lexeme
305 )
306 whitespace->then(inner)
307 }
308
309 let parse = (str: string, ~scope: array<string>, ~gen=?) =>
310 Parser.runParser(mkParser(~scope, ~gen?), str)
311
312 let rec concrete = t =>
313 switch t {
314 | Schematic(_) => false
315 | Atom(s) => Atom.concrete(s)
316 | Compound({subexps}) => subexps->Array.some(concrete)
317 | _ => false
318 }
319 let mapTerms = (t, f) => f(t)
320}