{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Numeric.TypedList
( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)
, RepresentableList (..)
, Dict1 (..), DictList
, TypeList, types, typeables, inferTypeableList
, order, order'
, cons, snoc
, Numeric.TypedList.reverse
, Numeric.TypedList.take
, Numeric.TypedList.drop
, Numeric.TypedList.head
, Numeric.TypedList.tail
, Numeric.TypedList.last
, Numeric.TypedList.init
, Numeric.TypedList.splitAt
, Numeric.TypedList.stripPrefix
, Numeric.TypedList.stripSuffix
, Numeric.TypedList.sameList
, Numeric.TypedList.concat
, Numeric.TypedList.length
, Numeric.TypedList.map
, module Data.Type.List
, typedListShowsPrecC, typedListShowsPrec
, typedListReadPrec, withTypedListReadPrec
) where
import Control.Arrow (first)
import Data.Constraint hiding ((***))
import Data.Data
import Data.Type.List
import Data.Type.List.Internal
import Data.Type.Lits
import Data.Void
import GHC.Base (Type)
import GHC.Exts
import GHC.Generics hiding (Infix, Prefix)
import qualified Text.ParserCombinators.ReadPrec as Read
import qualified Text.Read as Read
import qualified Text.Read.Lex as Read
import qualified Type.Reflection as R
import Unsafe.Coerce (unsafeCoerce)
import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, dimVal, minusDimM)
newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]
deriving (Typeable)
type role TypedList representational representational
{-# COMPLETE TypeList #-}
{-# COMPLETE EvList #-}
{-# COMPLETE U, (:*) #-}
{-# COMPLETE U, Cons #-}
{-# COMPLETE U, Snoc #-}
{-# COMPLETE Empty, (:*) #-}
{-# COMPLETE Empty, Cons #-}
{-# COMPLETE Empty, Snoc #-}
{-# COMPLETE Reverse #-}
instance (Typeable k, Typeable f, Typeable xs, All Data (Map f xs))
=> Data (TypedList (f :: (k -> Type)) (xs :: [k])) where
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypedList f xs -> c (TypedList f xs)
gfoldl forall d b. Data d => c (d -> b) -> d -> c b
_ forall g. g -> c g
z TypedList f xs
U = TypedList f xs -> c (TypedList f xs)
forall g. g -> c g
z TypedList f xs
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
gfoldl forall d b. Data d => c (d -> b) -> d -> c b
k forall g. g -> c g
z (f y
x :* TypedList f ys
xs) = case forall (x :: k) (xs :: [k]).
(Typeable xs, xs ~ (x : xs)) =>
Dict (Typeable x, Typeable xs)
forall k (ys :: [k]) (x :: k) (xs :: [k]).
(Typeable ys, ys ~ (x : xs)) =>
Dict (Typeable x, Typeable xs)
inferTypeableCons @xs of
Dict (Typeable y, Typeable ys)
Dict -> (f y -> TypedList f ys -> TypedList f xs)
-> c (f y -> TypedList f ys -> TypedList f xs)
forall g. g -> c g
z f y -> TypedList f ys -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
(:*) c (f y -> TypedList f ys -> TypedList f xs)
-> f y -> c (TypedList f ys -> TypedList f xs)
forall d b. Data d => c (d -> b) -> d -> c b
`k` f y
x c (TypedList f ys -> TypedList f xs)
-> TypedList f ys -> c (TypedList f xs)
forall d b. Data d => c (d -> b) -> d -> c b
`k` TypedList f ys
xs
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypedList f xs)
gunfold forall b r. Data b => c (b -> r) -> c r
k forall r. r -> c r
z Constr
_ = case Typeable xs => TypeList xs
forall k (xs :: [k]). Typeable xs => TypeList xs
typeables @xs of
TypeList xs
U -> TypedList f xs -> c (TypedList f xs)
forall r. r -> c r
z TypedList f xs
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
Proxy y
_ :* TypedList Proxy ys
_ -> case forall (x :: k) (xs :: [k]).
(Typeable xs, xs ~ (x : xs)) =>
Dict (Typeable x, Typeable xs)
forall k (ys :: [k]) (x :: k) (xs :: [k]).
(Typeable ys, ys ~ (x : xs)) =>
Dict (Typeable x, Typeable xs)
inferTypeableCons @xs of Dict (Typeable y, Typeable ys)
Dict -> c (TypedList f ys -> TypedList f xs) -> c (TypedList f xs)
forall b r. Data b => c (b -> r) -> c r
k (c (f y -> TypedList f ys -> TypedList f xs)
-> c (TypedList f ys -> TypedList f xs)
forall b r. Data b => c (b -> r) -> c r
k ((f y -> TypedList f ys -> TypedList f xs)
-> c (f y -> TypedList f ys -> TypedList f xs)
forall r. r -> c r
z f y -> TypedList f ys -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
(:*)))
toConstr :: TypedList f xs -> Constr
toConstr TypedList f xs
U = Constr
typedListConstrEmpty
toConstr (f y
_ :* TypedList f ys
_) = Constr
typedListConstrCons
dataTypeOf :: TypedList f xs -> DataType
dataTypeOf TypedList f xs
_ = DataType
typedListDataType
typedListDataType :: DataType
typedListDataType :: DataType
typedListDataType = String -> [Constr] -> DataType
mkDataType
String
"Numeric.TypedList.TypedList" [Constr
typedListConstrEmpty, Constr
typedListConstrCons]
typedListConstrEmpty :: Constr
typedListConstrEmpty :: Constr
typedListConstrEmpty = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
typedListDataType String
"U" [] Fixity
Prefix
typedListConstrCons :: Constr
typedListConstrCons :: Constr
typedListConstrCons = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
typedListDataType String
":*" [] Fixity
Infix
type family TypedListRepNil (xs :: [k]) :: (Type -> Type) where
TypedListRepNil '[] = C1 ('MetaCons "U" 'PrefixI 'False) U1
TypedListRepNil (_ ': _) = Rec0 Void
type family TypedListRepCons (f :: (k -> Type)) (xs :: [k]) :: (Type -> Type) where
TypedListRepCons _ '[]
= Rec0 Void
TypedListRepCons f (x ': xs)
= C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness
'NoSourceStrictness 'DecidedLazy)
(Rec0 (f x))
:*:
S1 ('MetaSel 'Nothing 'NoSourceUnpackedness
'NoSourceStrictness 'DecidedLazy)
(Rec0 (TypedList f xs))
)
instance Generic (TypedList (f :: (k -> Type)) (xs :: [k])) where
type Rep (TypedList f xs) = D1
('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False)
( TypedListRepNil xs :+: TypedListRepCons f xs )
from :: TypedList f xs -> Rep (TypedList f xs) x
from TypedList f xs
U = (:+:) (M1 C ('MetaCons "U" 'PrefixI 'False) U1) (Rec0 Void) x
-> M1
D
('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False)
(M1 C ('MetaCons "U" 'PrefixI 'False) U1 :+: Rec0 Void)
x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1 C ('MetaCons "U" 'PrefixI 'False) U1 x
-> (:+:) (M1 C ('MetaCons "U" 'PrefixI 'False) U1) (Rec0 Void) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (U1 x -> M1 C ('MetaCons "U" 'PrefixI 'False) U1 x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 U1 x
forall k (p :: k). U1 p
U1))
from (f y
x :* TypedList f ys
xs) = (:+:)
(Rec0 Void)
(M1
C
('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
:*: M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys))))
x
-> M1
D
('MetaData "TypedList" "Numeric.TypedList" "dimensions" 'False)
(Rec0 Void
:+: M1
C
('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
:*: M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys))))
x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1
C
('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
:*: M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys)))
x
-> (:+:)
(Rec0 Void)
(M1
C
('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
:*: M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys))))
x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 ((:*:)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y)))
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys)))
x
-> M1
C
('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
:*: M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys)))
x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (K1 R (f y) x
-> M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f y -> K1 R (f y) x
forall k i c (p :: k). c -> K1 i c p
K1 f y
x) M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y))
x
-> M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys))
x
-> (:*:)
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (f y)))
(M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys)))
x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: K1 R (TypedList f ys) x
-> M1
S
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(K1 R (TypedList f ys))
x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (TypedList f ys -> K1 R (TypedList f ys) x
forall k i c (p :: k). c -> K1 i c p
K1 TypedList f ys
xs))))
to :: Rep (TypedList f xs) x -> TypedList f xs
to (M1 (L1 _))
| Dict (xs ~ '[])
Dict <- Dict (xs ~ '[])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @'[] = TypedList f xs
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
to (M1 (R1 xxs))
| Dict (xs ~ (Head xs : Tail xs))
Dict <- Dict (xs ~ (Head xs : Tail xs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @(Head xs ': Tail xs)
, M1 (M1 (K1 x) :*: M1 (K1 xs)) <- TypedListRepCons f xs x
xxs = f (Head xs)
x f (Head xs) -> TypedList f (Tail xs) -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* TypedList f (Tail xs)
xs
type TypeList = (TypedList Proxy :: [k] -> Type)
data Dict1 :: (k -> Constraint) -> k -> Type where
Dict1 :: c a => Dict1 c a
deriving Typeable
instance (Typeable k, Typeable p, Typeable a, p a)
=> Data (Dict1 (p :: k -> Constraint) (a :: k)) where
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Dict1 p a -> c (Dict1 p a)
gfoldl forall d b. Data d => c (d -> b) -> d -> c b
_ forall g. g -> c g
z Dict1 p a
Dict1 = Dict1 p a -> c (Dict1 p a)
forall g. g -> c g
z Dict1 p a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1
toConstr :: Dict1 p a -> Constr
toConstr Dict1 p a
_ = Constr
dictConstr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Dict1 p a)
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
z Constr
_ = Dict1 p a -> c (Dict1 p a)
forall r. r -> c r
z Dict1 p a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1
dataTypeOf :: Dict1 p a -> DataType
dataTypeOf Dict1 p a
_ = DataType
dictDataType
dictConstr :: Constr
dictConstr :: Constr
dictConstr = DataType -> String -> [String] -> Fixity -> Constr
mkConstr DataType
dictDataType String
"Dict1" [] Fixity
Prefix
dictDataType :: DataType
dictDataType :: DataType
dictDataType = String -> [Constr] -> DataType
mkDataType String
"Numeric.TypedList.Dict1" [Constr
dictConstr]
deriving instance Eq (Dict1 (p :: k -> Constraint) (a :: k))
deriving instance Ord (Dict1 (p :: k -> Constraint) (a :: k))
deriving instance Show (Dict1 (p :: k -> Constraint) (a :: k))
type DictList (c :: k -> Constraint)
= (TypedList (Dict1 c) :: [k] -> Type)
pattern TypeList :: forall xs . () => RepresentableList xs => TypeList xs
pattern $bTypeList :: TypeList xs
$mTypeList :: forall r k (xs :: [k]).
TypeList xs -> (RepresentableList xs => r) -> (Void# -> r) -> r
TypeList <- (mkRTL -> Dict)
where
TypeList = RepresentableList xs => TypeList xs
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @xs
pattern EvList :: forall c xs
. () => (All c xs, RepresentableList xs) => DictList c xs
pattern $bEvList :: DictList c xs
$mEvList :: forall r k (c :: k -> Constraint) (xs :: [k]).
DictList c xs
-> ((All c xs, RepresentableList xs) => r) -> (Void# -> r) -> r
EvList <- (mkEVL -> Dict)
where
EvList = TypedList Proxy xs -> DictList c xs
forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *).
All c xs =>
TypedList f xs -> DictList c xs
_evList (RepresentableList xs => TypedList Proxy xs
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @xs)
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern $bU :: TypedList f xs
$mU :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs -> ((xs ~ '[]) => r) -> (Void# -> r) -> r
U <- (patTL @k @f @xs -> PatCNil)
where
U = [Any] -> TypedList f xs
coerce ([] :: [Any])
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. () => (xs ~ '[]) => TypedList f xs
pattern $bEmpty :: TypedList f xs
$mEmpty :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs -> ((xs ~ '[]) => r) -> (Void# -> r) -> r
Empty = U
pattern (:*) :: forall f xs
. ()
=> forall y ys
. (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs
pattern $b:* :: f y -> TypedList f ys -> TypedList f xs
$m:* :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs
-> (forall (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> r)
-> (Void# -> r)
-> r
(:*) x xs = Cons x xs
infixr 5 :*
pattern Cons :: forall f xs
. ()
=> forall y ys
. (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs
pattern $bCons :: f y -> TypedList f ys -> TypedList f xs
$mCons :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs
-> (forall (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> r)
-> (Void# -> r)
-> r
Cons x xs <- (patTL @_ @f @xs -> PatCons x xs)
where
Cons = f y -> TypedList f ys -> TypedList f xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> TypedList f xs -> TypedList f (x :+ xs)
Numeric.TypedList.cons
pattern Snoc :: forall f xs . ()
=> forall sy y . SnocList sy y xs
=> TypedList f sy -> f y -> TypedList f xs
pattern $bSnoc :: TypedList f sy -> f y -> TypedList f xs
$mSnoc :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs
-> (forall (sy :: [k]) (y :: k).
SnocList sy y xs =>
TypedList f sy -> f y -> r)
-> (Void# -> r)
-> r
Snoc sx x <- (unsnocTL @_ @f @xs -> PatSnoc sx x)
where
Snoc = TypedList f sy -> f y -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]) (x :: k).
TypedList f xs -> f x -> TypedList f (xs +: x)
Numeric.TypedList.snoc
pattern Reverse :: forall f xs . ()
=> forall sx . ReverseList xs sx
=> TypedList f sx -> TypedList f xs
pattern $bReverse :: TypedList f sx -> TypedList f xs
$mReverse :: forall r k (f :: k -> *) (xs :: [k]).
TypedList f xs
-> (forall (sx :: [k]). ReverseList xs sx => TypedList f sx -> r)
-> (Void# -> r)
-> r
Reverse sx <- (unreverseTL @_ @f @xs -> PatReverse sx)
where
Reverse = TypedList f sx -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> TypedList f (Reverse xs)
Numeric.TypedList.reverse
cons :: forall f x xs
. f x -> TypedList f xs -> TypedList f (x :+ xs)
cons :: f x -> TypedList f xs -> TypedList f (x :+ xs)
cons f x
x TypedList f xs
xs = [Any] -> TypedList f (x :+ xs)
forall k (f :: k -> *) (xs :: [k]). [Any] -> TypedList f xs
TypedList (f x -> Any
forall a b. a -> b
unsafeCoerce f x
x Any -> [Any] -> [Any]
forall a. a -> [a] -> [a]
: TypedList f xs -> [Any]
coerce TypedList f xs
xs)
{-# INLINE cons #-}
snoc :: forall f xs x
. TypedList f xs -> f x -> TypedList f (xs +: x)
snoc :: TypedList f xs -> f x -> TypedList f (xs +: x)
snoc TypedList f xs
xs f x
x = [Any] -> TypedList f (xs +: x)
forall k (f :: k -> *) (xs :: [k]). [Any] -> TypedList f xs
TypedList (TypedList f xs -> [Any]
coerce TypedList f xs
xs [Any] -> [Any] -> [Any]
forall a. [a] -> [a] -> [a]
++ [f x -> Any
forall a b. a -> b
unsafeCoerce f x
x])
{-# INLINE snoc #-}
reverse :: forall f xs
. TypedList f xs -> TypedList f (Reverse xs)
reverse :: TypedList f xs -> TypedList f (Reverse xs)
reverse = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Reverse xs)
coerce ([Any] -> [Any]
forall a. [a] -> [a]
Prelude.reverse :: [Any] -> [Any])
{-# INLINE reverse #-}
head :: forall f xs
. TypedList f xs -> f (Head xs)
head :: TypedList f xs -> f (Head xs)
head (TypedList [Any]
xs) = Any -> f (Head xs)
forall a b. a -> b
unsafeCoerce ([Any] -> Any
forall a. [a] -> a
Prelude.head [Any]
xs)
{-# INLINE head #-}
tail :: forall f xs
. TypedList f xs -> TypedList f (Tail xs)
tail :: TypedList f xs -> TypedList f (Tail xs)
tail = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Tail xs)
coerce ([Any] -> [Any]
forall a. [a] -> [a]
Prelude.tail :: [Any] -> [Any])
{-# INLINE tail #-}
init :: forall f xs
. TypedList f xs -> TypedList f (Init xs)
init :: TypedList f xs -> TypedList f (Init xs)
init = ([Any] -> [Any]) -> TypedList f xs -> TypedList f (Init xs)
coerce ([Any] -> [Any]
forall a. [a] -> [a]
Prelude.init :: [Any] -> [Any])
{-# INLINE init #-}
last :: forall f xs
. TypedList f xs -> f (Last xs)
last :: TypedList f xs -> f (Last xs)
last (TypedList [Any]
xs) = Any -> f (Last xs)
forall a b. a -> b
unsafeCoerce ([Any] -> Any
forall a. [a] -> a
Prelude.last [Any]
xs)
{-# INLINE last #-}
take :: forall (n :: Nat) f xs
. Dim n -> TypedList f xs -> TypedList f (Take n xs)
take :: Dim n -> TypedList f xs -> TypedList f (Take n xs)
take = (Dim n -> [Any] -> [Any])
-> Dim n -> TypedList f xs -> TypedList f (Take n xs)
coerce (Int -> [Any] -> [Any]
forall a. Int -> [a] -> [a]
Prelude.take (Int -> [Any] -> [Any])
-> (Dim n -> Int) -> Dim n -> [Any] -> [Any]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim n -> Int
forall k (x :: k). Dim x -> Int
dimValInt :: Dim n -> [Any] -> [Any])
{-# INLINE take #-}
drop :: forall (n :: Nat) f xs
. Dim n -> TypedList f xs -> TypedList f (Drop n xs)
drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs)
drop = (Dim n -> [Any] -> [Any])
-> Dim n -> TypedList f xs -> TypedList f (Drop n xs)
coerce (Int -> [Any] -> [Any]
forall a. Int -> [a] -> [a]
Prelude.drop (Int -> [Any] -> [Any])
-> (Dim n -> Int) -> Dim n -> [Any] -> [Any]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim n -> Int
forall k (x :: k). Dim x -> Int
dimValInt :: Dim n -> [Any] -> [Any])
{-# INLINE drop #-}
length :: forall f xs
. TypedList f xs -> Dim (Length xs)
length :: TypedList f xs -> Dim (Length xs)
length = TypedList f xs -> Dim (Length xs)
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> Dim (Length xs)
order
{-# INLINE length #-}
splitAt :: forall (n :: Nat) f xs
. Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
splitAt :: Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
splitAt = (Dim n -> [Any] -> ([Any], [Any]))
-> Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
coerce (Int -> [Any] -> ([Any], [Any])
forall a. Int -> [a] -> ([a], [a])
Prelude.splitAt (Int -> [Any] -> ([Any], [Any]))
-> (Dim n -> Int) -> Dim n -> [Any] -> ([Any], [Any])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim n -> Int
forall k (x :: k). Dim x -> Int
dimValInt :: Dim n -> [Any] -> ([Any], [Any]))
{-# INLINE splitAt #-}
order' :: forall xs . RepresentableList xs => Dim (Length xs)
order' :: Dim (Length xs)
order' = TypedList Proxy xs -> Dim (Length xs)
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> Dim (Length xs)
order (RepresentableList xs => TypedList Proxy xs
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @xs)
{-# INLINE order' #-}
order :: forall f xs
. TypedList f xs -> Dim (Length xs)
order :: TypedList f xs -> Dim (Length xs)
order = ([Any] -> Word) -> TypedList f xs -> Dim (Length xs)
forall a b. a -> b
unsafeCoerce (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word) -> ([Any] -> Int) -> [Any] -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Any] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length :: [Any] -> Word)
{-# INLINE order #-}
concat :: forall f xs ys
. TypedList f xs
-> TypedList f ys
-> TypedList f (xs ++ ys)
concat :: TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
concat = ([Any] -> [Any] -> [Any])
-> TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
coerce ([Any] -> [Any] -> [Any]
forall a. [a] -> [a] -> [a]
(++) :: [Any] -> [Any] -> [Any])
{-# INLINE concat #-}
stripPrefix :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (TypedList f (StripPrefix xs ys))
stripPrefix :: TypedList f xs
-> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys))
stripPrefix TypedList f xs
U TypedList f ys
ys = TypedList f ys -> Maybe (TypedList f ys)
forall a. a -> Maybe a
Just TypedList f ys
ys
stripPrefix TypedList f xs
_ TypedList f ys
U = Maybe (TypedList f (StripPrefix xs ys))
forall a. Maybe a
Nothing
stripPrefix ((f y
x :: f x) :* TypedList f ys
xs) ((f y
y :: f y) :* TypedList f ys
ys)
| Just y :~: y
Refl <- (Typeable y, Typeable y) => Maybe (y :~: y)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @y
, f y
x f y -> f y -> Bool
forall a. Eq a => a -> a -> Bool
== f y
f y
y = Maybe (TypedList f (StripPrefix ys ys))
-> Maybe (TypedList f (StripPrefix (y : ys) (y : ys)))
coerce (TypedList f ys
-> TypedList f ys -> Maybe (TypedList f (StripPrefix ys ys))
forall k (f :: k -> *) (xs :: [k]) (ys :: [k]).
(All Typeable xs, All Typeable ys, All Eq (Map f xs)) =>
TypedList f xs
-> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys))
stripPrefix TypedList f ys
xs TypedList f ys
ys)
| Bool
otherwise = Maybe (TypedList f (StripPrefix xs ys))
forall a. Maybe a
Nothing
{-# INLINE stripPrefix #-}
stripSuffix :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (TypedList f (StripSuffix xs ys))
stripSuffix :: TypedList f xs
-> TypedList f ys -> Maybe (TypedList f (StripSuffix xs ys))
stripSuffix TypedList f xs
U TypedList f ys
ys = TypedList f ys -> Maybe (TypedList f ys)
forall a. a -> Maybe a
Just TypedList f ys
ys
stripSuffix TypedList f xs
_ TypedList f ys
U = Maybe (TypedList f (StripSuffix xs ys))
forall a. Maybe a
Nothing
stripSuffix TypedList f xs
xs TypedList f ys
ys
| Just Dim (Length ys - Length xs)
n <- TypedList f ys -> Dim (Length ys)
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> Dim (Length xs)
order TypedList f ys
ys Dim (Length ys)
-> Dim (Length xs) -> Maybe (Dim (Length ys - Length xs))
forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Maybe (Dim (n - m))
`minusDimM` TypedList f xs -> Dim (Length xs)
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> Dim (Length xs)
order TypedList f xs
xs
, (TypedList f (Take (Length ys - Length xs) ys)
zs, TypedList f (Drop (Length ys - Length xs) ys)
xs') <- Dim (Length ys - Length xs)
-> TypedList f ys
-> (TypedList f (Take (Length ys - Length xs) ys),
TypedList f (Drop (Length ys - Length xs) ys))
forall k (n :: Nat) (f :: k -> *) (xs :: [k]).
Dim n
-> TypedList f xs
-> (TypedList f (Take n xs), TypedList f (Drop n xs))
Numeric.TypedList.splitAt Dim (Length ys - Length xs)
n TypedList f ys
ys
, TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys)
EvList <- Dim (Length ys - Length xs)
-> TypedList (Dict1 Typeable) ys
-> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys)
forall k (n :: Nat) (f :: k -> *) (xs :: [k]).
Dim n -> TypedList f xs -> TypedList f (Drop n xs)
Numeric.TypedList.drop Dim (Length ys - Length xs)
n (TypedList (Dict1 Typeable) ys
-> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys))
-> TypedList (Dict1 Typeable) ys
-> TypedList (Dict1 Typeable) (Drop (Length ys - Length xs) ys)
forall a b. (a -> b) -> a -> b
$ TypedList f ys -> TypedList (Dict1 Typeable) ys
forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *).
All c xs =>
TypedList f xs -> DictList c xs
_evList @_ @Typeable TypedList f ys
ys
, Just (xs :~: Drop (Length ys - Length xs) ys
Refl, Bool
True) <- TypedList f xs
-> TypedList f (Drop (Length ys - Length xs) ys)
-> Maybe (xs :~: Drop (Length ys - Length xs) ys, Bool)
forall k (f :: k -> *) (xs :: [k]) (ys :: [k]).
(All Typeable xs, All Typeable ys, All Eq (Map f xs)) =>
TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
sameList TypedList f xs
xs TypedList f (Drop (Length ys - Length xs) ys)
xs'
= TypedList f (StripSuffix xs ys)
-> Maybe (TypedList f (StripSuffix xs ys))
forall a. a -> Maybe a
Just (TypedList f (Take (Length ys - Length xs) ys)
-> TypedList f (StripSuffix xs ys)
coerce TypedList f (Take (Length ys - Length xs) ys)
zs)
| Bool
otherwise = Maybe (TypedList f (StripSuffix xs ys))
forall a. Maybe a
Nothing
{-# INLINE stripSuffix #-}
sameList :: forall f xs ys
. ( All Typeable xs, All Typeable ys, All Eq (Map f xs))
=> TypedList f xs
-> TypedList f ys
-> Maybe (xs :~: ys, Bool)
sameList :: TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
sameList TypedList f xs
U TypedList f ys
U = (xs :~: xs, Bool) -> Maybe (xs :~: xs, Bool)
forall a. a -> Maybe a
Just (xs :~: xs
forall k (a :: k). a :~: a
Refl, Bool
True)
sameList ((f y
x :: f x) :* TypedList f ys
xs) ((f y
y :: f y) :* TypedList f ys
ys)
| Just y :~: y
Refl <- (Typeable y, Typeable y) => Maybe (y :~: y)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @y
, Just (ys :~: ys
Refl, Bool
b) <- TypedList f ys -> TypedList f ys -> Maybe (ys :~: ys, Bool)
forall k (f :: k -> *) (xs :: [k]) (ys :: [k]).
(All Typeable xs, All Typeable ys, All Eq (Map f xs)) =>
TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
sameList TypedList f ys
xs TypedList f ys
ys
= (xs :~: xs, Bool) -> Maybe (xs :~: xs, Bool)
forall a. a -> Maybe a
Just (xs :~: xs
forall k (a :: k). a :~: a
Refl, f y
x f y -> f y -> Bool
forall a. Eq a => a -> a -> Bool
== f y
f y
y Bool -> Bool -> Bool
&& Bool
b)
| Bool
otherwise
= Maybe (xs :~: ys, Bool)
forall a. Maybe a
Nothing
sameList TypedList f xs
_ TypedList f ys
_ = Maybe (xs :~: ys, Bool)
forall a. Maybe a
Nothing
map :: forall f g xs
. (forall a . f a -> g a)
-> TypedList f xs
-> TypedList g xs
map :: (forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs
map forall (a :: k). f a -> g a
k = ([Any] -> [Any]) -> TypedList f xs -> TypedList g xs
coerce ((Any -> Any) -> [Any] -> [Any]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map Any -> Any
k')
where
k' :: Any -> Any
k' :: Any -> Any
k' = (f Any -> g Any) -> Any -> Any
forall a b. a -> b
unsafeCoerce f Any -> g Any
forall (a :: k). f a -> g a
k
{-# INLINE map #-}
types :: forall f xs
. TypedList f xs -> TypeList xs
types :: TypedList f xs -> TypeList xs
types = (forall (a :: k). f a -> Proxy a) -> TypedList f xs -> TypeList xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
(forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs
Numeric.TypedList.map (Proxy a -> f a -> Proxy a
forall a b. a -> b -> a
const Proxy a
forall k (t :: k). Proxy t
Proxy)
{-# INLINE types #-}
typeables :: forall xs . Typeable xs => TypeList xs
typeables :: TypeList xs
typeables = case Typeable xs => TypeRep xs
forall k (a :: k). Typeable a => TypeRep a
R.typeRep @xs of
R.App (R.App TypeRep a
_ (TypeRep b
_ :: R.TypeRep (n :: k))) (TypeRep b
txs :: R.TypeRep (ns :: ks))
| Dict (k1 ~ k, k1 ~ [k])
Dict <- Dict (k1 ~ k1, k1 ~ k1) -> Dict (k1 ~ k, k1 ~ [k])
forall a b. a -> b
unsafeCoerce ((k1 ~ k1, k1 ~ k1) => Dict (k1 ~ k1, k1 ~ k1)
forall (a :: Constraint). a => Dict a
Dict @(k ~ k, ks ~ ks))
:: Dict (k ~ KindOfEl xs, ks ~ KindOf xs)
, Dict (xs ~ (b : b))
Dict <- Dict (xs ~ (b : b))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @(n ': ns)
-> Proxy b
forall k (t :: k). Proxy t
Proxy @n Proxy b -> TypedList Proxy b -> TypedList Proxy (b : b)
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* TypeRep b -> (Typeable b => TypedList Proxy b) -> TypedList Proxy b
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
R.withTypeable TypeRep b
txs (Typeable b => TypeList b
forall k (xs :: [k]). Typeable xs => TypeList xs
typeables @ns)
R.Con TyCon
_
-> TypedList Any '[] -> TypeList xs
forall a b. a -> b
unsafeCoerce TypedList Any '[]
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
TypeRep xs
r -> String -> TypeList xs
forall a. HasCallStack => String -> a
error (String
"typeables -- impossible typeRep: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep xs -> String
forall a. Show a => a -> String
show TypeRep xs
r)
{-# INLINE typeables #-}
inferTypeableList :: forall f xs
. (Typeable (KindOfEl xs), All Typeable xs)
=> TypedList f xs -> Dict (Typeable xs)
inferTypeableList :: TypedList f xs -> Dict (Typeable xs)
inferTypeableList TypedList f xs
U = Dict (Typeable xs)
forall (a :: Constraint). a => Dict a
Dict
inferTypeableList (f y
_ :* TypedList f ys
xs) = case TypedList f ys -> Dict (Typeable ys)
forall k (f :: k -> *) (xs :: [k]).
(Typeable k, All Typeable xs) =>
TypedList f xs -> Dict (Typeable xs)
inferTypeableList TypedList f ys
xs of Dict (Typeable ys)
Dict -> Dict (Typeable xs)
forall (a :: Constraint). a => Dict a
Dict
class RepresentableList xs where
tList :: TypeList xs
instance RepresentableList ('[] :: [k]) where
tList :: TypeList '[]
tList = TypeList '[]
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where
tList :: TypeList (x : xs)
tList = Proxy x
forall k (t :: k). Proxy t
Proxy @x Proxy x -> TypedList Proxy xs -> TypeList (x : xs)
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* RepresentableList xs => TypedList Proxy xs
forall k (xs :: [k]). RepresentableList xs => TypeList xs
tList @xs
typedListShowsPrecC :: forall c f xs
. All c xs
=> String
-> ( forall x . c x => Int -> f x -> ShowS )
-> Int -> TypedList f xs -> ShowS
typedListShowsPrecC :: String
-> (forall (x :: k). c x => Int -> f x -> ShowS)
-> Int
-> TypedList f xs
-> ShowS
typedListShowsPrecC String
_ forall (x :: k). c x => Int -> f x -> ShowS
_ Int
_ TypedList f xs
U = Char -> ShowS
showChar Char
'U'
typedListShowsPrecC String
consS forall (x :: k). c x => Int -> f x -> ShowS
elShowsPrec Int
p (f y
x :* TypedList f ys
xs) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
6)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> f y -> ShowS
forall (x :: k). c x => Int -> f x -> ShowS
elShowsPrec Int
6 f y
x
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
consS ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> (forall (x :: k). c x => Int -> f x -> ShowS)
-> Int
-> TypedList f ys
-> ShowS
forall k (c :: k -> Constraint) (f :: k -> *) (xs :: [k]).
All c xs =>
String
-> (forall (x :: k). c x => Int -> f x -> ShowS)
-> Int
-> TypedList f xs
-> ShowS
typedListShowsPrecC @c @f String
consS forall (x :: k). c x => Int -> f x -> ShowS
elShowsPrec Int
5 TypedList f ys
xs
typedListShowsPrec :: forall f xs
. ( forall x . Int -> f x -> ShowS )
-> Int -> TypedList f xs -> ShowS
typedListShowsPrec :: (forall (x :: k). Int -> f x -> ShowS)
-> Int -> TypedList f xs -> ShowS
typedListShowsPrec forall (x :: k). Int -> f x -> ShowS
_ Int
_ TypedList f xs
U = Char -> ShowS
showChar Char
'U'
typedListShowsPrec forall (x :: k). Int -> f x -> ShowS
elShowsPrec Int
p (f y
x :* TypedList f ys
xs) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
6) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
Int -> f y -> ShowS
forall (x :: k). Int -> f x -> ShowS
elShowsPrec Int
6 f y
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :* " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). Int -> f x -> ShowS)
-> Int -> TypedList f ys -> ShowS
forall k (f :: k -> *) (xs :: [k]).
(forall (x :: k). Int -> f x -> ShowS)
-> Int -> TypedList f xs -> ShowS
typedListShowsPrec @f forall (x :: k). Int -> f x -> ShowS
elShowsPrec Int
5 TypedList f ys
xs
typedListReadPrec :: forall c f xs g
. All c xs
=> String
-> ( forall x . c x => Read.ReadPrec (f x) )
-> TypedList g xs
-> Read.ReadPrec (TypedList f xs)
typedListReadPrec :: String
-> (forall (x :: k). c x => ReadPrec (f x))
-> TypedList g xs
-> ReadPrec (TypedList f xs)
typedListReadPrec String
_ forall (x :: k). c x => ReadPrec (f x)
_ TypedList g xs
U = ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs))
-> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)
forall a b. (a -> b) -> a -> b
$ TypedList f xs
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U TypedList f xs -> ReadPrec () -> ReadPrec (TypedList f xs)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
Read.lift (Lexeme -> ReadP ()
Read.expect (Lexeme -> ReadP ()) -> Lexeme -> ReadP ()
forall a b. (a -> b) -> a -> b
$ String -> Lexeme
Read.Ident String
"U")
typedListReadPrec String
consS forall (x :: k). c x => ReadPrec (f x)
elReadPrec (g y
_ :* TypedList g ys
ts) = ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs))
-> (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs))
-> ReadPrec (TypedList f xs)
-> ReadPrec (TypedList f xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)
forall a. Int -> ReadPrec a -> ReadPrec a
Read.prec Int
5 (ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs))
-> ReadPrec (TypedList f xs) -> ReadPrec (TypedList f xs)
forall a b. (a -> b) -> a -> b
$ do
f y
x <- ReadPrec (f y) -> ReadPrec (f y)
forall a. ReadPrec a -> ReadPrec a
Read.step ReadPrec (f y)
forall (x :: k). c x => ReadPrec (f x)
elReadPrec
ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
Read.lift (ReadP () -> ReadPrec ())
-> (Lexeme -> ReadP ()) -> Lexeme -> ReadPrec ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lexeme -> ReadP ()
Read.expect (Lexeme -> ReadPrec ()) -> Lexeme -> ReadPrec ()
forall a b. (a -> b) -> a -> b
$ String -> Lexeme
Read.Symbol String
consS
TypedList f ys
xs <- String
-> (forall (x :: k). c x => ReadPrec (f x))
-> TypedList g ys
-> ReadPrec (TypedList f ys)
forall k (c :: k -> Constraint) (f :: k -> *) (xs :: [k])
(g :: k -> *).
All c xs =>
String
-> (forall (x :: k). c x => ReadPrec (f x))
-> TypedList g xs
-> ReadPrec (TypedList f xs)
typedListReadPrec @c String
consS forall (x :: k). c x => ReadPrec (f x)
elReadPrec TypedList g ys
ts
TypedList f xs -> ReadPrec (TypedList f xs)
forall (m :: * -> *) a. Monad m => a -> m a
return (f y
x f y -> TypedList f ys -> TypedList f xs
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* TypedList f ys
xs)
withTypedListReadPrec :: forall f (r :: Type)
. (forall (z :: Type) .
( forall x . f x -> z) -> Read.ReadPrec z )
-> (forall xs . TypedList f xs -> r )
-> Read.ReadPrec r
withTypedListReadPrec :: (forall z. (forall (x :: k). f x -> z) -> ReadPrec z)
-> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r
withTypedListReadPrec forall z. (forall (x :: k). f x -> z) -> ReadPrec z
withElReadPrec forall (xs :: [k]). TypedList f xs -> r
use = ReadPrec r -> ReadPrec r
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec r -> ReadPrec r) -> ReadPrec r -> ReadPrec r
forall a b. (a -> b) -> a -> b
$
(TypedList f '[] -> r
forall (xs :: [k]). TypedList f xs -> r
use TypedList f '[]
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U r -> ReadPrec () -> ReadPrec r
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
Read.lift (Lexeme -> ReadP ()
Read.expect (Lexeme -> ReadP ()) -> Lexeme -> ReadP ()
forall a b. (a -> b) -> a -> b
$ String -> Lexeme
Read.Ident String
"U"))
ReadPrec r -> ReadPrec r -> ReadPrec r
forall a. ReadPrec a -> ReadPrec a -> ReadPrec a
Read.+++
Int -> ReadPrec r -> ReadPrec r
forall a. Int -> ReadPrec a -> ReadPrec a
Read.prec Int
5 (do
WithAnyTL forall (xs :: [k]). TypedList f xs -> r
withX <- ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r)
forall a. ReadPrec a -> ReadPrec a
Read.step (ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r))
-> ReadPrec (WithAnyTL f r) -> ReadPrec (WithAnyTL f r)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). f x -> WithAnyTL f r) -> ReadPrec (WithAnyTL f r)
forall z. (forall (x :: k). f x -> z) -> ReadPrec z
withElReadPrec (\f x
x -> (forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r
forall k (f :: k -> *) r.
(forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r
WithAnyTL ((forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r)
-> (forall (xs :: [k]). TypedList f xs -> r) -> WithAnyTL f r
forall a b. (a -> b) -> a -> b
$ TypedList f (x : xs) -> r
forall (xs :: [k]). TypedList f xs -> r
use (TypedList f (x : xs) -> r)
-> (TypedList f xs -> TypedList f (x : xs)) -> TypedList f xs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x
x f x -> TypedList f xs -> TypedList f (x : xs)
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:*))
ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
Read.lift (ReadP () -> ReadPrec ())
-> (Lexeme -> ReadP ()) -> Lexeme -> ReadPrec ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lexeme -> ReadP ()
Read.expect (Lexeme -> ReadPrec ()) -> Lexeme -> ReadPrec ()
forall a b. (a -> b) -> a -> b
$ String -> Lexeme
Read.Symbol String
":*"
(forall z. (forall (x :: k). f x -> z) -> ReadPrec z)
-> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r
forall k (f :: k -> *) r.
(forall z. (forall (x :: k). f x -> z) -> ReadPrec z)
-> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r
withTypedListReadPrec @f @r forall z. (forall (x :: k). f x -> z) -> ReadPrec z
withElReadPrec forall (xs :: [k]). TypedList f xs -> r
withX
)
newtype WithAnyTL (f :: k -> Type) (r :: Type)
= WithAnyTL (forall (xs :: [k]) . TypedList f xs -> r)
reifyRepList :: forall (k :: Type) (xs :: [k]) (r :: Type)
. TypeList xs
-> (RepresentableList xs => r)
-> r
reifyRepList :: TypeList xs -> (RepresentableList xs => r) -> r
reifyRepList TypeList xs
tl RepresentableList xs => r
k = MagicRepList xs r -> TypeList xs -> r
forall a b. a -> b
unsafeCoerce ((RepresentableList xs => r) -> MagicRepList xs r
forall k (xs :: [k]) r.
(RepresentableList xs => r) -> MagicRepList xs r
MagicRepList RepresentableList xs => r
k :: MagicRepList xs r) TypeList xs
tl
{-# INLINE reifyRepList #-}
newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r)
data PatReverse (f :: k -> Type) (xs :: [k])
= forall (sx :: [k]) . ReverseList xs sx => PatReverse (TypedList f sx)
unreverseTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatReverse f xs
unreverseTL :: TypedList f xs -> PatReverse f xs
unreverseTL TypedList f xs
xs
= case Dict (xs ~ Reverse (Reverse xs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @(Reverse (Reverse xs)) of
Dict (xs ~ Reverse (Reverse xs))
Dict -> TypedList f (Reverse xs) -> PatReverse f xs
forall k (f :: k -> *) (xs :: [k]) (sx :: [k]).
ReverseList xs sx =>
TypedList f sx -> PatReverse f xs
PatReverse @k @f @xs @(Reverse xs) (TypedList f xs -> TypedList f (Reverse xs)
forall k (f :: k -> *) (xs :: [k]).
TypedList f xs -> TypedList f (Reverse xs)
Numeric.TypedList.reverse TypedList f xs
xs)
{-# INLINE unreverseTL #-}
mkRTL :: forall (k :: Type) (xs :: [k])
. TypeList xs
-> Dict (RepresentableList xs)
mkRTL :: TypeList xs -> Dict (RepresentableList xs)
mkRTL TypeList xs
xs = TypeList xs
-> (RepresentableList xs => Dict (RepresentableList xs))
-> Dict (RepresentableList xs)
forall k (xs :: [k]) r.
TypeList xs -> (RepresentableList xs => r) -> r
reifyRepList TypeList xs
xs RepresentableList xs => Dict (RepresentableList xs)
forall (a :: Constraint). a => Dict a
Dict
{-# INLINE mkRTL #-}
data PatSnoc (f :: k -> Type) (xs :: [k]) where
PatSNil :: PatSnoc f '[]
PatSnoc :: SnocList xs s xss => TypedList f xs -> f s -> PatSnoc f xss
unsnocTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatSnoc f xs
unsnocTL :: TypedList f xs -> PatSnoc f xs
unsnocTL (TypedList [])
= case Dict (xs ~ '[])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @'[] of
Dict (xs ~ '[])
Dict -> PatSnoc f xs
forall k (f :: k -> *). PatSnoc f '[]
PatSNil
unsnocTL (TypedList (Any
x:[Any]
xs))
= case Dict (xs ~ (Init xs +: Last xs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @(Init xs +: Last xs) of
Dict (xs ~ (Init xs +: Last xs))
Dict -> TypedList f (Init xs) -> f (Last xs) -> PatSnoc f xs
forall k (xs :: [k]) (s :: k) (xss :: [k]) (f :: k -> *).
SnocList xs s xss =>
TypedList f xs -> f s -> PatSnoc f xss
PatSnoc ([Any] -> TypedList f (Init xs)
coerce [Any]
sy) (Any -> f (Last xs)
forall a b. a -> b
unsafeCoerce Any
y)
where
([Any]
sy, Any
y) = Any -> [Any] -> ([Any], Any)
unsnoc Any
x [Any]
xs
unsnoc :: Any -> [Any] -> ([Any], Any)
unsnoc :: Any -> [Any] -> ([Any], Any)
unsnoc Any
t [] = ([], Any
t)
unsnoc Any
t (Any
z:[Any]
zs) = ([Any] -> [Any]) -> ([Any], Any) -> ([Any], Any)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Any
tAny -> [Any] -> [Any]
forall a. a -> [a] -> [a]
:) (Any -> [Any] -> ([Any], Any)
unsnoc Any
z [Any]
zs)
{-# INLINE unsnocTL #-}
data PatCons (f :: k -> Type) (xs :: [k]) where
PatCNil :: PatCons f '[]
PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys)
patTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])
. TypedList f xs -> PatCons f xs
patTL :: TypedList f xs -> PatCons f xs
patTL (TypedList [])
= case Dict (xs ~ '[])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @'[] of
Dict (xs ~ '[])
Dict -> PatCons f xs
forall k (f :: k -> *). PatCons f '[]
PatCNil
patTL (TypedList (Any
x : [Any]
xs))
= case Dict (xs ~ (Head xs : Tail xs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @xs @(Head xs ': Tail xs) of
Dict (xs ~ (Head xs : Tail xs))
Dict -> f (Head xs)
-> TypedList f (Tail xs) -> PatCons f (Head xs : Tail xs)
forall a (f :: a -> *) (y :: a) (ys :: [a]).
f y -> TypedList f ys -> PatCons f (y : ys)
PatCons (Any -> f (Head xs)
forall a b. a -> b
unsafeCoerce Any
x) ([Any] -> TypedList f (Tail xs)
coerce [Any]
xs)
{-# INLINE patTL #-}
mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])
. DictList c xs -> Dict (All c xs, RepresentableList xs)
mkEVL :: DictList c xs -> Dict (All c xs, RepresentableList xs)
mkEVL DictList c xs
U = Dict (All c xs, RepresentableList xs)
forall (a :: Constraint). a => Dict a
Dict
mkEVL (Dict1 c y
Dict1 :* TypedList (Dict1 c) ys
evs) = case TypedList (Dict1 c) ys -> Dict (All c ys, RepresentableList ys)
forall k (c :: k -> Constraint) (xs :: [k]).
DictList c xs -> Dict (All c xs, RepresentableList xs)
mkEVL TypedList (Dict1 c) ys
evs of Dict (All c ys, RepresentableList ys)
Dict -> Dict (All c xs, RepresentableList xs)
forall (a :: Constraint). a => Dict a
Dict
_evList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) (f :: (k -> Type))
. All c xs => TypedList f xs -> DictList c xs
_evList :: TypedList f xs -> DictList c xs
_evList TypedList f xs
U = DictList c xs
forall k (f :: k -> *) (xs :: [k]). (xs ~ '[]) => TypedList f xs
U
_evList (f y
_ :* TypedList f ys
xs) = case TypedList f ys -> DictList c ys
forall k (c :: k -> Constraint) (xs :: [k]) (f :: k -> *).
All c xs =>
TypedList f xs -> DictList c xs
_evList TypedList f ys
xs of DictList c ys
evs -> Dict1 c y
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1 Dict1 c y -> DictList c ys -> DictList c xs
forall k (f :: k -> *) (xs :: [k]) (y :: k) (ys :: [k]).
(xs ~ (y : ys)) =>
f y -> TypedList f ys -> TypedList f xs
:* DictList c ys
evs
dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int
dimValInt :: Dim x -> Int
dimValInt = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> (Dim x -> Word) -> Dim x -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim x -> Word
forall k (x :: k). Dim x -> Word
dimVal