forked from
liamoc.net/holbert-ng
the next generation of the in-browser educational proof assistant
reorganise atom defns
the previous organisation didn't actually quite allow circular
coercions, which wasn't discovered because there weren't any.
resolve conflicts
+177
-172
+34
src/AtomBase.res
+34
src/AtomBase.res
···
1
+
// type level stuff to enable well-typed coercions
2
+
type atomTag<_> = ..
3
+
type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
4
+
5
+
// to allow circular coercions, we declare base types
6
+
// separately from relevant implementation
7
+
module type BASE_ATOM = {
8
+
type t
9
+
type atomTag<_> += Tag: atomTag<t>
10
+
let wrap: t => anyValue
11
+
}
12
+
13
+
module Make = (
14
+
T: {
15
+
type t
16
+
},
17
+
): (BASE_ATOM with type t = T.t) => {
18
+
type t = T.t
19
+
type atomTag<_> += Tag: atomTag<t>
20
+
let wrap = t => AnyValue(Tag, t)
21
+
}
22
+
23
+
module String = {
24
+
type piece =
25
+
| String(string)
26
+
| Var({idx: int})
27
+
| Schematic({schematic: int, allowed: array<int>})
28
+
include Make({type t = array<piece>})
29
+
}
30
+
31
+
module VarBase = {
32
+
type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
33
+
include Make({type t = varBase})
34
+
}
+58
-87
src/AtomDef.res
+58
-87
src/AtomDef.res
···
1
-
// type level stuff to enable well-typed coercions
2
-
type atomTag<_> = ..
3
-
type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
4
-
5
-
// to allow circular coercions, we declare base types
6
-
// separately from relevant implementation
7
-
module type BASE_ATOM = {
8
-
type t
9
-
type atomTag<_> += Tag: atomTag<t>
10
-
let wrap: t => anyValue
11
-
}
12
-
13
-
module MakeBaseAtom = (
14
-
T: {
15
-
type t
16
-
},
17
-
): (BASE_ATOM with type t = T.t) => {
18
-
type t = T.t
19
-
type atomTag<_> += Tag: atomTag<t>
20
-
let wrap = t => AnyValue(Tag, t)
21
-
}
1
+
open AtomBase
22
2
23
3
module type ATOM = {
24
-
module BaseAtom: BASE_ATOM
25
-
type t = BaseAtom.t
4
+
module Base: BASE_ATOM
5
+
type t = Base.t
26
6
type subst = Map.t<int, t>
27
7
let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
28
8
let prettyPrint: (t, ~scope: array<string>) => string
···
34
14
let coerce: anyValue => option<t>
35
15
}
36
16
37
-
type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
38
-
module VarBase = MakeBaseAtom({
39
-
type t = varBase
40
-
})
41
-
42
17
exception AtomExpected
43
18
44
-
module AtomListBase = MakeBaseAtom({
19
+
module AtomChoiceBase = Make({
45
20
type t = anyValue
46
21
})
47
22
48
-
module type ATOM_LIST = {
49
-
module HeadBase: BASE_ATOM
50
-
include ATOM with module BaseAtom = AtomListBase
51
-
let onHead: (t, HeadBase.t => 'a) => option<'a>
23
+
module type ATOM_CHOICE = {
24
+
module LeftBase: BASE_ATOM
25
+
include ATOM with module Base = AtomChoiceBase
26
+
let onLeft: (t, LeftBase.t => 'a) => option<'a>
52
27
}
53
28
54
-
module NilAtomList: ATOM_LIST = {
55
-
module HeadBase = MakeBaseAtom({
29
+
module EmptyAtomChoice: ATOM_CHOICE = {
30
+
module LeftBase = AtomBase.Make({
56
31
// empty
57
32
type t = {.}
58
33
})
59
-
module BaseAtom = AtomListBase
60
-
type t = BaseAtom.t
34
+
module Base = AtomChoiceBase
35
+
type t = Base.t
61
36
type subst = Map.t<int, t>
62
37
let parse = (_, ~scope as _, ~gen as _=?) => Error("expected atom")
63
-
// ideally we could check that the tags
64
-
// in each argument are the same before returning Seq.empty, otherwise throw
65
-
// but building up a type-level witness to tag equality is not easy with the
66
-
// extensible variant stuff
67
38
let unify = (_, _, ~gen as _=?) => Seq.empty
68
39
// this should probably throw too, but will be more
69
40
// informative to have it appear wherever it's called from
70
41
let prettyPrint = (_, ~scope as _) => "NIL (THIS IS AN ERROR!)"
71
-
let onHead = (_, _) => throw(AtomExpected)
42
+
let onLeft = (_, _) => throw(AtomExpected)
72
43
let coerce = _ => throw(AtomExpected)
73
44
let substitute = (_, _) => throw(AtomExpected)
74
45
let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
···
76
47
let concrete = _ => throw(AtomExpected)
77
48
}
78
49
79
-
module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
80
-
ATOM_LIST with module HeadBase = Head.BaseAtom
50
+
module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): (
51
+
ATOM_CHOICE with module LeftBase = Left.Base
81
52
) => {
82
-
module HeadBase = Head.BaseAtom
83
-
module Tail = Tail
84
-
module BaseAtom = AtomListBase
85
-
type t = BaseAtom.t
53
+
module LeftBase = Left.Base
54
+
module Right = Right
55
+
module Base = AtomChoiceBase
56
+
type t = Base.t
86
57
type subst = Map.t<int, t>
87
58
type gen = ref<int>
88
59
let getOrElse = Util.Option.getOrElse
89
60
let coerce = v => Some(v)
90
-
let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
61
+
let onLeft = (AnyValue(tag, val), f: Left.t => 'a): option<'a> =>
91
62
switch tag {
92
-
| Head.BaseAtom.Tag => Some(f(val))
63
+
| Left.Base.Tag => Some(f(val))
93
64
| _ => None
94
65
}
95
66
let parse = (s, ~scope, ~gen: option<gen>=?) => {
96
-
Head.parse(s, ~scope, ~gen?)
97
-
->Result.map(((r, rest)) => (HeadBase.wrap(r), rest))
98
-
->Util.Result.or(() => Tail.parse(s, ~scope, ~gen?))
67
+
Left.parse(s, ~scope, ~gen?)
68
+
->Result.map(((r, rest)) => (LeftBase.wrap(r), rest))
69
+
->Util.Result.or(() => Right.parse(s, ~scope, ~gen?))
99
70
}
100
71
let prettyPrint = (atom, ~scope) =>
101
72
atom
102
-
->onHead(val => Head.prettyPrint(val, ~scope))
103
-
->getOrElse(() => Tail.prettyPrint(atom, ~scope))
73
+
->onLeft(val => Left.prettyPrint(val, ~scope))
74
+
->getOrElse(() => Right.prettyPrint(atom, ~scope))
104
75
105
76
let unify = (a1, a2, ~gen=?) => {
106
77
let (AnyValue(tag1, val1), AnyValue(tag2, val2)) = (a1, a2)
107
78
switch (tag1, tag2) {
108
-
| (Head.BaseAtom.Tag, Head.BaseAtom.Tag) =>
109
-
Head.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(HeadBase.wrap))
110
-
| (_, _) => Tail.unify(a1, a2, ~gen?)
79
+
| (Left.Base.Tag, Left.Base.Tag) =>
80
+
Left.unify(val1, val2)->Seq.map(subst => subst->Util.mapMapValues(LeftBase.wrap))
81
+
| (_, _) => Right.unify(a1, a2, ~gen?)
111
82
}
112
83
}
113
-
let coerceToHead = (atom): option<Head.t> =>
114
-
atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
84
+
let coerceToLeft = (atom): option<Left.t> =>
85
+
atom->onLeft(val => Some(val))->getOrElse(() => Left.coerce(atom))
115
86
let substitute = (atom, subst: subst) =>
116
87
atom
117
-
->onHead(val => {
118
-
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToHead(v))
119
-
Head.substitute(val, leftSubs)->HeadBase.wrap
88
+
->onLeft(val => {
89
+
let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToLeft(v))
90
+
Left.substitute(val, leftSubs)->LeftBase.wrap
120
91
})
121
-
->getOrElse(() => Tail.substitute(atom, subst))
92
+
->getOrElse(() => Right.substitute(atom, subst))
122
93
123
94
let upshift = (atom, amount: int, ~from=?) =>
124
95
atom
125
-
->onHead(val => Head.upshift(val, amount, ~from?)->HeadBase.wrap)
126
-
->getOrElse(() => Tail.upshift(atom, amount, ~from?))
96
+
->onLeft(val => Left.upshift(val, amount, ~from?)->LeftBase.wrap)
97
+
->getOrElse(() => Right.upshift(atom, amount, ~from?))
127
98
let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
128
99
atom
129
-
->onHead(val =>
130
-
Head.substDeBruijn(
100
+
->onLeft(val =>
101
+
Left.substDeBruijn(
131
102
val,
132
-
substs->Array.map(o => o->Option.flatMap(coerceToHead)),
103
+
substs->Array.map(o => o->Option.flatMap(coerceToLeft)),
133
104
~from?,
134
-
)->HeadBase.wrap
105
+
)->LeftBase.wrap
135
106
)
136
-
->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
137
-
let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
107
+
->getOrElse(() => Right.substDeBruijn(atom, substs, ~from?))
108
+
let concrete = atom => atom->onLeft(Left.concrete)->getOrElse(() => Right.concrete(atom))
138
109
}
139
110
140
111
module type ATOM_VIEW = {
141
112
module Atom: ATOM
142
-
type props = {name: Atom.t, scope: array<string>}
113
+
type props = {atom: Atom.t, scope: array<string>}
143
114
let make: props => React.element
144
115
}
145
116
146
-
module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
147
-
type props = {name: NilAtomList.t, scope: array<string>}
117
+
module EmptyAtomChoiceView: ATOM_VIEW with module Atom := EmptyAtomChoice = {
118
+
type props = {atom: EmptyAtomChoice.t, scope: array<string>}
148
119
let make = _ => throw(AtomExpected)
149
120
}
150
121
151
-
module MakeAtomView = (
122
+
module MakeAtomChoiceView = (
152
123
Left: ATOM,
153
124
LeftView: ATOM_VIEW with module Atom := Left,
154
-
Right: ATOM_LIST,
125
+
Right: ATOM_CHOICE,
155
126
RightView: ATOM_VIEW with module Atom := Right,
156
-
Combined: module type of CombineAtom(Left, Right),
127
+
Combined: module type of MakeAtomChoice(Left, Right),
157
128
): (ATOM_VIEW with module Atom := Combined) => {
158
-
type props = {name: Combined.t, scope: array<string>}
159
-
let make = ({name, scope}: props) =>
160
-
name
161
-
->Combined.onHead(left => <LeftView name={left} scope />)
162
-
->Util.Option.getOrElse(() => <RightView name scope />)
129
+
type props = {atom: Combined.t, scope: array<string>}
130
+
let make = ({atom, scope}: props) =>
131
+
atom
132
+
->Combined.onLeft(left => <LeftView atom={left} scope />)
133
+
->Util.Option.getOrElse(() => <RightView atom scope />)
163
134
}
164
135
165
-
module MakeAtomAndView = (
136
+
module MakeAtomChoiceAndView = (
166
137
Left: ATOM,
167
138
LeftView: ATOM_VIEW with module Atom := Left,
168
-
Right: ATOM_LIST,
139
+
Right: ATOM_CHOICE,
169
140
RightView: ATOM_VIEW with module Atom := Right,
170
141
) => {
171
-
module Atom = CombineAtom(Left, Right)
172
-
module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
142
+
module Atom = MakeAtomChoice(Left, Right)
143
+
module AtomView = MakeAtomChoiceView(Left, LeftView, Right, RightView, Atom)
173
144
}
+1
-1
src/HOTerm.res
+1
-1
src/HOTerm.res
+2
-2
src/SExp.res
+2
-2
src/SExp.res
···
150
150
let rec lower = (term: t): option<Atom.t> =>
151
151
switch term {
152
152
| Atom(s) => Some(s)
153
-
| Var({idx}) => Atom.coerce(AtomDef.VarBase.wrap(Var({idx: idx})))
153
+
| Var({idx}) => Atom.coerce(AtomBase.VarBase.wrap(Var({idx: idx})))
154
154
| Schematic({schematic, allowed}) =>
155
-
Atom.coerce(AtomDef.VarBase.wrap(Schematic({schematic, allowed})))
155
+
Atom.coerce(AtomBase.VarBase.wrap(Schematic({schematic, allowed})))
156
156
| Compound({subexps: [e1]}) => lower(e1)
157
157
| _ => None
158
158
}
+2
-2
src/SExpView.res
+2
-2
src/SExpView.res
···
55
55
->React.array}
56
56
</span>
57
57
| Var({idx}) => viewVar({idx, scope})
58
-
| Atom(name) =>
58
+
| Atom(atom) =>
59
59
<span className="term-const">
60
-
<AtomView name scope />
60
+
<AtomView atom scope />
61
61
</span>
62
62
| Schematic({schematic: s, allowed: vs}) =>
63
63
<span className="term-schematic">
+4
-4
src/Scratch.res
+4
-4
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 Symbol = AtomDef.MakeAtomAndView(
45
+
module Symbol = AtomDef.MakeAtomChoiceAndView(
46
46
Symbolic.Atom,
47
47
Symbolic.AtomView,
48
-
AtomDef.NilAtomList,
49
-
AtomDef.NilAtomListView,
48
+
AtomDef.EmptyAtomChoice,
49
+
AtomDef.EmptyAtomChoiceView,
50
50
)
51
-
module StringSymbol = AtomDef.MakeAtomAndView(
51
+
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
52
52
StringA.Atom,
53
53
StringA.AtomView,
54
54
Symbol.Atom,
+18
-23
src/StringA.res
+18
-23
src/StringA.res
···
3
3
let cmp = Pervasives.compare
4
4
})
5
5
6
-
type piece =
7
-
| String(string)
8
-
| Var({idx: int})
9
-
| Schematic({schematic: int, allowed: array<int>})
10
-
type t = array<piece>
11
-
type meta = string
12
-
type schematic = int
6
+
module Base = AtomBase.String
7
+
type t = Base.t
8
+
type piece = Base.piece
13
9
14
-
module BaseAtom = AtomDef.MakeBaseAtom({
15
-
type t = t
16
-
})
10
+
module Atom = {
11
+
module Base = Base
12
+
type t = Base.t
13
+
type schematic = int
14
+
type meta = string
17
15
18
-
module Atom = {
19
-
module BaseAtom = BaseAtom
20
-
type t = t
21
16
type subst = Map.t<schematic, t>
22
17
let substitute = (term: t, subst: subst) =>
23
18
Array.flatMap(term, piece => {
···
101
96
| (_, _) => {
102
97
let (s1, ss) = uncons(s)
103
98
switch s1 {
104
-
| Schematic({schematic, allowed}) =>
99
+
| Base.Schematic({schematic, allowed}) =>
105
100
Belt.Array.range(0, Array.length(t))
106
101
->Array.map(i => {
107
102
let subTerm = Array.slice(t, ~start=0, ~end=i)
···
155
150
let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array<
156
151
array<(int, graphSub)>,
157
152
> => {
158
-
let piece = Schematic({schematic, allowed})
153
+
let piece = Base.Schematic({schematic, allowed})
159
154
let sub = switch edge {
160
155
| Eps => singletonSubst(schematic, [])
161
156
| PieceLitSub(p) => singletonSubst(schematic, [p, piece])
···
383
378
switch execRe(identRegex)
384
379
->Option.orElse(execRe(symbolRegex))
385
380
->Option.orElse(execRe(numberRegex)) {
386
-
| Some([match], l) => add(String(match), ~nAdvance=l)
381
+
| Some([match], l) => add(Base.String(match), ~nAdvance=l)
387
382
| Some(_) => error("regex string lit error")
388
383
| None => error("expected string")
389
384
}
···
462
457
let concrete = t =>
463
458
t->Array.every(p =>
464
459
switch p {
465
-
| Schematic(_) => false
460
+
| Base.Schematic(_) => false
466
461
| _ => true
467
462
}
468
463
)
469
-
let coerce = (AtomDef.AnyValue(tag, a)) =>
464
+
let coerce = (AtomBase.AnyValue(tag, a)) =>
470
465
switch tag {
471
-
| Symbolic.BaseAtom.Tag => Some([String(a)])
472
-
| AtomDef.VarBase.Tag =>
466
+
| Symbolic.Base.Tag => Some([Base.String(a)])
467
+
| AtomBase.VarBase.Tag =>
473
468
Some([
474
469
switch a {
475
470
| Var({idx}) => Var({idx: idx})
···
481
476
}
482
477
483
478
module AtomView = {
484
-
type props = {name: t, scope: array<string>}
479
+
type props = {atom: t, scope: array<string>}
485
480
type idx_props = {idx: int, scope: array<string>}
486
481
let viewVar = (props: idx_props) =>
487
482
switch props.scope[props.idx] {
···
527
522
}
528
523
529
524
@react.componentWithProps
530
-
let make = ({name, scope}) =>
525
+
let make = ({atom, scope}) =>
531
526
<span className="term-compound">
532
527
{React.string("\"")}
533
-
{name
528
+
{atom
534
529
->Array.mapWithIndex((piece, i) => {
535
530
let key = Int.toString(i)
536
531
<Piece piece scope key />
+3
-7
src/StringA.resi
+3
-7
src/StringA.resi
···
1
-
type rec piece =
2
-
| String(string)
3
-
| Var({idx: int})
4
-
| Schematic({schematic: int, allowed: array<int>})
5
-
type t = array<piece>
1
+
type t = AtomBase.String.t
6
2
7
-
module BaseAtom: AtomDef.BASE_ATOM with type t = t
8
-
module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
3
+
module Base: AtomBase.BASE_ATOM with type t = t
4
+
module Atom: AtomDef.ATOM with module Base = Base
9
5
module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
+12
-7
src/StringAxiomSet.res
+12
-7
src/StringAxiomSet.res
···
2
2
open! Util
3
3
4
4
module Make = (
5
-
Atom: AtomDef.ATOM_LIST,
5
+
Atom: AtomDef.ATOM_CHOICE,
6
6
Term: module type of SExp.Make(Atom),
7
7
JudgmentView: Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Term,
8
8
) => {
···
34
34
35
35
let destructureOpt = (r: Term.t): option<(StringA.Atom.t, Symbolic.Atom.t)> =>
36
36
switch r {
37
-
| Compound({subexps: [Atom(AtomDef.AnyValue(tag1, s)), Atom(AtomDef.AnyValue(tag2, name))]}) =>
37
+
| Compound({
38
+
subexps: [Atom(AtomBase.AnyValue(tag1, s)), Atom(AtomBase.AnyValue(tag2, name))],
39
+
}) =>
38
40
switch (tag1, tag2) {
39
-
| (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
41
+
| (StringA.Base.Tag, Symbolic.Base.Tag) => Some((s, name))
40
42
| _ => None
41
43
}
42
44
| _ => None
···
85
87
let aIdx = vars->Array.findIndex(i => i == a)
86
88
let bIdx = vars->Array.findIndex(i => i == b)
87
89
let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
88
-
Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
90
+
Array.concat(
91
+
Array.concat([AtomBase.String.Var({idx: aIdx})], t),
92
+
[AtomBase.String.Var({idx: bIdx})],
93
+
)
89
94
}
90
95
let lookupGroup = (name: string): option<int> =>
91
96
mentionedGroups->Array.findIndexOpt(g => name == g.name)
···
106
111
vars: rule.vars,
107
112
premises: rule.premises->Array.concat(inductionHyps),
108
113
conclusion: structure(
109
-
Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.BaseAtom.wrap),
114
+
Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.Base.wrap),
110
115
Var({idx: pIdx + baseIdx}),
111
116
),
112
117
}
···
118
123
{
119
124
Rule.vars: [],
120
125
premises: [],
121
-
conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.BaseAtom.wrap)),
126
+
conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.Base.wrap)),
122
127
},
123
128
],
124
129
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
125
130
),
126
131
conclusion: structure(
127
-
Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.BaseAtom.wrap),
132
+
Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.Base.wrap),
128
133
Var({idx: 0}),
129
134
), // TODO: clean here
130
135
}
+4
-4
src/Symbolic.res
+4
-4
src/Symbolic.res
···
1
-
module BaseAtom = AtomDef.MakeBaseAtom({
1
+
module Base = AtomBase.Make({
2
2
type t = string
3
3
})
4
4
5
5
module Atom = {
6
-
module BaseAtom = BaseAtom
6
+
module Base = Base
7
7
type t = string
8
8
type subst = Map.t<int, string>
9
9
let unify = (a, b, ~gen as _=?) =>
···
27
27
}
28
28
29
29
module AtomView = {
30
-
type props = {name: string, scope: array<string>}
31
-
let make = (props: props) => React.string(props.name)
30
+
type props = {atom: string, scope: array<string>}
31
+
let make = (props: props) => React.string(props.atom)
32
32
}
+2
-2
src/Symbolic.resi
+2
-2
src/Symbolic.resi
···
1
-
module BaseAtom: AtomDef.BASE_ATOM with type t = string
2
-
module Atom: AtomDef.ATOM with module BaseAtom = BaseAtom
1
+
module Base: AtomBase.BASE_ATOM with type t = string
2
+
module Atom: AtomDef.ATOM with module Base = Base
3
3
module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom
+13
-15
tests/HOTermTest.res
+13
-15
tests/HOTermTest.res
···
3
3
4
4
module Util = TestUtil.MakeTerm(HOTerm)
5
5
6
-
module Symbol = AtomDef.MakeAtomAndView(
6
+
module Symbol = AtomDef.MakeAtomChoiceAndView(
7
7
Symbolic.Atom,
8
8
Symbolic.AtomView,
9
-
AtomDef.NilAtomList,
10
-
AtomDef.NilAtomListView,
9
+
AtomDef.EmptyAtomChoice,
10
+
AtomDef.EmptyAtomChoiceView,
11
11
)
12
-
module StringSymbol = AtomDef.MakeAtomAndView(
12
+
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
13
13
StringA.Atom,
14
14
StringA.AtomView,
15
15
Symbol.Atom,
···
18
18
module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
19
19
module StringUtil = TestUtil.MakeTerm(StringHOTerm)
20
20
let wrapString = s => StringHOTerm.Symbol({
21
-
name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
21
+
name: AtomBase.AnyValue(StringA.Base.Tag, s),
22
22
constructor: false,
23
23
})
24
24
let wrapSymbol = s => StringHOTerm.Symbol({
25
-
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
25
+
name: AtomBase.AnyValue(Symbolic.Base.Tag, s),
26
26
constructor: false,
27
27
})
28
28
···
169
169
})
170
170
171
171
zoraBlock("string HOTerm functor", t => {
172
+
module B = AtomBase.String
172
173
t->block("parse string atom", t => {
173
-
t->StringUtil.testParse(`"x y"`, wrapString([StringA.String("x"), StringA.String("y")]))
174
-
t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([StringA.Var({idx: 0})]))
174
+
t->StringUtil.testParse(`"x y"`, wrapString([String("x"), String("y")]))
175
+
t->StringUtil.testParse(`"$s"`, ~scope=["s"], wrapString([AtomBase.String.Var({idx: 0})]))
175
176
t->StringUtil.testParsePrettyPrint(`"x y"`, `"x y"`)
176
177
})
177
178
t->block("parse symbolic atom", t => {
···
179
180
t->StringUtil.testParse(
180
181
"@cons",
181
182
StringHOTerm.Symbol({
182
-
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, "cons"),
183
+
name: AtomBase.AnyValue(Symbolic.Base.Tag, "cons"),
183
184
constructor: true,
184
185
}),
185
186
)
···
194
195
let substAdd = StringHOTerm.substAdd
195
196
t->equal(
196
197
StringHOTerm.unify(parse(`"a ?0() c"`), parse(`"a b c"`))->Seq.head,
197
-
Some(emptySubst->substAdd(0, wrapString([StringA.String("b")]))),
198
+
Some(emptySubst->substAdd(0, wrapString([String("b")]))),
198
199
)
199
200
t->equal(
200
201
StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head,
201
-
Some(emptySubst->substAdd(1, wrapString([StringA.String("a")]))),
202
+
Some(emptySubst->substAdd(1, wrapString([String("a")]))),
202
203
)
203
204
let choices =
204
205
StringHOTerm.unify(parse(`"?1() a"`), parse(`"a ?1()"`))
···
206
207
->Seq.toArray
207
208
t->equal(
208
209
choices,
209
-
[
210
-
emptySubst->substAdd(1, wrapString([])),
211
-
emptySubst->substAdd(1, wrapString([StringA.String("a")])),
212
-
],
210
+
[emptySubst->substAdd(1, wrapString([])), emptySubst->substAdd(1, wrapString([String("a")]))],
213
211
)
214
212
t->equal(StringHOTerm.unify(parse(`"a"`), parse(`"b"`))->Seq.head, None)
215
213
})
+24
-18
tests/RuleTest.res
+24
-18
tests/RuleTest.res
···
31
31
}
32
32
}
33
33
34
-
module Symbol = AtomDef.MakeAtomAndView(
34
+
module Symbol = AtomDef.MakeAtomChoiceAndView(
35
35
Symbolic.Atom,
36
36
Symbolic.AtomView,
37
-
AtomDef.NilAtomList,
38
-
AtomDef.NilAtomListView,
37
+
AtomDef.EmptyAtomChoice,
38
+
AtomDef.EmptyAtomChoiceView,
39
39
)
40
-
module StringSymbol = AtomDef.MakeAtomAndView(
40
+
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
41
41
StringA.Atom,
42
42
StringA.AtomView,
43
43
Symbol.Atom,
···
45
45
)
46
46
47
47
zoraBlock("string terms", t => {
48
+
module Symbol = AtomDef.MakeAtomChoiceAndView(
49
+
Symbolic.Atom,
50
+
Symbolic.AtomView,
51
+
AtomDef.EmptyAtomChoice,
52
+
AtomDef.EmptyAtomChoiceView,
53
+
)
54
+
module StringSymbol = AtomDef.MakeAtomChoiceAndView(
55
+
StringA.Atom,
56
+
StringA.AtomView,
57
+
Symbol.Atom,
58
+
Symbol.AtomView,
59
+
)
48
60
module StringSExp = SExp.Make(StringSymbol.Atom)
49
-
let wrapString = (s): StringSExp.t => Atom(AtomDef.AnyValue(StringA.BaseAtom.Tag, s))
50
-
let wrapSymbol = (s): StringSExp.t => Atom(AnyValue(Symbolic.BaseAtom.Tag, s))
61
+
let wrapString = (s): StringSExp.t => s->AtomBase.String.wrap->Atom
62
+
let wrapSymbol = (s): StringSExp.t => s->Symbolic.Base.wrap->Atom
51
63
module T = MakeTest(StringSExp, StringSExp)
52
64
t->T.testParseInner(
53
65
`[s1. ("$s1" p) |- ("($s1)" p)]`,
···
58
70
vars: [],
59
71
premises: [],
60
72
conclusion: StringSExp.Compound({
61
-
subexps: [wrapString([StringA.Var({idx: 0})]), wrapSymbol("p")],
73
+
subexps: [wrapString([Var({idx: 0})]), wrapSymbol("p")],
62
74
}),
63
75
},
64
76
],
65
77
conclusion: StringSExp.Compound({
66
-
subexps: [
67
-
wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
68
-
wrapSymbol("p"),
69
-
],
78
+
subexps: [wrapString([String("("), Var({idx: 0}), String(")")]), wrapSymbol("p")],
70
79
}),
71
80
},
72
81
)
···
75
84
zoraBlock("string HOTerms", t => {
76
85
module StringHOTerm = HOTerm.Make(StringSymbol.Atom)
77
86
let wrapString = (s): StringHOTerm.t => Symbol({
78
-
name: AtomDef.AnyValue(StringA.BaseAtom.Tag, s),
87
+
name: AtomBase.AnyValue(AtomBase.String.Tag, s),
79
88
constructor: false,
80
89
})
81
90
let wrapSymbol = (s): StringHOTerm.t => Symbol({
82
-
name: AtomDef.AnyValue(Symbolic.BaseAtom.Tag, s),
91
+
name: AtomBase.AnyValue(Symbolic.Base.Tag, s),
83
92
constructor: false,
84
93
})
85
94
let app = StringHOTerm.app
···
92
101
{
93
102
vars: [],
94
103
premises: [],
95
-
conclusion: app(wrapString([StringA.Var({idx: 0})]), [wrapSymbol("p")]),
104
+
conclusion: app(wrapString([Var({idx: 0})]), [wrapSymbol("p")]),
96
105
},
97
106
],
98
-
conclusion: app(
99
-
wrapString([StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")]),
100
-
[wrapSymbol("p")],
101
-
),
107
+
conclusion: app(wrapString([String("("), Var({idx: 0}), String(")")]), [wrapSymbol("p")]),
102
108
},
103
109
)
104
110
})