the next generation of the in-browser educational proof assistant
rename symbol -> atom
+72
-72
+2
-2
src/SExp.res
+2
-2
src/SExp.res
···
1
-
module ConstSymbol: SExpFunc.SYMBOL with type t = string = {
1
+
module SymbolAtom: SExpFunc.ATOM with type t = string = {
2
2
type t = string
3
3
type subst = Map.t<int, string>
4
4
let unify = (a, b) =>
···
23
23
let upshift = (t, _, ~from as _=?) => t
24
24
}
25
25
26
-
include SExpFunc.Make(ConstSymbol)
26
+
include SExpFunc.Make(SymbolAtom)
+3
-3
src/SExp.resi
+3
-3
src/SExp.resi
···
1
1
// NOTE: ideally we want something like:
2
-
// include module type of SExpFunc.Make(ConstSymbol)
2
+
// include module type of SExpFunc.Make(ConstAtom)
3
3
// this doesn't work because reasons. can come back to revisit
4
4
// but i honestly suspect this is a rescript compiler bug.
5
5
6
-
module Symbol: SExpFunc.SYMBOL with type t = string
6
+
module Atom: SExpFunc.ATOM with type t = string
7
7
type rec t =
8
-
| Symbol(Symbol.t)
8
+
| Atom(Atom.t)
9
9
| Compound({subexps: array<t>})
10
10
| Var({idx: int})
11
11
| Schematic({schematic: int, allowed: array<int>})
+26
-26
src/SExpFunc.res
+26
-26
src/SExpFunc.res
···
1
-
module type SYMBOL = {
1
+
module type ATOM = {
2
2
type t
3
3
type subst = Map.t<int, t>
4
4
let unify: (t, t) => Seq.t<subst>
···
19
19
let cmp = Pervasives.compare
20
20
})
21
21
22
-
module Make = (Symbol: SYMBOL): {
23
-
module Symbol: SYMBOL with type t = Symbol.t
22
+
module Make = (Atom: ATOM): {
23
+
module Atom: ATOM with type t = Atom.t
24
24
25
25
type rec t =
26
-
| Symbol(Symbol.t)
26
+
| Atom(Atom.t)
27
27
| Compound({subexps: array<t>})
28
28
| Var({idx: int})
29
29
| Schematic({schematic: int, allowed: array<int>})
···
37
37
let mapTerms: (t, t => t) => t
38
38
} => {
39
39
type rec t =
40
-
| Symbol(Symbol.t)
40
+
| Atom(Atom.t)
41
41
| Compound({subexps: array<t>})
42
42
| Var({idx: int})
43
43
| Schematic({schematic: int, allowed: array<int>})
44
44
| Ghost
45
-
module Symbol = Symbol
45
+
module Atom = Atom
46
46
type meta = string
47
47
type schematic = int
48
48
type subst = Map.t<schematic, t>
···
81
81
| None => term
82
82
| Some(found) => found
83
83
}
84
-
| Symbol(name) => {
84
+
| Atom(name) => {
85
85
let symbolSubs =
86
86
subst
87
87
->Map.entries
88
88
->Iterator.toArray
89
89
->Array.filterMap(((name, v)) =>
90
90
switch v {
91
-
| Symbol(v) => Some((name, v))
91
+
| Atom(v) => Some((name, v))
92
92
| _ => None
93
93
}
94
94
)
95
95
->Map.fromArray
96
-
Symbol(name->Symbol.substitute(symbolSubs))
96
+
Atom(name->Atom.substitute(symbolSubs))
97
97
}
98
98
| _ => term
99
99
}
···
122
122
}
123
123
let rec unifyTerm = (a: t, b: t): Seq.t<subst> =>
124
124
switch (a, b) {
125
-
| (Symbol(na), Symbol(nb)) =>
126
-
Symbol.unify(na, nb)->Seq.map(subst => subst->Util.mapMapValues(v => Symbol(v)))
125
+
| (Atom(na), Atom(nb)) =>
126
+
Atom.unify(na, nb)->Seq.map(subst => subst->Util.mapMapValues(v => Atom(v)))
127
127
| (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
128
128
unifyArray(Belt.Array.zip(xa, xb))
129
129
| (Var({idx: ia}), Var({idx: ib})) if ia == ib => Seq.once(emptySubst)
···
155
155
}
156
156
let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b)
157
157
158
-
let rec lower = (term: t): Symbol.t =>
158
+
let rec lower = (term: t): Atom.t =>
159
159
switch term {
160
-
| Symbol(s) => s
161
-
| Var({idx}) => Symbol.lowerVar(idx)
162
-
| Schematic({schematic, allowed}) => Symbol.lowerSchematic(schematic, allowed)
160
+
| Atom(s) => s
161
+
| Var({idx}) => Atom.lowerVar(idx)
162
+
| Schematic({schematic, allowed}) => Atom.lowerSchematic(schematic, allowed)
163
163
| Compound({subexps: [e1]}) => lower(e1)
164
-
| _ => Symbol.ghost
164
+
| _ => Atom.ghost
165
165
}
166
166
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
167
167
switch term {
168
-
| Symbol(s) => {
168
+
| Atom(s) => {
169
169
let symbolSubsts = substs->Array.map(lower)
170
-
Symbol(Symbol.substDeBruijn(s, symbolSubsts, ~from))
170
+
Atom(Atom.substDeBruijn(s, symbolSubsts, ~from))
171
171
}
172
172
173
173
| Compound({subexps}) =>
···
195
195
}
196
196
let rec upshift = (term: t, amount: int, ~from: int=0) =>
197
197
switch term {
198
-
| Symbol(s) => Symbol(s->Symbol.upshift(amount, ~from))
198
+
| Atom(s) => Atom(s->Atom.upshift(amount, ~from))
199
199
| Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
200
200
| Var({idx}) =>
201
201
Var({
···
246
246
}
247
247
let rec prettyPrint = (it: t, ~scope: array<string>) =>
248
248
switch it {
249
-
| Symbol(name) => Symbol.prettyPrint(name, ~scope)
249
+
| Atom(name) => Atom.prettyPrint(name, ~scope)
250
250
| Var({idx}) => prettyPrintVar(idx, scope)
251
251
| Schematic({schematic, allowed}) =>
252
252
"?"
···
266
266
let symbolRegexpString = `^([^\\s()\\[\\]]+)`
267
267
let varRegexpString = "^\\\\([0-9]+)$"
268
268
let schematicRegexpString = "^\\?([0-9]+)$"
269
-
type lexeme = LParen | RParen | VarT(int) | SymbolT(Symbol.t) | SchematicT(int)
269
+
type lexeme = LParen | RParen | VarT(int) | AtomT(Atom.t) | SchematicT(int)
270
270
let nameRES = "^([^\\s.\\[\\]()]+)\\."
271
271
let prettyPrintMeta = (str: string) => {
272
272
String.concat(str, ".")
···
322
322
let regularSymb = () => {
323
323
// FIX: not ideal to throw away symbol error message
324
324
Console.log(("current", cur.contents))
325
-
Symbol.parse(cur.contents, ~scope)
325
+
Atom.parse(cur.contents, ~scope)
326
326
->Util.Result.ok
327
327
->Option.map(((s, rest)) => {
328
328
cur := rest
329
329
Console.log(("parsed", s, cur.contents))
330
-
SymbolT(s)
330
+
AtomT(s)
331
331
})
332
332
}
333
333
switch checkVariable(symb) {
···
362
362
let rec parseExp = () => {
363
363
let tok = peek()
364
364
switch tok {
365
-
| Some(SymbolT(s)) => {
365
+
| Some(AtomT(s)) => {
366
366
let _ = lex()
367
-
Some(Symbol(s))
367
+
Some(Atom(s))
368
368
}
369
369
| Some(VarT(idx)) => {
370
370
let _ = lex()
···
431
431
let rec unifiesWithAnything = t =>
432
432
switch t {
433
433
| Schematic(_) => true
434
-
| Symbol(s) => Symbol.unifiesWithAnything(s)
434
+
| Atom(s) => Atom.unifiesWithAnything(s)
435
435
| Compound({subexps}) => subexps->Array.every(unifiesWithAnything)
436
436
| _ => false
437
437
}
+3
-3
src/SExpView.res
+3
-3
src/SExpView.res
···
1
-
module ConstSymbol = SExp.Symbol
2
-
module ConstSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := SExp.Symbol = {
1
+
module ConstAtom = SExp.Atom
2
+
module ConstAtomView: SExpViewFunc.ATOM_VIEW with module Atom := SExp.Atom = {
3
3
type props = {name: string, scope: array<string>}
4
4
let make = (props: props) => React.string(props.name)
5
5
}
6
6
7
-
include SExpViewFunc.Make(ConstSymbol, ConstSymbolView, SExp)
7
+
include SExpViewFunc.Make(ConstAtom, ConstAtomView, SExp)
+1
-1
src/SExpView.resi
+1
-1
src/SExpView.resi
+8
-8
src/SExpViewFunc.res
+8
-8
src/SExpViewFunc.res
···
1
-
module type SYMBOL_VIEW = {
2
-
module Symbol: SExpFunc.SYMBOL
3
-
type props = {name: Symbol.t, scope: array<string>}
1
+
module type ATOM_VIEW = {
2
+
module Atom: SExpFunc.ATOM
3
+
type props = {name: Atom.t, scope: array<string>}
4
4
let make: props => React.element
5
5
}
6
6
7
7
module Make = (
8
-
Symbol: SExpFunc.SYMBOL,
9
-
SymbolView: SYMBOL_VIEW with module Symbol := Symbol,
8
+
Atom: SExpFunc.ATOM,
9
+
AtomView: ATOM_VIEW with module Atom := Atom,
10
10
SExp: {
11
11
type rec t =
12
-
| Symbol(Symbol.t)
12
+
| Atom(Atom.t)
13
13
| Compound({subexps: array<t>})
14
14
| Var({idx: int})
15
15
| Schematic({schematic: int, allowed: array<int>})
···
72
72
->React.array}
73
73
</span>
74
74
| Var({idx}) => viewVar({idx, scope})
75
-
| Symbol(name) =>
75
+
| Atom(name) =>
76
76
<span className="term-const">
77
-
<SymbolView name scope />
77
+
<AtomView name scope />
78
78
</span>
79
79
| Schematic({schematic: s, allowed: vs}) =>
80
80
<span className="term-schematic">
+7
-7
src/StringAxiomSet.res
+7
-7
src/StringAxiomSet.res
···
33
33
34
34
let getSExpName = (t: SExp.t): option<string> =>
35
35
switch t {
36
-
| Symbol(name) => Some(name->SExp.Symbol.prettyPrint(~scope=[]))
36
+
| Atom(name) => Some(name->SExp.Atom.prettyPrint(~scope=[]))
37
37
| _ => None
38
38
}
39
39
40
40
open StringSExp
41
41
let destructure = (r: Judgment.t): (StringTerm.t, string) =>
42
42
switch r {
43
-
| Compound({subexps: [Symbol(StringS(s)), Symbol(ConstS(name))]}) => (s, name)
43
+
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name)
44
44
| _ => throw(Util.Unreachable("expected valid induction rule"))
45
45
}
46
46
let destructureOpt = (r: Judgment.t): option<(StringTerm.t, string)> =>
47
47
switch r {
48
-
| Compound({subexps: [Symbol(StringS(s)), Symbol(ConstS(name))]}) => Some((s, name))
48
+
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name))
49
49
| _ => None
50
50
}
51
51
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): Judgment.t => Compound({
···
110
110
vars: rule.vars,
111
111
premises: rule.premises->Array.concat(inductionHyps),
112
112
conclusion: structure(
113
-
surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringS->Symbol,
113
+
surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringS->Atom,
114
114
Var({idx: pIdx + baseIdx}),
115
115
),
116
116
}
···
122
122
{
123
123
Rule.vars: [],
124
124
premises: [],
125
-
conclusion: structure(Var({idx: xIdx}), Symbol(ConstS(group.name))),
125
+
conclusion: structure(Var({idx: xIdx}), Atom(ConstS(group.name))),
126
126
},
127
127
],
128
128
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
129
129
),
130
130
conclusion: structure(
131
-
surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx)->StringS->Symbol,
131
+
surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
132
132
Var({idx: 0}),
133
133
), // TODO: clean here
134
134
}
···
167
167
let grouped: dict<array<Rule.t>> = Dict.make()
168
168
raw->Dict.forEach(rule =>
169
169
switch rule.conclusion {
170
-
| Compound({subexps: [Symbol(StringS(_)), Symbol(ConstS(name))]}) =>
170
+
| Compound({subexps: [Atom(StringS(_)), Atom(ConstS(name))]}) =>
171
171
switch grouped->Dict.get(name) {
172
172
| None => grouped->Dict.set(name, [rule])
173
173
| Some(rs) => rs->Array.push(rule)
+7
-7
src/StringSExp.res
+7
-7
src/StringSExp.res
···
1
-
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.Symbol.t)
1
+
type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t)
2
2
3
-
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol = {
4
-
type t = stringSymbol
3
+
module StringAtom: SExpFunc.ATOM with type t = stringAtom = {
4
+
type t = stringAtom
5
5
type subst = Map.t<int, t>
6
6
type gen = ref<int>
7
7
let parse = (s, ~scope, ~gen: option<gen>=?) => {
8
8
StringTerm.parse(s, ~scope, ~gen?)
9
9
->Result.map(((r, rest)) => (StringS(r), rest))
10
10
->Util.Result.or(() =>
11
-
SExp.Symbol.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
11
+
SExp.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
12
)
13
13
}
14
14
let prettyPrint = (s, ~scope) =>
15
15
switch s {
16
16
| StringS(s) => StringTerm.prettyPrint(s, ~scope)
17
-
| ConstS(s) => SExp.Symbol.prettyPrint(s, ~scope)
17
+
| ConstS(s) => SExp.Atom.prettyPrint(s, ~scope)
18
18
}
19
19
let unify = (s1, s2) =>
20
20
switch (s1, s2) {
21
21
| (StringS(s1), StringS(s2)) =>
22
22
StringTerm.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
23
| (ConstS(s1), ConstS(s2)) =>
24
-
SExp.Symbol.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
24
+
SExp.Atom.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
25
25
| (_, _) => Seq.empty
26
26
}
27
27
let substitute = (s, subst: subst) =>
···
65
65
}
66
66
}
67
67
68
-
include SExpFunc.Make(StringSymbol)
68
+
include SExpFunc.Make(StringAtom)
+4
-4
src/StringSExp.resi
+4
-4
src/StringSExp.resi
···
1
-
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.Symbol.t)
2
-
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol
1
+
type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t)
2
+
module StringAtom: SExpFunc.ATOM with type t = stringAtom
3
3
4
4
type rec t =
5
-
| Symbol(StringSymbol.t)
5
+
| Atom(StringAtom.t)
6
6
| Compound({subexps: array<t>})
7
7
| Var({idx: int})
8
8
| Schematic({schematic: int, allowed: array<int>})
···
14
14
and type schematic = int
15
15
and type subst = Map.t<int, t>
16
16
17
-
module Symbol: SExpFunc.SYMBOL with type t := StringSymbol.t
17
+
module Atom: SExpFunc.ATOM with type t := StringAtom.t
18
18
let mapTerms: (t, t => t) => t
+4
-4
src/StringTermJView.res
+4
-4
src/StringTermJView.res
···
1
-
module StringSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := StringSExp.StringSymbol = {
2
-
type props = {name: StringSExp.StringSymbol.t, scope: array<string>}
1
+
module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringAtom = {
2
+
type props = {name: StringSExp.StringAtom.t, scope: array<string>}
3
3
let make = ({name, scope}: props) =>
4
4
switch name {
5
5
| StringSExp.StringS(term) => <StringTermView term scope />
6
-
| StringSExp.ConstS(name) => <SExpView.ConstSymbolView name scope />
6
+
| StringSExp.ConstS(name) => <SExpView.ConstAtomView name scope />
7
7
}
8
8
}
9
9
10
-
module View = SExpViewFunc.Make(StringSExp.StringSymbol, StringSymbolView, StringSExp)
10
+
module View = SExpViewFunc.Make(StringSExp.StringAtom, StringAtomView, StringSExp)
11
11
12
12
module TermView = View
13
13
type props = {
+2
-2
tests/RuleTest.res
+2
-2
tests/RuleTest.res
···
43
43
// premises: [],
44
44
// conclusion: StringSExp.Compound(
45
45
// [StringTerm.Var({idx: 0})],
46
-
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringSExp.Symbol,
46
+
// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom,
47
47
// ),
48
48
// },
49
49
// ],
50
50
// conclusion: (
51
51
// [StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")],
52
-
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringSExp.Symbol,
52
+
// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom,
53
53
// ),
54
54
// },
55
55
// )
+5
-5
tests/SExpTest.res
+5
-5
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("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="]"))
7
+
t->block("single char", t => t->Util.testParse("x", Atom("x")))
8
+
t->block("multi char", t => t->Util.testParse("xyz", Atom("xyz")))
9
+
t->block("judgement terminal", t => t->Util.testParse("a]", Atom("a"), ~expectRemaining="]"))
10
10
})
11
11
12
12
zoraBlock("parse var", t => {
···
27
27
28
28
zoraBlock("parse compound", t => {
29
29
t->block("unit", t => t->Util.testParse("()", Compound({subexps: []})))
30
-
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Symbol("a")]})))
30
+
t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Atom("a")]})))
31
31
t->block("multiple", t => {
32
32
t->Util.testParse(
33
33
"(a \\1 ?1())",
34
34
Compound({
35
-
subexps: [Symbol("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
35
+
subexps: [Atom("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})],
36
36
}),
37
37
)
38
38
})