Merge pull request #264 from ToposInstitute/diagram-analysis

Analyses for diagrams in models
ToposInstitute · Nov 19, 2024 · 40eaeab · 40eaeab
2 parents c646bbc + 20de659
commit 40eaeab
Show file tree

Hide file tree

Showing 19 changed files with 525 additions and 300 deletions.
diff --git a/packages/frontend/src/App.tsx b/packages/frontend/src/App.tsx
@@ -8,11 +8,10 @@ import * as uuid from "uuid";
 import { MultiProvider } from "@solid-primitives/context";
 import { Navigate, type RouteDefinition, type RouteSectionProps, Router } from "@solidjs/router";
 import { FirebaseProvider } from "solid-firebase";
-import { Show, createResource, lazy, useContext } from "solid-js";
+import { Show, createResource, lazy } from "solid-js";
 
-import type { JsonValue } from "catcolab-api";
-import { RepoContext, RpcContext, createRpcClient } from "./api";
-import { newModelDocument } from "./model/document";
+import { RepoContext, RpcContext, createRpcClient, useApi } from "./api";
+import { createModel } from "./model/document";
 import { HelpContainer, lazyMdx } from "./page/help_page";
 import { TheoryLibraryContext, stdTheories } from "./stdlib";
 
@@ -46,21 +45,9 @@ const Root = (props: RouteSectionProps<unknown>) => {
 };
 
 function CreateModel() {
-    const rpc = useContext(RpcContext);
-    invariant(rpc, "Missing context to create model");
+    const api = useApi();
 
-    const init = newModelDocument();
-
-    const [ref] = createResource<string>(async () => {
-        const result = await rpc.new_ref.mutate({
-            content: init as JsonValue,
-            permissions: {
-                anyone: "Read",
-            },
-        });
-        invariant(result.tag === "Ok", "Failed to create model");
-        return result.content;
-    });
+    const [ref] = createResource<string>(() => createModel(api));
 
     return <Show when={ref()}>{(ref) => <Navigate href={`/model/${ref()}`} />}</Show>;
 }

diff --git a/packages/frontend/src/analysis/analysis_editor.tsx b/packages/frontend/src/analysis/analysis_editor.tsx
@@ -1,12 +1,20 @@
 import Resizable, { type ContextValue } from "@corvu/resizable";
 import { useParams } from "@solidjs/router";
-import { Show, createEffect, createResource, createSignal, useContext } from "solid-js";
+import {
+    Match,
+    Show,
+    Switch,
+    createEffect,
+    createResource,
+    createSignal,
+    useContext,
+} from "solid-js";
 import { Dynamic } from "solid-js/web";
 import invariant from "tiny-invariant";
 
-import { RepoContext, RpcContext, getLiveDoc } from "../api";
+import { useApi } from "../api";
 import { IconButton, ResizableHandle } from "../components";
-import { LiveModelContext, type ModelDocument, enlivenModelDocument } from "../model";
+import { DiagramPane } from "../diagram/diagram_editor";
 import { ModelPane } from "../model/model_editor";
 import {
     type CellConstructor,
@@ -16,9 +24,15 @@ import {
 } from "../notebook";
 import { BrandedToolbar, HelpButton } from "../page";
 import { TheoryLibraryContext } from "../stdlib";
-import type { ModelAnalysisMeta } from "../theory";
-import type { AnalysisDocument, LiveAnalysisDocument } from "./document";
-import type { ModelAnalysis } from "./types";
+import type { AnalysisMeta } from "../theory";
+import { LiveAnalysisContext } from "./context";
+import {
+    type LiveAnalysisDocument,
+    type LiveDiagramAnalysisDocument,
+    type LiveModelAnalysisDocument,
+    getLiveAnalysis,
+} from "./document";
+import type { Analysis } from "./types";
 
 import PanelRight from "lucide-solid/icons/panel-right";
 import PanelRightClose from "lucide-solid/icons/panel-right-close";
@@ -28,87 +42,13 @@ export default function AnalysisPage() {
     const refId = params.ref;
     invariant(refId, "Must provide document ref as parameter to analysis page");
 
-    const rpc = useContext(RpcContext);
-    const repo = useContext(RepoContext);
+    const api = useApi();
     const theories = useContext(TheoryLibraryContext);
-    invariant(rpc && repo && theories, "Missing context for analysis page");
-
-    const [liveAnalysis] = createResource<LiveAnalysisDocument>(async () => {
-        const liveDoc = await getLiveDoc<AnalysisDocument>(rpc, repo, refId);
-        const { doc } = liveDoc;
-        invariant(doc.type === "analysis", () => `Expected analysis, got type: ${doc.type}`);
+    invariant(theories, "Must provide theory library as context to analysis page");
 
-        const liveModelDoc = await getLiveDoc<ModelDocument>(rpc, repo, doc.modelRef.refId);
-        const liveModel = enlivenModelDocument(doc.modelRef.refId, liveModelDoc, theories);
-
-        return { refId, liveDoc, liveModel };
-    });
+    const [liveAnalysis] = createResource(() => getLiveAnalysis(refId, api, theories));
 
-    return (
-        <Show when={liveAnalysis()}>
-            {(liveAnalysis) => <AnalysisDocumentEditor liveAnalysis={liveAnalysis()} />}
-        </Show>
-    );
-}
-
-/** Notebook editor for analyses of models of double theories.
- */
-export function AnalysisPane(props: {
-    liveAnalysis: LiveAnalysisDocument;
-}) {
-    const liveDoc = () => props.liveAnalysis.liveDoc;
-    return (
-        <LiveModelContext.Provider value={props.liveAnalysis.liveModel}>
-            <NotebookEditor
-                handle={liveDoc().docHandle}
-                path={["notebook"]}
-                notebook={liveDoc().doc.notebook}
-                changeNotebook={(f) => liveDoc().changeDoc((doc) => f(doc.notebook))}
-                formalCellEditor={ModelAnalysisCellEditor}
-                cellConstructors={modelAnalysisCellConstructors(
-                    props.liveAnalysis.liveModel.theory()?.modelAnalyses ?? [],
-                )}
-                noShortcuts={true}
-            />
-        </LiveModelContext.Provider>
-    );
-}
-
-function ModelAnalysisCellEditor(props: FormalCellEditorProps<ModelAnalysis>) {
-    const liveModel = useContext(LiveModelContext);
-    invariant(liveModel, "Live model should be provided as context for analysis");
-
-    return (
-        <Show when={liveModel.theory()?.modelAnalysis(props.content.id)}>
-            {(analysis) => (
-                <Dynamic
-                    component={analysis().component}
-                    liveModel={liveModel}
-                    content={props.content.content}
-                    changeContent={(f: (c: unknown) => void) =>
-                        props.changeContent((content) => f(content.content))
-                    }
-                />
-            )}
-        </Show>
-    );
-}
-
-function modelAnalysisCellConstructors(
-    analyses: ModelAnalysisMeta[],
-): CellConstructor<ModelAnalysis>[] {
-    return analyses.map((analysis) => {
-        const { id, name, description, initialContent } = analysis;
-        return {
-            name,
-            description,
-            construct: () =>
-                newFormalCell({
-                    id,
-                    content: initialContent(),
-                }),
-        };
-    });
+    return <AnalysisDocumentEditor liveAnalysis={liveAnalysis()} />;
 }
 
 /** Editor for a model of a double theory.
@@ -117,11 +57,8 @@ The editor includes a notebook for the model itself plus another pane for
 performing analysis of the model.
  */
 export function AnalysisDocumentEditor(props: {
-    liveAnalysis: LiveAnalysisDocument;
+    liveAnalysis?: LiveAnalysisDocument;
 }) {
-    const rpc = useContext(RpcContext);
-    invariant(rpc, "Must provide RPC context");
-
     const [resizableContext, setResizableContext] = createSignal<ContextValue>();
     const [isSidePanelOpen, setSidePanelOpen] = createSignal(true);
 
@@ -170,7 +107,7 @@ export function AnalysisDocumentEditor(props: {
                                     </Show>
                                 </IconButton>
                             </BrandedToolbar>
-                            <ModelPane liveModel={props.liveAnalysis.liveModel} />
+                            <AnalysisOfPane liveAnalysis={props.liveAnalysis} />
                         </Resizable.Panel>
                         <ResizableHandle hidden={!isSidePanelOpen()} />
                         <Resizable.Panel
@@ -184,7 +121,11 @@ export function AnalysisDocumentEditor(props: {
                         >
                             <div class="notebook-container">
                                 <h2>Analysis</h2>
-                                <AnalysisPane liveAnalysis={props.liveAnalysis} />
+                                <Show when={props.liveAnalysis}>
+                                    {(liveAnalysis) => (
+                                        <AnalysisNotebookEditor liveAnalysis={liveAnalysis()} />
+                                    )}
+                                </Show>
                             </div>
                         </Resizable.Panel>
                     </>
@@ -193,3 +134,107 @@ export function AnalysisDocumentEditor(props: {
         </Resizable>
     );
 }
+
+const AnalysisOfPane = (props: {
+    liveAnalysis?: LiveAnalysisDocument;
+}) => (
+    <Switch>
+        <Match when={props.liveAnalysis?.analysisType === "model" && props.liveAnalysis.liveModel}>
+            {(liveModel) => <ModelPane liveModel={liveModel()} />}
+        </Match>
+        <Match
+            when={props.liveAnalysis?.analysisType === "diagram" && props.liveAnalysis.liveDiagram}
+        >
+            {(liveDiagram) => <DiagramPane liveDiagram={liveDiagram()} />}
+        </Match>
+    </Switch>
+);
+
+/** Notebook editor for analyses of models of double theories.
+ */
+export function AnalysisNotebookEditor(props: {
+    liveAnalysis: LiveAnalysisDocument;
+}) {
+    const liveDoc = () => props.liveAnalysis.liveDoc;
+
+    const cellConstructors = () => {
+        let meta = undefined;
+        if (props.liveAnalysis.analysisType === "model") {
+            meta = props.liveAnalysis.liveModel.theory()?.modelAnalyses;
+        } else if (props.liveAnalysis.analysisType === "diagram") {
+            meta = props.liveAnalysis.liveDiagram.liveModel.theory()?.diagramAnalyses;
+        }
+        return (meta ?? []).map(analysisCellConstructor);
+    };
+
+    return (
+        <LiveAnalysisContext.Provider value={props.liveAnalysis}>
+            <NotebookEditor
+                handle={liveDoc().docHandle}
+                path={["notebook"]}
+                notebook={liveDoc().doc.notebook}
+                changeNotebook={(f) => liveDoc().changeDoc((doc) => f(doc.notebook))}
+                formalCellEditor={AnalysisCellEditor}
+                cellConstructors={cellConstructors()}
+                noShortcuts={true}
+            />
+        </LiveAnalysisContext.Provider>
+    );
+}
+
+function AnalysisCellEditor(props: FormalCellEditorProps<Analysis<unknown>>) {
+    const liveAnalysis = useContext(LiveAnalysisContext);
+    invariant(liveAnalysis, "Live analysis should be provided as context for cell editor");
+
+    return (
+        <Switch>
+            <Match
+                when={
+                    liveAnalysis.analysisType === "model" &&
+                    liveAnalysis.liveModel.theory()?.modelAnalysis(props.content.id)
+                }
+            >
+                {(analysis) => (
+                    <Dynamic
+                        component={analysis().component}
+                        liveModel={(liveAnalysis as LiveModelAnalysisDocument).liveModel}
+                        content={props.content.content}
+                        changeContent={(f: (c: unknown) => void) =>
+                            props.changeContent((content) => f(content.content))
+                        }
+                    />
+                )}
+            </Match>
+            <Match
+                when={
+                    liveAnalysis.analysisType === "diagram" &&
+                    liveAnalysis.liveDiagram.liveModel.theory()?.diagramAnalysis(props.content.id)
+                }
+            >
+                {(analysis) => (
+                    <Dynamic
+                        component={analysis().component}
+                        liveDiagram={(liveAnalysis as LiveDiagramAnalysisDocument).liveDiagram}
+                        content={props.content.content}
+                        changeContent={(f: (c: unknown) => void) =>
+                            props.changeContent((content) => f(content.content))
+                        }
+                    />
+                )}
+            </Match>
+        </Switch>
+    );
+}
+
+function analysisCellConstructor<T>(meta: AnalysisMeta<T>): CellConstructor<Analysis<T>> {
+    const { id, name, description, initialContent } = meta;
+    return {
+        name,
+        description,
+        construct: () =>
+            newFormalCell({
+                id,
+                content: initialContent(),
+            }),
+    };
+}
diff --git a/packages/frontend/src/analysis/context.ts b/packages/frontend/src/analysis/context.ts
@@ -0,0 +1,6 @@
+import { createContext } from "solid-js";
+
+import type { LiveAnalysisDocument } from "./document";
+
+/** Context for a live analysis. */
+export const LiveAnalysisContext = createContext<LiveAnalysisDocument>();