0 | ||| Utilities for the Knuth-Morris-Pratt string searching algorithm.
  1 | module Data.ByteString.Search.KnuthMorrisPratt.Internal
  2 |
  3 | import Data.Array.Core
  4 | import Data.Bits
  5 | import Data.ByteString
  6 | import Data.ByteString.Search.DFA.Types
  7 | import Data.DArray
  8 | import Data.Enum
  9 | import Data.Linear.Ref1
 10 |
 11 | %hide Data.Buffer.Core.get
 12 | %hide Data.Buffer.Core.set
 13 | %hide Data.ByteString.Search.DFA.Types.DFAStateSpace.states
 14 | %hide Data.List.Elem.get
 15 |
 16 | %default total
 17 |
 18 | ||| Mutable storage for the KMP border table.
 19 | |||
 20 | ||| The table contains one entry for every DFA state. Both table indices and
 21 | ||| stored border values are represented by `DFAState`, so their bounds are
 22 | ||| established once and carried as erased evidence.
 23 | |||
 24 | ||| The underlying storage is an Idris primitive array.
 25 | |||
 26 | public export
 27 | record KMPBorderTable (s : Type) (states : Bits32) where
 28 |   constructor MkKMPBorderTable
 29 |   arr : AnyPtr
 30 |
 31 | ||| A constructed KMP border table together with the DFA state space to
 32 | ||| which its indices and values belong.
 33 | |||
 34 | ||| Packaging the state space with the table allows `automaton` to reuse the
 35 | ||| exact same state-space witness rather than independently reconstructing
 36 | ||| and validating the pattern's state count.
 37 | |||
 38 | public export
 39 | record KMPBorders (s : Type) where
 40 |   constructor MkKMPBorders
 41 |   space : DFAStateSpace
 42 |   table : KMPBorderTable s space.states
 43 |
 44 | ||| Allocate an uninitialized KMP border table.
 45 | |||
 46 | ||| The table contains exactly one entry for each DFA state.
 47 | |||
 48 | export
 49 | newKMPBorderTable :  {states : Bits32}
 50 |                   -> F1 s (KMPBorderTable s states)
 51 | newKMPBorderTable {states} t =
 52 |   let arr # t := ffi (prim__emptyArray $ cast states) t
 53 |     in MkKMPBorderTable arr # t
 54 |
 55 | ||| Read a border value from the KMP border table.
 56 | |||
 57 | ||| The supplied index is already a valid `DFAState`, so no dynamic bounds
 58 | ||| validation is required. The stored result is itself another valid DFA
 59 | ||| state.
 60 | |||
 61 | export %inline
 62 | kmpBorder :  KMPBorderTable s states
 63 |           -> DFAState states
 64 |           -> F1 s (DFAState states)
 65 | kmpBorder table state t =
 66 |   let I idx := state
 67 |    in believe_me (prim__arrayGet table.arr (cast idx)) # t
 68 |
 69 | ||| Write a border value to the KMP border table.
 70 | |||
 71 | ||| Both the destination index and stored border value are already bounded by
 72 | ||| the same DFA state space, so no `Fin` conversion or runtime bounds check
 73 | ||| is required.
 74 | |||
 75 | export %inline
 76 | setKMPBorder :  KMPBorderTable s states
 77 |              -> DFAState states
 78 |              -> DFAState states
 79 |              -> F1' s
 80 | setKMPBorder table state border t =
 81 |   let I idx := state
 82 |    in ffi (prim__arraySet table.arr (cast idx) (believe_me border)) t
 83 |
 84 | ||| Construct the successor of a DFA state during DFA preprocessing.
 85 | |||
 86 | ||| This check occurs only while constructing preprocessing tables. It is
 87 | ||| never executed by the target-scanning DFA hot path.
 88 | |||
 89 | export %inline
 90 | nextDFAState :  (space : DFAStateSpace)
 91 |              -> DFAState space.states
 92 |              -> Maybe (DFAState space.states)
 93 | nextDFAState space state =
 94 |   tryIndex {r = space.states} (dfaStateValue state + 1)
 95 |
 96 | ||| Computes the suffix-oriented KMP border table for a given pattern.
 97 | |||
 98 | ||| Each entry associated with DFA state `i` stores the length of the longest
 99 | ||| proper prefix of `pattern[0..i-1]` that is also a suffix.
100 | |||
101 | ||| Unlike the previous implementation, table indices and border values are
102 | ||| represented directly by bounded `DFAState` values rather than `Nat`
103 | ||| values indexed through `Fin`.
104 | |||
105 | ||| Consequently, accesses to the border table require no `tryNatToFin` or
106 | ||| equivalent dynamic table-bounds conversion.
107 | |||
108 | ||| The result packages the table together with its `DFAStateSpace`, allowing
109 | ||| construction of the DFA transition table to reuse exactly the same state
110 | ||| space.
111 | |||
112 | ||| Example: "ANPANMAN"
113 | |||
114 | ||| Indices:  0  1  2  3  4  5  6  7  8
115 | ||| Borders:  0  0  0  0  1  2  0  1  2
116 | |||
117 | export
118 | kmpBorders :  (bs : ByteString)
119 |            -> F1 s (Maybe (KMPBorders s))
120 | kmpBorders bs t =
121 |   let Just stspace := dfaStateSpace bs
122 |         | Nothing =>
123 |             Nothing # t
124 |       arr # t      := newKMPBorderTable {states = stspace.states} t
125 |       zero         : DFAState stspace.states
126 |       zero         := I 0 {prf = stspace.statesPositive}
127 |       ()       # t := setKMPBorder arr zero zero t
128 |       Just one     := nextDFAState stspace zero
129 |         | Nothing =>
130 |             Nothing # t
131 |     in go stspace one zero arr t
132 |   where
133 |     mutual
134 |       ||| Continue resolving the border for the current pattern position.
135 |       |||
136 |       ||| On a matching pattern byte, both the current pattern position and
137 |       ||| border position advance by one. On a mismatch, the previous border
138 |       ||| value is read directly from the bounded KMP border table.
139 |       |||
140 |       advance :  (stspace : DFAStateSpace)
141 |               -> (i : DFAState stspace.states)
142 |               -> (j : DFAState stspace.states)
143 |               -> (wi : Bits8)
144 |               -> (arr : KMPBorderTable s stspace.states)
145 |               -> F1 s (Maybe (KMPBorders s))
146 |       advance stspace i j wi arr t =
147 |         let jidx    := cast {to=Nat} (dfaStateValue j)
148 |             Just wj := index jidx bs
149 |               | Nothing =>
150 |                   Nothing # t
151 |             False   := wi == wj
152 |               | True =>
153 |                   let Just i' := nextDFAState stspace i
154 |                         | Nothing =>
155 |                             Nothing # t
156 |                       Just j' := nextDFAState stspace j
157 |                         | Nothing =>
158 |                             Nothing # t
159 |                       () # t := setKMPBorder arr i' j' t
160 |                     in assert_total (go stspace i' j' arr t)
161 |             False   := dfaStateValue j == 0
162 |               | True =>
163 |                   let Just i' := nextDFAState stspace i
164 |                         | Nothing =>
165 |                             Nothing # t
166 |                       zero    : DFAState stspace.states
167 |                       zero    := I 0 {prf = stspace.statesPositive}
168 |                       ()  # t := setKMPBorder arr i' zero t
169 |                     in assert_total (go stspace i' zero arr t)
170 |             j'  # t := kmpBorder arr j t
171 |           in assert_total (advance stspace i j' wi arr t)
172 |       ||| Process the next pattern position while constructing the KMP border
173 |       ||| table.
174 |       |||
175 |       ||| `i` and `j` are already valid DFA states, so border-table indexing
176 |       ||| requires no dynamic conversion to `Fin`.
177 |       |||
178 |       go :  (stspace : DFAStateSpace)
179 |          -> (i : DFAState stspace.states)
180 |          -> (j : DFAState stspace.states)
181 |          -> (arr : KMPBorderTable s stspace.states)
182 |          -> F1 s (Maybe (KMPBorders s))
183 |       go stspace i j arr t =
184 |         let iidx    := cast {to=Nat} (dfaStateValue i)
185 |             False   := iidx == length bs
186 |               | True =>
187 |                   Just (MkKMPBorders stspace arr) # t
188 |             Just wi := index iidx bs
189 |               | Nothing =>
190 |                   Nothing # t
191 |          in assert_total (advance stspace i j wi arr t)
192 |