From 887eb258d5aab23bc65edb68a86287978e28ef4a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 14:45:31 +0200 Subject: [PATCH 01/10] add primary key to `associated_structures` table --- database/schema/001_structures.sql | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 36dfab28..a6550c3f 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -93,6 +93,7 @@ CREATE TABLE associated_structures ( associated_type TEXT NOT NULL, structure_id TEXT NOT NULL, associated_structure_id TEXT NOT NULL, + PRIMARY KEY (label, type, associated_type, structure_id), FOREIGN KEY (label, type, associated_type) REFERENCES associated_structure_types (label, type, associated_type) ON DELETE CASCADE, @@ -100,4 +101,6 @@ CREATE TABLE associated_structures ( REFERENCES structures (id, type) ON DELETE CASCADE, FOREIGN KEY (associated_structure_id, associated_type) REFERENCES structures (id, type) ON DELETE CASCADE -); \ No newline at end of file +); + +CREATE INDEX idx_structure_associations ON associated_structures (structure_id); \ No newline at end of file From b78a676810911b0655c4d41671a5fb9fae87ceda Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 14:48:41 +0200 Subject: [PATCH 02/10] reorder tables in file --- database/schema/001_structures.sql | 45 +++++++++++++++--------------- 1 file changed, 22 insertions(+), 23 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index a6550c3f..e76aee41 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -8,29 +8,6 @@ INSERT INTO structure_types (type) VALUES ('morphism'), ('symmetric_monoidal_category'); - -CREATE TABLE associated_structure_types ( - label TEXT NOT NULL, - type TEXT NOT NULL, - associated_type TEXT NOT NULL, - required INTEGER NOT NULL - CHECK (required in (TRUE, FALSE)), - PRIMARY KEY (label, type, associated_type), - UNIQUE (label, type), - FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE -); - -INSERT INTO associated_structure_types - (label, type, associated_type, required) -VALUES - ('domain', 'functor', 'category', TRUE), - ('codomain', 'functor', 'category', TRUE), - ('category', 'morphism', 'category', TRUE), - ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), - ('left_adjoint', 'functor', 'functor', FALSE), - ('right_adjoint', 'functor', 'functor', FALSE); - CREATE TABLE structures ( id TEXT PRIMARY KEY, type TEXT NOT NULL, @@ -87,6 +64,28 @@ CREATE TABLE structure_tag_assignments ( FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE ); +CREATE TABLE associated_structure_types ( + label TEXT NOT NULL, + type TEXT NOT NULL, + associated_type TEXT NOT NULL, + required INTEGER NOT NULL + CHECK (required in (TRUE, FALSE)), + PRIMARY KEY (label, type, associated_type), + UNIQUE (label, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, + FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE +); + +INSERT INTO associated_structure_types + (label, type, associated_type, required) +VALUES + ('domain', 'functor', 'category', TRUE), + ('codomain', 'functor', 'category', TRUE), + ('category', 'morphism', 'category', TRUE), + ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), + ('left_adjoint', 'functor', 'functor', FALSE), + ('right_adjoint', 'functor', 'functor', FALSE); + CREATE TABLE associated_structures ( label TEXT NOT NULL, type TEXT NOT NULL, From 66d04ef50e01d84aba8a94b85b526d82597d4830 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 15:00:05 +0200 Subject: [PATCH 03/10] fix definition of foreign key in `structures` table --- database/schema/001_structures.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index e76aee41..84002edc 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -19,7 +19,7 @@ CREATE TABLE structures ( parent TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, - FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT + FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT, FOREIGN KEY (parent, type) REFERENCES structures (id, type) ON DELETE RESTRICT ); From c57c27287c66d67972766d7c9fe0cae4f6668433 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 15:00:26 +0200 Subject: [PATCH 04/10] add more relevant indices also, rename some of the existing indices --- database/schema/001_structures.sql | 12 +++++++++--- database/schema/002_properties.sql | 2 +- database/schema/003_implications.sql | 8 ++++---- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 84002edc..dd15ab90 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -25,7 +25,9 @@ CREATE TABLE structures ( CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id)); -CREATE INDEX structure_by_type ON structures (type); +CREATE INDEX idx_structures_by_type ON structures (type); + +CREATE INDEX idx_structures_by_parent ON structures (parent, type); CREATE TABLE related_structures ( id INTEGER PRIMARY KEY, @@ -45,7 +47,7 @@ CREATE TABLE structure_comments ( FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE ); -CREATE INDEX idx_structure_comments ON structure_comments (structure_id); +CREATE INDEX idx_comments_by_structure ON structure_comments (structure_id); CREATE TABLE structure_tags ( id INTEGER PRIMARY KEY, @@ -64,6 +66,8 @@ CREATE TABLE structure_tag_assignments ( FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE ); +CREATE INDEX idx_structures_by_tag ON structure_tag_assignments (type, tag, structure_id); + CREATE TABLE associated_structure_types ( label TEXT NOT NULL, type TEXT NOT NULL, @@ -102,4 +106,6 @@ CREATE TABLE associated_structures ( REFERENCES structures (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_structure_associations ON associated_structures (structure_id); \ No newline at end of file +CREATE INDEX idx_associated_structures_by_structure ON associated_structures (structure_id); + +CREATE INDEX idx_associated_structures_by_target ON associated_structures (associated_structure_id, type, label); \ No newline at end of file diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index 439aaae8..3f6369d0 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -54,7 +54,7 @@ CREATE TABLE property_assignments ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_property_assigned ON property_assignments (property_id); +CREATE INDEX idx_property_assignments_by_property ON property_assignments (property_id); CREATE TABLE property_tags ( id INTEGER PRIMARY KEY, diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 35b27e61..2808483e 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -8,7 +8,7 @@ CREATE TABLE implications ( dual_implication_id TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, - FOREIGN KEY (dual_implication_id) REFERENCES implications (id) + FOREIGN KEY (dual_implication_id, type) REFERENCES implications (id, type) ); CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id)); @@ -26,7 +26,7 @@ CREATE TABLE assumptions ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_assumptions_property ON assumptions (property_id); +CREATE INDEX idx_assumptions_by_property ON assumptions (property_id); CREATE TABLE conclusions ( implication_id TEXT NOT NULL, @@ -39,7 +39,7 @@ CREATE TABLE conclusions ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_conclusions_property ON conclusions (property_id); +CREATE INDEX idx_conclusions_by_property ON conclusions (property_id); CREATE TABLE associated_assumptions ( implication_id TEXT NOT NULL, @@ -57,7 +57,7 @@ CREATE TABLE associated_assumptions ( ON DELETE RESTRICT ); -CREATE INDEX idx_assumptions_associated_property ON associated_assumptions (property_id); +CREATE INDEX idx_assumptions_associated_by_property ON associated_assumptions (property_id); CREATE VIEW implications_view AS SELECT From 72888f27f0ffe20d4cfd64cd5c492bfb72c02431 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 15:13:54 +0200 Subject: [PATCH 05/10] rename table column `parent` to `parent_structure_id` --- database/schema/001_structures.sql | 6 +++--- database/scripts/seed.ts | 2 +- database/scripts/utils/structures.ts | 12 +++++++----- src/lib/commons/types.ts | 2 +- src/lib/server/fetchers/structure.ts | 6 +++--- src/pages/StructurePage.svelte | 7 +++++-- 6 files changed, 20 insertions(+), 15 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index dd15ab90..a0360f06 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -16,18 +16,18 @@ CREATE TABLE structures ( description TEXT NOT NULL, nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), dual_structure_id TEXT, - parent TEXT, + parent_structure_id TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT, - FOREIGN KEY (parent, type) REFERENCES structures (id, type) ON DELETE RESTRICT + FOREIGN KEY (parent_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT ); CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id)); CREATE INDEX idx_structures_by_type ON structures (type); -CREATE INDEX idx_structures_by_parent ON structures (parent, type); +CREATE INDEX idx_structures_by_parent ON structures (parent_structure_id, type); CREATE TABLE related_structures ( id INTEGER PRIMARY KEY, diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 5eb7c605..ccb1dbbd 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -235,7 +235,7 @@ function seed_structures({ const structure_insert = db.prepare( `INSERT INTO structures ( id, type, name, notation, description, nlab_link, - dual_structure_id, parent + dual_structure_id, parent_structure_id ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)` ) diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index ea803720..406a48b8 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -83,11 +83,13 @@ export function is_dual_structure( */ export function get_structure_parent_map(db: Database, type: StructureType) { const structures = db - .prepare< - [StructureType], - { id: string; parent: string | null } - >(`SELECT id, parent FROM structures WHERE type = ?`) + .prepare<[StructureType], { id: string; parent_structure_id: string | null }>( + `SELECT id, parent_structure_id + FROM structures WHERE type = ?` + ) .all(type) - return new Map(structures.map((structure) => [structure.id, structure.parent])) + return new Map( + structures.map((structure) => [structure.id, structure.parent_structure_id]) + ) } diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 4969fb48..f34f5b2c 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -27,7 +27,7 @@ export type StructureDisplay = { dual_structure_id: string | null dual_structure_name: string | null dual_structure_notation: string | null - parent: string | null + parent_structure_id: string | null parent_name: string | null parent_notation: string | null } diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 460b8822..68feafdf 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -26,12 +26,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.dual_structure_id, ds.name AS dual_structure_name, ds.notation AS dual_structure_notation, - s.parent, + s.parent_structure_id, ps.name AS parent_name, ps.notation AS parent_notation FROM structures s LEFT JOIN structures ds ON ds.id = s.dual_structure_id - LEFT JOIN structures ps ON ps.id = s.parent + LEFT JOIN structures ps ON ps.id = s.parent_structure_id WHERE s.id = ?` ) .get(id) @@ -94,7 +94,7 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai const children = db .prepare<[string], RelatedStructure>( `SELECT s.id, s.name, s.notation - FROM structures s WHERE s.parent = ?` + FROM structures s WHERE s.parent_structure_id = ?` ) .all(id) diff --git a/src/pages/StructurePage.svelte b/src/pages/StructurePage.svelte index 63084f6d..9bbd69ae 100644 --- a/src/pages/StructurePage.svelte +++ b/src/pages/StructurePage.svelte @@ -76,10 +76,13 @@ {a.name} {/each} - {#if structure.parent} + {#if structure.parent_structure_id} Parent - + {@html structure.parent_notation} From e2e70d1349ab29c7cef3cb56c6a360139425041e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 17:22:11 +0200 Subject: [PATCH 06/10] rename table `associated_structure_types` to `structure_associations` --- database/schema/001_structures.sql | 6 +++--- database/schema/003_implications.sql | 2 +- database/scripts/deduce-implications.ts | 6 +++--- database/scripts/seed.ts | 12 ++++++------ src/lib/server/fetchers/implication.ts | 6 +++--- src/lib/server/fetchers/structure.ts | 10 +++++----- 6 files changed, 21 insertions(+), 21 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index a0360f06..1c23b296 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -68,7 +68,7 @@ CREATE TABLE structure_tag_assignments ( CREATE INDEX idx_structures_by_tag ON structure_tag_assignments (type, tag, structure_id); -CREATE TABLE associated_structure_types ( +CREATE TABLE structure_associations ( label TEXT NOT NULL, type TEXT NOT NULL, associated_type TEXT NOT NULL, @@ -80,7 +80,7 @@ CREATE TABLE associated_structure_types ( FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE ); -INSERT INTO associated_structure_types +INSERT INTO structure_associations (label, type, associated_type, required) VALUES ('domain', 'functor', 'category', TRUE), @@ -98,7 +98,7 @@ CREATE TABLE associated_structures ( associated_structure_id TEXT NOT NULL, PRIMARY KEY (label, type, associated_type, structure_id), FOREIGN KEY (label, type, associated_type) - REFERENCES associated_structure_types (label, type, associated_type) + REFERENCES structure_associations (label, type, associated_type) ON DELETE CASCADE, FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 2808483e..715c38fd 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -53,7 +53,7 @@ CREATE TABLE associated_assumptions ( FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (label, type, property_type) - REFERENCES associated_structure_types (label, type, associated_type) + REFERENCES structure_associations (label, type, associated_type) ON DELETE RESTRICT ); diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index 896d7ed5..3ed24464 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -24,10 +24,10 @@ export function clear_deduced_implications(type: StructureType) { * then P^op ===> Q^op holds as well. */ export function create_dualized_implications(type: StructureType) { - const associated_structure_types = db + const structure_associations = db .prepare<[StructureType], { label: string; associated_type: StructureType }>( `SELECT label, associated_type - FROM associated_structure_types WHERE type = ?` + FROM structure_associations WHERE type = ?` ) .all(type) @@ -157,7 +157,7 @@ export function create_dualized_implications(type: StructureType) { conclusion_insert.run(dual_id, c, type) } - for (const { label, associated_type } of associated_structure_types) { + for (const { label, associated_type } of structure_associations) { const duals = dual_associated_assumptions[label] for (const d of duals ?? []) { associated_assumption_insert.run( diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index ccb1dbbd..47c4aef8 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -222,13 +222,13 @@ function seed_structures({ folder: string extra?: (structure: T) => void }) { - const associated_structure_types = db + const structure_associations = db .prepare< [StructureType], { label: keyof T; associated_type: StructureType; required: 0 | 1 } >( `SELECT label, associated_type, required - FROM associated_structure_types WHERE type = ?` + FROM structure_associations WHERE type = ?` ) .all(type) @@ -303,7 +303,7 @@ function seed_structures({ record_structure_addition(structure.id) - for (const { label, associated_type, required } of associated_structure_types) { + for (const { label, associated_type, required } of structure_associations) { if (required && !structure[label]) { console.error( `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` @@ -467,10 +467,10 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string * Seeds all implications of a given type from YAML files. */ function seed_implications({ type, folder }: { type: StructureType; folder: string }) { - const associated_structure_types = db + const structure_associations = db .prepare<[StructureType], { label: string; associated_type: StructureType }>( `SELECT label, associated_type - FROM associated_structure_types WHERE type = ?` + FROM structure_associations WHERE type = ?` ) .all(type) @@ -522,7 +522,7 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri if (!impl.associated_assumptions) continue - for (const { label, associated_type } of associated_structure_types) { + for (const { label, associated_type } of structure_associations) { const assumptions = impl.associated_assumptions[label] ?? [] for (const p of assumptions) { associated_assumption_insert.run( diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index d357d72c..e890dac3 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -44,17 +44,17 @@ export function fetch_implication(type: StructureType, id: string) { ) .all(type, id) - const associated_structure_types = db + const structure_associations = db .prepare<[StructureType], { label: string; associated_type: StructureType }>( `SELECT label, associated_type - FROM associated_structure_types + FROM structure_associations WHERE type = ?` ) .all(type) const associated_types: AssociatedTypes = {} - for (const { label, associated_type } of associated_structure_types) { + for (const { label, associated_type } of structure_associations) { associated_types[label] = associated_type } diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 68feafdf..7bb9ef42 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -74,12 +74,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai FROM associated_structures a INNER JOIN structures s ON s.id = a.structure_id - INNER JOIN associated_structure_types ast + INNER JOIN structure_associations sa ON - ast.label = a.label - AND ast.type = a.type - AND ast.associated_type = a.associated_type - WHERE a.associated_structure_id = ? AND ast.required = TRUE + sa.label = a.label + AND sa.type = a.type + AND sa.associated_type = a.associated_type + WHERE a.associated_structure_id = ? AND sa.required = TRUE ORDER BY a.type, lower(s.name)` ) .all(id) From 216c6712e49fb471243c1e477e27137390c6a97d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 20:33:41 +0200 Subject: [PATCH 07/10] rename columns of `structure_associations` and `associated_structures` tables --- database/schema/001_structures.sql | 39 +++++---- database/schema/003_implications.sql | 4 +- database/scripts/deduce-implications.ts | 23 +++--- .../scripts/restrict-functor-properties.ts | 10 +-- .../scripts/restrict-morphism-properties.ts | 10 +-- database/scripts/seed.ts | 29 ++++--- database/scripts/test.ts | 80 +++++++++---------- database/scripts/utils/structures.ts | 4 +- src/lib/commons/types.ts | 4 +- src/lib/server/fetchers/implication.ts | 16 ++-- src/lib/server/fetchers/structure.ts | 22 ++--- src/pages/ImplicationPage.svelte | 17 ++-- src/pages/StructurePage.svelte | 2 +- src/routes/download/+page.svelte | 12 +-- 14 files changed, 132 insertions(+), 140 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 1c23b296..c0ff2432 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -70,18 +70,17 @@ CREATE INDEX idx_structures_by_tag ON structure_tag_assignments (type, tag, stru CREATE TABLE structure_associations ( label TEXT NOT NULL, - type TEXT NOT NULL, - associated_type TEXT NOT NULL, - required INTEGER NOT NULL - CHECK (required in (TRUE, FALSE)), - PRIMARY KEY (label, type, associated_type), - UNIQUE (label, type), - FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE + source_type TEXT NOT NULL, + target_type TEXT NOT NULL, + required INTEGER NOT NULL CHECK (required in (TRUE, FALSE)), + PRIMARY KEY (label, source_type), + UNIQUE (label, source_type, target_type), + FOREIGN KEY (source_type) REFERENCES structure_types (type) ON DELETE CASCADE, + FOREIGN KEY (target_type) REFERENCES structure_types (type) ON DELETE CASCADE ); INSERT INTO structure_associations - (label, type, associated_type, required) + (label, source_type, target_type, required) VALUES ('domain', 'functor', 'category', TRUE), ('codomain', 'functor', 'category', TRUE), @@ -92,20 +91,20 @@ VALUES CREATE TABLE associated_structures ( label TEXT NOT NULL, - type TEXT NOT NULL, - associated_type TEXT NOT NULL, - structure_id TEXT NOT NULL, - associated_structure_id TEXT NOT NULL, - PRIMARY KEY (label, type, associated_type, structure_id), - FOREIGN KEY (label, type, associated_type) - REFERENCES structure_associations (label, type, associated_type) + source_type TEXT NOT NULL, + target_type TEXT NOT NULL, + source_structure_id TEXT NOT NULL, + target_structure_id TEXT NOT NULL, + PRIMARY KEY (label, source_type, source_structure_id), + FOREIGN KEY (label, source_type, target_type) + REFERENCES structure_associations (label, source_type, target_type) ON DELETE CASCADE, - FOREIGN KEY (structure_id, type) + FOREIGN KEY (source_structure_id, source_type) REFERENCES structures (id, type) ON DELETE CASCADE, - FOREIGN KEY (associated_structure_id, associated_type) + FOREIGN KEY (target_structure_id, target_type) REFERENCES structures (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_associated_structures_by_structure ON associated_structures (structure_id); +CREATE INDEX idx_associated_structures_by_source ON associated_structures (source_structure_id); -CREATE INDEX idx_associated_structures_by_target ON associated_structures (associated_structure_id, type, label); \ No newline at end of file +CREATE INDEX idx_associated_structures_by_target ON associated_structures (target_structure_id); \ No newline at end of file diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 715c38fd..7765e4b5 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -53,11 +53,11 @@ CREATE TABLE associated_assumptions ( FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (label, type, property_type) - REFERENCES structure_associations (label, type, associated_type) + REFERENCES structure_associations (label, source_type, target_type) ON DELETE RESTRICT ); -CREATE INDEX idx_assumptions_associated_by_property ON associated_assumptions (property_id); +CREATE INDEX idx_associated_assumptions_by_property ON associated_assumptions (property_id); CREATE VIEW implications_view AS SELECT diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index 3ed24464..2a86aecd 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -25,9 +25,9 @@ export function clear_deduced_implications(type: StructureType) { */ export function create_dualized_implications(type: StructureType) { const structure_associations = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type - FROM structure_associations WHERE type = ?` + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations WHERE source_type = ?` ) .all(type) @@ -149,23 +149,22 @@ export function create_dualized_implications(type: StructureType) { dual_update.run(dual_id, impl.id) - for (const a of dual_assumptions) { - assumption_insert.run(dual_id, a, type) + for (const assumption of dual_assumptions) { + assumption_insert.run(dual_id, assumption, type) } - for (const c of dual_conclusions) { - conclusion_insert.run(dual_id, c, type) + for (const conclusion of dual_conclusions) { + conclusion_insert.run(dual_id, conclusion, type) } - for (const { label, associated_type } of structure_associations) { - const duals = dual_associated_assumptions[label] - for (const d of duals ?? []) { + for (const { label, target_type } of structure_associations) { + for (const assumption of dual_associated_assumptions[label] ?? []) { associated_assumption_insert.run( dual_id, label, - d, + assumption, type, - associated_type + target_type ) } } diff --git a/database/scripts/restrict-functor-properties.ts b/database/scripts/restrict-functor-properties.ts index 7230b009..eb03a3ca 100644 --- a/database/scripts/restrict-functor-properties.ts +++ b/database/scripts/restrict-functor-properties.ts @@ -29,18 +29,18 @@ function restrict_representable_functors() { check_redundancy ) SELECT - a.structure_id, + ass.source_structure_id, 'representable', 'functor', FALSE, 'The codomain is not $\\Set$.', TRUE, FALSE - FROM associated_structures a + FROM associated_structures ass WHERE - a.type = 'functor' - AND a.label = 'codomain' - AND a.associated_structure_id <> 'Set' + ass.source_type = 'functor' + AND ass.label = 'codomain' + AND ass.target_structure_id <> 'Set' ON CONFLICT (structure_id, property_id) DO UPDATE SET proof = excluded.proof, diff --git a/database/scripts/restrict-morphism-properties.ts b/database/scripts/restrict-morphism-properties.ts index e9e087f9..18582944 100644 --- a/database/scripts/restrict-morphism-properties.ts +++ b/database/scripts/restrict-morphism-properties.ts @@ -32,21 +32,21 @@ function restrict_normal_morphisms(variant: 'mono' | 'epi') { check_redundancy ) SELECT - sa.structure_id, + ass.source_structure_id, ?, 'morphism', FALSE, 'The ' || c.name || ' has no zero morphisms.', TRUE, FALSE - FROM associated_structures sa + FROM associated_structures ass INNER JOIN structures c - ON c.id = sa.associated_structure_id + ON c.id = ass.target_structure_id INNER JOIN property_assignments a ON a.structure_id = c.id WHERE - sa.type = 'morphism' - AND sa.label = 'category' + ass.source_type = 'morphism' + AND ass.label = 'category' AND a.property_id = 'zero morphisms' AND a.is_satisfied = FALSE ON CONFLICT (structure_id, property_id) diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 47c4aef8..aa14d457 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -225,10 +225,10 @@ function seed_structures({ const structure_associations = db .prepare< [StructureType], - { label: keyof T; associated_type: StructureType; required: 0 | 1 } + { label: keyof T; target_type: StructureType; required: 0 | 1 } >( - `SELECT label, associated_type, required - FROM structure_associations WHERE type = ?` + `SELECT label, target_type, required + FROM structure_associations WHERE source_type = ?` ) .all(type) @@ -270,8 +270,8 @@ function seed_structures({ const associated_structure_insert = db.prepare( `INSERT INTO associated_structures ( - label, type, associated_type, - structure_id, associated_structure_id + label, source_type, target_type, + source_structure_id, target_structure_id ) VALUES (?, ?, ?, ?, ?)` ) @@ -303,7 +303,7 @@ function seed_structures({ record_structure_addition(structure.id) - for (const { label, associated_type, required } of structure_associations) { + for (const { label, target_type, required } of structure_associations) { if (required && !structure[label]) { console.error( `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` @@ -315,7 +315,7 @@ function seed_structures({ associated_structure_insert.run( label, type, - associated_type, + target_type, structure.id, structure[label] ) @@ -468,9 +468,9 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string */ function seed_implications({ type, folder }: { type: StructureType; folder: string }) { const structure_associations = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type - FROM structure_associations WHERE type = ?` + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations WHERE source_type = ?` ) .all(type) @@ -522,15 +522,14 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri if (!impl.associated_assumptions) continue - for (const { label, associated_type } of structure_associations) { - const assumptions = impl.associated_assumptions[label] ?? [] - for (const p of assumptions) { + for (const { label, target_type } of structure_associations) { + for (const assumption of impl.associated_assumptions[label] ?? []) { associated_assumption_insert.run( impl.id, label, - p, + assumption, type, - associated_type + target_type ) } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 79ef2c91..24af5a1c 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -315,18 +315,18 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm1.structure_id AS right_1, - sm1.associated_structure_id AS left, - sm2.associated_structure_id AS right_2 - FROM associated_structures sm1 - LEFT JOIN associated_structures sm2 + ass1.source_structure_id AS right_1, + ass1.target_structure_id AS left, + ass2.target_structure_id AS right_2 + FROM associated_structures ass1 + LEFT JOIN associated_structures ass2 ON - sm2.type = 'functor' - AND sm2.structure_id = sm1.associated_structure_id - AND sm2.label = 'right_adjoint' + ass2.source_type = 'functor' + AND ass2.label = 'right_adjoint' + AND ass2.source_structure_id = ass1.target_structure_id WHERE - sm1.type = 'functor' - AND sm1.label = 'left_adjoint' + ass1.source_type = 'functor' + AND ass1.label = 'left_adjoint' AND (right_2 IS NULL OR right_2 <> right_1) `, format: ({ right_1, left, right_2 }) => @@ -335,18 +335,18 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm1.structure_id AS left_1, - sm1.associated_structure_id AS right, - sm2.associated_structure_id AS left_2 - FROM associated_structures sm1 - LEFT JOIN associated_structures sm2 + ass1.source_structure_id AS left_1, + ass1.target_structure_id AS right, + ass2.target_structure_id AS left_2 + FROM associated_structures ass1 + LEFT JOIN associated_structures ass2 ON - sm2.type = 'functor' - AND sm2.structure_id = sm1.associated_structure_id - AND sm2.label = 'left_adjoint' + ass2.source_type = 'functor' + AND ass2.label = 'left_adjoint' + AND ass2.source_structure_id = ass1.target_structure_id WHERE - sm1.type = 'functor' - AND sm1.label = 'right_adjoint' + ass1.source_type = 'functor' + AND ass1.label = 'right_adjoint' AND (left_2 IS NULL OR left_2 <> left_1) `, format: ({ left_1, right, left_2 }) => @@ -355,24 +355,24 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm.structure_id AS functor, - sm.associated_structure_id AS left_adjoint, - dom.associated_structure_id AS functor_domain, - adj_cod.associated_structure_id AS left_adjoint_codomain + ass.source_structure_id AS functor, + ass.target_structure_id AS left_adjoint, + dom.target_structure_id AS functor_domain, + adj_cod.target_structure_id AS left_adjoint_codomain FROM - associated_structures sm + associated_structures ass INNER JOIN associated_structures dom ON dom.label = 'domain' - AND dom.type = 'functor' - AND dom.structure_id = sm.structure_id + AND dom.source_type = 'functor' + AND dom.source_structure_id = ass.source_structure_id INNER JOIN associated_structures adj_cod ON adj_cod.label = 'codomain' - AND adj_cod.type = 'functor' - AND adj_cod.structure_id = sm.associated_structure_id + AND adj_cod.source_type = 'functor' + AND adj_cod.source_structure_id = ass.target_structure_id WHERE - sm.label = 'left_adjoint' + ass.label = 'left_adjoint' AND functor_domain <> left_adjoint_codomain `, format: ({ functor, left_adjoint, functor_domain, left_adjoint_codomain }) => @@ -381,24 +381,24 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm.structure_id AS functor, - sm.associated_structure_id AS left_adjoint, - cod.associated_structure_id AS functor_codomain, - adj_dom.associated_structure_id AS left_adjoint_domain + ass.source_structure_id AS functor, + ass.target_structure_id AS left_adjoint, + cod.target_structure_id AS functor_codomain, + adj_dom.target_structure_id AS left_adjoint_domain FROM - associated_structures sm + associated_structures ass INNER JOIN associated_structures cod ON cod.label = 'codomain' - AND cod.type = 'functor' - AND cod.structure_id = sm.structure_id + AND cod.source_type = 'functor' + AND cod.source_structure_id = ass.source_structure_id INNER JOIN associated_structures adj_dom ON adj_dom.label = 'domain' - AND adj_dom.type = 'functor' - AND adj_dom.structure_id = sm.associated_structure_id + AND adj_dom.source_type = 'functor' + AND adj_dom.source_structure_id = ass.target_structure_id WHERE - sm.label = 'left_adjoint' + ass.label = 'left_adjoint' AND functor_codomain <> left_adjoint_domain`, format: ({ functor, left_adjoint, functor_codomain, left_adjoint_domain }) => `❌ Domain/codomain mismatch: ${functor} has codomain ${functor_codomain}, but its left adjoint ${left_adjoint} has domain ${left_adjoint_domain}.` diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 406a48b8..f4b92dd2 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -40,9 +40,9 @@ export function get_structures(db: Database, type: StructureType): StructureMeta json_group_array(pa.property_id) AS props FROM structures s LEFT JOIN associated_structures ass - ON ass.structure_id = s.id + ON ass.source_structure_id = s.id LEFT JOIN property_assignments pa - ON pa.structure_id = ass.associated_structure_id + ON pa.structure_id = ass.target_structure_id AND pa.is_satisfied = TRUE WHERE s.type = ? GROUP BY s.id, ass.label diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index f34f5b2c..0d8241a2 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -15,7 +15,7 @@ export type RelatedStructure = StructureShort & { notation: string } export type AssociatedStructure = RelatedStructure & { label: string - associated_type: StructureType + type: StructureType } export type StructureDisplay = { @@ -32,7 +32,7 @@ export type StructureDisplay = { parent_notation: string | null } -export type AssociatedTypes = Record +export type TargetTypes = Record export type CommentObject = { id: number; comment: string } diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index e890dac3..3509c422 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -2,7 +2,7 @@ import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' import type { ImplicationDB, - AssociatedTypes, + TargetTypes, StructureShort, StructureType } from '$lib/commons/types' @@ -45,18 +45,18 @@ export function fetch_implication(type: StructureType, id: string) { .all(type, id) const structure_associations = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type FROM structure_associations - WHERE type = ?` + WHERE source_type = ?` ) .all(type) - const associated_types: AssociatedTypes = {} + const target_types: TargetTypes = {} - for (const { label, associated_type } of structure_associations) { - associated_types[label] = associated_type + for (const { label, target_type } of structure_associations) { + target_types[label] = target_type } - return { type, implication, property_relation_dict, structures, associated_types } + return { type, implication, property_relation_dict, structures, target_types } } diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 7bb9ef42..884111b2 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -46,12 +46,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.id, s.name, s.notation, - a.label, - a.associated_type - FROM associated_structures a + s.type, + ass.label + FROM associated_structures ass INNER JOIN structures s - ON s.id = a.associated_structure_id - WHERE a.structure_id = ?` + ON s.id = ass.target_structure_id + WHERE ass.source_structure_id = ?` ) .all(id) @@ -70,17 +70,17 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai const list_structures_based_on = db .prepare<[string], StructureShort & { type: StructureType }>( - `SELECT DISTINCT s.id, s.name, a.type + `SELECT DISTINCT s.id, s.name, s.type FROM associated_structures a INNER JOIN structures s - ON s.id = a.structure_id + ON s.id = a.source_structure_id INNER JOIN structure_associations sa ON sa.label = a.label - AND sa.type = a.type - AND sa.associated_type = a.associated_type - WHERE a.associated_structure_id = ? AND sa.required = TRUE - ORDER BY a.type, lower(s.name)` + AND sa.source_type = a.source_type + AND sa.target_type = a.target_type + WHERE a.target_structure_id = ? AND sa.required = TRUE + ORDER BY s.type, lower(s.name)` ) .all(id) diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 9eee9c02..31c790a6 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -7,7 +7,7 @@ import type { ImplicationDisplay, StructureShort, - AssociatedTypes, + TargetTypes, StructureType } from '$lib/commons/types' import { PLURALS } from '$shared/config' @@ -18,17 +18,12 @@ type: StructureType implication: ImplicationDisplay structures: StructureShort[] - associated_types: AssociatedTypes + target_types: TargetTypes property_relation_dict: Record> } - let { - type, - implication, - structures, - associated_types, - property_relation_dict - }: Props = $props() + let { type, implication, structures, target_types, property_relation_dict }: Props = + $props() let has_associated_assumptions = $derived( Object.values(implication.associated_assumptions).some((list) => list?.size) @@ -54,8 +49,8 @@ whose {remove_underscores(label)} {#each set as property, index} - {property_relation_dict[associated_types[label]][property]} - {get_property_label(property)}{#if index < set.size - 1}  and  diff --git a/src/pages/StructurePage.svelte b/src/pages/StructurePage.svelte index 9bbd69ae..3455f568 100644 --- a/src/pages/StructurePage.svelte +++ b/src/pages/StructurePage.svelte @@ -73,7 +73,7 @@ {#each associated_structures as a} {capitalize(remove_underscores(a.label))} - {a.name} + {a.name} {/each} {#if structure.parent_structure_id} diff --git a/src/routes/download/+page.svelte b/src/routes/download/+page.svelte index 5b09bd0d..6ad054b4 100644 --- a/src/routes/download/+page.svelte +++ b/src/routes/download/+page.svelte @@ -255,10 +255,10 @@ WHERE is_satisfied IS NULL;`} language="sql" title="Functors with left adjoints" code={`SELECT - structure_id AS functor, - associated_structure_id AS left_adjoint + source_structure_id AS functor, + target_structure_id AS left_adjoint FROM associated_structures -WHERE type = 'functor' +WHERE source_type = 'functor' AND label = 'left_adjoint';`} /> @@ -266,10 +266,10 @@ AND label = 'left_adjoint';`} language="sql" title="Symmetric monoidal categories with their underlying categories" code={`SELECT - structure_id AS symmetric_monoidal_category, - associated_structure_id AS category + source_structure_id AS symmetric_monoidal_category, + target_structure_id AS category FROM associated_structures -WHERE type = 'symmetric_monoidal_category' +WHERE source_type = 'symmetric_monoidal_category' AND label = 'underlying_category';`} /> From 11d45f6492e3ffab4104b0a4cffdd67d6952cd6d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 18 Sep 2026 20:38:11 +0200 Subject: [PATCH 08/10] refactor type for structure page --- src/pages/StructurePage.svelte | 27 ++------------------------- src/pages/TaggedStructuresPage.svelte | 4 ++-- 2 files changed, 4 insertions(+), 27 deletions(-) diff --git a/src/pages/StructurePage.svelte b/src/pages/StructurePage.svelte index 3455f568..9ae2ba54 100644 --- a/src/pages/StructurePage.svelte +++ b/src/pages/StructurePage.svelte @@ -6,34 +6,11 @@ import TagList from '$components/TagList.svelte' import IndistinguishableStructures from '$components/IndistinguishableStructures.svelte' import StructuresBasedOn from '$components/StructuresBasedOn.svelte' - import type { - AssociatedStructure, - CommentObject, - PropertyAssignmentDisplay, - PropertyShort, - RelatedStructure, - StructureDisplay, - StructureShort, - StructureShortDictionary, - StructureType - } from '$lib/commons/types' + import type { StructureDetails } from '$lib/commons/types' import type { Snippet } from 'svelte' import { capitalize, remove_underscores } from '$shared/utils' - type Props = { - type: StructureType - structure: StructureDisplay - associated_structures: AssociatedStructure[] - related_structures: RelatedStructure[] - structures_based_on: StructureShortDictionary - children: RelatedStructure[] - tags: string[] - satisfied_properties: PropertyAssignmentDisplay[] - unsatisfied_properties: PropertyAssignmentDisplay[] - unknown_properties: PropertyShort[] - undecidable_properties: PropertyAssignmentDisplay[] - indistinguishable_structures: StructureShort[] - comments: CommentObject[] + type Props = StructureDetails & { definition?: Snippet specials?: Snippet } diff --git a/src/pages/TaggedStructuresPage.svelte b/src/pages/TaggedStructuresPage.svelte index 39965f89..9b6ec66b 100644 --- a/src/pages/TaggedStructuresPage.svelte +++ b/src/pages/TaggedStructuresPage.svelte @@ -1,7 +1,7 @@