{-# 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
-- Copyright   :  (c) Artem Chirkin
-- License     :  BSD3
--
--
-- Provide a type-indexed heterogeneous list type @TypedList@.
-- Behind the facade, @TypedList@ is just a plain list of haskell pointers.
-- It is used to represent dimension lists, indices, and just flexible tuples.
--
-- Most of type-level functionality is implemented using GADT-like pattern synonyms.
-- Import this module qualified to use list-like functionality.
--
-----------------------------------------------------------------------------
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
      -- * Deriving Show and Read
    , 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)

-- | Type-indexed list
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 #-}

-- | Term-level structure of a @TypedList f xs@ is fully determined by its
--   type @Typeable xs@.
--   Thus, @gunfold@ does not use its last argument (@Constr@) at all,
--   relying on the structure of the type parameter.
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

-- | A list of type proxies
type TypeList = (TypedList Proxy :: [k] -> Type)

-- | Same as `Dict`, but allows to separate constraint function from
--   the type it is applied to.
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))


-- | A list of dicts for the same constraint over several types.
type DictList (c :: k -> Constraint)
  = (TypedList (Dict1 c) :: [k] -> Type)


-- | Pattern matching against this causes `RepresentableList` instance
--   come into scope.
--   Also it allows constructing a term-level list out of a constraint.
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 matching against this allows manipulating lists of constraints.
--   Useful when creating functions that change the shape of dimensions.
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)

-- | Zero-length type list
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])

-- | Zero-length type list; synonym to `U`.
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

-- | Constructing a type-indexed list
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 :*

-- | Constructing a type-indexed list in the canonical way
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

-- | Constructing a type-indexed list from the other end
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

-- | Reverse a typed list
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

-- | /O(1)/ append an element in front of a @TypedList@ (same as `(:)` for lists).
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 #-}

-- | /O(n)/ append an element to the end of a @TypedList@.
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 #-}

-- | /O(n)/ return elements of a @TypedList@ in reverse order.
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 #-}

-- | /O(1)/ Extract the first element of a @TypedList@, which must be non-empty.
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 #-}

-- | /O(1)/ Extract the elements after the head of a @TypedList@,
--   which must be non-empty.
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 #-}

-- | /O(n)/ Return all the elements of a @TypedList@ except the last one
--   (the list must be non-empty).
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 #-}

-- | /O(n)/ Extract the last element of a @TypedList@, which must be non-empty.
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 #-}

-- | /O(min(n,k))/ @take k xs@ returns a prefix of @xs@ of length @min(length xs, k)@.
--   It calls `Prelude.take` under the hood, so expect the same behavior.
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 #-}

-- | /O(min(n,k))/ @drop k xs@ returns a suffix of @xs@ of length @max(0, length xs - k)@.
--   It calls `Prelude.drop` under the hood, so expect the same behavior.
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 #-}

-- | Return the number of elements in a @TypedList@ (same as `order`).
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 #-}


-- | /O(min(n,k))/ @splitAt k xs@ has the same effect as @('take' k xs, 'drop' k xs)@.
--   It calls `Prelude.splitAt` under the hood, so expect the same behavior.
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 #-}


-- | Return the number of elements in a type list @xs@ bound by a constraint
--   @RepresentableList xs@ (same as `order`, but takes no value arguments).
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' #-}

-- | Return the number of elements in a @TypedList@ (same as `length`).
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 two @TypedList@s.
--   It calls `Prelude.(++)` under the hood, so expect the same behavior.
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 #-}

-- | Drops the given prefix from a @TypedList@.
--   It returns 'Nothing' if the @TypedList@ does not start with the prefix
--   given, or 'Just' the @TypedList@ after the prefix, if it does.
--   It calls `Prelude.stripPrefix` under the hood, so expect the same behavior.
--
--   This function can be used to find the type-level evidence that one type-level
--   list is indeed a prefix of another.
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 #-}

-- | Drops the given suffix from a @TypedList@.
--   It returns 'Nothing' if the @TypedList@ does not end with the suffix
--   given, or 'Just' the @TypedList@ before the suffix, if it does.
--
--   This function can be used to find the type-level evidence that one type-level
--   list is indeed a suffix of another.
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 #-}

-- | Returns two things at once:
--   (Evidence that types of lists match, value-level equality).
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 a function over contents of a typed list
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 #-}

-- | Get a constructible `TypeList` from any other `TypedList`;
--   Pattern matching agains the result brings `RepresentableList` constraint
--   into the scope:
--
--   > case types ts of TypeList -> ...
--
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 #-}

-- | Construct a @TypeList xs@ if there is an instance of @Typeable xs@ around.
--
--   This way, you can always bring `RepresentableList` instance into the scope
--   if you have a `Typeable` instance.
--
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 #-}

-- | If all elements of a @TypedList@ are @Typeable@,
--   then the list of these elements is also @Typeable@.
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

-- | Representable type lists.
--   Allows getting type information about list structure at runtime.
class RepresentableList xs where
  -- | Get type-level constructed list
  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

-- | Generic show function for a @TypedList@.
typedListShowsPrecC :: forall c f xs
                     . All c xs
                    => String
                       -- ^ Override cons symbol
                    -> ( forall x . c x => Int -> f x -> ShowS )
                       -- ^ How to show a single element
                    -> 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

-- | Generic show function for a @TypedList@.
typedListShowsPrec :: forall f xs
                    . ( forall x . Int -> f x -> ShowS )
                      -- ^ How to show a single element
                   -> 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

-- | Generic read function for a @TypedList@.
--   Requires a "template" to enforce the structure of the type list.
typedListReadPrec :: forall c f xs g
                   . All c xs
                  => String
                     -- ^ Override cons symbol
                  -> ( forall x . c x => Read.ReadPrec (f x) )
                     -- ^ How to read a single element
                  -> TypedList g xs
                     -- ^ Enforce the type structure of the result
                  -> 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)

-- | Generic read function for a @TypedList@ of unknown length.
withTypedListReadPrec :: forall f (r :: Type)
                       . (forall (z :: Type) .
                            ( forall x . f x -> z) -> Read.ReadPrec z )
                         -- ^ How to read a single element
                      -> (forall xs . TypedList f xs -> r )
                         -- ^ Consume the result
                      -> 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
    )

-- Workaround impredicative polymorphism
newtype WithAnyTL (f :: k -> Type) (r :: Type)
  = WithAnyTL (forall (xs :: [k]) . TypedList f xs -> r)

--------------------------------------------------------------------------------
-- internal
--------------------------------------------------------------------------------


-- | This function does GHC's magic to convert user-supplied `tList` function
--   to create an instance of `RepresentableList` typeclass at runtime.
--   The trick is taken from Edward Kmett's reflection library explained
--   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection
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