Move module hierarchy under CHAD.

1 files changed, 0 insertions, 192 deletions

diff --git a/src/Data.hs b/src/Data.hs
deleted file mode 100644
index e6978c8..0000000
--- a/src/Data.hs
+++ /dev/null
@@ -1,192 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-module Data (module Data, (:~:)(Refl), If) where
-
-import Data.Functor.Product
-import Data.GADT.Compare
-import Data.GADT.Show
-import Data.Some
-import Data.Type.Bool (If)
-import Data.Type.Equality
-import Unsafe.Coerce (unsafeCoerce)
-
-import Lemmas (Append)
-
-
-data Dict c where
-  Dict :: c => Dict c
-
-
-data SList f l where
-  SNil :: SList f '[]
-  SCons :: f a -> SList f l -> SList f (a : l)
-deriving instance (forall a. Show (f a)) => Show (SList f l)
-infixr `SCons`
-
-slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
-slistMap _ SNil = SNil
-slistMap f (SCons x list) = SCons (f x) (slistMap f list)
-
-slistMapA :: Applicative m => (forall t. f t -> m (g t)) -> SList f list -> m (SList g list)
-slistMapA _ SNil = pure SNil
-slistMapA f (SCons x list) = SCons <$> f x <*> slistMapA f list
-
-slistZip :: SList f list -> SList g list -> SList (Product f g) list
-slistZip SNil SNil = SNil
-slistZip (x `SCons` l1) (y `SCons` l2) = Pair x y `SCons` slistZip l1 l2
-
-unSList :: (forall t. f t -> a) -> SList f list -> [a]
-unSList _ SNil = []
-unSList f (x `SCons` l) = f x : unSList f l
-
-showSList :: (forall t. Int -> f t -> String) -> SList f list -> String
-showSList _ SNil = "SNil"
-showSList f (x `SCons` l) = f 11 x ++ " `SCons` " ++ showSList f l
-
-sappend :: SList f l1 -> SList f l2 -> SList f (Append l1 l2)
-sappend SNil l = l
-sappend (SCons x xs) l = SCons x (sappend xs l)
-
-type family Replicate n x where
-  Replicate Z x = '[]
-  Replicate (S n) x = x : Replicate n x
-
-sreplicate :: SNat n -> f t -> SList f (Replicate n t)
-sreplicate SZ _ = SNil
-sreplicate (SS n) x = x `SCons` sreplicate n x
-
-data Nat = Z | S Nat
-  deriving (Show, Eq, Ord)
-
-type N0 = Z
-type N1 = S N0
-type N2 = S N1
-type N3 = S N2
-
-data SNat n where
-  SZ :: SNat Z
-  SS :: SNat n -> SNat (S n)
-deriving instance Show (SNat n)
-
-instance GCompare SNat where
-  gcompare SZ SZ = GEQ
-  gcompare SZ _ = GLT
-  gcompare _ SZ = GGT
-  gcompare (SS n) (SS n') = gorderingLift1 (gcompare n n')
-
-instance TestEquality SNat where testEquality = geq
-instance GEq SNat where geq = defaultGeq
-instance GShow SNat where gshowsPrec = defaultGshowsPrec
-
-fromSNat :: SNat n -> Int
-fromSNat SZ = 0
-fromSNat (SS n) = succ (fromSNat n)
-
-unSNat :: SNat n -> Nat
-unSNat SZ = Z
-unSNat (SS n) = S (unSNat n)
-
-reSNat :: Nat -> Some SNat
-reSNat Z = Some SZ
-reSNat (S n) | Some n' <- reSNat n = Some (SS n')
-
-class KnownNat n where knownNat :: SNat n
-instance KnownNat Z where knownNat = SZ
-instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
-
-snatKnown :: SNat n -> Dict (KnownNat n)
-snatKnown SZ = Dict
-snatKnown (SS n) | Dict <- snatKnown n = Dict
-
-type family n + m where
-  Z + m = m
-  S n + m = S (n + m)
-
-type family n - m where
-  n - Z = n
-  S n - S m = n - m
-
-snatAdd :: SNat n -> SNat m -> SNat (n + m)
-snatAdd SZ m = m
-snatAdd (SS n) m = SS (snatAdd n m)
-
-lemPlusSuccRight :: n + S m :~: S (n + m)
-lemPlusSuccRight = unsafeCoerceRefl
-
-lemPlusZero :: n + Z :~: n
-lemPlusZero = unsafeCoerceRefl
-
-data Vec n t where
-  VNil :: Vec Z t
-  (:<) :: t -> Vec n t -> Vec (S n) t
-deriving instance Show t => Show (Vec n t)
-deriving instance Eq t => Eq (Vec n t)
-deriving instance Functor (Vec n)
-deriving instance Foldable (Vec n)
-deriving instance Traversable (Vec n)
-
-vecLength :: Vec n t -> SNat n
-vecLength VNil = SZ
-vecLength (_ :< v) = SS (vecLength v)
-
-vecGenerate :: SNat n -> (forall i. SNat i -> t) -> Vec n t
-vecGenerate = \n f -> go n f SZ
-  where
-    go :: SNat n -> (forall i. SNat i -> t) -> SNat i' -> Vec n t
-    go SZ _ _ = VNil
-    go (SS n) f i = f i :< go n f (SS i)
-
-vecReplicateA :: Applicative f => SNat n -> f a -> f (Vec n a)
-vecReplicateA SZ _ = pure VNil
-vecReplicateA (SS n) gen = (:<) <$> gen <*> vecReplicateA n gen
-
-vecZipWithA :: Applicative f => (a -> b -> f c) -> Vec n a -> Vec n b -> f (Vec n c)
-vecZipWithA _ VNil VNil = pure VNil
-vecZipWithA f (x :< xs) (y :< ys) = (:<) <$> f x y <*> vecZipWithA f xs ys
-
-vecInit :: Vec (S n) a -> Vec n a
-vecInit (_ :< VNil) = VNil
-vecInit (x :< xs@(_ :< _)) = x :< vecInit xs
-
-unsafeCoerceRefl :: a :~: b
-unsafeCoerceRefl = unsafeCoerce Refl
-
-gorderingLift1 :: GOrdering a a' -> GOrdering (f a) (f a')
-gorderingLift1 GLT = GLT
-gorderingLift1 GGT = GGT
-gorderingLift1 GEQ = GEQ
-
-gorderingLift2 :: GOrdering a a' -> GOrdering b b' -> GOrdering (f a b) (f a' b')
-gorderingLift2 GLT _ = GLT
-gorderingLift2 GGT _ = GGT
-gorderingLift2 GEQ GLT = GLT
-gorderingLift2 GEQ GGT = GGT
-gorderingLift2 GEQ GEQ = GEQ
-
-data Bag t = BNone | BOne t | BTwo !(Bag t) !(Bag t) | BMany [Bag t] | BList [t]
-  deriving (Show, Functor, Foldable, Traversable)
-
--- | This instance is mostly there just for 'pure'
-instance Applicative Bag where
-  pure = BOne
-  BNone <*> _ = BNone
-  BOne f <*> b = f <$> b
-  BTwo b1 b2 <*> b = BTwo (b1 <*> b) (b2 <*> b)
-  BMany bs <*> b = BMany (map (<*> b) bs)
-  BList bs <*> b = BMany (map (<$> b) bs)
-
-instance Semigroup (Bag t) where (<>) = BTwo
-instance Monoid (Bag t) where mempty = BNone
-
-data SBool b where
-  SF :: SBool False
-  ST :: SBool True
-deriving instance Show (SBool b)