the next generation of the in-browser educational proof assistant
1import * as ComponentGraph from "./componentgraph";
2import { AxiomS, ConfS, TheoremS, InductiveS, AxiomStr, TheoremStr } from "./Scratch.mjs";
3import ReactDOM from "react-dom/client";
4import React from "react";
5
6type Component = ComponentGraph.Component;
7
8//A bridge between any module that implements the COMPONENT signature from ReScript-land
9//and a ComponentGraph component.
10function HolComp(RComp : any) {
11 return class implements Component {
12 dependencyChanged : (id: string, comp: Component) => void;
13 deps : Record<string,Component>;
14 exports : Record<string,any>;
15 loaded: boolean;
16 root : ReactDOM.Root;
17 state: any;
18 toString() {
19 return RComp.serialise(this.state)
20 }
21 gatherImports() {
22 let ret = RComp.Ports.empty
23 for (const x in this.deps) {
24 if ("exports" in this.deps[x]) {
25 ret = RComp.Ports.combine(ret,this.deps[x]["exports"])
26 }
27 }
28 return ret
29 }
30 render(signal : (msg: any) => void) {
31 let Tag = RComp.make
32 this.root.render(
33 <Tag content={this.state} imports={this.gatherImports()}
34 onChange={ (state, exports) => {
35 if (exports) {
36 this.exports = exports
37 signal(null)
38 }
39 this.state = state;
40 this.render(signal)
41 }}
42 />
43 )
44 }
45 constructor(str: string,deps : Record<string,Component>, signal : (msg: any) => void, loaded : (msg: any) => void, view? : HTMLElement) {
46 this.deps = deps
47 this.loaded = false
48 if (view != null) {
49 const newDiv = document.createElement("div");
50 view.innerHTML = "";
51 view.appendChild(newDiv);
52 this.root = ReactDOM.createRoot(newDiv);
53 }
54 const imports = this.gatherImports();
55 var foo = RComp.deserialise(str,imports)
56 if (foo.TAG == "Ok") {
57 this.exports = foo._0[1]
58 this.state = foo._0[0]
59 this.dependencyChanged = (_depName, _comp) => {
60 this.render(signal)
61 };
62 loaded(null)
63 this.loaded = true;
64 this.render(signal)
65 } else {
66 view.innerHTML = foo._0
67 }
68 }
69 }
70
71}
72
73window.localStorage.clear()
74ComponentGraph.setup({
75 "hol-comp": HolComp(AxiomS),
76 "hol-inductive": HolComp(InductiveS),
77 "hol-config": HolComp(ConfS),
78 "hol-proof": HolComp(TheoremS),
79 "hol-string": HolComp(AxiomStr),
80 "hol-string-proof": HolComp(TheoremStr),
81}); //"hol-config": ConfigComponent, "hol-proof":ProofComponent});