All files / web/src/components/toys/euclid/data/scripts precomputeLayout.ts

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
/**
 * Pre-compute the optimal Sugiyama layout for all 48 Book I propositions.
 *
 * Run with:  npx tsx src/components/toys/euclid/data/scripts/precomputeLayout.ts
 *
 * This runs decrossOpt() (ILP-based globally optimal crossing minimization)
 * which may take seconds to minutes but produces the best possible layout.
 * The result is written to ../book1Layout.ts as static data.
 */

import { graphStratify, sugiyama, decrossOpt, coordSimplex, layeringSimplex } from 'd3-dag'
import { propositions, getPrerequisites, getAllPrerequisites } from '../book1'
import { writeFileSync } from 'fs'
import { resolve, dirname } from 'path'
import { fileURLToPath } from 'url'

const NODE_W = 130
const NODE_H = 48

// ---------------------------------------------------------------------------
// Transitive reduction (copied from propositionGraph.ts)
// ---------------------------------------------------------------------------

function transitiveReduction(visibleIds: number[]): Array<{ from: number; to: number }> {
  const visibleSet = new Set(visibleIds)
  const edges: Array<{ from: number; to: number }> = []

  for (const v of visibleIds) {
    const directParents = getPrerequisites(v).filter((d) => visibleSet.has(d))
    if (directParents.length <= 1) {
      for (const u of directParents) {
        edges.push({ from: u, to: v })
      }
      continue
    }

    const ancestorSets = new Map<number, Set<number>>()
    for (const u of directParents) {
      ancestorSets.set(u, new Set(getAllPrerequisites(u)))
    }

    for (const u of directParents) {
      let isRedundant = false
      for (const w of directParents) {
        if (w === u) continue
        if (ancestorSets.get(w)!.has(u)) {
          isRedundant = true
          break
        }
      }
      if (!isRedundant) {
        edges.push({ from: u, to: v })
      }
    }
  }

  return edges
}

// ---------------------------------------------------------------------------
// Compute levels
// ---------------------------------------------------------------------------

function computeLevels(): Map<number, number> {
  const levels = new Map<number, number>()
  function getLevel(id: number): number {
    if (levels.has(id)) return levels.get(id)!
    const deps = getPrerequisites(id)
    if (deps.length === 0) {
      levels.set(id, 0)
      return 0
    }
    const level = 1 + Math.max(...deps.map(getLevel))
    levels.set(id, level)
    return level
  }
  for (const p of propositions) getLevel(p.id)
  return levels
}

// ---------------------------------------------------------------------------
// Main
// ---------------------------------------------------------------------------

const allIds = propositions.map((p) => p.id)
const levels = computeLevels()
const reducedEdges = transitiveReduction(allIds)

console.log(`Nodes: ${allIds.length}, Edges: ${reducedEdges.length}`)

// Build parent map
const parentMap = new Map<string, string[]>()
for (const id of allIds) parentMap.set(String(id), [])
for (const { from, to } of reducedEdges) {
  parentMap.get(String(to))!.push(String(from))
}

const stratData = allIds.map((id) => ({
  id: String(id),
  parentIds: parentMap.get(String(id))!,
}))

const dag = graphStratify()(stratData)

console.log('Running sugiyama with decrossOpt()... this may take a while.')
console.time('layout')

const layout = sugiyama()
  .layering(layeringSimplex())
  .decross(decrossOpt())
  .coord(coordSimplex())
  .nodeSize([NODE_W + 24, NODE_H + 60])
  .gap([24, 12])

const { width, height } = layout(dag)
console.timeEnd('layout')
console.log(`Layout dimensions: ${width.toFixed(0)} x ${height.toFixed(0)}`)

// Extract positions
const nodePositions: Record<number, { x: number; y: number; level: number }> = {}
for (const node of dag.nodes()) {
  const id = Number(node.data.id)
  nodePositions[id] = {
    x: Math.round(node.x * 100) / 100,
    y: Math.round(node.y * 100) / 100,
    level: levels.get(id) ?? 0,
  }
}

// Extract edges
const edgeData: Array<{ from: number; to: number; points: Array<{ x: number; y: number }> }> = []
for (const link of dag.links()) {
  const from = Number(link.source.data.id)
  const to = Number(link.target.data.id)
  edgeData.push({
    from,
    to,
    points: link.points.map(([x, y]: [number, number]) => ({
      x: Math.round(x * 100) / 100,
      y: Math.round(y * 100) / 100,
    })),
  })
}

// Write output
const __dirname = dirname(fileURLToPath(import.meta.url))
const outPath = resolve(__dirname, '..', 'book1Layout.ts')

const output = `/**
 * Pre-computed optimal Sugiyama layout for all 48 Book I propositions.
 *
 * Generated by: npx tsx src/components/toys/euclid/data/scripts/precomputeLayout.ts
 * Algorithm: d3-dag sugiyama with decrossOpt() (ILP-based optimal crossing minimization)
 *
 * DO NOT EDIT — regenerate if book1.ts dependencies change.
 */

import type { NodeLayout, LayoutEdge } from './propositionGraph'

export const PRECOMPUTED_NODES: Record<number, NodeLayout> = ${JSON.stringify(nodePositions, null, 2)}

export const PRECOMPUTED_EDGES: LayoutEdge[] = ${JSON.stringify(edgeData, null, 2)}
`

writeFileSync(outPath, output)
console.log(`Written to ${outPath}`)