refactor fetching functions

Author: ScriptRaccoon

databases/catdat/scripts/config.ts

@@ -5,11 +5,9 @@ export const PLURALS = {
 	functor: 'functors',
 } as const
 
-// TODO: move this to the schema
 export const STRUCTURE_MAPS = [
 	['source', 'functor', 'category'],
 	['target', 'functor', 'category'],
 ] as const
 
-// TODO: move this to the schema
 export const STRUCTURES_WITH_DUALS: StructureType[] = ['category']

src/lib/commons/types.ts

@@ -120,6 +120,12 @@ export type ImplicationDisplay = Replace<
 	}
 >
 
+export type NormalizedImplication = {
+	id: string
+	assumptions: Set<string>
+	conclusion: string
+}
+
 export type SearchResults = {
 	contradiction: string[] | null
 	satisfied_properties: string[]

src/lib/server/consistency.ts

@@ -1,11 +1,7 @@
 import { is_subset } from './utils'
 import type { SqliteError } from 'better-sqlite3'
-import {
-	get_normalized_implications,
-	stringify_implication,
-	type NormalizedImplication,
-} from './implications'
-import type { StructureType } from '$lib/commons/types'
+import type { NormalizedImplication, StructureType } from '$lib/commons/types'
+import { get_normalized_implications } from './fetchers/implications'
 
 // TODO: If possible, remove the code duplication with deduction and redundancy scripts.
 
@@ -107,3 +103,7 @@ function build_shortest_proof(
 
 	return proof
 }
+
+function stringify_implication(implication: NormalizedImplication) {
+	return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}`
+}

src/lib/server/fetchers/category.ts

@@ -0,0 +1,69 @@
+import type {
+	CategorySpecificDisplay,
+	SpecialMorphism,
+	SpecialObject,
+	StructureShort,
+} from '$lib/commons/types'
+import sql from 'sql-template-tag'
+import { batch, query } from '$lib/server/db.catdat'
+import { error } from '@sveltejs/kit'
+
+export function fetch_category(id: string) {
+	const { results, err } = batch<
+		[CategorySpecificDisplay, SpecialObject, SpecialMorphism]
+	>([
+		// specific information for the category
+		sql`
+                SELECT c.objects, c.morphisms
+                FROM categories c
+                WHERE c.id = ${id}
+            `,
+		// special objects
+		sql`
+                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
+                FROM special_morphism_types t
+                LEFT JOIN special_morphisms s
+                    ON s.type = t.type AND s.category_id = ${id}
+                ORDER BY t.id
+            `,
+	])
+
+	if (err) error(500, 'Could not load category')
+
+	const [categories, special_objects, special_morphisms] = results
+
+	if (!categories.length) error(404, `Could not find category with ID '${id}'`)
+
+	return {
+		...categories[0],
+		special_objects,
+		special_morphisms,
+	}
+}
+
+export function fetch_categories_with_missing_morphisms() {
+	const { rows, err } = query<StructureShort & { count: number }>(
+		sql`
+			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
+			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
+}

src/lib/server/compare.ts src/lib/server/fetchers/comparison.tssrc/lib/server/compare.ts renamed to src/lib/server/fetchers/comparison.ts

@@ -1,18 +1,16 @@
-import { error, type RequestEvent } from '@sveltejs/kit'
+import { error } from '@sveltejs/kit'
 import { query } from '$lib/server/db.catdat'
 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'
 import { PLURALS } from '$lib/commons/structures'
+import { to_placeholders } from '$lib/server/utils'
 
-export function compare_handler(
-	event: RequestEvent,
+export function fetch_comparison_result(
+	compared_ids: string[],
 	type: StructureType,
+	callback: () => void,
 ): ComparisonResult {
-	if (!event.params.ids) error(400, `No ${type} selected for comparison`)
-
-	const compared_ids = event.params.ids?.split('/')
-
 	if (!compared_ids.length) error(400, `No ${type} selected for comparison`)
 
 	if (compared_ids.length > MAX_STRUCTURES_COMPARE) {
@@ -22,8 +20,6 @@ export function compare_handler(
 		)
 	}
 
-	const placeholders = compared_ids.map(() => '?').join(', ')
-
 	const { rows, err: err_cat } = query<{
 		id: string
 		name: string
@@ -32,7 +28,8 @@ export function compare_handler(
 		sql: `
 			SELECT id, name, notation 
 			FROM structures
-			WHERE type = ? AND id in (${placeholders})`,
+			WHERE type = ?
+			AND id in (${to_placeholders(compared_ids)})`,
 		values: [type, ...compared_ids],
 	})
 
@@ -69,7 +66,7 @@ export function compare_handler(
 
 	values.push(type)
 
-	const stmt = `
+	const comparison_query = `
 		SELECT
 			p.id AS property_id,
 			${select_columns}
@@ -79,18 +76,15 @@ export function compare_handler(
 		ORDER BY lower(p.id)`
 
 	const { rows: comparison_objects, err } = query<Record<string, string>>({
-		sql: stmt,
+		sql: comparison_query,
 		values,
 	})
 
-	if (err) error(500, 'Could not load properties')
+	if (err) error(500, 'Could not load comparison table')
 
 	const comparison_table = comparison_objects.map((obj) => Object.values(obj))
 
-	event.setHeaders({
-		// shared cache for 30min
-		'cache-control': 'public, max-age=0, s-maxage=1800',
-	})
+	callback()
 
 	return {
 		structures: render_nested_formulas(structures),

src/lib/server/fetchers/content.ts

@@ -0,0 +1,38 @@
+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'
+
+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} || '%'
+        `,
+	])
+
+	if (err_categories) error(500, 'Could not load context')
+
+	const [categories, category_properties, category_implications] = results
+
+	return { categories, category_properties, category_implications }
+}

src/lib/server/fetchers/functor.ts

@@ -0,0 +1,38 @@
+import type { FunctorSpecificDisplay } from '$lib/commons/types'
+import sql from 'sql-template-tag'
+import { query } from '$lib/server/db.catdat'
+import { error } from '@sveltejs/kit'
+
+export function fetch_functor(id: string) {
+	const { rows: functors, err } = query<FunctorSpecificDisplay>(
+		// specific information for the functor
+		sql`
+            SELECT
+                f.source,
+                f.target,
+                source.name AS source_name,
+                source.notation AS source_notation,
+                target.name AS target_name,
+                target.notation AS target_notation,
+                la.id AS left_adjoint,
+                la.name AS left_adjoint_name,
+                la.notation AS left_adjoint_notation,
+                ra.id AS right_adjoint,
+                ra.name AS right_adjoint_name,
+                ra.notation AS right_adjoint_notation
+            FROM functors f
+            INNER JOIN structures AS source ON source.id = f.source
+            INNER JOIN structures AS target ON target.id = f.target
+            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}
+        `,
+	)
+
+	if (err) error(500, 'Could not load functor')
+
+	if (!functors.length) error(404, `Could not find functor with ID '${id}'`)
+
+	return functors[0]
+}

src/lib/server/fetchers/implication.ts

@@ -18,21 +18,15 @@ export function fetch_implication(type: StructureType, id: string) {
                 target_assumptions,
                 conclusions
             FROM implications_view
-            WHERE
-                type = ${type}
-                AND id = ${id}
+            WHERE id = ${id}
         `,
 		sql`
-            SELECT s.id, s.name
-            FROM structures s
-            WHERE s.type = ${type}
-            AND EXISTS (
-                SELECT 1 FROM property_assignments cp
-                WHERE
-                    cp.type = ${type}
-                    AND cp.structure_id = s.id
-                    AND cp.proof LIKE '%/' || ${type} || '-implication/' || ${id} || '%'
-            )
+            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} || '%'
         `,
 	])
 

src/lib/server/fetchers/implications.ts

@@ -1,8 +1,13 @@
 import { query } from '$lib/server/db.catdat'
 import sql from 'sql-template-tag'
 import { error } from '@sveltejs/kit'
-import type { ImplicationDB, StructureType } from '$lib/commons/types'
+import type {
+	ImplicationDB,
+	NormalizedImplication,
+	StructureType,
+} from '$lib/commons/types'
 import { display_implication } from '$lib/server/transforms'
+import { parse_json_set } from '$lib/server/utils'
 
 export function fetch_implications(type: StructureType) {
 	const { rows, err } = query<ImplicationDB>(sql`
@@ -27,3 +32,63 @@ export function fetch_implications(type: StructureType) {
 
 	return { implications }
 }
+
+/**
+ * List of normalized implications of a given type that have,
+ * in the case of functors, no source and no target assumptions,
+ * 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
+		source_assumptions: string
+		target_assumptions: string
+		conclusions: string
+	}>(
+		sql`
+			SELECT
+				id,
+				is_equivalence,
+				assumptions,
+				source_assumptions,
+				target_assumptions,
+				conclusions
+			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<string>(impl.assumptions)
+		const source_assumptions = parse_json_set<string>(impl.source_assumptions)
+		const target_assumptions = parse_json_set<string>(impl.target_assumptions)
+		const conclusions = parse_json_set<string>(impl.conclusions)
+
+		if (source_assumptions.size > 0 || target_assumptions.size > 0) 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 }
+}