the previous organisation didn't actually quite allow circular coercions, which wasn't discovered because there weren't any.
resolve conflicts
+177
-172
Diff
round #2
+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
13
-
14
-
module BaseAtom = AtomDef.MakeBaseAtom({
15
-
type t = t
16
-
})
6
+
module Base = AtomBase.String
7
+
type t = Base.t
8
+
type piece = Base.piece
17
9
18
10
module Atom = {
19
-
module BaseAtom = BaseAtom
20
-
type t = t
11
+
module Base = Base
12
+
type t = Base.t
13
+
type schematic = int
14
+
type meta = string
15
+
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
})
History
3 rounds
0 comments
joshcbrown.tngl.sh
submitted
#2
1 commit
expand
collapse
reorganise atom defns
the previous organisation didn't actually quite allow circular
coercions, which wasn't discovered because there weren't any.
resolve conflicts
merge conflicts detected
expand
collapse
expand
collapse
- src/AtomDef.res:1
- src/HOTerm.res:6
- src/SExp.res:150
- src/SExpView.res:55
- src/Scratch.res:42
- src/StringA.res:3
- src/StringA.resi:1
- src/StringAxiomSet.res:2
- src/Symbolic.res:1
- src/Symbolic.resi:1
- tests/HOTermTest.res:3
- tests/RuleTest.res:31
expand 0 comments
joshcbrown.tngl.sh
submitted
#1
1 commit
expand
collapse
reorganise atom defns
the previous organisation didn't actually quite allow circular
coercions, which wasn't discovered because there weren't any.
expand 0 comments
joshcbrown.tngl.sh
submitted
#0
1 commit
expand
collapse
reorganise atom defns
the previous organisation didn't actually quite allow circular
coercions, which wasn't discovered because there weren't any.