From 174af2ba568de66e0d890825b8bda930b8e7bb96 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 10 Nov 2025 21:49:45 +0100 Subject: Move module hierarchy under CHAD. --- src/Data.hs | 192 ------------------------------------------------------------ 1 file changed, 192 deletions(-) delete mode 100644 src/Data.hs (limited to 'src/Data.hs') 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) -- cgit v1.2.3-70-g09d2