the next generation of the in-browser educational proof assistant
combine atom functor
+176
-108
+129
src/CombinedAtom.res
+129
src/CombinedAtom.res
···
1
+
module type ATOM = SExpFunc.ATOM
2
+
exception RawVarOrSchematic
3
+
4
+
module MakeAtom = (Left: ATOM, Right: ATOM): {
5
+
type base =
6
+
| Left(Left.t)
7
+
| Right(Right.t)
8
+
// neither of the below should appear organically. they're purely so we can lower
9
+
// substitutions to both Left.t and Right.t
10
+
| Var({idx: int})
11
+
| Schematic({schematic: int, allowed: array<int>})
12
+
include ATOM with type t = base
13
+
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
14
+
} => {
15
+
type base =
16
+
| Left(Left.t)
17
+
| Right(Right.t)
18
+
| Var({idx: int})
19
+
| Schematic({schematic: int, allowed: array<int>})
20
+
type t = base
21
+
type subst = Map.t<int, t>
22
+
type gen = ref<int>
23
+
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
24
+
switch t {
25
+
| Left(s) => leftBranch(s)
26
+
| Right(s) => rightBranch(s)
27
+
| _ => throw(RawVarOrSchematic)
28
+
}
29
+
let parse = (s, ~scope, ~gen: option<gen>=?) => {
30
+
Left.parse(s, ~scope, ~gen?)
31
+
->Result.map(((r, rest)) => (Left(r), rest))
32
+
->Util.Result.or(() =>
33
+
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
34
+
)
35
+
}
36
+
let prettyPrint = (s, ~scope) =>
37
+
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
38
+
let unify = (s1, s2, ~gen=?) =>
39
+
switch (s1, s2) {
40
+
| (Left(s1), Left(s2)) =>
41
+
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
42
+
| (Right(s1), Right(s2)) =>
43
+
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
44
+
| (_, _) => Seq.empty
45
+
}
46
+
let substitute = (s, subst: subst) => {
47
+
s->match(
48
+
left => {
49
+
let leftSubs = subst->Util.Map.filterMap((_, v) =>
50
+
switch v {
51
+
| Left(s) => Some(s)
52
+
| _ => None
53
+
}
54
+
)
55
+
Left(Left.substitute(left, leftSubs))
56
+
},
57
+
right => {
58
+
let rightSubs = subst->Util.Map.filterMap((_, v) =>
59
+
switch v {
60
+
| Right(s) => Some(s)
61
+
| _ => None
62
+
}
63
+
)
64
+
Right(Right.substitute(right, rightSubs))
65
+
},
66
+
)
67
+
}
68
+
let upshift = (s, amount: int, ~from=?) =>
69
+
s->match(
70
+
left => Left(left->Left.upshift(amount, ~from?)),
71
+
right => Right(right->Right.upshift(amount, ~from?)),
72
+
)
73
+
let lowerVar = idx => Some(Var({idx: idx}))
74
+
let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed}))
75
+
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
76
+
s->match(
77
+
left => {
78
+
let leftSubs = substs->Array.map(s =>
79
+
switch s {
80
+
| Some(Left(s)) => Some(s)
81
+
| Some(Var({idx})) => Left.lowerVar(idx)
82
+
| Some(Schematic({schematic, allowed})) => Left.lowerSchematic(schematic, allowed)
83
+
| _ => None
84
+
}
85
+
)
86
+
Left(Left.substDeBruijn(left, leftSubs, ~from?))
87
+
},
88
+
right => {
89
+
let rightSubs = substs->Array.map(s =>
90
+
switch s {
91
+
| Some(Right(s)) => Some(s)
92
+
| Some(Var({idx})) => Right.lowerVar(idx)
93
+
| Some(Schematic({schematic, allowed})) => Right.lowerSchematic(schematic, allowed)
94
+
| _ => None
95
+
}
96
+
)
97
+
Right(Right.substDeBruijn(right, rightSubs, ~from?))
98
+
},
99
+
)
100
+
let concrete = s => s->match(Left.concrete, Right.concrete)
101
+
}
102
+
103
+
module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW
104
+
module MakeAtomView = (
105
+
Left: ATOM,
106
+
LeftView: ATOM_VIEW with module Atom := Left,
107
+
Right: ATOM,
108
+
RightView: ATOM_VIEW with module Atom := Right,
109
+
Combined: module type of MakeAtom(Left, Right),
110
+
): {
111
+
include ATOM_VIEW with module Atom := Combined
112
+
} => {
113
+
type props = {name: Combined.t, scope: array<string>}
114
+
let make = ({name, scope}: props) =>
115
+
name->Combined.match(
116
+
left => <LeftView name={left} scope />,
117
+
right => <RightView name={right} scope />,
118
+
)
119
+
}
120
+
121
+
module MakeAtomAndView = (
122
+
Left: ATOM,
123
+
LeftView: ATOM_VIEW with module Atom := Left,
124
+
Right: ATOM,
125
+
RightView: ATOM_VIEW with module Atom := Right,
126
+
) => {
127
+
module Atom = MakeAtom(Left, Right)
128
+
module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
129
+
}
+3
-4
src/HOTerm.res
+3
-4
src/HOTerm.res
···
1
-
open Util
2
1
module IntCmp = Belt.Id.MakeComparable({
3
2
type t = int
4
3
let cmp = Pervasives.compare
···
102
101
| Ok(newIdx) =>
103
102
let new = newIdx + from
104
103
if new < 0 {
105
-
throw(Err("mapbind: negative index"))
104
+
throw(Util.Err("mapbind: negative index"))
106
105
}
107
106
Var({
108
107
idx: new,
···
132
131
let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from)
133
132
let downshift = (term: t, amount: int, ~from: int=1) => {
134
133
if amount > from {
135
-
throw(Err("downshift amount must be less than from"))
134
+
throw(Util.Err("downshift amount must be less than from"))
136
135
}
137
136
mapbind(term, idx => idx - amount, ~from)
138
137
}
···
651
650
let (tail, rest3) = parseSimple("("->String.concat(rest2))
652
651
switch tail {
653
652
| ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3)
654
-
| _ => throw(Unreachable("bug"))
653
+
| _ => throw(Util.Unreachable("bug"))
655
654
}
656
655
}
657
656
}
+6
src/Scratch.res
+6
src/Scratch.res
···
42
42
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView))
43
43
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)
44
44
45
+
module StringSymbol = CombinedAtom.MakeAtomAndView(
46
+
StringA.Atom,
47
+
StringA.AtomView,
48
+
Symbolic.Atom,
49
+
Symbolic.AtomView,
50
+
)
45
51
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
46
52
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
47
53
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
+2
-14
src/StringA.res
+2
-14
src/StringA.res
···
333
333
334
334
type gen = ref<int>
335
335
336
-
let prettyPrintVar = (idx: int, scope: array<string>) =>
337
-
"$" ++
338
-
switch scope[idx] {
339
-
| Some(n) if Array.indexOf(scope, n) == idx => n
340
-
| _ => "\\"->String.concat(String.make(idx))
341
-
}
342
336
let prettyPrint = (term: t, ~scope: array<string>) =>
343
337
`"${Array.map(term, piece => {
344
338
switch piece {
345
339
| String(str) => str
346
-
| Var({idx}) => prettyPrintVar(idx, scope)
347
-
| Schematic({schematic, allowed}) => {
348
-
let allowedStr =
349
-
allowed
350
-
->Array.map(idx => prettyPrintVar(idx, scope))
351
-
->Array.join(" ")
352
-
`?${Int.toString(schematic)}(${allowedStr})`
353
-
}
340
+
| Var({idx}) => Util.prettyPrintVar(idx, scope)
341
+
| Schematic({schematic, allowed}) => Util.prettyPrintSchematic(schematic, allowed, scope)
354
342
}
355
343
})->Array.join(" ")}"`
356
344
+12
-6
src/StringAxiomSet.res
+12
-6
src/StringAxiomSet.res
···
1
1
open Component
2
2
3
+
module StringSymbol = CombinedAtom.MakeAtomAndView(
4
+
StringA.Atom,
5
+
StringA.AtomView,
6
+
Symbolic.Atom,
7
+
Symbolic.AtomView,
8
+
)
3
9
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
4
10
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
5
11
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
···
38
44
39
45
let destructure = (r: StringSExp.t): (StringA.Atom.t, string) =>
40
46
switch r {
41
-
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name)
47
+
| Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => (s, name)
42
48
| _ => throw(Util.Unreachable("expected valid induction rule"))
43
49
}
44
50
let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> =>
45
51
switch r {
46
-
| Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name))
52
+
| Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => Some((s, name))
47
53
| _ => None
48
54
}
49
55
let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({
···
108
114
vars: rule.vars,
109
115
premises: rule.premises->Array.concat(inductionHyps),
110
116
conclusion: structure(
111
-
surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringS->Atom,
117
+
surround(s, aIdx + baseIdx, bIdx + baseIdx)->Left->Atom,
112
118
Var({idx: pIdx + baseIdx}),
113
119
),
114
120
}
···
120
126
{
121
127
Rule.vars: [],
122
128
premises: [],
123
-
conclusion: structure(Var({idx: xIdx}), Atom(ConstS(group.name))),
129
+
conclusion: structure(Var({idx: xIdx}), Atom(Right(group.name))),
124
130
},
125
131
],
126
132
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
127
133
),
128
134
conclusion: structure(
129
-
surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom,
135
+
surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->Left->Atom,
130
136
Var({idx: 0}),
131
137
), // TODO: clean here
132
138
}
···
165
171
let grouped: dict<array<Rule.t>> = Dict.make()
166
172
raw->Dict.forEach(rule =>
167
173
switch rule.conclusion {
168
-
| Compound({subexps: [Atom(StringS(_)), Atom(ConstS(name))]}) =>
174
+
| Compound({subexps: [Atom(Left(_)), Atom(Right(name))]}) =>
169
175
switch grouped->Dict.get(name) {
170
176
| None => grouped->Dict.set(name, [rule])
171
177
| Some(rs) => rs->Array.push(rule)
-81
src/StringSymbol.res
-81
src/StringSymbol.res
···
1
-
type t = StringS(StringA.Atom.t) | ConstS(string)
2
-
3
-
module Atom: SExpFunc.ATOM with type t = t = {
4
-
type t = t
5
-
type subst = Map.t<int, t>
6
-
type gen = ref<int>
7
-
let parse = (s, ~scope, ~gen: option<gen>=?) => {
8
-
StringA.Atom.parse(s, ~scope, ~gen?)
9
-
->Result.map(((r, rest)) => (StringS(r), rest))
10
-
->Util.Result.or(() =>
11
-
Symbolic.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
-
)
13
-
}
14
-
let prettyPrint = (s, ~scope) =>
15
-
switch s {
16
-
| StringS(s) => StringA.Atom.prettyPrint(s, ~scope)
17
-
| ConstS(s) => Symbolic.Atom.prettyPrint(s, ~scope)
18
-
}
19
-
let unify = (s1, s2, ~gen=?) =>
20
-
switch (s1, s2) {
21
-
| (StringS(s1), StringS(s2)) =>
22
-
StringA.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
-
| (ConstS(s1), ConstS(s2)) =>
24
-
Symbolic.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
25
-
| (_, _) => Seq.empty
26
-
}
27
-
let substitute = (s, subst: subst) =>
28
-
switch s {
29
-
| StringS(s) => {
30
-
let stringSubs =
31
-
subst
32
-
->Map.entries
33
-
->Iterator.toArrayWithMapper(((i, v)) =>
34
-
switch v {
35
-
| StringS(s) => Some((i, s))
36
-
| _ => None
37
-
}
38
-
)
39
-
->Array.keepSome
40
-
->Map.fromArray
41
-
StringS(StringA.Atom.substitute(s, stringSubs))
42
-
}
43
-
| ConstS(s) => ConstS(s)
44
-
}
45
-
let upshift = (s, amount: int, ~from=?) =>
46
-
switch s {
47
-
| StringS(s) => StringS(s->StringA.Atom.upshift(amount, ~from?))
48
-
| ConstS(s) => ConstS(s)
49
-
}
50
-
let lowerVar = idx => Some(StringS([StringA.Var({idx: idx})]))
51
-
let lowerSchematic = (schematic, allowed) => Some(
52
-
StringS([StringA.Schematic({schematic, allowed})]),
53
-
)
54
-
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
55
-
switch s {
56
-
| StringS(s) => {
57
-
let stringSubs = substs->Array.map(s =>
58
-
switch s {
59
-
| Some(StringS(s)) => Some(s)
60
-
| _ => None
61
-
}
62
-
)
63
-
StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?))
64
-
}
65
-
| ConstS(s) => ConstS(s)
66
-
}
67
-
let concrete = s =>
68
-
switch s {
69
-
| StringS(s) => StringA.Atom.concrete(s)
70
-
| ConstS(_) => false
71
-
}
72
-
}
73
-
74
-
module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom = {
75
-
type props = {name: Atom.t, scope: array<string>}
76
-
let make = ({name, scope}: props) =>
77
-
switch name {
78
-
| StringS(name) => <StringA.AtomView name scope />
79
-
| ConstS(name) => <Symbolic.AtomView name scope />
80
-
}
81
-
}
-3
src/StringSymbol.resi
-3
src/StringSymbol.resi
+24
src/Util.res
+24
src/Util.res
···
34
34
->showArray
35
35
}
36
36
37
+
let prettyPrintVar = (idx: int, scope: array<string>) =>
38
+
"$" ++
39
+
switch scope[idx] {
40
+
| Some(n) if Array.indexOf(scope, n) == idx => n
41
+
| _ => "\\"->String.concat(String.make(idx))
42
+
}
43
+
let prettyPrintSchematic = (schematic: int, allowed: array<int>, scope: array<string>) => {
44
+
let allowedStr =
45
+
allowed
46
+
->Array.map(idx => prettyPrintVar(idx, scope))
47
+
->Array.join(" ")
48
+
`?${Int.toString(schematic)}(${allowedStr})`
49
+
}
50
+
37
51
let mapIntersectionWith = (m1: Map.t<'k, 'a>, m2: Map.t<'k, 'b>, f: ('a, 'b) => 'c) => {
38
52
let go = (m1, m2) => {
39
53
let nu: Map.t<'k, 'c> = Map.make()
···
84
98
->Iterator.toArray
85
99
->Array.filter(((a, b)) => a == b)
86
100
->Array.length == Map.size(m2)
101
+
}
102
+
103
+
module Map = {
104
+
type t<'k, 'v> = Map.t<'k, 'v>
105
+
let filterMap = (m: t<'k, 'v1>, f: ('k, 'v1) => option<'v2>): t<'k, 'v2> =>
106
+
m
107
+
->Map.entries
108
+
->Iterator.toArrayWithMapper(((i, v)) => f(i, v)->Option.map(v => (i, v)))
109
+
->Array.keepSome
110
+
->Map.fromArray
87
111
}
88
112
89
113
let arrayWithIndex = (arr: array<React.element>) => {