the next generation of the in-browser educational proof assistant
1open Signatures
2open Component
3open MethodView
4module Make = (
5 Term: TERM,
6 Judgment: JUDGMENT with module Term := Term,
7 JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
8 MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
9) => {
10 module Rule = Rule.Make(Term, Judgment)
11 module Proof = Proof.Make(Term, Judgment, MethodView.Method)
12 module Context = Method.Context(Term, Judgment)
13 module ProofView = ProofView.Make(Term, Judgment, JudgmentView, MethodView)
14 open RuleView
15 module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
16 module Ports = Ports(Term, Judgment)
17 type state = {
18 name: string,
19 rule: Rule.t,
20 proof: Proof.t,
21 gen: Term.gen,
22 substFailed: option<string>,
23 }
24 type props = {
25 content: state,
26 imports: Ports.t,
27 onChange: (state, ~exports: Ports.t=?) => unit,
28 }
29 let serialise = (state: state) => {
30 state.rule
31 ->Rule.prettyPrintTopLevel(~name=state.name)
32 ->String.concat("\n\n")
33 ->String.concat(Proof.prettyPrint(state.proof, ~scope=[]))
34 }
35 let deserialise = (str: string, ~imports: Ports.t) => {
36 let _facts = imports.facts
37 let gen = Term.makeGen()
38 let cur = ref(str)
39 switch Rule.parseTopLevel(cur.contents, ~scope=[], ~gen) {
40 | Error(e) => Error(e)
41 | Ok(((rule, name), s)) =>
42 switch Proof.parse(s, ~scope=[], ~gen) {
43 | Error(e) => Error(e)
44 | Ok((_, s')) if String.length(String.trim(s')) > 0 =>
45 Error("Trailing input: "->String.concat(s'))
46 | Ok((proof, _)) =>
47 Ok((
48 {name, rule, proof, gen, substFailed: None},
49 {Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None},
50 ))
51 }
52 }
53 }
54 let make = props => {
55 let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
56 let ctx: Context.t = {fixes: [], globalFacts: props.imports.facts, localFacts: Dict.make()}
57 let checked = Proof.check(ctx, props.content.proof, props.content.rule)
58 let sidebarRef = React.useRef(Nullable.null)
59 let proofChanged = (proof, subst) => {
60 let proof = Proof.uncheck(proof)->Proof.substitute(subst)
61 props.onChange(
62 try {
63 Proof.check(ctx, proof, props.content.rule)->ignore
64 {...props.content, proof, substFailed: None}
65 } catch {
66 | SExp.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
67 },
68 ~exports={
69 Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
70 ruleStyle: None,
71 },
72 )
73 }
74
75 <SidebarContext sidebarRef>
76 <h3> {React.string("Theorem")} </h3>
77 <RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
78 {React.string(props.content.name)}
79 </RuleView>
80 <h4> {React.string("Proof")} </h4>
81 <ProofView
82 ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged
83 />
84 {switch props.content.substFailed {
85 | Some(msg) => React.string(msg)
86 | None => React.null
87 }}
88 <div className="sidebar" ref={ReactDOM.Ref.domRef(sidebarRef)} />
89 </SidebarContext>
90 }
91}