From ebc0e9443da167b6e8f7ef780eec41e681ce0b58 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 7 Jul 2026 00:17:38 +0200 Subject: [PATCH 01/17] create shared folder and support imports --- databases/tsconfig.json | 14 ++++++++++++++ package.json | 12 ++++++------ shared/utils.ts | 0 svelte.config.js | 3 ++- 4 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 databases/tsconfig.json create mode 100644 shared/utils.ts diff --git a/databases/tsconfig.json b/databases/tsconfig.json new file mode 100644 index 000000000..0bee711b6 --- /dev/null +++ b/databases/tsconfig.json @@ -0,0 +1,14 @@ +{ + "compilerOptions": { + "module": "ESNext", + "moduleResolution": "bundler", + "paths": { + "$shared/*": ["../shared/*"] + }, + "strict": true, + "esModuleInterop": true, + "resolveJsonModule": true, + "noEmit": true + }, + "include": ["**/*.ts"] +} diff --git a/package.json b/package.json index aac44ed52..d9d76059c 100644 --- a/package.json +++ b/package.json @@ -19,14 +19,14 @@ "db:kill": "rm -rf databases/catdat/catdat.db", "db:setup:catdat": "pnpm db:kill && tsx databases/catdat/scripts/setup.ts", "db:setup": "pnpm db:kill && tsx databases/catdat/scripts/setup.ts && tsx databases/app/scripts/setup.ts", - "db:seed": "tsx databases/catdat/scripts/seed.ts", - "db:deduce": "tsx databases/catdat/scripts/deduce.ts", - "db:test": "tsx databases/catdat/scripts/test.ts", + "db:seed": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/seed.ts", + "db:deduce": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/deduce.ts", + "db:test": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/test.ts", "db:snapshot": "cp databases/catdat/catdat.db static/databases/catdat-snapshot.db", "db:update": "pnpm db:seed && pnpm db:deduce && pnpm db:test && pnpm db:snapshot", - "db:watch": "tsx databases/catdat/scripts/watch.ts", - "db:redundancies": "tsx databases/catdat/scripts/redundancies.ts", - "db:proof-length": "tsx databases/catdat/scripts/proof-length.ts", + "db:watch": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/watch.ts", + "db:redundancies": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/redundancies.ts", + "db:proof-length": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/proof-length.ts", "e2e": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test", "e2e:debug": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --debug", "e2e:ui": "PUBLIC_PLAYWRIGHT=true pnpm exec playwright test --ui" diff --git a/shared/utils.ts b/shared/utils.ts new file mode 100644 index 000000000..e69de29bb diff --git a/svelte.config.js b/svelte.config.js index 721beb7a1..2e3148e60 100644 --- a/svelte.config.js +++ b/svelte.config.js @@ -7,7 +7,8 @@ const config = { kit: { alias: { $components: './src/components', - $pages: './src/pages' + $pages: './src/pages', + $shared: './shared' }, adapter: adapter() } From c2680724c2ca0552de02383c80aa4e2ea58dff53 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 7 Jul 2026 00:27:41 +0200 Subject: [PATCH 02/17] add structure types to shared code --- databases/catdat/scripts/config.ts | 4 +--- databases/catdat/scripts/deduce-implications.ts | 3 ++- databases/catdat/scripts/deduce-structure-properties.ts | 3 ++- databases/catdat/scripts/proof-length.ts | 2 +- databases/catdat/scripts/redundancies.ts | 2 +- databases/catdat/scripts/seed.ts | 3 ++- databases/catdat/scripts/test.ts | 3 ++- databases/catdat/scripts/utils/implications.ts | 2 +- databases/catdat/scripts/utils/properties.ts | 2 +- databases/catdat/scripts/utils/structures.ts | 3 ++- shared/config.ts | 3 +++ src/components/StructureSelector.svelte | 3 ++- src/lib/commons/structures.ts | 4 +--- src/lib/commons/types.ts | 2 +- src/routes/[type]-list/+page.server.ts | 3 ++- src/routes/missing/+page.server.ts | 2 +- src/routes/missing/+page.svelte | 3 ++- 17 files changed, 27 insertions(+), 20 deletions(-) create mode 100644 shared/config.ts diff --git a/databases/catdat/scripts/config.ts b/databases/catdat/scripts/config.ts index 7014eef2d..484ba0af7 100644 --- a/databases/catdat/scripts/config.ts +++ b/databases/catdat/scripts/config.ts @@ -1,6 +1,4 @@ -export const STRUCTURE_TYPES = ['category', 'functor', 'morphism'] as const - -export type StructureType = (typeof STRUCTURE_TYPES)[number] +import { type StructureType } from '$shared/config' export const STRUCTURE_TYPES_WITH_DUALS: StructureType[] = ['category'] diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts index ef7eff7ce..e5e9ef4b2 100644 --- a/databases/catdat/scripts/deduce-implications.ts +++ b/databases/catdat/scripts/deduce-implications.ts @@ -1,4 +1,5 @@ -import { STRUCTURE_TYPES_WITH_DUALS, type StructureType } from './config' +import { STRUCTURE_TYPES_WITH_DUALS } from './config' +import { type StructureType } from '$shared/config' import { are_equal_sets, parse_nested_json_set, parse_json_set } from './utils/helpers' import { get_client } from './utils/db' diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index cbb827ba3..a06076fd1 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -17,7 +17,8 @@ import { get_proof_string, NormalizedImplication } from './utils/implications' -import { STRUCTURE_TYPES_WITH_DUALS, type StructureType } from './config' +import { STRUCTURE_TYPES_WITH_DUALS } from './config' +import { type StructureType } from '$shared/config' import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures' /** diff --git a/databases/catdat/scripts/proof-length.ts b/databases/catdat/scripts/proof-length.ts index af5544169..fc06a516d 100644 --- a/databases/catdat/scripts/proof-length.ts +++ b/databases/catdat/scripts/proof-length.ts @@ -1,4 +1,4 @@ -import { type StructureType } from './config' +import { type StructureType } from '$shared/config' import { get_client } from './utils/db' const db = get_client() diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 3e1af4df6..67d7eef6c 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -4,7 +4,7 @@ import { get_deduced_unsatisfied_properties } from './deduce-structure-properties' import { get_property_assignments_by_deduction } from './utils/properties' -import type { StructureType } from './config' +import { type StructureType } from '$shared/config' import { get_normalized_implications, type NormalizedImplication diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 78eb7bfd1..e5a92fae9 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -12,7 +12,8 @@ import type { MorphismYaml } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' -import { PLURALS, STRUCTURE_TYPES, type StructureType } from './config' +import { PLURALS } from './config' +import { STRUCTURE_TYPES, type StructureType } from '$shared/config' const db = get_client() diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index f34ee047d..5e6461e73 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -14,7 +14,8 @@ import decided_functors from './expected-data/decided-functors.json' import decided_morphisms from './expected-data/decided-morphisms.json' import { capitalize } from './utils/helpers' import { get_client } from './utils/db' -import { PLURALS, STRUCTURE_TYPES, type StructureType } from './config' +import { PLURALS } from './config' +import { STRUCTURE_TYPES, type StructureType } from '$shared/config' import fs from 'node:fs' import path from 'node:path' import { decode_property_ID } from '../../../src/lib/commons/property.utils' diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index 5c02874ef..6dfcba3ad 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -1,6 +1,6 @@ import { type Database } from 'better-sqlite3' import type { PropertyMeta } from './properties' -import { StructureType } from '../config' +import { type StructureType } from '$shared/config' import { parse_nested_json_set, parse_json_set } from './helpers' import { get_property_label } from '../../../../src/lib/commons/property.utils' diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts index cdfcfa84c..e84ec9919 100644 --- a/databases/catdat/scripts/utils/properties.ts +++ b/databases/catdat/scripts/utils/properties.ts @@ -1,5 +1,5 @@ import { type Database } from 'better-sqlite3' -import type { StructureType } from '../config' +import { type StructureType } from '$shared/config' /** * Property of a categorical structure diff --git a/databases/catdat/scripts/utils/structures.ts b/databases/catdat/scripts/utils/structures.ts index 565f848e9..d870fdd79 100644 --- a/databases/catdat/scripts/utils/structures.ts +++ b/databases/catdat/scripts/utils/structures.ts @@ -1,5 +1,6 @@ import { type Database } from 'better-sqlite3' -import { StructureType, TABLES } from '../config' +import { TABLES } from '../config' +import { type StructureType } from '$shared/config' /** * Type for various types of categorical structures (category, functor, ...) diff --git a/shared/config.ts b/shared/config.ts new file mode 100644 index 000000000..aed1ffc39 --- /dev/null +++ b/shared/config.ts @@ -0,0 +1,3 @@ +export const STRUCTURE_TYPES = ['category', 'functor', 'morphism'] as const + +export type StructureType = (typeof STRUCTURE_TYPES)[number] diff --git a/src/components/StructureSelector.svelte b/src/components/StructureSelector.svelte index c73e86cf7..7efc2b82b 100644 --- a/src/components/StructureSelector.svelte +++ b/src/components/StructureSelector.svelte @@ -1,8 +1,9 @@ diff --git a/src/routes/[type]-comparison/+page.server.ts b/src/routes/[type]-comparison/+page.server.ts index 6164bf3ce..421c78d3d 100644 --- a/src/routes/[type]-comparison/+page.server.ts +++ b/src/routes/[type]-comparison/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_structures } from '$lib/server/fetchers/structures' import { error } from '@sveltejs/kit' diff --git a/src/routes/[type]-comparison/[...ids]/+page.server.ts b/src/routes/[type]-comparison/[...ids]/+page.server.ts index 326717db7..4599c77b5 100644 --- a/src/routes/[type]-comparison/[...ids]/+page.server.ts +++ b/src/routes/[type]-comparison/[...ids]/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_comparison_result } from '$lib/server/fetchers/comparison' import { cache_page } from '$lib/server/utils' import { error } from '@sveltejs/kit' diff --git a/src/routes/[type]-implication/[id]/+page.server.ts b/src/routes/[type]-implication/[id]/+page.server.ts index 5dc67fa23..acb0de2ad 100644 --- a/src/routes/[type]-implication/[id]/+page.server.ts +++ b/src/routes/[type]-implication/[id]/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_implication } from '$lib/server/fetchers/implication' import { render_nested_formulas } from '$lib/server/formulas' import { error } from '@sveltejs/kit' diff --git a/src/routes/[type]-implications/+page.server.ts b/src/routes/[type]-implications/+page.server.ts index d8e406583..ccfb65564 100644 --- a/src/routes/[type]-implications/+page.server.ts +++ b/src/routes/[type]-implications/+page.server.ts @@ -1,6 +1,6 @@ import { render_nested_formulas } from '$lib/server/formulas' import { fetch_implications } from '$lib/server/fetchers/implications' -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { error } from '@sveltejs/kit' export const load = (event) => { diff --git a/src/routes/[type]-list/+page.server.ts b/src/routes/[type]-list/+page.server.ts index d38d204ec..ebc7eb0ac 100644 --- a/src/routes/[type]-list/+page.server.ts +++ b/src/routes/[type]-list/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_structures_and_tags } from '$lib/server/fetchers/structures' import { error } from '@sveltejs/kit' import type { EntryGenerator } from './$types' diff --git a/src/routes/[type]-list/[tag]/+page.server.ts b/src/routes/[type]-list/[tag]/+page.server.ts index b167a39c3..3050f2c03 100644 --- a/src/routes/[type]-list/[tag]/+page.server.ts +++ b/src/routes/[type]-list/[tag]/+page.server.ts @@ -1,5 +1,5 @@ import { fetch_tagged_structures } from '$lib/server/fetchers/structures' -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { error } from '@sveltejs/kit' import type { EntryGenerator } from './$types' import { fetch_structure_tags } from '$lib/server/fetchers/tags' diff --git a/src/routes/[type]-properties/+page.server.ts b/src/routes/[type]-properties/+page.server.ts index c9b3687fe..07950b57d 100644 --- a/src/routes/[type]-properties/+page.server.ts +++ b/src/routes/[type]-properties/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_grouped_properties_and_tags } from '$lib/server/fetchers/properties' import { error } from '@sveltejs/kit' diff --git a/src/routes/[type]-properties/[tag]/+page.server.ts b/src/routes/[type]-properties/[tag]/+page.server.ts index 28049e913..d5508d79f 100644 --- a/src/routes/[type]-properties/[tag]/+page.server.ts +++ b/src/routes/[type]-properties/[tag]/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { fetch_tagged_properties } from '$lib/server/fetchers/properties' import { error } from '@sveltejs/kit' import type { EntryGenerator } from './$types' diff --git a/src/routes/[type]-property/[id]/+page.server.ts b/src/routes/[type]-property/[id]/+page.server.ts index 51bb06fe2..c78782d44 100644 --- a/src/routes/[type]-property/[id]/+page.server.ts +++ b/src/routes/[type]-property/[id]/+page.server.ts @@ -1,7 +1,7 @@ import { render_nested_formulas } from '$lib/server/formulas' -import { decode_property_ID } from '$lib/commons/property.utils' +import { decode_property_ID } from '$shared/property.utils' import { fetch_property } from '$lib/server/fetchers/property' -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { error } from '@sveltejs/kit' export const load = (event) => { diff --git a/src/routes/[type]-search/+page.server.ts b/src/routes/[type]-search/+page.server.ts index 3bdfc3016..963f48f24 100644 --- a/src/routes/[type]-search/+page.server.ts +++ b/src/routes/[type]-search/+page.server.ts @@ -1,4 +1,4 @@ -import { is_structure_type } from '$lib/commons/structures' +import { is_structure_type } from '$shared/config' import { get_property_ids } from '$lib/server/fetchers/properties' import { error } from '@sveltejs/kit' diff --git a/src/routes/[type]-search/+page.svelte b/src/routes/[type]-search/+page.svelte index de71fe568..e19c21d44 100644 --- a/src/routes/[type]-search/+page.svelte +++ b/src/routes/[type]-search/+page.svelte @@ -1,5 +1,5 @@ From aa128b61f5c0506c163d2b13b5c512e22bd0774e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 7 Jul 2026 09:12:38 +0200 Subject: [PATCH 04/17] small refactorings --- databases/catdat/scripts/proof-length.ts | 12 +++++++----- databases/catdat/scripts/redundancies.ts | 5 +++-- src/lib/server/{utils.ts => cache.ts} | 0 src/lib/server/formulas.ts | 8 +++++++- src/lib/server/macros.ts | 7 ------- .../[type]-comparison/[...ids]/+page.server.ts | 2 +- src/routes/[type]-search/results/+page.server.ts | 2 +- 7 files changed, 19 insertions(+), 17 deletions(-) rename src/lib/server/{utils.ts => cache.ts} (100%) delete mode 100644 src/lib/server/macros.ts diff --git a/databases/catdat/scripts/proof-length.ts b/databases/catdat/scripts/proof-length.ts index fc06a516d..e4176f911 100644 --- a/databases/catdat/scripts/proof-length.ts +++ b/databases/catdat/scripts/proof-length.ts @@ -1,4 +1,4 @@ -import { type StructureType } from '$shared/config' +import { STRUCTURE_TYPES, type StructureType } from '$shared/config' import { get_client } from './utils/db' const db = get_client() @@ -12,10 +12,12 @@ report_long_proofs() * perhaps be moved to a separate content page. */ function report_long_proofs() { - report_long_property_proofs('category') - report_long_property_proofs('functor') - report_long_implication_proofs('category') - report_long_implication_proofs('functor') + for (const type of STRUCTURE_TYPES) { + report_long_property_proofs(type) + } + for (const type of STRUCTURE_TYPES) { + report_long_implication_proofs(type) + } } function report_long_property_proofs(type: StructureType) { diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 67d7eef6c..feabc9044 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -20,8 +20,9 @@ check_redundancies() * No error is thrown intentionally. */ function check_redundancies() { - check_redundant_property_assignments('category') - check_redundant_property_assignments('functor') + for (const type of STRUCTURE_TYPES) { + check_redundant_property_assignments(type) + } } /** diff --git a/src/lib/server/utils.ts b/src/lib/server/cache.ts similarity index 100% rename from src/lib/server/utils.ts rename to src/lib/server/cache.ts diff --git a/src/lib/server/formulas.ts b/src/lib/server/formulas.ts index da9b89dfb..302b851cb 100644 --- a/src/lib/server/formulas.ts +++ b/src/lib/server/formulas.ts @@ -1,6 +1,12 @@ import katex from 'katex' import { is_object } from '$shared/utils' -import { MACROS } from './macros' +import YAML from 'yaml' +import path from 'node:path' +import fs from 'node:fs' + +const MACROS = YAML.parse( + fs.readFileSync(path.resolve('databases', 'catdat', 'data', 'macros.yaml'), 'utf8'), +) as Record export const MATH_REGEX = /\$\$(.*?)\$\$|\$(.*?)\$/gs diff --git a/src/lib/server/macros.ts b/src/lib/server/macros.ts deleted file mode 100644 index 36c84d050..000000000 --- a/src/lib/server/macros.ts +++ /dev/null @@ -1,7 +0,0 @@ -import YAML from 'yaml' -import path from 'node:path' -import fs from 'node:fs' - -export const MACROS = YAML.parse( - fs.readFileSync(path.resolve('databases', 'catdat', 'data', 'macros.yaml'), 'utf8') -) as Record diff --git a/src/routes/[type]-comparison/[...ids]/+page.server.ts b/src/routes/[type]-comparison/[...ids]/+page.server.ts index 4599c77b5..f39bd4f4f 100644 --- a/src/routes/[type]-comparison/[...ids]/+page.server.ts +++ b/src/routes/[type]-comparison/[...ids]/+page.server.ts @@ -1,6 +1,6 @@ import { is_structure_type } from '$shared/config' import { fetch_comparison_result } from '$lib/server/fetchers/comparison' -import { cache_page } from '$lib/server/utils' +import { cache_page } from '$lib/server/cache' import { error } from '@sveltejs/kit' export const prerender = false diff --git a/src/routes/[type]-search/results/+page.server.ts b/src/routes/[type]-search/results/+page.server.ts index b8082a9a2..9194e3149 100644 --- a/src/routes/[type]-search/results/+page.server.ts +++ b/src/routes/[type]-search/results/+page.server.ts @@ -1,6 +1,6 @@ import { is_structure_type } from '$shared/config' import { fetch_search_results } from '$lib/server/fetchers/search' -import { cache_page } from '$lib/server/utils' +import { cache_page } from '$lib/server/cache' import { error } from '@sveltejs/kit' export const prerender = false From c666ab377cc9aae04c1a96166e72d2caae205fef Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 9 Jul 2026 12:33:53 +0200 Subject: [PATCH 05/17] remove parse_nested_json_list, use set utility instead, adjust implication type --- databases/catdat/scripts/utils/implications.ts | 4 ++-- shared/utils.ts | 9 --------- src/components/ImplicationItem.svelte | 2 +- src/lib/commons/types.ts | 2 +- src/lib/server/fetchers/implications.ts | 6 +++--- src/lib/server/transforms.ts | 4 ++-- src/pages/ImplicationPage.svelte | 8 ++++---- 7 files changed, 13 insertions(+), 22 deletions(-) diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index 76a90d8d3..d02f3b4db 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -41,8 +41,8 @@ export function get_normalized_implications( assumptions, conclusions, mapped_assumptions - FROM implications_view i - WHERE i.type = ?` + FROM implications_view + WHERE type = ?` ) .all(type) diff --git a/shared/utils.ts b/shared/utils.ts index 805e479e8..fe4a3eaac 100644 --- a/shared/utils.ts +++ b/shared/utils.ts @@ -51,15 +51,6 @@ export function parse_nested_json_set(json: string): Partial(json: string): Partial> { - const obj = JSON.parse(json) - const result: Partial> = {} - for (const key in obj) { - result[key] = JSON.parse(obj[key]) - } - return result -} - export function to_placeholders(arr: string[]): string { return arr.map(() => '?').join(', ') } diff --git a/src/components/ImplicationItem.svelte b/src/components/ImplicationItem.svelte index bdfb6fe9e..4e4932536 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -18,7 +18,7 @@ let { type, implication, highlighted_property }: Props = $props() let has_additional_assumptions = $derived( - Object.values(implication.mapped_assumptions).some((list) => list?.length) + Object.values(implication.mapped_assumptions).some((list) => list?.size) ) diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 84f24f4eb..1c67c6ac0 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -97,7 +97,7 @@ export type ImplicationDisplay = Replace< is_deduced: boolean assumptions: string[] conclusions: string[] - mapped_assumptions: Partial> + mapped_assumptions: Partial>> } > diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts index 4d1697d49..a280844d4 100644 --- a/src/lib/server/fetchers/implications.ts +++ b/src/lib/server/fetchers/implications.ts @@ -7,7 +7,7 @@ import type { StructureType } from '$lib/commons/types' import { display_implication } from '$lib/server/transforms' -import { parse_json_set, parse_nested_json_list } from '$shared/utils' +import { parse_json_set, parse_nested_json_set } from '$shared/utils' export function fetch_implications(type: StructureType) { const { rows, err } = query(sql` @@ -67,9 +67,9 @@ export function get_normalized_implications(type: StructureType) { for (const impl of rows) { const assumptions = parse_json_set(impl.assumptions) const conclusions = parse_json_set(impl.conclusions) - const mapped_assumptions = parse_nested_json_list(impl.mapped_assumptions) + const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) - if (Object.values(mapped_assumptions).some((list) => list?.length)) continue + if (Object.values(mapped_assumptions).some((list) => list?.size)) continue for (const conclusion of conclusions) { implications.push({ id: impl.id, assumptions, conclusion }) diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index 97833b0e4..b5c808a79 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -6,7 +6,7 @@ import type { ImplicationDB, ImplicationDisplay } from '$lib/commons/types' -import { parse_nested_json_list } from '$shared/utils' +import { parse_nested_json_set } from '$shared/utils' export function display_property(property: PropertyDB): PropertyDisplay { return { @@ -39,6 +39,6 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp proof: implication.proof, assumptions: JSON.parse(implication.assumptions), conclusions: JSON.parse(implication.conclusions), - mapped_assumptions: parse_nested_json_list(implication.mapped_assumptions) + mapped_assumptions: parse_nested_json_set(implication.mapped_assumptions) } } diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index ef992684e..ed25d86a4 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -39,14 +39,14 @@ {/each}

-{#each Object.entries(implication.mapped_assumptions) as [map, list]} - {#if list?.length} +{#each Object.entries(implication.mapped_assumptions) as [map, set]} + {#if set?.size}

Requirements of the {map}: - {#each list as property, index} + {#each set as property, index} {property}{#if index < list.length - 1} + >{#if index < set.size - 1} ,  {/if} {/each} From b0afade004cf44c7413fb203ad2377bc74598eff Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 9 Jul 2026 12:50:05 +0200 Subject: [PATCH 06/17] move function for normalized implications to the shared folder --- .../scripts/deduce-structure-properties.ts | 8 +- databases/catdat/scripts/redundancies.ts | 2 +- .../catdat/scripts/utils/implications.ts | 86 +----------------- shared/implications.ts | 88 +++++++++++++++++++ src/lib/commons/types.ts | 6 -- src/lib/server/consistency.ts | 14 +-- src/lib/server/fetchers/implications.ts | 64 +------------- src/lib/server/fetchers/missing_data.ts | 10 +-- 8 files changed, 107 insertions(+), 171 deletions(-) create mode 100644 shared/implications.ts diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index efb6d3fc7..a8950770a 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -11,14 +11,10 @@ import { get_property_assignments, type PropertyMeta } from './utils/properties' -import { - get_contradiction_string, - get_normalized_implications, - get_proof_string, - NormalizedImplication -} from './utils/implications' +import { get_contradiction_string, get_proof_string } from './utils/implications' import { type StructureType, STRUCTURE_TYPES_WITH_DUALS } from '$shared/config' import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures' +import { get_normalized_implications, NormalizedImplication } from '$shared/implications' /** * Returns the set of satisfied properties that can be deduced from a set diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index feabc9044..ad2f168cf 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -8,7 +8,7 @@ import { type StructureType } from '$shared/config' import { get_normalized_implications, type NormalizedImplication -} from './utils/implications' +} from '$shared/implications' import { get_structures } from './utils/structures' const db = get_client() diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index d02f3b4db..2d5f6a5a8 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -1,91 +1,7 @@ -import { type Database } from 'better-sqlite3' import type { PropertyMeta } from './properties' import { type StructureType } from '$shared/config' -import { parse_nested_json_set, parse_json_set } from '$shared/utils' import { get_property_label } from '$shared/property.utils' - -export type NormalizedImplication = { - id: string - assumptions: Set - conclusion: string - mapped_assumptions?: Partial>> -} - -/** - * Implications have the form - * P_1 + ... + P_n ===> Q_1 + ... + Q_m - * or - * P_1 + ... + P_n <===> Q_1 + ... + Q_m. - * This function decomposes them into normalized implications, - * which have the form - * P_1 + ... + P_n ===> Q. - */ -export function get_normalized_implications( - db: Database, - type: StructureType -): NormalizedImplication[] { - const implications_db = db - .prepare< - [StructureType], - { - id: string - is_equivalence: 0 | 1 - assumptions: string - conclusions: string - mapped_assumptions: string - } - >( - `SELECT - id, - is_equivalence, - assumptions, - conclusions, - mapped_assumptions - FROM implications_view - WHERE type = ?` - ) - .all(type) - - const implications: NormalizedImplication[] = [] - - for (const impl of implications_db) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) - - for (const conclusion of conclusions) { - const implication: NormalizedImplication = { - id: impl.id, - assumptions, - conclusion - } - - if (Object.keys(mapped_assumptions).length > 0) { - implication.mapped_assumptions = mapped_assumptions - } - - implications.push(implication) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - const implication: NormalizedImplication = { - id: impl.id, - assumptions: conclusions, - conclusion: assumption - } - - if (Object.keys(mapped_assumptions).length > 0) { - implication.mapped_assumptions = mapped_assumptions - } - - implications.push(implication) - } - } - } - - return implications -} +import { type NormalizedImplication } from '$shared/implications' function get_assumption_string( implication: NormalizedImplication, diff --git a/shared/implications.ts b/shared/implications.ts new file mode 100644 index 000000000..2347b9d15 --- /dev/null +++ b/shared/implications.ts @@ -0,0 +1,88 @@ +import { type Database } from 'better-sqlite3' +import { type StructureType } from './config' +import { parse_json_set, parse_nested_json_set } from './utils' + +export type NormalizedImplication = { + id: string + assumptions: Set + conclusion: string + mapped_assumptions?: Partial>> +} + +/** + * Implications have the form + * P_1 + ... + P_n ===> Q_1 + ... + Q_m + * or + * P_1 + ... + P_n <===> Q_1 + ... + Q_m. + * This function decomposes them into normalized implications, + * which have the form + * P_1 + ... + P_n ===> Q. + */ +export function get_normalized_implications( + db: Database, + type: StructureType +): NormalizedImplication[] { + const implications_db = db + .prepare< + [StructureType], + { + id: string + is_equivalence: 0 | 1 + assumptions: string + conclusions: string + mapped_assumptions: string + } + >( + `SELECT + id, + is_equivalence, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE type = ?` + ) + .all(type) + + const implications: NormalizedImplication[] = [] + + for (const impl of implications_db) { + const assumptions = parse_json_set(impl.assumptions) + const conclusions = parse_json_set(impl.conclusions) + const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) + + const has_mapped_assumptions = Object.keys(mapped_assumptions).length > 0 + + for (const conclusion of conclusions) { + const implication: NormalizedImplication = { + id: impl.id, + assumptions, + conclusion + } + + if (has_mapped_assumptions) { + implication.mapped_assumptions = mapped_assumptions + } + + implications.push(implication) + } + + if (impl.is_equivalence) { + for (const assumption of assumptions) { + const implication: NormalizedImplication = { + id: impl.id, + assumptions: conclusions, + conclusion: assumption + } + + if (has_mapped_assumptions) { + implication.mapped_assumptions = mapped_assumptions + } + + implications.push(implication) + } + } + } + + return implications +} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 1c67c6ac0..53bc336b7 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -101,12 +101,6 @@ export type ImplicationDisplay = Replace< } > -export type NormalizedImplication = { - id: string - assumptions: Set - conclusion: string -} - export type SearchResults = { contradiction: string[] | null satisfied_properties: string[] diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index 69f28f9fc..ed7e9e43e 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -1,7 +1,11 @@ import { is_subset } from '$shared/utils' import type { SqliteError } from 'better-sqlite3' -import type { NormalizedImplication, StructureType } from '$lib/commons/types' -import { get_normalized_implications } from './fetchers/implications' +import type { StructureType } from '$lib/commons/types' +import { + get_normalized_implications, + type NormalizedImplication +} from '$shared/implications' +import { db } from './db.catdat' // TODO: If possible, remove the code duplication with deduction and redundancy scripts. @@ -15,9 +19,9 @@ export function get_contradiction( if (unsatisfied_properties.has(p)) return { contradiction, err: null } } - const { implications, err } = get_normalized_implications(type) - - if (err) return { contradiction: null, err } + const implications = get_normalized_implications(db, type).filter( + (impl) => !impl.mapped_assumptions + ) const contradiction = contradiction_worker( satisfied_properties, diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts index a280844d4..54e52a8ba 100644 --- a/src/lib/server/fetchers/implications.ts +++ b/src/lib/server/fetchers/implications.ts @@ -1,13 +1,8 @@ import { query } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import { error } from '@sveltejs/kit' -import type { - ImplicationDB, - NormalizedImplication, - StructureType -} from '$lib/commons/types' +import type { ImplicationDB, StructureType } from '$lib/commons/types' import { display_implication } from '$lib/server/transforms' -import { parse_json_set, parse_nested_json_set } from '$shared/utils' export function fetch_implications(type: StructureType) { const { rows, err } = query(sql` @@ -31,60 +26,3 @@ export function fetch_implications(type: StructureType) { return { type, implications } } - -/** - * List of normalized implications of a given type that have no mapped assumptions - * (e.g. no source and no target assumptions in the case of functors), - * i.e. those that are universally true. Only those are relevant - * for the consistency check. - */ -export function get_normalized_implications(type: StructureType) { - // TODO: remove duplication with deduction script - - const { rows, err } = query<{ - id: string - is_equivalence: 0 | 1 - assumptions: string - mapped_assumptions: string - conclusions: string - }>( - sql` - SELECT - id, - is_equivalence, - assumptions, - conclusions, - mapped_assumptions - FROM implications_view - WHERE type = ${type} - ` - ) - - if (err) return { implications: null, err } - - const implications: NormalizedImplication[] = [] - - for (const impl of rows) { - const assumptions = parse_json_set(impl.assumptions) - const conclusions = parse_json_set(impl.conclusions) - const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) - - if (Object.values(mapped_assumptions).some((list) => list?.size)) continue - - for (const conclusion of conclusions) { - implications.push({ id: impl.id, assumptions, conclusion }) - } - - if (impl.is_equivalence) { - for (const assumption of assumptions) { - implications.push({ - id: impl.id, - assumptions: conclusions, - conclusion: assumption - }) - } - } - } - - return { implications, err: null } -} diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index 9a67bc7bf..d023fd0f3 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -1,9 +1,9 @@ -import { batch } from '$lib/server/db.catdat' +import { batch, db } from '$lib/server/db.catdat' import sql from 'sql-template-tag' import type { StructureShort, StructureType } from '$lib/commons/types' import { error } from '@sveltejs/kit' import { contradiction_worker } from '$lib/server/consistency' -import { get_normalized_implications } from './implications' +import { get_normalized_implications } from '$shared/implications' export function fetch_missing_data(type: StructureType) { const { results, err } = batch< @@ -87,9 +87,9 @@ export function fetch_missing_data(type: StructureType) { 0 ) - const { implications, err: err_imp } = get_normalized_implications(type) - - if (err_imp) error(500, 'Failed to load data') + const implications = get_normalized_implications(db, type).filter( + (impl) => !impl.mapped_assumptions + ) const witnessed_pairs_set = new Set(witnessed_pairs.map(({ p, q }) => `${p}|${q}`)) From 8f594eb9816f9fbbd221c9c044f35f1b76023f64 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Jul 2026 22:59:43 +0200 Subject: [PATCH 07/17] move `get_client` helper from /databases to /shared --- databases/catdat/scripts/deduce-implications.ts | 4 ++-- databases/catdat/scripts/deduce-special-morphisms.ts | 4 ++-- databases/catdat/scripts/deduce-special-objects.ts | 4 ++-- .../catdat/scripts/deduce-structure-properties.ts | 4 ++-- databases/catdat/scripts/proof-length.ts | 5 +++-- databases/catdat/scripts/redundancies.ts | 6 +++--- .../catdat/scripts/restrict-functor-properties.ts | 4 ++-- databases/catdat/scripts/seed.ts | 4 ++-- databases/catdat/scripts/setup.ts | 4 ++-- databases/catdat/scripts/test.ts | 4 ++-- databases/catdat/scripts/utils/db.ts | 9 --------- shared/db.ts | 10 ++++++++++ 12 files changed, 32 insertions(+), 30 deletions(-) delete mode 100644 databases/catdat/scripts/utils/db.ts create mode 100644 shared/db.ts diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts index 117cc4655..a74438f44 100644 --- a/databases/catdat/scripts/deduce-implications.ts +++ b/databases/catdat/scripts/deduce-implications.ts @@ -1,8 +1,8 @@ import { type StructureType, STRUCTURE_TYPES_WITH_DUALS } from '$shared/config' import { are_equal_sets, parse_nested_json_set, parse_json_set } from '$shared/utils' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' -const db = get_client() +const db = get_client({ readonly: false }) /** * Clears all deduced implications. This is done before the deduction starts. diff --git a/databases/catdat/scripts/deduce-special-morphisms.ts b/databases/catdat/scripts/deduce-special-morphisms.ts index b3bcf14e8..1eadedbd5 100644 --- a/databases/catdat/scripts/deduce-special-morphisms.ts +++ b/databases/catdat/scripts/deduce-special-morphisms.ts @@ -1,6 +1,6 @@ -import { get_client } from './utils/db' +import { get_client } from '$shared/db' -const db = get_client() +const db = get_client({ readonly: false }) // TODO: deduce further morphisms, // e.g. isomorphisms = bijective morphisms in algebraic categories, diff --git a/databases/catdat/scripts/deduce-special-objects.ts b/databases/catdat/scripts/deduce-special-objects.ts index c944a3b49..50fce1809 100644 --- a/databases/catdat/scripts/deduce-special-objects.ts +++ b/databases/catdat/scripts/deduce-special-objects.ts @@ -1,6 +1,6 @@ -import { get_client } from './utils/db' +import { get_client } from '$shared/db' -const db = get_client() +const db = get_client({ readonly: false }) export function deduce_special_objects() { console.info('\n--- Deduce special objects ---') diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index a8950770a..fba2f34c8 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -5,7 +5,7 @@ import { type Database, SqliteError } from 'better-sqlite3' import { is_subset } from '$shared/utils' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' import { get_properties_dict, get_property_assignments, @@ -388,7 +388,7 @@ function delete_deduced_properties(db: Database, type: StructureType) { export function deduce_properties_for_structures(type: StructureType) { console.info(`\n--- Deduce ${type} properties ---`) - const db = get_client() + const db = get_client({ readonly: false }) delete_deduced_properties(db, type) diff --git a/databases/catdat/scripts/proof-length.ts b/databases/catdat/scripts/proof-length.ts index e4176f911..ebfde75c5 100644 --- a/databases/catdat/scripts/proof-length.ts +++ b/databases/catdat/scripts/proof-length.ts @@ -1,7 +1,8 @@ import { STRUCTURE_TYPES, type StructureType } from '$shared/config' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' +get_client -const db = get_client() +const db = get_client({ readonly: true }) const PROOF_LENGTH_THRESHOLD = 1200 diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index ad2f168cf..3c615a753 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -1,17 +1,17 @@ -import { get_client } from './utils/db' +import { get_client } from '$shared/db' import { get_deduced_satisfied_properties, get_deduced_unsatisfied_properties } from './deduce-structure-properties' import { get_property_assignments_by_deduction } from './utils/properties' -import { type StructureType } from '$shared/config' +import { STRUCTURE_TYPES, type StructureType } from '$shared/config' import { get_normalized_implications, type NormalizedImplication } from '$shared/implications' import { get_structures } from './utils/structures' -const db = get_client() +const db = get_client({ readonly: true }) check_redundancies() diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index c7af74cb2..d246a3f84 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -1,6 +1,6 @@ -import { get_client } from './utils/db' +import { get_client } from '$shared/db' -const db = get_client() +const db = get_client({ readonly: false }) /** * Ensures that only functors with target Set are representable. diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index db15ef8ff..fe25f8e8d 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -1,6 +1,6 @@ import path from 'node:path' import { seed_file, seed_files } from './utils/seed.helpers' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' import type { CategoryYaml, ConfigYaml, @@ -14,7 +14,7 @@ import type { import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' -const db = get_client() +const db = get_client({ readonly: false }) const data_folder = path.resolve('databases', 'catdat', 'data') diff --git a/databases/catdat/scripts/setup.ts b/databases/catdat/scripts/setup.ts index f70c93a2d..62bbbf0ee 100644 --- a/databases/catdat/scripts/setup.ts +++ b/databases/catdat/scripts/setup.ts @@ -1,6 +1,6 @@ import fs from 'node:fs' import path from 'node:path' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' import { create_schema_hash, write_schema_hash } from './utils/schema' const schema_folder = path.resolve('databases', 'catdat', 'schema') @@ -13,7 +13,7 @@ setup() function setup() { console.info('\n--- Setup CatDat database ---') - const db = get_client() + const db = get_client({ readonly: false }) const files = fs .readdirSync(schema_folder, 'utf8') diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index 790f200b6..472379a72 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -13,13 +13,13 @@ import decided_categories from './expected-data/decided-categories.json' import decided_functors from './expected-data/decided-functors.json' import decided_morphisms from './expected-data/decided-morphisms.json' import { capitalize } from '$shared/utils' -import { get_client } from './utils/db' +import { get_client } from '$shared/db' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' import fs from 'node:fs' import path from 'node:path' import { decode_property_ID } from '$shared/property.utils' -const db = get_client() +const db = get_client({ readonly: true }) execute_tests() diff --git a/databases/catdat/scripts/utils/db.ts b/databases/catdat/scripts/utils/db.ts deleted file mode 100644 index a2b477874..000000000 --- a/databases/catdat/scripts/utils/db.ts +++ /dev/null @@ -1,9 +0,0 @@ -import Database from 'better-sqlite3' -import path from 'node:path' - -export function get_client() { - const db_path = path.resolve('databases', 'catdat', 'catdat.db') - const db = new Database(db_path, { readonly: false }) - db.pragma('foreign_keys = ON') - return db -} diff --git a/shared/db.ts b/shared/db.ts new file mode 100644 index 000000000..19cf92365 --- /dev/null +++ b/shared/db.ts @@ -0,0 +1,10 @@ +import Database from 'better-sqlite3' +import path from 'node:path' + +const db_path = path.resolve('databases', 'catdat', 'catdat.db') + +export function get_client(options: { readonly: boolean }) { + const db = new Database(db_path, options) + db.pragma('foreign_keys = ON') + return db +} From d06f66b350fd5bd1edf0f37c977c7d698fed6714 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Jul 2026 23:46:49 +0200 Subject: [PATCH 08/17] create client in Svelte app using `get_client` from shared folder --- src/lib/server/db.catdat.ts | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/lib/server/db.catdat.ts b/src/lib/server/db.catdat.ts index b936667ec..c795e4fd5 100644 --- a/src/lib/server/db.catdat.ts +++ b/src/lib/server/db.catdat.ts @@ -1,17 +1,17 @@ import type { Arrayed } from '$lib/commons/types' -import Database, { type SqliteError } from 'better-sqlite3' -import path from 'node:path' +import { type SqliteError } from 'better-sqlite3' -const db_path = path.resolve('databases', 'catdat', 'catdat.db') +import { get_client } from '$shared/db' /** * Database client for the CatDat database holding all mathematical knowledge */ -const db = new Database(db_path, { readonly: true, fileMustExist: true }) +export const db = get_client({ readonly: true }) /** * Small wrapper around db.prepare.all to handle errors, * use sql templates, and specify the type of the result. + * @deprecated */ export function query({ sql, values = [] }: { sql: string; values?: any[] }) { try { @@ -26,6 +26,7 @@ export function query({ sql, values = [] }: { sql: string; values?: any[] }) /** * Small wrapper around db.transaction to handle errors * use sql templates, and specify the type of the result. + * @deprecated */ export function batch(queries: { sql: string; values?: any[] }[]) { try { From bfe38b2d7bdce0bba01e601e1692bdc5d688fffd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 8 Jul 2026 23:47:44 +0200 Subject: [PATCH 09/17] use db.prepare for fetching data in Svelte app --- shared/config.ts | 2 +- shared/utils.ts | 2 +- src/lib/commons/types.ts | 7 +- src/lib/server/consistency.ts | 9 +- src/lib/server/db.catdat.ts | 50 -------- src/lib/server/db.ts | 6 + src/lib/server/fetchers/category.ts | 106 +++++++++-------- src/lib/server/fetchers/comparison.ts | 97 +++++++--------- src/lib/server/fetchers/content.ts | 54 ++++----- src/lib/server/fetchers/functor.ts | 22 ++-- src/lib/server/fetchers/implication.ts | 50 ++++---- src/lib/server/fetchers/implications.ts | 38 +++--- src/lib/server/fetchers/missing_data.ts | 104 ++++++++--------- src/lib/server/fetchers/morphism.ts | 22 ++-- src/lib/server/fetchers/properties.ts | 84 ++++++-------- src/lib/server/fetchers/property.ts | 147 +++++++++++------------- src/lib/server/fetchers/search.ts | 55 ++++----- src/lib/server/fetchers/structure.ts | 142 ++++++++++------------- src/lib/server/fetchers/structures.ts | 79 ++++++------- src/lib/server/fetchers/tags.ts | 29 +++-- 20 files changed, 482 insertions(+), 623 deletions(-) delete mode 100644 src/lib/server/db.catdat.ts create mode 100644 src/lib/server/db.ts diff --git a/shared/config.ts b/shared/config.ts index b2792f0fb..9e4a2311f 100644 --- a/shared/config.ts +++ b/shared/config.ts @@ -11,5 +11,5 @@ export const STRUCTURE_TYPES_WITH_DUALS: StructureType[] = ['category'] export const PLURALS: Record = { category: 'categories', functor: 'functors', - morphism: 'morphisms', + morphism: 'morphisms' } diff --git a/shared/utils.ts b/shared/utils.ts index fe4a3eaac..020592a23 100644 --- a/shared/utils.ts +++ b/shared/utils.ts @@ -52,7 +52,7 @@ export function parse_nested_json_set(json: string): Partial '?').join(', ') + return `(${arr.map(() => '?').join(', ')})` } export function strip_math(s: string) { diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 53bc336b7..3745873f0 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -28,8 +28,6 @@ export type StructureDisplay = { export type MappedTypes = Record -export type TagObject = { tag: string } - export type CommentObject = { id: number; comment: string } export type PropertyDB = { @@ -68,6 +66,11 @@ export type PropertyAssignmentDisplay = { is_deduced: boolean } +export type CategoryDefinition = { + objects: string + morphisms: string +} + export type SpecialObject = { type: string description: string diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index ed7e9e43e..a99772cc7 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -1,11 +1,10 @@ import { is_subset } from '$shared/utils' -import type { SqliteError } from 'better-sqlite3' import type { StructureType } from '$lib/commons/types' import { get_normalized_implications, type NormalizedImplication } from '$shared/implications' -import { db } from './db.catdat' +import { db } from './db' // TODO: If possible, remove the code duplication with deduction and redundancy scripts. @@ -13,10 +12,10 @@ export function get_contradiction( satisfied_properties: Set, unsatisfied_properties: Set, type: StructureType -): { contradiction: string[] | null; err: SqliteError | null } { +): { contradiction: string[] | null } { for (const p of satisfied_properties) { const contradiction = [`${p} ⟹ ${p}`] - if (unsatisfied_properties.has(p)) return { contradiction, err: null } + if (unsatisfied_properties.has(p)) return { contradiction } } const implications = get_normalized_implications(db, type).filter( @@ -29,7 +28,7 @@ export function get_contradiction( implications ) - return { contradiction, err: null } + return { contradiction } } export function contradiction_worker( diff --git a/src/lib/server/db.catdat.ts b/src/lib/server/db.catdat.ts deleted file mode 100644 index c795e4fd5..000000000 --- a/src/lib/server/db.catdat.ts +++ /dev/null @@ -1,50 +0,0 @@ -import type { Arrayed } from '$lib/commons/types' -import { type SqliteError } from 'better-sqlite3' - -import { get_client } from '$shared/db' - -/** - * Database client for the CatDat database holding all mathematical knowledge - */ -export const db = get_client({ readonly: true }) - -/** - * Small wrapper around db.prepare.all to handle errors, - * use sql templates, and specify the type of the result. - * @deprecated - */ -export function query({ sql, values = [] }: { sql: string; values?: any[] }) { - try { - const rows = db.prepare(sql).all(...values) - return { rows, err: null } - } catch (err) { - console.error(err) - return { rows: null, err: err as SqliteError } - } -} - -/** - * Small wrapper around db.transaction to handle errors - * use sql templates, and specify the type of the result. - * @deprecated - */ -export function batch(queries: { sql: string; values?: any[] }[]) { - try { - const run_batch = db.transaction(() => { - const results = [] - - for (const { sql, values = [] } of queries) { - const result = db.prepare(sql).all(...values) - results.push(result) - } - - return results - }) - - const results = run_batch() as Arrayed - return { results, err: null } - } catch (err) { - console.error(err) - return { rows: null, err: err as SqliteError } - } -} diff --git a/src/lib/server/db.ts b/src/lib/server/db.ts new file mode 100644 index 000000000..878e0c097 --- /dev/null +++ b/src/lib/server/db.ts @@ -0,0 +1,6 @@ +import { get_client } from '$shared/db' + +/** + * Database client for the CatDat database holding all mathematical knowledge + */ +export const db = get_client({ readonly: true }) diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index 170baf9ed..edfdf13a0 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -1,58 +1,57 @@ -import type { SpecialMorphism, SpecialObject, StructureShort } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { batch, query } from '$lib/server/db.catdat' +import type { + CategoryDefinition, + SpecialMorphism, + SpecialObject, + StructureShort +} from '$lib/commons/types' +import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_category(id: string) { - const { results, err } = batch< - [ - { objects: string; morphisms: string }, - SpecialObject, - SpecialMorphism, - StructureShort - ] - >([ - // specific information for the category - sql` - SELECT c.objects, c.morphisms + const category = db + .prepare<[string], CategoryDefinition>( + `SELECT c.objects, c.morphisms FROM categories c - WHERE c.id = ${id} - `, - // special objects - sql` - SELECT s.type, s.description + WHERE c.id = ?` + ) + .get(id) + + if (!category) error(404, `Could not find category with ID '${id}'`) + + const special_objects = db + .prepare<[string], SpecialObject>( + `SELECT s.type, s.description FROM special_objects s - INNER JOIN special_object_types t ON t.type = s.type - WHERE s.category_id = ${id} - ORDER BY t.id - `, - // special morphisms - sql` - SELECT t.type, s.description, s.proof + INNER JOIN special_object_types t + ON t.type = s.type + WHERE s.category_id = ? + ORDER BY t.id` + ) + .all(id) + + const special_morphisms = db + .prepare<[string], SpecialMorphism>( + `SELECT t.type, s.description, s.proof FROM special_morphism_types t LEFT JOIN special_morphisms s - ON s.type = t.type AND s.category_id = ${id} - ORDER BY t.id - `, - // functors whose source or target is the current category - sql` - SELECT f.id, s.name + ON s.type = t.type AND s.category_id = ? + ORDER BY t.id` + ) + .all(id) + + const functors = db + .prepare<[string, string], StructureShort>( + `SELECT f.id, s.name FROM functors f INNER JOIN structures s ON s.id = f.id - WHERE f.source = ${id} OR f.target = ${id} - ORDER BY lower(s.name) - ` - ]) - - if (err) error(500, 'Could not load category') - - const [categories, special_objects, special_morphisms, functors] = results - - if (!categories.length) error(404, `Could not find category with ID '${id}'`) + WHERE f.source = ? OR f.target = ? + ORDER BY lower(s.name)` + ) + .all(id, id) return { type: 'category' as const, - ...categories[0], + ...category, special_objects, special_morphisms, functors @@ -60,20 +59,19 @@ export function fetch_category(id: string) { } export function fetch_categories_with_missing_morphisms() { - const { rows, err } = query( - sql` - SELECT s.id, s.name, COUNT(*) AS count + return db + .prepare( + `SELECT + s.id, + s.name, + COUNT(*) AS count FROM structures s JOIN special_morphism_types t LEFT JOIN special_morphisms m - ON m.category_id = s.id AND m.type = t.type + ON m.category_id = s.id AND m.type = t.type WHERE s.type = 'category' AND m.type IS NULL GROUP BY s.id - ORDER BY lower(s.name); - ` - ) - - if (err) error(500, 'Failed to load data') - - return rows + ORDER BY lower(s.name)` + ) + .all() } diff --git a/src/lib/server/fetchers/comparison.ts b/src/lib/server/fetchers/comparison.ts index 05a6ecbde..3c5f674e1 100644 --- a/src/lib/server/fetchers/comparison.ts +++ b/src/lib/server/fetchers/comparison.ts @@ -1,5 +1,5 @@ import { error } from '@sveltejs/kit' -import { query } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { render_nested_formulas } from '$lib/server/formulas' import { MAX_STRUCTURES_COMPARE } from '$lib/commons/compare.utils' import type { ComparisonResult, StructureType } from '$lib/commons/types' @@ -20,69 +20,30 @@ export function fetch_comparison_result( ) } - const { rows, err: err_cat } = query<{ - id: string - name: string - notation: string - }>({ - sql: ` - SELECT id, name, notation + const unsorted_structures = db + .prepare( + `SELECT id, name, notation FROM structures WHERE type = ? - AND id in (${to_placeholders(compared_ids)})`, - values: [type, ...compared_ids] - }) - - if (err_cat) error(500, `Could not load ${PLURALS[type]}`) + AND id in ${to_placeholders(compared_ids)}` + ) + .all(type, ...compared_ids) - const invalid_id = compared_ids.find((id) => rows.every((row) => row.id !== id)) + const invalid_id = compared_ids.find((id) => + unsorted_structures.every((row) => row.id !== id) + ) if (invalid_id) error(404, `Could not find ${type} with ID '${invalid_id}'`) - const structures = rows.sort( + const structures = unsorted_structures.sort( (a, b) => compared_ids.indexOf(a.id) - compared_ids.indexOf(b.id) ) - const select_columns = compared_ids - .map( - (_, i) => - `CASE - WHEN a${i}.is_satisfied = TRUE THEN 'yes' - WHEN a${i}.is_satisfied = FALSE THEN 'no' - ELSE 'unknown' - END AS struct${i}` - ) - .join(',\n') - - const join_fragments: string[] = [] - const values: string[] = [] - - compared_ids.forEach((id, i) => { - join_fragments.push(` - LEFT JOIN property_assignments a${i} - ON a${i}.property_id = p.id AND a${i}.structure_id = ? - `) - values.push(id) - }) - - values.push(type) - - const comparison_query = ` - SELECT - p.id AS property_id, - ${select_columns} - FROM properties p - ${join_fragments.join('\n')} - WHERE p.type = ? - ORDER BY lower(p.id)` - - const { rows: comparison_objects, err } = query>({ - sql: comparison_query, - values - }) - - if (err) error(500, 'Could not load comparison table') + const comparison_query = get_comparison_query(compared_ids) - const comparison_table = comparison_objects.map((obj) => Object.values(obj)) + const comparison_table = db + .prepare(comparison_query) + .raw() + .all(...compared_ids, type) callback() @@ -92,3 +53,29 @@ export function fetch_comparison_result( type } } + +function get_comparison_query(compared_ids: string[]) { + const columns = compared_ids.map( + (_, i) => + `CASE + WHEN a${i}.is_satisfied = TRUE THEN 'yes' + WHEN a${i}.is_satisfied = FALSE THEN 'no' + ELSE 'unknown' + END AS struct${i}` + ) + + const joins = compared_ids.map( + (_, i) => + `LEFT JOIN property_assignments a${i} + ON a${i}.property_id = p.id AND a${i}.structure_id = ?` + ) + + return ` + SELECT + p.id AS property_id, + ${columns.join(',\n')} + FROM properties p + ${joins.join('\n')} + WHERE p.type = ? + ORDER BY lower(p.id)` +} diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index b235f4206..5b233684a 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -1,38 +1,32 @@ import type { PropertyShort, StructureShort } from '$lib/commons/types' -import { batch } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' +import { db } from '$lib/server/db' export function fetch_category_references(content_id: string) { - const { results, err: err_categories } = batch< - [StructureShort, PropertyShort, { id: string }] - >([ - sql` - SELECT DISTINCT s.id, s.name - FROM property_assignments pa - INNER JOIN structures s ON s.id = pa.structure_id - WHERE - pa.type = 'category' - AND pa.proof LIKE '%/content/' || ${content_id} || '%' - - `, - sql` - SELECT id, relation FROM properties - WHERE - type = 'category' - AND description LIKE '%/content/' || ${content_id} || '%' - `, - sql` - SELECT id FROM implications - WHERE - type = 'category' - AND proof LIKE '%/content/' || ${content_id} || '%' - ` - ]) + const categories = db + .prepare<[string], StructureShort>( + `SELECT DISTINCT s.id, s.name + FROM property_assignments pa + INNER JOIN structures s ON s.id = pa.structure_id + WHERE pa.type = 'category' + AND pa.proof LIKE '%/content/' || ? || '%'` + ) + .all(content_id) - if (err_categories) error(500, 'Could not load context') + const category_properties = db + .prepare<[string], PropertyShort>( + `SELECT id, relation FROM properties + WHERE type = 'category' + AND description LIKE '%/content/' || ? || '%'` + ) + .all(content_id) - const [categories, category_properties, category_implications] = results + const category_implications = db + .prepare<[string], { id: string }>( + `SELECT id FROM implications + WHERE type = 'category' + AND proof LIKE '%/content/' || ? || '%'` + ) + .all(content_id) return { categories, category_properties, category_implications } } diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts index 5e4705dec..448dc8d5f 100644 --- a/src/lib/server/fetchers/functor.ts +++ b/src/lib/server/fetchers/functor.ts @@ -1,13 +1,11 @@ import type { FunctorSpecificDisplay } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { query } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_functor(id: string) { - const { rows: functors, err } = query( - // specific information for the functor - sql` - SELECT + const functor = db + .prepare<[string], FunctorSpecificDisplay>( + `SELECT f.source, f.target, source.name AS source_name, @@ -26,13 +24,11 @@ export function fetch_functor(id: string) { LEFT JOIN structures AS la ON la.id = f.left_adjoint LEFT JOIN functors AS rf ON rf.left_adjoint = f.id LEFT JOIN structures AS ra ON ra.id = rf.id - WHERE f.id = ${id} - ` - ) + WHERE f.id = ?` + ) + .get(id) - if (err) error(500, 'Could not load functor') + if (!functor) error(404, `Could not find functor with ID '${id}'`) - if (!functors.length) error(404, `Could not find functor with ID '${id}'`) - - return { type: 'functor' as const, ...functors[0] } + return { type: 'functor' as const, ...functor } } diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index 36b7bd7eb..48e18cf8c 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -1,5 +1,4 @@ -import { batch } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' +import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' import type { ImplicationDB, @@ -10,11 +9,9 @@ import type { import { display_implication } from '$lib/server/transforms' export function fetch_implication(type: StructureType, id: string) { - const { results, err } = batch< - [ImplicationDB, StructureShort, { map: string; mapped_type: StructureType }] - >([ - sql` - SELECT + const implication_db = db + .prepare<[string], ImplicationDB>( + `SELECT id, is_equivalence, is_deduced, @@ -24,32 +21,33 @@ export function fetch_implication(type: StructureType, id: string) { conclusions, mapped_assumptions FROM implications_view - WHERE id = ${id} - `, - sql` - SELECT DISTINCT s.id, s.name + WHERE id = ?` + ) + .get(id) + + const structures = db + .prepare<[StructureType, string], StructureShort>( + `SELECT DISTINCT s.id, s.name FROM property_assignments pa INNER JOIN structures s ON s.id = pa.structure_id - WHERE - pa.type = ${type} - AND pa.proof LIKE '%/' || ${type} || '-implication/' || ${id} || '%' - `, - sql` - SELECT map, mapped_type + WHERE pa.type = ? + AND pa.proof LIKE '%/' || pa.type || '-implication/' || ? || '%'` + ) + .all(type, id) + + const structure_maps = db + .prepare<[StructureType], { map: string; mapped_type: StructureType }>( + `SELECT map, mapped_type FROM structure_maps - WHERE type = ${type} - ` - ]) - - if (err) error(500, 'Could not load implication') - - const [implications, structures, structure_maps] = results + WHERE type = ?` + ) + .all(type) - if (!implications.length) { + if (!implication_db) { error(404, `Could not find implication with ID '${id}'`) } - const implication = display_implication(implications[0]) + const implication = display_implication(implication_db) const mapped_types: MappedTypes = {} diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts index 54e52a8ba..42bdcb253 100644 --- a/src/lib/server/fetchers/implications.ts +++ b/src/lib/server/fetchers/implications.ts @@ -1,28 +1,26 @@ -import { query } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' -import { error } from '@sveltejs/kit' +import { db } from '$lib/server/db' import type { ImplicationDB, StructureType } from '$lib/commons/types' import { display_implication } from '$lib/server/transforms' export function fetch_implications(type: StructureType) { - const { rows, err } = query(sql` - SELECT - id, - is_equivalence, - is_deduced, - dualized_from, - proof, - assumptions, - conclusions, - mapped_assumptions - FROM implications_view - WHERE type = ${type} - ORDER BY lower(assumptions) || ' ' || lower(conclusions) - `) + const implications_db = db + .prepare<[StructureType], ImplicationDB>( + `SELECT + id, + is_equivalence, + is_deduced, + dualized_from, + proof, + assumptions, + conclusions, + mapped_assumptions + FROM implications_view + WHERE type = ? + ORDER BY lower(assumptions) || ' ' || lower(conclusions)` + ) + .all(type) - if (err) error(500, 'Could not load implications') - - const implications = rows.map(display_implication) + const implications = implications_db.map(display_implication) return { type, implications } } diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index d023fd0f3..0ead8d4ce 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -1,86 +1,76 @@ -import { batch, db } from '$lib/server/db.catdat' -import sql from 'sql-template-tag' +import { db } from '$lib/server/db' import type { StructureShort, StructureType } from '$lib/commons/types' -import { error } from '@sveltejs/kit' import { contradiction_worker } from '$lib/server/consistency' import { get_normalized_implications } from '$shared/implications' export function fetch_missing_data(type: StructureType) { - const { results, err } = batch< - [ - StructureShort & { count: number }, - { id1: string; name1: string; id2: string; name2: string }, - { id: string; dual_property_id: string | null }, - { p: string; q: string } - ] - >([ - // structures with unknown properties - sql` - SELECT s.id, s.name, COUNT(*) AS count + const structures_with_unknown_properties = db + .prepare<[StructureType], StructureShort & { count: number }>( + `SELECT + s.id, + s.name, + COUNT(*) AS count FROM structures s INNER JOIN properties p ON p.type = s.type LEFT JOIN property_assignments pa - ON pa.structure_id = s.id - AND pa.property_id = p.id - WHERE - s.type = ${type} - AND pa.property_id IS NULL + ON pa.structure_id = s.id AND pa.property_id = p.id + WHERE s.type = ? AND pa.property_id IS NULL GROUP BY s.id - ORDER BY lower(s.name); - `, - // undistinguishable structure pairs - sql` - SELECT + ORDER BY lower(s.name)` + ) + .all(type) + + const undistinguishable_structure_pairs = db + .prepare< + [StructureType], + { id1: string; name1: string; id2: string; name2: string } + >( + `SELECT s1.id AS id1, s1.name AS name1, s2.id AS id2, s2.name AS name2 FROM structures s1 JOIN structures s2 - ON s1.id < s2.id AND s2.type = s1.type + ON s1.id < s2.id AND s2.type = s1.type JOIN properties p ON p.type = s1.type LEFT JOIN property_assignments a1 - ON a1.structure_id = s1.id AND a1.property_id = p.id + ON a1.structure_id = s1.id AND a1.property_id = p.id LEFT JOIN property_assignments a2 - ON a2.structure_id = s2.id AND a2.property_id = p.id - WHERE s1.type = ${type} + ON a2.structure_id = s2.id AND a2.property_id = p.id + WHERE s1.type = ? GROUP BY s1.id, s1.name, s2.id, s2.name HAVING SUM( - CASE - WHEN a1.is_satisfied IS a2.is_satisfied THEN 0 - ELSE 1 - END - ) = 0; - `, - // properties - sql` - SELECT id, dual_property_id + CASE + WHEN a1.is_satisfied IS a2.is_satisfied THEN 0 + ELSE 1 + END + ) = 0` + ) + .all(type) + + const properties = db + .prepare<[StructureType], { id: string; dual_property_id: string | null }>( + `SELECT id, dual_property_id FROM properties - WHERE type = ${type} - ORDER BY lower(id) - `, - // witnessed property combinations of the form "p and not q" - sql` - SELECT DISTINCT + WHERE type = ? + ORDER BY lower(id)` + ) + .all(type) + + const witnessed_pairs = db + .prepare<[StructureType], { p: string; q: string }>( + `SELECT DISTINCT a.property_id AS p, an.property_id AS q FROM property_assignments a INNER JOIN property_assignments an ON a.structure_id = an.structure_id WHERE - a.type = ${type} - AND an.type = ${type} + a.type = ? + AND an.type = a.type AND a.is_satisfied = TRUE - AND an.is_satisfied = FALSE - ` - ]) - - if (err) error(500, 'Failed to load data') - - const [ - structures_with_unknown_properties, - undistinguishable_structure_pairs, - properties, - witnessed_pairs - ] = results + AND an.is_satisfied = FALSE` + ) + .all(type) const total_unknown_property_pairs = structures_with_unknown_properties.reduce( (total, item) => item.count + total, diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts index 4fdc5e7fe..8aacbf9a8 100644 --- a/src/lib/server/fetchers/morphism.ts +++ b/src/lib/server/fetchers/morphism.ts @@ -1,25 +1,21 @@ import type { MorphismSpecificDisplay } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { query } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_morphism(id: string) { - const { rows: morphisms, err } = query( - // specific information for the morphism - sql` - SELECT + const morphism = db + .prepare<[string], MorphismSpecificDisplay>( + `SELECT c.id AS category, c.name AS category_name, c.notation AS category_notation FROM morphisms m INNER JOIN structures AS c ON c.id = m.category - WHERE m.id = ${id} - ` - ) + WHERE m.id = ?` + ) + .get(id) - if (err) error(500, 'Could not load morphism') + if (!morphism) error(404, `Could not find morphism with ID '${id}'`) - if (!morphisms.length) error(404, `Could not find morphism with ID '${id}'`) - - return { type: 'morphism' as const, ...morphisms[0] } + return { type: 'morphism' as const, ...morphism } } diff --git a/src/lib/server/fetchers/properties.ts b/src/lib/server/fetchers/properties.ts index ee31927b5..442751e8a 100644 --- a/src/lib/server/fetchers/properties.ts +++ b/src/lib/server/fetchers/properties.ts @@ -1,52 +1,44 @@ import type { GroupedPropertyShort, PropertyShort, - StructureType, - TagObject + StructureType } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { query, batch } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' +import { db } from '$lib/server/db' export function get_property_ids(type: StructureType) { - const { rows, err } = query<{ id: string }>( - sql` - SELECT id FROM properties - WHERE type = ${type} - ORDER BY lower(id) - ` - ) - - if (err) error(500, 'Failed to load properties') - - return rows.map(({ id }) => id) + return db + .prepare<[StructureType], string>( + `SELECT id FROM properties + WHERE type = ? + ORDER BY lower(id)` + ) + .pluck() + .all(type) } export function fetch_grouped_properties_and_tags(type: StructureType) { - const { results, err } = batch<[GroupedPropertyShort, TagObject]>([ - sql` - SELECT id, relation, dual_property_id - FROM properties - WHERE type = ${type} - ORDER BY lower(id) - `, - sql` - SELECT t.tag + const properties = db + .prepare<[StructureType], GroupedPropertyShort>( + `SELECT id, relation, dual_property_id + FROM properties + WHERE type = ? + ORDER BY lower(id)` + ) + .all(type) + + const tags = db + .prepare<[StructureType], string>( + `SELECT t.tag FROM property_tags t - WHERE t.type = ${type} + WHERE t.type = ? AND EXISTS ( SELECT 1 FROM property_tag_assignments a - WHERE a.tag = t.tag AND a.type = ${type} + WHERE a.tag = t.tag AND a.type = t.type ) - ORDER BY t.id - ` - ]) - - if (err) error(500, 'Failed to load properties') - - const [properties, tag_objects] = results - - const tags = tag_objects.map(({ tag }) => tag) + ORDER BY t.id` + ) + .pluck() + .all(type) const seen = new Set() @@ -79,16 +71,16 @@ export function fetch_grouped_properties_and_tags(type: StructureType) { } export function fetch_tagged_properties(type: StructureType, tag: string) { - const { rows: properties, err } = query(sql` - SELECT p.id, p.relation - FROM property_tag_assignments t - INNER JOIN properties p - ON p.id = t.property_id AND p.type = ${type} - WHERE t.tag = ${tag} AND t.type = ${type} - ORDER BY lower(id) - `) - - if (err) error(500, `Properties could not be loaded`) + const properties = db + .prepare<[StructureType, string], PropertyShort>( + `SELECT p.id, p.relation + FROM property_tag_assignments t + INNER JOIN properties p + ON p.id = t.property_id AND p.type = ? + WHERE t.tag = ? AND t.type = p.type + ORDER BY lower(id)` + ) + .all(type, tag) return { type, properties, tag } } diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts index e4d5244d2..90b391f71 100644 --- a/src/lib/server/fetchers/property.ts +++ b/src/lib/server/fetchers/property.ts @@ -2,28 +2,16 @@ import type { ImplicationDB, StructureShort, PropertyDB, - StructureType, - TagObject + StructureType } from '$lib/commons/types' -import { batch } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { display_implication, display_property } from '$lib/server/transforms' import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' export function fetch_property(type: StructureType, id: string) { - const { results, err } = batch< - [ - PropertyDB, - { id: string }, - TagObject, - ImplicationDB, - StructureShort & { is_satisfied: 0 | 1 | null }, - StructureShort - ] - >([ - // basic information - sql` - SELECT + const property_db = db + .prepare<[string, StructureType], PropertyDB>( + `SELECT id, relation, description, @@ -31,27 +19,41 @@ export function fetch_property(type: StructureType, id: string) { nlab_link, invariant_under_equivalences FROM properties - WHERE id = ${id} AND type = ${type} - `, - // related properties - sql` - SELECT related_property_id AS id + WHERE id = ? AND type = ?` + ) + .get(id, type) + + if (!property_db) { + error(404, `Could not find ${type} property with ID '${id}'`) + } + + const property = display_property(property_db) + + const related_properties = db + .prepare<[string, StructureType], string>( + `SELECT related_property_id AS id FROM related_properties - WHERE property_id = ${id} AND type = ${type} - ORDER BY lower(id) - `, - // tags - sql` - SELECT pt.tag + WHERE property_id = ? AND type = ? + ORDER BY lower(id)` + ) + .pluck() + .all(id, type) + + const tags = db + .prepare<[StructureType, string], string>( + `SELECT pt.tag FROM property_tag_assignments pt INNER JOIN property_tags t - ON t.tag = pt.tag AND t.type = ${type} - WHERE pt.property_id = ${id} AND pt.type = ${type} - ORDER BY t.id - `, - // relevant implications - sql` - SELECT + ON t.tag = pt.tag AND t.type = ? + WHERE pt.property_id = ? AND pt.type = t.type + ORDER BY t.id` + ) + .pluck() + .all(type, id) + + const relevant_implications_db = db + .prepare( + `SELECT id, is_equivalence, is_deduced, @@ -61,73 +63,54 @@ export function fetch_property(type: StructureType, id: string) { conclusions, mapped_assumptions FROM implications_view - WHERE type = ${type} + WHERE type = ? AND ( EXISTS ( SELECT 1 FROM json_each(conclusions) - WHERE value = ${id} + WHERE value = ? ) OR EXISTS ( SELECT 1 FROM json_each(assumptions) - WHERE value = ${id} + WHERE value = ? ) ) - ORDER BY lower(assumptions) || ' ' || lower(conclusions) - `, - // known structures - sql` - SELECT s.id, s.name, pa.is_satisfied + ORDER BY lower(assumptions) || ' ' || lower(conclusions)` + ) + .all(type, id, id) + + const relevant_implications = relevant_implications_db.map(display_implication) + + const known_structures = db + .prepare< + [StructureType, string], + StructureShort & { is_satisfied: 0 | 1 | null } + >( + `SELECT s.id, s.name, pa.is_satisfied FROM property_assignments pa INNER JOIN structures s ON s.id = pa.structure_id - WHERE - s.type = ${type} - AND pa.property_id = ${id} - ORDER BY lower(s.name) - `, - // unknown structures - sql` - SELECT s.id, s.name + WHERE s.type = ? AND pa.property_id = ? + ORDER BY lower(s.name)` + ) + .all(type, id) + + const unknown_structures = db + .prepare<[string, StructureType], StructureShort>( + `SELECT s.id, s.name FROM structures s LEFT JOIN property_assignments pa - ON pa.structure_id = s.id - AND pa.property_id = ${id} - WHERE - s.type = ${type} - AND pa.property_id IS NULL - ORDER BY lower(s.name) - ` - ]) - - if (err) error(500, 'Could not load property') - - const [ - properties, - related, - tag_objects, - relevant_implications_db, - known_structures, - unknown_structures - ] = results - - if (!properties.length) { - error(404, `Could not find property with ID '${id}'`) - } - - const property = display_property(properties[0]) - - const related_properties = related.map(({ id }) => id) - - const tags = tag_objects.map(({ tag }) => tag) + ON pa.structure_id = s.id AND pa.property_id = ? + WHERE s.type = ? AND pa.property_id IS NULL + ORDER BY lower(s.name)` + ) + .all(id, type) const examples = known_structures.filter((f) => f.is_satisfied === 1) const counterexamples = known_structures.filter((f) => f.is_satisfied === 0) const undecidable_structures = known_structures.filter((f) => f.is_satisfied === null) - const relevant_implications = relevant_implications_db.map(display_implication) - for (const impl of relevant_implications) { if (!impl.is_equivalence && impl.conclusions.includes(id)) { impl.conclusions = [id] diff --git a/src/lib/server/fetchers/search.ts b/src/lib/server/fetchers/search.ts index abccc34ed..856eb4f8a 100644 --- a/src/lib/server/fetchers/search.ts +++ b/src/lib/server/fetchers/search.ts @@ -1,11 +1,10 @@ import { decode_property_ID } from '$shared/property.utils' -import { query } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' import { SEARCH_SEPARATOR } from '$lib/commons/search.config' import { get_contradiction } from '$lib/server/consistency' import type { SearchResults, StructureShort, StructureType } from '$lib/commons/types' import { to_placeholders } from '$shared/utils' -import sql from 'sql-template-tag' export function fetch_search_results( satisfied_query: string | null, @@ -17,21 +16,18 @@ export function fetch_search_results( error(400, 'No properties selected') } - const { rows: all_properties_objects, err: err_all } = query<{ - id: string - dual_property_id: string | null - }>(sql` - SELECT id, dual_property_id FROM properties - WHERE type = ${type} - ORDER BY lower(id) - `) + const all_properties = db + .prepare<[StructureType], { id: string; dual_property_id: string | null }>( + `SELECT id, dual_property_id FROM properties + WHERE type = ? + ORDER BY lower(id)` + ) + .all(type) - if (err_all) error(500, 'Failed to load properties') - - const all_properties = new Set(all_properties_objects.map(({ id }) => id)) + const all_properties_ids = new Set(all_properties.map(({ id }) => id)) const dual_properties_dict: Record = {} - for (const row of all_properties_objects) { + for (const row of all_properties) { dual_properties_dict[row.id] = row.dual_property_id } @@ -40,7 +36,7 @@ export function fetch_search_results( : [] const invalid_satisfied_property = satisfied_properties.find( - (p) => !all_properties.has(p) + (p) => !all_properties_ids.has(p) ) if (invalid_satisfied_property) { @@ -52,7 +48,7 @@ export function fetch_search_results( : [] const invalid_unsatisfied_property = unsatisfied_properties.find( - (p) => !all_properties.has(p) + (p) => !all_properties_ids.has(p) ) if (invalid_unsatisfied_property) { @@ -71,14 +67,12 @@ export function fetch_search_results( dual_satisfied_properties.every(Boolean) && dual_unsatisfied_properties.every(Boolean) - const { contradiction, err: err_con } = get_contradiction( + const { contradiction } = get_contradiction( new Set(satisfied_properties), new Set(unsatisfied_properties), type ) - if (err_con) error(500, 'Consistency check failed') - if (contradiction) { callback() @@ -97,17 +91,19 @@ export function fetch_search_results( const all_selected_properties = [...satisfied_properties, ...unsatisfied_properties] const search_query = ` - SELECT s.id, s.name FROM structures s - INNER JOIN property_assignments a ON a.structure_id = s.id + SELECT s.id, s.name + FROM structures s + INNER JOIN property_assignments a + ON a.structure_id = s.id WHERE s.type = ? AND a.type = s.type - AND property_id IN (${to_placeholders(all_selected_properties)}) + AND property_id IN ${to_placeholders(all_selected_properties)} GROUP BY structure_id HAVING SUM ( CASE WHEN - property_id IN (${to_placeholders(satisfied_properties)}) + property_id IN ${to_placeholders(satisfied_properties)} AND is_satisfied = TRUE THEN 1 ELSE 0 @@ -117,7 +113,7 @@ export function fetch_search_results( SUM( CASE WHEN - property_id IN (${to_placeholders(unsatisfied_properties)}) + property_id IN ${to_placeholders(unsatisfied_properties)} AND is_satisfied = FALSE THEN 1 ELSE 0 @@ -126,17 +122,14 @@ export function fetch_search_results( ORDER BY lower(s.name) ` - const { rows: found_structures, err } = query({ - sql: search_query, - values: [ + const found_structures = db + .prepare(search_query) + .all( type, ...all_selected_properties, ...satisfied_properties, ...unsatisfied_properties - ] - }) - - if (err) error(500, 'Search failed') + ) callback() diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 955f13328..e63f211fc 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -6,29 +6,16 @@ import type { StructureDetails, StructureDisplay, StructureShort, - StructureType, - TagObject + StructureType } from '$lib/commons/types' import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' -import { batch } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' import { display_property_assignment } from '$lib/server/transforms' export function fetch_structure(type: StructureType, id: string): StructureDetails { - const { err, results } = batch< - [ - StructureDisplay, - RelatedStructure, - TagObject, - PropertyAssignmentDB, - PropertyShort, - StructureShort, - CommentObject - ] - >([ - // basic information - sql` - SELECT + const structure = db + .prepare<[string], StructureDisplay>( + `SELECT s.id, s.name, s.notation, @@ -39,30 +26,41 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai ds.notation AS dual_structure_notation FROM structures s LEFT JOIN structures ds ON ds.id = s.dual_structure_id - WHERE s.id = ${id} - `, - // related structures - sql` - SELECT + WHERE s.id = ?` + ) + .get(id) + + if (!structure) { + error(404, `Could not find ${type} with ID '${id}'`) + } + + const related_structures = db + .prepare<[string], RelatedStructure>( + `SELECT c.id, c.name, c.notation FROM related_structures r INNER JOIN structures c ON c.id = r.related_structure_id - WHERE r.structure_id = ${id} - ORDER BY lower(c.name) - `, - // tags - sql` - SELECT st.tag + WHERE r.structure_id = ? + ORDER BY lower(c.name)` + ) + .all(id) + + const tags = db + .prepare<[StructureType, string], string>( + `SELECT st.tag FROM structure_tag_assignments st INNER JOIN structure_tags t ON t.tag = st.tag - WHERE t.type = ${type} AND st.structure_id = ${id} - ORDER BY t.id - `, - // properties - sql` - SELECT + WHERE t.type = ? AND st.structure_id = ? + ORDER BY t.id` + ) + .pluck() + .all(type, id) + + const properties_db = db + .prepare<[string], PropertyAssignmentDB>( + `SELECT pa.property_id AS id, pa.is_satisfied, pa.proof, @@ -76,64 +74,50 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai ON p.id = pa.property_id AND p.type = pa.type INNER JOIN relations r ON r.relation = p.relation - WHERE pa.structure_id = ${id} - ORDER BY pa.id - `, - // unknown properties - sql` - SELECT p.id, p.relation + WHERE pa.structure_id = ? + ORDER BY pa.id` + ) + .all(id) + + const unknown_properties = db + .prepare<[StructureType, string], PropertyShort>( + `SELECT p.id, p.relation FROM properties p - WHERE p.type = ${type} AND NOT EXISTS ( + WHERE p.type = ? + AND NOT EXISTS ( SELECT 1 FROM property_assignments - WHERE structure_id = ${id} AND property_id = p.id + WHERE structure_id = ? AND property_id = p.id ) - ORDER BY lower(p.id) - `, - // undistinguishable structures - sql` - SELECT u.id, u.name + ORDER BY lower(p.id)` + ) + .all(type, id) + + const undistinguishable_structures = db + .prepare<[string, StructureType, string], StructureShort>( + `SELECT u.id, u.name FROM structures u JOIN properties p ON p.type = u.type LEFT JOIN property_assignments pa - ON pa.structure_id = ${id} - AND pa.property_id = p.id + ON pa.structure_id = ? AND pa.property_id = p.id LEFT JOIN property_assignments up - ON up.structure_id = u.id - AND up.property_id = p.id - WHERE - u.type = ${type} - AND u.id != ${id} + ON up.structure_id = u.id AND up.property_id = p.id + WHERE u.type = ? AND u.id != ? GROUP BY u.id, u.name HAVING SUM( CASE WHEN pa.is_satisfied IS up.is_satisfied THEN 0 ELSE 1 END - ) = 0; - `, - // comments - sql` - SELECT id, comment FROM structure_comments - WHERE structure_id = ${id} - ` - ]) - - if (err) error(500, `Could not load ${type} with ID ${id}`) - - const [ - structures, - related_structures, - tag_objects, - properties_db, - unknown_properties, - undistinguishable_structures, - comments - ] = results - - if (!structures.length) error(404, `Could not find ${type} with ID '${id}'`) + ) = 0` + ) + .all(id, type, id) - const structure = structures[0] - const tags = tag_objects.map(({ tag }) => tag) + const comments = db + .prepare<[string], CommentObject>( + `SELECT id, comment FROM structure_comments + WHERE structure_id = ?` + ) + .all(id) const satisfied_properties = properties_db .filter((obj) => obj.is_satisfied === 1) diff --git a/src/lib/server/fetchers/structures.ts b/src/lib/server/fetchers/structures.ts index 4889f3f1e..d3cddf4f2 100644 --- a/src/lib/server/fetchers/structures.ts +++ b/src/lib/server/fetchers/structures.ts @@ -1,62 +1,57 @@ -import { capitalize } from '$shared/utils' -import { PLURALS } from '$shared/config' -import type { StructureShort, StructureType, TagObject } from '$lib/commons/types' -import { batch, query } from '$lib/server/db.catdat' -import { error } from '@sveltejs/kit' -import sql from 'sql-template-tag' +import type { StructureShort, StructureType } from '$lib/commons/types' +import { db } from '$lib/server/db' export function fetch_structures(type: StructureType) { - const { rows: structures, err } = query(sql` - SELECT id, name - FROM structures - WHERE type = ${type} - ORDER BY lower(name) - `) - - if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) + const structures = db + .prepare<[StructureType], StructureShort>( + `SELECT id, name + FROM structures + WHERE type = ? + ORDER BY lower(name)` + ) + .all(type) return { structures, type } } export function fetch_structures_and_tags(type: StructureType) { - const { results, err } = batch<[StructureShort, TagObject]>([ - sql` - SELECT id, name + const structures = db + .prepare<[StructureType], StructureShort>( + `SELECT id, name FROM structures - WHERE type = ${type} - ORDER BY lower(name)`, - sql` - SELECT t.tag + WHERE type = ? + ORDER BY lower(name)` + ) + .all(type) + + const tags = db + .prepare<[StructureType], string>( + `SELECT t.tag FROM structure_tags t - WHERE t.type = ${type} + WHERE t.type = ? AND EXISTS ( SELECT 1 FROM structure_tag_assignments a - WHERE a.tag = t.tag AND a.type = ${type} + WHERE a.tag = t.tag AND a.type = t.type ) - ORDER BY t.id - ` - ]) - - if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) - - const [structures, tag_objects] = results - - const tags = tag_objects.map(({ tag }) => tag) + ORDER BY t.id` + ) + .pluck() + .all(type) return { type, structures, tags } } export function fetch_tagged_structures(type: StructureType, tag: string) { - const { rows: structures, err } = query(sql` - SELECT s.id, s.name - FROM structure_tag_assignments t - INNER JOIN structures s - ON s.id = t.structure_id - WHERE t.tag = ${tag} AND t.type = ${type} - ORDER BY lower(name) - `) - - if (err) error(500, `${capitalize(PLURALS[type])} could not be loaded`) + const structures = db + .prepare<[StructureType, string], StructureShort>( + `SELECT s.id, s.name + FROM structure_tag_assignments t + INNER JOIN structures s + ON s.id = t.structure_id + WHERE t.type = ? AND t.tag = ? + ORDER BY lower(name)` + ) + .all(type, tag) return { type, structures, tag } } diff --git a/src/lib/server/fetchers/tags.ts b/src/lib/server/fetchers/tags.ts index dfd30d0e1..627df5b1b 100644 --- a/src/lib/server/fetchers/tags.ts +++ b/src/lib/server/fetchers/tags.ts @@ -1,23 +1,20 @@ import type { StructureType } from '$lib/commons/types' -import sql from 'sql-template-tag' -import { query } from '$lib/server/db.catdat' +import { db } from '$lib/server/db' export function fetch_structure_tags() { - const { rows, err } = query<{ tag: string; type: StructureType }>(sql` - SELECT tag, type FROM structure_tags - `) - - if (err) throw new Error('Database error: Failed to load structure tags') - - return rows + return db + .prepare< + never[], + { tag: string; type: StructureType } + >(`SELECT tag, type FROM structure_tags`) + .all() } export function fetch_property_tags() { - const { rows, err } = query<{ tag: string; type: StructureType }>(sql` - SELECT tag, type FROM property_tags - `) - - if (err) throw new Error('Database error: Failed to load property tags') - - return rows + return db + .prepare< + never[], + { tag: string; type: StructureType } + >(`SELECT tag, type FROM property_tags`) + .all() } From 455926ab30d28f5e12f6d538f49db472a5c224e0 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 9 Jul 2026 23:46:28 +0200 Subject: [PATCH 10/17] update comments to include all types of structures --- databases/catdat/scripts/deduce-structure-properties.ts | 2 +- databases/catdat/scripts/redundancies.ts | 2 +- databases/catdat/scripts/seed.ts | 1 - databases/catdat/scripts/test.ts | 6 +++--- databases/catdat/scripts/utils/properties.ts | 3 +-- 5 files changed, 6 insertions(+), 8 deletions(-) diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index fba2f34c8..535a2d8d3 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -1,6 +1,6 @@ /** * This file contains all functions that are used to deduce properties - * for categories and functors. + * for categories and other categorical structures. */ import { type Database, SqliteError } from 'better-sqlite3' diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 3c615a753..bcceacd95 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -27,7 +27,7 @@ function check_redundancies() { /** * Checks for redundant (structure, property)-assignments and logs - * one per functor if any are found (satisfied or unsatisfied). + * one per structure if any are found (satisfied or unsatisfied). * No error is thrown intentionally. */ function check_redundant_property_assignments(type: StructureType) { diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index fe25f8e8d..8d23b94aa 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -89,7 +89,6 @@ function clear_all_tables() { db.prepare(`DELETE FROM structure_tags`).run() db.prepare(`DELETE FROM relations`).run() - // this deletes categories and functors automatically db.prepare(`DELETE FROM structures`).run() }) diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index 472379a72..c651a1ab3 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -117,7 +117,7 @@ function test_positivity(structure_id: string, type: StructureType) { } /** - * Tests for all properties p,q of categories or functors that + * Tests for all properties p,q of structures that * if p is dual to q, then q is dual to p. */ function test_mutual_property_duals(type: StructureType) { @@ -145,7 +145,7 @@ function test_mutual_property_duals(type: StructureType) { } /** - * Tests that for a specified list of categories or functors all properties have + * Tests that for a specified list of structures all properties have * been decided. If this test fails, property assignments or implications are missing. */ function test_decided_structures(structure_ids: string[], type: StructureType) { @@ -173,7 +173,7 @@ function test_decided_structures(structure_ids: string[], type: StructureType) { } /** - * Tests if selected categories or functors behave as expected: + * Tests if selected structures behave as expected: * All of their properties in the database have to match those in the * respective JSON files in the subfolder "expected-data". * We exclude undecidable properties here. diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts index e84ec9919..c05353ea5 100644 --- a/databases/catdat/scripts/utils/properties.ts +++ b/databases/catdat/scripts/utils/properties.ts @@ -38,8 +38,7 @@ export function get_properties_dict(db: Database, type: StructureType) { /** * Returns a dictionary with all assigned properties of a list of structures - * (categories or functors), grouped by id and - * value (satisfied / unsatisfied / undecidable). + * grouped by id and value (satisfied / unsatisfied / undecidable). */ export function get_property_assignments( db: Database, From 70a2a3aa827e770204ace8582a94db8c05ccb260 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 10 Jul 2026 00:00:32 +0200 Subject: [PATCH 11/17] small refactor in contradiction worker --- shared/implications.ts | 4 ++++ src/lib/server/consistency.ts | 11 ++++------- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/shared/implications.ts b/shared/implications.ts index 2347b9d15..9fbfb749f 100644 --- a/shared/implications.ts +++ b/shared/implications.ts @@ -86,3 +86,7 @@ export function get_normalized_implications( return implications } + +export function stringify_implication(implication: NormalizedImplication) { + return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` +} diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index a99772cc7..cd874661f 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -2,7 +2,8 @@ import { is_subset } from '$shared/utils' import type { StructureType } from '$lib/commons/types' import { get_normalized_implications, - type NormalizedImplication + type NormalizedImplication, + stringify_implication } from '$shared/implications' import { db } from './db' @@ -40,7 +41,7 @@ export function contradiction_worker( if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`] } - const deduction_dict: Record = {} + const deduction_dict: Partial> = {} const deduced_satisfied_properties = new Set(satisfied_properties) // bfs to find contradiction @@ -82,7 +83,7 @@ export function contradiction_worker( function build_shortest_proof( satisfied_properties: Set, - deduction_dict: Record, + deduction_dict: Partial>, target_property: string ) { const proof: string[] = [] @@ -106,7 +107,3 @@ function build_shortest_proof( return proof } - -function stringify_implication(implication: NormalizedImplication) { - return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}` -} From 2cb3c1455f65876a6745618fd9accc4bbdbf2210 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 10 Jul 2026 15:58:35 +0200 Subject: [PATCH 12/17] use shared deduction helpers for deduction script, redundancy check and consistency function --- .../scripts/deduce-structure-properties.ts | 240 ++++-------------- databases/catdat/scripts/redundancies.ts | 35 ++- shared/deduction.utils.ts | 134 ++++++++++ src/lib/server/consistency.ts | 54 +--- 4 files changed, 222 insertions(+), 241 deletions(-) create mode 100644 shared/deduction.utils.ts diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 535a2d8d3..9ef7ba2cb 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -4,7 +4,7 @@ */ import { type Database, SqliteError } from 'better-sqlite3' -import { is_subset } from '$shared/utils' +import { deduce_properties, refute_properties } from '$shared/deduction.utils' import { get_client } from '$shared/db' import { get_properties_dict, @@ -17,148 +17,74 @@ import { get_structures, is_dual_structure, type StructureMeta } from './utils/s import { get_normalized_implications, NormalizedImplication } from '$shared/implications' /** - * Returns the set of satisfied properties that can be deduced from a set - * of satisfied properties, based on a list of normalized implications. If a - * property dictionary is provided, human-readable proofs are generated as well. + * Deduce satisfied properties for a given structure from given ones + * by using a list of normalized implications. + * Human-readable proofs are generated as well. + * Warning: This mutates the set of satisfied properties. */ -export function get_deduced_satisfied_properties( - satisfied_properties: Set, +function deduce_satisfied_properties( + db: Database, + structure: StructureMeta, implications: NormalizedImplication[], - options: { - properties_dict?: Record - stop_when_found?: string - }, - type: StructureType, - associated_satisfied_properties?: Record> + satisfied_properties: Set, + properties_dict: Record, + type: StructureType ) { - const found = new Set() - const proofs: Record = {} - const deduced_satisfied_properties = new Set(satisfied_properties) - - while (true) { - const newly_found = new Set() - - for (const implication of implications) { - const is_valid = - is_subset(implication.assumptions, deduced_satisfied_properties) && - !deduced_satisfied_properties.has(implication.conclusion) && - !newly_found.has(implication.conclusion) - - if (!is_valid) continue - - if (implication.mapped_assumptions) { - const is_applicable = Object.keys(implication.mapped_assumptions).every( - (key) => { - return is_subset( - implication.mapped_assumptions?.[key] ?? new Set(), - associated_satisfied_properties?.[key] ?? new Set() - ) - } - ) - if (!is_applicable) continue - } - - newly_found.add(implication.conclusion) - found.add(implication.conclusion) - - if (options?.stop_when_found === implication.conclusion) { - deduced_satisfied_properties.add(implication.conclusion) - return { deduced_satisfied_properties, found, proofs } - } - - if (options.properties_dict) { - proofs[implication.conclusion] = get_proof_string( - implication, - options.properties_dict, - type - ) - } - } + const { found, proofs } = deduce_properties( + satisfied_properties, + implications, + (implication) => ({ + proof: get_proof_string(implication, properties_dict, type), + stop: false + }), + structure.associated_satisfied_properties + ) - for (const p of newly_found) deduced_satisfied_properties.add(p) + for (const p of found) satisfied_properties.add(p) - if (!newly_found.size) break - } + save_satisfied_properties(db, structure.id, found, proofs, type) - return { deduced_satisfied_properties, found, proofs } + console.info(`Deduced ${found.size} satisfied properties for ${structure.id}`) } /** - * Returns the set of unsatisfied properties that can be deduced from - * a set of satisfied properties and a set of unsatisfied properties, - * based on a list of normalized implications. If a property dictionary - * is provided, human-readable proofs are generated as well. + * Deduce unsatisfied properties for a given structure from given ones + * by using satisfied properties and a list of normalized implications. + * Human-readable proofs are generated as well. + * Warning: This mutates the set of unsatisfied properties. */ -export function get_deduced_unsatisfied_properties( +function deduce_unsatisfied_properties( + db: Database, + structure: StructureMeta, + implications: NormalizedImplication[], satisfied_properties: Set, unsatisfied_properties: Set, - implications: NormalizedImplication[], - options: { - properties_dict?: Record - stop_when_found?: string - }, - type: StructureType, - associated_satisfied_properties?: Record> + properties_dict: Record, + type: StructureType ) { - const found = new Set() - const proofs: Record = {} - const deduced_unsatisfied_properties = new Set(unsatisfied_properties) - - while (true) { - const newly_found = new Set() - - for (const implication of implications) { - if (!deduced_unsatisfied_properties.has(implication.conclusion)) continue - for (const p of implication.assumptions) { - const is_valid = - !deduced_unsatisfied_properties.has(p) && - !newly_found.has(p) && - is_subset(implication.assumptions, satisfied_properties, { - exception: p - }) - if (!is_valid) continue - - if (implication.mapped_assumptions) { - const is_applicable = Object.keys( - implication.mapped_assumptions - ).every((key) => { - return is_subset( - implication.mapped_assumptions?.[key] ?? new Set(), - associated_satisfied_properties?.[key] ?? new Set() - ) - }) - if (!is_applicable) continue - } - - if (satisfied_properties.has(p)) { - throw new Error(`Contradiction has been found for: ${p}`) - } - - if (options?.stop_when_found === p) { - deduced_unsatisfied_properties.add(p) - return { deduced_unsatisfied_properties, found, proofs } - } - - newly_found.add(p) - found.add(p) - - if (options.properties_dict) { - proofs[p] = get_contradiction_string( - implication, - options.properties_dict, - p, - type - ) - } + const { found, proofs } = refute_properties( + satisfied_properties, + unsatisfied_properties, + implications, + (implication, property) => { + return { + proof: get_contradiction_string( + implication, + properties_dict, + property, + type + ), + stop: false } - } + }, + structure.associated_satisfied_properties + ) - for (const p of newly_found) deduced_unsatisfied_properties.add(p) + for (const p of found) unsatisfied_properties.add(p) - if (!newly_found.size) break - } + save_unsatisfied_properties(db, structure.id, found, proofs, type) - return { deduced_unsatisfied_properties, found, proofs } + console.info(`Deduced ${found.size} unsatisfied properties for ${structure.id}`) } /** @@ -168,7 +94,7 @@ function save_satisfied_properties( db: Database, structure_id: string, found: Set, - proofs: Record, + proofs: Partial>, type: StructureType ) { if (found.size === 0) return @@ -205,7 +131,7 @@ function save_unsatisfied_properties( db: Database, structure_id: string, found: Set, - proofs: Record, + proofs: Partial>, type: StructureType ) { if (found.size === 0) return @@ -235,64 +161,6 @@ function save_unsatisfied_properties( } } -/** - * Deduce satisfied properties for a given structure from given ones - * by using the list of normalized implications. - * Warning: This mutates the set of satisfied properties. - */ -function deduce_satisfied_properties( - db: Database, - structure: StructureMeta, - implications: NormalizedImplication[], - satisfied_properties: Set, - properties_dict: Record, - type: StructureType -) { - const { found, proofs } = get_deduced_satisfied_properties( - satisfied_properties, - implications, - { properties_dict }, - type, - structure.associated_satisfied_properties - ) - - for (const p of found) satisfied_properties.add(p) - - save_satisfied_properties(db, structure.id, found, proofs, type) - - console.info(`Deduced ${found.size} satisfied properties for ${structure.id}`) -} - -/** - * Deduce unsatisfied properties for a given structure from given ones - * by using the satisfied properties and the list of normalized implications. - * Warning: This mutates the set of unsatisfied properties. - */ -function deduce_unsatisfied_properties( - db: Database, - structure: StructureMeta, - implications: NormalizedImplication[], - satisfied_properties: Set, - unsatisfied_properties: Set, - properties_dict: Record, - type: StructureType -) { - const { found, proofs } = get_deduced_unsatisfied_properties( - satisfied_properties, - unsatisfied_properties, - implications, - { properties_dict }, - type, - structure.associated_satisfied_properties - ) - - for (const p of found) unsatisfied_properties.add(p) - - save_unsatisfied_properties(db, structure.id, found, proofs, type) - - console.info(`Deduced ${found.size} unsatisfied properties for ${structure.id}`) -} - /** * Assign dual properties to dual structures: * If C has property P, then C^op has property P^op (if defined). diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index bcceacd95..446f52467 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -1,14 +1,12 @@ import { get_client } from '$shared/db' -import { - get_deduced_satisfied_properties, - get_deduced_unsatisfied_properties -} from './deduce-structure-properties' import { get_property_assignments_by_deduction } from './utils/properties' import { STRUCTURE_TYPES, type StructureType } from '$shared/config' import { get_normalized_implications, + stringify_implication, type NormalizedImplication } from '$shared/implications' +import { deduce_properties, refute_properties } from '$shared/deduction.utils' import { get_structures } from './utils/structures' const db = get_client({ readonly: true }) @@ -49,7 +47,6 @@ function check_redundant_property_assignments(type: StructureType) { for (const structure of structures) { const redundant_satisfied_property = get_redundant_satisfied_property( - type, assignments[structure.id].satisfied.non_deduced, implications, ignore_dict[structure.id], @@ -70,7 +67,6 @@ function check_redundant_property_assignments(type: StructureType) { ]) const redundant_unsatisfied_property = get_redundant_unsatisfied_property( - type, all_satisfied_properties, assignments[structure.id].unsatisfied.non_deduced, implications, @@ -105,7 +101,6 @@ function check_redundant_property_assignments(type: StructureType) { * If no such property exists, null is returned. */ function get_redundant_satisfied_property( - type: StructureType, satisfied_properties: Set, implications: NormalizedImplication[], ignored: Set = new Set(), @@ -113,17 +108,24 @@ function get_redundant_satisfied_property( ) { for (const p of [...satisfied_properties]) { if (ignored.has(p)) continue + satisfied_properties.delete(p) - const { deduced_satisfied_properties } = get_deduced_satisfied_properties( + + const { deduced_satisfied_properties } = deduce_properties( satisfied_properties, implications, - { stop_when_found: p }, - type, + (implication) => ({ + proof: stringify_implication(implication), + stop: implication.conclusion === p + }), associated_satisfied_properties ) + if (deduced_satisfied_properties.has(p)) return p + satisfied_properties.add(p) } + return null } @@ -134,7 +136,6 @@ function get_redundant_satisfied_property( * If no such property exists, null is returned. */ function get_redundant_unsatisfied_property( - type: StructureType, satisfied_properties: Set, unsatisfied_properties: Set, implications: NormalizedImplication[], @@ -143,16 +144,22 @@ function get_redundant_unsatisfied_property( ) { for (const p of [...unsatisfied_properties]) { if (ignored.has(p)) continue + unsatisfied_properties.delete(p) - const { deduced_unsatisfied_properties } = get_deduced_unsatisfied_properties( + + const { deduced_unsatisfied_properties } = refute_properties( satisfied_properties, unsatisfied_properties, implications, - { stop_when_found: p }, - type, + (implication, property) => ({ + proof: stringify_implication(implication), + stop: property === p + }), associated_satisfied_properties ) + if (deduced_unsatisfied_properties.has(p)) return p + unsatisfied_properties.add(p) } return null diff --git a/shared/deduction.utils.ts b/shared/deduction.utils.ts new file mode 100644 index 000000000..9127b5012 --- /dev/null +++ b/shared/deduction.utils.ts @@ -0,0 +1,134 @@ +import { type NormalizedImplication } from './implications' +import { is_subset } from './utils' + +export function deduce_properties( + satisfied_properties: Set, + implications: NormalizedImplication[], + on_discover: (implication: NormalizedImplication) => { + proof: ProofType + stop: boolean + }, + associated_satisfied_properties?: Record> +) { + const found = new Set() + const proofs: Partial> = {} + const deduced_satisfied_properties = new Set(satisfied_properties) + + while (true) { + const newly_found = new Set() + + for (const implication of implications) { + const is_valid = + is_subset(implication.assumptions, deduced_satisfied_properties) && + !deduced_satisfied_properties.has(implication.conclusion) && + !newly_found.has(implication.conclusion) + + if (!is_valid) continue + + if (!is_applicable(implication, associated_satisfied_properties)) continue + + newly_found.add(implication.conclusion) + found.add(implication.conclusion) + + const { proof, stop } = on_discover(implication) + + proofs[implication.conclusion] = proof + + if (stop) { + for (const p of newly_found) deduced_satisfied_properties.add(p) + return { + deduced_satisfied_properties, + found, + proofs, + stop_property: implication.conclusion + } + } + } + + for (const p of newly_found) deduced_satisfied_properties.add(p) + + if (!newly_found.size) break + } + + return { deduced_satisfied_properties, found, proofs } +} + +export function refute_properties( + satisfied_properties: Set, + unsatisfied_properties: Set, + implications: NormalizedImplication[], + on_discover: ( + implication: NormalizedImplication, + property: string + ) => { proof: ProofType; stop: boolean }, + associated_satisfied_properties?: Record> +) { + const found = new Set() + const proofs: Partial> = {} + const deduced_unsatisfied_properties = new Set(unsatisfied_properties) + + while (true) { + const newly_found = new Set() + + for (const implication of implications) { + if (!deduced_unsatisfied_properties.has(implication.conclusion)) continue + + for (const property of implication.assumptions) { + const is_valid = + !deduced_unsatisfied_properties.has(property) && + !newly_found.has(property) && + is_subset(implication.assumptions, satisfied_properties, { + exception: property + }) + + if (!is_valid) continue + + if (!is_applicable(implication, associated_satisfied_properties)) continue + + if (satisfied_properties.has(property)) { + throw new Error(`Contradiction has been found for: ${property}`) + } + + newly_found.add(property) + found.add(property) + + const discovery = on_discover(implication, property) + + if (discovery.proof !== undefined) { + proofs[property] = discovery.proof + } + + if (discovery.stop) { + for (const p of newly_found) deduced_unsatisfied_properties.add(p) + return { + deduced_unsatisfied_properties, + found, + proofs, + stop_property: property + } + } + } + } + + for (const property of newly_found) deduced_unsatisfied_properties.add(property) + + if (!newly_found.size) break + } + + return { deduced_unsatisfied_properties, found, proofs } +} + +function is_applicable( + implication: NormalizedImplication, + associated_satisfied_properties?: Record> +) { + return ( + !implication.mapped_assumptions || + Object.keys(implication.mapped_assumptions).every((key) => { + return is_subset( + implication.mapped_assumptions?.[key] ?? new Set(), + associated_satisfied_properties?.[key] ?? new Set() + ) + }) + ) +} diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index cd874661f..1e9cab31a 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -1,4 +1,4 @@ -import { is_subset } from '$shared/utils' +import { deduce_properties } from '$shared/deduction.utils' import type { StructureType } from '$lib/commons/types' import { get_normalized_implications, @@ -7,8 +7,6 @@ import { } from '$shared/implications' import { db } from './db' -// TODO: If possible, remove the code duplication with deduction and redundancy scripts. - export function get_contradiction( satisfied_properties: Set, unsatisfied_properties: Set, @@ -41,49 +39,23 @@ export function contradiction_worker( if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`] } - const deduction_dict: Partial> = {} - const deduced_satisfied_properties = new Set(satisfied_properties) - - // bfs to find contradiction - - let contradictory_property: string | null = null - - while (!contradictory_property) { - const new_properties = new Set() - - for (const implication of implications) { - const is_valid = - is_subset(implication.assumptions, deduced_satisfied_properties) && - !deduced_satisfied_properties.has(implication.conclusion) && - !new_properties.has(implication.conclusion) - if (!is_valid) continue - - new_properties.add(implication.conclusion) - deduction_dict[implication.conclusion] = implication - - if (unsatisfied_properties.has(implication.conclusion)) { - contradictory_property = implication.conclusion - break - } - } - - if (!new_properties.size) break - - for (const p of new_properties) deduced_satisfied_properties.add(p) - } - - if (!contradictory_property) return null - - return build_shortest_proof( + const { proofs, stop_property } = deduce_properties( satisfied_properties, - deduction_dict, - contradictory_property + implications, + (implication) => ({ + proof: implication, + stop: unsatisfied_properties.has(implication.conclusion) + }) ) + + if (!stop_property) return null + + return build_shortest_proof(satisfied_properties, proofs, stop_property) } function build_shortest_proof( satisfied_properties: Set, - deduction_dict: Partial>, + proofs: Partial>, target_property: string ) { const proof: string[] = [] @@ -95,7 +67,7 @@ function build_shortest_proof( if (satisfied_properties.has(property)) return visited_properties.add(property) - const implication = deduction_dict[property] + const implication = proofs[property] if (!implication) throw new Error(`Missing deduction for property: ${property}`) for (const p of implication.assumptions) derive(p) From 204f87ac0e97ae0bda71c1a40eb857684589cac4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 10 Jul 2026 23:55:48 +0200 Subject: [PATCH 13/17] improve error handling for contradictory property assignments --- .../scripts/deduce-structure-properties.ts | 52 ++++++------------- databases/catdat/scripts/seed.ts | 15 ++++++ shared/utils.ts | 11 ++++ 3 files changed, 43 insertions(+), 35 deletions(-) diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 9ef7ba2cb..54549a050 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -3,7 +3,7 @@ * for categories and other categorical structures. */ -import { type Database, SqliteError } from 'better-sqlite3' +import { type Database } from 'better-sqlite3' import { deduce_properties, refute_properties } from '$shared/deduction.utils' import { get_client } from '$shared/db' import { @@ -27,19 +27,27 @@ function deduce_satisfied_properties( structure: StructureMeta, implications: NormalizedImplication[], satisfied_properties: Set, + unsatisfied_properties: Set, properties_dict: Record, type: StructureType ) { - const { found, proofs } = deduce_properties( + const { found, proofs, stop_property } = deduce_properties( satisfied_properties, implications, (implication) => ({ proof: get_proof_string(implication, properties_dict, type), - stop: false + stop: unsatisfied_properties.has(implication.conclusion) }), structure.associated_satisfied_properties ) + if (stop_property) { + console.error( + `❌ Property assignments of ${structure.id} are contradictory: "${stop_property}" can be deduced from its satisfied properties, but is marked as unsatisfied.` + ) + process.exit(1) + } + for (const p of found) satisfied_properties.add(p) save_satisfied_properties(db, structure.id, found, proofs, type) @@ -99,28 +107,14 @@ function save_satisfied_properties( ) { if (found.size === 0) return - const err_msg = `❌ Failed to complete deduction of satisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` - const property_insert = db.prepare(` INSERT INTO property_assignments (structure_id, property_id, type, is_satisfied, proof, is_deduced) VALUES (?, ?, ?, TRUE, ?, TRUE) `) - try { - for (const p of found) { - property_insert.run(structure_id, p, type, proofs[p]) - } - } catch (err) { - if (err instanceof SqliteError) { - if (err.code.startsWith('SQLITE_CONSTRAINT')) { - console.error(err_msg) - } - console.error(err.message) - } else { - console.error(err) - } - process.exit(1) + for (const p of found) { + property_insert.run(structure_id, p, type, proofs[p]) } } @@ -136,28 +130,14 @@ function save_unsatisfied_properties( ) { if (found.size === 0) return - const err_msg = `❌ Failed to complete deduction of unsatisfied properties for ${structure_id} because of a conflict. The likely cause is a contradiction between its assigned properties.` - const property_insert = db.prepare(` INSERT INTO property_assignments (structure_id, property_id, type, is_satisfied, proof, is_deduced) VALUES (?, ?, ?, FALSE, ?, TRUE) `) - try { - for (const p of found) { - property_insert.run(structure_id, p, type, proofs[p]) - } - } catch (err) { - if (err instanceof SqliteError) { - if (err.code.startsWith('SQLITE_CONSTRAINT')) { - console.error(err_msg) - } - console.error(err.message) - } else { - console.error(err) - } - process.exit(1) + for (const p of found) { + property_insert.run(structure_id, p, type, proofs[p]) } } @@ -274,6 +254,7 @@ export function deduce_properties_for_structures(type: StructureType) { structure, implications, assigned.satisfied, + assigned.unsatisfied, properties_dict, type ) @@ -319,6 +300,7 @@ export function deduce_properties_for_structures(type: StructureType) { structure, implications, assigned.satisfied, + assigned.unsatisfied, properties_dict, type ) diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 8d23b94aa..535051854 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -13,6 +13,7 @@ import type { } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' +import { are_disjoint } from '$shared/utils' const db = get_client({ readonly: false }) @@ -215,6 +216,20 @@ function seed_structures({ } function insert_structure(structure: T) { + const properties_are_disjoint = are_disjoint( + [ + structure.satisfied_properties, + structure.unsatisfied_properties, + structure.undecidable_properties ?? [] + ], + (entry) => entry.property + ) + + if (!properties_are_disjoint) { + console.error(`❌ Properties of ${structure.id} are contradictory.`) + process.exit(1) + } + structure_insert.run( structure.id, type, diff --git a/shared/utils.ts b/shared/utils.ts index 020592a23..afd32977a 100644 --- a/shared/utils.ts +++ b/shared/utils.ts @@ -17,6 +17,17 @@ export function is_subset(a: Set, b: Set, options?: { exception: T }) { return true } +export function are_disjoint(lists: T[][], transform: (x: T) => S) { + for (let i = 0; i < lists.length; i++) { + const a = lists[i].map(transform) + for (let j = i + 1; j < lists.length; j++) { + const b = lists[j].map(transform) + if (a.some((x) => b.includes(x))) return false + } + } + return true +} + export const sleep = (delay: number) => new Promise((res) => setTimeout(res, delay)) export function capitalize(txt: string) { From d46a9f27adb3532b96d938f472a012129fa3c8fd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 11 Jul 2026 00:15:15 +0200 Subject: [PATCH 14/17] minor refactoring --- databases/catdat/scripts/redundancies.ts | 4 ++-- databases/catdat/scripts/utils/properties.ts | 4 +--- databases/catdat/scripts/utils/structures.ts | 10 +++++++--- shared/deduction.utils.ts | 6 +++--- 4 files changed, 13 insertions(+), 11 deletions(-) diff --git a/databases/catdat/scripts/redundancies.ts b/databases/catdat/scripts/redundancies.ts index 446f52467..bf3520a7e 100644 --- a/databases/catdat/scripts/redundancies.ts +++ b/databases/catdat/scripts/redundancies.ts @@ -104,7 +104,7 @@ function get_redundant_satisfied_property( satisfied_properties: Set, implications: NormalizedImplication[], ignored: Set = new Set(), - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> ) { for (const p of [...satisfied_properties]) { if (ignored.has(p)) continue @@ -140,7 +140,7 @@ function get_redundant_unsatisfied_property( unsatisfied_properties: Set, implications: NormalizedImplication[], ignored: Set = new Set(), - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> ) { for (const p of [...unsatisfied_properties]) { if (ignored.has(p)) continue diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts index c05353ea5..df629bccb 100644 --- a/databases/catdat/scripts/utils/properties.ts +++ b/databases/catdat/scripts/utils/properties.ts @@ -122,9 +122,7 @@ export function get_property_assignments_by_deduction( is_satisfied, is_deduced FROM property_assignments - WHERE - type = ? - AND is_satisfied IS NOT NULL` + WHERE type = ? AND is_satisfied IS NOT NULL` ) .all(type) diff --git a/databases/catdat/scripts/utils/structures.ts b/databases/catdat/scripts/utils/structures.ts index d8ca7ec57..17c6848e6 100644 --- a/databases/catdat/scripts/utils/structures.ts +++ b/databases/catdat/scripts/utils/structures.ts @@ -8,7 +8,7 @@ export type StructureMeta = { id: string name: string dual?: string | null - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> } /** @@ -18,7 +18,7 @@ export type StructureMeta = { const TABLES: Record = { category: 'categories', functor: 'functors', - morphism: 'morphisms', + morphism: 'morphisms' } /** @@ -40,7 +40,11 @@ export function get_structures(db: Database, type: StructureType): StructureMeta .all(type) const structure_maps = db - .prepare<[StructureType], string>(`SELECT map FROM structure_maps WHERE type = ?`) + .prepare<[StructureType], string>( + `SELECT map + FROM structure_maps + WHERE type = ?` + ) .pluck() .all(type) diff --git a/shared/deduction.utils.ts b/shared/deduction.utils.ts index 9127b5012..4fe21763f 100644 --- a/shared/deduction.utils.ts +++ b/shared/deduction.utils.ts @@ -8,7 +8,7 @@ export function deduce_properties( proof: ProofType stop: boolean }, - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> ) { const found = new Set() const proofs: Partial> = {} @@ -61,7 +61,7 @@ export function refute_properties( implication: NormalizedImplication, property: string ) => { proof: ProofType; stop: boolean }, - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> ) { const found = new Set() const proofs: Partial> = {} @@ -120,7 +120,7 @@ export function refute_properties( function is_applicable( implication: NormalizedImplication, - associated_satisfied_properties?: Record> + associated_satisfied_properties?: Partial>> ) { return ( !implication.mapped_assumptions || From a32ee483b18f7e6fa174b595b1bf15c4d3dfbb24 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 11 Jul 2026 08:25:15 +0200 Subject: [PATCH 15/17] fix setup script --- package.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/package.json b/package.json index d9d76059c..6e756261c 100644 --- a/package.json +++ b/package.json @@ -17,8 +17,8 @@ "env:check": "tsx scripts/env.check", "db:shell": "sqlite3 databases/catdat/catdat.db", "db:kill": "rm -rf databases/catdat/catdat.db", - "db:setup:catdat": "pnpm db:kill && tsx databases/catdat/scripts/setup.ts", - "db:setup": "pnpm db:kill && tsx databases/catdat/scripts/setup.ts && tsx databases/app/scripts/setup.ts", + "db:setup:catdat": "pnpm db:kill && tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/setup.ts", + "db:setup": "pnpm db:kill && tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/setup.ts && tsx --tsconfig databases/tsconfig.json databases/app/scripts/setup.ts", "db:seed": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/seed.ts", "db:deduce": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/deduce.ts", "db:test": "tsx --tsconfig databases/tsconfig.json databases/catdat/scripts/test.ts", From 8190946f6c7e73e1a0ee0df1be21de8766715546 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 11 Jul 2026 08:32:35 +0200 Subject: [PATCH 16/17] remove redundancy check from test workflow this does not report any error anyway, and should only be used during development --- .github/workflows/test.yaml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml index 020e30eb0..61e6b5934 100644 --- a/.github/workflows/test.yaml +++ b/.github/workflows/test.yaml @@ -34,9 +34,6 @@ jobs: pnpm db:setup:catdat pnpm db:update - - name: Redundancy check - run: pnpm db:redundancies - - name: Cache Playwright browsers uses: actions/cache@v6 with: From 07d9f1a4aa02113c1c218b4f1dd7273f8c100488 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 11 Jul 2026 08:46:49 +0200 Subject: [PATCH 17/17] reduce logs in CI --- .cspell.json | 3 ++- databases/app/scripts/setup.ts | 7 +++--- .../catdat/scripts/deduce-implications.ts | 11 ++++++--- .../scripts/deduce-special-morphisms.ts | 3 ++- .../catdat/scripts/deduce-special-objects.ts | 3 ++- .../scripts/deduce-structure-properties.ts | 11 +++++---- .../scripts/restrict-functor-properties.ts | 3 ++- databases/catdat/scripts/seed.ts | 6 ++--- databases/catdat/scripts/setup.ts | 5 ++-- databases/catdat/scripts/test.ts | 24 ++++++++++--------- .../catdat/scripts/utils/seed.helpers.ts | 7 +++--- shared/utils.ts | 4 ++++ 12 files changed, 53 insertions(+), 34 deletions(-) diff --git a/.cspell.json b/.cspell.json index a9926c364..96b8cde14 100644 --- a/.cspell.json +++ b/.cspell.json @@ -18,7 +18,8 @@ "esbuild", "coloneqq", "FiltVect", - "networkidle" + "networkidle", + "devlog" ], "words": [ "abelian", diff --git a/databases/app/scripts/setup.ts b/databases/app/scripts/setup.ts index 106d38bde..7bcc51691 100644 --- a/databases/app/scripts/setup.ts +++ b/databases/app/scripts/setup.ts @@ -1,5 +1,6 @@ import dotenv from 'dotenv' import { createClient } from '@libsql/client' +import { devlog } from '$shared/utils' dotenv.config({ quiet: true }) @@ -39,7 +40,7 @@ async function create_visits_table() { ) `) - console.info('Visits table ready') + devlog('Visits table ready') } /** @@ -58,7 +59,7 @@ async function create_submissions_table() { ) `) - console.info('Submissions table ready') + devlog('Submissions table ready') } /** @@ -74,5 +75,5 @@ async function create_actions_table() { ) `) - console.info('User actions table ready') + devlog('User actions table ready') } diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts index a74438f44..14ed69ea8 100644 --- a/databases/catdat/scripts/deduce-implications.ts +++ b/databases/catdat/scripts/deduce-implications.ts @@ -1,5 +1,10 @@ import { type StructureType, STRUCTURE_TYPES_WITH_DUALS } from '$shared/config' -import { are_equal_sets, parse_nested_json_set, parse_json_set } from '$shared/utils' +import { + are_equal_sets, + parse_nested_json_set, + parse_json_set, + devlog +} from '$shared/utils' import { get_client } from '$shared/db' const db = get_client({ readonly: false }) @@ -151,7 +156,7 @@ export function create_dualized_implications(type: StructureType) { } } - console.info(`Deduced ${count} ${type} implications by duality`) + devlog(`Deduced ${count} ${type} implications by duality`) }) insert_duals() @@ -203,5 +208,5 @@ export function create_self_dual_implications(type: StructureType) { conclusion_insert.run(implication_id, p.dual, type) } - console.info(`Deduced ${relevant_props.length} ${type} implications by self-duality`) + devlog(`Deduced ${relevant_props.length} ${type} implications by self-duality`) } diff --git a/databases/catdat/scripts/deduce-special-morphisms.ts b/databases/catdat/scripts/deduce-special-morphisms.ts index 1eadedbd5..5d167fb82 100644 --- a/databases/catdat/scripts/deduce-special-morphisms.ts +++ b/databases/catdat/scripts/deduce-special-morphisms.ts @@ -1,4 +1,5 @@ import { get_client } from '$shared/db' +import { devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -46,5 +47,5 @@ function deduce_special_morphisms_of_dual_categories() { ) .run() - console.info(`Deduced ${res.changes} special morphisms by duality`) + devlog(`Deduced ${res.changes} special morphisms by duality`) } diff --git a/databases/catdat/scripts/deduce-special-objects.ts b/databases/catdat/scripts/deduce-special-objects.ts index 50fce1809..c65c57914 100644 --- a/databases/catdat/scripts/deduce-special-objects.ts +++ b/databases/catdat/scripts/deduce-special-objects.ts @@ -1,4 +1,5 @@ import { get_client } from '$shared/db' +import { devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -40,5 +41,5 @@ function deduce_special_objects_of_dual_categories() { ) .run() - console.info(`Deduced ${res.changes} special objects by duality`) + devlog(`Deduced ${res.changes} special objects by duality`) } diff --git a/databases/catdat/scripts/deduce-structure-properties.ts b/databases/catdat/scripts/deduce-structure-properties.ts index 54549a050..a17f331b5 100644 --- a/databases/catdat/scripts/deduce-structure-properties.ts +++ b/databases/catdat/scripts/deduce-structure-properties.ts @@ -15,6 +15,7 @@ import { get_contradiction_string, get_proof_string } from './utils/implications import { type StructureType, STRUCTURE_TYPES_WITH_DUALS } from '$shared/config' import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures' import { get_normalized_implications, NormalizedImplication } from '$shared/implications' +import { devlog } from '$shared/utils' /** * Deduce satisfied properties for a given structure from given ones @@ -52,7 +53,7 @@ function deduce_satisfied_properties( save_satisfied_properties(db, structure.id, found, proofs, type) - console.info(`Deduced ${found.size} satisfied properties for ${structure.id}`) + devlog(`Deduced ${found.size} satisfied properties for ${structure.id}`) } /** @@ -92,7 +93,7 @@ function deduce_unsatisfied_properties( save_unsatisfied_properties(db, structure.id, found, proofs, type) - console.info(`Deduced ${found.size} unsatisfied properties for ${structure.id}`) + devlog(`Deduced ${found.size} unsatisfied properties for ${structure.id}`) } /** @@ -199,7 +200,7 @@ function deduce_dual_properties( property_insert.run(structure.id, p, type, 1, proof_satisfied) } - console.info( + devlog( `Deduced ${new_satisfied.size} satisfied properties by duality for ${structure.id}` ) @@ -207,7 +208,7 @@ function deduce_dual_properties( property_insert.run(structure.id, q, type, 0, proof_unsatisfied) } - console.info( + devlog( `Deduced ${new_unsatisfied.size} unsatisfied properties by duality for ${structure.id}` ) @@ -215,7 +216,7 @@ function deduce_dual_properties( property_insert.run(structure.id, q, type, null, proof_undecidable) } - console.info( + devlog( `Deduced ${new_undecidable.size} undecidable properties by duality for ${structure.id}` ) } diff --git a/databases/catdat/scripts/restrict-functor-properties.ts b/databases/catdat/scripts/restrict-functor-properties.ts index d246a3f84..70588dd65 100644 --- a/databases/catdat/scripts/restrict-functor-properties.ts +++ b/databases/catdat/scripts/restrict-functor-properties.ts @@ -1,4 +1,5 @@ import { get_client } from '$shared/db' +import { devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -38,5 +39,5 @@ export function restrict_representable_functors() { ) .run() - console.info(`Deduced that ${res.changes} functors cannot be representable`) + devlog(`Deduced that ${res.changes} functors cannot be representable`) } diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 535051854..9c60ddf84 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -13,7 +13,7 @@ import type { } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' -import { are_disjoint } from '$shared/utils' +import { are_disjoint, devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -48,7 +48,7 @@ function seed() { * Checks if the schema is up-to-date, and throws an error otherwise. */ function check_schema() { - console.info(`\nCheck schema ...`) + devlog(`\nCheck schema ...`) const schema_hash = get_saved_schema_hash() const actual_hash = create_schema_hash() @@ -63,7 +63,7 @@ function check_schema() { * Clears all tables in the database. This is done as a first step. */ function clear_all_tables() { - console.info(`\nClear all tables ...`) + devlog(`\nClear all tables ...`) const tx = db.transaction(() => { db.pragma('defer_foreign_keys = ON') diff --git a/databases/catdat/scripts/setup.ts b/databases/catdat/scripts/setup.ts index 62bbbf0ee..4c1fa136e 100644 --- a/databases/catdat/scripts/setup.ts +++ b/databases/catdat/scripts/setup.ts @@ -2,6 +2,7 @@ import fs from 'node:fs' import path from 'node:path' import { get_client } from '$shared/db' import { create_schema_hash, write_schema_hash } from './utils/schema' +import { devlog } from '$shared/utils' const schema_folder = path.resolve('databases', 'catdat', 'schema') @@ -26,7 +27,7 @@ function setup() { for (const file of files) { const sql = fs.readFileSync(path.join(schema_folder, file), 'utf8') - console.info(`Apply: ${file}`) + devlog(`Apply: ${file}`) try { db.exec(sql) @@ -39,5 +40,5 @@ function setup() { const hash = create_schema_hash() write_schema_hash(hash) - console.info('Setup complete') + devlog('Setup complete') } diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index c651a1ab3..1e501574d 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -12,7 +12,7 @@ import id_Set_expected from './expected-data/id_Set.json' import decided_categories from './expected-data/decided-categories.json' import decided_functors from './expected-data/decided-functors.json' import decided_morphisms from './expected-data/decided-morphisms.json' -import { capitalize } from '$shared/utils' +import { capitalize, devlog } from '$shared/utils' import { get_client } from '$shared/db' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' import fs from 'node:fs' @@ -28,10 +28,12 @@ execute_tests() */ function execute_tests() { try { - console.info('--- Test link targets ---') + console.info('--- Database Tests ---') + + devlog('\n--- Test link targets ---') check_link_targets_exist() - console.info('\n--- Test categories ---') + devlog('\n--- Test categories ---') test_mutual_structure_duals('category') test_positivity('1', 'category') @@ -42,7 +44,7 @@ function execute_tests() { 'category' ) - console.info('\n--- Test functors ---') + devlog('\n--- Test functors ---') test_positivity('id_Set', 'functor') test_mutual_property_duals('functor') @@ -52,7 +54,7 @@ function execute_tests() { 'functor' ) - console.info('\n--- Test morphisms ---') + devlog('\n--- Test morphisms ---') test_positivity('id_X', 'morphism') test_decided_structures(decided_morphisms, 'morphism') @@ -91,7 +93,7 @@ function test_mutual_structure_duals(type: StructureType) { } } - console.info(`✅ ${capitalize(PLURALS[type])} are mutually dual`) + devlog(`✅ ${capitalize(PLURALS[type])} are mutually dual`) } /** @@ -113,7 +115,7 @@ function test_positivity(structure_id: string, type: StructureType) { ) } - console.info(`✅ The ${type} ${structure_id} has no unsatisfied properties`) + devlog(`✅ The ${type} ${structure_id} has no unsatisfied properties`) } /** @@ -141,7 +143,7 @@ function test_mutual_property_duals(type: StructureType) { } } - console.info(`✅ ${capitalize(type)} properties are mutually dual`) + devlog(`✅ ${capitalize(type)} properties are mutually dual`) } /** @@ -168,7 +170,7 @@ function test_decided_structures(structure_ids: string[], type: StructureType) { ) } - console.info(`✅ All properties have been decided for ${structure_id}`) + devlog(`✅ All properties have been decided for ${structure_id}`) } } @@ -199,7 +201,7 @@ function test_properties_of_selected_structures( throw new Error(`❌ Incorrect property of ${structure_id}: ${property_id}`) } - console.info(`✅ Properties of ${structure_id} are correct`) + devlog(`✅ Properties of ${structure_id} are correct`) } } @@ -285,5 +287,5 @@ function check_link_targets_exist() { } } - console.info(`✅ Link targets exist`) + devlog(`✅ Link targets exist`) } diff --git a/databases/catdat/scripts/utils/seed.helpers.ts b/databases/catdat/scripts/utils/seed.helpers.ts index 1b04e7d2c..933675168 100644 --- a/databases/catdat/scripts/utils/seed.helpers.ts +++ b/databases/catdat/scripts/utils/seed.helpers.ts @@ -2,6 +2,7 @@ import type { Database } from 'better-sqlite3' import path from 'node:path' import fs from 'node:fs' import YAML from 'yaml' +import { devlog } from '$shared/utils' function read_yaml_file(...parts: string[]): T { const content = fs.readFileSync(path.join(...parts), 'utf8') @@ -21,7 +22,7 @@ export function seed_file( file: string, insert: (item: T) => void ) { - console.info(`\nSeed ${label} ...`) + devlog(`\nSeed ${label} ...`) const item = read_yaml_file(file) const tx = db.transaction(() => { @@ -43,7 +44,7 @@ export function seed_files( folder: string, insert: (item: T) => void ) { - console.info(`\nSeed ${label} ...`) + devlog(`\nSeed ${label} ...`) const files = get_yaml_files(folder) @@ -51,7 +52,7 @@ export function seed_files( db.pragma('defer_foreign_keys = ON') for (const file of files) { - console.info(`Seed: ${file}`) + devlog(`Seed: ${file}`) const item = read_yaml_file(folder, file) insert(item) diff --git a/shared/utils.ts b/shared/utils.ts index afd32977a..0cb45d731 100644 --- a/shared/utils.ts +++ b/shared/utils.ts @@ -73,3 +73,7 @@ export function strip_math(s: string) { export function add_math(s: string) { return `$${s}$` } + +export function devlog(msg: string) { + if (!process.env.CI) console.info(msg) +}