Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions databases/catdat/scripts/config.ts
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
export type StructureType = 'category' | 'functor' | 'morphism'
export const STRUCTURE_TYPES = ['category', 'functor', 'morphism'] as const

export type StructureType = (typeof STRUCTURE_TYPES)[number]

export const STRUCTURE_TYPES_WITH_DUALS: StructureType[] = ['category']

export const PLURALS = {
category: 'categories',
functor: 'functors',
morphism: 'morphisms',
} as const

export const STRUCTURES: StructureType[] = ['category', 'functor', 'morphism']

export const STRUCTURES_WITH_DUALS: StructureType[] = ['category']

export const TABLES = {
category: 'categories',
functor: 'functors',
Expand Down
4 changes: 2 additions & 2 deletions databases/catdat/scripts/deduce-implications.ts
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import { STRUCTURES_WITH_DUALS, type StructureType } from './config'
import { STRUCTURE_TYPES_WITH_DUALS, type StructureType } from './config'
import { are_equal_sets, parse_nested_json_set, parse_json_set } from './utils/helpers'
import { get_client } from './utils/db'

Expand Down Expand Up @@ -161,7 +161,7 @@ export function create_dualized_implications(type: StructureType) {
* Creates all trivial implications of the form "self-dual + P ===> P^op".
*/
export function create_self_dual_implications(type: StructureType) {
if (!STRUCTURES_WITH_DUALS.includes(type)) return
if (!STRUCTURE_TYPES_WITH_DUALS.includes(type)) return

const relevant_props = db
.prepare<[StructureType], { id: string; dual: string }>(
Expand Down
4 changes: 2 additions & 2 deletions databases/catdat/scripts/deduce-structure-properties.ts
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ import {
get_proof_string,
NormalizedImplication,
} from './utils/implications'
import { STRUCTURES_WITH_DUALS, type StructureType } from './config'
import { STRUCTURE_TYPES_WITH_DUALS, type StructureType } from './config'
import { get_structures, is_dual_structure, type StructureMeta } from './utils/structures'

/**
Expand Down Expand Up @@ -428,7 +428,7 @@ export function deduce_properties_for_structures(type: StructureType) {

deduction()

if (!STRUCTURES_WITH_DUALS.includes(type)) return
if (!STRUCTURE_TYPES_WITH_DUALS.includes(type)) return

const dual_deduction = db.transaction(() => {
for (const structure of structures) {
Expand Down
4 changes: 2 additions & 2 deletions databases/catdat/scripts/seed.ts
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import type {
MorphismYaml,
} from './utils/seed.types'
import { create_schema_hash, get_saved_schema_hash } from './utils/schema'
import { PLURALS, STRUCTURES, type StructureType } from './config'
import { PLURALS, STRUCTURE_TYPES, type StructureType } from './config'

const db = get_client()

Expand Down Expand Up @@ -126,7 +126,7 @@ function seed_config() {
)

function insert_config(config: ConfigYaml) {
for (const type of STRUCTURES) {
for (const type of STRUCTURE_TYPES) {
for (const tag of config.structure_tags) {
structure_tag_insert.run(tag, type)
}
Expand Down
4 changes: 2 additions & 2 deletions databases/catdat/scripts/test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ 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, STRUCTURES, type StructureType } from './config'
import { PLURALS, STRUCTURE_TYPES, type StructureType } from './config'
import fs from 'node:fs'
import path from 'node:path'
import { decode_property_ID } from '../../../src/lib/commons/property.url'
Expand Down Expand Up @@ -242,7 +242,7 @@ function check_link_targets_exist() {

for (const { proof, error_prefix } of proofs) {
const link_regex = new RegExp(
`<a\\s+href="\\/(${STRUCTURES.join('|')})(?:-(implication|property))?\\/([^"]+)"`,
`<a\\s+href="\\/(${STRUCTURE_TYPES.join('|')})(?:-(implication|property))?\\/([^"]+)"`,
'g',
)

Expand Down
8 changes: 4 additions & 4 deletions src/components/StructureSelector.svelte
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
<script lang="ts">
import { goto } from '$app/navigation'
import { page } from '$app/state'
import { PLURALS, STRUCTURES } from '$lib/commons/structures'
import { PLURALS, STRUCTURE_TYPES } from '$lib/commons/structures'
import type { StructureType } from '$lib/commons/types'

type Props = {
Expand All @@ -24,7 +24,7 @@
} else if (path.includes('-comparison')) {
goto(`/${selected_type}-comparison`)
} else {
goto(`/${PLURALS[selected_type]}`)
goto(`/${selected_type}-list`)
}
}

Expand All @@ -33,8 +33,8 @@

<label for={id}>Structure</label>

<select {id} bind:value={selected_type} onchange={handle_change} aria-label="Structure">
{#each STRUCTURES as structure}
<select {id} bind:value={selected_type} onchange={handle_change}>
{#each STRUCTURE_TYPES as structure}
<option value={structure}>{PLURALS[structure]}</option>
{/each}
</select>
Expand Down
3 changes: 1 addition & 2 deletions src/components/TagList.svelte
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
<script lang="ts">
import { goto } from '$app/navigation'
import { PLURALS } from '$lib/commons/structures'
import type { StructureType } from '$lib/commons/types'
import Chip from './Chip.svelte'
import ChipGroup from './ChipGroup.svelte'
Expand All @@ -15,7 +14,7 @@

function filter_by_tag(tag: string) {
if (sort === 'structure') {
goto(`/${PLURALS[type]}/${tag}`)
goto(`/${type}-list/${tag}`)
} else {
goto(`/${type}-properties/${tag}`)
}
Expand Down
4 changes: 2 additions & 2 deletions src/lib/client/nav.ts
Original file line number Diff line number Diff line change
Expand Up @@ -32,9 +32,9 @@ export function get_navigation_links(type: StructureType): Link[] {
icon: faHome,
},
{
href: `/${PLURALS[type]}`,
href: `/${type}-list`,
text: capitalize(PLURALS[type]),
nested: [`/${type}/`, `/${PLURALS[type]}/`],
nested: [`/${type}/`, `/${type}-list/`],
icon: faDatabase,
},
{
Expand Down
15 changes: 9 additions & 6 deletions src/lib/commons/structures.ts
Original file line number Diff line number Diff line change
@@ -1,17 +1,20 @@
import type { StructureType } from './types'
export const STRUCTURE_TYPES = ['category', 'functor', 'morphism'] as const

export const STRUCTURES: StructureType[] = ['category', 'functor', 'morphism']
export type StructureType = (typeof STRUCTURE_TYPES)[number]

export const PLURALS = {
export function is_structure_type(txt: string): txt is StructureType {
return (STRUCTURE_TYPES as readonly string[]).includes(txt)
}

export const PLURALS: Record<StructureType, string> = {
category: 'categories',
functor: 'functors',
morphism: 'morphisms',
}

export function get_selected_type(pathname: string): StructureType {
for (const type of STRUCTURES) {
const matches =
pathname.startsWith(`/${type}`) || pathname.startsWith(`/${PLURALS[type]}`)
for (const type of STRUCTURE_TYPES) {
const matches = pathname.startsWith(`/${type}`)
if (matches) return type
}
return 'category'
Expand Down
76 changes: 48 additions & 28 deletions src/lib/commons/types.ts
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
import type { StructureType } from './structures'

export type { StructureType }

export type Arrayed<T extends readonly unknown[]> = {
[K in keyof T]: T[K][]
}

type Replace<T, R extends Partial<Record<keyof T, any>>> = Omit<T, keyof R> & R

export type StructureType = 'category' | 'functor' | 'morphism'

export type StructureShort = {
id: string
name: string
Expand All @@ -24,32 +26,6 @@ export type StructureDisplay = {
dual_structure_notation: string | null
}

export type CategorySpecificDisplay = {
objects: string
morphisms: string
}

export type FunctorSpecificDisplay = {
source: string
source_name: string
source_notation: string
target: string
target_name: string
target_notation: string
left_adjoint: string | null
left_adjoint_name: string | null
left_adjoint_notation: string | null
right_adjoint: string | null
right_adjoint_name: string | null
right_adjoint_notation: string | null
}

export type MorphismSpecificDisplay = {
category: string
category_name: string
category_notation: string
}

export type MappedTypes = Record<string, StructureType>

export type TagObject = { tag: string }
Expand Down Expand Up @@ -140,9 +116,53 @@ export type SearchResults = {
dual_unsatisfied_properties: (string | null)[]
dual_search_available: boolean
found_structures: StructureShort[]
type: StructureType
}

export type ComparisonResult = {
structures: RelatedStructure[]
comparison_table: string[][]
type: StructureType
}

export type StructureDetails = {
type: StructureType
structure: StructureDisplay
related_structures: RelatedStructure[]
tags: string[]
satisfied_properties: PropertyAssignmentDisplay[]
unsatisfied_properties: PropertyAssignmentDisplay[]
unknown_properties: PropertyShort[]
undecidable_properties: PropertyAssignmentDisplay[]
undistinguishable_structures: StructureShort[]
comments: CommentObject[]
}

export type CategorySpecificDisplay = {
objects: string
morphisms: string
special_objects: SpecialObject[]
special_morphisms: SpecialMorphism[]
functors: StructureShort[]
}

export type FunctorSpecificDisplay = {
source: string
source_name: string
source_notation: string
target: string
target_name: string
target_notation: string
left_adjoint: string | null
left_adjoint_name: string | null
left_adjoint_notation: string | null
right_adjoint: string | null
right_adjoint_name: string | null
right_adjoint_notation: string | null
}

export type MorphismSpecificDisplay = {
category: string
category_name: string
category_notation: string
}
15 changes: 8 additions & 7 deletions src/lib/server/fetchers/category.ts
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
import type {
CategorySpecificDisplay,
SpecialMorphism,
SpecialObject,
StructureShort,
} from '$lib/commons/types'
import type { 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, StructureShort]
[
{ objects: string; morphisms: string },
SpecialObject,
SpecialMorphism,
StructureShort,
]
>([
// specific information for the category
sql`
Expand Down Expand Up @@ -51,6 +51,7 @@ export function fetch_category(id: string) {
if (!categories.length) error(404, `Could not find category with ID '${id}'`)

return {
type: 'category' as const,
...categories[0],
special_objects,
special_morphisms,
Expand Down
1 change: 1 addition & 0 deletions src/lib/server/fetchers/comparison.ts
Original file line number Diff line number Diff line change
Expand Up @@ -89,5 +89,6 @@ export function fetch_comparison_result(
return {
structures: render_nested_formulas(structures),
comparison_table,
type,
}
}
2 changes: 1 addition & 1 deletion src/lib/server/fetchers/functor.ts
Original file line number Diff line number Diff line change
Expand Up @@ -34,5 +34,5 @@ export function fetch_functor(id: string) {

if (!functors.length) error(404, `Could not find functor with ID '${id}'`)

return functors[0]
return { type: 'functor' as const, ...functors[0] }
}
2 changes: 1 addition & 1 deletion src/lib/server/fetchers/implication.ts
Original file line number Diff line number Diff line change
Expand Up @@ -57,5 +57,5 @@ export function fetch_implication(type: StructureType, id: string) {
mapped_types[map] = mapped_type
}

return { implication, structures, mapped_types }
return { type, implication, structures, mapped_types }
}
2 changes: 1 addition & 1 deletion src/lib/server/fetchers/implications.ts
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ export function fetch_implications(type: StructureType) {

const implications = rows.map(display_implication)

return { implications }
return { type, implications }
}

/**
Expand Down
2 changes: 1 addition & 1 deletion src/lib/server/fetchers/morphism.ts
Original file line number Diff line number Diff line change
Expand Up @@ -21,5 +21,5 @@ export function fetch_morphism(id: string) {

if (!morphisms.length) error(404, `Could not find morphism with ID '${id}'`)

return morphisms[0]
return { type: 'morphism' as const, ...morphisms[0] }
}
4 changes: 2 additions & 2 deletions src/lib/server/fetchers/properties.ts
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ export function fetch_grouped_properties_and_tags(type: StructureType) {
const total = properties.length
const grouped_total = grouped_properties.length

return { grouped_properties, total, grouped_total, tags }
return { type, grouped_properties, total, grouped_total, tags }
}

export function fetch_tagged_properties(type: StructureType, tag: string) {
Expand All @@ -90,5 +90,5 @@ export function fetch_tagged_properties(type: StructureType, tag: string) {

if (err) error(500, `Properties could not be loaded`)

return { properties, tag }
return { type, properties, tag }
}
1 change: 1 addition & 0 deletions src/lib/server/fetchers/property.ts
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,7 @@ export function fetch_property(type: StructureType, id: string) {
}

return {
type,
property,
related_properties,
tags,
Expand Down
2 changes: 2 additions & 0 deletions src/lib/server/fetchers/search.ts
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ export function fetch_search_results(
dual_unsatisfied_properties,
dual_search_available,
found_structures: [],
type,
}
}

Expand Down Expand Up @@ -147,5 +148,6 @@ export function fetch_search_results(
dual_unsatisfied_properties,
dual_search_available,
found_structures,
type,
}
}
Loading