diff --git a/src/components/PropertyAssignmentList.svelte b/src/components/PropertyAssignmentList.svelte
new file mode 100644
index 00000000..55ad116f
--- /dev/null
+++ b/src/components/PropertyAssignmentList.svelte
@@ -0,0 +1,134 @@
+
+
+
+ New here? Click any
+ icon to view the proof for that property.
+
+
+
+
+
Satisfied Properties
+
+ {#if assignment_level.value === 'all'}
+
Assigned properties
+ !p.is_deduced)}
+ {type}
+ />
+
+
Deduced properties
+ p.is_deduced)}
+ {type}
+ />
+ {:else if assignment_level.value === 'merged'}
+
+ {:else if assignment_level.value === 'basic'}
+
Assigned properties; further properties can be deduced.
+ !p.is_deduced)}
+ {type}
+ />
+ {/if}
+
+
+
+
Unsatisfied Properties
+
+ {#if assignment_level.value === 'all'}
+
Assigned properties
+ !p.is_deduced)}
+ {type}
+ />
+
+
Deduced properties*
+ p.is_deduced)}
+ {type}
+ />
+
+
*This also uses the deduced satisfied properties.
+ {:else if assignment_level.value === 'merged'}
+
+ {:else if assignment_level.value === 'basic'}
+
Assigned properties; further properties can be deduced.
+ !p.is_deduced)}
+ {type}
+ />
+ {/if}
+
+
+
+
+
Unknown properties
+
+ {#if unknown_properties.length > 0}
+
+ {pluralize(unknown_properties.length, {
+ one: "There is {count} property for which the database doesn't have an answer if it is satisfied or not.",
+ other: "There are {count} properties for which the database doesn't have an answer if they are satisfied or not.",
+ })}
+
+ Please help to contribute the data!
+
+ {pluralize(undecidable_properties.length, {
+ one: 'There is {count} property for which it cannot be decided if it is satisfied or not.',
+ other: 'There are {count} properties for which it cannot be decided if they are satisfied or not.',
+ })}
+
+ These {PLURALS[type]} in the database currently have exactly the same properties
+ as the {name}. This indicates that the data may be incomplete or that a
+ distinguishing property may be missing from the database.
+
+
+
+
+{/if}
diff --git a/src/lib/client/config.ts b/src/lib/client/config.ts
deleted file mode 100644
index 6e309903..00000000
--- a/src/lib/client/config.ts
+++ /dev/null
@@ -1 +0,0 @@
-export const STRUCTURES = ['categories', 'functors']
diff --git a/src/lib/client/nav.ts b/src/lib/client/nav.ts
new file mode 100644
index 00000000..caac1959
--- /dev/null
+++ b/src/lib/client/nav.ts
@@ -0,0 +1,100 @@
+import type { StructureType } from '$lib/commons/types'
+import {
+ faArrowsSplitUpAndLeft,
+ faBook,
+ faChartBar,
+ faCog,
+ faCubes,
+ faDatabase,
+ faDownload,
+ faHome,
+ faList,
+ faPenToSquare,
+ faPuzzlePiece,
+ faSearch,
+ type IconDefinition,
+} from '@fortawesome/free-solid-svg-icons'
+import { capitalize } from './utils'
+import { PLURALS } from '$lib/commons/structures'
+
+type Link = {
+ href: string
+ text: string
+ nested?: string
+ icon: IconDefinition
+}
+
+export function get_navigation_links(type: StructureType): Link[] {
+ return [
+ {
+ href: '/',
+ text: 'Home',
+ icon: faHome,
+ },
+ {
+ href: `/${PLURALS[type]}`,
+ text: capitalize(PLURALS[type]),
+ nested: `/${type}/`,
+ icon: faDatabase,
+ },
+ {
+ href: `/${type}-properties`,
+ text: `Properties`,
+ nested: `/${type}-property/`,
+ icon: faList,
+ },
+ {
+ href: `/${type}-implications`,
+ text: `Implications`,
+ nested: `/${type}-implication`,
+ icon: faArrowsSplitUpAndLeft,
+ },
+ {
+ href: `/${type}-comparison`,
+ text: `Compare`,
+ icon: faChartBar,
+ nested: `/${type}-comparison`,
+ },
+ {
+ href: `/${type}-search`,
+ text: `Search`,
+ icon: faSearch,
+ nested: `/${type}-search/results`,
+ },
+ ]
+}
+
+export function get_footer_links() {
+ return [
+ {
+ href: '/content/contribute',
+ text: 'Contribute',
+ icon: faPenToSquare,
+ },
+ {
+ href: '/settings',
+ text: 'Settings',
+ icon: faCog,
+ },
+ {
+ href: '/missing',
+ text: 'Missing data',
+ icon: faPuzzlePiece,
+ },
+ {
+ href: '/content/resources',
+ text: 'Resources',
+ icon: faBook,
+ },
+ {
+ href: '/content/foundations',
+ text: 'Foundations',
+ icon: faCubes,
+ },
+ {
+ href: '/download',
+ text: 'Download',
+ icon: faDownload,
+ },
+ ]
+}
diff --git a/src/lib/client/utils.ts b/src/lib/client/utils.ts
index a8d57074..08731e49 100644
--- a/src/lib/client/utils.ts
+++ b/src/lib/client/utils.ts
@@ -1,4 +1,3 @@
-import { goto } from '$app/navigation'
import type { Attachment } from 'svelte/attachments'
export function get_device_type() {
@@ -8,15 +7,15 @@ export function get_device_type() {
return 'desktop'
}
-export function filter_by_tag(tag: string) {
- goto(`/categories/${tag}`)
-}
-
export function pluralize(count: number, forms: { one: string; other: string }) {
const word = count === 1 ? forms.one : forms.other
return word.replace('{count}', String(count))
}
+export function capitalize(txt: string) {
+ return txt[0].toUpperCase() + txt.slice(1)
+}
+
/**
* Removes accents from letters and transforms to lowercase
*/
diff --git a/src/lib/commons/compare.utils.ts b/src/lib/commons/compare.utils.ts
new file mode 100644
index 00000000..e91e4777
--- /dev/null
+++ b/src/lib/commons/compare.utils.ts
@@ -0,0 +1,30 @@
+import { browser } from '$app/environment'
+import type { StructureType } from './types'
+import { is_string_array } from './utils'
+
+export const MAX_STRUCTURES_COMPARE = 10
+
+export function get_compared_structures(type: StructureType): string[] {
+ if (!browser) return []
+
+ const names_string = window.sessionStorage.getItem(`comparison:${type}`)
+ if (!names_string) return []
+
+ try {
+ const parsed_names: unknown = JSON.parse(names_string)
+ const is_valid = is_string_array(parsed_names)
+ return is_valid ? parsed_names : []
+ } catch {
+ console.error('Error parsing saved structured from sessionStorage')
+ return []
+ }
+}
+
+export function save_comparison(type: StructureType, compared_categories: string[]) {
+ if (!browser) return
+
+ window.sessionStorage.setItem(
+ `comparison:${type}`,
+ JSON.stringify(compared_categories),
+ )
+}
diff --git a/src/lib/commons/property.url.ts b/src/lib/commons/property.url.ts
index 3d9afbe8..6fb6598c 100644
--- a/src/lib/commons/property.url.ts
+++ b/src/lib/commons/property.url.ts
@@ -1,3 +1,5 @@
+import type { StructureType } from './types'
+
const ENCODE_MAP: Record = {
' ': '_',
'ℵ₀': 'aleph0',
@@ -28,6 +30,6 @@ export function decode_property_ID(str: string): string {
return decoded
}
-export function get_property_url(id: string, type: 'category' | 'functor') {
+export function get_property_url(id: string, type: StructureType) {
return `/${type}-property/${encode_property_ID(id)}`
}
diff --git a/src/lib/commons/structures.ts b/src/lib/commons/structures.ts
new file mode 100644
index 00000000..12584308
--- /dev/null
+++ b/src/lib/commons/structures.ts
@@ -0,0 +1,8 @@
+import type { StructureType } from './types'
+
+export const STRUCTURES: StructureType[] = ['category', 'functor']
+
+export const PLURALS = {
+ category: 'categories',
+ functor: 'functors',
+}
diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts
index bed2e1ef..61c5fcd9 100644
--- a/src/lib/commons/types.ts
+++ b/src/lib/commons/types.ts
@@ -4,6 +4,15 @@ export type Arrayed = {
type Replace>> = Omit & R
+export type StructureType = 'category' | 'functor'
+
+export type StructureShort = {
+ id: string
+ name: string
+}
+
+export type RelatedStructure = StructureShort & { notation: string }
+
export type CategoryDisplay = {
id: string
name: string
@@ -17,34 +26,10 @@ export type CategoryDisplay = {
dual_category_notation: string | null
}
-export type CategoryShort = Pick
-
-export type RelatedCategory = Pick
-
export type TagObject = { tag: string }
export type CommentObject = { id: number; comment: string }
-export type ImplicationDB = {
- id: string
- is_equivalence: 0 | 1
- reason: string
- assumptions: string
- conclusions: string
- is_deduced: 0 | 1
- dualized_from?: string | null
-}
-
-export type ImplicationDisplay = Replace<
- ImplicationDB,
- {
- is_equivalence: boolean
- is_deduced: boolean
- assumptions: string[]
- conclusions: string[]
- }
->
-
export type PropertyDB = {
id: string
relation: string
@@ -61,19 +46,25 @@ export type PropertyDisplay = Replace<
export type PropertyShort = Pick
-export type DescriptionWithReason = {
- description: string
- reason: string | null
-}
+export type GroupedPropertyShort = Pick<
+ PropertyDB,
+ 'id' | 'relation' | 'dual_property_id'
+>
-export type CategoryPropertyDB = {
+export type PropertyAssignmentDB = {
id: string
reason: string
relation: string
is_deduced: 0 | 1
+ is_satisfied: 0 | 1 | null
}
-export type CategoryProperty = Replace
+export type PropertyAssignmentDisplay = {
+ id: string
+ reason: string
+ relation: string
+ is_deduced: boolean
+}
export type SpecialObject = {
type: string
@@ -86,16 +77,10 @@ export type SpecialMorphism = {
reason: string
}
-export type Structure = 'categories' | 'functors'
-
-export type FunctorShort = {
- id: string
- name: string
-}
-
-export type FunctorDB = {
+export type FunctorDisplay = {
id: string
name: string
+ notation: string
source: string
target: string
source_name: string
@@ -104,54 +89,43 @@ export type FunctorDB = {
nlab_link: string | null
}
-export type FunctorPropertyDB = {
- id: string
- relation: string
- description: string
- nlab_link: string | null
- invariant_under_equivalences: 0 | 1
- dual_property_id: string | null
-}
-
-export type FunctorPropertyShort = Pick
-
-export type FunctorProperty = Replace<
- FunctorPropertyDB,
- {
- invariant_under_equivalences: boolean
- }
->
-
-export type FunctorImplicationDB = {
+export type ImplicationDB = {
id: string
is_equivalence: 0 | 1
+ is_deduced: 0 | 1
+ dualized_from: string | null
reason: string
assumptions: string
conclusions: string
- source_assumptions: string
- target_assumptions: string
- dualized_from?: string | null
+ source_assumptions?: string // for functors
+ target_assumptions?: string // for functors
}
-export type FunctorImplicationDisplay = Replace<
- FunctorImplicationDB,
+export type ImplicationDisplay = Replace<
+ ImplicationDB,
{
is_equivalence: boolean
+ is_deduced: boolean
assumptions: string[]
conclusions: string[]
- source_assumptions: string[]
- target_assumptions: string[]
+ source_assumptions?: string[]
+ target_assumptions?: string[]
}
>
-export type FunctorPropertyAssignmentDB = {
- id: string
- reason: string
- relation: string
- is_deduced: 0 | 1
+export type SearchResults = {
+ type: StructureType
+ contradiction: string[] | null
+ satisfied_properties: string[]
+ unsatisfied_properties: string[]
+ dual_satisfied_properties: (string | null)[]
+ dual_unsatisfied_properties: (string | null)[]
+ dual_search_available: boolean
+ found_structures: StructureShort[]
}
-export type FunctorPropertyAssignment = Replace<
- FunctorPropertyAssignmentDB,
- { is_deduced: boolean }
->
+export type ComparisonResult = {
+ type: StructureType
+ structures: RelatedStructure[]
+ comparison_table: string[][]
+}
diff --git a/src/lib/server/compare.ts b/src/lib/server/compare.ts
new file mode 100644
index 00000000..9309ab38
--- /dev/null
+++ b/src/lib/server/compare.ts
@@ -0,0 +1,97 @@
+import { error, type RequestEvent } 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'
+
+export function compare_handler(
+ event: RequestEvent,
+ type: StructureType,
+): 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) {
+ error(
+ 400,
+ `It is only possible to compare up to ${MAX_STRUCTURES_COMPARE} ${PLURALS[type]}`,
+ )
+ }
+
+ const placeholders = compared_ids.map(() => '?').join(', ')
+
+ const { rows, err: err_cat } = query<{
+ id: string
+ name: string
+ notation: string
+ }>({
+ sql: `
+ SELECT id, name, notation
+ FROM ${PLURALS[type]}
+ WHERE id in (${placeholders})`,
+ values: compared_ids,
+ })
+
+ if (err_cat) error(500, `Could not load ${PLURALS[type]}`)
+
+ const invalid_id = compared_ids.find((id) => rows.every((row) => row.id !== id))
+ if (invalid_id) error(404, `Could not find ${type} with ID '${invalid_id}'`)
+
+ const structures = rows.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 ${type}_property_assignments a${i}
+ ON a${i}.property_id = p.id AND a${i}.${type}_id = ?
+ `)
+ values.push(id)
+ })
+
+ const stmt = `
+ SELECT
+ p.id AS property_id,
+ ${select_columns}
+ FROM ${type}_properties p
+ ${join_fragments.join('\n')}
+ ORDER BY lower(p.id)`
+
+ const { rows: comparison_objects, err } = query>({
+ sql: stmt,
+ values,
+ })
+
+ if (err) error(500, 'Could not load properties')
+
+ 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',
+ })
+
+ return {
+ type,
+ structures: render_nested_formulas(structures),
+ comparison_table,
+ }
+}
diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts
index 5a6caee1..fbf94cdf 100644
--- a/src/lib/server/consistency.ts
+++ b/src/lib/server/consistency.ts
@@ -1,42 +1,49 @@
import sql from 'sql-template-tag'
import { query } from '$lib/server/db.catdat'
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'
// TODO: If possible, remove the code duplication with deduction and redundancy scripts.
-type NormalizedCategoryImplication = {
- id: string
- assumptions: Set
- conclusion: string
-}
-
export function get_contradiction(
satisfied_properties: Set,
unsatisfied_properties: Set,
-): string[] | null {
+ type: StructureType,
+): { contradiction: string[] | null; err: SqliteError | null } {
for (const p of satisfied_properties) {
- if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`]
+ const contradiction = [`${p} ⟹ ${p}`]
+ if (unsatisfied_properties.has(p)) return { contradiction, err: null }
}
- const implications = get_normalized_category_implications()
+ const { implications, err } = get_normalized_implications(type)
+
+ if (err) return { contradiction: null, err }
- return contradiction_worker(
+ const contradiction = contradiction_worker(
satisfied_properties,
unsatisfied_properties,
implications,
)
+
+ return { contradiction, err: null }
}
function contradiction_worker(
satisfied_properties: Set,
unsatisfied_properties: Set,
- implications: NormalizedCategoryImplication[],
+ implications: NormalizedImplication[],
): string[] | null {
for (const p of satisfied_properties) {
if (unsatisfied_properties.has(p)) return [`${p} ⟹ ${p}`]
}
- const deduction_dict: Record = {}
+ const deduction_dict: Record = {}
const deduced_satisfied_properties = new Set(satisfied_properties)
// bfs to find contradiction
@@ -78,7 +85,7 @@ function contradiction_worker(
function build_shortest_proof(
satisfied_properties: Set,
- deduction_dict: Record,
+ deduction_dict: Record,
target_property: string,
) {
const proof: string[] = []
@@ -103,55 +110,17 @@ function build_shortest_proof(
return proof
}
-function get_normalized_category_implications() {
- const { rows, err } = query<{
- id: string
- assumptions: string
- conclusions: string
- is_equivalence: 0 | 1
- }>(
- sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`,
- )
-
- if (err) throw err
-
- const implications: NormalizedCategoryImplication[] = []
-
- for (const impl of rows) {
- const assumptions = new Set(JSON.parse(impl.assumptions))
- const conclusions = new Set(JSON.parse(impl.conclusions))
-
- 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
-}
-
-function stringify_implication(implication: NormalizedCategoryImplication) {
- return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}`
-}
-
export function get_missing_combinations() {
- const implications = get_normalized_category_implications()
+ const { implications, err: err_imp } = get_normalized_implications('category')
+
+ if (err_imp) return { err: err_imp, missing_combinations: [] }
const { rows: properties, err } = query<{
id: string
dual_property_id: string | null
}>(sql`SELECT id, dual_property_id FROM category_properties ORDER BY lower(id)`)
- if (err) throw err
+ if (err) return { err, missing_combinations: [] }
const { rows: existing, err: err_existing } = query<{
p: string
@@ -164,11 +133,11 @@ export function get_missing_combinations() {
WHERE cp.is_satisfied = TRUE AND cnp.is_satisfied = FALSE
`)
- if (err_existing) throw err_existing
+ if (err_existing) return { err: err_existing, missing_combinations: [] }
const witnessed_pairs = new Set(existing.map(({ p, q }) => `${p}|${q}`))
- const missing_pairs: [string, string][] = []
+ const missing_combinations: [string, string][] = []
for (const p of properties) {
for (const q of properties) {
@@ -190,9 +159,9 @@ export function get_missing_combinations() {
implications,
)
- if (!contradiction) missing_pairs.push([p.id, q.id])
+ if (!contradiction) missing_combinations.push([p.id, q.id])
}
}
- return missing_pairs
+ return { missing_combinations, err: null }
}
diff --git a/src/lib/server/db.catdat.ts b/src/lib/server/db.catdat.ts
index 1d065f59..e61c4cf6 100644
--- a/src/lib/server/db.catdat.ts
+++ b/src/lib/server/db.catdat.ts
@@ -1,5 +1,5 @@
import type { Arrayed } from '$lib/commons/types'
-import Database, { SqliteError } from 'better-sqlite3'
+import Database, { type SqliteError } from 'better-sqlite3'
import path from 'node:path'
const db_path = path.resolve('databases', 'catdat', 'catdat.db')
diff --git a/src/lib/server/implications.ts b/src/lib/server/implications.ts
new file mode 100644
index 00000000..2160e127
--- /dev/null
+++ b/src/lib/server/implications.ts
@@ -0,0 +1,114 @@
+import sql from 'sql-template-tag'
+import { query } from './db.catdat'
+import { parse_json_set } from './utils'
+import type { StructureType } from '$lib/commons/types'
+
+// TODO: If possible, remove the code duplication with deduction and redundancy scripts.
+
+export type NormalizedImplication = {
+ id: string
+ assumptions: Set
+ conclusion: string
+}
+
+/**
+ * List of normalized implications of a given type of structure.
+ */
+export function get_normalized_implications(type: StructureType) {
+ if (type === 'category') return get_normalized_category_implications()
+ if (type === 'functor') return get_normalized_functor_implications()
+ throw new Error('Unsupported type')
+}
+
+/**
+ * List of normalized implications of categories.
+ */
+function get_normalized_category_implications() {
+ const { rows, err } = query<{
+ id: string
+ assumptions: string
+ conclusions: string
+ is_equivalence: 0 | 1
+ }>(
+ sql`SELECT id, assumptions, conclusions, is_equivalence FROM category_implications_view`,
+ )
+
+ 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)
+
+ 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 }
+}
+
+/**
+ * List of normalized implications of functors that have no source or target
+ * assumptions, i.e. those that are universally true. Only those are relevant
+ * for the consistency check.
+ */
+function get_normalized_functor_implications() {
+ const { rows, err } = query<{
+ id: string
+ assumptions: string
+ conclusions: string
+ source_assumptions: string
+ target_assumptions: string
+ is_equivalence: 0 | 1
+ }>(
+ sql`
+ SELECT id, assumptions, source_assumptions, target_assumptions,
+ conclusions, is_equivalence
+ FROM functor_implications_view`,
+ )
+
+ if (err) return { implications: null, err }
+
+ const implications: NormalizedImplication[] = []
+
+ for (const impl of rows) {
+ const assumptions = parse_json_set(impl.assumptions)
+ const source_assumptions = parse_json_set(impl.source_assumptions)
+ const target_assumptions = parse_json_set(impl.target_assumptions)
+ const conclusions = parse_json_set(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 }
+}
+
+export function stringify_implication(implication: NormalizedImplication) {
+ return `${[...implication.assumptions].join(' ∧ ')} ⟹ ${implication.conclusion}`
+}
diff --git a/src/lib/server/properties.ts b/src/lib/server/properties.ts
new file mode 100644
index 00000000..b275757b
--- /dev/null
+++ b/src/lib/server/properties.ts
@@ -0,0 +1,14 @@
+import type { StructureType } from '$lib/commons/types'
+import { query } from './db.catdat'
+import { error } from '@sveltejs/kit'
+
+export function get_property_ids(type: StructureType) {
+ const { rows, err } = query<{ id: string }>({
+ sql: `SELECT id FROM ${type}_properties ORDER BY lower(id)`,
+ values: [],
+ })
+
+ if (err) error(500, 'Failed to load properties')
+
+ return rows.map(({ id }) => id)
+}
diff --git a/src/lib/server/search.ts b/src/lib/server/search.ts
index 538a64fc..246afeae 100644
--- a/src/lib/server/search.ts
+++ b/src/lib/server/search.ts
@@ -2,16 +2,19 @@ import type { RequestEvent } from '@sveltejs/kit'
import { decode_property_ID } from '$lib/commons/property.url'
import { query } from '$lib/server/db.catdat'
import { error } from '@sveltejs/kit'
-import sql from 'sql-template-tag'
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 './utils'
+import { PLURALS } from '$lib/commons/structures'
-type NamedObject = {
- id: string
- name: string
+function cache_page(event: RequestEvent) {
+ event.setHeaders({
+ 'cache-control': 'public, max-age=0, s-maxage=1800', // shared cache for 30min
+ })
}
-export function search_handler(event: RequestEvent, type: 'category' | 'functor') {
+export function search_handler(event: RequestEvent, type: StructureType): SearchResults {
const satisfied_query = event.url.searchParams.get('satisfied')
const unsatisfied_query = event.url.searchParams.get('unsatisfied')
@@ -22,11 +25,14 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
const { rows: all_properties_objects, err: err_all } = query<{
id: string
dual_property_id: string | null
- }>(get_property_query(type))
+ }>({
+ sql: `SELECT id, dual_property_id FROM ${type}_properties ORDER BY lower(id)`,
+ values: [],
+ })
if (err_all) error(500, 'Failed to load properties')
- const all_properties = all_properties_objects.map(({ id }) => id)
+ const all_properties = new Set(all_properties_objects.map(({ id }) => id))
const dual_properties_dict: Record = {}
for (const row of all_properties_objects) {
@@ -38,7 +44,7 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
: []
const invalid_satisfied_property = satisfied_properties.find(
- (p) => !all_properties.includes(p),
+ (p) => !all_properties.has(p),
)
if (invalid_satisfied_property) {
@@ -50,7 +56,7 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
: []
const invalid_unsatisfied_property = unsatisfied_properties.find(
- (p) => !all_properties.includes(p),
+ (p) => !all_properties.has(p),
)
if (invalid_unsatisfied_property) {
@@ -69,46 +75,60 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
dual_satisfied_properties.every(Boolean) &&
dual_unsatisfied_properties.every(Boolean)
- // TODO: implement this for functors as well
- if (type === 'category') {
- try {
- const contradiction = get_contradiction(
- new Set(satisfied_properties),
- new Set(unsatisfied_properties),
- )
-
- if (contradiction) {
- event.setHeaders({
- // shared cache for 30min
- 'cache-control': 'public, max-age=0, s-maxage=1800',
- })
-
- return {
- contradiction,
- all_properties,
- satisfied_properties,
- unsatisfied_properties,
- found_objects: [],
- dual_satisfied_properties,
- dual_unsatisfied_properties,
- dual_search_available,
- }
- }
- } catch (err) {
- error(500, 'Consistency check failed')
- }
- }
-
- const all_selected_properties = satisfied_properties.concat(unsatisfied_properties)
-
- const search_query = get_search_query(
- satisfied_properties,
- unsatisfied_properties,
- all_selected_properties,
+ const { contradiction, err: err_con } = get_contradiction(
+ new Set(satisfied_properties),
+ new Set(unsatisfied_properties),
type,
)
- const { rows: found_objects, err } = query({
+ if (err_con) error(500, 'Consistency check failed')
+
+ if (contradiction) {
+ cache_page(event)
+
+ return {
+ type,
+ contradiction,
+ satisfied_properties,
+ unsatisfied_properties,
+ dual_satisfied_properties,
+ dual_unsatisfied_properties,
+ dual_search_available,
+ found_structures: [],
+ }
+ }
+
+ const all_selected_properties = [...satisfied_properties, ...unsatisfied_properties]
+
+ const search_query = `
+ SELECT s.id, s.name FROM ${PLURALS[type]} s
+ INNER JOIN ${type}_property_assignments a ON a.${type}_id = s.id
+ WHERE property_id IN (${to_placeholders(all_selected_properties)})
+ GROUP BY ${type}_id
+ HAVING
+ SUM (
+ CASE
+ WHEN
+ property_id IN (${to_placeholders(satisfied_properties)})
+ AND is_satisfied = TRUE
+ THEN 1
+ ELSE 0
+ END
+ ) = ${satisfied_properties.length}
+ AND
+ SUM(
+ CASE
+ WHEN
+ property_id IN (${to_placeholders(unsatisfied_properties)})
+ AND is_satisfied = FALSE
+ THEN 1
+ ELSE 0
+ END
+ ) = ${unsatisfied_properties.length}
+ ORDER BY lower(s.name)
+ `
+
+ const { rows: found_structures, err } = query({
sql: search_query,
values: [
...all_selected_properties,
@@ -119,102 +139,16 @@ export function search_handler(event: RequestEvent, type: 'category' | 'functor'
if (err) error(500, 'Search failed')
- event.setHeaders({
- // shared cache for 30min
- 'cache-control': 'public, max-age=0, s-maxage=1800',
- })
+ cache_page(event)
return {
+ type,
contradiction: null,
- all_properties,
satisfied_properties,
unsatisfied_properties,
- found_objects,
dual_satisfied_properties,
dual_unsatisfied_properties,
dual_search_available,
+ found_structures,
}
}
-
-function get_property_query(type: 'category' | 'functor') {
- if (type === 'category') {
- return sql`SELECT id, dual_property_id FROM category_properties ORDER BY lower(id)`
- }
- if (type === 'functor') {
- return sql`SELECT id, dual_property_id FROM functor_properties ORDER BY lower(id)`
- }
- throw new Error('Invalid type')
-}
-
-function to_placeholders(arr: string[]): string {
- return arr.map(() => '?').join(', ')
-}
-
-function get_search_query(
- satisfied_properties: string[],
- unsatisfied_properties: string[],
- all_selected_properties: string[],
- type: 'category' | 'functor',
-) {
- if (type === 'category') {
- return `
- SELECT c.id, c.name FROM categories c
- INNER JOIN category_property_assignments cp ON cp.category_id = c.id
- WHERE property_id IN (${to_placeholders(all_selected_properties)})
- GROUP BY category_id
- HAVING
- SUM (
- CASE
- WHEN
- property_id IN (${to_placeholders(satisfied_properties)})
- AND is_satisfied = TRUE
- THEN 1
- ELSE 0
- END
- ) = ${satisfied_properties.length}
- AND
- SUM(
- CASE
- WHEN
- property_id IN (${to_placeholders(unsatisfied_properties)})
- AND is_satisfied = FALSE
- THEN 1
- ELSE 0
- END
- ) = ${unsatisfied_properties.length}
- ORDER BY lower(c.name)
- `
- }
-
- if (type === 'functor') {
- return `
- SELECT f.id, f.name FROM functors f
- INNER JOIN functor_property_assignments fp ON fp.functor_id = f.id
- WHERE property_id IN (${to_placeholders(all_selected_properties)})
- GROUP BY functor_id
- HAVING
- SUM (
- CASE
- WHEN
- property_id IN (${to_placeholders(satisfied_properties)})
- AND is_satisfied = TRUE
- THEN 1
- ELSE 0
- END
- ) = ${satisfied_properties.length}
- AND
- SUM(
- CASE
- WHEN
- property_id IN (${to_placeholders(unsatisfied_properties)})
- AND is_satisfied = FALSE
- THEN 1
- ELSE 0
- END
- ) = ${unsatisfied_properties.length}
- ORDER BY lower(f.name)
- `
- }
-
- throw new Error('Invalid type')
-}
diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts
new file mode 100644
index 00000000..dbb08a07
--- /dev/null
+++ b/src/lib/server/transforms.ts
@@ -0,0 +1,48 @@
+import type {
+ PropertyDB,
+ PropertyDisplay,
+ PropertyAssignmentDB,
+ PropertyAssignmentDisplay,
+ ImplicationDB,
+ ImplicationDisplay,
+} from '$lib/commons/types'
+
+export function display_property(property: PropertyDB): PropertyDisplay {
+ return {
+ id: property.id,
+ relation: property.relation,
+ description: property.description,
+ dual_property_id: property.dual_property_id,
+ nlab_link: property.nlab_link,
+ invariant_under_equivalences: Boolean(property.invariant_under_equivalences),
+ }
+}
+
+export function display_property_assignment(
+ property: PropertyAssignmentDB,
+): PropertyAssignmentDisplay {
+ return {
+ id: property.id,
+ reason: property.reason,
+ is_deduced: Boolean(property.is_deduced),
+ relation: property.relation,
+ }
+}
+
+export function display_implication(implication: ImplicationDB): ImplicationDisplay {
+ return {
+ id: implication.id,
+ is_equivalence: Boolean(implication.is_equivalence),
+ is_deduced: Boolean(implication.is_deduced),
+ dualized_from: implication.dualized_from,
+ reason: implication.reason,
+ assumptions: JSON.parse(implication.assumptions),
+ source_assumptions: implication.source_assumptions
+ ? JSON.parse(implication.source_assumptions)
+ : undefined,
+ target_assumptions: implication.target_assumptions
+ ? JSON.parse(implication.target_assumptions)
+ : undefined,
+ conclusions: JSON.parse(implication.conclusions),
+ }
+}
diff --git a/src/lib/server/utils.ts b/src/lib/server/utils.ts
index 20d4ec3f..ab5fbc3c 100644
--- a/src/lib/server/utils.ts
+++ b/src/lib/server/utils.ts
@@ -1,18 +1,3 @@
-import type {
- CategoryProperty,
- CategoryPropertyDB,
- FunctorImplicationDB,
- FunctorImplicationDisplay,
- FunctorProperty,
- FunctorPropertyAssignment,
- FunctorPropertyAssignmentDB,
- FunctorPropertyDB,
- ImplicationDB,
- ImplicationDisplay,
- PropertyDB,
- PropertyDisplay,
-} from '$lib/commons/types'
-
export function is_object(obj: unknown): obj is Record {
return obj != null && obj.constructor.name === 'Object'
}
@@ -24,75 +9,12 @@ export function is_subset(a: Set, b: Set) {
return true
}
-export const sleep = (delay: number) => new Promise((res) => setTimeout(res, delay))
-
-export function display_implication(implication: ImplicationDB): ImplicationDisplay {
- return {
- id: implication.id,
- is_equivalence: Boolean(implication.is_equivalence),
- reason: implication.reason,
- is_deduced: Boolean(implication.is_deduced),
- assumptions: JSON.parse(implication.assumptions),
- conclusions: JSON.parse(implication.conclusions),
- dualized_from: implication.dualized_from,
- }
+export function to_placeholders(arr: string[]): string {
+ return arr.map(() => '?').join(', ')
}
-export function display_property(property: PropertyDB): PropertyDisplay {
- return {
- id: property.id,
- relation: property.relation,
- description: property.description,
- dual_property_id: property.dual_property_id,
- nlab_link: property.nlab_link,
- invariant_under_equivalences: Boolean(property.invariant_under_equivalences),
- }
-}
-
-export function display_category_property_assignment(
- property: CategoryPropertyDB,
-): CategoryProperty {
- return {
- id: property.id,
- reason: property.reason,
- is_deduced: Boolean(property.is_deduced),
- relation: property.relation,
- }
-}
-
-export function display_functor_property(property: FunctorPropertyDB): FunctorProperty {
- return {
- id: property.id,
- relation: property.relation,
- description: property.description,
- dual_property_id: property.dual_property_id,
- nlab_link: property.nlab_link,
- invariant_under_equivalences: Boolean(property.invariant_under_equivalences),
- }
-}
-
-export function display_functor_property_assignment(
- property: FunctorPropertyAssignmentDB,
-): FunctorPropertyAssignment {
- return {
- id: property.id,
- reason: property.reason,
- is_deduced: Boolean(property.is_deduced),
- relation: property.relation,
- }
-}
+export const sleep = (delay: number) => new Promise((res) => setTimeout(res, delay))
-export function display_functor_implication(
- implication: FunctorImplicationDB,
-): FunctorImplicationDisplay {
- return {
- id: implication.id,
- is_equivalence: Boolean(implication.is_equivalence),
- reason: implication.reason,
- assumptions: JSON.parse(implication.assumptions),
- source_assumptions: JSON.parse(implication.source_assumptions),
- target_assumptions: JSON.parse(implication.target_assumptions),
- conclusions: JSON.parse(implication.conclusions),
- dualized_from: implication.dualized_from,
- }
+export function parse_json_set(json: string): Set {
+ return new Set(JSON.parse(json))
}
diff --git a/src/lib/states/assignment_level.svelte.ts b/src/lib/states/assignment_level.svelte.ts
new file mode 100644
index 00000000..af9586a9
--- /dev/null
+++ b/src/lib/states/assignment_level.svelte.ts
@@ -0,0 +1,33 @@
+import { browser } from '$app/environment'
+
+export const ASSIGNMENT_LEVELS = {
+ all: 'Show all properties for a structure. Indicate which properties have been manually assigned and which have been deduced. This is the default.',
+ merged: "Show all properties for a structure, but don't indicate which properties are manually assigned and which have been deduced.",
+ basic: 'Show only those properties for a structure that have been manually assigned. Deduced properties are not shown.',
+} as const
+
+type AssignmentLevel = keyof typeof ASSIGNMENT_LEVELS
+
+function is_valid_assignment_level(level: string | null): level is AssignmentLevel {
+ return level != null && Object.keys(ASSIGNMENT_LEVELS).includes(level)
+}
+
+const DEFAULT_ASSIGNMENT_LEVEL: AssignmentLevel = 'all'
+
+export const assignment_level = $state<{ value: AssignmentLevel }>({
+ value: get_saved_assignment_level(),
+})
+
+function get_saved_assignment_level(): AssignmentLevel {
+ if (!browser) return DEFAULT_ASSIGNMENT_LEVEL
+ const saved_assignment_level = localStorage.getItem('assignment_level')
+
+ return is_valid_assignment_level(saved_assignment_level)
+ ? saved_assignment_level
+ : DEFAULT_ASSIGNMENT_LEVEL
+}
+
+export function update_assignment_level(level: AssignmentLevel) {
+ if (!browser) return
+ localStorage.setItem('assignment_level', level)
+}
diff --git a/src/lib/states/detail_level.svelte.ts b/src/lib/states/detail_level.svelte.ts
deleted file mode 100644
index 63e3c491..00000000
--- a/src/lib/states/detail_level.svelte.ts
+++ /dev/null
@@ -1,35 +0,0 @@
-import { browser } from '$app/environment'
-
-export const CATEGORY_DETAIL_LEVELS = {
- all: 'Show all properties for a category. Indicate which properties have been manually assigned and which have been deduced. This is the default.',
- merged: "Show all properties for a category, but don't indicate which properties are manually assigned and which have been deduced.",
- basic: 'Show only those properties for a category that have been manually assigned. Deduced properties are not shown.',
-} as const
-
-type CategoryDetailLevel = keyof typeof CATEGORY_DETAIL_LEVELS
-
-function is_valid_category_detail_level(
- level: string | null,
-): level is CategoryDetailLevel {
- return level != null && Object.keys(CATEGORY_DETAIL_LEVELS).includes(level)
-}
-
-const DEFAULT_CATEGORY_DETAIL_LEVEL: CategoryDetailLevel = 'all'
-
-export const category_detail_level = $state<{ value: CategoryDetailLevel }>({
- value: get_saved_category_detail_level(),
-})
-
-function get_saved_category_detail_level(): CategoryDetailLevel {
- if (!browser) return DEFAULT_CATEGORY_DETAIL_LEVEL
- const saved_category_detail_level = localStorage.getItem('category_detail_level')
-
- return is_valid_category_detail_level(saved_category_detail_level)
- ? saved_category_detail_level
- : DEFAULT_CATEGORY_DETAIL_LEVEL
-}
-
-export function update_category_detail_level(level: CategoryDetailLevel) {
- if (!browser) return
- localStorage.setItem('category_detail_level', level)
-}
diff --git a/src/pages/ComparisonPage.svelte b/src/pages/ComparisonPage.svelte
new file mode 100644
index 00000000..7b34ccec
--- /dev/null
+++ b/src/pages/ComparisonPage.svelte
@@ -0,0 +1,85 @@
+
+
+
+
+
Compare {PLURALS[type]}
+
+
+ Select up to {MAX_STRUCTURES_COMPARE}
+ {PLURALS[type]} to compare their properties with each other.
+ {#if compared_structures.length === MAX_STRUCTURES_COMPARE}
+ The maximum is reached.
+ {/if}
+