seed lemmas

Author: ScriptRaccoon

databases/catdat/scripts/seed.yaml.ts

@@ -2,7 +2,12 @@ import fs from 'node:fs'
 import path from 'node:path'
 import { get_client } from './shared'
 import YAML from 'yaml'
-import type { CategoryYaml, ConfigYaml, CategoryPropertyYaml } from './yaml.types'
+import type {
+	CategoryYaml,
+	ConfigYaml,
+	CategoryPropertyYaml,
+	LemmaYaml,
+} from './yaml.types'
 
 const db = get_client()
 
@@ -19,13 +24,15 @@ function seed() {
 	clear_all_data()
 
 	seed_config()
+
+	seed_lemmas()
 	seed_category_properties()
 	seed_categories()
 
 	// TODO: seed implications
 	// TODO: seed category property assignments
 	// TODO: seed category property comments
-	// TODO: seed lemmas, and all the other tables
+	// TODO: seed all the other tables
 }
 
 function clear_all_data() {
@@ -241,3 +248,25 @@ function seed_category_properties() {
 		}
 	})()
 }
+
+function seed_lemmas() {
+	const lemma_folder = path.join(data_folder, 'lemmas')
+
+	const lemma_files = fs
+		.readdirSync(lemma_folder)
+		.filter((file) => file.endsWith('.yaml'))
+		.sort()
+
+	const lemma_insert = db.prepare(
+		`INSERT INTO lemmas (id, title, claim, proof) VALUES (?, ?, ?, ?)`,
+	)
+
+	db.transaction(() => {
+		for (const lemma_file of lemma_files) {
+			const content = fs.readFileSync(path.join(lemma_folder, lemma_file), 'utf8')
+			const lemma = YAML.parse(content) as LemmaYaml
+
+			lemma_insert.run(lemma.id, lemma.title, lemma.claim, lemma.proof)
+		}
+	})()
+}

databases/catdat/scripts/yaml.types.ts

@@ -61,3 +61,10 @@ export type CategoryPropertyYaml = {
 	invariant_under_equivalences: boolean
 	related_properties: string[]
 }
+
+export type LemmaYaml = {
+	id: string
+	title: string
+	claim: string
+	proof: string
+}