the next generation of the in-browser educational proof assistant
slightly neater workaround for sexp functor
+26
-63
+2
-18
src/SExp.resi
+2
-18
src/SExp.resi
···
1
-
// NOTE: ideally we want something like:
2
-
// include module type of SExpFunc.Make(ConstAtom)
3
-
// this doesn't work because reasons. can come back to revisit
4
-
// but i honestly suspect this is a rescript compiler bug.
5
-
6
-
module Atom: SExpFunc.ATOM with type t = string
7
-
type rec t =
8
-
| Atom(Atom.t)
9
-
| Compound({subexps: array<t>})
10
-
| Var({idx: int})
11
-
| Schematic({schematic: int, allowed: array<int>})
12
-
| Ghost
1
+
module SymbolAtom: SExpFunc.ATOM with type t = string
13
2
14
-
include Signatures.TERM
15
-
with type t := t
16
-
and type meta = string
17
-
and type schematic = int
18
-
and type subst = Map.t<int, t>
19
-
let mapTerms: (t, t => t) => t
3
+
include module type of SExpFunc.Make(SymbolAtom)
-2
src/SExpFunc.res
-2
src/SExpFunc.res
+2
-1
src/SExpJView.res
+2
-1
src/SExpJView.res
+4
-1
src/SExpJView.resi
+4
-1
src/SExpJView.resi
···
1
-
include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExp
1
+
// really feel like this shouldn't be necessary...
2
+
module SExpJ: Signatures.JUDGMENT with module Term := SExp and type t = SExp.t
3
+
4
+
include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExpJ
+2
-3
src/SExpView.res
+2
-3
src/SExpView.res
···
1
-
module ConstAtom = SExp.Atom
2
-
module ConstAtomView: SExpViewFunc.ATOM_VIEW with module Atom := SExp.Atom = {
1
+
module SymbolAtomView: SExpViewFunc.ATOM_VIEW with module Atom := SExp.SymbolAtom = {
3
2
type props = {name: string, scope: array<string>}
4
3
let make = (props: props) => React.string(props.name)
5
4
}
6
5
7
-
include SExpViewFunc.Make(ConstAtom, ConstAtomView, SExp)
6
+
include SExpViewFunc.Make(SExp.SymbolAtom, SymbolAtomView, SExp)
+1
-1
src/SExpView.resi
+1
-1
src/SExpView.resi
+1
-14
src/SExpViewFunc.res
+1
-14
src/SExpViewFunc.res
···
7
7
module Make = (
8
8
Atom: SExpFunc.ATOM,
9
9
AtomView: ATOM_VIEW with module Atom := Atom,
10
-
SExp: {
11
-
type rec t =
12
-
| Atom(Atom.t)
13
-
| Compound({subexps: array<t>})
14
-
| Var({idx: int})
15
-
| Schematic({schematic: int, allowed: array<int>})
16
-
| Ghost
17
-
include Signatures.TERM
18
-
with type t := t
19
-
and type meta = string
20
-
and type schematic = int
21
-
and type subst = Map.t<int, t>
22
-
let mapTerms: (t, t => t) => t
23
-
},
10
+
SExp: module type of SExpFunc.Make(Atom),
24
11
): {
25
12
include Signatures.TERM_VIEW with module Term := SExp
26
13
} => {
+1
-1
src/StringAxiomSet.res
+1
-1
src/StringAxiomSet.res
+6
-4
src/StringSExp.res
+6
-4
src/StringSExp.res
···
1
-
type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t)
1
+
type stringSExpAtom = StringS(StringAtom.t) | ConstS(string)
2
2
3
3
module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom = {
4
4
type t = stringSExpAtom
···
8
8
StringAtom.parse(s, ~scope, ~gen?)
9
9
->Result.map(((r, rest)) => (StringS(r), rest))
10
10
->Util.Result.or(() =>
11
-
SExp.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
11
+
SExp.SymbolAtom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest))
12
12
)
13
13
}
14
14
let prettyPrint = (s, ~scope) =>
15
15
switch s {
16
16
| StringS(s) => StringAtom.prettyPrint(s, ~scope)
17
-
| ConstS(s) => SExp.Atom.prettyPrint(s, ~scope)
17
+
| ConstS(s) => SExp.SymbolAtom.prettyPrint(s, ~scope)
18
18
}
19
19
let unify = (s1, s2, ~gen=?) =>
20
20
switch (s1, s2) {
21
21
| (StringS(s1), StringS(s2)) =>
22
22
StringAtom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v)))
23
23
| (ConstS(s1), ConstS(s2)) =>
24
-
SExp.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v)))
24
+
SExp.SymbolAtom.unify(s1, s2, ~gen?)->Seq.map(subst =>
25
+
subst->Util.mapMapValues(v => ConstS(v))
26
+
)
25
27
| (_, _) => Seq.empty
26
28
}
27
29
let substitute = (s, subst: subst) =>
+2
-16
src/StringSExp.resi
+2
-16
src/StringSExp.resi
···
1
-
type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t)
1
+
type stringSExpAtom = StringS(StringAtom.t) | ConstS(string)
2
2
module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom
3
3
4
-
type rec t =
5
-
| Atom(StringSExpAtom.t)
6
-
| Compound({subexps: array<t>})
7
-
| Var({idx: int})
8
-
| Schematic({schematic: int, allowed: array<int>})
9
-
| Ghost
10
-
11
-
include Signatures.TERM
12
-
with type t := t
13
-
and type meta = string
14
-
and type schematic = int
15
-
and type subst = Map.t<int, t>
16
-
17
-
module Atom: SExpFunc.ATOM with type t := StringSExpAtom.t
18
-
let mapTerms: (t, t => t) => t
4
+
include module type of SExpFunc.Make(StringSExpAtom)
+2
-1
src/StringSExpJView.res
+2
-1
src/StringSExpJView.res
···
3
3
let make = ({name, scope}: props) =>
4
4
switch name {
5
5
| StringSExp.StringS(name) => <StringAtomView name scope />
6
-
| StringSExp.ConstS(name) => <SExpView.ConstAtomView name scope />
6
+
| StringSExp.ConstS(name) => <SExpView.SymbolAtomView name scope />
7
7
}
8
8
}
9
9
10
+
module StringSExpJ = StringSExp
10
11
module View = SExpViewFunc.Make(StringSExp.StringSExpAtom, StringAtomView, StringSExp)
11
12
12
13
module TermView = View
+3
-1
src/StringSExpJView.resi
+3
-1
src/StringSExpJView.resi
···
1
-
include Signatures.JUDGMENT_VIEW with module Term := StringSExp and module Judgment := StringSExp
1
+
module StringSExpJ: Signatures.JUDGMENT with module Term := StringSExp and type t = StringSExp.t
2
+
3
+
include Signatures.JUDGMENT_VIEW with module Term := StringSExp and module Judgment := StringSExpJ