the next generation of the in-browser educational proof assistant
implement new string judgment type
+117
-27
+2
-1
src/SExp.res
+2
-1
src/SExp.res
···
8
8
Seq.empty
9
9
}
10
10
let prettyPrint = (name, ~scope as _: array<string>) => name
11
-
let parse = (string, ~scope as _: array<string>) => Ok((string, ""))
11
+
let parse = (string, ~scope as _: array<string>, ~gen as _=?) => Ok((string, ""))
12
+
let substitute = (name, _) => name
12
13
}
13
14
14
15
include SExpFunc.Make(ConstSymbol)
+16
-1
src/SExpFunc.res
+16
-1
src/SExpFunc.res
···
3
3
type subst = Map.t<int, t>
4
4
let unify: (t, t) => Seq.t<subst>
5
5
let prettyPrint: (t, ~scope: array<string>) => string
6
-
let parse: (string, ~scope: array<string>) => result<(t, string), string>
6
+
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
7
+
let substitute: (t, subst) => t
7
8
}
8
9
9
10
module IntCmp = Belt.Id.MakeComparable({
···
69
70
switch Map.get(subst, schematic) {
70
71
| None => term
71
72
| Some(found) => found
73
+
}
74
+
| Symbol(name) => {
75
+
let symbolSubs =
76
+
subst
77
+
->Map.entries
78
+
->Iterator.toArray
79
+
->Array.filterMap(((name, v)) =>
80
+
switch v {
81
+
| Symbol(v) => Some((name, v))
82
+
| _ => None
83
+
}
84
+
)
85
+
->Map.fromArray
86
+
Symbol(name->Symbol.substitute(symbolSubs))
72
87
}
73
88
| _ => term
74
89
}
+2
-3
src/StringTerm.resi
+2
-3
src/StringTerm.resi
···
5
5
| Ghost
6
6
type t = array<piece>
7
7
type subst = Map.t<int, t>
8
+
type gen = ref<int>
8
9
9
10
include Signatures.TERM
10
11
with type t := t
11
12
and type meta = string
12
13
and type schematic = int
13
14
and type subst := subst
14
-
15
-
let fromSExp: SExp.t => t
16
-
let toSExp: t => SExp.t
15
+
and type gen := gen
+88
-21
src/StringTermJudgment.res
+88
-21
src/StringTermJudgment.res
···
1
-
type t = (StringTerm.t, SExp.t)
2
-
type substCodom = StringV(StringTerm.t) | SExpV(SExp.t)
1
+
module StringSymbol: SExpFunc.SYMBOL = {
2
+
type t = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
3
+
type subst = Map.t<int, t>
4
+
type gen = ref<int>
5
+
let parse = (s, ~scope, ~gen: option<gen>=?) => {
6
+
StringTerm.parse(s, ~scope, ~gen?)
7
+
->Result.map(((r, rest)) => (StringS(r), rest))
8
+
->Util.Result.or(() =>
9
+
SExp.ConstSymbol.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
10
+
)
11
+
}
12
+
let prettyPrint = (s, ~scope) =>
13
+
switch s {
14
+
| StringS(s) => StringTerm.prettyPrint(s, ~scope)
15
+
| ConstS(s) => SExp.ConstSymbol.prettyPrint(s, ~scope)
16
+
}
17
+
let unify = (s1, s2) =>
18
+
switch (s1, s2) {
19
+
| (StringS(s1), StringS(s2)) =>
20
+
StringTerm.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
21
+
| (ConstS(s1), ConstS(s2)) =>
22
+
SExp.ConstSymbol.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
23
+
| (_, _) => Seq.empty
24
+
}
25
+
let substitute = (s, subst: subst) =>
26
+
switch s {
27
+
| StringS(s) => {
28
+
let stringSubs = subst->Util.mapMapValues(v =>
29
+
switch v {
30
+
| StringS(s) => s
31
+
| _ => throw(Util.Unreachable("const should not have map values"))
32
+
}
33
+
)
34
+
StringS(StringTerm.substitute(s, stringSubs))
35
+
}
36
+
| ConstS(s) => ConstS(s)
37
+
}
38
+
}
39
+
module StringSExp = SExpFunc.Make(StringSymbol)
40
+
41
+
let toSExp = (t: StringTerm.t): StringSExp.t => {
42
+
let convertPiece = (p: StringTerm.piece): StringSExp.t =>
43
+
switch p {
44
+
| StringTerm.String(s) => {
45
+
let (s, _) = StringSymbol.parse(s, ~scope=[])->Result.getExn
46
+
StringSExp.Symbol(s)
47
+
}
48
+
| StringTerm.Var({idx}) => StringSExp.Var({idx: idx})
49
+
| StringTerm.Schematic({schematic, allowed}) => StringSExp.Schematic({schematic, allowed})
50
+
| StringTerm.Ghost => StringSExp.ghostTerm
51
+
}
52
+
switch Array.length(t) {
53
+
| 1 => convertPiece(t[0]->Option.getExn)
54
+
| _ => StringSExp.Compound({subexps: Array.map(t, convertPiece)})
55
+
}
56
+
}
57
+
58
+
let rec fromSExp = (t: StringSExp.t): StringTerm.t =>
59
+
switch t {
60
+
| StringSExp.Symbol(name) => [StringTerm.String(StringSymbol.prettyPrint(name, ~scope=[]))]
61
+
| StringSExp.Schematic({schematic, allowed}) => [StringTerm.Schematic({schematic, allowed})]
62
+
| StringSExp.Var({idx}) => [StringTerm.Var({idx: idx})]
63
+
| StringSExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp)
64
+
| StringSExp.Ghost => [StringTerm.Ghost]
65
+
}
66
+
67
+
type t = (StringTerm.t, StringSExp.t)
68
+
type substCodom = StringV(StringTerm.t) | SExpV(StringSExp.t)
3
69
type subst = Map.t<int, substCodom>
4
70
type schematic = int
5
71
type meta = string
6
72
7
73
let mapSubst = Util.mapMapValues
8
74
let mergeSubsts: (subst, subst) => subst = Util.mapUnion
9
-
let splitSub: subst => (StringTerm.subst, SExp.subst) = s => {
75
+
let splitSub: subst => (StringTerm.subst, StringSExp.subst) = s => {
10
76
let stringSub = Map.make()
11
77
let judgeSub = Map.make()
12
78
s->Map.forEachWithKey((v, k) => {
13
79
switch v {
14
80
| StringV(t) => {
15
81
stringSub->Map.set(k, t)
16
-
judgeSub->Map.set(k, t->StringTerm.toSExp)
82
+
judgeSub->Map.set(k, t->toSExp)
17
83
}
18
84
| SExpV(t) => {
19
-
stringSub->Map.set(k, t->StringTerm.fromSExp)
85
+
stringSub->Map.set(k, t->fromSExp)
20
86
judgeSub->Map.set(k, t)
21
87
}
22
88
}
···
25
91
}
26
92
let substitute = ((term, judge): t, sub) => {
27
93
let (stringSub, judgeSub) = splitSub(sub)
28
-
(StringTerm.substitute(term, stringSub), SExp.substitute(judge, judgeSub))
94
+
(StringTerm.substitute(term, stringSub), StringSExp.substitute(judge, judgeSub))
29
95
}
30
96
31
97
let substituteSubstCodom = (s: substCodom, subst: subst) => {
32
98
let (stringSub, judgeSub) = splitSub(subst)
33
99
switch s {
34
100
| StringV(t) => StringV(StringTerm.substitute(t, stringSub))
35
-
| SExpV(t) => SExpV(SExp.substitute(t, judgeSub))
101
+
| SExpV(t) => SExpV(StringSExp.substitute(t, judgeSub))
36
102
}
37
103
}
38
104
let equivalent = ((t1, j1): t, (t2, j2): t) =>
39
-
StringTerm.equivalent(t1, t2) && SExp.equivalent(j1, j2)
105
+
StringTerm.equivalent(t1, t2) && StringSExp.equivalent(j1, j2)
40
106
let reduce = t => t
41
107
let unify = ((t1, j1): t, (t2, j2): t, ~gen as _=?) => {
42
108
// cartesian prod of possible unifications
43
-
let judgeSubs = SExp.unify(j1, j2)->Seq.map(s => s->Util.mapMapValues(t => SExpV(t)))
109
+
let judgeSubs = StringSExp.unify(j1, j2)->Seq.map(s => s->Util.mapMapValues(t => SExpV(t)))
44
110
let stringSubs = StringTerm.unify(t1, t2)->Seq.map(s => s->Util.mapMapValues(t => StringV(t)))
45
111
judgeSubs->Seq.flatMap(judgeSub =>
46
112
// NOTE: silent failure mode here where substitution exists for a given schematic on both string
···
54
120
let stringScope = scope->Array.map(v =>
55
121
switch v {
56
122
| StringV(t) => t
57
-
| SExpV(t) => StringTerm.fromSExp(t)
123
+
| SExpV(t) => fromSExp(t)
58
124
}
59
125
)
60
126
let judgeScope = scope->Array.map(v =>
61
127
switch v {
62
128
| SExpV(t) => t
63
-
| StringV(t) => StringTerm.toSExp(t)
129
+
| StringV(t) => toSExp(t)
64
130
}
65
131
)
66
-
(StringTerm.substDeBruijn(t, stringScope, ~from), SExp.substDeBruijn(j, judgeScope, ~from))
132
+
(StringTerm.substDeBruijn(t, stringScope, ~from), StringSExp.substDeBruijn(j, judgeScope, ~from))
67
133
}
68
134
let upshift = ((t, j): t, amount: int, ~from: int=0) => (
69
135
StringTerm.upshift(t, amount, ~from),
70
-
SExp.upshift(j, amount, ~from),
136
+
StringSExp.upshift(j, amount, ~from),
71
137
)
72
138
73
139
let upshiftSubstCodom = (v: substCodom, amount: int, ~from: int=0) =>
74
140
switch v {
75
141
| StringV(t) => StringV(StringTerm.upshift(t, amount, ~from))
76
-
| SExpV(j) => SExpV(SExp.upshift(j, amount, ~from))
142
+
| SExpV(j) => SExpV(StringSExp.upshift(j, amount, ~from))
77
143
}
78
144
79
145
let mapTerms = ((t, j): t, f: StringTerm.t => StringTerm.t): t => {
80
146
// Apply the function to both the string term and the sexp (converted to/from string term)
81
147
let newT = f(t)
82
-
let newJ = j->StringTerm.fromSExp->f->StringTerm.toSExp
148
+
// FIX: is this necessary? is mapTerms even used?
149
+
let newJ = j->fromSExp->f->toSExp
83
150
(newT, newJ)
84
151
}
85
152
86
-
let parse = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => {
153
+
let parse = (str: string, ~scope: array<string>, ~gen: option<ref<int>>=?) => {
87
154
StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) =>
88
-
SExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str))
155
+
StringSExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str))
89
156
)
90
157
}
91
158
···
97
164
switch StringTerm.parse(str, ~scope, ~gen?) {
98
165
| Ok(t, str) => Ok(StringV(t), str)
99
166
| Error(stringE) =>
100
-
switch SExp.parse(str, ~scope) {
167
+
switch StringSExp.parse(str, ~scope) {
101
168
| Ok(t, str) => Ok(SExpV(t), str)
102
169
| Error(sExpE) =>
103
170
Error(
···
108
175
}
109
176
110
177
let prettyPrint = ((t, j): t, ~scope: array<StringTerm.meta>) =>
111
-
`${StringTerm.prettyPrint(t, ~scope)} ${SExp.prettyPrint(j, ~scope)}`
178
+
`${StringTerm.prettyPrint(t, ~scope)} ${StringSExp.prettyPrint(j, ~scope)}`
112
179
let prettyPrintSubstCodom = (v: substCodom, ~scope: array<StringTerm.meta>) =>
113
180
switch v {
114
181
| StringV(t) => StringTerm.prettyPrint(t, ~scope)
115
-
| SExpV(t) => SExp.prettyPrint(t, ~scope)
182
+
| SExpV(t) => StringSExp.prettyPrint(t, ~scope)
116
183
}
117
184
118
-
let ghostJudgment = (StringTerm.ghostTerm, SExp.ghostTerm)
185
+
let ghostJudgment = (StringTerm.ghostTerm, StringSExp.ghostTerm)
+4
-1
src/StringTermJudgment.resi
+4
-1
src/StringTermJudgment.resi