0 | ||| Utilities for the DFA string searching algorithm.
  1 | module Data.ByteString.Search.DFA.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.ByteString.Search.KnuthMorrisPratt.Internal
  8 | import Data.DArray
  9 | import Data.Enum
 10 | import Data.Linear.Ref1
 11 |
 12 | %hide Data.Buffer.Core.get
 13 | %hide Data.Buffer.Core.set
 14 | %hide Data.List.Elem.get
 15 |
 16 | %default total
 17 |
 18 | ||| Builds a deterministic finite automaton (DFA) for pattern matching over a
 19 | ||| `ByteString`.
 20 | |||
 21 | ||| The automaton encodes transitions from `(state, input byte)` to the next
 22 | ||| DFA state.
 23 | |||
 24 | ||| Unlike the previous implementation, transition-table positions and
 25 | ||| transition values are represented by bounded `Index` values. Bounds are
 26 | ||| established while constructing the automaton and are erased at runtime.
 27 | |||
 28 | ||| The resulting search-time transition path therefore requires no
 29 | ||| `tryNatToFin`, `tryIndex`, or other dynamic DFA-table bounds conversion.
 30 | |||
 31 | export
 32 | automaton :  (bs : ByteString)
 33 |           -> F1 s (Maybe (DFAutomaton s))
 34 | automaton bs t =
 35 |    let bord                          # t := kmpBorders bs t
 36 |        Just (MkKMPBorders stspace bord') := bord
 37 |          | Nothing =>
 38 |              Nothing # t
 39 |        arr                           # t := newDFATable {states = stspace.states} {statesPrf = stspace.statesBounded} t
 40 |        result                        # t := go stspace Z arr bord' t
 41 |        Just result'                      := result
 42 |          | Nothing =>
 43 |              Nothing # t
 44 |      in Just (MkDFAutomaton stspace result') # t
 45 |   where
 46 |     fillState :  (space : DFAStateSpace)
 47 |               -> (state : DFAState space.states)
 48 |               -> (byte : Bits8)
 49 |               -> (patbyte : Maybe Bits8)
 50 |               -> (bordcur : DFAState space.states)
 51 |               -> (arr : DFATable s space.states)
 52 |               -> F1 s (Maybe (DFATable s space.states))
 53 |     fillState space state byte patbyte bordcur arr t =
 54 |       let stateval      := dfaStateValue state
 55 |           Just patbyte' := patbyte
 56 |             | Nothing =>
 57 |                 let False        := stateval == 0
 58 |                       | True =>
 59 |                           let zero   := zeroDFAState space
 60 |                               () # t := setDFATransition {statesPrf = space.statesBounded} arr state byte zero t
 61 |                               True   := byte == 0
 62 |                                 | False =>
 63 |                                     assert_total (fillState space state (byte - 1) patbyte bordcur arr t)
 64 |                             in Just arr # t
 65 |                     bordcur' # t := dfaTransition {statesPrf = space.statesBounded} arr bordcur byte t
 66 |                     ()       # t := setDFATransition {statesPrf = space.statesBounded} arr state byte bordcur' t
 67 |                     True         := byte == 0
 68 |                       | False =>
 69 |                           assert_total (fillState space state (byte - 1) patbyte bordcur' arr t)
 70 |                   in Just arr # t
 71 |           False         := byte == patbyte'
 72 |             | True =>
 73 |                 let Just next := toDFAState space (S $ cast stateval)
 74 |                       | Nothing =>
 75 |                           Nothing # t
 76 |                     ()    # t := setDFATransition {statesPrf = space.statesBounded} arr state byte next t
 77 |                     True      := byte == 0
 78 |                       | False =>
 79 |                           assert_total (fillState space state (byte - 1) patbyte bordcur arr t)
 80 |                   in Just arr # t
 81 |           False         := stateval == 0
 82 |             | True =>
 83 |                 let zero   := zeroDFAState space
 84 |                     () # t := setDFATransition {statesPrf = space.statesBounded} arr state byte zero t
 85 |                     True   := byte == 0
 86 |                       | False =>
 87 |                           assert_total (fillState space state (byte - 1) patbyte bordcur arr t)
 88 |                   in Just arr # t
 89 |           bordcur'  # t := dfaTransition {statesPrf = space.statesBounded} arr bordcur byte t
 90 |           ()        # t := setDFATransition {statesPrf = space.statesBounded} arr state byte bordcur' t
 91 |           True          := byte == 0
 92 |             | False =>
 93 |                 assert_total (fillState space state (byte - 1) patbyte bordcur' arr t)
 94 |         in Just arr # t
 95 |     ||| Construct the transition rows for each DFA state.
 96 |     |||
 97 |     ||| The KMP border table and DFA transition table share the same bounded
 98 |     ||| state space, so border values can be consumed directly as DFA states
 99 |     ||| without any intermediate `Nat` or `Fin` conversion.
100 |     |||
101 |     go :  (stspace : DFAStateSpace)
102 |        -> (state : Nat)
103 |        -> (arr : DFATable s stspace.states)
104 |        -> (bord : KMPBorderTable s stspace.states)
105 |        -> F1 s (Maybe (DFATable s stspace.states))
106 |     go stspace state arr bord t =
107 |       let False          := state > length bs
108 |             | True =>
109 |                 Just arr # t
110 |           Just state' := toDFAState stspace state
111 |             | Nothing =>
112 |                 Nothing # t
113 |           bordcur # t := kmpBorder bord state' t
114 |           patbyte        := index state bs
115 |           arr'       # t := fillState stspace state' 255 patbyte bordcur arr t
116 |           Just arr''     := arr'
117 |             | Nothing =>
118 |                 Nothing # t
119 |        in assert_total (go stspace (S state) arr'' bord t)
120 |