1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module SplayList
( SplayList (..)
, pattern Cons, pattern Snoc
, Measured (..)
, split
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Arrow
import Data.Function
import Data.Data
import Data.Maybe
import Data.Monoid
import FreeVars
------------------------------------------------------------------------
data SplayList a
= Nil
| Singleton a
| Append_ !(Measure a) !ChangeFV (SplayList a) (SplayList a)
deriving (Typeable)
deriving instance (Show a, Show (Measure a)) => Show (SplayList a)
toList = go []
where
go i Nil = i
go i (Singleton a) = a: i
go acc (Append l r) = go (go acc r) l
instance (Measured a, Eq a) => Eq (SplayList a) where (==) = (==) `on` toList
instance (Measured a, Ord a) => Ord (SplayList a) where compare = compare `on` toList
--------------------------------------------
class (HasFV a, Measure a ~ Nat) => Measured a where
type Measure a :: *
measure :: a -> Measure a
instance Measured a => Monoid (SplayList a) where
mempty = Nil
Nil `mappend` ys = ys
xs `mappend` Nil = xs
xs `mappend` ys = Append xs ys
instance (Measured a, HasFV a) => HasFV (SplayList a) where
fvLens = \case
Nil -> lConst Nil
Singleton (fvLens -> (s, f)) -> (s, Singleton . f)
Append_ n (fvLens -> (s, f)) l r -> (s, \s -> Append_ n (f s) l r)
instance (Measured a) => Measured (SplayList a) where
type Measure (SplayList a) = Measure a
measure Nil = mempty
measure (Singleton a) = measure a
measure (Append_ n _ _ _) = n
--------------------------------------------
getAppend (Append_ _ s x z) = Just (expand''' (measure z) s x, expand'' s z)
getAppend _ = Nothing
pattern Append :: () => Measured a => SplayList a -> SplayList a -> SplayList a
pattern Append l r <- (getAppend -> Just (l, r))
where Append x@(fvLens -> (ux, _)) z@(fvLens -> (uz, _)) = Append_ us (Same s) x z
where
SFV us s = SFV (measure x) ux <> SFV (measure z) uz
pattern Cons a as <- (viewl -> Just (a, ascendL -> as))
where Cons a as = Singleton a <> as
viewl Nil = Nothing
viewl xs = Just $ go [] xs
where
go xs (Singleton a) = (a, xs)
go xs (Append l r) = go (r: xs) l
ascendL [] = Nil
ascendL (x: xs) = go x xs
where
go !a = \case
[] -> a
b: [] -> a `app` b
b: c: xs -> go (a `app` Append b c) xs
Append a b `app` c = Append a (Append b c)
a `app` b = Append a b
pattern Snoc as a <- (viewr -> Just (a, ascendR -> as))
where Snoc as a = as <> Singleton a
viewr Nil = Nothing
viewr xs = Just $ go [] xs
where
go xs (Singleton a) = (a, xs)
go xs (Append l r) = go (l: xs) r
ascendR [] = Nil
ascendR (x: xs) = go x xs
where
go !c = \case
[] -> c
a: [] -> a `app` c
b: a: xs -> go (Append a b `app` c) xs
a `app` Append b c = Append (Append a b) c
a `app` b = Append a b
-- | Split a list at the point where the predicate on the measure changes from False to True.
split :: Measured a => (Nat -> Bool) -> SplayList a -> (SplayList a, SplayList a)
split _ Nil = (Nil, Nil)
split p xs
| p mempty = (Nil, xs)
| p (measure xs) = go mempty [] [] xs
| otherwise = (xs, Nil)
where
go m ls rs = \case
Append l r
| p n -> go m ls (r: rs) l
| otherwise -> go n (l: ls) rs r
where
n = m <> measure l
xs | p (m <> measure xs) -> (ascendR ls, ascendL $ xs: rs)
| otherwise -> (ascendR $ xs: ls, ascendL rs)
|