{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} -- | Module : Termonad.Config.Vec -- Description : A small library of dependent types -- Copyright : (c) Dennis Gosnell, 2018 -- License : BSD3 -- Stability : experimental -- Portability : POSIX -- -- This is a small library of dependent types. It provides indexed types like -- 'Fin', 'Vec', and 'Matrix'. -- -- This is mainly used in Termonad for "Termonad.Config.Colour" to represent -- length-indexed colour lists. -- -- This module implements a subset of the functionality from the abandoned -- <http://hackage.haskell.org/package/type-combinators type-combinators> library. -- Ideally this module would be split out to a separate package. -- If you're interested in working on something like this, please see -- <https://github.com/cdepillabout/termonad/issues/70 this issue> on Github. module Termonad.Config.Vec -- ( Fin -- , I(I) -- , M(M) -- , N3 -- , N24 -- , N6 -- , N8 -- , Prod((:<), Ø) -- , Range -- , Vec -- , VecT((:+), (:*), ØV, EmptyV) -- , fin -- , genMatrix_ -- , setSubmatrix -- , genVec_ -- , vSetAt' -- ) where import Termonad.Prelude hiding ((\\), index) import Data.Distributive (Distributive(distribute)) import qualified Data.Foldable as Data.Foldable import Data.Functor.Rep (Representable(..), apRep, bindRep, distributeRep, pureRep) import Data.Kind (Type) import Data.Singletons.Prelude import Data.Singletons.TH import Text.Show (showParen, showString) import Unsafe.Coerce (unsafeCoerce) -------------------------- -- Misc VecT Operations -- -------------------------- -- TODO: These could be implemented? -- data Range n l m = Range (IFin ('S n) l) (IFin ('S n) (l + m)) -- deriving (Show, Eq) -- instance (Known (IFin ('S n)) l, Known (IFin ('S n)) (l + m)) -- => Known (Range n l) m where -- type KnownC (Range n l) m -- = (Known (IFin ('S n)) l, Known (IFin ('S n)) (l + m)) -- known = Range known known -- updateRange :: Range n l m -> (Fin m -> f a -> f a) -> VecT n f a -> VecT n f a -- updateRange = \case -- Range IFZ IFZ -> \_ -> id -- Range (IFS l) (IFS m) -> \f -> onTail (updateRange (Range l m) f) \\ m -- Range IFZ (IFS m) -> \f -> onTail (updateRange (Range IFZ m) $ f . FS) -- . onHead (f FZ) \\ m -- setRange :: Range n l m -> VecT m f a -> VecT n f a -> VecT n f a -- setRange r nv = updateRange r (\i _ -> index i nv) -- updateSubmatrix -- :: (ns ~ Fsts3 nlms, ms ~ Thds3 nlms) -- => HList (Uncur3 Range) nlms -> (HList Fin ms -> a -> a) -> M ns a -> M ns a -- updateSubmatrix = \case -- Ø -> \f -> (f Ø <$>) -- Uncur3 r :< rs -> \f -> onMatrix . updateRange r $ \i -> -- asM . updateSubmatrix rs $ f . (i :<) -- setSubmatrix -- :: (ns ~ Fsts3 nlms, ms ~ Thds3 nlms) -- => HList (Uncur3 Range) nlms -> M ms a -> M ns a -> M ns a -- setSubmatrix rs sm = updateSubmatrix rs $ \is _ -> indexMatrix is sm ----------- -- Peano -- ----------- $(