module Data.List.Tagged (
TaggedList(..),
UntaggedList(..),
TL(..),
ATL(..),
append,
eqLists,
extractRightsOrLefts,
fromList,
fromListAsUntagged,
head,
join,
length,
map,
mapM_,
replace,
tail,
toList,
withTL,
zipf,
TupleOf(..),
TupleConvertable(..),
) where
import Prelude
(Bool(..)
,Either(..)
,Eq(..)
,Functor
,Monad(..)
,const
,error
,fmap
,id
,otherwise
,snd
,undefined
,($)
,(.)
,(&&)
)
import Control.Applicative (Applicative,liftA2,pure)
import Control.Monad.Trans.Abort (Abort,abort,runAbort)
import Data.Binary (Binary,get,put)
import Data.Foldable (Foldable,foldMap)
import Data.Monoid (Monoid,mappend,mempty)
import Data.Traversable (Traversable,traverse)
import Data.Typeable (Typeable)
import TypeLevel.NaturalNumber
(N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15
,Zero
,SuccessorTo
)
import TypeLevel.NaturalNumber.Induction (Induction(deduction2M),induction,deduction,transform)
import TypeLevel.NaturalNumber.Operations (Plus)
import Data.NaturalNumber (NaturalNumber,N,asN)
newtype TL α n = TL { unwrapTL :: TaggedList n α }
newtype ATL t α n = ATL { unwrapATL :: t (TaggedList n α) }
data TaggedList n α where
E :: TaggedList Zero α
(:.) :: α → TaggedList n α → TaggedList (SuccessorTo n) α
deriving Typeable
infixr :.
data UntaggedList α = ∀ n. UntaggedList (TaggedList n α) deriving Typeable
instance (Induction n, Binary α) ⇒ Binary (TaggedList n α) where
get = fmap fromList get
put = put . toList
instance Binary α ⇒ Binary (UntaggedList α) where
get = fmap fromListAsUntagged get
put (UntaggedList l) = put (toList l)
instance (Induction n, Eq α) ⇒ Eq (TaggedList n α) where
x == y = runAbort (deduction2M () (\_ _ _ → return True) step (TL x) (TL y))
where
step :: Eq α ⇒ TL α (SuccessorTo n) → TL α (SuccessorTo n) → () → Abort Bool (TL α n,TL α n,())
step (TL (x :. xs)) (TL (y :. ys)) b
| x /= y = abort False
| otherwise = return (TL xs,TL ys,())
instance Induction n ⇒ Foldable (TaggedList n) where
foldMap f l = deduction mempty (const id) (step f) (TL l)
where
step :: Monoid m ⇒ (α → m) → TL α (SuccessorTo n) → m → (TL α n,m)
step f (TL (x :. xs)) a = (TL xs,a `mappend` f x)
instance Induction n ⇒ Functor (TaggedList n) where
fmap f = withTL (transform (const (TL E)) (step f))
where
step :: ∀ α β n. (α → β) → (TL α n → TL β n) → TL α (SuccessorTo n) → TL β (SuccessorTo n)
step f recurse (TL (x :. xs)) = TL (f x :. withTL recurse xs)
instance Induction n ⇒ Traversable (TaggedList n) where
traverse f = unwrapATL . transform (const . ATL . pure $ E) (step f) . TL
where
step :: ∀ α β t n. Applicative t ⇒ (α → t β) → (TL α n → ATL t β n) → TL α (SuccessorTo n) → ATL t β (SuccessorTo n)
step f recurse (TL (x :. xs)) = ATL (liftA2 (:.) (f x) (unwrapATL . recurse . TL $ xs))
append :: TaggedList m α → TaggedList n α → TaggedList (Plus m n) α
append E = id
append (x :. xs) = (x :.) . append xs
eqLists :: Eq α ⇒ TaggedList m α → TaggedList n α → Bool
eqLists E E = True
eqLists E _ = False
eqLists _ E = False
eqLists (x:.xs) (y:.ys) = (x == y) && eqLists xs ys
extractRightsOrLefts :: TaggedList n (Either α β) → Either [α] (TaggedList n β)
extractRightsOrLefts E = Right E
extractRightsOrLefts (Left x :. rest) =
case extractRightsOrLefts rest of
Left xs → Left (x:xs)
Right _ → Left [x]
extractRightsOrLefts (Right x :. rest) =
case extractRightsOrLefts rest of
Left es → Left es
Right xs → Right (x:.xs)
fromList :: Induction n ⇒ [α] → TaggedList n α
fromList = unwrapTL . snd . induction z i
where
z [] = (undefined,TL E)
z _ = error "List is too long to convert into a tagged list of the given length."
i (x:xs) (TL l) = (xs,TL (x :. l))
i [] _ = error "List is too short to convert into a tagged list of the given length."
fromListAsUntagged :: [α] → UntaggedList α
fromListAsUntagged [] = UntaggedList E
fromListAsUntagged (x:rest) =
case fromListAsUntagged rest of
UntaggedList xs → UntaggedList (x :. xs)
head :: TaggedList (SuccessorTo n) α → α
head (x :. _) = x
join :: TaggedList m α → TaggedList n α → (TaggedList (Plus m n) α,TaggedList (Plus m n) β → (TaggedList m β,TaggedList n β))
join E v = (v,\z → (E,z))
join (x :. xs) v =
let (vv,split) = join xs v
in (x :. vv
,(\(y :. ys) → let (a,b) = split ys in (y :. a,b))
)
length :: NaturalNumber n ⇒ TaggedList n α → N n
length _ = asN
map :: (α → β) → TaggedList n α → TaggedList n β
map f E = E
map f (x :. xs) = f x :. map f xs
mapM_ :: Monad m ⇒ (α → m β) → TaggedList n α → m ()
mapM_ f E = return ()
mapM_ f (x :. xs) = f x >> mapM_ f xs
replace :: [α] → TaggedList n β → TaggedList n α
replace [] E = E
replace [] _ = error "There are not enough elements in the list to replace all elements of the tagged list."
replace (x:xs) (_:.ys) = x :. replace xs ys
replace (x:xs) E = error "There are too many elements in the list to replace all elements of the tagged list."
tail :: TaggedList (SuccessorTo n) α → TaggedList n α
tail (_ :. xs) = xs
toList :: TaggedList n α → [α]
toList E = []
toList (x :. xs) = x : toList xs
withTL :: (TL α n → TL β n) → TaggedList n α → TaggedList n β
withTL f = unwrapTL . f . TL
zipf :: TaggedList n (α → β) → TaggedList n α → TaggedList n β
zipf E E = E
zipf (f :. fs) (x :. xs) = f x :. zipf fs xs
type family TupleOf n α
type instance TupleOf N0 α = ()
type instance TupleOf N1 α = (α)
type instance TupleOf N2 α = (α,α)
type instance TupleOf N3 α = (α,α,α)
type instance TupleOf N4 α = (α,α,α,α)
type instance TupleOf N5 α = (α,α,α,α,α)
type instance TupleOf N6 α = (α,α,α,α,α,α)
type instance TupleOf N7 α = (α,α,α,α,α,α,α)
type instance TupleOf N8 α = (α,α,α,α,α,α,α,α)
type instance TupleOf N9 α = (α,α,α,α,α,α,α,α,α)
type instance TupleOf N10 α = (α,α,α,α,α,α,α,α,α,α)
type instance TupleOf N11 α = (α,α,α,α,α,α,α,α,α,α,α)
type instance TupleOf N12 α = (α,α,α,α,α,α,α,α,α,α,α,α)
type instance TupleOf N13 α = (α,α,α,α,α,α,α,α,α,α,α,α,α)
type instance TupleOf N14 α = (α,α,α,α,α,α,α,α,α,α,α,α,α,α)
type instance TupleOf N15 α = (α,α,α,α,α,α,α,α,α,α,α,α,α,α,α)
class TupleConvertable n where
fromTuple :: TupleOf n α → TaggedList n α
toTuple :: TaggedList n α → TupleOf n α
instance TupleConvertable N0 where
fromTuple _ = E
toTuple _ = ()
instance TupleConvertable N1 where
fromTuple (x1) = x1:.E
toTuple (x1:.E) = (x1)
instance TupleConvertable N2 where
fromTuple (x1,x2) = x1:.x2:.E
toTuple (x1:.x2:.E) = (x1,x2)
instance TupleConvertable N3 where
fromTuple (x1,x2,x3) = x1:.x2:.x3:.E
toTuple (x1:.x2:.x3:.E) = (x1,x2,x3)
instance TupleConvertable N4 where
fromTuple (x1,x2,x3,x4) = x1:.x2:.x3:.x4:.E
toTuple (x1:.x2:.x3:.x4:.E) = (x1,x2,x3,x4)
instance TupleConvertable N5 where
fromTuple (x1,x2,x3,x4,x5) = x1:.x2:.x3:.x4:.x5:.E
toTuple (x1:.x2:.x3:.x4:.x5:.E) = (x1,x2,x3,x4,x5)
instance TupleConvertable N6 where
fromTuple (x1,x2,x3,x4,x5,x6) = x1:.x2:.x3:.x4:.x5:.x6:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.E) = (x1,x2,x3,x4,x5,x6)
instance TupleConvertable N7 where
fromTuple (x1,x2,x3,x4,x5,x6,x7) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.E) = (x1,x2,x3,x4,x5,x6,x7)
instance TupleConvertable N8 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.E) = (x1,x2,x3,x4,x5,x6,x7,x8)
instance TupleConvertable N9 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9)
instance TupleConvertable N10 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
instance TupleConvertable N11 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
instance TupleConvertable N12 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
instance TupleConvertable N13 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
instance TupleConvertable N14 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.x14:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.x14:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
instance TupleConvertable N15 where
fromTuple (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) = x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.x14:.x15:.E
toTuple (x1:.x2:.x3:.x4:.x5:.x6:.x7:.x8:.x9:.x10:.x11:.x12:.x13:.x14:.x15:.E) = (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)