the next generation of the in-browser educational proof assistant
remove redundant StringTermJudgment
+6
-164
+1
-12
src/StringTermJView.res
+1
-12
src/StringTermJView.res
···
10
10
}
11
11
12
12
module TermView = StringTermView
13
-
type props = {
14
-
judgment: StringTermJudgment.t,
15
-
scope: array<string>,
16
-
}
17
-
module SExpView = SExpViewFunc.Make(
13
+
include SExpViewFunc.Make(
18
14
StringTermJudgment.StringSymbol,
19
15
StringSymbolView,
20
16
StringTermJudgment.StringSExp,
21
17
)
22
-
let make = ({judgment: (term, j), scope}) => {
23
-
<span className="term-compound">
24
-
<StringTermView term scope />
25
-
{React.string(" ")}
26
-
<SExpView term=j scope />
27
-
</span>
28
-
}
+1
-1
src/StringTermJView.resi
+1
-1
src/StringTermJView.resi
+2
-147
src/StringTermJudgment.res
+2
-147
src/StringTermJudgment.res
···
43
43
| ConstS(s) => SExp.ConstSymbol.constSymbol(s)
44
44
}
45
45
}
46
-
module StringSExp = SExpFunc.Make(StringSymbol)
47
-
let constSymbol = (s: string): StringSExp.t => StringSExp.Symbol(ConstS(SExp.pSymbol(s)))
48
-
49
-
let toSExp = (t: StringTerm.t): StringSExp.t => {
50
-
let convertPiece = (p: StringTerm.piece): StringSExp.t =>
51
-
switch p {
52
-
| StringTerm.String(s) => {
53
-
let (s, _) = StringSymbol.parse(s, ~scope=[])->Result.getExn
54
-
StringSExp.Symbol(s)
55
-
}
56
-
| StringTerm.Var({idx}) => StringSExp.Var({idx: idx})
57
-
| StringTerm.Schematic({schematic, allowed}) => StringSExp.Schematic({schematic, allowed})
58
-
| StringTerm.Ghost => StringSExp.ghostTerm
59
-
}
60
-
switch Array.length(t) {
61
-
| 1 => convertPiece(t[0]->Option.getExn)
62
-
| _ => StringSExp.Compound({subexps: Array.map(t, convertPiece)})
63
-
}
64
-
}
65
46
66
-
let rec fromSExp = (t: StringSExp.t): StringTerm.t =>
67
-
switch t {
68
-
| StringSExp.Symbol(name) => [StringTerm.String(StringSymbol.prettyPrint(name, ~scope=[]))]
69
-
| StringSExp.Schematic({schematic, allowed}) => [StringTerm.Schematic({schematic, allowed})]
70
-
| StringSExp.Var({idx}) => [StringTerm.Var({idx: idx})]
71
-
| StringSExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp)
72
-
| StringSExp.Ghost => [StringTerm.Ghost]
73
-
}
74
-
75
-
type t = (StringTerm.t, StringSExp.t)
76
-
type substCodom = StringV(StringTerm.t) | SExpV(StringSExp.t)
77
-
type subst = Map.t<int, substCodom>
78
-
type schematic = int
79
-
type meta = string
80
-
81
-
let mapSubst = Util.mapMapValues
82
-
let mergeSubsts: (subst, subst) => subst = Util.mapUnion
83
-
let splitSub: subst => (StringTerm.subst, StringSExp.subst) = s => {
84
-
let stringSub = Map.make()
85
-
let judgeSub = Map.make()
86
-
s->Map.forEachWithKey((v, k) => {
87
-
switch v {
88
-
| StringV(t) => {
89
-
stringSub->Map.set(k, t)
90
-
judgeSub->Map.set(k, t->toSExp)
91
-
}
92
-
| SExpV(t) => {
93
-
stringSub->Map.set(k, t->fromSExp)
94
-
judgeSub->Map.set(k, t)
95
-
}
96
-
}
97
-
})
98
-
(stringSub, judgeSub)
99
-
}
100
-
let substitute = ((term, judge): t, sub) => {
101
-
let (stringSub, judgeSub) = splitSub(sub)
102
-
(StringTerm.substitute(term, stringSub), StringSExp.substitute(judge, judgeSub))
103
-
}
104
-
105
-
let substituteSubstCodom = (s: substCodom, subst: subst) => {
106
-
let (stringSub, judgeSub) = splitSub(subst)
107
-
switch s {
108
-
| StringV(t) => StringV(StringTerm.substitute(t, stringSub))
109
-
| SExpV(t) => SExpV(StringSExp.substitute(t, judgeSub))
110
-
}
111
-
}
112
-
let equivalent = ((t1, j1): t, (t2, j2): t) =>
113
-
StringTerm.equivalent(t1, t2) && StringSExp.equivalent(j1, j2)
114
-
let reduce = t => t
115
-
let unify = ((t1, j1): t, (t2, j2): t, ~gen as _=?) => {
116
-
// cartesian prod of possible unifications
117
-
let judgeSubs = StringSExp.unify(j1, j2)->Seq.map(s => s->Util.mapMapValues(t => SExpV(t)))
118
-
let stringSubs = StringTerm.unify(t1, t2)->Seq.map(s => s->Util.mapMapValues(t => StringV(t)))
119
-
judgeSubs->Seq.flatMap(judgeSub =>
120
-
// NOTE: silent failure mode here where substitution exists for a given schematic on both string
121
-
// SExp side. for now, bias string sub. in future, maybe consider this not a valid judgement to begin with.
122
-
stringSubs->Seq.map(stringSub => Util.mapUnion(stringSub, judgeSub))
123
-
)
124
-
}
125
-
let substDeBruijn = ((t, j): t, scope: array<substCodom>, ~from: int=0) => {
126
-
// NOTE: implicit type coercion here. if we unify and expect a string but get an sexp,
127
-
// perform naive flattening of compound to substitute. likewise in opposite direction.
128
-
let stringScope = scope->Array.map(v =>
129
-
switch v {
130
-
| StringV(t) => t
131
-
| SExpV(t) => fromSExp(t)
132
-
}
133
-
)
134
-
let judgeScope = scope->Array.map(v =>
135
-
switch v {
136
-
| SExpV(t) => t
137
-
| StringV(t) => toSExp(t)
138
-
}
139
-
)
140
-
(StringTerm.substDeBruijn(t, stringScope, ~from), StringSExp.substDeBruijn(j, judgeScope, ~from))
141
-
}
142
-
let upshift = ((t, j): t, amount: int, ~from: int=0) => (
143
-
StringTerm.upshift(t, amount, ~from),
144
-
StringSExp.upshift(j, amount, ~from),
145
-
)
146
-
147
-
let upshiftSubstCodom = (v: substCodom, amount: int, ~from: int=0) =>
148
-
switch v {
149
-
| StringV(t) => StringV(StringTerm.upshift(t, amount, ~from))
150
-
| SExpV(j) => SExpV(StringSExp.upshift(j, amount, ~from))
151
-
}
152
-
153
-
let mapTerms = ((t, j): t, f: StringTerm.t => StringTerm.t): t => {
154
-
// Apply the function to both the string term and the sexp (converted to/from string term)
155
-
let newT = f(t)
156
-
// FIX: is this necessary? is mapTerms even used?
157
-
let newJ = j->fromSExp->f->toSExp
158
-
(newT, newJ)
159
-
}
160
-
161
-
let parse = (str: string, ~scope: array<string>, ~gen: option<ref<int>>=?) => {
162
-
StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) =>
163
-
StringSExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str))
164
-
)
165
-
}
166
-
167
-
// HACK: this does work due to the hacky string-sexp conversion we have inplace with substitutions,
168
-
// but a different solution would be preferable
169
-
let placeSubstCodom = (x: int, ~scope: array<string>) => StringV(StringTerm.place(x, ~scope))
170
-
171
-
let parseSubstCodom = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => {
172
-
switch StringTerm.parse(str, ~scope, ~gen?) {
173
-
| Ok(t, str) => Ok(StringV(t), str)
174
-
| Error(stringE) =>
175
-
switch StringSExp.parse(str, ~scope) {
176
-
| Ok(t, str) => Ok(SExpV(t), str)
177
-
| Error(sExpE) =>
178
-
Error(
179
-
`string or sexp expected.\nstring parsing failed with error: ${stringE}\nsexp parsing failed with error: ${sExpE}`,
180
-
)
181
-
}
182
-
}
183
-
}
184
-
185
-
let prettyPrint = ((t, j): t, ~scope: array<StringTerm.meta>) =>
186
-
`${StringTerm.prettyPrint(t, ~scope)} ${StringSExp.prettyPrint(j, ~scope)}`
187
-
let prettyPrintSubstCodom = (v: substCodom, ~scope: array<StringTerm.meta>) =>
188
-
switch v {
189
-
| StringV(t) => StringTerm.prettyPrint(t, ~scope)
190
-
| SExpV(t) => StringSExp.prettyPrint(t, ~scope)
191
-
}
192
-
193
-
let ghostJudgment = (StringTerm.ghostTerm, StringSExp.ghostTerm)
47
+
module StringSExp = SExpFunc.Make(StringSymbol)
48
+
include TermAsJudgment.Make(StringSExp)
+2
-4
src/StringTermJudgment.resi
+2
-4
src/StringTermJudgment.resi
···
2
2
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol
3
3
4
4
module StringSExp: module type of SExpFunc.Make(StringSymbol)
5
-
6
-
type t = (StringTerm.t, StringSExp.t)
7
-
let constSymbol: string => StringSExp.t
5
+
type t = StringSExp.t
8
6
9
-
include Signatures.JUDGMENT with module Term := StringTerm and type t := t
7
+
include Signatures.JUDGMENT with module Term := StringSExp and type t := t