Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 5 additions & 18 deletions packages/frontend/src/App.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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";

Expand Down Expand Up @@ -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>;
}
Expand Down
225 changes: 135 additions & 90 deletions packages/frontend/src/analysis/analysis_editor.tsx
Original file line number Diff line number Diff line change
@@ -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,
Expand All @@ -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";
Expand All @@ -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.
Expand All @@ -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);

Expand Down Expand Up @@ -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
Expand All @@ -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>
</>
Expand All @@ -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(),
}),
};
}
6 changes: 6 additions & 0 deletions packages/frontend/src/analysis/context.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
import { createContext } from "solid-js";

import type { LiveAnalysisDocument } from "./document";

/** Context for a live analysis. */
export const LiveAnalysisContext = createContext<LiveAnalysisDocument>();
Loading