0 | module Text.Matcher
  1 |
  2 | import public Data.Maybe -- reexporting for `IsJust` in `MatchesWhole` and friends
  3 | import Data.SnocList
  4 | import Data.Vect
  5 |
  6 | import Decidable.Decidable
  7 |
  8 | import Syntax.IHateParens.Function
  9 |
 10 | %default total
 11 |
 12 | ---------------------------------------
 13 | --- Data types representing results ---
 14 | ---------------------------------------
 15 |
 16 | public export
 17 | record OneMatchInside a where
 18 |   constructor MkOneMatchInside
 19 |   unmatchedPre  : String
 20 |   matchedStr    : String
 21 |   matchedVal    : a
 22 |   unmatchedPost : String
 23 |
 24 | public export %inline
 25 | forgetVal : OneMatchInside a -> (String, String, String)
 26 | forgetVal $ MkOneMatchInside pre str _ post = (pre, str, post)
 27 |
 28 | public export
 29 | data AllMatchedInside : Type -> Type where
 30 |   Stop  : (post : String) -> AllMatchedInside a
 31 |   Match : (pre : String) -> (matched : String) -> (val : a) -> (cont : AllMatchedInside a) -> AllMatchedInside a
 32 |
 33 | public export
 34 | matchedCnt : AllMatchedInside a -> Nat
 35 | matchedCnt $ Stop {}         = Z
 36 | matchedCnt $ Match {cont, _} = S $ matchedCnt cont
 37 |
 38 | public export
 39 | matchedStrs' : (ms : AllMatchedInside a) -> Vect (matchedCnt ms) String
 40 | matchedStrs' $ Stop _                 = []
 41 | matchedStrs' $ Match _ matched _ cont = matched :: matchedStrs' cont
 42 |
 43 | public export
 44 | matchedVals' : (ms : AllMatchedInside a) -> Vect (matchedCnt ms) a
 45 | matchedVals' $ Stop _             = []
 46 | matchedVals' $ Match _ _ val cont = val :: matchedVals' cont
 47 |
 48 | public export
 49 | matchedStrs : AllMatchedInside a -> List String
 50 | matchedStrs $ Stop _                 = []
 51 | matchedStrs $ Match _ matched _ cont = matched :: matchedStrs cont
 52 |
 53 | public export
 54 | matchedVals : AllMatchedInside a -> List a
 55 | matchedVals $ Stop _             = []
 56 | matchedVals $ Match _ _ val cont = val :: matchedVals cont
 57 |
 58 | -------------------------
 59 | --- Matcher interface ---
 60 | -------------------------
 61 |
 62 | public export
 63 | interface TextMatcher tm where
 64 |   matchWhole'  : (multiline : Bool) -> tm a -> String -> Maybe a
 65 |   -- Invariant that must hold is that `unmatchedPre ++ matchedStr ++ unmatchedPost` must be equal to the original string
 66 |   matchInside' : (multiline : Bool) -> tm a -> String -> Maybe $ OneMatchInside a
 67 |   matchAll'    : (multiline : Bool) -> tm a -> String -> AllMatchedInside a
 68 |
 69 |   matchWhole' multiline m str = matchInside' multiline m str >>= \case
 70 |     MkOneMatchInside "" _ val "" => Just val
 71 |     _                            => Nothing
 72 |   matchAll' multiline m str = do
 73 |     let Just $ MkOneMatchInside pre match val post = matchInside' multiline m str | Nothing => Stop str
 74 |     if length post < length str
 75 |       then Match pre match val $ matchAll' multiline m $ assert_smaller str post
 76 |       else case strUncons str of
 77 |              Nothing => Match pre match val $ Stop post
 78 |              Just (k, str') => case matchAll' multiline m $ assert_smaller str str' of
 79 |                Stop post' => Match pre match val $ Stop $ strCons k post'
 80 |                Match pre' match' val' cont' => Match pre match val $ Match (strCons k pre') match' val' cont'
 81 |
 82 | parameters {default False multiline : Bool} {auto _ : TextMatcher tm} (matcher : tm a)
 83 |
 84 |   parameters (input : String)
 85 |
 86 |     -- The following functions are a workaround of current inability of interfaces to hold functions with `default` arguments.
 87 |     public export %inline matchWhole  : Maybe a                  ; matchWhole  = matchWhole'  multiline matcher input
 88 |     public export %inline matchInside : Maybe $ OneMatchInside a ; matchInside = matchInside' multiline matcher input
 89 |     public export %inline matchAll    : AllMatchedInside a       ; matchAll    = matchAll'    multiline matcher input
 90 |
 91 |     ---------------------------------------------------
 92 |     --- Type-level predicate and functions using it ---
 93 |     ---------------------------------------------------
 94 |
 95 |     public export %inline
 96 |     MatchesWhole, MatchesInside : Type
 97 |     MatchesWhole = IsJust matchWhole
 98 |     MatchesInside = IsJust matchInside
 99 |
100 |     public export %inline
101 |     doesMatchWhole : Dec MatchesWhole
102 |     doesMatchWhole = isItJust _
103 |
104 |     public export %inline
105 |     doesMatchInside : Dec MatchesInside
106 |     doesMatchInside = isItJust _
107 |
108 |     public export %inline
109 |     matchWholeResult : (0 _ : MatchesWhole) => a
110 |     matchWholeResult = fromJust matchWhole
111 |
112 |     public export %inline
113 |     matchInsideResult : (0 _ : MatchesInside) => OneMatchInside a
114 |     matchInsideResult = fromJust matchInside
115 |
116 |   -----------------------------
117 |   --- Replacement functions ---
118 |   -----------------------------
119 |
120 |   export
121 |   replaceOne : (replacement : (match : String) -> (val : a) -> String) ->
122 |                String -> String
123 |   replaceOne replacement str = maybe str rep $ matchInside str where
124 |     %inline rep : OneMatchInside a -> String
125 |     rep $ MkOneMatchInside pre match val post = pre ++ replacement match val ++ post
126 |
127 |   export
128 |   replaceAll : (replacement : (orig : String) -> (val : a) -> String) ->
129 |                String -> String
130 |   replaceAll replacement = concat . rep [<] . matchAll where
131 |     rep : SnocList String -> AllMatchedInside a -> SnocList String
132 |     rep acc $ Stop post                  = acc :< post
133 |     rep acc $ Match pre matched val cont = rep .| acc :< pre :< replacement matched val .| cont
134 |
135 | --- Modifiers for replacement functions ---
136 |
137 | public export %inline
138 | (.str) : (t -> (String -> a -> String) -> String -> String) ->
139 |          (t -> (String -> String)      -> String -> String)
140 | f.str p r = f p $ const . r
141 |
142 | public export %inline
143 | (.val) : (t -> (String -> a -> String) -> String -> String) ->
144 |          (t -> (a -> String)           -> String -> String)
145 | f.val p = f p . const
146 |
147 | public export %inline
148 | (.const) : (t -> (String -> a -> String) -> String -> String) ->
149 |            (t -> String                  -> String -> String)
150 | f.const p = f p . const . const
151 |