the next generation of the in-browser educational proof assistant
1// type level stuff to enable well-typed coercions
2type atomTag<_> = ..
3type rec anyValue = AnyValue(atomTag<'a>, 'a): anyValue
4
5// to allow circular coercions, we declare base types
6// separately from relevant implementation
7module type BASE_ATOM = {
8 type t
9 type atomTag<_> += Tag: atomTag<t>
10 let wrap: t => anyValue
11}
12
13module 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}
22
23module type ATOM = {
24 module BaseAtom: BASE_ATOM
25 type t = BaseAtom.t
26 type subst = Map.t<int, t>
27 let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst>
28 let prettyPrint: (t, ~scope: array<string>) => string
29 let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
30 let substitute: (t, subst) => t
31 let upshift: (t, int, ~from: int=?) => t
32 let substDeBruijn: (t, array<option<t>>, ~from: int=?) => t
33 let concrete: t => bool
34 let coerce: anyValue => option<t>
35}
36
37type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>})
38module VarBase = MakeBaseAtom({
39 type t = varBase
40})
41
42exception AtomExpected
43
44module AtomListBase = MakeBaseAtom({
45 type t = anyValue
46})
47
48module type ATOM_LIST = {
49 module HeadBase: BASE_ATOM
50 include ATOM with module BaseAtom = AtomListBase
51 let onHead: (t, HeadBase.t => 'a) => option<'a>
52}
53
54module NilAtomList: ATOM_LIST = {
55 module HeadBase = MakeBaseAtom({
56 // empty
57 type t = {.}
58 })
59 module BaseAtom = AtomListBase
60 type t = BaseAtom.t
61 type subst = Map.t<int, t>
62 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 let unify = (_, _, ~gen as _=?) => Seq.empty
68 // this should probably throw too, but will be more
69 // informative to have it appear wherever it's called from
70 let prettyPrint = (_, ~scope as _) => "NIL (THIS IS AN ERROR!)"
71 let onHead = (_, _) => throw(AtomExpected)
72 let coerce = _ => throw(AtomExpected)
73 let substitute = (_, _) => throw(AtomExpected)
74 let upshift = (_, _, ~from as _=?) => throw(AtomExpected)
75 let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected)
76 let concrete = _ => throw(AtomExpected)
77}
78
79module CombineAtom = (Head: ATOM, Tail: ATOM_LIST): (
80 ATOM_LIST with module HeadBase = Head.BaseAtom
81) => {
82 module HeadBase = Head.BaseAtom
83 module Tail = Tail
84 module BaseAtom = AtomListBase
85 type t = BaseAtom.t
86 type subst = Map.t<int, t>
87 type gen = ref<int>
88 let getOrElse = Util.Option.getOrElse
89 let coerce = v => Some(v)
90 let onHead = (AnyValue(tag, val), f: Head.t => 'a): option<'a> =>
91 switch tag {
92 | Head.BaseAtom.Tag => Some(f(val))
93 | _ => None
94 }
95 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?))
99 }
100 let prettyPrint = (atom, ~scope) =>
101 atom
102 ->onHead(val => Head.prettyPrint(val, ~scope))
103 ->getOrElse(() => Tail.prettyPrint(atom, ~scope))
104
105 let unify = (a1, a2, ~gen=?) => {
106 let (AnyValue(tag1, val1), AnyValue(tag2, val2)) = (a1, a2)
107 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?)
111 }
112 }
113 let coerceToHead = (atom): option<Head.t> =>
114 atom->onHead(val => Some(val))->getOrElse(() => Head.coerce(atom))
115 let substitute = (atom, subst: subst) =>
116 atom
117 ->onHead(val => {
118 let leftSubs = subst->Util.Map.filterMap((_, v) => coerceToHead(v))
119 Head.substitute(val, leftSubs)->HeadBase.wrap
120 })
121 ->getOrElse(() => Tail.substitute(atom, subst))
122
123 let upshift = (atom, amount: int, ~from=?) =>
124 atom
125 ->onHead(val => Head.upshift(val, amount, ~from?)->HeadBase.wrap)
126 ->getOrElse(() => Tail.upshift(atom, amount, ~from?))
127 let substDeBruijn = (atom, substs: array<option<t>>, ~from=?) =>
128 atom
129 ->onHead(val =>
130 Head.substDeBruijn(
131 val,
132 substs->Array.map(o => o->Option.flatMap(coerceToHead)),
133 ~from?,
134 )->HeadBase.wrap
135 )
136 ->getOrElse(() => Tail.substDeBruijn(atom, substs, ~from?))
137 let concrete = atom => atom->onHead(Head.concrete)->getOrElse(() => Tail.concrete(atom))
138}
139
140module type ATOM_VIEW = {
141 module Atom: ATOM
142 type props = {name: Atom.t, scope: array<string>}
143 let make: props => React.element
144}
145
146module NilAtomListView: ATOM_VIEW with module Atom := NilAtomList = {
147 type props = {name: NilAtomList.t, scope: array<string>}
148 let make = _ => throw(AtomExpected)
149}
150
151module MakeAtomView = (
152 Left: ATOM,
153 LeftView: ATOM_VIEW with module Atom := Left,
154 Right: ATOM_LIST,
155 RightView: ATOM_VIEW with module Atom := Right,
156 Combined: module type of CombineAtom(Left, Right),
157): (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 />)
163}
164
165module MakeAtomAndView = (
166 Left: ATOM,
167 LeftView: ATOM_VIEW with module Atom := Left,
168 Right: ATOM_LIST,
169 RightView: ATOM_VIEW with module Atom := Right,
170) => {
171 module Atom = CombineAtom(Left, Right)
172 module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom)
173}