Skip to content

Commit 9bcd331

Browse files
ScriptRaccoonScriptRaccoon
committed
adapt scripts
1 parent 2f0d6bc commit 9bcd331

11 files changed

Lines changed: 419 additions & 429 deletions

‎databases/catdat/scripts/deduce-category-implications.ts‎

Lines changed: 71 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -1,59 +1,61 @@
1-
import type { Client } from '@libsql/client'
21
import { are_equal_sets } from './shared'
2+
import { type Database } from 'better-sqlite3'
33

44
/**
55
* Deduces implications from given ones.
66
*/
7-
export async function deduce_category_implications(db: Client) {
7+
export function deduce_category_implications(db: Database) {
88
console.info('\n--- Deduce category implications ---')
9-
await clear_deduced_category_implications(db)
10-
await create_dualized_category_implications(db)
11-
await create_self_dual_category_implications(db)
9+
clear_deduced_category_implications(db)
10+
create_dualized_category_implications(db)
11+
create_self_dual_category_implications(db)
1212
}
1313

1414
/**
1515
* Clears all deduced implications. This is done as a first step.
1616
*/
17-
async function clear_deduced_category_implications(db: Client) {
18-
await db.execute(`DELETE FROM category_implications WHERE is_deduced = TRUE`)
17+
function clear_deduced_category_implications(db: Database) {
18+
db.exec(`DELETE FROM category_implications WHERE is_deduced = TRUE`)
1919
}
2020

2121
/**
2222
* Dualizes all implications by dualizing the involved properties
2323
* (in case they have a dual). For example, if P ===> Q holds,
2424
* then P^op ===> Q^op holds as well.
2525
*/
26-
async function create_dualized_category_implications(db: Client) {
27-
const res = await db.execute(`
28-
SELECT
29-
v.id,
30-
v.assumptions,
31-
v.conclusions,
32-
v.is_equivalence,
33-
v.reason,
34-
(
35-
SELECT json_group_array(p.dual_property_id)
36-
FROM json_each(v.assumptions) a
37-
JOIN category_properties p ON p.id = a.value
38-
) AS dual_assumptions,
39-
(
40-
SELECT json_group_array(p.dual_property_id)
41-
FROM json_each(v.conclusions) c
42-
JOIN category_properties p ON p.id = c.value
43-
) AS dual_conclusions
44-
FROM category_implications_view v
45-
WHERE v.is_deduced = FALSE
46-
`)
47-
48-
const implications = res.rows as unknown as {
26+
function create_dualized_category_implications(db: Database) {
27+
type FullImplication = {
4928
id: string
5029
assumptions: string
5130
conclusions: string
5231
dual_assumptions: string
5332
dual_conclusions: string
5433
is_equivalence: number
5534
reason: string
56-
}[]
35+
}
36+
37+
const implications = db
38+
.prepare(
39+
`SELECT
40+
v.id,
41+
v.assumptions,
42+
v.conclusions,
43+
v.is_equivalence,
44+
v.reason,
45+
(
46+
SELECT json_group_array(p.dual_property_id)
47+
FROM json_each(v.assumptions) a
48+
JOIN category_properties p ON p.id = a.value
49+
) AS dual_assumptions,
50+
(
51+
SELECT json_group_array(p.dual_property_id)
52+
FROM json_each(v.conclusions) c
53+
JOIN category_properties p ON p.id = c.value
54+
) AS dual_conclusions
55+
FROM category_implications_view v
56+
WHERE v.is_deduced = FALSE`,
57+
)
58+
.all() as FullImplication[]
5759

5860
const dualizable_implications = implications.filter((impl) => {
5961
const has_null =
@@ -72,64 +74,65 @@ async function create_dualized_category_implications(db: Client) {
7274
)
7375
})
7476

75-
await db.batch(
76-
dualizable_implications.map((impl) => ({
77-
sql: `
78-
INSERT INTO category_implications_view (
77+
const insert_duals = db.transaction(() => {
78+
for (const impl of dualizable_implications) {
79+
db.prepare(
80+
`INSERT INTO category_implications_view (
7981
id,
8082
assumptions,
8183
conclusions,
8284
is_equivalence,
8385
reason,
8486
is_deduced,
8587
dualized_from
86-
) VALUES (?, ?, ?, ?, ?, ?, ?)`,
87-
args: [
88+
) VALUES (?, ?, ?, ?, ?, TRUE, ?)`,
89+
).run(
8890
`dual_${impl.id}`,
8991
impl.dual_assumptions,
9092
impl.dual_conclusions,
9193
impl.is_equivalence,
9294
'This follows from the dual implication.',
93-
true,
9495
impl.id,
95-
],
96-
})),
97-
'write',
98-
)
96+
)
97+
}
98+
})
9999

100+
insert_duals()
100101
console.info(`Deduced ${dualizable_implications.length} implications by duality`)
101102
}
102103

103104
/**
104105
* Creates all trivial implications of the form
105106
* self-dual + P ===> P^op
106107
*/
107-
async function create_self_dual_category_implications(db: Client) {
108-
const { rows } = await db.execute(`
109-
INSERT INTO category_implications_view (
110-
id,
111-
assumptions,
112-
conclusions,
113-
is_equivalence,
114-
reason,
115-
is_deduced
116-
)
117-
SELECT
118-
'self-dual_' || p.id,
119-
json_array('self-dual', p.id),
120-
json_array(p.dual_property_id),
121-
FALSE,
122-
'This holds by self-duality.',
123-
TRUE
124-
FROM
125-
category_properties p
126-
WHERE
127-
p.dual_property_id IS NOT NULL
128-
AND p.id != 'self-dual'
129-
AND p.id != p.dual_property_id
130-
AND p.invariant_under_equivalences = TRUE
131-
RETURNING id
132-
`)
108+
function create_self_dual_category_implications(db: Database) {
109+
const rows = db
110+
.prepare(
111+
`INSERT INTO category_implications_view (
112+
id,
113+
assumptions,
114+
conclusions,
115+
is_equivalence,
116+
reason,
117+
is_deduced
118+
)
119+
SELECT
120+
'self-dual_' || p.id,
121+
json_array('self-dual', p.id),
122+
json_array(p.dual_property_id),
123+
FALSE,
124+
'This holds by self-duality.',
125+
TRUE
126+
FROM
127+
category_properties p
128+
WHERE
129+
p.dual_property_id IS NOT NULL
130+
AND p.id != 'self-dual'
131+
AND p.id != p.dual_property_id
132+
AND p.invariant_under_equivalences = TRUE
133+
RETURNING id`,
134+
)
135+
.all()
133136

134137
console.info(`Deduced ${rows.length} implications by self-duality`)
135138
}

0 commit comments

Comments
 (0)