the next generation of the in-browser educational proof assistant
finished?
+110
-17
+4
-2
src/SExp.res
+4
-2
src/SExp.res
···
1
-
module ConstSymbol: SExpFunc.SYMBOL = {
1
+
module ConstSymbol: SExpFunc.SYMBOL with type t = string = {
2
2
type t = string
3
3
type subst = Map.t<int, string>
4
4
let unify = (a, b) =>
···
10
10
let prettyPrint = (name, ~scope as _: array<string>) => name
11
11
let parse = (string, ~scope as _: array<string>, ~gen as _=?) => Ok((string, ""))
12
12
let substitute = (name, _) => name
13
+
let constSymbol = name => Some(name)
13
14
}
14
15
15
16
include SExpFunc.Make(ConstSymbol)
16
-
let symbol = s => s->ConstSymbol.parse(~scope=[])->Result.getExn->Pair.first->Symbol
17
+
let pSymbol = s => s->ConstSymbol.parse(~scope=[])->Result.getExn->Pair.first
18
+
let symbol = s => s->pSymbol->Symbol
17
19
let getSymbol = s => s->ConstSymbol.prettyPrint(~scope=[])
+4
-1
src/SExp.resi
+4
-1
src/SExp.resi
···
1
-
module ConstSymbol: SExpFunc.SYMBOL
1
+
// TODO: i only added the with type t = string later.
2
+
// may remove need for helpers down bottom
3
+
module ConstSymbol: SExpFunc.SYMBOL with type t = string
2
4
3
5
include module type of SExpFunc.Make(ConstSymbol)
4
6
let symbol: string => t
7
+
let pSymbol: string => ConstSymbol.t
5
8
let getSymbol: ConstSymbol.t => string
+2
src/SExpFunc.res
+2
src/SExpFunc.res
···
5
5
let prettyPrint: (t, ~scope: array<string>) => string
6
6
let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string>
7
7
let substitute: (t, subst) => t
8
+
// used for grouping judgments together for rule induction
9
+
let constSymbol: t => option<string>
8
10
}
9
11
10
12
module IntCmp = Belt.Id.MakeComparable({
+68
src/SExpViewFunc.res
+68
src/SExpViewFunc.res
···
1
+
module Make = (Symbol: SExpFunc.SYMBOL, SExp: module type of SExpFunc.Make(Symbol)): {
2
+
include Signatures.TERM_VIEW with module Term := SExp
3
+
} => {
4
+
type props = {term: SExp.t, scope: array<string>}
5
+
open Util
6
+
type idx_props = {idx: int, scope: array<string>}
7
+
let viewVar = (props: idx_props) =>
8
+
switch props.scope[props.idx] {
9
+
| Some(n) if Array.indexOf(props.scope, n) == props.idx =>
10
+
<span className="term-metavar"> {React.string(n)} </span>
11
+
| _ =>
12
+
<span className="term-metavar-unnamed">
13
+
{React.string("\\")}
14
+
{React.int(props.idx)}
15
+
</span>
16
+
}
17
+
18
+
let makeMeta = (str: string) =>
19
+
<span className="rule-binder">
20
+
{React.string(str)}
21
+
{React.string(".")}
22
+
</span>
23
+
24
+
let parenthesise = f =>
25
+
[
26
+
<span className="symbol" key={"-1"}> {React.string("(")} </span>,
27
+
...f,
28
+
<span className="symbol" key={"-2"}> {React.string(")")} </span>,
29
+
]
30
+
31
+
let intersperse = a =>
32
+
a->Array.flatMapWithIndex((e, i) =>
33
+
if i == 0 {
34
+
[e]
35
+
} else {
36
+
[React.string(" "), e]
37
+
}
38
+
)
39
+
40
+
@react.componentWithProps
41
+
let rec make = ({term, scope}) =>
42
+
switch term {
43
+
| Compound({subexps: bits}) =>
44
+
<span className="term-compound">
45
+
{bits
46
+
->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i)))
47
+
->intersperse
48
+
->parenthesise
49
+
->React.array}
50
+
</span>
51
+
| Var({idx}) => viewVar({idx, scope})
52
+
| Symbol(name) =>
53
+
<span className="term-const"> {React.string(name->SExp.Symbol.prettyPrint(~scope))} </span>
54
+
| Schematic({schematic: s, allowed: vs}) =>
55
+
<span className="term-schematic">
56
+
{React.string("?")}
57
+
{React.int(s)}
58
+
<span className="term-schematic-telescope">
59
+
{vs
60
+
->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
61
+
->intersperse
62
+
->parenthesise
63
+
->React.array}
64
+
</span>
65
+
</span>
66
+
| Ghost => React.null
67
+
}
68
+
}
+12
-9
src/StringAxiomSet.res
+12
-9
src/StringAxiomSet.res
···
24
24
}
25
25
26
26
module Set = Belt.Set.String
27
+
module SExp = StringTermJudgment.StringSExp
27
28
let varsInRule = (rule: Rule.t) => {
28
29
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
29
30
s->Set.union(Set.fromArray(r.vars))
···
78
79
Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})])
79
80
}
80
81
let lookupGroup = (t: SExp.t): option<int> =>
81
-
mentionedGroups->Array.findIndexOpt(g => t == SExp.symbol(g.name))
82
+
mentionedGroups->Array.findIndexOpt(g => t == StringTermJudgment.constSymbol(g.name))
82
83
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
83
84
let baseIdx = baseIdx + Array.length(rule.vars)
84
85
let inductionHyps =
···
102
103
{
103
104
Rule.vars: [],
104
105
premises: [],
105
-
conclusion: ([StringTerm.Var({idx: xIdx})], SExp.symbol(group.name)),
106
+
conclusion: ([StringTerm.Var({idx: xIdx})], StringTermJudgment.constSymbol(group.name)),
106
107
},
107
108
],
108
109
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
···
144
145
let grouped: dict<array<Rule.t>> = Dict.make()
145
146
raw->Dict.forEach(rule =>
146
147
switch rule.conclusion->Pair.second {
147
-
| Symbol(name) => {
148
-
let name = SExp.getSymbol(name)
149
-
switch grouped->Dict.get(name) {
150
-
| None => grouped->Dict.set(name, [rule])
151
-
| Some(rs) => rs->Array.push(rule)
152
-
}
153
-
}
148
+
| Symbol(name) => StringTermJudgment.StringSymbol.constSymbol(name)
149
+
->Option.map(
150
+
name =>
151
+
switch grouped->Dict.get(name) {
152
+
| None => grouped->Dict.set(name, [rule])
153
+
| Some(rs) => rs->Array.push(rule)
154
+
},
155
+
)
156
+
->ignore
154
157
| _ => ()
155
158
}
156
159
)
+1
src/StringTermJView.res
+1
src/StringTermJView.res
+10
-2
src/StringTermJudgment.res
+10
-2
src/StringTermJudgment.res
···
1
-
module StringSymbol: SExpFunc.SYMBOL = {
2
-
type t = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
1
+
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
2
+
3
+
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol = {
4
+
type t = stringSymbol
3
5
type subst = Map.t<int, t>
4
6
type gen = ref<int>
5
7
let parse = (s, ~scope, ~gen: option<gen>=?) => {
···
35
37
}
36
38
| ConstS(s) => ConstS(s)
37
39
}
40
+
let constSymbol = s =>
41
+
switch s {
42
+
| StringS(_) => None
43
+
| ConstS(s) => SExp.ConstSymbol.constSymbol(s)
44
+
}
38
45
}
39
46
module StringSExp = SExpFunc.Make(StringSymbol)
47
+
let constSymbol = (s: string): StringSExp.t => StringSExp.Symbol(ConstS(SExp.pSymbol(s)))
40
48
41
49
let toSExp = (t: StringTerm.t): StringSExp.t => {
42
50
let convertPiece = (p: StringTerm.piece): StringSExp.t =>
+4
-1
src/StringTermJudgment.resi
+4
-1
src/StringTermJudgment.resi
···
1
-
module StringSymbol: SExpFunc.SYMBOL
1
+
type stringSymbol = StringS(StringTerm.t) | ConstS(SExp.ConstSymbol.t)
2
+
module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol
3
+
2
4
module StringSExp: module type of SExpFunc.Make(StringSymbol)
3
5
4
6
type t = (StringTerm.t, StringSExp.t)
7
+
let constSymbol: string => StringSExp.t
5
8
6
9
include Signatures.JUDGMENT with module Term := StringTerm and type t := t
+5
-2
tests/RuleTest.res
+5
-2
tests/RuleTest.res
···
41
41
{
42
42
vars: [],
43
43
premises: [],
44
-
conclusion: ([StringTerm.Var({idx: 0})], SExp.symbol("p")),
44
+
conclusion: (
45
+
[StringTerm.Var({idx: 0})],
46
+
SExp.pSymbol("p")->StringTermJudgment.ConstS->StringTermJudgment.StringSExp.Symbol,
47
+
),
45
48
},
46
49
],
47
50
conclusion: (
48
51
[StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")],
49
-
SExp.symbol("p"),
52
+
SExp.pSymbol("p")->StringTermJudgment.ConstS->StringTermJudgment.StringSExp.Symbol,
50
53
),
51
54
},
52
55
)