0 | module TyRE.DisjointMatches
  1 |
  2 | import Data.SnocList
  3 | import Data.List
  4 |
  5 | infix 6 :+:,.+.
  6 | infix 7 :<,::
  7 |
  8 | ||| A data structure to represent succesful (disjoint) matches in a string.
  9 | ||| A string is written here as alternatating sequence of substring and matches.
 10 | ||| E.g. the string "aaadeebbjk" matched against r "((a*d)|(bb))!" is represented as
 11 | ||| Snoc (Snoc (Prefix []) (Just 3) ['e', 'e']) Nothing ['j','k']
 12 | ||| Similar: DisjointMatches
 13 | public export
 14 | data DisjointMatchesSnoc : Type -> Type where
 15 |   Prefix : SnocList Char -> DisjointMatchesSnoc a
 16 |   Snoc   : DisjointMatchesSnoc a -> a -> SnocList Char -> DisjointMatchesSnoc a
 17 |
 18 | export
 19 | (:<) : DisjointMatchesSnoc a -> Char -> DisjointMatchesSnoc a
 20 | (:<) (Prefix cs) c            = Prefix (cs :< c)
 21 | (:<) (Snoc dm parseTree cs) c = Snoc dm parseTree (cs :< c)
 22 |
 23 | export
 24 | (:+:) : DisjointMatchesSnoc a -> a -> DisjointMatchesSnoc a
 25 | (:+:) dm parseTree = Snoc dm parseTree [<]
 26 |
 27 | ||| A data structure to represent succesful (disjoint) matches in a string.
 28 | ||| A string is written here as alternatating sequence of substring and matches.
 29 | ||| E.g. the string "aaadeebbjk" matched against r "((a*d)|(bb))!" is represented as
 30 | ||| Cons [] (Just 3) (Cons ['e', 'e'] Nothing (Suffix ['j','k']))
 31 | ||| Similar: DisjointMatchesSnoc
 32 | public export
 33 | data DisjointMatches : Type -> Type where
 34 |   Suffix : List Char -> DisjointMatches a
 35 |   Cons : List Char -> a -> DisjointMatches a -> DisjointMatches a
 36 |
 37 | export
 38 | (::) : DisjointMatches a -> Char -> DisjointMatches a
 39 | (::) (Suffix cs) c = Suffix (c :: cs)
 40 | (::) (Cons cs parse tail) c = Cons (c :: cs) parse tail
 41 |
 42 | export
 43 | (.+.) : a -> DisjointMatches a -> DisjointMatches a
 44 | (.+.) parse dm = Cons [] parse dm
 45 |
 46 | export
 47 | (<>>) : DisjointMatchesSnoc a -> DisjointMatches a -> DisjointMatches a
 48 | (<>>) (Prefix sc)      (Suffix cs)    = Suffix (sc <>> cs)
 49 | (<>>) (Prefix sc)      (Cons cs p tl) = Cons (sc <>> cs) p tl
 50 | (<>>) (Snoc nck p sc)  (Suffix cs)    = nck <>> Cons [] p (Suffix (sc <>> cs))
 51 | (<>>) (Snoc nck p sc)  (Cons cs q tl) = nck <>> Cons [] p (Cons (sc <>> cs) q tl)
 52 |
 53 | export
 54 | (<><) : DisjointMatchesSnoc a  -> DisjointMatches a -> DisjointMatchesSnoc a
 55 | (<><) (Prefix sc)     (Suffix cs)    = Prefix (sc <>< cs)
 56 | (<><) (Snoc nck p sc) (Suffix cs)    = Snoc nck p (sc <>< cs)
 57 | (<><) (Prefix sc)     (Cons cs p tl) = Snoc (Prefix (sc <>< cs)) p [<] <>< tl
 58 | (<><) (Snoc nck p sc) (Cons cs q tl) = Snoc (Snoc nck p (sc <>< cs)) q [<] <>< tl
 59 |
 60 | public export
 61 | Cast (DisjointMatchesSnoc a) (DisjointMatches a) where
 62 |   cast sx = sx <>> (Suffix [])
 63 |
 64 | public export
 65 | Cast (DisjointMatches a) (DisjointMatchesSnoc a) where
 66 |   cast xs = (Prefix [<]) <>< xs
 67 |
 68 | public export
 69 | Functor DisjointMatches where
 70 |   map f (Suffix cs) = Suffix cs
 71 |   map f (Cons cs parse tail) = Cons cs (f parse) (map f tail)
 72 |
 73 | public export
 74 | Functor DisjointMatchesSnoc where
 75 |   map f (Prefix sc) = Prefix sc
 76 |   map f (Snoc neck parse sc) = Snoc (map f neck) (f parse) sc
 77 |
 78 | export
 79 | toString : (a -> String) -> DisjointMatches a -> String
 80 | toString f (Suffix cs) = fastPack cs
 81 | toString f (Cons cs parse tail) = (fastPack cs) ++ (f parse) ++ (toString f tail)
 82 |
 83 | export
 84 | toStringSnoc : (a -> String) -> DisjointMatchesSnoc a -> String
 85 | toStringSnoc f (Prefix sc) = fastPack (cast sc)
 86 | toStringSnoc f (Snoc neck parse sc) = (toStringSnoc f neck) ++ (f parse) ++ fastPack (cast sc)
 87 |
 88 | export
 89 | Show a => Show (DisjointMatches a) where
 90 |   show (Suffix cs) = fastPack cs
 91 |   show (Cons cs pt tail) = fastPack cs ++ "~~" ++ show pt ++ "~~" ++ show tail
 92 |
 93 | export
 94 | Show a => Show (DisjointMatchesSnoc a) where
 95 |   show (Prefix cs) = fastPack $ toList cs
 96 |   show (Snoc neck pt cs) = show neck ++ "~~" ++ show pt ++ "~~" ++ fastPack (toList cs)
 97 |
 98 | export
 99 | length : DisjointMatches a -> Nat
100 | length (Suffix _)       = Z
101 | length (Cons _ _ tail)  = S (length tail)
102 |