045: range() emitted by hand, Pure's meaning kept or dropped where the proof could license it (range.c; every way's answers the executor's and the stitched build's, for all 61,285 points): a code point's machine instructions in the executor 14,488, stitched 8,144, exact (registers, a plain call; doubles, fmod, the finite and whole checks, the tree read, the budget) 2,474, integers 1,587, a flat column 1,083, both 226, C 129; a round of halving exact 217, both 19.8, C 11.3: the bar (3x C's round) missed by exact, passed by both

1 files changed, 36 insertions, 0 deletions

diff --git a/research/experiments/045-proof-compiler/variants/range-out.patch b/research/experiments/045-proof-compiler/variants/range-out.patch
new file mode 100644
index 0000000..5cad619
--- /dev/null
+++ b/research/experiments/045-proof-compiler/variants/range-out.patch
@@ -0,0 +1,36 @@
+--- linebreak.aup
++++ range-out.aup
+@@ -153,30 +153,11 @@
+ }
+ 
+ on line {
+-  let codes, cls, eff, start, nonspace, ri, at: list of number
+-  let joined, numeric: list of bool
++  let out: list of i64
+   for p in line.points {
+-    let i = codes.count
+     let r = range(p.code)
+-    let c = ranges[r].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
+-    let e = if joins { previous } else if mark { AL } else { c }
+-    codes.append(p.code)
+-    cls.append(c)
+-    at.append(r)
+-    joined.append(joins)
+-    eff.append(e)
+-    start.append(if joins { start[i - 1] } else { i })
+-    nonspace.append(if e != SP { start[i] } else if i > 0 { nonspace[i - 1] } else { -1 })
+-    numeric.append(if joins { numeric[i - 1] } else { e == NU || ((e == SY || e == IS) && i > 0 && numeric[i - 1]) })
+-    ri.append(if joins { ri[i - 1] } else if e == RI { (if i > 0 { ri[i - 1] } else { 0 }) + 1 } else { 0 })
++    out.append(i64(r % 256))
++    out.append(i64(r // 256))
+   }
+-  let t = Text { codes: codes, cls: cls, eff: eff, joined: joined, start: start, nonspace: nonspace, numeric: numeric, ri: ri,
+-                 at: at }
+-  let out: list of i64 = [0]                                                          # LB2
+-  for i in 1 .. codes.count { out.append(i64(decide(t, i))) }
+-  if codes.count > 0 { out.append(2) }                                                # LB3
+   breaks = bytes(out)
+ }