the next generation of the in-browser educational proof assistant
1open Component
2open! Util
3
4module Make = (
5 Atom: AtomDef.ATOM_LIST,
6 Term: module type of SExp.Make(Atom),
7 JudgmentView: Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Term,
8) => {
9 module Rule = Rule.Make(Term, Term)
10 module RuleView = RuleView.Make(Term, Term, JudgmentView)
11 module Ports = Ports(Term, Term)
12 type state = {
13 raw: dict<Rule.t>,
14 derived: dict<Rule.t>,
15 }
16
17 type props = {
18 content: state,
19 imports: Ports.t,
20 onChange: (state, ~exports: Ports.t=?) => unit,
21 }
22
23 type judgeGroup = {
24 name: string,
25 rules: array<Rule.t>,
26 }
27
28 module Set = Belt.Set.String
29 let varsInRule = (rule: Rule.t) => {
30 rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
31 s->Set.union(Set.fromArray(r.vars))
32 )
33 }
34
35 let destructureOpt = (r: Term.t): option<(StringA.Atom.t, Symbolic.Atom.t)> =>
36 switch r {
37 | Compound({subexps: [Atom(AtomDef.AnyValue(tag1, s)), Atom(AtomDef.AnyValue(tag2, name))]}) =>
38 switch (tag1, tag2) {
39 | (StringA.BaseAtom.Tag, Symbolic.BaseAtom.Tag) => Some((s, name))
40 | _ => None
41 }
42 | _ => None
43 }
44 exception InvalidStringInductionPattern
45 let destructure = (r: Term.t): (StringA.Atom.t, string) =>
46 destructureOpt(r)->Option.getOrElse(() => throw(InvalidStringInductionPattern))
47 let structure = (lhs: Term.t, rhs: Term.t): Term.t => Compound({
48 subexps: [lhs, rhs],
49 })
50 let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
51 judgeGroup,
52 > => {
53 let allGroupNames = allGroups->Array.map(g => g.name)
54 let groupNames: array<string> = Array.concat(
55 [group.name],
56 group.rules
57 ->Array.flatMap(r =>
58 r.premises
59 ->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second))
60 ->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
61 )
62 ->Set.fromArray
63 ->Set.remove(group.name)
64 ->Set.toArray,
65 )
66 groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
67 }
68
69 let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
70 let allVars =
71 mentionedGroups
72 ->Array.flatMap(g => g.rules)
73 ->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
74 let rec genVar = (base: string) => {
75 if allVars->Set.has(base) {
76 genVar(`${base}'`)
77 } else {
78 base
79 }
80 }
81 let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
82 let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
83 let vars = Array.concat(ps, [b, x, a])
84 let xIdx = vars->Array.findIndex(i => i == x)
85 let aIdx = vars->Array.findIndex(i => i == a)
86 let bIdx = vars->Array.findIndex(i => i == b)
87 let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => {
88 Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})])
89 }
90 let lookupGroup = (name: string): option<int> =>
91 mentionedGroups->Array.findIndexOpt(g => name == g.name)
92 let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
93 let baseIdx = baseIdx + Array.length(rule.vars)
94 let (s, name) = destructure(rule.conclusion)
95 let inductionHyps =
96 rule.premises
97 ->Array.filter(r =>
98 r.conclusion
99 ->destructureOpt
100 ->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup)
101 ->Option.isSome
102 )
103 ->Array.map(r => replaceJudgeRHS(r, baseIdx))
104 let pIdx = lookupGroup(name)->Option.getExn
105 {
106 vars: rule.vars,
107 premises: rule.premises->Array.concat(inductionHyps),
108 conclusion: structure(
109 Atom(surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringA.BaseAtom.wrap),
110 Var({idx: pIdx + baseIdx}),
111 ),
112 }
113 }
114 {
115 vars,
116 premises: Array.concat(
117 [
118 {
119 Rule.vars: [],
120 premises: [],
121 conclusion: structure(Var({idx: xIdx}), Atom(group.name->Symbolic.BaseAtom.wrap)),
122 },
123 ],
124 mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
125 ),
126 conclusion: structure(
127 Atom(surround([Var({idx: xIdx})], aIdx, bIdx)->StringA.BaseAtom.wrap),
128 Var({idx: 0}),
129 ), // TODO: clean here
130 }
131 }
132
133 let deserialise = (str: string, ~imports as _: Ports.t) => {
134 let getBase = (str: string) => {
135 let cur = ref(str)
136 let go = ref(true)
137 let results = Dict.make()
138 let ret = ref(Error("impossible"))
139 while go.contents {
140 switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
141 | Ok((t, n), rest) =>
142 if n->String.trim == "" {
143 go := false
144 ret := Error("Rule given with no name")
145 } else {
146 Dict.set(results, n, t)
147 if rest->String.trim == "" {
148 go := false
149 ret := Ok(results)
150 } else {
151 cur := rest
152 }
153 }
154 | Error(e) => {
155 go := false
156 ret := Error(e)
157 }
158 }
159 }
160 ret.contents
161 }
162 getBase(str)->Result.map(raw => {
163 let grouped: dict<array<Rule.t>> = Dict.make()
164 raw->Dict.forEach(rule =>
165 switch rule.conclusion->destructureOpt {
166 | Some((_, name)) =>
167 switch grouped->Dict.get(name) {
168 | None => grouped->Dict.set(name, [rule])
169 | Some(rs) => rs->Array.push(rule)
170 }
171 | _ => ()
172 }
173 )
174 let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
175 let derived: Dict.t<Rule.t> = Dict.make()
176 allGroups->Array.forEach(group => {
177 // NOTE: this can clash with other names. is this an issue?
178 derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
179 let mentionedGroups = findMentionedRuleGroups(group, allGroups)
180 if mentionedGroups->Array.length > 1 {
181 derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
182 }
183 })
184 ({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
185 })
186 }
187
188 let serialise = (state: state) => {
189 state.raw
190 ->Dict.toArray
191 ->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
192 ->Array.join("\n")
193 }
194
195 let make = props => {
196 let makeRules = content =>
197 <div
198 className={"axiom-set axiom-set-"->String.concat(
199 String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
200 )}
201 >
202 {content
203 ->Dict.toArray
204 ->Array.mapWithIndex(((n, r), i) =>
205 <RuleView
206 rule={r}
207 scope={[]}
208 key={String.make(i)}
209 style={props.imports.ruleStyle->Option.getOr(Hybrid)}
210 >
211 {React.string(n)}
212 </RuleView>
213 )
214 ->React.array}
215 </div>
216 <div>
217 {makeRules(props.content.raw)}
218 <p> {React.string("derived")} </p>
219 {makeRules(props.content.derived)}
220 </div>
221 }
222}