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