the next generation of the in-browser educational proof assistant
Merge pull request #27 from joshcbrown/atom-combine-coerce
Combine and coerce atoms generically
authored by
Liam O'Connor
and committed by
GitHub
5b716ec3
dacd4ade
+247
-158
+1
-1
index.html
+1
-1
index.html
+152
src/AtomDef.res
+152
src/AtomDef.res
···
1
+
// type level stuff to enable well-typed coercions
2
+
type atomTag<_> = ..
3
+
4
+
module type ATOM = {
5
+
type t
6
+
type subst = Map.t<int, t>
7
+
type atomTag<_> += Tag: atomTag<t>
8
+
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
9
+
let prettyPrint: (t, ~scope: array<string>) => string
10
+
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
11
+
let substitute: (t, subst) => t
12
+
let upshift: (t, int, ~from: int=?) => t
13
+
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
14
+
let concrete: t => bool
15
+
}
16
+
17
+
type rec hValue = HValue(atomTag<'a>, 'a): hValue
18
+
module type COERCIBLE_ATOM = {
19
+
include ATOM
20
+
let coerce: hValue => option<t>
21
+
let wrap: t => hValue
22
+
}
23
+
24
+
type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
25
+
type atomTag<_> += SExpTag: atomTag<loweredSExp>
26
+
27
+
exception MatchCombineAtomForeign
28
+
29
+
module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): {
30
+
type rec base =
31
+
| Left(Left.t)
32
+
| Right(Right.t)
33
+
// strictly for coercions
34
+
// occurs when passed from some relative in the tree
35
+
// or when SExp values are lowered into loweredSExp
36
+
| Foreign(hValue)
37
+
include COERCIBLE_ATOM with type t = base
38
+
let match: (t, Left.t => 'a, Right.t => 'a) => 'a
39
+
} => {
40
+
type rec base =
41
+
| Left(Left.t)
42
+
| Right(Right.t)
43
+
| Foreign(hValue)
44
+
type t = base
45
+
type subst = Map.t<int, t>
46
+
type gen = ref<int>
47
+
type atomTag<_> += Tag: atomTag<t>
48
+
let coerce = v => Some(Foreign(v))
49
+
let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a =>
50
+
switch t {
51
+
| Left(s) => leftBranch(s)
52
+
| Right(s) => rightBranch(s)
53
+
| Foreign(_) => throw(MatchCombineAtomForeign)
54
+
}
55
+
let wrap = t =>
56
+
switch t {
57
+
| Left(s) => Left.wrap(s)
58
+
| Right(s) => Right.wrap(s)
59
+
| Foreign(val) => val
60
+
}
61
+
let parse = (s, ~scope, ~gen: option<gen>=?) => {
62
+
Left.parse(s, ~scope, ~gen?)
63
+
->Result.map(((r, rest)) => (Left(r), rest))
64
+
->Util.Result.or(() =>
65
+
Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest))
66
+
)
67
+
}
68
+
let prettyPrint = (s, ~scope) =>
69
+
s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope))
70
+
let unify = (s1, s2, ~gen=?) =>
71
+
switch (s1, s2) {
72
+
| (Left(s1), Left(s2)) =>
73
+
Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v)))
74
+
| (Right(s1), Right(s2)) =>
75
+
Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v)))
76
+
| (_, _) => Seq.empty
77
+
}
78
+
let coerceToLeft = (t): option<Left.t> =>
79
+
switch t {
80
+
| Left(s) => Some(s)
81
+
| Right(s) => Right.wrap(s)->Left.coerce
82
+
| Foreign(v) => Left.coerce(v)
83
+
}
84
+
let coerceToRight = (t): option<Right.t> =>
85
+
switch t {
86
+
| Right(s) => Some(s)
87
+
| Left(s) => Left.wrap(s)->Right.coerce
88
+
| Foreign(v) => Right.coerce(v)
89
+
}
90
+
let substitute = (s, subst: subst) => {
91
+
s->match(
92
+
left => {
93
+
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
94
+
Left(Left.substitute(left, leftSubs))
95
+
},
96
+
right => {
97
+
let rightSubs = subst->Util.Map.filterMap((_, v) => coerceToRight(v))
98
+
Right(Right.substitute(right, rightSubs))
99
+
},
100
+
)
101
+
}
102
+
let upshift = (s, amount: int, ~from=?) =>
103
+
s->match(
104
+
left => Left(left->Left.upshift(amount, ~from?)),
105
+
right => Right(right->Right.upshift(amount, ~from?)),
106
+
)
107
+
let substDeBruijn = (s, substs: array<option<t>>, ~from=?) =>
108
+
s->match(
109
+
left => {
110
+
let leftSubs = substs->Array.map(o => o->Option.flatMap(coerceToLeft))
111
+
Left(Left.substDeBruijn(left, leftSubs, ~from?))
112
+
},
113
+
right => {
114
+
let rightSubs = substs->Array.map(o => o->Option.flatMap(coerceToRight))
115
+
Right(Right.substDeBruijn(right, rightSubs, ~from?))
116
+
},
117
+
)
118
+
let concrete = s => s->match(Left.concrete, Right.concrete)
119
+
}
120
+
121
+
module type ATOM_VIEW = {
122
+
module Atom: ATOM
123
+
type props = {name: Atom.t, scope: array<string>}
124
+
let make: props => React.element
125
+
}
126
+
127
+
module MakeAtomView = (
128
+
Left: COERCIBLE_ATOM,
129
+
LeftView: ATOM_VIEW with module Atom := Left,
130
+
Right: COERCIBLE_ATOM,
131
+
RightView: ATOM_VIEW with module Atom := Right,
132
+
Combined: module type of CombineAtom(Left, Right),
133
+
): {
134
+
include ATOM_VIEW with module Atom := Combined
135
+
} => {
136
+
type props = {name: Combined.t, scope: array<string>}
137
+
let make = ({name, scope}: props) =>
138
+
name->Combined.match(
139
+
left => <LeftView name={left} scope />,
140
+
right => <RightView name={right} scope />,
141
+
)
142
+
}
143
+
144
+
module MakeAtomAndView = (
145
+
Left: COERCIBLE_ATOM,
146
+
LeftView: ATOM_VIEW with module Atom := Left,
147
+
Right: COERCIBLE_ATOM,
148
+
RightView: ATOM_VIEW with module Atom := Right,
149
+
) => {
150
+
module Atom = CombineAtom(Left, Right)
151
+
module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
152
+
}
+24
src/Coercible.res
+24
src/Coercible.res
···
1
+
open AtomDef
2
+
3
+
module StringA: COERCIBLE_ATOM with type t = StringA.t = {
4
+
include StringA.Atom
5
+
let coerce = (HValue(tag, a)) =>
6
+
switch tag {
7
+
| Symbolic.Atom.Tag => Some([StringA.String(a)])
8
+
| AtomDef.SExpTag =>
9
+
Some([
10
+
switch a {
11
+
| Var({idx}) => StringA.Var({idx: idx})
12
+
| Schematic({schematic, allowed}) => StringA.Schematic({schematic, allowed})
13
+
},
14
+
])
15
+
| _ => None
16
+
}
17
+
let wrap = a => HValue(StringA.Atom.Tag, a)
18
+
}
19
+
20
+
module Symbolic: COERCIBLE_ATOM with type t = Symbolic.Atom.t = {
21
+
include Symbolic.Atom
22
+
let coerce = _ => None
23
+
let wrap = a => HValue(Symbolic.Atom.Tag, a)
24
+
}
+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
}
+5
-17
src/SExpFunc.res
src/SExp.res
+5
-17
src/SExpFunc.res
src/SExp.res
···
1
1
exception SubstNotCompatible(string)
2
2
3
-
module type ATOM = {
4
-
type t
5
-
type subst = Map.t<int, t>
6
-
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
7
-
let prettyPrint: (t, ~scope: array<string>) => string
8
-
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
9
-
let substitute: (t, subst) => t
10
-
let upshift: (t, int, ~from: int=?) => t
11
-
// used for when trying to substitute a variable of the wrong type
12
-
let lowerVar: int => option<t>
13
-
let lowerSchematic: (int, array<int>) => option<t>
14
-
let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
15
-
let concrete: t => bool
16
-
}
3
+
module type ATOM = AtomDef.ATOM
17
4
18
5
module IntCmp = Belt.Id.MakeComparable({
19
6
type t = int
20
7
let cmp = Pervasives.compare
21
8
})
22
9
23
-
module Make = (Atom: ATOM): {
10
+
module Make = (Atom: AtomDef.COERCIBLE_ATOM): {
24
11
type rec t =
25
12
| Atom(Atom.t)
26
13
| Compound({subexps: array<t>})
···
163
150
let rec lower = (term: t): option<Atom.t> =>
164
151
switch term {
165
152
| Atom(s) => Some(s)
166
-
| Var({idx}) => Atom.lowerVar(idx)
167
-
| Schematic({schematic, allowed}) => Atom.lowerSchematic(schematic, allowed)
153
+
| Var({idx}) => Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx})))
154
+
| Schematic({schematic, allowed}) =>
155
+
Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed})))
168
156
| Compound({subexps: [e1]}) => lower(e1)
169
157
| _ => None
170
158
}
+3
-7
src/SExpViewFunc.res
src/SExpView.res
+3
-7
src/SExpViewFunc.res
src/SExpView.res
···
1
-
module type ATOM_VIEW = {
2
-
module Atom: SExpFunc.ATOM
3
-
type props = {name: Atom.t, scope: array<string>}
4
-
let make: props => React.element
5
-
}
1
+
module type ATOM_VIEW = AtomDef.ATOM_VIEW
6
2
7
3
module Make = (
8
-
Atom: SExpFunc.ATOM,
4
+
Atom: AtomDef.COERCIBLE_ATOM,
9
5
AtomView: ATOM_VIEW with module Atom := Atom,
10
-
SExp: module type of SExpFunc.Make(Atom),
6
+
SExp: module type of SExp.Make(Atom),
11
7
): {
12
8
include Signatures.TERM_VIEW with module Term := SExp
13
9
} => {
+8
-2
src/Scratch.res
+8
-2
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 StringSExp = SExpFunc.Make(StringSymbol.Atom)
46
-
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
45
+
module StringSymbol = AtomDef.MakeAtomAndView(
46
+
Coercible.StringA,
47
+
StringA.AtomView,
48
+
Coercible.Symbolic,
49
+
Symbolic.AtomView,
50
+
)
51
+
module StringSExp = SExp.Make(StringSymbol.Atom)
52
+
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
47
53
module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
48
54
module AxiomStr = Editable.TextArea(StringAxiomSet)
49
55
+4
-26
src/StringA.res
+4
-26
src/StringA.res
···
14
14
module Atom = {
15
15
type t = t
16
16
type subst = Map.t<schematic, t>
17
+
type AtomDef.atomTag<_> += Tag: AtomDef.atomTag<t>
17
18
let substitute = (term: t, subst: subst) =>
18
19
Array.flatMap(term, piece => {
19
20
switch piece {
···
282
283
switch Option.getUnsafe(substs[var - from]) {
283
284
| Some(v) => v
284
285
| None =>
285
-
throw(
286
-
SExpFunc.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`),
287
-
)
286
+
throw(SExp.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`))
288
287
}
289
288
} else {
290
289
[Var({idx: var - to})]
···
333
332
334
333
type gen = ref<int>
335
334
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
335
let prettyPrint = (term: t, ~scope: array<string>) =>
343
336
`"${Array.map(term, piece => {
344
337
switch piece {
345
338
| 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
-
}
339
+
| Var({idx}) => Util.prettyPrintVar(idx, scope)
340
+
| Schematic({schematic, allowed}) => Util.prettyPrintSchematic(schematic, allowed, scope)
354
341
}
355
342
})->Array.join(" ")}"`
356
343
···
468
455
469
456
acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents)))
470
457
}
471
-
472
-
let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})])
473
-
let lowerVar = idx => Some([Var({idx: idx})])
474
458
let concrete = t =>
475
459
t->Array.every(p =>
476
460
switch p {
···
493
477
{React.int(props.idx)}
494
478
</span>
495
479
}
496
-
497
-
let makeMeta = (str: string) =>
498
-
<span className="rule-binder">
499
-
{React.string(str)}
500
-
{React.string(".")}
501
-
</span>
502
480
503
481
let parenthesise = f =>
504
482
[
+2
-2
src/StringA.resi
+2
-2
src/StringA.resi
···
4
4
| Schematic({schematic: int, allowed: array<int>})
5
5
type t = array<piece>
6
6
7
-
module Atom: SExpFunc.ATOM with type t = t
8
-
module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom
7
+
module Atom: AtomDef.ATOM with type t = t
8
+
module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
+14
-8
src/StringAxiomSet.res
+14
-8
src/StringAxiomSet.res
···
1
1
open Component
2
2
3
-
module StringSExp = SExpFunc.Make(StringSymbol.Atom)
4
-
module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
3
+
module StringSymbol = AtomDef.MakeAtomAndView(
4
+
Coercible.StringA,
5
+
StringA.AtomView,
6
+
Coercible.Symbolic,
7
+
Symbolic.AtomView,
8
+
)
9
+
module StringSExp = SExp.Make(StringSymbol.Atom)
10
+
module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp)
5
11
module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)
6
12
7
13
module Rule = Rule.Make(StringSExp, StringSExp)
···
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
+2
-2
src/Symbolic.res
+2
-2
src/Symbolic.res
···
1
1
type t = string
2
2
module Atom = {
3
+
open AtomDef
3
4
type t = string
4
5
type subst = Map.t<int, string>
6
+
type atomTag<_> += Tag: atomTag<t>
5
7
let unify = (a, b, ~gen as _=?) =>
6
8
if a == b {
7
9
Seq.once(Map.make())
···
16
18
| _ => Error("constant symbol parse error")
17
19
}
18
20
let substitute = (name, _) => name
19
-
let lowerVar = _ => None
20
-
let lowerSchematic = (_, _) => None
21
21
let substDeBruijn = (name, _, ~from as _=?) => name
22
22
let concrete = _ => false
23
23
let upshift = (t, _, ~from as _=?) => t
+2
-2
src/Symbolic.resi
+2
-2
src/Symbolic.resi
+1
-1
src/Theorem.res
+1
-1
src/Theorem.res
···
63
63
Proof.check(ctx, proof, props.content.rule)->ignore
64
64
{...props.content, proof, substFailed: None}
65
65
} catch {
66
-
| SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
66
+
| SExp.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
67
67
},
68
68
~exports={
69
69
Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
+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>) => {
+1
-1
tests/SExpTest.res
+1
-1
tests/SExpTest.res