diff --git a/packages/catlog-wasm/src/model_diagram.rs b/packages/catlog-wasm/src/model_diagram.rs index d0b0b7b97..00cd1300b 100644 --- a/packages/catlog-wasm/src/model_diagram.rs +++ b/packages/catlog-wasm/src/model_diagram.rs @@ -1,11 +1,15 @@ //! Wasm bindings for diagrams in models of a double theory. +use std::collections::HashMap; use std::rc::Rc; use all_the_same::all_the_same; +use catlog::tt; +use catlog::tt::toplevel::Toplevel; use derive_more::From; use serde::{Deserialize, Serialize}; use tsify::Tsify; +use ustr::ustr; use wasm_bindgen::prelude::*; use catcolab_document_types::current::*; @@ -22,7 +26,7 @@ use super::result::JsResult; use super::theory::{DblTheory, DblTheoryBox}; /// A box containing a diagram in a model of a double theory. -#[derive(From)] +#[derive(From, Clone)] pub enum DblModelDiagramBox { /// A diagram in a model of a discrete double theory. Discrete(diagram::DblModelDiagram), @@ -30,6 +34,7 @@ pub enum DblModelDiagramBox { } /// Wasm binding for a diagram in a model of a double theory. +#[derive(Clone)] #[wasm_bindgen] pub struct DblModelDiagram { /// The boxed underlying diagram. @@ -279,6 +284,63 @@ pub struct ModelDiagramValidationResult( pub JsResult<(), Vec>, ); +/// A named collection of diagrams of double models. +#[wasm_bindgen] +pub struct DblDiagramMap { + #[wasm_bindgen(skip)] + diagrams: HashMap, + #[wasm_bindgen(skip)] + toplevel: Toplevel, +} + +impl Default for DblDiagramMap { + fn default() -> Self { + Self::new() + } +} + +#[wasm_bindgen] +impl DblDiagramMap { + /// Constructs an empty collection of models. + #[wasm_bindgen(constructor)] + pub fn new() -> Self { + DblDiagramMap { + diagrams: HashMap::new(), + toplevel: Toplevel::new(tt::theory::std_theories()), + } + } + + /// Returns whether the collection contains a model with the given name. + #[wasm_bindgen(js_name = "has")] + pub fn contains_key(&self, id: &str) -> bool { + self.diagrams.contains_key(id) + } + + /// Inserts a model with the given name. + #[wasm_bindgen(js_name = "set")] + pub fn insert(&mut self, id: String, diagram: &DblModelDiagram) { + // let id_ustr = ustr(&id); + self.diagrams.insert(id, diagram.clone()); + // let DblModelDiagramBox::Discrete(diagram::DblModelDiagram(_, model)) = diagram.diagram + // else { + // panic!() + // }; + // if let Some((ty_s, ty_v)) = &model.ty { + // let Some(theory) = model.theory().try_into_tt() else { + // return; + // }; + // self.toplevel.declarations.insert( + // NameSegment::Text(id_ustr), + // TopDecl::Type(Type::new( + // tt::theory::Theory::new(ustr("_").into(), theory), + // ty_s.clone(), + // ty_v.clone(), + // )), + // ); + // } + } +} + /// Elaborates a diagram defined by a notebook into a catlog diagram. #[wasm_bindgen(js_name = "elaborateDiagram")] pub fn elaborate_diagram( @@ -290,6 +352,7 @@ pub fn elaborate_diagram( match judgment { DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?, DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?, + DiagramJudgment::Instantiation(_) => return Err("Instantiation not supported".into()), DiagramJudgment::Equation(_) => { return Err("Elaboration of equations in diagrams is not yet supported".into()); } diff --git a/packages/catlog-wasm/src/theories.rs b/packages/catlog-wasm/src/theories.rs index f01b6c7a1..72386e4f7 100644 --- a/packages/catlog-wasm/src/theories.rs +++ b/packages/catlog-wasm/src/theories.rs @@ -534,6 +534,23 @@ impl ThPowerSystem { } } +/// A theory of the DEC +#[wasm_bindgen] +pub struct ThDEC(Rc>); + +#[wasm_bindgen] +impl ThDEC { + #[wasm_bindgen(constructor)] + pub fn new() -> Self { + Self(Rc::new(theories::th_multicategory())) // TODO symmetric? + } + + #[wasm_bindgen] + pub fn theory(&self) -> DblTheory { + DblTheory(self.0.clone().into()) + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/packages/catlog-wasm/src/theory.rs b/packages/catlog-wasm/src/theory.rs index ba3ac2692..4c626f736 100644 --- a/packages/catlog-wasm/src/theory.rs +++ b/packages/catlog-wasm/src/theory.rs @@ -324,6 +324,14 @@ impl DblTheory { } }) } + + /// Does the theory support elaboriating diagrams? + /// + /// Eventually diagrams will be replaced by instances. + #[wasm_bindgen(js_name = "canElaborateDiagrams")] + pub fn can_elaborate_diagrams(&self) -> bool { + matches!(&self.0, DblTheoryBox::Discrete(_)) + } } /// Mapping from object types to numerical indices. diff --git a/packages/document-methods/src/diagram.ts b/packages/document-methods/src/diagram.ts index 7769eee44..faacba636 100644 --- a/packages/document-methods/src/diagram.ts +++ b/packages/document-methods/src/diagram.ts @@ -53,6 +53,18 @@ export const newDiagramMorphismDecl = ( cod: null, }); +/** Create a new instantiation of an existing model. */ +export const newInstantiatedDiagram = ( + diagram?: Link | null, +): DiagramJudgment & { tag: "instantiation" } => ({ + tag: "instantiation", + id: v7(), + name: "", + diagram: diagram ?? null, + specializations: [], +}); + + /** Duplicate a diagram judgment, creating a fresh UUID. */ export const duplicateDiagramJudgment = (jgmt: DiagramJudgment): DiagramJudgment => ({ ...structuredClone(jgmt), diff --git a/packages/document-types/src/v0/diagram_judgment.rs b/packages/document-types/src/v0/diagram_judgment.rs index dc15d04f9..107fa6cee 100644 --- a/packages/document-types/src/v0/diagram_judgment.rs +++ b/packages/document-types/src/v0/diagram_judgment.rs @@ -2,6 +2,8 @@ use serde::{Deserialize, Serialize}; use tsify::Tsify; use uuid::Uuid; +use crate::v1::Link; + use super::model::{Mor, Ob}; use super::theory::{MorType, ObType}; @@ -80,4 +82,36 @@ pub enum DiagramJudgment { /// Declares an equation between morphisms in the diagram. #[serde(rename = "equation")] Equation(DiagramEqnDecl), + + /// Declares an instantiated diagram + #[serde(rename = "instantiation")] + Instantiation(InstantiatedDiagram), +} + +/// Instantiates an existing diagram into the current diagram +#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] +pub struct InstantiatedDiagram { + /// Human-readable label for the instantiation. + pub name: String, + + /// Globally unique identifier of the instantiation. + pub id: Uuid, + + /// Link to the diagram to instantiate. + pub diagram: Option, + + /// List of specializations to perform on the instantiated diagram. + pub specializations: Vec, +} + +/// A specialization of a generating object in an instantiated diagram. +#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] +pub struct SpecializeDiagram { + /// ID (qualified name) of generating object to specialize. + pub id: Option, + + /// Object to insert as the specialization. + pub ob: Option, } diff --git a/packages/frontend/src/App.tsx b/packages/frontend/src/App.tsx index df312edd4..6012062b4 100644 --- a/packages/frontend/src/App.tsx +++ b/packages/frontend/src/App.tsx @@ -11,6 +11,7 @@ import * as uuid from "uuid"; import { Button } from "catcolab-ui-components"; import { Api, ApiContext, useApi } from "./api"; +import { createDiagramLibraryWithApi, DiagramLibraryContext } from "./diagram"; import { helpRoutes } from "./help/routes"; import { createModelLibraryWithApi, ModelLibraryContext } from "./model"; import { createModel } from "./model/document"; @@ -43,6 +44,7 @@ const Root = (props: RouteSectionProps) => { const theories = stdTheories; const models = createModelLibraryWithApi(api, theories); + const diagrams = createDiagramLibraryWithApi(api, theories); return ( @@ -51,6 +53,7 @@ const Root = (props: RouteSectionProps) => { [ApiContext, api], [TheoryLibraryContext, theories], [ModelLibraryContext, models], + [DiagramLibraryContext, diagrams], UserStateProvider, ]} > diff --git a/packages/frontend/src/components/id_input.tsx b/packages/frontend/src/components/id_input.tsx index 5ffb66c0d..3c07562e3 100644 --- a/packages/frontend/src/components/id_input.tsx +++ b/packages/frontend/src/components/id_input.tsx @@ -113,7 +113,7 @@ export function IdInput( const isComplete = () => { const name = props.id ? idToText(props.id) : ""; - return text() === name; + return name === "" || text() === name; }; const status = (): InlineInputErrorStatus => { @@ -126,7 +126,12 @@ export function IdInput( return null; }; - const setNewId = () => props.generateId && props.setId(props.generateId()); + const setNewId = () => { + if (props.generateId) { + const newId = props.generateId(); + props.setId(newId); + } + }; const labelType = (id: Uuid | null): "named" | "anonymous" | "undefined" => { if (id == null) { diff --git a/packages/frontend/src/components/index.ts b/packages/frontend/src/components/index.ts index bfd3e3164..512883926 100644 --- a/packages/frontend/src/components/index.ts +++ b/packages/frontend/src/components/index.ts @@ -3,3 +3,4 @@ export * from "./document_picker"; export * from "./id_input"; export * from "./json_import"; export * from "./rich_text_editor"; +export * from "./instantiation_cell_editor.tsx"; diff --git a/packages/frontend/src/model/instantiation_cell_editor.css b/packages/frontend/src/components/instantiation_cell_editor.css similarity index 100% rename from packages/frontend/src/model/instantiation_cell_editor.css rename to packages/frontend/src/components/instantiation_cell_editor.css diff --git a/packages/frontend/src/model/instantiation_cell_editor.tsx b/packages/frontend/src/components/instantiation_cell_editor.tsx similarity index 64% rename from packages/frontend/src/model/instantiation_cell_editor.tsx rename to packages/frontend/src/components/instantiation_cell_editor.tsx index 09f4c1916..559af2ac1 100644 --- a/packages/frontend/src/model/instantiation_cell_editor.tsx +++ b/packages/frontend/src/components/instantiation_cell_editor.tsx @@ -1,75 +1,46 @@ import type { DocInfo } from "catcolab-api/src/user_state"; +import type { Accessor } from "solid-js"; import { batch, createEffect, Index, Show, splitProps, untrack, useContext } from "solid-js"; import invariant from "tiny-invariant"; +import { Nb } from "catcolab-document-methods"; import { type FocusHandle, NameInput, type TextInputOptions, useChildFocus, } from "catcolab-ui-components"; -import type { DblModel, InstantiatedModel, Ob, SpecializeModel } from "catlog-wasm"; -import { useApi } from "../api"; -import { DocumentPicker, IdInput, IdInputPlaceholder } from "../components"; +import type { Ob, DblModel } from "catlog-wasm"; import type { CellActions } from "../notebook"; -import { DocRefIdContext } from "../page/context"; -import { useUserState } from "../user/user_state_context"; -import { LiveModelContext, ModelLibraryContext } from "./context"; +import { IdInput, IdInputPlaceholder } from "./id_input.tsx"; +import { DocumentPicker } from "./document_picker.tsx"; import { ObInput } from "./object_input"; import "./instantiation_cell_editor.css"; -/** Editor for an instantiation cell in a model */ -export function InstantiationCellEditor(props: { - instantiation: InstantiatedModel; - modifyInstantiation: (f: (inst: InstantiatedModel) => void) => void; - focus: FocusHandle; - actions: CellActions; -}) { - const api = useApi(); - const docRefId = useContext(DocRefIdContext); - const liveModel = useContext(LiveModelContext); - const userState = useUserState(); +export type Specialization = { id: string | null; ob: Ob | null }; - const filterCompletions = (refId: string, doc: DocInfo) => { - if (doc.typeName !== "model") { - return false; - } - if (docRefId && refId === docRefId()) { - return false; - } - const theory = liveModel?.().liveDoc.doc.theory; - if (theory && doc.theory !== theory) { - return false; - } - return true; - }; - - const refId = () => props.instantiation.model?._id; - const setRefId = (refId: string | null) => { - props.modifyInstantiation((inst) => { - inst.model = refId ? api.makeUnversionedLink(refId, "instantiation") : null; - // Auto-fill the name from the selected model's title when unnamed. - if (refId && !inst.name) { - const docName = userState.documents[refId]?.name; - if (docName) { - inst.name = docName; - } - } - }); - }; - - const models = useContext(ModelLibraryContext); - invariant(models); - const instantiated = models.useElaboratedModel(refId); +export interface InstantiatedSomething { + name: string; + specializations: Specialization[]; +} +export function InstantiationCellEditor( + props: { + instantiation: InstantiatedSomething; + modifyInstantiation: (f: (inst: InstantiatedSomething) => void) => void; + pickerConfig: PickerConfig; + specializationConfig: InstantiationConfig; + } & CellEditorProps, +) { // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted cell. const focus = useChildFocus(props.focus, { - default: refId() == null ? "model" : "name", + default: props.config.refId() == null ? props.config.kind : "name", }); const specializationFocus = useChildFocus(focus.childFocus("specializations"), { default: 0, }); + const activateIndex = (index: number) => batch(() => { focus.setActiveChild("specializations"); @@ -103,7 +74,10 @@ export function InstantiationCellEditor(props: { * kept so the user can correct them. */ const pruneEmptySpecializations = () => { - const specs = props.instantiation.specializations; + const specs = props.instantiation?.specializations; + if (specs == undefined) { + return; + } // Collect indices of empty rows in increasing order. const removedIndices: number[] = []; for (let i = 0; i < specs.length; i++) { @@ -151,18 +125,19 @@ export function InstantiationCellEditor(props: { }); const exitDownFromTop = () => { - if (props.instantiation.specializations.length === 0) { + if (props.instantiation?.specializations.length === 0) { props.actions.activateBelow(); } else { activateIndex(0); } }; + // In diagrams, there are instantiatedJudgments, obJudgments, obGenerators, etc. return (
-
+
props.modifyInstantiation((inst) => { inst.name = name; @@ -174,42 +149,42 @@ export function InstantiationCellEditor(props: { deleteForward={props.actions.deleteForward} exitUp={props.actions.activateAbove} exitDown={exitDownFromTop} - exitRight={() => focus.setActiveChild("model")} - exitForward={() => focus.setActiveChild("model")} + exitRight={() => focus.setActiveChild(props.config.kind)} + exitForward={() => focus.setActiveChild(props.config.kind)} focus={focus.childFocus("name")} /> { - setRefId(newRefId); - // After picking a model, move focus out of the picker + props.config.setRefId(newRefId); + // After picking a something, move focus out of the picker // and into the specializations area so the user can // keep going on the keyboard. If there are no rows // yet, add an empty one to focus. if (newRefId) { - if (props.instantiation.specializations.length === 0) { + if (props.instantiation?.specializations.length === 0) { insertSpecializationAtTop(); } else { activateIndex(0); } } }} - filterCompletions={filterCompletions} + filterCompletions={props.config.filterCompletions} placeholder="..." deleteBackward={() => focus.setActiveChild("name")} exitUp={props.actions.activateAbove} exitDown={exitDownFromTop} exitLeft={() => focus.setActiveChild("name")} exitBackward={() => focus.setActiveChild("name")} - focus={focus.childFocus("model")} + focus={focus.childFocus(props.config.kind)} />
    - + {(spec, i) => (
  • idInputTexts.set(i, text)} - instantiatedModel={instantiated()?.validatedModel.model ?? null} + instantiated={props.instantiated} focus={specializationFocus.childFocus(i)} createBelow={() => { props.modifyInstantiation((inst) => { @@ -251,16 +226,16 @@ export function InstantiationCellEditor(props: {
    • )}     - +
  • { appendSpecialization(); props.focus.setFocused(true); evt.preventDefault(); }} > -
    +
    @@ -272,15 +247,72 @@ export function InstantiationCellEditor(props: { ); } -type InstantiationCellComponent = "name" | "model" | "specializations"; +type InstantiationCellComponent = "name" | string | "specializations"; + +export interface ObLookup { + hasOb(ob: Ob): boolean; + obGenerators(): QualifiedName[]; + obGeneratorLabel(id: QualifiedName): QualifiedLabel | undefined; + obGeneratorWithLabel(label: QualifiedLabel): NameLookup; + obType(ob: Ob): ObType; +} + +export interface PickerConfig { + kind: string; + refId(): string | undefined; + setRefId(refId: string | null): void; + filterCompletions(refId: string, doc: DocInfo): boolean; + hasInstantiated: Accessor; +} + +export interface SpecConfig { + completions: Accessor; + idToLavel(id: QualifiedName): Qua +} + +export interface InstantiationConfig { + kind: string; + refId(): string | undefined; + setRefId(refId: string | null): void; + filterCompletions(refId: string, doc: DocInfo): boolean; + /** Whether an instantiated doc has been resolved — drives the CSS class and add-row */ + hasInstantiated: Accessor; + + // Id-side completions for specialization rows + completions: Accessor; + idToLabel(id: QualifiedName): QualifiedLabel | undefined; + labelToId(label: QualifiedLabel): NameLookup | undefined; + + // Ob-side render prop + obSide( + props: { + specialization: { id: string | null; ob: Ob | null }; + modifySpecialization: (f: (spec: { id: string | null; ob: Ob | null }) => void) => void; + focus: FocusHandle; + } & Pick, + ): JSX.Element; +} function SpecializationEditor( allProps: { - specialization: SpecializeModel; - modifySpecialization: (f: (spec: SpecializeModel) => void) => void; - instantiatedModel: DblModel | null; - /** Called when the displayed text of the id input changes. */ + specialization: { id: string | null; ob: Ob | null }; + modifySpecialization: (f: (spec: { id: string | null; ob: Ob | null }) => void) => void; + completions?: QualifiedName[]; + idToLabel: (id: QualifiedName) => QualifiedLabel | undefined; + labelToId: (label: QualifiedLabel) => NameLookup | undefined; onIdTextChange?: (text: string) => void; + obSide: ( + props: { + specialization: { id: string | null; ob: Ob | null }; + modifySpecialization: ( + f: (spec: { id: string | null; ob: Ob | null }) => void, + ) => void; + focus: FocusHandle; + deleteBackward: () => void; + exitBackward: () => void; + exitLeft: () => void; + } & Pick, + ) => JSX.Element; focus: FocusHandle; } & Pick, ) { @@ -289,18 +321,8 @@ function SpecializationEditor( // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted row. const focus = useChildFocus(props.focus, { default: "id" }); - const obType = () => { - const id = props.specialization.id; - if (id) { - const ob: Ob = { tag: "Basic", content: id }; - if (props.instantiatedModel?.hasOb(ob)) { - return props.instantiatedModel.obType(ob); - } - } - }; - return ( -
    +
    props.instantiatedModel?.obGeneratorLabel(id)} - labelToId={(label) => props.instantiatedModel?.obGeneratorWithLabel(label)} + completions={props.completions} + idToLabel={props.idToLabel} + labelToId={props.labelToId} focus={focus.childFocus("id")} deleteBackward={props.deleteBackward} exitForward={() => focus.setActiveChild("ob")} @@ -320,25 +342,15 @@ function SpecializationEditor( {...inputProps} /> - }> - {(obType) => ( - { - props.modifySpecialization((spec) => { - spec.ob = ob; - }); - }} - obType={obType()} - focus={focus.childFocus("ob")} - deleteBackward={() => focus.setActiveChild("id")} - exitBackward={() => focus.setActiveChild("id")} - exitLeft={() => focus.setActiveChild("id")} - {...inputProps} - /> - )} - + {props.obSide({ + specialization: props.specialization, + modifySpecialization: props.modifySpecialization, + focus: focus.childFocus("ob"), + deleteBackward: () => focus.setActiveChild("id"), + exitBackward: () => focus.setActiveChild("id"), + exitLeft: () => focus.setActiveChild("id"), + ...inputProps, + })}
    ); } diff --git a/packages/frontend/src/diagram/context.ts b/packages/frontend/src/diagram/context.ts index c13ea9cb6..13e21373b 100644 --- a/packages/frontend/src/diagram/context.ts +++ b/packages/frontend/src/diagram/context.ts @@ -1,6 +1,10 @@ import { type Accessor, createContext } from "solid-js"; +import type { DiagramLibrary } from "./diagram_library"; import type { LiveDiagramDoc } from "./document"; +/** Context for a library of diagrams. */ +export const DiagramLibraryContext = createContext>(); + /** Context for a live diagram in a model. */ export const LiveDiagramContext = createContext>(); diff --git a/packages/frontend/src/diagram/diagram_editor.tsx b/packages/frontend/src/diagram/diagram_editor.tsx index 12e3e93ab..a58a50dc4 100644 --- a/packages/frontend/src/diagram/diagram_editor.tsx +++ b/packages/frontend/src/diagram/diagram_editor.tsx @@ -10,6 +10,7 @@ import { type CellConstructor, type FormalCellEditorProps, NotebookEditor } from import type { InstanceTypeMeta } from "../theory"; import { LiveDiagramContext } from "./context"; import type { LiveDiagramDoc } from "./document"; +import { DiagramInstantiationCellEditor } from "./diagram_instantiation_cell_editor"; import { DiagramMorphismCellEditor } from "./morphism_cell_editor"; import { DiagramObjectCellEditor } from "./object_cell_editor"; @@ -19,8 +20,10 @@ export function DiagramNotebookEditor(props: { liveDiagram: LiveDiagramDoc; focu const liveDoc = () => props.liveDiagram.liveDoc; const liveModel = () => props.liveDiagram.liveModel; - const cellConstructors = () => - (liveModel().theory()?.instanceTypes ?? []).map(diagramCellConstructor); + const cellConstructors = () => { + const theory = liveModel().theory(); + return theory ? diagramCellConstructors(theory) : []; + }; return ( ) { /> )} + + + props.changeContent((c) => f(c as InstantiatedDiagram))} + focus={props.focus} + actions={props.actions} + /> + + {" "} ); } +function diagramCellConstructors(theory: Theory): CellConstructor[] { + const constructors: CellConstructor[] = []; + constructors.push({ + name: "Instantiate", + description: "Instantiate an existing model into this one", + shortcut: ["I"], + construct() { + return Nb.newFormalCell(Diagram.newInstantiatedDiagram()); + }, + }); + for (const meta of theory.instanceTypes ?? []) { + constructors.push(diagramCellConstructor(meta)); + } + return constructors; +} + function diagramCellConstructor(meta: InstanceTypeMeta): CellConstructor { const { tag, name, description, shortcut } = meta; return { @@ -113,6 +142,8 @@ function judgmentLabel(judgment: DiagramJudgment): string | undefined { return theory?.instanceObTypeMeta(judgment.obType)?.name; case "morphism": return theory?.instanceMorTypeMeta(judgment.morType)?.name; + case "instantiation": + return theory?.name; case "equation": return "Equation"; default: diff --git a/packages/frontend/src/diagram/diagram_instantiation_cell_editor.css b/packages/frontend/src/diagram/diagram_instantiation_cell_editor.css new file mode 100644 index 000000000..e1c30e71d --- /dev/null +++ b/packages/frontend/src/diagram/diagram_instantiation_cell_editor.css @@ -0,0 +1,105 @@ +.model-instantiation-decl { + display: flex; + flex-direction: row; + gap: 1ex; + align-items: baseline; + + & .is-a:before { + content: ":"; + } +} + +.model-specializations { + --add-specialization-height: 1.5em; + + /* Use a grid so the arrow column is always at the same x position across + all rows, regardless of what is rendered on the left or right side. */ + display: grid; + grid-template-columns: max-content max-content 1fr; + align-items: baseline; + column-gap: 1ex; + row-gap: 0; + + position: relative; + list-style: none; + + margin-left: 0.5rem; + padding-left: 1rem; + transition: padding-bottom 0.15s; + + &.has-instantiated { + padding-bottom: var(--add-specialization-height); + } + + &:before { + content: ""; + position: absolute; + left: 0; + top: 0; + bottom: 0; + width: 2px; + background: var(--color-gray-450); + transition: bottom 0.15s; + } + + &.has-instantiated:before { + bottom: var(--add-specialization-height); + } + + /* Each row spans all three grid columns by becoming a subgrid. */ + & > li { + display: grid; + grid-template-columns: subgrid; + grid-column: 1 / -1; + align-items: baseline; + } +} + +.model-specialization { + display: grid; + grid-template-columns: subgrid; + grid-column: 1 / -1; + align-items: baseline; + + & .specialize-as:before { + content: "⟵"; + } + + /* Mark the left-hand side as a sub-object with a leading dot. The left + cell is the first grid item in every row (left, arrow, right). */ + & > :nth-child(1):before { + content: "."; + margin-right: -0.4ex; + } +} + +.model-specialization-add { + cursor: pointer; + height: 0; + overflow: hidden; + pointer-events: none; + opacity: 0; + transition: + opacity 0.15s, + height 0.15s; +} + +.formal-judgment:hover .model-specializations.has-instantiated, +.formal-judgment:focus-within .model-specializations.has-instantiated { + padding-bottom: 0; + + &:before { + bottom: 0; + } +} + +.formal-judgment:hover .model-specializations.has-instantiated .model-specialization-add, +.formal-judgment:focus-within .model-specializations.has-instantiated .model-specialization-add { + opacity: 0.5; + height: var(--add-specialization-height); + pointer-events: auto; + + &:hover { + opacity: 0.85; + } +} diff --git a/packages/frontend/src/diagram/diagram_instantiation_cell_editor.tsx b/packages/frontend/src/diagram/diagram_instantiation_cell_editor.tsx new file mode 100644 index 000000000..0b282d9e0 --- /dev/null +++ b/packages/frontend/src/diagram/diagram_instantiation_cell_editor.tsx @@ -0,0 +1,137 @@ +import { useContext } from "solid-js"; +import invariant from "tiny-invariant"; + +import { Nb } from "catcolab-document-methods"; +import type { InstantiatedDiagram, DiagramJudgment } from "catcolab-document-types"; +import { type FocusHandle } from "catcolab-ui-components"; +import type { Ob } from "catlog-wasm"; +import { useApi } from "../api"; +import { IdInput, InstantiationCellEditor, type InstantiationConfig } from "../components"; +import type { CellActions } from "../notebook"; +import { DocRefIdContext } from "../page/context"; +import { useUserState } from "../user/user_state_context"; +import { LiveDiagramContext, DiagramLibraryContext } from "./context"; + +export function DiagramInstantiationCellEditor(props: { + instantiation: InstantiatedDiagram; + changeContent: (f: (content: InstantiatedDiagram) => void) => void; + focus: FocusHandle; + actions: CellActions; +}) { + const api = useApi(); + const docRefId = useContext(DocRefIdContext); + const liveDiagram = useContext(LiveDiagramContext); + const userState = useUserState(); + const diagrams = useContext(DiagramLibraryContext); + invariant(diagrams); + + const refId = () => props.instantiation.diagram?._id; + const instantiated = diagrams.useLiveDiagram(refId); + + // --- completions from the instantiated diagram's judgments --- + const instantiatedJudgments = (): DiagramJudgment[] => { + const live = instantiated(); + if (!live) return []; + return Nb.getFormalContent(live.liveDoc.doc.notebook); + }; + + const obJudgments = () => instantiatedJudgments().filter((j) => j.tag === "object"); + + // --- completions from the current diagram's judgments --- + const currentJudgments = (): DiagramJudgment[] => { + const live = liveDiagram?.(); + if (!live) return []; + return Nb.getFormalContent(live.liveDoc.doc.notebook); + }; + + const currentObJudgments = () => currentJudgments().filter((j) => j.tag === "object"); + const currentObGenerators = () => currentObJudgments().map((j) => j.id); + + const currentObIdToLabel = (id: string): string[] | undefined => { + const j = currentObJudgments().find((j) => j.id === id); + return j?.name ? [j.name] : undefined; + }; + + const currentObLabelToId = (label: string[]) => { + const name = label[0]; + const matches = currentObJudgments().filter((j) => j.name === name); + if (matches.length === 1) return { tag: "Unique" as const, content: matches[0].id }; + if (matches.length > 1) return { tag: "Ambiguous" as const }; + return { tag: "None" as const }; + }; + + const config: InstantiationConfig = { + kind: "diagram", + + refId, + + setRefId(id) { + props.changeContent((inst) => { + inst.diagram = id ? api.makeUnversionedLink(id, "instantiation") : null; + if (id && !inst.name) { + const docName = userState.documents[id]?.name; + if (docName) inst.name = docName; + } + }); + }, + + filterCompletions(refId, doc) { + if (doc.typeName !== "diagram") return false; + if (docRefId && refId === docRefId()) return false; + const theory = liveDiagram?.().liveDoc.doc.theory; + if (theory && doc.theory !== theory) return false; + return true; + }, + + hasInstantiated: () => instantiated() != null, + + // id-side: from the instantiated diagram's judgments + completions: () => obJudgments().map((j) => j.id), + idToLabel(id) { + const j = obJudgments().find((j) => j.id === id); + return j?.name ? [j.name] : undefined; + }, + labelToId(label) { + const name = label[0]; + const matches = obJudgments().filter((j) => j.name === name); + if (matches.length === 1) return { tag: "Unique" as const, content: matches[0].id }; + if (matches.length > 1) return { tag: "Ambiguous" as const }; + return { tag: "None" as const }; + }, + + // this should be + obSide(p) { + return ( + { + p.modifySpecialization((spec) => { + spec.ob = id ? { tag: "Basic", content: id } : null; + }); + }} + completions={currentObGenerators()} + idToLabel={currentObIdToLabel} + labelToId={currentObLabelToId} + focus={p.focus} + deleteBackward={p.deleteBackward} + exitBackward={p.exitBackward} + exitLeft={p.exitLeft} + createBelow={p.createBelow} + exitDown={p.exitDown} + exitUp={p.exitUp} + /> + ); + }, + }; + + return ( + props.changeContent((content) => f(content as InstantiatedDiagram))} + config={config} + focus={props.focus} + actions={props.actions} + /> + ); +} diff --git a/packages/frontend/src/diagram/diagram_library.tsx b/packages/frontend/src/diagram/diagram_library.tsx new file mode 100644 index 000000000..75f4bc309 --- /dev/null +++ b/packages/frontend/src/diagram/diagram_library.tsx @@ -0,0 +1,361 @@ +import { + type AnyDocumentId, + type DocHandle, + type DocHandleChangePayload, + interpretAsDocumentId, + type Patch, + type Repo, +} from "@automerge/automerge-repo"; +import { ReactiveMap } from "@solid-primitives/map"; +import { type Accessor, createResource, onCleanup } from "solid-js"; +import invariant from "tiny-invariant"; +import * as uuid from "uuid"; + +import { Nb, type DiagramDocument } from "catcolab-document-methods"; +import { + type DblDiagram, + DblDiagramMap, + type DblTheory, + type Document, + elaborateDiagram, + type DiagramNotebook, + type DiagramValidationResult, + type Uuid, +} from "catlog-wasm"; +import { type Api, findAndMigrate, type LiveDoc, makeLiveDoc } from "../api"; +import type { Theory, TheoryLibrary } from "../theory"; +import type { LiveDiagramDoc } from "./document"; + +/** An elaborated diagram along with its validation status. */ +export type ValidatedDiagram = + /** A successfully elaborated and validated diagram. */ + | { + tag: "Valid"; + diagram: DblDiagram; + } + /** An elaborated diagram with one or more validation errors. */ + | { + tag: "Invalid"; + diagram: DblDiagram; + errors: (DiagramValidationResult & { tag: "Err" })["content"]; + } + /** A diagram that failed to even elaborate. */ + | { + tag: "Illformed"; + diagram: null; + error: string; + }; + +/** An entry in a `DiagramLibrary`. */ +export type DiagramEntry = { + /** The double theory that the diagram is a diagram of. */ + theory: Theory; + + /** The elaborated and validated diagram. */ + validatedDiagram: ValidatedDiagram; + + /** Generation number, incremented each time the diagram is elaborated. + + Mainly intended for debugging and testing purposes. + */ + generation: number; +}; + +type DiagramLibraryParameters = { + canonicalize: (refId: RefId) => DiagramKey; + fetch: (refId: RefId) => Promise>; + theories: TheoryLibrary; +}; + +type DiagramKey = string & { __diagramLibraryKey: true }; + +type DocHandleWithDestructor = { + docHandle: DocHandle; + destroy: () => void; +}; + +/** Create a `DiagramLibrary` from an API object within a Solid component. */ +export function createDiagramLibraryWithApi( + api: Api, + theories: TheoryLibrary, +): DiagramLibrary { + const library = DiagramLibrary.withApi(api, theories); + onCleanup(() => library.destroy()); + return library; +} + +/** Create a `DiagramLibrary` from an Automerge repo within a Solid component. */ +export function createDiagramLibraryWithRepo( + repo: Repo, + theories: TheoryLibrary, +): DiagramLibrary { + const library = DiagramLibrary.withRepo(repo, theories); + onCleanup(() => library.destroy()); + return library; +} + +/** A reactive library of diagrams. + +Maintains a library of diagrams, each associated with an Automerge document, +elaborating and validating a diagram when its associated document changes and +caching the result. Moreover, the cache is reactive when used in a Solid +reactive context. + */ +export class DiagramLibrary { + private entries: ReactiveMap; + private handles: Map; + private isElaborating: Set; + private params: DiagramLibraryParameters; + + constructor(params: DiagramLibraryParameters) { + this.entries = new ReactiveMap(); + this.handles = new Map(); + this.isElaborating = new Set(); + this.params = params; + } + + get size(): number { + return this.entries.size; + } + + static withApi(api: Api, theories: TheoryLibrary): DiagramLibrary { + return new DiagramLibrary({ + canonicalize(refId) { + invariant(uuid.validate(refId), () => `Ref ID is not a valid UUID: ${refId}`); + return refId as DiagramKey; + }, + fetch(refId) { + return api.getDocHandle(refId); + }, + theories, + }); + } + + static withRepo(repo: Repo, theories: TheoryLibrary): DiagramLibrary { + return new DiagramLibrary({ + canonicalize(docId) { + return interpretAsDocumentId(docId) as string as DiagramKey; + }, + fetch(docId) { + return findAndMigrate(repo, docId); + }, + theories, + }); + } + + /** Destroys the diagram library. + + Removes all cached document handles and associated event handlers. If you + create a diagram library in a component by calling `createDiagramLibrary`, this + method will be called automatically when the component unmounts. It is safe + to call this method multiple times. + */ + destroy() { + for (const handle of this.handles.values()) { + handle.destroy(); + } + this.handles.clear(); + this.entries.clear(); + } + + /** Adds a diagram to the library, if it has not already been added. */ + private async addDiagram(refId: RefId) { + const key = this.params.canonicalize(refId); + if (this.entries.has(key)) { + return; + } + + const docHandle = await this.params.fetch(refId); + const [theory, validatedDiagram] = await this.elaborateAndValidate(key, docHandle.doc()); + + const onChange = (payload: DocHandleChangePayload) => this.onChange(key, payload); + docHandle.on("change", onChange); + + this.handles.set(key, { + docHandle, + destroy() { + docHandle.off("change", onChange); + }, + }); + + this.entries.set(key, { + theory, + validatedDiagram, + generation: 1, + }); + } + + private async onChange(key: DiagramKey, payload: DocHandleChangePayload) { + const doc = payload.doc; + if (payload.patches.some((patch) => isPatchToFormalContent(doc, patch))) { + const [theory, validatedDiagram] = await this.elaborateAndValidate(key, doc); + + const generation = (this.entries.get(key)?.generation ?? 0) + 1; + this.entries.set(key, { theory, validatedDiagram, generation }); + } + } + + /** Gets reactive accessor for elaborated diagram. */ + async getElaboratedDiagram(refId: RefId): Promise> { + await this.addDiagram(refId); + + const key = this.params.canonicalize(refId); + return () => this.entries.get(key); + } + + /** Gets "live" diagram containing a reactive diagram document. */ + async getLiveDiagram(refId: RefId): Promise { + await this.addDiagram(refId); + + const key = this.params.canonicalize(refId); + const docHandle = this.handles.get(key)?.docHandle; + invariant(docHandle); + + const liveDoc = makeLiveDoc(docHandle, "diagram"); + return makeLiveDiagram(liveDoc, () => this.entries.get(key)); + } + + /** Use elaborated diagram in a component. */ + useElaboratedDiagram(refId: () => RefId | undefined): Accessor { + const [resource] = createResource(refId, (refId) => this.getElaboratedDiagram(refId)); + return () => resource()?.(); + } + + /** Use "live" diagram in a component. */ + useLiveDiagram(refId: () => RefId | undefined): Accessor { + const [liveDiagram] = createResource(refId, (refId) => this.getLiveDiagram(refId)); + return liveDiagram; + } + + // Outer method detects cycles to avoid looping infinitely. + private async elaborateAndValidate( + key: DiagramKey, + doc: Document, + ): Promise<[Theory, ValidatedDiagram]> { + const theories = this.params.theories; + + if (doc.type !== "diagram" || !doc.theory) { + const theory = await theories.get(theories.defaultTheoryMetadata().id); + const validatedDiagram: ValidatedDiagram = { + tag: "Illformed", + diagram: null, + error: `Document should be a diagram, but has type: ${doc.type}`, + }; + return [theory, validatedDiagram]; + } + + const theory = await theories.get(doc.theory); + let validatedDiagram: ValidatedDiagram; + try { + if (this.isElaborating.has(key)) { + const error = "Diagram contains a cycle of instantiations"; + validatedDiagram = { tag: "Illformed", diagram: null, error }; + } else { + this.isElaborating.add(key); + validatedDiagram = await this._elaborateAndValidate( + key, + doc.notebook, + theory.theory, + ); + } + } finally { + this.isElaborating.delete(key); + } + + return [theory, validatedDiagram]; + } + + // Inner method actually elaborates. Do not call directly! + private async _elaborateAndValidate( + key: DiagramKey, + notebook: DiagramNotebook, + theory: DblTheory, + ): Promise { + return { + tag: "Illformed", + diagram: null, + error: "Diagram elaboration not yet implemented", + }; + // const instantiated = new DblDiagramMap(); + // for (const cell of Nb.getFormalContent(notebook)) { + // if (!(cell.tag === "instantiation" && cell.diagram)) { + // continue; + // } + // const refId = cell.diagram._id; + // if (instantiated.has(refId)) { + // continue; + // } + + // await this.addDiagram(refId as RefId); + // const entry = this.entries.get(this.params.canonicalize(refId as RefId)); + // invariant(entry); + // if (entry.validatedDiagram.tag === "Illformed") { + // const error = `Instantiated diagram is ill-formed: ${entry.validatedDiagram.error}`; + // return { tag: "Illformed", diagram: null, error }; + // } + // instantiated.set(refId, entry.validatedDiagram.diagram); + // } + + // return elaborateAndValidateDiagram(notebook, instantiated, theory, key); + } +} + +/** Elaborate and then validate a diagram notebook. */ +function elaborateAndValidateDiagram( + notebook: DiagramNotebook, + instantiated: DblDiagramMap, + theory: DblTheory, + refId: string, +): ValidatedDiagram { + let diagram: DblDiagram; + try { + diagram = elaborateDiagram(notebook, instantiated, theory, refId); + } catch (e) { + return { tag: "Illformed", diagram: null, error: String(e) }; + } + const result = diagram.validate(); + if (result.tag === "Ok") { + return { tag: "Valid", diagram }; + } else { + return { tag: "Invalid", diagram, errors: result.content }; + } +} + +/** Does the patch to the diagram document affect its formal content? */ +function isPatchToFormalContent(doc: Document, patch: Patch): boolean { + const path = patch.path; + if (!(path[0] === "type" || path[0] === "theory" || path[0] === "notebook")) { + // Ignore changes to top-level data like document name. + return false; + } + if (path[0] === "notebook" && path[1] === "cellContents" && path[2]) { + // Ignores changes to cells without formal content. + const cell = doc.notebook.cellContents[path[2]]; + if (cell?.tag !== "formal") { + return false; + } + // TODO: When only the human-readable labels are changed, update the + // id-label mappings but don't re-elaborate the diagram! + } + return true; +} + +const makeLiveDiagram = ( + liveDoc: LiveDoc, + getEntry: Accessor, +): LiveDiagramDoc => ({ + type: "diagram", + liveDoc, + theory() { + return getEntry()?.theory; + }, + elaboratedDiagram() { + const entry = getEntry(); + if (entry && entry.validatedDiagram.tag !== "Illformed") { + return entry.validatedDiagram.diagram; + } + }, + validatedDiagram() { + return getEntry()?.validatedDiagram; + }, +}); diff --git a/packages/frontend/src/diagram/document.ts b/packages/frontend/src/diagram/document.ts index 4c0363850..b8c0084bd 100644 --- a/packages/frontend/src/diagram/document.ts +++ b/packages/frontend/src/diagram/document.ts @@ -77,6 +77,9 @@ export function enlivenDiagramDocument( // Abort immediately if the theory is undefined or the model is invalid. return undefined; } + if (!(th && th.theory.canElaborateDiagrams())) { + return undefined; + } const { model } = validatedModel; let diagram: DblModelDiagram; try { diff --git a/packages/frontend/src/diagram/index.ts b/packages/frontend/src/diagram/index.ts index 1e4041662..04dcd196d 100644 --- a/packages/frontend/src/diagram/index.ts +++ b/packages/frontend/src/diagram/index.ts @@ -1,2 +1,3 @@ export * from "./context"; export * from "./document"; +export * from "./diagram_library"; diff --git a/packages/frontend/src/diagram/morphism_cell_editor.tsx b/packages/frontend/src/diagram/morphism_cell_editor.tsx index bd698c0d3..101b3d960 100644 --- a/packages/frontend/src/diagram/morphism_cell_editor.tsx +++ b/packages/frontend/src/diagram/morphism_cell_editor.tsx @@ -1,6 +1,5 @@ -import { useContext } from "solid-js"; +import { createMemo, useContext } from "solid-js"; import invariant from "tiny-invariant"; -import { v7 } from "uuid"; import { type FocusHandle, useChildFocus } from "catcolab-ui-components"; import type { DiagramMorDecl } from "catlog-wasm"; @@ -8,7 +7,7 @@ import { BasicMorInput } from "../model/morphism_input"; import type { CellActions } from "../notebook"; import type { Theory } from "../theory"; import { LiveDiagramContext } from "./context"; -import { BasicObInput } from "./object_input"; +import { ObInput } from "./object_input"; import arrowStyles from "../stdlib/arrow_styles.module.css"; import "./morphism_cell_editor.css"; @@ -27,8 +26,28 @@ export function DiagramMorphismCellEditor(props: { // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted cell. const focus = useChildFocus(props.focus, { default: "mor" }); - const domType = () => props.theory.theory.src(props.decl.morType); - const codType = () => props.theory.theory.tgt(props.decl.morType); + const morTypeMeta = () => props.theory.modelMorTypeMeta(props.decl.morType); + + const domType = createMemo(() => { + const theory = props.theory.theory; + const op = morTypeMeta()?.domain?.apply; + if (op === undefined) { + return theory.src(props.decl.morType); + } else { + return theory.dom(op); + } + }); + + const codType = createMemo(() => { + const theory = props.theory.theory; + const op = morTypeMeta()?.codomain?.apply; + if (op === undefined) { + return theory.tgt(props.decl.morType); + } else { + // Codomain type for operation should equal target type above. + return theory.dom(op); + } + }); const errors = () => { const validated = liveDiagram().validatedDiagram(); @@ -45,7 +64,7 @@ export function DiagramMorphismCellEditor(props: { return (
    - { @@ -54,7 +73,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={domType()} - generateId={v7} isInvalid={domInvalid()} focus={focus.childFocus("dom")} deleteForward={() => focus.setActiveChild("mor")} @@ -88,7 +106,7 @@ export function DiagramMorphismCellEditor(props: {
    - { @@ -97,7 +115,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={codType()} - generateId={v7} isInvalid={codInvalid()} focus={focus.childFocus("cod")} deleteBackward={() => focus.setActiveChild("mor")} diff --git a/packages/frontend/src/diagram/object_input.tsx b/packages/frontend/src/diagram/object_input.tsx index aaf9da5d8..ea7c43719 100644 --- a/packages/frontend/src/diagram/object_input.tsx +++ b/packages/frontend/src/diagram/object_input.tsx @@ -1,9 +1,147 @@ -import { useContext } from "solid-js"; +import { deepEqual } from "fast-equals"; +import { type Component, splitProps, useContext } from "solid-js"; +import { Dynamic } from "solid-js/web"; import invariant from "tiny-invariant"; -import type { Ob, ObType, QualifiedName } from "catlog-wasm"; +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, ObOp, ObType, QualifiedName } from "catlog-wasm"; import { type IdInputOptions, ObIdInput } from "../components"; import { LiveDiagramContext } from "./context"; +import { ObListEditor } from "./object_list_editor"; + +/** Props passed to any object input component. */ +export type ObInputProps = { + /** Current value of object, if any. */ + ob: Ob | null; + + /** Handler to set a new value of the object. */ + setOb: (ob: Ob | null) => void; + + /** Type of object being edited. */ + obType: ObType; + + /** Placeholder text to show when no object has been chosen. */ + placeholder?: string; + + /** Whether the choice of object is invalid, say by having wrong type. + + This is a stub; we should propagate error messages from the core. + */ + isInvalid?: boolean; +}; + +/** Input an object that already exists in a model. */ +export function ObInput( + allProps: ObInputProps & + TextInputOptions & { + /** Operation to apply to the object afterwards, if any. */ + applyOp?: ObOp; + }, +) { + const [props, otherProps] = splitProps(allProps, ["ob", "setOb", "obType", "applyOp"]); + + const ob = () => { + if (props.applyOp) { + return props.ob?.tag === "App" && deepEqual(props.ob.content.op, props.applyOp) + ? props.ob.content.ob + : null; + } else { + return props.ob; + } + }; + + const setOb = (ob: Ob | null) => { + if (ob && props.applyOp) { + props.setOb({ + tag: "App", + content: { + op: props.applyOp, + ob, + }, + }); + } else { + props.setOb(ob); + } + }; + + return ( + + ); +} + +function obEditorForType(obType: ObType): Component { + if (obType.tag === "Basic") { + return BasicObInput; + } else if (obType.tag === "ModeApp") { + switch (obType.content.modality) { + case "Discrete": + case "Codiscrete": + return obEditorForType(obType.content.obType); + case "List": + case "SymmetricList": + case "CocartesianList": + case "CartesianList": + case "AdditiveList": { + return ObListEditor; + } + } + } + throw new Error(`No editor for object of type: ${obType}`); +} + +/** Object lookup that falls back to formalJudgments when the diagram + * cannot be elaborated (e.g. modal theories). + */ +export function createObLookup(liveDiagram: Accessor) { + const elaborated = () => liveDiagram().elaboratedDiagram(); + const judgments = () => liveDiagram().formalJudgments(); + + function completions(obType?: ObType): Uuid[] | undefined { + const diag = elaborated(); + if (diag && obType) { + return diag.obGeneratorsWithType(obType); + } + if (!obType) { + return undefined; + } + return judgments() + .filter((j) => j.tag === "object" && deepEqual(j.obType, obType)) + .map((j) => j.id); + } + + function idToLabel(id: QualifiedName): QualifiedLabel | undefined { + const diag = elaborated(); + if (diag) { + return diag.obGeneratorLabel(id); + } + const found = judgments().find((j) => j.tag === "object" && j.id === id); + return found?.tag === "object" && found.name ? [found.name] : undefined; + } + + function labelToId(label: QualifiedLabel): NameLookup | undefined { + const diag = elaborated(); + if (diag) { + return diag.obGeneratorWithLabel(label); + } + const name = String(label[0]); + const matches = judgments().filter((j) => j.tag === "object" && j.name === name); + if (matches.length === 1) { + return { tag: "Unique", content: matches[0].id }; + } + if (matches.length > 1) { + return { tag: "Ambiguous" }; + } + return { tag: "None" }; + } + + return { completions, idToLabel, labelToId }; +} /** Input a basic object in a diagram via its human-readable name. */ @@ -17,15 +155,14 @@ export function BasicObInput( const liveDiagram = useContext(LiveDiagramContext); invariant(liveDiagram, "Live diagram should be provided as context"); - const completions = (): QualifiedName[] | undefined => - props.obType && liveDiagram().elaboratedDiagram()?.obGeneratorsWithType(props.obType); + const lookup = createObLookup(liveDiagram); // FIXME: Push diagram labels into Wasm layer. return ( liveDiagram().elaboratedDiagram()?.obGeneratorLabel(id)} - labelToId={(label) => liveDiagram().elaboratedDiagram()?.obGeneratorWithLabel(label)} + completions={lookup.completions(props.obType)} + idToLabel={lookup.idToLabel} + labelToId={lookup.labelToId} {...props} /> ); diff --git a/packages/frontend/src/diagram/object_list_editor.css b/packages/frontend/src/diagram/object_list_editor.css new file mode 100644 index 000000000..dc7a896ed --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.css @@ -0,0 +1,10 @@ +.diagram-object-decl { + display: flex; + flex-direction: row; + gap: 1ex; + align-items: baseline; + + & .is-a:before { + content: ":"; + } +} diff --git a/packages/frontend/src/diagram/object_list_editor.tsx b/packages/frontend/src/diagram/object_list_editor.tsx new file mode 100644 index 000000000..5b63795b7 --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.tsx @@ -0,0 +1,199 @@ +import { + batch, + createEffect, + createSignal, + Index, + type JSX, + mergeProps, + Show, + untrack, + useContext, +} from "solid-js"; +import invariant from "tiny-invariant"; + +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, QualifiedName } from "catlog-wasm"; +import { ObIdInput } from "../components"; +import { removeProxyAndCopy } from "../util/remove_proxy_and_copy"; +import { LiveDiagramContext } from "./context"; +import type { ObInputProps } from "./object_input"; +import { createObLookup } from "./object_input.tsx"; + +import "./object_list_editor.css"; + +type ObListEditorProps = ObInputProps & + TextInputOptions & { + insertKey?: string; + startDelimiter?: JSX.Element | string; + endDelimiter?: JSX.Element | string; + separator?: (index: number) => JSX.Element | string; + }; + +/** Edits a list of objects of given type. */ +export function ObListEditor(originalProps: ObListEditorProps) { + const props = mergeProps( + { + insertKey: ",", + startDelimiter:
    {"["}
    , + endDelimiter:
    {"]"}
    , + separator: () =>
    {","}
    , + }, + originalProps, + ); + + const liveDiagram = useContext(LiveDiagramContext); + invariant(liveDiagram, "Live model should be provided as context"); + + const lookup = createObLookup(liveDiagram); + + const [activeIndex, setActiveIndex] = createSignal(0); + + const setObList = (objects: Array) => { + props.setOb({ + tag: "List", + content: { + modality: modeAppType().content.modality, + objects, + }, + }); + }; + + const updateObList = (f: (objects: Array) => void) => { + const objects = removeProxyAndCopy(obList()); + f(objects); + setObList(objects); + }; + + const insertNewOb = (i: number) => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 0, null); + }); + setActiveIndex(i); + }); + }; + + const modeAppType = () => { + if (props.obType.tag !== "ModeApp") { + throw new Error(`Object type should be a list modality, received: ${props.obType}`); + } + return props.obType; + }; + + const obList = (): Array => { + if (!props.ob) { + return []; + } + if (props.ob.tag !== "List") { + throw new Error(`Object should be a list, received: ${props.ob}`); + } + return props.ob.content.objects; + }; + + const completions = (): QualifiedName[] | undefined => + lookup.completions(modeAppType().content.obType); + + // Make the default value the empty list, rather than null. + createEffect(() => { + if (!props.ob) { + setObList([]); + } + }); + + // Insert into new object into empty list when focus is gained. + createEffect(() => { + if (props.isActive && untrack(obList).length === 0) { + insertNewOb(0); + } + }); + + return ( +
      { + if (obList().length === 0) { + insertNewOb(0); + props.hasFocused?.(); + evt.preventDefault(); + } + }} + > + {props.startDelimiter} + }> + {(ob, i) => ( +
    • + 0 && props.separator}>{(sep) => sep()(i)} + { + updateObList((objects) => { + objects[i] = ob; + }); + }} + placeholder={props.placeholder} + idToLabel={lookup.idToLabel} + labelToId={lookup.labelToId} + completions={completions()} + isActive={props.isActive && activeIndex() === i} + deleteBackward={() => + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteBackward?.(); + } else { + setActiveIndex(i - 1); + } + }) + } + deleteForward={() => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteForward?.(); + } + }); + }} + exitBackward={() => props.exitBackward?.()} + exitForward={() => props.exitForward?.()} + exitLeft={() => { + if (i === 0) { + props.exitLeft?.(); + } else { + setActiveIndex(i - 1); + } + }} + exitRight={() => { + if (i === obList().length - 1) { + props.exitRight?.(); + } else { + setActiveIndex(i + 1); + } + }} + interceptKeyDown={(evt) => { + if (evt.key === props.insertKey) { + insertNewOb(i + 1); + return true; + } else if (evt.key === "Home" && !evt.shiftKey) { + // TODO: Should move to beginning of input. + setActiveIndex(0); + } else if (evt.key === "End" && !evt.shiftKey) { + setActiveIndex(obList().length - 1); + } + return false; + }} + hasFocused={() => { + setActiveIndex(i); + props.hasFocused?.(); + }} + /> +
      • + )} +       + {props.endDelimiter} +
    + ); +} diff --git a/packages/frontend/src/model/model_editor.tsx b/packages/frontend/src/model/model_editor.tsx index 8236b2e21..0e1101c02 100644 --- a/packages/frontend/src/model/model_editor.tsx +++ b/packages/frontend/src/model/model_editor.tsx @@ -6,10 +6,10 @@ import { Model, Nb } from "catcolab-document-methods"; import type { InstantiatedModel, ModelJudgment, MorDecl, ObDecl } from "catcolab-document-types"; import { type FocusHandle } from "catcolab-ui-components"; import { type CellConstructor, type FormalCellEditorProps, NotebookEditor } from "../notebook"; +import { ModelInstantiationCellEditor } from "./model_instantiation_cell.tsx"; import { TheoryLibraryContext, type ModelTypeMeta, type Theory } from "../theory"; import { LiveModelContext } from "./context"; import type { LiveModelDoc } from "./document"; -import { InstantiationCellEditor } from "./instantiation_cell_editor"; /** Notebook editor for a model of a double theory. */ @@ -95,11 +95,9 @@ export function ModelCellEditor(props: FormalCellEditorProps) { }} - - props.changeContent((content) => f(content as InstantiatedModel)) - } + changeContent={(f) => props.changeContent((c) => f(c as InstantiatedModel))} focus={props.focus} actions={props.actions} /> diff --git a/packages/frontend/src/model/model_instantiation_cell.tsx b/packages/frontend/src/model/model_instantiation_cell.tsx new file mode 100644 index 000000000..c5695dd3f --- /dev/null +++ b/packages/frontend/src/model/model_instantiation_cell.tsx @@ -0,0 +1,116 @@ +import {useContext} from "solid-js"; +import invariant from "tiny-invariant"; + +import { useApi } from "../api"; +import {useUserState} from "../user/user_state_context"; +import { DocRefIdContext } from "../page/context"; +import { LiveModelContext, ModelLibraryContext } from "./context"; +import type { LiveModelDoc } from "./document"; +import { InstantiationCellEditor } from "../components"; + +export function ModelInstantiationCellEditor(props: { + instantiation: InstantiatedModel; + changeContent: (f: (content: InstantiatedModel) => void) => void; + focus: FocusHandle; + actions: CellActions; +}) { + const liveModel = useContext(LiveModelContext); + const models = useContext(ModelLibraryContext); + invariant(models); + const api = useApi(); + const docRefId = useContext(DocRefIdContext); + const userState = useUserState(); + + const refId = () => props.instantiation.model?._id; + const elaborated = models.useElaboratedModel(refId); + + const filterCompletions = (refId, doc) => { + if (doc.typeName !== "model") { + return false; + } + if (docRefId && refId === docRefId()) { + return false; + } + const theory = liveModel?.().liveDoc.doc.theory; + if (theory && doc.theory !== theory) { + return false; + } + return true; + }; + + const config: InstantiationConfig = { + kind: "model", + + refId, + + setRefId(id) { + props.changeContent((inst) => { + inst.model = id ? api.makeUnversionedLink(id, "instantiation") : null; + if (id && !inst.name) { + const docName = userState.documents[id]?.name; + if (docName) inst.name = docName; + } + }); + }, + + filterCompletions(refId, doc) { + if (doc.typeName !== "model") return false; + if (docRefId && refId === docRefId()) return false; + const theory = liveModel?.().liveDoc.doc.theory; + if (theory && doc.theory !== theory) return false; + return true; + }, + + hasInstantiated: () => props.instantiation != null, + + completions: () => props.instantiation.obGenerators(), + idToLabel: (id) => props.instantiation.obGeneratorLabel(id), + labelToId: (label) => props.instantiation.obGeneratorWithLabel(label), + + obSide(p) { + const obType = () => { + const id = p.specialization.id; + if (id) { + const ob: Ob = { tag: "Basic", content: id }; + const m = props.instantiation; + if (m?.hasOb(ob)) return m.obType(ob); + } + }; + return ( + }> + {(obType) => ( + + p.modifySpecialization((s) => { + s.ob = ob; + }) + } + obType={obType()} + focus={p.focus} + deleteBackward={p.deleteBackward} + exitBackward={p.exitBackward} + exitLeft={p.exitLeft} + createBelow={p.createBelow} + exitDown={p.exitDown} + exitUp={p.exitUp} + /> + )} + + ); + }, + }; + + return ( + + props.changeContent((content) => f(content as InstantiatedModel)) + } + config={config} + focus={props.focus} + actions={props.actions} + /> + ); +} diff --git a/packages/frontend/src/stdlib/theories.ts b/packages/frontend/src/stdlib/theories.ts index 507e13a2d..d516d2d83 100644 --- a/packages/frontend/src/stdlib/theories.ts +++ b/packages/frontend/src/stdlib/theories.ts @@ -143,13 +143,13 @@ stdTheories.add( stdTheories.add( { - id: "unary-dec", + id: "dec", name: "Discrete exterior calculus (DEC)", description: "DEC operators on a geometrical space", iconLetters: ["D", "c"], group: "Experimental", }, - async () => (await import("./theories/unary-dec")).default, + async () => (await import("./theories/dec")).default, ); stdTheories.add( diff --git a/packages/frontend/src/stdlib/theories/dec.ts b/packages/frontend/src/stdlib/theories/dec.ts new file mode 100644 index 000000000..7991ca22b --- /dev/null +++ b/packages/frontend/src/stdlib/theories/dec.ts @@ -0,0 +1,59 @@ +import { lazy } from "solid-js"; + +import { ThDEC } from "catlog-wasm"; +import { type DiagramAnalysisMeta, Theory, type TheoryMeta } from "../../theory"; + +const ObjectCellEditor = lazy(() => import("../../model/object_cell_editor")); +const MorphismCellEditor = lazy(() => import("../../model/morphism_cell_editor")); + +export default function createThDECTheory(theoryMeta: TheoryMeta): Theory { + const thDEC = new ThDEC(); + const diagramAnalyses: DiagramAnalysisMeta[] = []; + + return new Theory({ + ...theoryMeta, + theory: thDEC.theory(), + modelTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + editor: ObjectCellEditor, + name: "Form", + description: "State of the system", + shortcut: ["O"], + }, + { + tag: "MorType", + morType: { + tag: "Basic", + content: "Multihom", + }, + editor: MorphismCellEditor, + name: "Operation", + description: "Event causing change of state", + shortcut: ["M"], + }, + ], + instanceOfName: "Diagrams in", + instanceTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + name: "Element", + description: "State of the system", + shortcut: ["O"], + }, + { + tag: "MorType", + morType: { + tag: "Basic", + content: "Multihom", + }, + name: "Operation", + description: "Event causing change of state", + shortcut: ["M"], + }, + ], + diagramAnalyses: diagramAnalyses, + }); +} diff --git a/packages/frontend/src/stdlib/theories/unary-dec.ts b/packages/frontend/src/stdlib/theories/unary-dec.ts deleted file mode 100644 index eec36a32a..000000000 --- a/packages/frontend/src/stdlib/theories/unary-dec.ts +++ /dev/null @@ -1,94 +0,0 @@ -import { lazy } from "solid-js"; - -import { ThCategoryWithScalars } from "catlog-wasm"; -import { Theory, type TheoryMeta } from "../../theory"; -import * as analyses from "../analyses"; - -const ObjectCellEditor = lazy(() => import("../../model/object_cell_editor")); -const MorphismCellEditor = lazy(() => import("../../model/morphism_cell_editor")); - -export default function createUnaryDECTheory(theoryMeta: TheoryMeta): Theory { - const thCategoryWithScalars = new ThCategoryWithScalars(); - - return new Theory({ - ...theoryMeta, - theory: thCategoryWithScalars.theory(), - modelTypes: [ - { - tag: "ObType", - obType: { tag: "Basic", content: "Object" }, - editor: ObjectCellEditor, - name: "Form type", - shortcut: ["F"], - description: "A type of differential form on the space", - }, - { - tag: "MorType", - morType: { tag: "Basic", content: "Nonscalar" }, - editor: MorphismCellEditor, - name: "Operator", - shortcut: ["D"], - description: "A differential operator", - }, - { - tag: "MorType", - morType: { - tag: "Hom", - content: { tag: "Basic", content: "Object" }, - }, - editor: MorphismCellEditor, - name: "Scalar", - arrowStyle: "scalar", - shortcut: ["S"], - description: "Multiplication by a scalar", - }, - ], - instanceOfName: "Equations in", - instanceTypes: [ - { - tag: "ObType", - obType: { tag: "Basic", content: "Object" }, - name: "Form", - description: "A form on the space", - shortcut: ["F"], - }, - { - tag: "MorType", - morType: { tag: "Basic", content: "Nonscalar" }, - name: "Apply operator", - description: "An application of an operator to a form", - shortcut: ["D"], - }, - { - tag: "MorType", - morType: { - tag: "Hom", - content: { tag: "Basic", content: "Object" }, - }, - name: "Scalar multiply", - description: "A scalar multiplication on a form", - shortcut: ["S"], - }, - ], - modelAnalyses: [ - analyses.modelGraph({ - id: "graph", - name: "Visualization", - description: "Visualize the operations as a graph", - help: "visualization", - }), - ], - diagramAnalyses: [ - analyses.diagramGraph({ - id: "graph", - name: "Visualization", - description: "Visualize the equations as a diagram", - }), - analyses.decapodes({ - id: "decapodes", - name: "Simulation", - description: "Simulate the PDE using Decapodes", - }), - ], - }); -}