From b67d0726e008c511848711d67e0ee6be14941421 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:36:08 -0400 Subject: [PATCH 1/8] Represent source-bound Unicode subset break opportunities and codepoint spans --- src/IB/Reflow/SourceBreaks.idric | 188 +++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 src/IB/Reflow/SourceBreaks.idric diff --git a/src/IB/Reflow/SourceBreaks.idric b/src/IB/Reflow/SourceBreaks.idric new file mode 100644 index 0000000..bb07bd2 --- /dev/null +++ b/src/IB/Reflow/SourceBreaks.idric @@ -0,0 +1,188 @@ +module IB.Reflow.SourceBreaks + +import Data.Text + +-- A source-bound list of possible line breaks. Offsets count decoded Unicode +-- code points (elements of unpack), NOT UTF-8 bytes, UTF-16 units or glyphs. +-- A break is the position immediately AFTER source_offset characters. +-- The source text itself remains canonical. No renderer output is reparsed. +public export +data BreakKind + = PossibleBreak + | MandatoryBreak + | DiscretionaryHyphen + | ZeroWidthBreak + | SourceEnd + +public export +record SourceBreak where + constructor At + source_offset : Number + break_kind : BreakKind + +public export +record SourceLine where + constructor FromSource + first_codepoint : Number + after_last_codepoint : Number + visible_text : Text + ending : BreakKind + +is_han : Char → Bool +is_han value = + let number = ord value in + (number >= 19968 && number <= 40959) || + (number >= 13312 && number <= 19903) + +-- Deliberately bounded Unicode tailoring, NOT the complete UAX #14. +-- ASCII SPACE, ZERO WIDTH SPACE, SOFT HYPHEN, hard line endings and selected +-- Han–Han boundaries produce candidates. NBSP/WORD JOINER and emoji ZWJ do +-- not generate breaks. Complete Unicode/locale break data can supply an +-- independently qualified list of SourceBreak values to the same solver. +hard_line_end : Char → List Char → Bool +hard_line_end '\r' ('\n' :: _) = False +hard_line_end '\r' _ = True +hard_line_end '\n' _ = True +hard_line_end value _ = + let number = ord value in + number ≟ 133 || number ≟ 8232 || number ≟ 8233 + +classify : Char → List Char → Maybe BreakKind +classify value rest = + if hard_line_end value rest then Just MandatoryBreak + else if ord value ≟ 173 then Just DiscretionaryHyphen + else if ord value ≟ 8203 then Just ZeroWidthBreak + else if value ≟ ' ' then Just PossibleBreak + else if is_han value then + case rest of + next :: _ ⇒ if is_han next then Just PossibleBreak else Nothing + [] ⇒ Nothing + else Nothing + +is_empty : List Char → Bool +is_empty [] = True +is_empty (_ :: _) = False + +scan_breaks : Number → List Char → List SourceBreak +scan_breaks offset [] = [At offset SourceEnd] +scan_breaks offset (value :: rest) = + let later = scan_breaks (S offset) rest in + case classify value rest of + Nothing ⇒ later + Just kind ⇒ + if is_empty rest + then case kind of + MandatoryBreak ⇒ [At (S offset) MandatoryBreak] + _ ⇒ later + else At (S offset) kind :: later + +public export +source_breaks : Text → List SourceBreak +source_breaks text = scan_breaks 0 (unpack text) + +-- Checks do not establish all of UAX #14/#29. They *do* fail closed on +-- malformed ranges, duplicate/reordered cuts, missing mandatory breaks, cuts +-- inside CRLF or after ZWJ/word joiner, and cuts before common combining marks. +-- Full segmentation is a separate, versioned provider qualification. +at_position : Number → List Char → Maybe Char +at_position Z [] = Nothing +at_position Z (value :: _) = Just value +at_position (S position) [] = Nothing +at_position (S position) (_ :: rest) = at_position position rest + +before : Number → List Char → Maybe Char +before Z chars = Nothing +before (S previous) chars = at_position previous chars + +is_combining_mark : Char → Bool +is_combining_mark value = + let number = ord value in + (number >= 768 && number <= 879) || + (number >= 6832 && number <= 6911) || + (number >= 7616 && number <= 7679) || + (number >= 8400 && number <= 8447) || + (number >= 65056 && number <= 65071) + +safe_cut : List Char → Number → Bool +safe_cut chars offset = + case (before offset chars, at_position offset chars) of + (Just previous, Just next) ⇒ + not (previous ≟ '\r' && next ≟ '\n') && + not (ord previous ≟ 8205 || ord previous ≟ 8288) && + not (ord next ≟ 8205 || ord next ≟ 8288) && + not (is_combining_mark next) && + not (next ≟ '\r' || next ≟ '\n') + _ ⇒ True + +requires_break : List Char → Number → Bool +requires_break chars offset = + case before offset chars of + Nothing ⇒ False + Just previous ⇒ + let remaining = drop offset chars in + hard_line_end previous remaining + +same_kind : BreakKind → BreakKind → Bool +same_kind PossibleBreak PossibleBreak = True +same_kind MandatoryBreak MandatoryBreak = True +same_kind DiscretionaryHyphen DiscretionaryHyphen = True +same_kind ZeroWidthBreak ZeroWidthBreak = True +same_kind SourceEnd SourceEnd = True +same_kind _ _ = False + +-- For a declared mandatory cut, check that the source actually forces it. +-- The end marker is allowed only at the exact end, except that a hard final +-- newline is represented by MandatoryBreak instead. +kind_is_sound : List Char → Number → BreakKind → Bool +kind_is_sound chars offset MandatoryBreak = requires_break chars offset +kind_is_sound chars offset DiscretionaryHyphen = + case before offset chars of + Just previous ⇒ ord previous ≟ 173 + Nothing ⇒ False +kind_is_sound chars offset ZeroWidthBreak = + case before offset chars of + Just previous ⇒ ord previous ≟ 8203 + Nothing ⇒ False +kind_is_sound chars offset PossibleBreak = + not (requires_break chars offset) +kind_is_sound chars offset SourceEnd = + offset ≟ length chars && not (requires_break chars offset) + +well_ordered : List Char → Number → List SourceBreak → Bool +well_ordered chars previous [] = previous ≟ length chars +well_ordered chars previous (At offset kind :: rest) = + offset > previous && offset <= length chars && + safe_cut chars offset && + kind_is_sound chars offset kind && + well_ordered chars offset rest + +has_mandatory : Number → List SourceBreak → Bool +has_mandatory offset [] = False +has_mandatory offset (At position kind :: rest) = + if offset ≟ position + then same_kind kind MandatoryBreak + else has_mandatory offset rest + +all_hard_breaks : Number → List Char → List SourceBreak → Bool +all_hard_breaks offset [] breaks = True +all_hard_breaks offset (value :: rest) breaks = + let next = S offset in + if hard_line_end value rest + then has_mandatory next breaks && all_hard_breaks next rest breaks + else all_hard_breaks next rest breaks + +public export +valid_source_breaks : Text → List SourceBreak → Bool +valid_source_breaks text breaks = + let chars = unpack text in + case breaks of + [] ⇒ is_empty chars + _ ⇒ well_ordered chars 0 breaks && all_hard_breaks 0 chars breaks + +-- Reconstruct EXACT decoded source from offsets, regardless of paint spelling. +-- This is an independent identity oracle for layouts with discretionary marks. +public export +source_for_line : Text → SourceLine → Text +source_for_line source line = + pack (take (line.after_last_codepoint - line.first_codepoint) + (drop line.first_codepoint (unpack source))) From 7bdb1162b5ceafc3133ee2fc3c9dfc58f0232580 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:37:45 -0400 Subject: [PATCH 2/8] Validate mandatory Unicode breaks, preserve exact source spans and refuse unsafe cuts --- src/IB/Reflow/SourceBreaks.idric | 33 ++++++++++++++++++++++---------- 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/src/IB/Reflow/SourceBreaks.idric b/src/IB/Reflow/SourceBreaks.idric index bb07bd2..f7ba27c 100644 --- a/src/IB/Reflow/SourceBreaks.idric +++ b/src/IB/Reflow/SourceBreaks.idric @@ -1,6 +1,7 @@ module IB.Reflow.SourceBreaks import Data.Text +import IB.Reflow.Arithmetic -- A source-bound list of possible line breaks. Offsets count decoded Unicode -- code points (elements of unpack), NOT UTF-8 bytes, UTF-16 units or glyphs. @@ -52,7 +53,12 @@ classify value rest = if hard_line_end value rest then Just MandatoryBreak else if ord value ≟ 173 then Just DiscretionaryHyphen else if ord value ≟ 8203 then Just ZeroWidthBreak - else if value ≟ ' ' then Just PossibleBreak + else if value ≟ ' ' then + case rest of + next :: _ ⇒ + if hard_line_end next [] || ord next ≟ 8205 || ord next ≟ 8288 + then Nothing else Just PossibleBreak + [] ⇒ Nothing else if is_han value then case rest of next :: _ ⇒ if is_han next then Just PossibleBreak else Nothing @@ -103,15 +109,19 @@ is_combining_mark value = (number >= 8400 && number <= 8447) || (number >= 65056 && number <= 65071) -safe_cut : List Char → Number → Bool -safe_cut chars offset = +safe_cut : List Char → Number → BreakKind → Bool +safe_cut chars offset kind = case (before offset chars, at_position offset chars) of (Just previous, Just next) ⇒ not (previous ≟ '\r' && next ≟ '\n') && not (ord previous ≟ 8205 || ord previous ≟ 8288) && not (ord next ≟ 8205 || ord next ≟ 8288) && - not (is_combining_mark next) && - not (next ≟ '\r' || next ≟ '\n') + (case kind of + MandatoryBreak ⇒ True + _ ⇒ not (is_combining_mark next)) && + (case kind of + MandatoryBreak ⇒ True + _ ⇒ not (hard_line_end next [])) _ ⇒ True requires_break : List Char → Number → Bool @@ -152,7 +162,7 @@ well_ordered : List Char → Number → List SourceBreak → Bool well_ordered chars previous [] = previous ≟ length chars well_ordered chars previous (At offset kind :: rest) = offset > previous && offset <= length chars && - safe_cut chars offset && + safe_cut chars offset kind && kind_is_sound chars offset kind && well_ordered chars offset rest @@ -175,8 +185,11 @@ public export valid_source_breaks : Text → List SourceBreak → Bool valid_source_breaks text breaks = let chars = unpack text in - case breaks of - [] ⇒ is_empty chars + case chars of + [] ⇒ case breaks of + [] ⇒ True + [At Z SourceEnd] ⇒ True + _ ⇒ False _ ⇒ well_ordered chars 0 breaks && all_hard_breaks 0 chars breaks -- Reconstruct EXACT decoded source from offsets, regardless of paint spelling. @@ -184,5 +197,5 @@ valid_source_breaks text breaks = public export source_for_line : Text → SourceLine → Text source_for_line source line = - pack (take (line.after_last_codepoint - line.first_codepoint) - (drop line.first_codepoint (unpack source))) + pack (take (nonnegative_difference line.after_last_codepoint line.first_codepoint) + (drop line.first_codepoint (unpack source))) From 2405a487f1d33a1b54fb7d21cd33372d6270943e Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:38:57 -0400 Subject: [PATCH 3/8] Implement source-preserving greedy and objective-based reflow over checked Unicode break positions --- src/IB/Reflow/Source.idric | 216 +++++++++++++++++++++++++++++++++++++ 1 file changed, 216 insertions(+) create mode 100644 src/IB/Reflow/Source.idric diff --git a/src/IB/Reflow/Source.idric b/src/IB/Reflow/Source.idric new file mode 100644 index 0000000..f29afc8 --- /dev/null +++ b/src/IB/Reflow/Source.idric @@ -0,0 +1,216 @@ +module IB.Reflow.Source + +import Data.Text +import IB.Reflow +import IB.Reflow.Arithmetic +import IB.Reflow.SourceBreaks + +-- Unlike the earlier atomic-word reflow, this preserves source character +-- offsets and never normalizes or edits canonical source. The visible text is +-- a derived projection: paragraph controls are hidden, trailing display +-- spaces are suppressed, and a chosen soft-hyphen cut adds a visible "-". +-- This simple hyphen glyph is a policy, NOT locale-specific shaping. +hidden_character : Char → Bool +hidden_character char = + let point = ord char in + point ≟ 173 || point ≟ 8203 || + point ≟ 10 || point ≟ 13 || + point ≟ 133 || point ≟ 8232 || point ≟ 8233 + +without_controls : List Char → List Char +without_controls [] = [] +without_controls (char :: rest) = + if hidden_character char + then without_controls rest + else char :: without_controls rest + +strip_trailing_space : List Char → List Char +strip_trailing_space [] = [] +strip_trailing_space (' ' :: rest) = strip_trailing_space rest +strip_trailing_space (char :: rest) = char :: rest + +source_line : Text → Number → SourceBreak → SourceLine +source_line source start (At finish kind) = + let span = FromSource start finish "" kind in + let raw = unpack (source_for_line source span) in + let painted = pack (reverse (strip_trailing_space + (reverse (without_controls raw)))) in + let shown = case kind of + DiscretionaryHyphen ⇒ painted ++ "-" + _ ⇒ painted in + FromSource start finish shown kind + +line_fits : (Text → Number) → Number → SourceLine → Bool +line_fits measure width line = + measure line.visible_text <= width + +terminal : BreakKind → Bool +terminal MandatoryBreak = True +terminal SourceEnd = True +terminal _ = False + +-- A greedy line chooses the farthest candidate that fits, stopping at the +-- first mandatory boundary. If not even the earliest candidate fits, emit +-- that atomic source run intact and report the overrun through line geometry. +-- It never invents an illegal break to stay inside the width. +last_fitting : Text → (Text → Number) → Number → Number → + SourceBreak → List SourceBreak → Maybe SourceBreak → SourceBreak +last_fitting source measure width start first [] chosen = + case chosen of + Nothing ⇒ first + Just answer ⇒ answer +last_fitting source measure width start first (candidate :: more) chosen = + let fits = line_fits measure width (source_line source start candidate) in + let best = if fits then Just candidate else chosen in + if terminal candidate.break_kind + then case best of + Nothing ⇒ first + Just answer ⇒ answer + else last_fitting source measure width start first more best + +select_greedy : Text → (Text → Number) → Number → Number → + List SourceBreak → SourceBreak +select_greedy source measure width start [] = At start SourceEnd +select_greedy source measure width start (first :: later) = + if terminal first.break_kind + then first + else let first_fit = line_fits measure width + (source_line source start first) in + last_fitting source measure width start first later + (if first_fit then Just first else Nothing) + +after_cut : Number → List SourceBreak → List SourceBreak +after_cut offset [] = [] +after_cut offset (cut :: rest) = + if cut.source_offset <= offset then after_cut offset rest + else cut :: rest + +greedy_lines : Text → (Text → Number) → Number → Number → + List SourceBreak → List SourceLine +greedy_lines source measure width start [] = [] +greedy_lines source measure width start cuts = + let chosen = select_greedy source measure width start cuts in + source_line source start chosen :: + greedy_lines source measure width chosen.source_offset + (after_cut chosen.source_offset cuts) + +record SourcePlan where + constructor PlannedSource + total_cost : Number + number_of_lines : Number + lines : List SourceLine + +badness : reflow_adverb → Number → Number → Bool → Number +badness mode width used last = + let unused = nonnegative_difference width used in + if used > width + then let excess = nonnegative_difference used width in + 1000000000 + excess * excess + else case mode of + ignoring_final_line ⇒ if last then 0 else unused * unused + minimizing_raggedness ⇒ unused * unused * unused + _ ⇒ unused * unused + +combined_cost : reflow_adverb → Number → Number → Number +combined_cost minimizing_worst_gap first later = + if first >= later then first else later +combined_cost _ first later = first + later + +soft_hyphen_cost : BreakKind → Number +soft_hyphen_cost DiscretionaryHyphen = 50 +soft_hyphen_cost _ = 0 + +candidate_plan : Text → reflow_adverb → (Text → Number) → Number → + Number → SourceBreak → SourcePlan → SourcePlan +candidate_plan source mode measure width start cut (PlannedSource tail_cost count tail) = + let line = source_line source start cut in + let last = cut.source_offset ≟ length (unpack source) in + let cost = badness mode width (measure line.visible_text) last in + let adjusted = cost + soft_hyphen_cost cut.break_kind in + PlannedSource (combined_cost mode adjusted tail_cost) + (S count) (line :: tail) + +prefer_plan : reflow_adverb → SourcePlan → SourcePlan → SourcePlan +prefer_plan without_extra_lines first second = + if first.number_of_lines < second.number_of_lines then first + else if first.number_of_lines > second.number_of_lines then second + else if first.total_cost <= second.total_cost then first else second +prefer_plan mode first second = + if first.total_cost <= second.total_cost then first else second + +update_best : reflow_adverb → Maybe SourcePlan → SourcePlan → Maybe SourcePlan +update_best mode Nothing candidate = Just candidate +update_best mode (Just current) candidate = + Just (prefer_plan mode current candidate) + +-- Candidate plans are aligned with the source offsets of cuts. The first +-- candidate is always admissible, even if it exceeds the width; later ones +-- must fit. Required boundaries cap the search, so a plan cannot cross them. +consider_cuts : Text → reflow_adverb → (Text → Number) → Number → + Number → Bool → List SourceBreak → List SourcePlan → + Maybe SourcePlan → Maybe SourcePlan +consider_cuts source mode measure width start first [] plans best = best +consider_cuts source mode measure width start first cuts [] best = best +consider_cuts source mode measure width start first + (cut :: rest) (tail :: tails) best = + let line = source_line source start cut in + let admissible = first || line_fits measure width line in + let next_best = + if admissible + then update_best mode best + (candidate_plan source mode measure width start cut tail) + else best in + if terminal cut.break_kind + then next_best + else consider_cuts source mode measure width start False + rest tails next_best + +plan_from : Text → reflow_adverb → (Text → Number) → Number → + Number → List SourceBreak → List SourcePlan → SourcePlan +plan_from source mode measure width start cuts tails = + case consider_cuts source mode measure width start True cuts tails Nothing of + Just answer ⇒ answer + Nothing ⇒ PlannedSource 0 0 [] + +suffix_plans : Text → reflow_adverb → (Text → Number) → Number → + List SourceBreak → List SourcePlan +suffix_plans source mode measure width [] = [PlannedSource 0 0 []] +suffix_plans source mode measure width (At offset kind :: later) = + let tails = suffix_plans source mode measure width later in + let plan = plan_from source mode measure width offset later tails in + plan :: tails + +optimal_lines : Text → reflow_adverb → (Text → Number) → Number → + List SourceBreak → List SourceLine +optimal_lines source mode measure width cuts = + let tails = suffix_plans source mode measure width cuts in + let (PlannedSource _ _ lines) = plan_from source mode measure width 0 cuts tails in + lines + +-- On the source-bound representation the following requests are genuinely +-- implemented: greedy, minimum squared/cubic/maximum slack, final-line-free +-- and *exact* minimum-line-count/secondarily minimum-square-slack. +-- The last differs from the atomic-word threshold heuristic, by design. +-- Streaming requires a lifetime-aware source-offset accumulator, and TeX +-- needs actual variable-width glue/penalty nodes, so those fail explicitly. +public export +reflow_at_breaks : ReflowRequirements → (Text → Number) → Text → + List SourceBreak → Either Text (List SourceLine) +reflow_at_breaks (Requirements Z _) measure source cuts = + Left "Reflow width must be positive" +reflow_at_breaks (Requirements width mode) measure source cuts = + if not (valid_source_breaks source cuts) + then Left "Invalid, unsafe or incomplete source break opportunities" + else case unpack source of + [] ⇒ Right [] + _ ⇒ case mode of + promptly ⇒ Right (greedy_lines source measure width 0 cuts) + streamingly ⇒ Left "Source-offset streaming has not been qualified" + typographically ⇒ Left "Source-backed adjustable glue is not qualified" + _ ⇒ Right (optimal_lines source mode measure width cuts) + +public export +reflow_source : ReflowRequirements → (Text → Number) → Text → + Either Text (List SourceLine) +reflow_source requirements measure source = + reflow_at_breaks requirements measure source (source_breaks source) From ae685a1ede3f43d9b5fa5df13341bb5a613e83b1 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:40:21 -0400 Subject: [PATCH 4/8] Add source-identity and Unicode boundary refusal tests for source-preserving reflow --- src/SourceReflowSmoke.idric | 134 ++++++++++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) create mode 100644 src/SourceReflowSmoke.idric diff --git a/src/SourceReflowSmoke.idric b/src/SourceReflowSmoke.idric new file mode 100644 index 0000000..bca508e --- /dev/null +++ b/src/SourceReflowSmoke.idric @@ -0,0 +1,134 @@ +module SourceReflowSmoke + +import Data.Text +import IB.Reflow +import IB.Reflow.Source +import IB.Reflow.SourceBreaks +import System + +codepoint_width : Text → Number +codepoint_width value = length (unpack value) + +display_lines : List SourceLine → List Text +display_lines [] = [] +display_lines (line :: rest) = + line.visible_text :: display_lines rest + +matches : List Text → Either Text (List SourceLine) → Bool +matches wanted (Right lines) = wanted ≟ display_lines lines +matches wanted _ = False + +refused : Either Text (List SourceLine) → Bool +refused (Left _) = True +refused _ = False + +join_raw : Text → List SourceLine → Text +join_raw source [] = "" +join_raw source (line :: rest) = + source_for_line source line ++ join_raw source rest + +contiguous : Text → Number → List SourceLine → Bool +contiguous source offset [] = offset ≟ length (unpack source) +contiguous source offset (line :: rest) = + line.first_codepoint ≟ offset && + line.after_last_codepoint > offset && + line.after_last_codepoint <= length (unpack source) && + contiguous source line.after_last_codepoint rest + +source_unchanged : Text → Either Text (List SourceLine) → Bool +source_unchanged source (Right lines) = + join_raw source lines ≟ source && + contiguous source 0 lines +source_unchanged source _ = False + +kind_is : BreakKind → BreakKind → Bool +kind_is PossibleBreak PossibleBreak = True +kind_is MandatoryBreak MandatoryBreak = True +kind_is DiscretionaryHyphen DiscretionaryHyphen = True +kind_is ZeroWidthBreak ZeroWidthBreak = True +kind_is SourceEnd SourceEnd = True +kind_is _ _ = False + +has_cut : Number → BreakKind → List SourceBreak → Bool +has_cut offset wanted [] = False +has_cut offset wanted (cut :: rest) = + (offset ≟ cut.source_offset && kind_is wanted cut.break_kind) || + has_cut offset wanted rest + +some_breaks_are_refused : Bool +some_breaks_are_refused = + let source = "a\r\nb" in + let no_mandatory = [At 4 SourceEnd] in + let inside_crlf = [At 2 PossibleBreak, At 3 MandatoryBreak, At 4 SourceEnd] in + let duplicate = [At 2 PossibleBreak, At 2 PossibleBreak, At 3 SourceEnd] in + not (valid_source_breaks source no_mandatory) && + not (valid_source_breaks source inside_crlf) && + not (valid_source_breaks "a b" duplicate) && + not (valid_source_breaks "éx" [At 1 PossibleBreak, At 3 SourceEnd]) && + not (valid_source_breaks "👩‍💻x" [At 2 PossibleBreak, At 4 SourceEnd]) + +all_modes_preserve : Text → List reflow_adverb → Bool +all_modes_preserve source [] = True +all_modes_preserve source (mode :: rest) = + source_unchanged source + (reflow_source (Requirements 2 mode) codepoint_width source) && + all_modes_preserve source rest + +run_cases : Bool +run_cases = + let basic = matches ["red", "blue"] + (reflow_source (Requirements 4 promptly) codepoint_width "red blue") in + let soft = "ab­cd" in + let soft_short = matches ["ab-", "cd"] + (reflow_source (Requirements 3 promptly) codepoint_width soft) in + let soft_long = matches ["abcd"] + (reflow_source (Requirements 4 evenly) codepoint_width soft) in + let soft_source = source_unchanged soft + (reflow_source (Requirements 3 promptly) codepoint_width soft) in + let zero_width_space = matches ["ab", "cd"] + (reflow_source (Requirements 2 promptly) codepoint_width "ab​cd") in + let han = matches ["漢字", "漢字"] + (reflow_source (Requirements 2 evenly) codepoint_width "漢字漢字") in + let crlf = matches ["a", "b"] + (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in + let crlf_source = source_unchanged "a\r\nb" + (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in + let blank_line = matches ["a", "", "b"] + (reflow_source (Requirements 1 promptly) codepoint_width "a\n\nb") in + let nbspace = matches ["a b", "c"] + (reflow_source (Requirements 3 promptly) codepoint_width "a b c") in + let right_to_left = matches ["שלום", "hello"] + (reflow_source (Requirements 5 promptly) codepoint_width "שלום hello") in + let final_newline = matches ["end"] + (reflow_source (Requirements 5 promptly) codepoint_width "end\n") in + let no_break_before_joiner = not (has_cut 2 PossibleBreak (source_breaks "a ⁠b")) in + let correct_kinds = + has_cut 3 MandatoryBreak (source_breaks "a\r\nb") && + has_cut 3 DiscretionaryHyphen (source_breaks "ab­cd") && + has_cut 3 ZeroWidthBreak (source_breaks "ab​cd") in + let preserves_every_mode = all_modes_preserve + "a\r\n漢字 ab­cd" + [promptly, evenly, minimizing_raggedness, + ignoring_final_line, minimizing_worst_gap, without_extra_lines] in + let unsupported_modes = + refused (reflow_source (Requirements 5 typographically) + codepoint_width "aa bb") && + refused (reflow_source (Requirements 5 streamingly) + codepoint_width "aa bb") in + let bad_width = refused (reflow_source (Requirements 0 promptly) + codepoint_width "abc") in + let bad_breaks = refused (reflow_at_breaks (Requirements 5 promptly) + codepoint_width "a\r\nb" [At 4 SourceEnd]) in + let empty_input = matches [] + (reflow_source (Requirements 5 promptly) codepoint_width "") in + basic && soft_short && soft_long && soft_source && zero_width_space && + han && crlf && crlf_source && blank_line && nbspace && right_to_left && + final_newline && no_break_before_joiner && correct_kinds && + preserves_every_mode && unsupported_modes && bad_width && bad_breaks && + empty_input && some_breaks_are_refused + +main : IO () +main = do + let passed = run_cases + putStrLn ("source-reflow-unicode-offset-cases=" ++ show passed) + if passed then pure () else exitFailure From 4c7ac3f4529e39b953b8fe9a8cefcb4c89038e95 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:40:41 -0400 Subject: [PATCH 5/8] =?UTF-8?q?Run=20source-bound=20Unicode=20line-break?= =?UTF-8?q?=20and=20identity=20tests=20through=20existing=20Idri=C3=A7=20C?= =?UTF-8?q?I?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- bin/ci_browser_foundation.grease | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/bin/ci_browser_foundation.grease b/bin/ci_browser_foundation.grease index 1d53849..a775152 100755 --- a/bin/ci_browser_foundation.grease +++ b/bin/ci_browser_foundation.grease @@ -153,6 +153,10 @@ build_information_programs() { 2>&1 | tee /tmp/idric-reflow-compile.txt test -x ./build/exec/ib-reflow-smoke ! grep -q '^Error:' /tmp/idric-reflow-compile.txt + "$idric_prefix/bin/idris2" SourceReflowSmoke.idric -o ib-source-reflow-smoke \ + 2>&1 | tee /tmp/idric-source-reflow-compile.txt + test -x ./build/exec/ib-source-reflow-smoke + ! grep -q '^Error:' /tmp/idric-source-reflow-compile.txt } exercise_information() { @@ -199,6 +203,8 @@ exercise_information() { grep -Fx 'reflow-knuth-spacings=True' /tmp/ib-reflow-smoke.txt grep -Fx 'reflow-incremental-revisions=True' /tmp/ib-reflow-smoke.txt grep -Fx 'reflow-arithmetic=True' /tmp/ib-reflow-smoke.txt + src/build/exec/ib-source-reflow-smoke | tee /tmp/ib-source-reflow-smoke.txt + grep -Fx 'source-reflow-unicode-offset-cases=True' /tmp/ib-source-reflow-smoke.txt sh -n bin/prepaint_arxiv_progressively.grease sh -n tests/test_arxiv_progressive_prepaint.grease sh tests/test_arxiv_progressive_prepaint.grease From 01e299d213ffdb2b2fd93323e0f7128c502dd357 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:48:17 -0400 Subject: [PATCH 6/8] Simplify source reflow parser-sensitive nested case/let expressions --- src/IB/Reflow/Source.idric | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/src/IB/Reflow/Source.idric b/src/IB/Reflow/Source.idric index f29afc8..82fcce4 100644 --- a/src/IB/Reflow/Source.idric +++ b/src/IB/Reflow/Source.idric @@ -29,16 +29,16 @@ strip_trailing_space [] = [] strip_trailing_space (' ' :: rest) = strip_trailing_space rest strip_trailing_space (char :: rest) = char :: rest +display_break_mark : BreakKind → Text → Text +display_break_mark DiscretionaryHyphen painted = painted ++ "-" +display_break_mark _ painted = painted + source_line : Text → Number → SourceBreak → SourceLine source_line source start (At finish kind) = let span = FromSource start finish "" kind in let raw = unpack (source_for_line source span) in - let painted = pack (reverse (strip_trailing_space - (reverse (without_controls raw)))) in - let shown = case kind of - DiscretionaryHyphen ⇒ painted ++ "-" - _ ⇒ painted in - FromSource start finish shown kind + let painted = pack (reverse (strip_trailing_space (reverse (without_controls raw)))) in + FromSource start finish (display_break_mark kind painted) kind line_fits : (Text → Number) → Number → SourceLine → Bool line_fits measure width line = @@ -155,15 +155,14 @@ consider_cuts source mode measure width start first (cut :: rest) (tail :: tails) best = let line = source_line source start cut in let admissible = first || line_fits measure width line in - let next_best = - if admissible - then update_best mode best - (candidate_plan source mode measure width start cut tail) - else best in if terminal cut.break_kind - then next_best - else consider_cuts source mode measure width start False - rest tails next_best + then if admissible + then update_best mode best (candidate_plan source mode measure width start cut tail) + else best + else if admissible + then consider_cuts source mode measure width start False rest tails + (update_best mode best (candidate_plan source mode measure width start cut tail)) + else consider_cuts source mode measure width start False rest tails best plan_from : Text → reflow_adverb → (Text → Number) → Number → Number → List SourceBreak → List SourcePlan → SourcePlan From 61cbc1bdcb6318748d0511d3b2e5420a50ace878 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 17 Oct 2026 19:48:57 -0400 Subject: [PATCH 7/8] =?UTF-8?q?Keep=20source=20reflow=20smoke=20call=20sit?= =?UTF-8?q?es=20compatible=20with=20pinned=20Idri=C3=A7=20parser?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/SourceReflowSmoke.idric | 52 +++++++++++++------------------------ 1 file changed, 18 insertions(+), 34 deletions(-) diff --git a/src/SourceReflowSmoke.idric b/src/SourceReflowSmoke.idric index bca508e..c25b894 100644 --- a/src/SourceReflowSmoke.idric +++ b/src/SourceReflowSmoke.idric @@ -76,51 +76,35 @@ all_modes_preserve source (mode :: rest) = run_cases : Bool run_cases = - let basic = matches ["red", "blue"] - (reflow_source (Requirements 4 promptly) codepoint_width "red blue") in + let basic = matches ["red", "blue"] (reflow_source (Requirements 4 promptly) codepoint_width "red blue") in let soft = "ab­cd" in - let soft_short = matches ["ab-", "cd"] - (reflow_source (Requirements 3 promptly) codepoint_width soft) in - let soft_long = matches ["abcd"] - (reflow_source (Requirements 4 evenly) codepoint_width soft) in - let soft_source = source_unchanged soft - (reflow_source (Requirements 3 promptly) codepoint_width soft) in - let zero_width_space = matches ["ab", "cd"] - (reflow_source (Requirements 2 promptly) codepoint_width "ab​cd") in - let han = matches ["漢字", "漢字"] - (reflow_source (Requirements 2 evenly) codepoint_width "漢字漢字") in - let crlf = matches ["a", "b"] - (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in - let crlf_source = source_unchanged "a\r\nb" - (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in - let blank_line = matches ["a", "", "b"] - (reflow_source (Requirements 1 promptly) codepoint_width "a\n\nb") in - let nbspace = matches ["a b", "c"] - (reflow_source (Requirements 3 promptly) codepoint_width "a b c") in - let right_to_left = matches ["שלום", "hello"] - (reflow_source (Requirements 5 promptly) codepoint_width "שלום hello") in - let final_newline = matches ["end"] - (reflow_source (Requirements 5 promptly) codepoint_width "end\n") in + let soft_short = matches ["ab-", "cd"] (reflow_source (Requirements 3 promptly) codepoint_width soft) in + let soft_long = matches ["abcd"] (reflow_source (Requirements 4 evenly) codepoint_width soft) in + let soft_source = source_unchanged soft (reflow_source (Requirements 3 promptly) codepoint_width soft) in + let zero_width_space = matches ["ab", "cd"] (reflow_source (Requirements 2 promptly) codepoint_width "ab​cd") in + let han = matches ["漢字", "漢字"] (reflow_source (Requirements 2 evenly) codepoint_width "漢字漢字") in + let crlf = matches ["a", "b"] (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in + let crlf_source = source_unchanged "a\r\nb" (reflow_source (Requirements 1 promptly) codepoint_width "a\r\nb") in + let blank_line = matches ["a", "", "b"] (reflow_source (Requirements 1 promptly) codepoint_width "a\n\nb") in + let nbspace = matches ["a b", "c"] (reflow_source (Requirements 3 promptly) codepoint_width "a b c") in + let right_to_left = matches ["שלום", "hello"] (reflow_source (Requirements 5 promptly) codepoint_width "שלום hello") in + let final_newline = matches ["end"] (reflow_source (Requirements 5 promptly) codepoint_width "end\n") in let no_break_before_joiner = not (has_cut 2 PossibleBreak (source_breaks "a ⁠b")) in let correct_kinds = has_cut 3 MandatoryBreak (source_breaks "a\r\nb") && has_cut 3 DiscretionaryHyphen (source_breaks "ab­cd") && has_cut 3 ZeroWidthBreak (source_breaks "ab​cd") in - let preserves_every_mode = all_modes_preserve - "a\r\n漢字 ab­cd" - [promptly, evenly, minimizing_raggedness, - ignoring_final_line, minimizing_worst_gap, without_extra_lines] in + let preserves_every_mode = all_modes_preserve "a\r\n漢字 ab­cd" + [promptly, evenly, minimizing_raggedness, ignoring_final_line, + minimizing_worst_gap, without_extra_lines] in let unsupported_modes = refused (reflow_source (Requirements 5 typographically) codepoint_width "aa bb") && refused (reflow_source (Requirements 5 streamingly) codepoint_width "aa bb") in - let bad_width = refused (reflow_source (Requirements 0 promptly) - codepoint_width "abc") in - let bad_breaks = refused (reflow_at_breaks (Requirements 5 promptly) - codepoint_width "a\r\nb" [At 4 SourceEnd]) in - let empty_input = matches [] - (reflow_source (Requirements 5 promptly) codepoint_width "") in + let bad_width = refused (reflow_source (Requirements 0 promptly) codepoint_width "abc") in + let bad_breaks = refused (reflow_at_breaks (Requirements 5 promptly) codepoint_width "a\r\nb" [At 4 SourceEnd]) in + let empty_input = matches [] (reflow_source (Requirements 5 promptly) codepoint_width "") in basic && soft_short && soft_long && soft_source && zero_width_space && han && crlf && crlf_source && blank_line && nbspace && right_to_left && final_newline && no_break_before_joiner && correct_kinds && From 4a7380c5f25409443c5e8c1ae17bd358372012fc Mon Sep 17 00:00:00 2001 From: i Date: Mon, 19 Oct 2026 19:57:46 -0400 Subject: [PATCH 8/8] Make source reflow total and repair pinned-compiler smoke syntax Annotate the candidate selection, bound greedy recursion by the candidate count and refuse exhausted descent, and keep multiline smoke applications within the pinned parser's accepted syntax. The original Unicode/source-offset, all-mode, unsupported-mode and full reflow assertions remain intact. --- src/IB/Reflow/Source.idric | 24 +++++++++++++++--------- src/SourceReflowSmoke.idric | 10 +++------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/IB/Reflow/Source.idric b/src/IB/Reflow/Source.idric index 82fcce4..32a4508 100644 --- a/src/IB/Reflow/Source.idric +++ b/src/IB/Reflow/Source.idric @@ -61,7 +61,7 @@ last_fitting source measure width start first [] chosen = Just answer ⇒ answer last_fitting source measure width start first (candidate :: more) chosen = let fits = line_fits measure width (source_line source start candidate) in - let best = if fits then Just candidate else chosen in + let best : Maybe SourceBreak = if fits then Just candidate else chosen in if terminal candidate.break_kind then case best of Nothing ⇒ first @@ -85,14 +85,20 @@ after_cut offset (cut :: rest) = if cut.source_offset <= offset then after_cut offset rest else cut :: rest -greedy_lines : Text → (Text → Number) → Number → Number → - List SourceBreak → List SourceLine -greedy_lines source measure width start [] = [] -greedy_lines source measure width start cuts = +-- A valid selection consumes at least one candidate. Bound recursive descent +-- by the original candidate count; an exhausted budget refuses the projection +-- rather than silently dropping source or asserting an unchecked termination. +greedy_lines : Number → Text → (Text → Number) → Number → Number → + List SourceBreak → Either Text (List SourceLine) +greedy_lines remaining_choices source measure width start [] = Right [] +greedy_lines Z source measure width start cuts = + Left "Reflow candidate budget exhausted" +greedy_lines (S remaining_choices) source measure width start cuts = let chosen = select_greedy source measure width start cuts in - source_line source start chosen :: - greedy_lines source measure width chosen.source_offset - (after_cut chosen.source_offset cuts) + case greedy_lines remaining_choices source measure width chosen.source_offset + (after_cut chosen.source_offset cuts) of + Left message ⇒ Left message + Right later_lines ⇒ Right (source_line source start chosen :: later_lines) record SourcePlan where constructor PlannedSource @@ -203,7 +209,7 @@ reflow_at_breaks (Requirements width mode) measure source cuts = else case unpack source of [] ⇒ Right [] _ ⇒ case mode of - promptly ⇒ Right (greedy_lines source measure width 0 cuts) + promptly ⇒ greedy_lines (length cuts) source measure width 0 cuts streamingly ⇒ Left "Source-offset streaming has not been qualified" typographically ⇒ Left "Source-backed adjustable glue is not qualified" _ ⇒ Right (optimal_lines source mode measure width cuts) diff --git a/src/SourceReflowSmoke.idric b/src/SourceReflowSmoke.idric index c25b894..41d0c7d 100644 --- a/src/SourceReflowSmoke.idric +++ b/src/SourceReflowSmoke.idric @@ -94,14 +94,10 @@ run_cases = has_cut 3 MandatoryBreak (source_breaks "a\r\nb") && has_cut 3 DiscretionaryHyphen (source_breaks "ab­cd") && has_cut 3 ZeroWidthBreak (source_breaks "ab​cd") in - let preserves_every_mode = all_modes_preserve "a\r\n漢字 ab­cd" - [promptly, evenly, minimizing_raggedness, ignoring_final_line, - minimizing_worst_gap, without_extra_lines] in + let preserves_every_mode = all_modes_preserve "a\r\n漢字 ab­cd" [promptly, evenly, minimizing_raggedness, ignoring_final_line, minimizing_worst_gap, without_extra_lines] in let unsupported_modes = - refused (reflow_source (Requirements 5 typographically) - codepoint_width "aa bb") && - refused (reflow_source (Requirements 5 streamingly) - codepoint_width "aa bb") in + refused (reflow_source (Requirements 5 typographically) codepoint_width "aa bb") && + refused (reflow_source (Requirements 5 streamingly) codepoint_width "aa bb") in let bad_width = refused (reflow_source (Requirements 0 promptly) codepoint_width "abc") in let bad_breaks = refused (reflow_at_breaks (Requirements 5 promptly) codepoint_width "a\r\nb" [At 4 SourceEnd]) in let empty_input = matches [] (reflow_source (Requirements 5 promptly) codepoint_width "") in