0 | module Libraries.Data.DList
 1 |
 2 | %default total
 3 |
 4 | export
 5 | record DList (a : Type) where
 6 |   constructor MkDList
 7 |   runDList : List a -> List a
 8 |
 9 | export %inline
10 | Nil : DList a
11 | Nil = MkDList id
12 |
13 | export %inline
14 | singleton : a -> DList a
15 | singleton a = MkDList (a ::)
16 |
17 | export %inline
18 | (::) : a -> DList a -> DList a
19 | (::) a as = MkDList ((a ::) . runDList as)
20 |
21 | export %inline
22 | snoc : DList a -> a -> DList a
23 | snoc as a = MkDList (runDList as . (a ::))
24 |
25 | export %inline
26 | appendR : DList a -> List a -> DList a
27 | appendR as bs = MkDList (runDList as . (bs ++))
28 |
29 | export %inline
30 | appendL : List a -> DList a -> DList a
31 | appendL as bs = MkDList ((as ++) . runDList bs)
32 |
33 | export %inline
34 | (++) : DList a -> DList a -> DList a
35 | as ++ bs = MkDList (runDList as . runDList bs)
36 |
37 | export %inline
38 | reify : DList a -> List a
39 | reify as = runDList as []
40 |
41 | -- NB: No Functor instance because it's too expensive to reify, map, put back
42 | -- Consider using a different data structure if you need mapping (e.g. a rope)
43 |
44 | export %inline
45 | Semigroup (DList a) where
46 |   xs <+> ys = xs ++ ys
47 |
48 | export %inline
49 | Monoid (DList a) where
50 |   neutral = []
51 |
52 | export %inline
53 | FromString (DList String) where
54 |   fromString = singleton
55 |