the next generation of the in-browser educational proof assistant
first attempt at functorising s-expressions
+450
-402
+3
-4
src/InductiveSet.res
+3
-4
src/InductiveSet.res
···
1
1
open Signatures
2
2
open Component
3
-
open Util
4
3
5
4
// InductiveSet is specific to HOTerm to allow pattern matching on term structure
6
5
module Make = (
···
57
56
let generateInductionRule = (group: predicateGroup, allGroups: array<predicateGroup>): Rule.t => {
58
57
let {name: str, arity: i} = group
59
58
let numFormers = Array.length(allGroups)
60
-
let groupIndex = mustFindIndex(allGroups, g => g.name == str && g.arity == i)
59
+
let groupIndex = Util.mustFindIndex(allGroups, g => g.name == str && g.arity == i)
61
60
62
61
let findFormerIndex = (name, arity) =>
63
-
mustFindIndex(allGroups, g => g.name == name && g.arity == arity)
62
+
Util.mustFindIndex(allGroups, g => g.name == name && g.arity == arity)
64
63
65
64
let generateInductiveHypothesis = (premise: Rule.t, offset: int): option<Rule.t> => {
66
65
let (head, args) = HOTerm.strip(premise.conclusion)
···
89
88
let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion)
90
89
let typeIndex = switch conclusionHead {
91
90
| Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs))
92
-
| _ => throw(Unreachable("Constructor conclusion must have a Symbol head"))
91
+
| _ => throw(Util.Unreachable("Constructor conclusion must have a Symbol head"))
93
92
}
94
93
95
94
{
+1
-1
src/Method.res
+1
-1
src/Method.res
···
1
1
open Signatures
2
-
open Util
3
2
module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
4
3
module Rule = Rule.Make(Term, Judgment)
5
4
type t = {
···
37
36
}
38
37
39
38
let seqSizeLimit = 100
39
+
let newline = Util.newline
40
40
41
41
module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
42
42
module Rule = Rule.Make(Term, Judgment)
+8
-362
src/SExp.res
+8
-362
src/SExp.res
···
1
-
module IntCmp = Belt.Id.MakeComparable({
2
-
type t = int
3
-
let cmp = Pervasives.compare
4
-
})
5
-
6
-
type rec t =
7
-
| Symbol({name: string})
8
-
| Compound({subexps: array<t>})
9
-
| Var({idx: int})
10
-
| Schematic({schematic: int, allowed: array<int>})
11
-
| Ghost
12
-
type meta = string
13
-
type schematic = int
14
-
type subst = Map.t<schematic, t>
15
-
let substEqual = Util.mapEqual
16
-
let mapSubst = Util.mapMapValues
17
-
let makeSubst = () => {
18
-
Map.make()
19
-
}
20
-
let equivalent = (a: t, b: t) => {
21
-
a == b
22
-
}
23
-
let reduce = (term: t) => term
24
-
let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
25
-
switch it {
26
-
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
27
-
| Compound({subexps}) =>
28
-
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
29
-
Belt.Set.union(s, schematicsIn(x))
30
-
)
31
-
| _ => Belt.Set.make(~id=module(IntCmp))
32
-
}
33
-
let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
34
-
switch it {
35
-
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
36
-
| Compound({subexps}) =>
37
-
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
38
-
Belt.Set.union(s, freeVarsIn(x))
39
-
)
40
-
| _ => Belt.Set.make(~id=module(IntCmp))
41
-
}
42
-
let rec substitute = (term: t, subst: subst) =>
43
-
switch term {
44
-
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))})
45
-
| Schematic({schematic, _}) =>
46
-
switch Map.get(subst, schematic) {
47
-
| None => term
48
-
| Some(found) => found
49
-
}
50
-
| _ => term
51
-
}
52
-
53
-
let combineSubst = (s: subst, t: subst) => {
54
-
let nu = Map.make()
55
-
Map.entries(s)->Iterator.forEach(opt =>
56
-
switch opt {
57
-
| None => ()
58
-
| Some((key, term)) => nu->Map.set(key, term->substitute(t))
59
-
}
60
-
)
61
-
Map.entries(t)->Iterator.forEach(opt =>
62
-
switch opt {
63
-
| None => ()
64
-
| Some((key, term)) => nu->Map.set(key, term->substitute(s))
65
-
}
66
-
)
67
-
nu
68
-
}
69
-
let emptySubst: subst = Map.make()
70
-
let singletonSubst: (int, t) => subst = (schematic, term) => {
71
-
let s = Map.make()
72
-
s->Map.set(schematic, term)
73
-
s
74
-
}
75
-
let rec unifyTerm = (a: t, b: t) =>
76
-
switch (a, b) {
77
-
| (Symbol({name: na}), Symbol({name: nb})) if na == nb => Some(emptySubst)
78
-
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst)
79
-
| (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => Some(emptySubst)
80
-
| (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
81
-
unifyArray(Belt.Array.zip(xa, xb))
82
-
| (Schematic({schematic, allowed}), t)
83
-
if !Belt.Set.has(schematicsIn(t), schematic) &&
84
-
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
85
-
Some(singletonSubst(schematic, t))
86
-
| (t, Schematic({schematic, allowed}))
87
-
if !Belt.Set.has(schematicsIn(t), schematic) &&
88
-
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
89
-
Some(singletonSubst(schematic, t))
90
-
| (_, _) => None
91
-
}
92
-
and unifyArray = (a: array<(t, t)>) => {
93
-
if Array.length(a) == 0 {
94
-
Some(emptySubst)
95
-
} else {
96
-
let (x, y) = a[0]->Option.getUnsafe
97
-
switch unifyTerm(x, y) {
98
-
| None => None
99
-
| Some(s1) =>
100
-
switch a
101
-
->Array.sliceToEnd(~start=1)
102
-
->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
103
-
->unifyArray {
104
-
| None => None
105
-
| Some(s2) => Some(combineSubst(s1, s2))
106
-
}
107
-
}
108
-
}
109
-
}
110
-
let unify = (a: t, b: t, ~gen as _=?) => {
111
-
Seq.fromArray(
112
-
switch unifyTerm(a, b) {
113
-
| None => []
114
-
| Some(s) => [s]
115
-
},
116
-
)
117
-
}
118
-
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
119
-
switch term {
120
-
| Symbol(_) => term
121
-
| Compound({subexps}) =>
122
-
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
123
-
| Var({idx: var}) =>
124
-
if var < from {
125
-
term
126
-
} else if var - from < Array.length(substs) && var - from >= 0 {
127
-
Option.getUnsafe(substs[var - from])
128
-
} else {
129
-
Var({idx: var - Array.length(substs)})
130
-
}
131
-
| Schematic({schematic, allowed}) =>
132
-
Schematic({
133
-
schematic,
134
-
allowed: Array.filterMap(allowed, i =>
135
-
if i < from + Array.length(substs) {
136
-
None
137
-
} else {
138
-
Some(i - (from + Array.length(substs)))
139
-
}
140
-
),
141
-
})
142
-
| Ghost => Ghost
143
-
}
144
-
let rec upshift = (term: t, amount: int, ~from: int=0) =>
145
-
switch term {
146
-
| Symbol(_) => term
147
-
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
148
-
| Var({idx}) =>
149
-
Var({
150
-
idx: if idx >= from {
151
-
idx + amount
152
-
} else {
153
-
idx
154
-
},
155
-
})
156
-
| Schematic({schematic, allowed}) =>
157
-
Schematic({
158
-
schematic,
159
-
allowed: Array.map(allowed, i =>
160
-
if i >= from {
161
-
i + amount
162
-
} else {
163
-
i
164
-
}
165
-
),
166
-
})
167
-
| Ghost => Ghost
168
-
}
169
-
let place = (x: int, ~scope: array<string>) => Schematic({
170
-
schematic: x,
171
-
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
172
-
})
173
-
let mergeSubsts = Util.mapUnion
174
-
175
-
type gen = ref<int>
176
-
let seen = (g: gen, s: int) => {
177
-
if s >= g.contents {
178
-
g := s + 1
179
-
}
180
-
}
181
-
let fresh = (g: gen, ~replacing as _=?) => {
182
-
let v = g.contents
183
-
g := g.contents + 1
184
-
v
185
-
}
186
-
let prettyPrintVar = (idx: int, scope: array<string>) => {
187
-
Console.log(("ppVar", "idx", idx, "scope[idx]", scope[idx], "scope", scope))
188
-
switch scope[idx] {
189
-
| Some(n) if Array.indexOf(scope, n) == idx => n
190
-
| _ => "\\"->String.concat(String.make(idx))
191
-
}
192
-
}
193
-
let makeGen = () => {
194
-
ref(0)
1
+
module ConstSymbol: SExpFunc.SYMBOL = {
2
+
type t = string
3
+
let match = (nameA, nameB) => nameA == nameB
4
+
let prettyPrint = (name, ~scope as _: array<string>) => name
5
+
let parse = (string, ~scope as _: array<string>) => Ok((string, ""))
195
6
}
196
-
let rec prettyPrint = (it: t, ~scope: array<string>) =>
197
-
switch it {
198
-
| Symbol({name}) => name
199
-
| Var({idx}) => prettyPrintVar(idx, scope)
200
-
| Schematic({schematic, allowed}) =>
201
-
"?"
202
-
->String.concat(String.make(schematic))
203
-
->String.concat("(")
204
-
->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " "))
205
-
->String.concat(")")
206
-
| Compound({subexps}) =>
207
-
"("
208
-
->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
209
-
->String.concat(")")
210
-
| Ghost => "§SExp.Ghost"
211
-
}
212
7
213
-
let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
214
-
let symbolRegexpString = `^([^\\s()\\[\\]]+)`
215
-
let varRegexpString = "^\\\\([0-9]+)$"
216
-
let schematicRegexpString = "^\\?([0-9]+)$"
217
-
type lexeme = LParen | RParen | VarT(int) | SymbolT(string) | SchematicT(int)
218
-
let nameRES = "^([^\\s.\\[\\]()]+)\\."
219
-
let prettyPrintMeta = (str: string) => {
220
-
String.concat(str, ".")
221
-
}
222
-
let parseMeta = (str: string) => {
223
-
let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
224
-
switch re->RegExp.exec(str->String.trim) {
225
-
| None => Error("not a meta name")
226
-
| Some(res) =>
227
-
switch RegExp.Result.matches(res) {
228
-
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
229
-
| _ => Error("impossible happened")
230
-
}
231
-
}
232
-
}
233
-
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
234
-
let cur = ref(String.make(str))
235
-
let lex: unit => option<lexeme> = () => {
236
-
let str = String.trim(cur.contents)
237
-
cur := str
238
-
let checkVariable = (candidate: string) => {
239
-
let varRegexp = RegExp.fromString(varRegexpString)
240
-
switch Array.indexOf(scope, candidate) {
241
-
| -1 =>
242
-
switch varRegexp->RegExp.exec(candidate) {
243
-
| Some(res') =>
244
-
switch RegExp.Result.matches(res') {
245
-
| [idx] => Some(idx->Int.fromString->Option.getUnsafe)
246
-
| _ => None
247
-
}
248
-
| None => None
249
-
}
250
-
| idx => Some(idx)
251
-
}
252
-
}
253
-
if String.get(str, 0) == Some("(") {
254
-
cur := String.sliceToEnd(str, ~start=1)
255
-
Some(LParen)
256
-
} else if String.get(str, 0) == Some(")") {
257
-
cur := String.sliceToEnd(str, ~start=1)
258
-
Some(RParen)
259
-
} else {
260
-
let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
261
-
switch symbolRegexp->RegExp.exec(str) {
262
-
| None => None
263
-
| Some(res) =>
264
-
switch RegExp.Result.matches(res) {
265
-
| [symb] => {
266
-
cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
267
-
switch checkVariable(symb) {
268
-
| Some(idx) => Some(VarT(idx))
269
-
| None => {
270
-
let schematicRegexp = RegExp.fromString(schematicRegexpString)
271
-
switch schematicRegexp->RegExp.exec(symb) {
272
-
| None => Some(SymbolT(symb))
273
-
| Some(res') =>
274
-
switch RegExp.Result.matches(res') {
275
-
| [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe))
276
-
| _ => Some(SymbolT(symb))
277
-
}
278
-
}
279
-
}
280
-
}
281
-
}
282
-
| _ => None
283
-
}
284
-
}
285
-
}
286
-
}
287
-
288
-
let peek = () => {
289
-
// a bit slow, better would be to keep a backlog of lexed tokens..
290
-
let str = String.make(cur.contents)
291
-
let tok = lex()
292
-
cur := str
293
-
tok
294
-
}
295
-
exception ParseError(string)
296
-
let rec parseExp = () => {
297
-
let tok = peek()
298
-
switch tok {
299
-
| Some(SymbolT(s)) => {
300
-
let _ = lex()
301
-
Some(Symbol({name: s}))
302
-
}
303
-
| Some(VarT(idx)) => {
304
-
let _ = lex()
305
-
Some(Var({idx: idx}))
306
-
}
307
-
| Some(SchematicT(num)) => {
308
-
let _ = lex()
309
-
switch lex() {
310
-
| Some(LParen) => {
311
-
let it = ref(None)
312
-
let bits = []
313
-
let getVar = (t: option<lexeme>) =>
314
-
switch t {
315
-
| Some(VarT(idx)) => Some(idx)
316
-
| _ => None
317
-
}
318
-
while {
319
-
it := lex()
320
-
it.contents->getVar->Option.isSome
321
-
} {
322
-
Array.push(bits, it.contents->getVar->Option.getUnsafe)
323
-
}
324
-
switch it.contents {
325
-
| Some(RParen) =>
326
-
switch gen {
327
-
| Some(g) => {
328
-
seen(g, num)
329
-
Some(Schematic({schematic: num, allowed: bits}))
330
-
}
331
-
| None => throw(ParseError("Schematics not allowed here"))
332
-
}
333
-
| _ => throw(ParseError("Expected closing parenthesis"))
334
-
}
335
-
}
336
-
| _ => throw(ParseError("Expected opening parenthesis"))
337
-
}
338
-
}
339
-
| Some(LParen) => {
340
-
let _ = lex()
341
-
let bits = []
342
-
let it = ref(None)
343
-
while {
344
-
it := parseExp()
345
-
it.contents->Option.isSome
346
-
} {
347
-
Array.push(bits, it.contents->Option.getUnsafe)
348
-
}
349
-
switch lex() {
350
-
| Some(RParen) => Some(Compound({subexps: bits}))
351
-
| _ => throw(ParseError("Expected closing parenthesis"))
352
-
}
353
-
}
354
-
| _ => None
355
-
}
356
-
}
357
-
switch parseExp() {
358
-
| exception ParseError(s) => Error(s)
359
-
| None => Error("No expression to parse")
360
-
| Some(e) => Ok((e, cur.contents))
361
-
}
362
-
}
363
-
364
-
let ghostTerm = Ghost
8
+
include SExpFunc.Make(ConstSymbol)
9
+
let symbol = s => s->ConstSymbol.parse(~scope=[])->Result.getExn->Pair.first->Symbol
10
+
let getSymbol = s => s->ConstSymbol.prettyPrint(~scope=[])
+4
-11
src/SExp.resi
+4
-11
src/SExp.resi
···
1
-
type rec t =
2
-
| Symbol({name: string})
3
-
| Compound({subexps: array<t>})
4
-
| Var({idx: int})
5
-
| Schematic({schematic: int, allowed: array<int>})
6
-
| Ghost
1
+
module ConstSymbol: SExpFunc.SYMBOL
7
2
8
-
include Signatures.TERM
9
-
with type t := t
10
-
and type meta = string
11
-
and type schematic = int
12
-
and type subst = Map.t<int, t>
3
+
include module type of SExpFunc.Make(ConstSymbol)
4
+
let symbol: string => t
5
+
let getSymbol: ConstSymbol.t => string
+396
src/SExpFunc.res
+396
src/SExpFunc.res
···
1
+
module type SYMBOL = {
2
+
type t
3
+
let match: (t, t) => bool
4
+
let prettyPrint: (t, ~scope: array<string>) => string
5
+
let parse: (string, ~scope: array<string>) => result<(t, string), string>
6
+
}
7
+
8
+
module IntCmp = Belt.Id.MakeComparable({
9
+
type t = int
10
+
let cmp = Pervasives.compare
11
+
})
12
+
13
+
module Make = (Symbol: SYMBOL): {
14
+
type rec t =
15
+
| Symbol(Symbol.t)
16
+
| Compound({subexps: array<t>})
17
+
| Var({idx: int})
18
+
| Schematic({schematic: int, allowed: array<int>})
19
+
| Ghost
20
+
module Symbol: SYMBOL with type t := Symbol.t
21
+
include Signatures.TERM
22
+
with type t := t
23
+
and type meta = string
24
+
and type schematic = int
25
+
and type subst = Map.t<int, t>
26
+
} => {
27
+
type rec t =
28
+
| Symbol(Symbol.t)
29
+
| Compound({subexps: array<t>})
30
+
| Var({idx: int})
31
+
| Schematic({schematic: int, allowed: array<int>})
32
+
| Ghost
33
+
module Symbol = Symbol
34
+
type meta = string
35
+
type schematic = int
36
+
type subst = Map.t<schematic, t>
37
+
let substEqual = Util.mapEqual
38
+
let mapSubst = Util.mapMapValues
39
+
let makeSubst = () => {
40
+
Map.make()
41
+
}
42
+
let equivalent = (a: t, b: t) => {
43
+
a == b
44
+
}
45
+
let reduce = (term: t) => term
46
+
let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
47
+
switch it {
48
+
| Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
49
+
| Compound({subexps}) =>
50
+
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
51
+
Belt.Set.union(s, schematicsIn(x))
52
+
)
53
+
| _ => Belt.Set.make(~id=module(IntCmp))
54
+
}
55
+
let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
56
+
switch it {
57
+
| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
58
+
| Compound({subexps}) =>
59
+
subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
60
+
Belt.Set.union(s, freeVarsIn(x))
61
+
)
62
+
| _ => Belt.Set.make(~id=module(IntCmp))
63
+
}
64
+
let rec substitute = (term: t, subst: subst) =>
65
+
switch term {
66
+
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))})
67
+
| Schematic({schematic, _}) =>
68
+
switch Map.get(subst, schematic) {
69
+
| None => term
70
+
| Some(found) => found
71
+
}
72
+
| _ => term
73
+
}
74
+
75
+
let combineSubst = (s: subst, t: subst) => {
76
+
let nu = Map.make()
77
+
Map.entries(s)->Iterator.forEach(opt =>
78
+
switch opt {
79
+
| None => ()
80
+
| Some((key, term)) => nu->Map.set(key, term->substitute(t))
81
+
}
82
+
)
83
+
Map.entries(t)->Iterator.forEach(opt =>
84
+
switch opt {
85
+
| None => ()
86
+
| Some((key, term)) => nu->Map.set(key, term->substitute(s))
87
+
}
88
+
)
89
+
nu
90
+
}
91
+
let emptySubst: subst = Map.make()
92
+
let singletonSubst: (int, t) => subst = (schematic, term) => {
93
+
let s = Map.make()
94
+
s->Map.set(schematic, term)
95
+
s
96
+
}
97
+
let rec unifyTerm = (a: t, b: t) =>
98
+
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)
102
+
| (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
103
+
unifyArray(Belt.Array.zip(xa, xb))
104
+
| (Schematic({schematic, allowed}), t)
105
+
if !Belt.Set.has(schematicsIn(t), schematic) &&
106
+
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
107
+
Some(singletonSubst(schematic, t))
108
+
| (t, Schematic({schematic, allowed}))
109
+
if !Belt.Set.has(schematicsIn(t), schematic) &&
110
+
Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
111
+
Some(singletonSubst(schematic, t))
112
+
| (_, _) => None
113
+
}
114
+
and unifyArray = (a: array<(t, t)>) => {
115
+
if Array.length(a) == 0 {
116
+
Some(emptySubst)
117
+
} else {
118
+
let (x, y) = a[0]->Option.getUnsafe
119
+
switch unifyTerm(x, y) {
120
+
| None => None
121
+
| Some(s1) =>
122
+
switch a
123
+
->Array.sliceToEnd(~start=1)
124
+
->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
125
+
->unifyArray {
126
+
| None => None
127
+
| Some(s2) => Some(combineSubst(s1, s2))
128
+
}
129
+
}
130
+
}
131
+
}
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
+
}
140
+
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
141
+
switch term {
142
+
| Symbol(_) => term
143
+
| Compound({subexps}) =>
144
+
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
145
+
| Var({idx: var}) =>
146
+
if var < from {
147
+
term
148
+
} else if var - from < Array.length(substs) && var - from >= 0 {
149
+
Option.getUnsafe(substs[var - from])
150
+
} else {
151
+
Var({idx: var - Array.length(substs)})
152
+
}
153
+
| Schematic({schematic, allowed}) =>
154
+
Schematic({
155
+
schematic,
156
+
allowed: Array.filterMap(allowed, i =>
157
+
if i < from + Array.length(substs) {
158
+
None
159
+
} else {
160
+
Some(i - (from + Array.length(substs)))
161
+
}
162
+
),
163
+
})
164
+
| Ghost => Ghost
165
+
}
166
+
let rec upshift = (term: t, amount: int, ~from: int=0) =>
167
+
switch term {
168
+
| Symbol(_) => term
169
+
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
170
+
| Var({idx}) =>
171
+
Var({
172
+
idx: if idx >= from {
173
+
idx + amount
174
+
} else {
175
+
idx
176
+
},
177
+
})
178
+
| Schematic({schematic, allowed}) =>
179
+
Schematic({
180
+
schematic,
181
+
allowed: Array.map(allowed, i =>
182
+
if i >= from {
183
+
i + amount
184
+
} else {
185
+
i
186
+
}
187
+
),
188
+
})
189
+
| Ghost => Ghost
190
+
}
191
+
let place = (x: int, ~scope: array<string>) => Schematic({
192
+
schematic: x,
193
+
allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
194
+
})
195
+
let mergeSubsts = Util.mapUnion
196
+
197
+
type gen = ref<int>
198
+
let seen = (g: gen, s: int) => {
199
+
if s >= g.contents {
200
+
g := s + 1
201
+
}
202
+
}
203
+
let fresh = (g: gen, ~replacing as _=?) => {
204
+
let v = g.contents
205
+
g := g.contents + 1
206
+
v
207
+
}
208
+
let prettyPrintVar = (idx: int, scope: array<string>) => {
209
+
switch scope[idx] {
210
+
| Some(n) if Array.indexOf(scope, n) == idx => n
211
+
| _ => "\\"->String.concat(String.make(idx))
212
+
}
213
+
}
214
+
let makeGen = () => {
215
+
ref(0)
216
+
}
217
+
let rec prettyPrint = (it: t, ~scope: array<string>) =>
218
+
switch it {
219
+
| Symbol(name) => Symbol.prettyPrint(name, ~scope)
220
+
| Var({idx}) => prettyPrintVar(idx, scope)
221
+
| Schematic({schematic, allowed}) =>
222
+
"?"
223
+
->String.concat(String.make(schematic))
224
+
->String.concat("(")
225
+
->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " "))
226
+
->String.concat(")")
227
+
| Compound({subexps}) =>
228
+
"("
229
+
->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
230
+
->String.concat(")")
231
+
| Ghost => "§SExp.Ghost"
232
+
}
233
+
234
+
let prettyPrintSubst = (sub, ~scope) =>
235
+
Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope))
236
+
let symbolRegexpString = `^([^\\s()\\[\\]]+)`
237
+
let varRegexpString = "^\\\\([0-9]+)$"
238
+
let schematicRegexpString = "^\\?([0-9]+)$"
239
+
type lexeme = LParen | RParen | VarT(int) | SymbolT(Symbol.t) | SchematicT(int)
240
+
let nameRES = "^([^\\s.\\[\\]()]+)\\."
241
+
let prettyPrintMeta = (str: string) => {
242
+
String.concat(str, ".")
243
+
}
244
+
let parseMeta = (str: string) => {
245
+
let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
246
+
switch re->RegExp.exec(str->String.trim) {
247
+
| None => Error("not a meta name")
248
+
| Some(res) =>
249
+
switch RegExp.Result.matches(res) {
250
+
| [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
251
+
| _ => Error("impossible happened")
252
+
}
253
+
}
254
+
}
255
+
let parse = (str: string, ~scope: array<string>, ~gen=?) => {
256
+
let cur = ref(String.make(str))
257
+
let lex: unit => option<lexeme> = () => {
258
+
let str = String.trim(cur.contents)
259
+
cur := str
260
+
let checkVariable = (candidate: string) => {
261
+
let varRegexp = RegExp.fromString(varRegexpString)
262
+
switch Array.indexOf(scope, candidate) {
263
+
| -1 =>
264
+
switch varRegexp->RegExp.exec(candidate) {
265
+
| Some(res') =>
266
+
switch RegExp.Result.matches(res') {
267
+
| [idx] => Some(idx->Int.fromString->Option.getUnsafe)
268
+
| _ => None
269
+
}
270
+
| None => None
271
+
}
272
+
| idx => Some(idx)
273
+
}
274
+
}
275
+
if String.get(str, 0) == Some("(") {
276
+
cur := String.sliceToEnd(str, ~start=1)
277
+
Some(LParen)
278
+
} else if String.get(str, 0) == Some(")") {
279
+
cur := String.sliceToEnd(str, ~start=1)
280
+
Some(RParen)
281
+
} else {
282
+
let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
283
+
switch symbolRegexp->RegExp.exec(str) {
284
+
| None => None
285
+
| Some(res) =>
286
+
switch RegExp.Result.matches(res) {
287
+
| [symb] => {
288
+
cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
289
+
let parseSymb = () => {
290
+
// FIX: not ideal to throw away symbol error message
291
+
Symbol.parse(symb, ~scope)
292
+
->Util.Result.ok
293
+
->Option.map(((s, rest)) => {
294
+
cur := rest->String.concat(cur.contents)
295
+
SymbolT(s)
296
+
})
297
+
}
298
+
switch checkVariable(symb) {
299
+
| Some(idx) => Some(VarT(idx))
300
+
| None => {
301
+
let schematicRegexp = RegExp.fromString(schematicRegexpString)
302
+
switch schematicRegexp->RegExp.exec(symb) {
303
+
| None => parseSymb()
304
+
| Some(res') =>
305
+
switch RegExp.Result.matches(res') {
306
+
| [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe))
307
+
| _ => parseSymb()
308
+
}
309
+
}
310
+
}
311
+
}
312
+
}
313
+
| _ => None
314
+
}
315
+
}
316
+
}
317
+
}
318
+
319
+
let peek = () => {
320
+
// a bit slow, better would be to keep a backlog of lexed tokens..
321
+
let str = String.make(cur.contents)
322
+
let tok = lex()
323
+
cur := str
324
+
tok
325
+
}
326
+
exception ParseError(string)
327
+
let rec parseExp = () => {
328
+
let tok = peek()
329
+
switch tok {
330
+
| Some(SymbolT(s)) => {
331
+
let _ = lex()
332
+
Some(Symbol(s))
333
+
}
334
+
| Some(VarT(idx)) => {
335
+
let _ = lex()
336
+
Some(Var({idx: idx}))
337
+
}
338
+
| Some(SchematicT(num)) => {
339
+
let _ = lex()
340
+
switch lex() {
341
+
| Some(LParen) => {
342
+
let it = ref(None)
343
+
let bits = []
344
+
let getVar = (t: option<lexeme>) =>
345
+
switch t {
346
+
| Some(VarT(idx)) => Some(idx)
347
+
| _ => None
348
+
}
349
+
while {
350
+
it := lex()
351
+
it.contents->getVar->Option.isSome
352
+
} {
353
+
Array.push(bits, it.contents->getVar->Option.getUnsafe)
354
+
}
355
+
switch it.contents {
356
+
| Some(RParen) =>
357
+
switch gen {
358
+
| Some(g) => {
359
+
seen(g, num)
360
+
Some(Schematic({schematic: num, allowed: bits}))
361
+
}
362
+
| None => throw(ParseError("Schematics not allowed here"))
363
+
}
364
+
| _ => throw(ParseError("Expected closing parenthesis"))
365
+
}
366
+
}
367
+
| _ => throw(ParseError("Expected opening parenthesis"))
368
+
}
369
+
}
370
+
| Some(LParen) => {
371
+
let _ = lex()
372
+
let bits = []
373
+
let it = ref(None)
374
+
while {
375
+
it := parseExp()
376
+
it.contents->Option.isSome
377
+
} {
378
+
Array.push(bits, it.contents->Option.getUnsafe)
379
+
}
380
+
switch lex() {
381
+
| Some(RParen) => Some(Compound({subexps: bits}))
382
+
| _ => throw(ParseError("Expected closing parenthesis"))
383
+
}
384
+
}
385
+
| _ => None
386
+
}
387
+
}
388
+
switch parseExp() {
389
+
| exception ParseError(s) => Error(s)
390
+
| None => Error("No expression to parse")
391
+
| Some(e) => Ok((e, cur.contents))
392
+
}
393
+
}
394
+
395
+
let ghostTerm = Ghost
396
+
}
+2
-1
src/SExpView.res
+2
-1
src/SExpView.res
···
46
46
->React.array}
47
47
</span>
48
48
| Var({idx}) => viewVar({idx, scope})
49
-
| Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
49
+
| Symbol(name) =>
50
+
<span className="term-const"> {React.string(name->SExp.Symbol.prettyPrint(~scope))} </span>
50
51
| Schematic({schematic: s, allowed: vs}) =>
51
52
<span className="term-schematic">
52
53
{React.string("?")}
+13
-9
src/StringAxiomSet.res
+13
-9
src/StringAxiomSet.res
···
32
32
33
33
let getSExpName = (t: SExp.t): option<string> =>
34
34
switch t {
35
-
| Symbol({name}) => Some(name)
35
+
| Symbol(name) => Some(name->SExp.Symbol.prettyPrint(~scope=[]))
36
36
| _ => None
37
37
}
38
38
···
78
78
Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})])
79
79
}
80
80
let lookupGroup = (t: SExp.t): option<int> =>
81
-
mentionedGroups->Array.findIndexOpt(g => t == SExp.Symbol({name: g.name}))
81
+
mentionedGroups->Array.findIndexOpt(g => t == SExp.symbol(g.name))
82
82
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
83
83
let baseIdx = baseIdx + Array.length(rule.vars)
84
84
let inductionHyps =
···
102
102
{
103
103
Rule.vars: [],
104
104
premises: [],
105
-
conclusion: ([StringTerm.Var({idx: xIdx})], Symbol({name: group.name})),
105
+
conclusion: ([StringTerm.Var({idx: xIdx})], SExp.symbol(group.name)),
106
106
},
107
107
],
108
108
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
···
144
144
let grouped: dict<array<Rule.t>> = Dict.make()
145
145
raw->Dict.forEach(rule =>
146
146
switch rule.conclusion->Pair.second {
147
-
| Symbol({name: a}) =>
148
-
switch grouped->Dict.get(a) {
149
-
| None => grouped->Dict.set(a, [rule])
150
-
| Some(rs) => rs->Array.push(rule)
147
+
| Symbol(name) => {
148
+
let name = SExp.getSymbol(name)
149
+
switch grouped->Dict.get(name) {
150
+
| None => grouped->Dict.set(name, [rule])
151
+
| Some(rs) => rs->Array.push(rule)
152
+
}
151
153
}
152
154
| _ => ()
153
155
}
···
178
180
<div
179
181
className={"axiom-set axiom-set-"->String.concat(
180
182
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
181
-
)}>
183
+
)}
184
+
>
182
185
{content
183
186
->Dict.toArray
184
187
->Array.mapWithIndex(((n, r), i) =>
···
186
189
rule={r}
187
190
scope={[]}
188
191
key={String.make(i)}
189
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
192
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
193
+
>
190
194
{React.string(n)}
191
195
</RuleView>
192
196
)
+6
-2
src/StringTerm.res
+6
-2
src/StringTerm.res
···
506
506
let toSExp = t => {
507
507
let convertPiece = p =>
508
508
switch p {
509
-
| String(s) => SExp.Symbol({name: s})
509
+
| String(s) => {
510
+
// FIX: dirty as fuck
511
+
let (s, _) = SExp.Symbol.parse(s, ~scope=[])->Result.getExn
512
+
SExp.Symbol(s)
513
+
}
510
514
| Var({idx}) => SExp.Var({idx: idx})
511
515
| Schematic({schematic, allowed}) => SExp.Schematic({schematic, allowed})
512
516
| Ghost => SExp.ghostTerm
···
519
523
520
524
let rec fromSExp = (t: SExp.t) =>
521
525
switch t {
522
-
| SExp.Symbol({name}) => [String(name)]
526
+
| SExp.Symbol(name) => [String(SExp.Symbol.prettyPrint(name, ~scope=[]))]
523
527
| SExp.Schematic({schematic, allowed}) => [Schematic({schematic, allowed})]
524
528
| SExp.Var({idx}) => [Var({idx: idx})]
525
529
| SExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp)
+8
src/Util.res
+8
src/Util.res
+2
-2
tests/RuleTest.res
+2
-2
tests/RuleTest.res
···
41
41
{
42
42
vars: [],
43
43
premises: [],
44
-
conclusion: ([StringTerm.Var({idx: 0})], Symbol({name: "p"})),
44
+
conclusion: ([StringTerm.Var({idx: 0})], SExp.symbol("p")),
45
45
},
46
46
],
47
47
conclusion: (
48
48
[StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")],
49
-
SExp.Symbol({name: "p"}),
49
+
SExp.symbol("p"),
50
50
),
51
51
},
52
52
)
+5
-7
tests/SExpTest.res
+5
-7
tests/SExpTest.res
···
4
4
module Util = TestUtil.MakeTerm(SExp)
5
5
6
6
zoraBlock("parse symbol", t => {
7
-
t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"})))
8
-
t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"})))
9
-
t->block("judgement terminal", t =>
10
-
t->Util.testParse("a]", Symbol({name: "a"}), ~expectRemaining="]")
11
-
)
7
+
t->block("single char", t => t->Util.testParse("x", symbol("x")))
8
+
t->block("multi char", t => t->Util.testParse("xyz", symbol("xyz")))
9
+
t->block("judgement terminal", t => t->Util.testParse("a]", symbol("a"), ~expectRemaining="]"))
12
10
})
13
11
14
12
zoraBlock("parse var", t => {
···
29
27
30
28
zoraBlock("parse compound", t => {
31
29
t->block("unit", t => t->Util.testParse("()", Compound({subexps: []})))
32
-
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Symbol({name: "a"})]})))
30
+
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [symbol("a")]})))
33
31
t->block("multiple", t => {
34
32
t->Util.testParse(
35
33
"(a \\1 ?1())",
36
34
Compound({
37
-
subexps: [Symbol({name: "a"}), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
35
+
subexps: [symbol("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
38
36
}),
39
37
)
40
38
})
+2
-3
tests/TestUtil.res
+2
-3
tests/TestUtil.res
···
1
1
open Signatures
2
2
open Zora
3
-
open Util
4
3
5
4
let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn
6
5
···
64
63
| Ok((term, "")) => term
65
64
| Ok((_, rest)) => {
66
65
t->fail(~msg="parse incomplete: " ++ rest)
67
-
throw(Unreachable(""))
66
+
throw(Util.Unreachable(""))
68
67
}
69
68
| Error(msg) => {
70
69
t->fail(~msg="parse failed: " ++ msg)
71
-
throw(Unreachable(""))
70
+
throw(Util.Unreachable(""))
72
71
}
73
72
}
74
73
}