0 | module Data.Regex
 1 |
 2 | import public TyRE.StringRE
 3 | import public TyRE.DisjointMatches
 4 | import TyRE.Parser
 5 |
 6 | %default total
 7 |
 8 | export
 9 | parse : TyRE a -> String -> Maybe a
10 | parse tyre str = parseFull tyre (fastUnpack str)
11 |
12 | export
13 | match : TyRE a -> String -> Bool
14 | match tyre str = isJust $ parse (ignore tyre) str
15 |
16 | export
17 | parsePrefix : (tyre : TyRE a) -> String -> (greedy : Bool) -> (Maybe a, String)
18 | parsePrefix tyre cs greedy =
19 |   bimap id fastPack (parsePrefix tyre (fastUnpack cs) greedy)
20 |
21 | export
22 | partial
23 | getToken : (greedy : Bool) -> TyRE a -> Stream Char -> (Maybe a, Stream Char)
24 | getToken greedy tyre stm = getToken tyre stm greedy
25 |
26 | export
27 | partial -- consuming makes this function terminating, however we do not prove this
28 | asDisjointMatches : (tyre : TyRE a) -> {auto 0 consuming : IsConsuming tyre}
29 |                   -> String -> (greedy : Bool) -> DisjointMatches a
30 | asDisjointMatches tyre str greedy
31 |   = asDisjointMatches tyre (fastUnpack str) greedy
32 |
33 | export
34 | partial
35 | substitute : (tyre: TyRE a) -> {auto 0 consuming : IsConsuming tyre}
36 |           -> (a -> String) -> String -> String
37 | substitute tyre f str = toString f (asDisjointMatches tyre str True)