From 17e7c0d78debcef20c58949b851675e160fe6b07 Mon Sep 17 00:00:00 2001 From: i Date: Fri, 11 Sep 2026 22:38:43 -0400 Subject: [PATCH 1/5] Add source occurrence strand semantics --- src/IB/Occurrence.idric | 197 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 src/IB/Occurrence.idric diff --git a/src/IB/Occurrence.idric b/src/IB/Occurrence.idric new file mode 100644 index 00000000..99f2e431 --- /dev/null +++ b/src/IB/Occurrence.idric @@ -0,0 +1,197 @@ +module IB.Occurrence + +%default total + +-- Authoritative source text remains separate from fragment and strand indexes. +public export +data AuthoritativeText = SourceText String String + +public export +source_id : AuthoritativeText → String +source_id (SourceText value _) = value + +public export +source_text : AuthoritativeText → String +source_text (SourceText _ value) = value + +-- Source ranges are half-open: source_start <= coordinate < source_end. +public export +data SourceFragment = Fragment String String Nat Nat + +public export +fragment_id : SourceFragment → String +fragment_id (Fragment value _ _ _) = value + +public export +fragment_source_id : SourceFragment → String +fragment_source_id (Fragment _ value _ _) = value + +public export +fragment_source_start : SourceFragment → Nat +fragment_source_start (Fragment _ _ value _) = value + +public export +fragment_source_end : SourceFragment → Nat +fragment_source_end (Fragment _ _ _ value) = value + +-- A materialized strand keeps the hot document-order path contiguous. +public export +data DocumentStrand = Strand String String (List String) + +public export +strand_id : DocumentStrand → String +strand_id (Strand value _ _) = value + +public export +strand_source_id : DocumentStrand → String +strand_source_id (Strand _ value _) = value + +public export +strand_fragment_ids : DocumentStrand → List String +strand_fragment_ids (Strand _ _ value) = value + +-- Each literal occurrence retains both its source coordinate and its position +-- on the materialized strand. The fragment id remains the durable identity. +public export +data Occurrence = Hit Nat Nat String + +public export +occurrence_source_start : Occurrence → Nat +occurrence_source_start (Hit value _ _) = value + +public export +occurrence_strand_position : Occurrence → Nat +occurrence_strand_position (Hit _ value _) = value + +public export +occurrence_fragment_id : Occurrence → String +occurrence_fragment_id (Hit _ _ value) = value + +starts_with_chars : List Char → List Char → Bool +starts_with_chars [] _ = True +starts_with_chars (_ :: _) [] = False +starts_with_chars (wanted :: wanted_rest) (value :: rest) = + wanted == value && starts_with_chars wanted_rest rest + +literal_offsets_from : Nat → List Char → List Char → List Nat +literal_offsets_from position wanted [] = [] +literal_offsets_from position wanted chars@(_ :: rest) = + if starts_with_chars wanted chars + then position :: literal_offsets_from (S position) wanted rest + else literal_offsets_from (S position) wanted rest + +-- Empty text is not treated as an occurrence at every source coordinate. +public export +literal_offsets : String → AuthoritativeText → List Nat +literal_offsets wanted source = + if wanted == "" + then [] + else literal_offsets_from 0 (unpack wanted) (unpack (source_text source)) + +nat_less : Nat → Nat → Bool +nat_less Z Z = False +nat_less Z (S _) = True +nat_less (S _) Z = False +nat_less (S left) (S right) = nat_less left right + +contains_coordinate : Nat → SourceFragment → Bool +contains_coordinate coordinate fragment = + not (nat_less coordinate (fragment_source_start fragment)) && + nat_less coordinate (fragment_source_end fragment) + +fragment_at_coordinate : String → Nat → List SourceFragment → Maybe String +fragment_at_coordinate wanted_source coordinate [] = Nothing +fragment_at_coordinate wanted_source coordinate (fragment :: rest) = + if fragment_source_id fragment == wanted_source && contains_coordinate coordinate fragment + then Just (fragment_id fragment) + else fragment_at_coordinate wanted_source coordinate rest + +strand_position_from : Nat → String → List String → Maybe Nat +strand_position_from position wanted [] = Nothing +strand_position_from position wanted (value :: rest) = + if wanted == value + then Just position + else strand_position_from (S position) wanted rest + +strand_position : String → DocumentStrand → Maybe Nat +strand_position wanted strand = strand_position_from 0 wanted (strand_fragment_ids strand) + +occurrence_at : String → List SourceFragment → DocumentStrand → Nat → Maybe Occurrence +occurrence_at wanted_source fragments strand coordinate = + case fragment_at_coordinate wanted_source coordinate fragments of + Nothing ⇒ Nothing + Just found_fragment ⇒ + case strand_position found_fragment strand of + Nothing ⇒ Nothing + Just position ⇒ Just (Hit coordinate position found_fragment) + +collect_occurrences : String → List SourceFragment → DocumentStrand → List Nat → List Occurrence +collect_occurrences wanted_source fragments strand [] = [] +collect_occurrences wanted_source fragments strand (coordinate :: rest) = + case occurrence_at wanted_source fragments strand coordinate of + Nothing ⇒ collect_occurrences wanted_source fragments strand rest + Just occurrence ⇒ occurrence :: collect_occurrences wanted_source fragments strand rest + +-- Search the authoritative source, then map each exact match back onto stable +-- fragments and the materialized document-order strand. No alias, fuzzy, +-- semantic, or model-derived matching occurs here. +public export +search_occurrences : String → AuthoritativeText → List SourceFragment → DocumentStrand → List Occurrence +search_occurrences wanted source fragments strand = + if source_id source == strand_source_id strand + then collect_occurrences (source_id source) fragments strand (literal_offsets wanted source) + else [] + +seen_fragment : String → List String → Bool +seen_fragment wanted [] = False +seen_fragment wanted (value :: rest) = wanted == value || seen_fragment wanted rest + +unique_occurrence_fragments : List String → List Occurrence → List String +unique_occurrence_fragments seen [] = [] +unique_occurrence_fragments seen (occurrence :: rest) = + let value = occurrence_fragment_id occurrence in + if seen_fragment value seen + then unique_occurrence_fragments seen rest + else value :: unique_occurrence_fragments (value :: seen) rest + +public export +matching_fragment_ids : String → AuthoritativeText → List SourceFragment → DocumentStrand → List String +matching_fragment_ids wanted source fragments strand = + unique_occurrence_fragments [] (search_occurrences wanted source fragments strand) + +subtract_saturating : Nat → Nat → Nat +subtract_saturating value Z = value +subtract_saturating Z (S _) = Z +subtract_saturating (S value) (S amount) = subtract_saturating value amount + +window_from : Nat → Nat → Nat → List String → List String +window_from index lower upper [] = [] +window_from index lower upper (value :: rest) = + if nat_less upper index + then [] + else if nat_less index lower + then window_from (S index) lower upper rest + else value :: window_from (S index) lower upper rest + +fragment_id_at : Nat → List String → Maybe String +fragment_id_at Z [] = Nothing +fragment_id_at Z (value :: _) = Just value +fragment_id_at (S position) [] = Nothing +fragment_id_at (S position) (_ :: rest) = fragment_id_at position rest + +-- A hit is only windowed against the strand revision it still matches. A stale +-- position/id pair fails rather than silently returning context around a +-- different fragment. +public export +context_fragment_ids : Nat → Nat → Occurrence → DocumentStrand → Maybe (List String) +context_fragment_ids before after occurrence strand = + let position = occurrence_strand_position occurrence in + let ids = strand_fragment_ids strand in + case fragment_id_at position ids of + Nothing ⇒ Nothing + Just current ⇒ + if current == occurrence_fragment_id occurrence + then let lower = subtract_saturating position before in + let upper = position + after in + Just (window_from 0 lower upper ids) + else Nothing From 717e1615fd6f535952ec1d8df06cf42f7320d55d Mon Sep 17 00:00:00 2001 From: i Date: Fri, 11 Sep 2026 22:39:05 -0400 Subject: [PATCH 2/5] Exercise occurrence strand semantics --- src/OccurrenceSmoke.idric | 68 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 src/OccurrenceSmoke.idric diff --git a/src/OccurrenceSmoke.idric b/src/OccurrenceSmoke.idric new file mode 100644 index 00000000..9bbdc7f9 --- /dev/null +++ b/src/OccurrenceSmoke.idric @@ -0,0 +1,68 @@ +module OccurrenceSmoke + +import IB.Occurrence + +%default total + +sample_source : AuthoritativeText +sample_source = SourceText "fixture:known-reading:sherlock-adventures" "Holmes one.\nWatson two.\nHolmes three.\nAdler four." + +sample_fragments : List SourceFragment +sample_fragments = [ + Fragment "f0001" "fixture:known-reading:sherlock-adventures" 0 12, + Fragment "f0002" "fixture:known-reading:sherlock-adventures" 12 24, + Fragment "f0003" "fixture:known-reading:sherlock-adventures" 24 38, + Fragment "f0004" "fixture:known-reading:sherlock-adventures" 38 49 + ] + +sample_strand : DocumentStrand +sample_strand = Strand + "document-order:sherlock-adventures" + "fixture:known-reading:sherlock-adventures" + ["f0001", "f0002", "f0003", "f0004"] + +unicode_source : AuthoritativeText +unicode_source = SourceText "fixture:unicode" "東京と京都" + +unicode_fragments : List SourceFragment +unicode_fragments = [Fragment "u0001" "fixture:unicode" 0 5] + +unicode_strand : DocumentStrand +unicode_strand = Strand "document-order:unicode" "fixture:unicode" ["u0001"] + +occurrence_at_index : Nat → List Occurrence → Maybe Occurrence +occurrence_at_index Z [] = Nothing +occurrence_at_index Z (value :: _) = Just value +occurrence_at_index (S index) [] = Nothing +occurrence_at_index (S index) (_ :: rest) = occurrence_at_index index rest + +window_count : Nat → Nat → Maybe Occurrence → DocumentStrand → Nat +window_count before after Nothing strand = 0 +window_count before after (Just occurrence) strand = + case context_fragment_ids before after occurrence strand of + Nothing ⇒ 0 + Just ids ⇒ length ids + +window_available : Nat → Nat → Maybe Occurrence → DocumentStrand → Bool +window_available before after Nothing strand = False +window_available before after (Just occurrence) strand = + case context_fragment_ids before after occurrence strand of + Nothing ⇒ False + Just _ ⇒ True + +main : IO () +main = do + let holmes = search_occurrences "Holmes" sample_source sample_fragments sample_strand + let crossing = search_occurrences "one.\nWatson" sample_source sample_fragments sample_strand + let unicode = search_occurrences "京都" unicode_source unicode_fragments unicode_strand + let stale = Strand + "document-order:sherlock-adventures:changed" + "fixture:known-reading:sherlock-adventures" + ["f0002", "f0001", "f0003", "f0004"] + putStrLn ("occurrence-count=" ++ show (length holmes)) + putStrLn ("matching-fragment-count=" ++ show (length (matching_fragment_ids "Holmes" sample_source sample_fragments sample_strand))) + putStrLn ("cross-boundary-count=" ++ show (length crossing)) + putStrLn ("first-window-count=" ++ show (window_count 1 1 (occurrence_at_index 0 holmes) sample_strand)) + putStrLn ("second-window-count=" ++ show (window_count 1 1 (occurrence_at_index 1 holmes) sample_strand)) + putStrLn ("stale-window=" ++ show (window_available 1 1 (occurrence_at_index 0 holmes) stale)) + putStrLn ("unicode-count=" ++ show (length unicode)) From 5d7debb86ace6bdf626102e38a2b2e4f8f8983f3 Mon Sep 17 00:00:00 2001 From: i Date: Fri, 11 Sep 2026 22:40:34 -0400 Subject: [PATCH 3/5] Exercise occurrence strand semantics in core CI --- bin/ci_browser_foundation.grease | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/bin/ci_browser_foundation.grease b/bin/ci_browser_foundation.grease index 105a2556..45e90f0c 100755 --- a/bin/ci_browser_foundation.grease +++ b/bin/ci_browser_foundation.grease @@ -54,6 +54,19 @@ exercise_core() { grep -Fx 'temporary-needs-language-model=True' /tmp/ib-smoke.txt grep -Fx 'prefetch-bounded=2' /tmp/ib-smoke.txt grep -Fx 'prefetch-reading=1' /tmp/ib-smoke.txt + + "$idric_prefix/bin/idris2" OccurrenceSmoke.idric -o ib-occurrence-smoke \ + 2>&1 | tee /tmp/idric-occurrence-compile.txt + test -x ./build/exec/ib-occurrence-smoke + ! grep -q '^Error:' /tmp/idric-occurrence-compile.txt + ./build/exec/ib-occurrence-smoke | tee /tmp/ib-occurrence-smoke.txt + grep -Fx 'occurrence-count=2' /tmp/ib-occurrence-smoke.txt + grep -Fx 'matching-fragment-count=2' /tmp/ib-occurrence-smoke.txt + grep -Fx 'cross-boundary-count=1' /tmp/ib-occurrence-smoke.txt + grep -Fx 'first-window-count=2' /tmp/ib-occurrence-smoke.txt + grep -Fx 'second-window-count=3' /tmp/ib-occurrence-smoke.txt + grep -Fx 'stale-window=False' /tmp/ib-occurrence-smoke.txt + grep -Fx 'unicode-count=1' /tmp/ib-occurrence-smoke.txt } exercise_workbench() { From 8a716cee7f07762e9f463c6b56ac2b390a69bebe Mon Sep 17 00:00:00 2001 From: i Date: Fri, 11 Sep 2026 22:42:15 -0400 Subject: [PATCH 4/5] Keep strands source-agnostic --- src/IB/Occurrence.idric | 41 +++++++++++++++++++---------------------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/src/IB/Occurrence.idric b/src/IB/Occurrence.idric index 99f2e431..f60674b7 100644 --- a/src/IB/Occurrence.idric +++ b/src/IB/Occurrence.idric @@ -34,24 +34,22 @@ public export fragment_source_end : SourceFragment → Nat fragment_source_end (Fragment _ _ _ value) = value --- A materialized strand keeps the hot document-order path contiguous. +-- A strand is source-agnostic. The occurrence path uses a document-order +-- strand, but other strands may cross source boundaries. public export -data DocumentStrand = Strand String String (List String) +data Strand = MaterializedStrand String (List String) public export -strand_id : DocumentStrand → String -strand_id (Strand value _ _) = value +strand_id : Strand → String +strand_id (MaterializedStrand value _) = value public export -strand_source_id : DocumentStrand → String -strand_source_id (Strand _ value _) = value - -public export -strand_fragment_ids : DocumentStrand → List String -strand_fragment_ids (Strand _ _ value) = value +strand_fragment_ids : Strand → List String +strand_fragment_ids (MaterializedStrand _ value) = value -- Each literal occurrence retains both its source coordinate and its position --- on the materialized strand. The fragment id remains the durable identity. +-- on the supplied materialized strand. The fragment id remains the durable +-- identity. public export data Occurrence = Hit Nat Nat String @@ -113,10 +111,10 @@ strand_position_from position wanted (value :: rest) = then Just position else strand_position_from (S position) wanted rest -strand_position : String → DocumentStrand → Maybe Nat +strand_position : String → Strand → Maybe Nat strand_position wanted strand = strand_position_from 0 wanted (strand_fragment_ids strand) -occurrence_at : String → List SourceFragment → DocumentStrand → Nat → Maybe Occurrence +occurrence_at : String → List SourceFragment → Strand → Nat → Maybe Occurrence occurrence_at wanted_source fragments strand coordinate = case fragment_at_coordinate wanted_source coordinate fragments of Nothing ⇒ Nothing @@ -125,7 +123,7 @@ occurrence_at wanted_source fragments strand coordinate = Nothing ⇒ Nothing Just position ⇒ Just (Hit coordinate position found_fragment) -collect_occurrences : String → List SourceFragment → DocumentStrand → List Nat → List Occurrence +collect_occurrences : String → List SourceFragment → Strand → List Nat → List Occurrence collect_occurrences wanted_source fragments strand [] = [] collect_occurrences wanted_source fragments strand (coordinate :: rest) = case occurrence_at wanted_source fragments strand coordinate of @@ -133,14 +131,13 @@ collect_occurrences wanted_source fragments strand (coordinate :: rest) = Just occurrence ⇒ occurrence :: collect_occurrences wanted_source fragments strand rest -- Search the authoritative source, then map each exact match back onto stable --- fragments and the materialized document-order strand. No alias, fuzzy, --- semantic, or model-derived matching occurs here. +-- fragments and the supplied materialized strand. For #54 that strand is the +-- source's document-order strand. No alias, fuzzy, semantic, or model-derived +-- matching occurs here. public export -search_occurrences : String → AuthoritativeText → List SourceFragment → DocumentStrand → List Occurrence +search_occurrences : String → AuthoritativeText → List SourceFragment → Strand → List Occurrence search_occurrences wanted source fragments strand = - if source_id source == strand_source_id strand - then collect_occurrences (source_id source) fragments strand (literal_offsets wanted source) - else [] + collect_occurrences (source_id source) fragments strand (literal_offsets wanted source) seen_fragment : String → List String → Bool seen_fragment wanted [] = False @@ -155,7 +152,7 @@ unique_occurrence_fragments seen (occurrence :: rest) = else value :: unique_occurrence_fragments (value :: seen) rest public export -matching_fragment_ids : String → AuthoritativeText → List SourceFragment → DocumentStrand → List String +matching_fragment_ids : String → AuthoritativeText → List SourceFragment → Strand → List String matching_fragment_ids wanted source fragments strand = unique_occurrence_fragments [] (search_occurrences wanted source fragments strand) @@ -183,7 +180,7 @@ fragment_id_at (S position) (_ :: rest) = fragment_id_at position rest -- position/id pair fails rather than silently returning context around a -- different fragment. public export -context_fragment_ids : Nat → Nat → Occurrence → DocumentStrand → Maybe (List String) +context_fragment_ids : Nat → Nat → Occurrence → Strand → Maybe (List String) context_fragment_ids before after occurrence strand = let position = occurrence_strand_position occurrence in let ids = strand_fragment_ids strand in From b632b3c56cf57877aa34f938cb29d9f156204a5d Mon Sep 17 00:00:00 2001 From: i Date: Fri, 11 Sep 2026 22:42:31 -0400 Subject: [PATCH 5/5] Exercise source-agnostic strands --- src/OccurrenceSmoke.idric | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/OccurrenceSmoke.idric b/src/OccurrenceSmoke.idric index 9bbdc7f9..040daf06 100644 --- a/src/OccurrenceSmoke.idric +++ b/src/OccurrenceSmoke.idric @@ -15,10 +15,9 @@ sample_fragments = [ Fragment "f0004" "fixture:known-reading:sherlock-adventures" 38 49 ] -sample_strand : DocumentStrand -sample_strand = Strand +sample_strand : Strand +sample_strand = MaterializedStrand "document-order:sherlock-adventures" - "fixture:known-reading:sherlock-adventures" ["f0001", "f0002", "f0003", "f0004"] unicode_source : AuthoritativeText @@ -27,8 +26,8 @@ unicode_source = SourceText "fixture:unicode" "東京と京都" unicode_fragments : List SourceFragment unicode_fragments = [Fragment "u0001" "fixture:unicode" 0 5] -unicode_strand : DocumentStrand -unicode_strand = Strand "document-order:unicode" "fixture:unicode" ["u0001"] +unicode_strand : Strand +unicode_strand = MaterializedStrand "document-order:unicode" ["u0001"] occurrence_at_index : Nat → List Occurrence → Maybe Occurrence occurrence_at_index Z [] = Nothing @@ -36,14 +35,14 @@ occurrence_at_index Z (value :: _) = Just value occurrence_at_index (S index) [] = Nothing occurrence_at_index (S index) (_ :: rest) = occurrence_at_index index rest -window_count : Nat → Nat → Maybe Occurrence → DocumentStrand → Nat +window_count : Nat → Nat → Maybe Occurrence → Strand → Nat window_count before after Nothing strand = 0 window_count before after (Just occurrence) strand = case context_fragment_ids before after occurrence strand of Nothing ⇒ 0 Just ids ⇒ length ids -window_available : Nat → Nat → Maybe Occurrence → DocumentStrand → Bool +window_available : Nat → Nat → Maybe Occurrence → Strand → Bool window_available before after Nothing strand = False window_available before after (Just occurrence) strand = case context_fragment_ids before after occurrence strand of @@ -55,9 +54,8 @@ main = do let holmes = search_occurrences "Holmes" sample_source sample_fragments sample_strand let crossing = search_occurrences "one.\nWatson" sample_source sample_fragments sample_strand let unicode = search_occurrences "京都" unicode_source unicode_fragments unicode_strand - let stale = Strand + let stale = MaterializedStrand "document-order:sherlock-adventures:changed" - "fixture:known-reading:sherlock-adventures" ["f0002", "f0001", "f0003", "f0004"] putStrLn ("occurrence-count=" ++ show (length holmes)) putStrLn ("matching-fragment-count=" ++ show (length (matching_fragment_ids "Holmes" sample_source sample_fragments sample_strand)))