aboutsummaryrefslogtreecommitdiffstats
path: root/research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch
diff options
context:
space:
mode:
authoreunhhu <[email protected]>2026-10-19 14:37:55 +0100
committereunhhu <[email protected]>2026-10-19 14:37:55 +0100
commit519df326fe131c94a706c0d8b8f23ca8f093af3b (patch)
treed0abae610187ff9c3b160d30a2cf8cc095831a0a /research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch
parentcf3a1d66c2af6146d895065fa65d132191d48e00 (diff)
downloadpure-519df326fe131c94a706c0d8b8f23ca8f093af3b.tar.gz
pure-519df326fe131c94a706c0d8b8f23ca8f093af3b.zip
045: the app keyed and its range found by a seek, emitted as it says (no algorithm the app does not state, nothing copied out of the tree): aup takes ranges as a list keyed by last and first(x in ranges where x.last >= code) as its range, the executor answers every line and is itself 40,258 to 27,934 machine instructions a point; the hand rungs on it (the seek by each level's guide keys and the leaf's key column, the found item's fields read from it, the other ranges read by key): keyed_shared 788 a point, end to end 813 with 348 cycles (the position-halving seek of a1382de, another program, 604 with 373 cycles; Vega's C 251 with 93)
Diffstat (limited to 'research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch')
-rw-r--r--research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch77
1 files changed, 77 insertions, 0 deletions
diff --git a/research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch b/research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch
new file mode 100644
index 0000000..e05efab
--- /dev/null
+++ b/research/experiments/045-proof-compiler/variants/linebreak-keyed2.patch
@@ -0,0 +1,77 @@
+--- linebreak.aup
++++ linebreak-keyed2.aup
+@@ -3,7 +3,7 @@
+ # loaded once: each its class after LB1, whether an initial or a final quotation mark (Pi, Pf), East Asian (width F, W
+ # or H), and pictographic and unassigned (Extended_Pictographic and Cn). A line's boundaries, the ends included, are 0
+ # (none), 1 (allowed) or 2 (mandatory).
+-record Range {
++record Row { # a range as the load message gives it: by its first code point
+ start = 0
+ class = 0
+ pi = false
+@@ -11,6 +11,14 @@
+ east = false
+ pictographic = false
+ }
++record Range { # a range as the state keeps it: by its last code point
++ last = 0
++ class = 0
++ pi = false
++ pf = false
++ east = false
++ pictographic = false
++}
+ record Point {
+ code = 0
+ }
+@@ -25,10 +33,10 @@
+ ri: list of number # how many regional indicators end at its unit
+ at: list of number # its range
+ }
+-state ranges: list of Range # by start, from 0
++state ranges: list of Range by last # by its last code point, every one up to 0x10FFFF in one
+ state breaks: bytes # the last line's boundaries
+ view boundaries = breaks
+-input load = message { rows: list of Range }
++input load = message { rows: list of Row }
+ input line = message { points: list of Point }
+
+ fn BK = 0; fn CR = 1; fn LF = 2; fn NL = 3; fn SP = 4; fn ZW = 5; fn ZWJ = 6; fn CM = 7; fn WJ = 8; fn GL = 9
+@@ -40,18 +48,15 @@
+ fn end(c) = c == BK || c == CR || c == LF || c == NL
+
+ on load {
+- for r in load.rows { ranges.append(Range { ..r }) }
++ let n = load.rows.count
++ for i in 0 .. n {
++ let last = if i + 1 < n { load.rows[i + 1].start - 1 } else { 0x10FFFF }
++ ranges.add(Range { last: last, class: load.rows[i].class, pi: load.rows[i].pi, pf: load.rows[i].pf,
++ east: load.rows[i].east, pictographic: load.rows[i].pictographic })
++ }
+ }
+
+ # The range holding code point c (ranges by start: the last whose start is c or before).
+-fn range(c) {
+- let low, high = 0, ranges.count
+- while high - low > 1 {
+- let middle = (low + high) // 2
+- if ranges[middle].start <= c { low = middle } else { high = middle }
+- }
+- return low
+-}
+
+ fn next_unit(t, i) {
+ let j = i + 1
+@@ -157,8 +162,10 @@
+ let joined, numeric: list of bool
+ for p in line.points {
+ let i = codes.count
+- let r = range(p.code)
+- let c = ranges[r].class
++ let code = p.code
++ let found = first(x in ranges where x.last >= code) # its range: a seek, the item itself
++ let r = found.last
++ let c = found.class
+ let mark = c == CM || c == ZWJ
+ let previous = if i > 0 { eff[i - 1] } else { SP }
+ let joins = mark && i > 0 && !end(previous) && previous != SP && previous != ZW # LB9, LB10