0 | module Data.Refined.String
 1 |
 2 | import public Data.Refined.Char
 3 | import public Data.Refined.List
 4 | import public Data.Refined.Core
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | 0 Len : (p : Integer -> Type) -> String -> Type
10 | Len p = p `On` cast . prim__strLength
11 |
12 | public export
13 | 0 Str : (p : List Char -> Type) -> String -> Type
14 | Str p = p `On` unpack
15 |
16 | ||| Proof that a (non-empty) list of characters does not start with
17 | ||| a whitespace character.
18 | public export
19 | data LeftTrimmed : List Char -> Type where
20 |   LTCons :
21 |        {0 cs : _}
22 |     -> {0 c : _}
23 |     -> Holds (Prelude.not . Prelude.isControl) c
24 |     -> LeftTrimmed (c :: cs)
25 |
26 | public export
27 | HDec0 (List Char) LeftTrimmed where
28 |   hdec0 (c::_)  = map LTCons $ hdec0 c
29 |   hdec0 []      = Nothing0
30 |
31 | public export
32 | HDec (List Char) LeftTrimmed where
33 |   hdec (c::_)  = map LTCons $ hdec c
34 |   hdec []      = Nothing
35 |
36 | ||| Proof that a list of characters does not start with a whitespace character.
37 | public export
38 | data RightTrimmed : List Char -> Type where
39 |   RT1 :
40 |        {0 c : _}
41 |     -> Holds (Prelude.not . Prelude.isControl) c
42 |     -> RightTrimmed [c]
43 |   RTCons :
44 |        {0 cs : _}
45 |     -> {0 c : _}
46 |     -> RightTrimmed cs
47 |     -> RightTrimmed (c :: cs)
48 |
49 | public export
50 | HDec0 (List Char) RightTrimmed where
51 |   hdec0 [c]     = map RT1 $ hdec0 c
52 |   hdec0 (c::cs) = map RTCons $ hdec0 cs
53 |   hdec0 []      = Nothing0
54 |
55 | public export
56 | HDec (List Char) RightTrimmed where
57 |   hdec [c]     = map RT1 $ hdec c
58 |   hdec (c::cs) = map RTCons $ hdec cs
59 |   hdec []      = Nothing
60 |
61 | public export
62 | 0 Trimmed : List Char -> Type
63 | Trimmed = LeftTrimmed && RightTrimmed
64 |