the next generation of the in-browser educational proof assistant
remove StringTermJudgment
+33
-45
+11
-10
src/Scratch.res
+11
-10
src/Scratch.res
···
1
1
module HOTermJ = TermAsJudgment.HOTermJ
2
+
module StringSExpJ = TermAsJudgment.StringSExpJ
2
3
3
4
module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTermJ, HOTermJView))
4
5
module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTermJ, HOTermJView))
···
51
52
52
53
module AxiomStr = Editable.TextArea(StringAxiomSet)
53
54
module DerivationsOrLemmasStrView = MethodView.CombineMethodView(
54
-
StringTermJudgment.StringSExp,
55
-
StringTermJudgment.StringSExpJ,
56
-
MethodView.DerivationView(StringTermJudgment.StringSExp, StringTermJudgment.StringSExpJ),
55
+
StringSExp,
56
+
StringSExpJ,
57
+
MethodView.DerivationView(StringSExp, StringSExpJ),
57
58
MethodView.LemmaView(
58
-
StringTermJudgment.StringSExp,
59
-
StringTermJudgment.StringSExpJ,
59
+
StringSExp,
60
+
StringSExpJ,
60
61
StringTermJView,
61
62
),
62
63
)
63
64
module DLEStrView = MethodView.CombineMethodView(
64
-
StringTermJudgment.StringSExp,
65
-
StringTermJudgment.StringSExpJ,
65
+
StringSExp,
66
+
StringSExpJ,
66
67
DerivationsOrLemmasStrView,
67
-
MethodView.EliminationView(StringTermJudgment.StringSExp, StringTermJudgment.StringSExpJ),
68
+
MethodView.EliminationView(StringSExp, StringSExpJ),
68
69
)
69
70
module TheoremStr = Editable.TextArea(
70
71
Theorem.Make(
71
-
StringTermJudgment.StringSExp,
72
-
StringTermJudgment.StringSExpJ,
72
+
StringSExp,
73
+
StringSExpJ,
73
74
StringTermJView,
74
75
DLEStrView,
75
76
),
+4
-4
src/StringAxiomSet.res
+4
-4
src/StringAxiomSet.res
···
1
1
open Component
2
2
3
-
module Term = StringTermJudgment.StringSExp
4
-
module Judgment = StringTermJudgment.StringSExpJ
3
+
module Term = StringSExp
4
+
module Judgment = TermAsJudgment.StringSExpJ
5
5
module JudgmentView = StringTermJView
6
6
7
7
module Rule = Rule.Make(Term, Judgment)
···
24
24
}
25
25
26
26
module Set = Belt.Set.String
27
-
module SExp = StringTermJudgment.StringSExp
27
+
module SExp = StringSExp
28
28
let varsInRule = (rule: Rule.t) => {
29
29
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
30
30
s->Set.union(Set.fromArray(r.vars))
···
37
37
| _ => None
38
38
}
39
39
40
-
open StringTermJudgment
40
+
open StringSExp
41
41
let destructure = (r: Judgment.t): (StringTerm.t, string) =>
42
42
switch r {
43
43
| Compound({subexps: [Symbol(StringS(s)), Symbol(ConstS(name))]}) => (s, name)
+4
src/StringSExp.resi
+4
src/StringSExp.resi
+6
-11
src/StringTermJView.res
+6
-11
src/StringTermJView.res
···
1
-
module StringSymbolView: SExpViewFunc.SYMBOL_VIEW
2
-
with module Symbol := StringTermJudgment.StringSymbol = {
3
-
type props = {name: StringTermJudgment.StringSymbol.t, scope: array<string>}
1
+
module StringSymbolView: SExpViewFunc.SYMBOL_VIEW with module Symbol := StringSExp.StringSymbol = {
2
+
type props = {name: StringSExp.StringSymbol.t, scope: array<string>}
4
3
let make = ({name, scope}: props) =>
5
4
switch name {
6
-
| StringTermJudgment.StringS(term) => <StringTermView term scope />
7
-
| StringTermJudgment.ConstS(name) => <SExpView.ConstSymbolView name scope />
5
+
| StringSExp.StringS(term) => <StringTermView term scope />
6
+
| StringSExp.ConstS(name) => <SExpView.ConstSymbolView name scope />
8
7
}
9
8
}
10
9
11
-
module View = SExpViewFunc.Make(
12
-
StringTermJudgment.StringSymbol,
13
-
StringSymbolView,
14
-
StringTermJudgment.StringSExp,
15
-
)
10
+
module View = SExpViewFunc.Make(StringSExp.StringSymbol, StringSymbolView, StringSExp)
16
11
17
12
module TermView = View
18
13
type props = {
19
-
judgment: StringTermJudgment.StringSExp.t,
14
+
judgment: StringSExp.t,
20
15
scope: array<string>,
21
16
}
22
17
let make = ({judgment, scope}) => View.make({term: judgment, scope})
+2
-2
src/StringTermJView.resi
+2
-2
src/StringTermJView.resi
+1
-5
src/StringTermJudgment.res
src/StringSExp.res
+1
-5
src/StringTermJudgment.res
src/StringSExp.res
···
60
60
}
61
61
}
62
62
63
-
module StringSExp = SExpFunc.Make(StringSymbol)
64
-
module StringSExpJ = TermAsJudgment.Make(StringSExp)
65
-
include TermAsJudgment.Make(StringSExp)
66
-
67
-
let constSymbol = (s: string): StringSExp.t => s->ConstS->StringSExp.Symbol
63
+
include SExpFunc.Make(StringSymbol)
-9
src/StringTermJudgment.resi
-9
src/StringTermJudgment.resi
···
1
-
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
2
-
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol
3
-
4
-
module StringSExp: module type of SExpFunc.Make(StringSymbol)
5
-
module StringSExpJ: module type of TermAsJudgment.Make(StringSExp)
6
-
type t = StringSExpJ.t
7
-
let constSymbol: string => StringSExp.t
8
-
9
-
include Signatures.JUDGMENT with module Term := StringSExp and type t := t
+1
src/TermAsJudgment.res
+1
src/TermAsJudgment.res
+4
-4
tests/RuleTest.res
+4
-4
tests/RuleTest.res
···
32
32
}
33
33
34
34
// zoraBlock("string terms", t => {
35
-
// module T = MakeTest(StringTermJudgment.StringSExp, StringTermJudgment.StringSExpJ)
35
+
// module T = MakeTest(StringSExp, StringSExpJ)
36
36
// t->T.testParseInner(
37
37
// `[s1. ("$s1" p) |- ("($s1)" p)]`,
38
38
// {
···
41
41
// {
42
42
// vars: [],
43
43
// premises: [],
44
-
// conclusion: StringTermJudgment.StringSExp.Compound(
44
+
// conclusion: StringSExp.Compound(
45
45
// [StringTerm.Var({idx: 0})],
46
-
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringTermJudgment.StringSExp.Symbol,
46
+
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringSExp.Symbol,
47
47
// ),
48
48
// },
49
49
// ],
50
50
// conclusion: (
51
51
// [StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")],
52
-
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringTermJudgment.StringSExp.Symbol,
52
+
// SExp.pSymbol("p")->StringTermJudgment.ConstS->StringSExp.Symbol,
53
53
// ),
54
54
// },
55
55
// )