module Longboi where
import qualified Prelude
import Prelude (Bool(..))
data Nat = Z | S Nat
deriving (Prelude.Eq, Prelude.Show)
infixl 6 +,
infixl 7 *
type family (n :: Nat) + (m :: Nat) :: Nat where
Z + m = m
(S n) + m = S (n + m)
type family (n :: Nat) * (m :: Nat) :: Nat where
Z * m = Z
(S n) * m = (n * m) + m
type family (n :: Nat) (m :: Nat) :: Nat where
Z m = Z
(S n) Z = S n
(S n) m = S (n m)
type family Min (n :: Nat) (m :: Nat) :: Nat where
Min Z Z = Z
Min Z (S m) = Z
Min (S n) Z = Z
Min (S n) (S m) = S (Min n m)
type family Max (n :: Nat) (m :: Nat) :: Nat where
Max Z Z = Z
Max Z (S m) = S m
Max (S n) Z = S n
Max (S n) (S m) = S (Max n m)
data Longboi a (n :: Nat) where
Nil :: Longboi a Z
Cons :: a -> Longboi a n -> Longboi a (S n)
deriving instance Prelude.Eq a => Prelude.Eq (Longboi a n)
type family Length (xs :: Longboi a (n :: Nat)) :: Nat where
Length Nil = Z
Length (Cons x xs) = (S Z) + Length xs
type family Contains (xs :: Longboi a (n :: Nat)) (elem :: a) :: Bool where
Contains Nil _ = False
Contains (Cons x xs) x = True
Contains (Cons x xs) y = Contains xs y
infixr 5 ++
(++) :: Longboi a n -> Longboi a m -> Longboi a (n + m)
(Cons x xs) ++ ys = Cons x (xs ++ ys)
Nil ++ ys = ys
type family Append (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (m :: Nat)) :: Longboi a (n + m) where
Append (Cons x xs) ys = Cons x (Append xs ys)
Append Nil ys = ys
type family Head (xs :: Longboi a (n :: Nat)) :: a where
Head (Cons x _) = x
type family Last (xs :: Longboi a (n :: Nat)) :: a where
Last (Cons x Nil) = x
Last (Cons x xs) = Last xs
type family Tail (xs :: Longboi a ((S n) :: Nat)) :: Longboi a (n :: Nat) where
Tail (Cons _ xs) = xs
type family Init (xs :: Longboi a ((S n) :: Nat)) :: Longboi a (n :: Nat) where
Init (Cons _ Nil) = Nil
Init (Cons x xs ) = Cons x (Init xs)
type family Null (xs :: Longboi a (n :: Nat)) :: Bool where
Null Nil = True
Null _ = False
type family VMap (f :: a -> b) (xs :: Longboi a (n :: Nat)) :: Longboi b (n :: Nat) where
VMap _ Nil = Nil
VMap f (Cons x xs) = Cons (f x) (VMap f xs)
type family Foldl (f :: a -> b -> a) (x :: a) (ys :: Longboi b (n :: Nat)) :: a where
Foldl _ x Nil = x
Foldl f y (Cons x xs) = Foldl f (f y x) xs
type family Foldr (f :: a -> b -> b) (x :: b) (ys :: Longboi a (n :: Nat)) :: b where
Foldr _ y Nil = y
Foldr f y (Cons x xs) = f x (Foldr f y xs)
type family ZipWithSame (f :: a -> b -> c) (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (n :: Nat)) :: Longboi c (n :: Nat) where
ZipWithSame _ Nil Nil = Nil
ZipWithSame f (Cons a as) (Cons b bs) = Cons (f a b) (ZipWithSame f as bs)
type family ZipWith (f :: a -> b -> c) (xs :: Longboi a (n :: Nat)) (ys :: Longboi a (m :: Nat)) :: Longboi c (Min n m) where
ZipWith _ Nil Nil = Nil
ZipWith _ Nil (Cons _ _) = Nil
ZipWith _ (Cons _ _) Nil = Nil
ZipWith f (Cons a as) (Cons b bs) = Cons (f a b) (ZipWith f as bs)
head :: Longboi a (S n) -> a
head (Cons x _) = x
last :: Longboi a n -> a
last (Cons x Nil) = x
last (Cons x xs) = last xs
tail :: Longboi a (S n) -> Longboi a n
tail (Cons _ xs) = xs
init :: Longboi a (S n) -> Longboi a n
init (Cons x xs) =
case xs of
Nil -> Nil
(Cons _ _) -> Cons x (init xs)
uncons :: Longboi a (S n) -> (a, Longboi a n)
uncons (Cons x xs) = (x, xs)
null :: Longboi a n -> Bool
null Nil = True
null _ = False
vmap :: (a -> b) -> Longboi a n -> Longboi b n
vmap _ Nil = Nil
vmap f (Cons x xs) = Cons (f x) (vmap f xs)
foldl :: (a -> b -> a) -> a -> Longboi b n -> a
foldl _ x Nil = x
foldl f y (Cons x xs) = foldl f (f y x) xs
foldr :: (a -> b -> b) -> b -> Longboi a n -> b
foldr _ y Nil = y
foldr f y (Cons x xs) = f x (foldr f y xs)
toList :: Longboi a n -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs
zipWithSame :: (a -> b -> c) -> Longboi a n -> Longboi b n -> Longboi c n
zipWithSame _ Nil Nil = Nil
zipWithSame f (Cons a as) (Cons b bs) = Cons (f a b) (zipWithSame f as bs)
zipWith :: (a -> b -> c) -> Longboi a n -> Longboi b m -> Longboi c (Min n m)
zipWith _ Nil Nil = Nil
zipWith _ Nil (Cons _ _) = Nil
zipWith _ (Cons _ _) Nil = Nil
zipWith f (Cons a as) (Cons b bs) = Cons (f a b) (zipWith f as bs)