Consistent clearing of deduced data

databases/catdat/schema/005_special_objects.sql

@@ -9,6 +9,8 @@ CREATE TABLE special_objects (
     category_id TEXT NOT NULL,
     type TEXT NOT NULL,
     description TEXT NOT NULL,
+    is_deduced INTEGER NOT NULL DEFAULT FALSE
+        CHECK (is_deduced in (TRUE, FALSE)),
     PRIMARY KEY (category_id, type),
     FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT,
     FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE

databases/catdat/schema/006_special-morphisms.sql

@@ -10,6 +10,8 @@ CREATE TABLE special_morphisms (
     type TEXT NOT NULL,
     description TEXT NOT NULL,
     proof TEXT NOT NULL,
+    is_deduced INTEGER NOT NULL DEFAULT FALSE
+        CHECK (is_deduced in (TRUE, FALSE)),
     PRIMARY KEY (category_id, type),
     FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT,
     FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE

databases/catdat/scripts/deduce-special-morphisms.ts

@@ -8,28 +8,41 @@ const db = get_client()
 
 export function deduce_special_morphisms() {
 	console.info('\n--- Deduce special morphisms ---')
+	clear_deduced_special_morphisms()
 	deduce_special_morphisms_of_dual_categories()
 }
 
+/**
+ * Clears deduced special morphisms
+ */
+function clear_deduced_special_morphisms() {
+	db.prepare(`DELETE FROM special_morphisms WHERE is_deduced = TRUE`).run()
+}
+
 /**
  * Deduce special morphisms in dual categories.
  * For example, monomorphisms in C describe epimorphisms in C^op.
  */
 function deduce_special_morphisms_of_dual_categories() {
 	const res = db
 		.prepare(
-			`INSERT INTO special_morphisms
-                (category_id, type, description, proof)
+			`INSERT INTO special_morphisms (
+                category_id,
+                type,
+                description,
+                proof,
+                is_deduced
+            )
             SELECT
                 c.dual_structure_id,
                 t.dual,
                 m.description,
-                'This is deduced from its dual category.'
+                'This is deduced from its dual category.',
+                TRUE
             FROM structures c
             INNER JOIN special_morphisms m ON m.category_id = c.id
             INNER JOIN special_morphism_types t ON t.type = m.type
-            WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL
-            ON CONFLICT DO NOTHING`,
+            WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL`,
 		)
 		.run()
 

databases/catdat/scripts/deduce-special-objects.ts

@@ -4,26 +4,39 @@ const db = get_client()
 
 export function deduce_special_objects() {
 	console.info('\n--- Deduce special objects ---')
+	clear_deduced_special_objects()
 	deduce_special_objects_of_dual_categories()
 }
 
+/**
+ * Clears deduced special objects
+ */
+function clear_deduced_special_objects() {
+	db.prepare(`DELETE FROM special_objects WHERE is_deduced = TRUE`).run()
+}
+
 /**
  * Deduce special objects in dual categories.
  * For example, initial objects in C describe the terminal objects in C^op.
  */
-async function deduce_special_objects_of_dual_categories() {
+function deduce_special_objects_of_dual_categories() {
 	const res = db
 		.prepare(
-			`INSERT INTO special_objects (category_id, type, description)
+			`INSERT INTO special_objects (
+                category_id,
+                type,
+                description,
+                is_deduced
+            )
             SELECT
                 c.dual_structure_id,
                 t.dual,
-                o.description
+                o.description,
+                TRUE
             FROM structures c
             INNER JOIN special_objects o ON o.category_id = c.id
             INNER JOIN special_object_types t ON t.type = o.type
-            WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL
-            ON CONFLICT DO NOTHING`,
+            WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL`,
 		)
 		.run()
 

databases/catdat/scripts/deduce-structure-properties.ts

@@ -394,14 +394,14 @@ export function deduce_properties_for_structures(type: StructureType) {
 
 	const db = get_client()
 
+	delete_deduced_properties(db, type)
+
 	const implications = get_normalized_implications(db, type)
 	const structures = get_structures(db, type)
 	const properties_dict = get_properties_dict(db, type)
 	const get_assigned_properties = get_property_assignments(db, structures, type)
 
 	const deduction = db.transaction(() => {
-		delete_deduced_properties(db, type)
-
 		for (const structure of structures) {
 			const assigned = get_assigned_properties[structure.id]
 

databases/catdat/scripts/deduce.ts

@@ -23,8 +23,8 @@ function deduce() {
 	deduce_special_morphisms()
 
 	// --- functors ---
-	restrict_representable_functors()
 	clear_deduced_implications('functor')
 	create_dualized_implications('functor')
 	deduce_properties_for_structures('functor')
+	restrict_representable_functors()
 }

databases/catdat/scripts/restrict-functor-properties.ts

@@ -26,11 +26,15 @@ export function restrict_representable_functors() {
                 'functor',
                 FALSE,
                 'The target category is not $\\Set$.',
-                FALSE,
+                TRUE,
                 FALSE
             FROM functors f
             WHERE f.target <> 'Set'
-            ON CONFLICT (structure_id, property_id) DO NOTHING`,
+            ON CONFLICT (structure_id, property_id)
+            DO UPDATE SET
+                proof = excluded.proof,
+                is_deduced = excluded.is_deduced,
+                check_redundancy = excluded.check_redundancy`,
 		)
 		.run()