0 | module Data.String.Iterator
 1 |
 2 | import Control.Monad.Identity
 3 | import public Data.List.Lazy
 4 |
 5 | %default total
 6 |
 7 | -- Backend-dependent string iteration type,
 8 | -- parameterised by the string that it iterates over.
 9 | --
10 | -- Beware: the index is checked only up to definitional equality.
11 | -- In theory, you could run `decEq` on two strings
12 | -- with the same content but allocated in different memory locations
13 | -- and use the obtained Refl to coerce iterators between them.
14 | --
15 | -- The strictly correct solution is to make the iterators independent
16 | -- from the exact memory location of the string given to `uncons`.
17 | -- (For example, byte offsets satisfy this requirement.)
18 | export
19 | data StringIterator : String -> Type where [external]
20 |
21 | -- This function is private
22 | -- to avoid subverting the linearity guarantees of withString.
23 | %foreign
24 |   "scheme:blodwen-string-iterator-new"
25 |   "RefC:stringIteratorNew"
26 |   "javascript:stringIterator:new"
27 | private
28 | fromString : (str : String) -> StringIterator str
29 |
30 | -- This function uses a linear string iterator
31 | -- so that backends can use mutating iterators.
32 | export
33 | withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
34 | withString str f = f (fromString str)
35 |
36 | ||| Runs the action `f` on the slice `res` of the original string `str` represented by the
37 | ||| iterator `it`
38 | %foreign
39 |   "scheme:blodwen-string-iterator-to-string"
40 |   "RefC:stringIteratorToString"
41 |   "javascript:stringIterator:toString"
42 | export
43 | withIteratorString : (str : String)
44 |                   -> (1 it : StringIterator str)
45 |                   -> (f : (res : String) -> a)
46 |                   -> a
47 |
48 | -- We use a custom data type instead of Maybe (Char, StringIterator)
49 | -- to remove one level of pointer indirection
50 | -- in every iteration of something that's likely to be a hot loop,
51 | -- and to avoid one allocation per character.
52 | --
53 | -- The Char field of Character is unrestricted for flexibility.
54 | public export
55 | data UnconsResult : String -> Type where
56 |   EOF : UnconsResult str
57 |   Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str
58 |
59 | -- We pass the whole string to the uncons function
60 | -- to avoid yet another allocation per character
61 | -- because for many backends, StringIterator can be simply an integer
62 | -- (e.g. byte offset into an UTF-8 string).
63 | %foreign
64 |   "scheme:blodwen-string-iterator-next"
65 |   "RefC:stringIteratorNext"
66 |   "javascript:stringIterator:next"
67 | export
68 | uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
69 |
70 | export
71 | foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
72 | foldl op acc str = withString str (loop acc)
73 |   where
74 |     loop : accTy -> (1 it : StringIterator str) -> accTy
75 |     loop acc it =
76 |       case uncons str it of
77 |         EOF => acc
78 |         Character c it' => loop (acc `op` c) (assert_smaller it it')
79 |
80 | export
81 | unpack : String -> LazyList Char
82 | unpack str = runIdentity $ withString str unpack'
83 |   where
84 |     -- This is a Functor instance of Identity, but linear in second argument
85 |     %inline
86 |     mapId : forall a, b. (a -> b) -> (1 x : Identity a) -> Identity b
87 |     mapId f (Id x) = Id (f x)
88 |
89 |     unpack' : (1 it : StringIterator str) -> Identity (Lazy (LazyList Char))
90 |     unpack' it =
91 |       case uncons str it of
92 |         EOF => pure []
93 |         Character c it' => mapId (c ::) (unpack' $ assert_smaller it it')
94 |