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 diff --git a/src/IB/Reflow/Source.idric b/src/IB/Reflow/Source.idric new file mode 100644 index 0000000..32a4508 --- /dev/null +++ b/src/IB/Reflow/Source.idric @@ -0,0 +1,221 @@ +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 + +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 + FromSource start finish (display_break_mark kind painted) 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 : Maybe SourceBreak = 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 + +-- 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 + 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 + 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 + if terminal cut.break_kind + 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 +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 ⇒ 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) + +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) diff --git a/src/IB/Reflow/SourceBreaks.idric b/src/IB/Reflow/SourceBreaks.idric new file mode 100644 index 0000000..f7ba27c --- /dev/null +++ b/src/IB/Reflow/SourceBreaks.idric @@ -0,0 +1,201 @@ +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. +-- 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 + 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 + [] ⇒ 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 → 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) && + (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 +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 && + 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 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. +-- 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 (nonnegative_difference line.after_last_codepoint line.first_codepoint) + (drop line.first_codepoint (unpack source))) diff --git a/src/SourceReflowSmoke.idric b/src/SourceReflowSmoke.idric new file mode 100644 index 0000000..41d0c7d --- /dev/null +++ b/src/SourceReflowSmoke.idric @@ -0,0 +1,114 @@ +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