dimensions 1.0.1.1 → 2.0.0.0

raw patch · 24 files changed

+2913/−2568 lines, 24 filesdep +constraints-derivingdep +ghcdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: constraints-deriving, ghc

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• dimensions.cabal +66/−57
• src/Data/Type/List.hs +232/−0
• src/Data/Type/List/InjectiveSnoc.hs +67/−0
• src/Data/Type/List/Internal.hs +27/−0
• src/Data/Type/Lits.hs +115/−0
• src/Numeric/Dim.hs +0/−446
• src/Numeric/Dimensions.hs +13/−17
• src/Numeric/Dimensions/Dim.hs +1084/−0
• src/Numeric/Dimensions/Dim.hs-boot +13/−0
• src/Numeric/Dimensions/Dims.hs +0/−440
• src/Numeric/Dimensions/Fold.hs +0/−334
• src/Numeric/Dimensions/Idx.hs +483/−0
• src/Numeric/Dimensions/Idxs.hs +0/−427
• src/Numeric/Tuple.hs +3/−10
• src/Numeric/Tuple/Lazy.hs +59/−132
• src/Numeric/Tuple/Strict.hs +60/−133
• src/Numeric/Type/Evidence.hs +0/−59
• src/Numeric/Type/List.hs +0/−222
• src/Numeric/TypedList.hs +357/−129
• test/Numeric/DimTest.hs +0/−86
• test/Numeric/Dimensions/DimTest.hs +159/−0
• test/Numeric/Dimensions/DimsTest.hs +0/−67
• test/Numeric/Dimensions/IdxTest.hs +165/−0
• test/Spec.hs +10/−9

@@ -1,65 +1,74 @@-name: dimensions-version: 1.0.1.1-cabal-version: >=1.22-build-type: Simple-license: BSD3-license-file: LICENSE-copyright: (c) Artem Chirkin-maintainer: chirkin@arch.ethz.ch-homepage: https://github.com/achirkin/easytensor#readme-synopsis: Safe type-level dimensionality for multidimensional data.-description:-    Safe type-level dimensionality for multidimensional data.-category: Math, Geometry-author: Artem Chirkin+cabal-version: 1.12 -source-repository head-    type: git-    location: https://github.com/achirkin/easytensor.git-    subdir: dimensions+-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: 982b8bf6393fdd487b646f7c7a3b258acba9501a6d106861757a3b4a49f3de82 +name:           dimensions+version:        2.0.0.0+synopsis:       Safe type-level dimensionality for multidimensional data.+description:    Safe type-level dimensionality for multidimensional data. Please see the README on GitHub at <https://github.com/achirkin/easytensor#readme>+category:       math, geometry+homepage:       https://github.com/achirkin/easytensor#readme+bug-reports:    https://github.com/achirkin/easytensor/issues+author:         Artem Chirkin+maintainer:     achirkin@users.noreply.github.com+copyright:      Copyright: (c) 2019 Artem Chirkin+license:        BSD3+license-file:   LICENSE+build-type:     Simple -flag unsafeindices-    description:-        Disable bound checks on Idx and Idxs types.-    default: False+source-repository head+  type: git+  location: https://github.com/achirkin/easytensor+  subdir: dimensions +flag unsafeindices+  description: Disable bound checks on Idx and Idxs types.+  manual: True+  default: False  library--    if flag(unsafeindices)-        cpp-options: -DUNSAFE_INDICES-    exposed-modules:-        Numeric.Dim-        Numeric.Tuple-        Numeric.Tuple.Lazy-        Numeric.Tuple.Strict-        Numeric.Type.Evidence-        Numeric.Type.List-        Numeric.TypedList-        Numeric.Dimensions-        Numeric.Dimensions.Dims-        Numeric.Dimensions.Idxs-        Numeric.Dimensions.Fold-    build-depends:-        base >=4.9 && <5-    default-language: Haskell2010-    hs-source-dirs: src-    ghc-options: -Wall-+  exposed-modules:+      Data.Type.List+      Data.Type.Lits+      Numeric.Dimensions+      Numeric.Dimensions.Dim+      Numeric.Dimensions.Idx+      Numeric.Tuple+      Numeric.Tuple.Lazy+      Numeric.Tuple.Strict+      Numeric.TypedList+  other-modules:+      Data.Type.List.InjectiveSnoc+      Data.Type.List.Internal+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Wtabs -Wmissing-local-signatures -Wmissing-home-modules -Widentities+  build-depends:+      base >=4.10 && <5+    , constraints-deriving >=1 && <2+    , ghc+  if flag(unsafeindices)+    cpp-options: -DUNSAFE_INDICES+  default-language: Haskell2010  test-suite dimensions-test--    type: exitcode-stdio-1.0-    main-is: Spec.hs-    other-modules:-        Numeric.DimTest-        Numeric.Dimensions.DimsTest-    build-depends:-        base -any,-        Cabal -any,-        QuickCheck -any,-        dimensions -any-    default-language: Haskell2010-    hs-source-dirs: test-    ghc-options: -Wall+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Numeric.Dimensions.DimTest+      Numeric.Dimensions.IdxTest+      Paths_dimensions+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Wtabs -Wmissing-local-signatures -Wmissing-home-modules -Widentities+  build-depends:+      Cabal+    , QuickCheck+    , base+    , constraints-deriving >=1 && <2+    , dimensions+  default-language: Haskell2010

@@ -0,0 +1,232 @@+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.List+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Provides type-level operations on lists.+--+--+--------------------------------------------------------------------------------++module Data.Type.List+  ( -- * Basic operations+    type (++), type (+:), type (:+)+  , Empty, Cons, Snoc, Head+  , Tail, Last, Init, Concat+  , StripPrefix, StripSuffix+  , Reverse, Take, Drop, Length+    -- * Operations on elements+  , All, Map, Elem+    -- * Concatenation and its evidence+  , ConcatList, evStripSuffix, evStripPrefix, evConcat+    -- * Data.Typeable+  , inferTypeableCons+  ) where++import Data.Constraint         ((:-) (..), Constraint, Dict (..))+import Data.Type.List.Internal (Snoc)+import Data.Type.Lits+import GHC.Base                (Type)+import Type.Reflection+import Unsafe.Coerce           (unsafeCoerce)++-- | Empty list, same as @'[]@.+type Empty = '[]++-- | Appending a list, represents an @Op@ counterpart of @(':)@.+type Cons (a :: k) (as :: [k])+    = a ': as++-- | Extract the first element of a list, which must be non-empty.+type family Head (xs :: [k]) :: k where+    Head ('[] :: [k]) = TypeError ( ListError k "Head: empty type-level list." )+    Head (x ': _)     = x++-- | Extract the elements after the head of a list, which must be non-empty.+type family Tail (xs :: [k]) :: [k] where+    Tail ('[] :: [k]) = TypeError ( ListError k "Tail: empty type-level list." )+    Tail (_ ': xs)    = xs++-- | Extract the last element of a list, which must be non-empty.+type family Last (xs :: [k]) :: k where+    Last ('[] :: [k]) = TypeError ( ListError k "Last: empty type-level list." )+    Last '[x]         = x+    Last (_ ': xs)    = Last xs++-- | Extract all but last elements of a list, which must be non-empty.+type family Init (xs :: [k]) :: [k] where+    Init ('[] :: [k]) = TypeError ( ListError k "Init: empty type-level list." )+    Init '[x]         = '[]+    Init (x ': xs)    = x ': Init xs++-- | @Take n xs@ returns the prefix of a list of length @max n (length xs)@.+type family Take (n :: Nat) (xs :: [k]) :: [k] where+    Take 0  _        = '[]+    Take n (x ': xs) = x ': Take (n - 1) xs+    Take _ '[]       = '[]++-- | @Drop n xs@ drops up to @n@ elements of @xs@.+type family Drop (n :: Nat) (xs :: [k]) :: [k] where+    Drop 0  xs       = xs+    Drop n (_ ': xs) = Drop (n - 1) xs+    Drop _ '[]       = '[]++-- | Append two lists.+type family Concat (as :: [k]) (bs :: [k]) :: [k] where+    Concat '[]        bs       = bs+    Concat  as       '[]       = as+    Concat (a ': as)  bs       = a ': Concat as bs++-- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise.+type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where+    StripPrefix  as        as         = '[]+    StripPrefix '[]        asbs       = asbs+    StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs+    StripPrefix (a ': as) (b ': asbs)+      = TypeError+        ( 'Text "StripPrefix: the first argument is not a prefix of the second."+        ':$$:+          'Text "Failed prefix: " ':<>: 'ShowType (a ': as)+        ':$$:+          'Text "Second argument: " ':<>: 'ShowType (b ': asbs)+        )+    StripPrefix (a ': as) '[]+      = TypeError+        ( 'Text "StripPrefix: the first argument is longer than the second."+        ':$$:+          'Text "Failed prefix: " ':<>: 'ShowType (a ': as)+        ':$$:+          'Text "The reduced second argument is empty."+        )++-- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise.+type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where+    StripSuffix  bs        bs         = '[]+    StripSuffix '[]        asbs       = asbs+    StripSuffix (a ': bs) (b ': bs)+      = TypeError+        ( 'Text "StripSuffix: the first argument is not a suffix of the second."+        ':$$:+          'Text "Failed match: "+            ':<>: 'ShowType ((a ': bs) ~ (b ': bs))+        )+    StripSuffix (b ': bs) '[]+      = TypeError+        ( 'Text "StripSuffix: the first argument is longer than the second."+        ':$$:+          'Text "Failed suffix: " ':<>: 'ShowType (b ': bs)+        ':$$:+          'Text "The reduced second argument is empty."+        )+    StripSuffix  bs       (a ': asbs) = a ': StripSuffix bs asbs++-- | Returns the elements of a list in reverse order.+type family Reverse (xs :: [k]) :: [k] where+    -- Note: the goal is not to write a fast implementation,+    --       but make it easier for the type checker to simplify things.+    --       This is only going to be executed during compile time,+    --       so there is no real performance impact.+    Reverse '[] = '[]+    Reverse (x ': xs) = Snoc (Reverse xs) x++-- | Number of elements in a list.+type family Length (xs :: [k]) :: Nat where+    Length '[]       = 0+    Length (x ': xs) = Length xs + 1++-- | Synonym for a type-level @Cons@.+type (a :: k) :+ (as :: [k]) = a ': as+infixr 5 :+++-- | Synonym for a type-level @Snoc@.+type (ns :: [k]) +: (n :: k) = Snoc ns n+infixl 6 +:++-- | Infix-style synonym for concatenation+type (as :: [k]) ++ (bs :: [k]) = Concat as bs+infixr 5 ++++-- | All elements of a type list must satisfy the same constraint.+type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where+    All _ '[]       = ()+    All f (x ': xs) = (f x, All f xs)++-- | Map a functor over the elements of a type list.+type family Map (f :: a -> b) (xs :: [a]) :: [b] where+    Map f '[]       = '[]+    Map f (x ': xs) = f x ': Map f xs++-- | Check if an item is a member of a list.+type family Elem (x :: k) (xs :: [k]) :: Constraint where+    Elem x (x ': xs) = ()+    Elem x (_ ': xs) = Elem x xs++type ListError k t+    = 'Text t ':$$:+    ( 'Text "Type-level error occured when operating on a list of kind "+      ':<>: 'ShowType [k] ':<>: 'Text "."+    )++-- | Represent a triple of lists forming a relation @(as ++ bs) ~ asbs@+type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) =+    ( asbs ~ Concat as bs+    , as   ~ StripSuffix bs asbs+    , bs   ~ StripPrefix as asbs+    )++-- | Derive @ConcatList@ given @Concat@+evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+          . (asbs ~ Concat as bs) :- ConcatList as bs asbs+evConcat = Sub $ unsafeCoerce+  ( Dict :: Dict+    ( asbs ~ Concat as bs+    , as   ~ as+    , bs   ~ bs+    )+  )++-- | Derive @ConcatList@ given @StripSuffix@+evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+               . (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs+evStripSuffix = Sub $ unsafeCoerce+  ( Dict :: Dict+    ( asbs ~ asbs+    , as   ~ StripSuffix bs asbs+    , bs   ~ bs+    )+  )++-- | Derive @ConcatList@ given @StripPrefix@+evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+               . (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs+evStripPrefix = Sub $ unsafeCoerce+  ( Dict :: Dict+    ( asbs ~ asbs+    , as   ~ as+    , bs   ~ StripPrefix as asbs+    )+  )++-- | Given a @Typeable@ list, infer this constraint for its parts.+inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k])+                   . (Typeable ys, ys ~ (x ': xs))+                  => Dict (Typeable x, Typeable xs)+inferTypeableCons = case typeRep @ys of+  App _ xRep `App` xsRep+    -> case ( withTypeable xRep  (Dict @(Typeable x))+            , withTypeable xsRep (Dict @(Typeable xs))+            ) of+        (Dict, Dict) -> Dict

@@ -0,0 +1,67 @@+{-# OPTIONS_GHC -fobject-code   #-}+{-# OPTIONS_HADDOCK hide, prune #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.List.InjectiveSnoc+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- A small core plugin to make GHC think that @Snoc@ is injective+--+--+--------------------------------------------------------------------------------+module Data.Type.List.InjectiveSnoc ( plugin ) where+++import           CoAxiom    (CoAxBranch (..), CoAxiom (..), mapAccumBranches)+import           Data.Maybe (fromMaybe)+import           GhcPlugins++-- NB: check out+--  https://github.com/ghc/ghc/blob/bf73419518ca550e85188616f860961c7e2a336b/compiler/typecheck/TcTypeNats.hs+--  for further ideas.+--  Maybe, I can use BuiltInSynFamily to do a lot of super cool stuff!++-- | A small core plugin to make GHC think that @Snoc@ is injective+plugin :: Plugin+plugin = defaultPlugin+  { installCoreToDos =+      const $ pure . (CoreDoPluginPass "InjectiveSnoc" injectiveSnocPass :)+  }++injectiveSnocPass :: ModGuts -> CoreM ModGuts+injectiveSnocPass = pure . modSnocFam updateSnocFam++modSnocFam :: (TyCon -> TyCon) -> ModGuts -> ModGuts+modSnocFam f guts = guts {mg_tcs = map g (mg_tcs guts)}+  where+    g tc+      | nameOccName (tyConName tc) == mkTcOcc "Snoc" = f tc+      | otherwise = tc++updateSnocFam :: TyCon -> TyCon+updateSnocFam tc = fromMaybe tc $ do+    axiom <- isClosedSynFamilyTyConWithAxiom_maybe tc+    let newAxiom = axiom+          { co_ax_tc = newTc+          , co_ax_branches = mapAccumBranches f (co_ax_branches axiom)+          }+        f _ b = b { cab_rhs = repTc (cab_rhs b) }+        repTc t = case splitTyConApp_maybe t of+          Just (c, ts)+            | nameOccName (tyConName c) == mkTcOcc "Snoc"+              -> mkTyConApp newTc $ map repTc ts+            | otherwise+              -> mkTyConApp c $ map repTc ts+          Nothing+              -> t+        newTc = mkFamilyTyCon+          (tyConName tc)    -- Name+          (tyConBinders tc)   -- [TyConBinder]+          (tyConResKind tc) -- Kind+          (famTcResVar tc)  -- Maybe Name+          (ClosedSynFamilyTyCon (Just newAxiom)) -- FamTyConFlav+          (tyConAssoc_maybe tc)  -- Maybe Class+          -- Injectivity copied from a dummy injective TF with the same head+          (Injective [True, True, True])     -- Injectivity+    return newTc

@@ -0,0 +1,27 @@+{-# OPTIONS_GHC -fobject-code       #-}+{-# OPTIONS_GHC -fplugin Data.Type.List.InjectiveSnoc #-}+{-# OPTIONS_HADDOCK hide, prune     #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators          #-}++{-# LANGUAGE TypeInType             #-}+{-# LANGUAGE UndecidableInstances   #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.List.Internal+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- Thanks to @Data.Type.List.InjectiveSnoc@, @Snoc@ appears to be injective+-- for an oustide viewer.+--+--+--------------------------------------------------------------------------------+module Data.Type.List.Internal ( Snoc ) where++-- | Appending a list on the other side.+type family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where+    Snoc (x ': xs) y = x ': Snoc xs y+    Snoc '[]       y = '[y]

@@ -0,0 +1,115 @@+{-# LANGUAGE CPP                  #-}+{-# LANGUAGE ConstraintKinds      #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE ExplicitForAll       #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+#if __GLASGOW_HASKELL__ >= 806+{-# LANGUAGE NoStarIsType         #-}+#endif+++{-# LANGUAGE FlexibleContexts     #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.List+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- A Mixture of `GHC.TypeLits` and  `GHC.TypeNats` with @Nat@s represented as+-- @Natural@ at runtime, plus some helper functions of our own.+--+--------------------------------------------------------------------------------++module Data.Type.Lits+  ( -- * Kinds+    TN.Nat, TL.Symbol+    -- * Linking type and value level+  , TN.KnownNat, TN.natVal, TN.natVal'+  , TL.KnownSymbol, TL.symbolVal, TL.symbolVal'+  , TN.SomeNat(..), TL.SomeSymbol(..)+  , TN.someNatVal, TL.someSymbolVal+  , TN.sameNat, TL.sameSymbol+    -- * Functions on type literals+  , type (+), type (*), type (^), type (-)+  , type TN.Div, type TN.Mod, type TN.Log2+  , TL.AppendSymbol, ShowNat+  , TN.CmpNat, TL.CmpSymbol, type (<=)+  , SOrdering (..), cmpNat, cmpSymbol+    -- * User-defined type errors+  , TL.TypeError+  , TL.ErrorMessage(..)+  ) where+++import           Data.Kind     (Constraint, Type)+import qualified GHC.TypeLits  as TL+import           GHC.TypeNats  (type (*), type (+), type (-), type (^))+import qualified GHC.TypeNats  as TN+import           Unsafe.Coerce (unsafeCoerce)+++++-- | Convert a type-level @Nat@ into a type-level @Symbol@.+type family ShowNat (n :: TN.Nat) :: TL.Symbol where+    -- lol+    ShowNat 0 = "0"+    ShowNat 1 = "1"+    ShowNat 2 = "2"+    ShowNat 3 = "3"+    ShowNat 4 = "4"+    ShowNat 5 = "5"+    ShowNat 6 = "6"+    ShowNat 7 = "7"+    ShowNat 8 = "8"+    ShowNat 9 = "9"+    ShowNat d = TL.AppendSymbol (ShowNat (TN.Div d 10)) (ShowNat (TN.Mod d 10))+++-- | Singleton-style version of `Ordering`.+--   Pattern-match againts its constructor to witness the result of+--   type-level comparison.+data SOrdering :: Ordering -> Type where+    SLT :: SOrdering 'LT+    SEQ :: SOrdering 'EQ+    SGT :: SOrdering 'GT++-- | Pattern-match against the result of this function to get the evidence+--   of comparing type-level Nats.+cmpNat :: forall (a :: TN.Nat) (b :: TN.Nat) (proxy :: TN.Nat -> Type)+        . (TN.KnownNat a, TN.KnownNat b)+       => proxy a -> proxy b -> SOrdering (TN.CmpNat a b)+cmpNat a b+  = case compare (TN.natVal a) (TN.natVal b) of+    LT -> unsafeCoerce SLT+    EQ -> unsafeCoerce SEQ+    GT -> unsafeCoerce SGT+{-# INLINE cmpNat #-}++-- | Pattern-match against the result of this function to get the evidence+--   of comparing type-level Symbols.+cmpSymbol :: forall (a :: TL.Symbol) (b :: TL.Symbol) (proxy :: TL.Symbol -> Type)+           . (TL.KnownSymbol a, TL.KnownSymbol b)+          => proxy a -> proxy b -> SOrdering (TL.CmpSymbol a b)+cmpSymbol a b+  = case compare (TL.symbolVal a) (TL.symbolVal b) of+    LT -> unsafeCoerce SLT+    EQ -> unsafeCoerce SEQ+    GT -> unsafeCoerce SGT+{-# INLINE cmpSymbol #-}++-- | Comparison of type-level naturals, as a constraint.+type (<=) (a :: TN.Nat) (b :: TN.Nat) = LE a b (TN.CmpNat a b)++type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: Constraint where+    LE _ _ 'LT = ()+    LE _ _ 'EQ = ()+    LE a b 'GT = TL.TypeError+      ('TL.Text "Cannot deduce type-level Nat relation: "+          'TL.:<>: 'TL.ShowType a+          'TL.:<>: 'TL.Text " <= "+          'TL.:<>: 'TL.ShowType b+      )

@@ -1,446 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes   #-}-{-# LANGUAGE CPP                   #-}-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE ExplicitNamespaces    #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE KindSignatures        #-}-{-# LANGUAGE MagicHash             #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PatternSynonyms       #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE Rank2Types            #-}-{-# LANGUAGE RoleAnnotations       #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE Strict                #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE UndecidableInstances  #-}-{-# LANGUAGE ViewPatterns          #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dim--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ This module is based on `GHC.TypeLits` and re-exports its functionality.--- It provides `KnownDim` class that is similar to `KnownNat`, but keeps--- `Word`s instead of `Integer`s;--- Also it provides `Dim` data type serving as a singleton--- suitable for recovering an instance of the `KnownDim` class.--- A set of utility functions provide inference functionality, so--- that `KnownDim` can be preserved over some type-level operations.----------------------------------------------------------------------------------module Numeric.Dim-  ( -- * Type level numbers that can be unknown.-    XNat (..), XN, N, XNatType (..)-    -- * Term level dimension-  , Dim (Dim, D, Dn, Dx), SomeDim-  , KnownDim (..), KnownXNatType (..)-  , dimVal, dimVal', someDimVal-  , sameDim, sameDim'-  , compareDim, compareDim'-  , constrain, constrainBy, relax-    -- * Simple Dim arithmetics-    ---    --   The functions below create singleton values that work as a witness-    --   of `KnownDim` instance for type-level Nat operations.-    --   For example, to show that @(a + b)@ is a @KnownDim@, one writes:-    ---    --   > case plusDim dA dB of-    --   >   D -> ... -- here we know KnownDim ( a + b )-    ---    --   There is a bug and a feature in these functions though:-    --   they are implemented in terms of @Num Word@, which means that-    --   their results are subject to integer overflow.-    --   The good side is the confidence that they behave exactly as-    --   their @Word@ counterparts.-  , plusDim, minusDim, minusDimM, timesDim, powerDim-    -- * Re-export part of `GHC.TypeLits` for convenience-  , TL.Nat, TL.CmpNat, type (TL.+), type (TL.-), type (TL.*), type (TL.^)-  , MinDim, FixedDim, inferDimLE-    -- * Inferring kind of type-level dimension-  , KnownDimKind (..), DimKind (..)-  ) where---import           Data.Type.Bool-import           Data.Type.Equality-import           GHC.Base           (Type)-import           GHC.Exts           (Constraint, Proxy#, proxy#, unsafeCoerce#)-import           GHC.TypeLits       as TL--import           Numeric.Type.Evidence----- | Either known or unknown at compile-time natural number-data XNat = XN Nat | N Nat--- | Unknown natural number, known to be not smaller than the given Nat-type XN (n::Nat) = 'XN n--- | Known natural number-type N (n::Nat) = 'N n---- | Find out whether @XNat@ is of known or constrained type.-data XNatType :: XNat -> Type where-  -- | Given @XNat@ is known-  Nt  :: XNatType ('N n)-  -- | Given @XNat@ is constrained unknown-  XNt :: XNatType ('XN m)---- | Same as `SomeNat`-type SomeDim = Dim ('XN 0)---- | Singleton type to store type-level dimension value.------   On the one hand, it can be used to let type-inference system know---   relations between type-level naturals.---   On the other hand, this is just a newtype wrapper on the @Word@ type.------   Usually, the type parameter of @Dim@ is either @Nat@ or @XNat@.---   If dimensionality of your data is known in advance, use @Nat@;---   if you know the size of some dimensions, but do not know the size---   of others, use @XNat@s to represent them.-newtype Dim (x :: k) = DimSing Word--- Starting from GHC 8.2, compiler supports specifying lists of complete--- pattern synonyms.-#if __GLASGOW_HASKELL__ >= 802-{-# COMPLETE D #-}-{-# COMPLETE Dn, Dx #-}-{-# COMPLETE Dim #-}-#endif----- | Independently of the kind of type-level number,---   construct an instance of `KnownDim` from it.------   Match against this pattern to bring `KnownDim` instance into scope---   when you don't know the kind of the @Dim@ parameter.-pattern Dim :: forall (n :: k) . () => KnownDim n => Dim n-pattern Dim <- (dimEv -> E)-  where-    Dim = dim @_ @n----- | Same as @Dim@ pattern, but constrained to @Nat@ kind.-pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n-pattern D <- (dimEv -> E)-  where-    D = dim @_ @n---- | Statically known `XNat`-pattern Dn :: forall (xn :: XNat) . KnownXNatType xn-           => forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn-pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k)-  where-    Dn k = unsafeCoerce# k---- | `XNat` that is unknown at compile time.---   Same as `SomeNat`, but for a dimension:---   Hide dimension size inside, but allow specifying its minimum possible value.-pattern Dx :: forall (xn :: XNat) . KnownXNatType xn-           => forall (n :: Nat) (m :: Nat)-            . (KnownDim n, MinDim m n, xn ~ 'XN m) => Dim n -> Dim xn-pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)-  where-    Dx k = unsafeCoerce# k---- | This class provides the `Dim` associated with a type-level natural.-class KnownDim (n :: k) where-    -- | Get value of type-level dim at runtime.-    ---    --   Note, this function is supposed to be used with @TypeApplications@,-    --   and the @KnownDim@ class has varying kind of the parameter;-    --   thus, the function has two type paremeters (kind and type of @n@).-    --   For example, you can type:-    ---    --   >>>:set -XTypeApplications-    --   >>>:set -XDataKinds-    --   >>>:t dim @Nat @3-    --   dim @Nat @3 :: Dim 3-    ---    --   >>>:set -XTypeOperators-    --   >>>:t dim @_ @(13 - 6)-    --   dim @_ @(13 - 6) :: Dim 7-    ---    ---    --   >>>:t dim @_ @(N 17)-    --   dim @_ @(N 17) :: Dim (N 17)-    ---    dim :: Dim n----- | Find out the type of `XNat` constructor-class KnownXNatType (n :: XNat) where-  -- | Pattern-match against this to out the type of `XNat` constructor-  xNatType :: XNatType n--instance KnownXNatType ('N n) where-  xNatType = Nt-  {-# INLINE xNatType #-}--instance KnownXNatType ('XN n) where-  xNatType = XNt-  {-# INLINE xNatType #-}----- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`.-dimVal :: Dim (x :: k) -> Word-dimVal = unsafeCoerce#-{-# INLINE dimVal #-}---- | Similar to `natVal` from `GHC.TypeLits`, but returns `Word`.-dimVal' :: forall n . KnownDim n => Word-dimVal' = unsafeCoerce# (dim @_ @n)-{-# INLINE dimVal' #-}---- | Friendly error message if `m <= n` constraint is not satisfied.---   Use this type family instead of @(<=)@ if possible---   or try `inferDimLE` function as the last resort.-type family MinDim (m :: Nat) (n :: Nat) :: Constraint where-  MinDim m n =-    If (CmpNat m n == 'GT)-       (TypeError-         ('Text "Minimum Dim size constraint ("-            ':<>: 'ShowType m-            ':<>: 'Text " <= "-            ':<>: 'ShowType n-            ':<>: 'Text ") is not satisfied."-         ':$$: 'Text "Minimum Dim: " ':<>: 'ShowType m-         ':$$: 'Text " Actual Dim: " ':<>: 'ShowType n-         ) :: Constraint-       )-       (m <= n)---- | Constraints given by an XNat type on possible values of a Nat hidden inside.-type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where-  FixedDim ('N a)  b = a ~ b-  FixedDim ('XN m) b = MinDim m b--instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where-    {-# INLINE dim #-}-    dim = DimSing (fromInteger (natVal' (proxy# :: Proxy# n)))--instance {-# OVERLAPPING #-} KnownDim 0  where-  { {-# INLINE dim #-}; dim = DimSing 0 }-instance {-# OVERLAPPING #-} KnownDim 1  where-  { {-# INLINE dim #-}; dim = DimSing 1 }-instance {-# OVERLAPPING #-} KnownDim 2  where-  { {-# INLINE dim #-}; dim = DimSing 2 }-instance {-# OVERLAPPING #-} KnownDim 3  where-  { {-# INLINE dim #-}; dim = DimSing 3 }-instance {-# OVERLAPPING #-} KnownDim 4  where-  { {-# INLINE dim #-}; dim = DimSing 4 }-instance {-# OVERLAPPING #-} KnownDim 5  where-  { {-# INLINE dim #-}; dim = DimSing 5 }-instance {-# OVERLAPPING #-} KnownDim 6  where-  { {-# INLINE dim #-}; dim = DimSing 6 }-instance {-# OVERLAPPING #-} KnownDim 7  where-  { {-# INLINE dim #-}; dim = DimSing 7 }-instance {-# OVERLAPPING #-} KnownDim 8  where-  { {-# INLINE dim #-}; dim = DimSing 8 }-instance {-# OVERLAPPING #-} KnownDim 9  where-  { {-# INLINE dim #-}; dim = DimSing 9 }-instance {-# OVERLAPPING #-} KnownDim 10 where-  { {-# INLINE dim #-}; dim = DimSing 10 }-instance {-# OVERLAPPING #-} KnownDim 11 where-  { {-# INLINE dim #-}; dim = DimSing 11 }-instance {-# OVERLAPPING #-} KnownDim 12 where-  { {-# INLINE dim #-}; dim = DimSing 12 }-instance {-# OVERLAPPING #-} KnownDim 13 where-  { {-# INLINE dim #-}; dim = DimSing 13 }-instance {-# OVERLAPPING #-} KnownDim 14 where-  { {-# INLINE dim #-}; dim = DimSing 14 }-instance {-# OVERLAPPING #-} KnownDim 15 where-  { {-# INLINE dim #-}; dim = DimSing 15 }-instance {-# OVERLAPPING #-} KnownDim 16 where-  { {-# INLINE dim #-}; dim = DimSing 16 }-instance {-# OVERLAPPING #-} KnownDim 17 where-  { {-# INLINE dim #-}; dim = DimSing 17 }-instance {-# OVERLAPPING #-} KnownDim 18 where-  { {-# INLINE dim #-}; dim = DimSing 18 }-instance {-# OVERLAPPING #-} KnownDim 19 where-  { {-# INLINE dim #-}; dim = DimSing 19 }-instance {-# OVERLAPPING #-} KnownDim 20 where-  { {-# INLINE dim #-}; dim = DimSing 20 }--instance KnownDim n => KnownDim ('N n) where-    {-# INLINE dim #-}-    dim = unsafeCoerce# (dim @Nat @n)---- | Similar to `someNatVal` from `GHC.TypeLits`.-someDimVal :: Word -> SomeDim-someDimVal = unsafeCoerce#-{-# INLINE someDimVal #-}----- | Change the minimum allowed size of a @Dim (XN x)@,---   while testing if the value inside satisfies it.-constrain :: forall (m :: Nat) x . KnownDim m-          => Dim x -> Maybe (Dim (XN m))-constrain (DimSing x) | dimVal' @m > x = Nothing-                      | otherwise      = Just (unsafeCoerce# x)-{-# INLINE constrain #-}---- | `constrain` with explicitly-passed constraining @Dim@---   to avoid @AllowAmbiguousTypes@.-constrainBy :: forall m x . Dim m -> Dim x -> Maybe (Dim (XN m))-constrainBy D = constrain @m-#if __GLASGOW_HASKELL__ < 802-constrainBy _ = error "Dim: Impossible pattern."-#endif---- | Decrease minimum allowed size of a @Dim (XN x)@.-relax :: forall (m :: Nat) (n :: Nat) . (MinDim m n) => Dim (XN n) -> Dim (XN m)-relax = unsafeCoerce#-{-# INLINE relax #-}----- | We either get evidence that this function---   was instantiated with the same type-level numbers, or Nothing.------   Note, this function works on @Nat@-indexed dimensions only,---   because @Dim (XN x)@ does not have runtime evidence to infer @x@---   and `KnownDim x` does not imply `KnownDim (XN x)`.-sameDim :: forall (x :: Nat) (y :: Nat)-         . Dim x -> Dim y -> Maybe (Evidence (x ~ y))-sameDim (DimSing a) (DimSing b)-  | a == b    = Just (unsafeCoerce# (E @(x ~ x)))-  | otherwise = Nothing-{-# INLINE sameDim #-}---- | We either get evidence that this function---   was instantiated with the same type-level numbers, or Nothing.-sameDim' :: forall (x :: Nat) (y :: Nat) p q-          . (KnownDim x, KnownDim y)-         => p x -> q y -> Maybe (Evidence (x ~ y))-sameDim' _ _ = sameDim (dim @Nat @x) (dim @Nat @y)-{-# INLINE sameDim' #-}---- | Ordering of dimension values.-compareDim :: Dim a -> Dim b -> Ordering-compareDim = unsafeCoerce# (compare :: Word -> Word -> Ordering)-{-# INLINE compareDim #-}----- | Ordering of dimension values.-compareDim' :: forall a b p q-             . (KnownDim a, KnownDim b) => p a -> q b -> Ordering-compareDim' _ _ = compareDim (dim @_ @a)  (dim @_ @b)-{-# INLINE compareDim' #-}---instance Eq (Dim (n :: Nat)) where-    _ == _ = True-    {-# INLINE (==) #-}--instance Eq (Dim (x :: XNat)) where-    DimSing a == DimSing b = a == b-    {-# INLINE (==) #-}--instance Ord (Dim (n :: Nat)) where-    compare _ _ = EQ-    {-# INLINE compare #-}--instance Ord (Dim (x :: XNat)) where-    compare = compareDim-    {-# INLINE compare #-}--instance Show (Dim x) where-    showsPrec p = showsPrec p . dimVal-    {-# INLINE showsPrec #-}--instance KnownDim m => Read (Dim ('XN m)) where-    readsPrec p xs = do (a,ys) <- readsPrec p xs-                        case constrain (someDimVal a) of-                          Nothing -> []-                          Just n  -> [(n,ys)]-----plusDim :: Dim n -> Dim m -> Dim (n + m)-plusDim (DimSing a) (DimSing b) = unsafeCoerce# (a + b)-{-# INLINE plusDim #-}--minusDim :: MinDim m n => Dim n -> Dim m -> Dim (n - m)-minusDim (DimSing a) (DimSing b) = unsafeCoerce# (a - b)-{-# INLINE minusDim #-}--minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m))-minusDimM (DimSing a) (DimSing b)-  | a >= b    = Just (unsafeCoerce# (a - b))-  | otherwise = Nothing-{-# INLINE minusDimM #-}--timesDim :: Dim n -> Dim m -> Dim ((TL.*) n m)-timesDim (DimSing a) (DimSing b) = unsafeCoerce# (a * b)-{-# INLINE timesDim #-}--powerDim :: Dim n -> Dim m -> Dim ((TL.^) n m)-powerDim (DimSing a) (DimSing b) = unsafeCoerce# (a ^ b)-{-# INLINE powerDim #-}----- | @MinDim@ implies @(<=)@, but this fact is not so clear to GHC.---   This function assures the type system that the relation takes place.-inferDimLE :: forall m n . MinDim m n => Evidence (m <= n)-inferDimLE = unsafeCoerce# (E @(n <= n))----- | GADT to support `KnownDimKind` type class.---   Match against its constructors to know if @k@ is @Nat@ or @XNat@-data DimKind :: Type -> Type where-    -- | Working on @Nat@.-    DimNat  :: DimKind Nat-    -- | Working on @XNat@.-    DimXNat :: DimKind XNat---- | Figure out whether the type-level dimension is `Nat` or `XNat`.---   Useful for generalized inference functions.-class KnownDimKind k where-    dimKind :: DimKind k--instance KnownDimKind Nat where-    dimKind = DimNat--instance KnownDimKind XNat where-    dimKind = DimXNat-------------------------------------------------------------------------------------- | This function does GHC's magic to convert user-supplied `dim` function---   to create an instance of `KnownDim` typeclass at runtime.---   The trick is taken from Edward Kmett's reflection library explained---   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection-reifyDim :: forall r d . Dim d -> (KnownDim d => r) -> r-reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d-{-# INLINE reifyDim #-}-newtype MagicDim d r = MagicDim (KnownDim d => r)--dimEv :: Dim d -> Evidence (KnownDim d)-dimEv d = reifyDim d E-{-# INLINE dimEv #-}--data PatXDim (xn :: XNat) where-  PatN :: KnownDim n => Dim n -> PatXDim ('N n)-  PatXN :: (KnownDim n, MinDim m n) => Dim n -> PatXDim ('XN m)--dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn-dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd)-  where-    dd = DimSing @Nat @_ k-dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn)-  where-    dd = DimSing @Nat @_ k-    f :: forall (d :: Nat) (m :: Nat)-       . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m)-    f d _ = case ( unsafeCoerce# (E @((CmpNat m m == 'GT) ~ 'False, m <= m))-                :: Evidence ((CmpNat m d == 'GT) ~ 'False, m <= d)-               ) of-      E -> PatXN d-{-# INLINE dimXNEv #-}

@@ -4,29 +4,25 @@ -- Copyright   :  (c) Artem Chirkin -- License     :  BSD3 ----- Maintainer  :  chirkin@arch.ethz.ch -- -- Provides a set of data types to define and traverse through multiple dimensions.--- The core types are `Dims ds` and `Idxs ds`, which fix dimension sizes at compile time.+-- The core types are `Dims ds` and `Idxs ds`,+--   which fix dimension sizes at compile time. ----- Lower indices go first, i.e. assumed enumeration---          is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).--- This is also to encourage column-first matrix enumeration and array layout.+-- Higher indices go first, i.e. assumed enumeration+--          is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik+-- This corresponds to row-first layout of matrices and multidimenional arrays. -- -----------------------------------------------------------------------------  module Numeric.Dimensions-  ( module Numeric.Dim-  , module Numeric.Dimensions.Dims-  , module Numeric.Dimensions.Idxs-  , module Numeric.Dimensions.Fold-  , module Numeric.Type.Evidence-  , module Numeric.Type.List+  ( module Numeric.Dimensions.Dim+  , module Numeric.Dimensions.Idx+  , module Data.Type.List+  , module Data.Constraint   ) where -import Numeric.Dim-import Numeric.Dimensions.Dims-import Numeric.Dimensions.Idxs-import Numeric.Dimensions.Fold-import Numeric.Type.Evidence-import Numeric.Type.List+import Data.Constraint         ((:-) (..), Dict (..), mapDict, (\\))+import Data.Type.List+import Numeric.Dimensions.Dim+import Numeric.Dimensions.Idx

@@ -0,0 +1,1084 @@+{-# LANGUAGE AllowAmbiguousTypes       #-}+{-# LANGUAGE CPP                       #-}+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE DeriveDataTypeable        #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE LambdaCase                #-}+{-# LANGUAGE MagicHash                 #-}+{-# LANGUAGE MultiParamTypeClasses     #-}+{-# LANGUAGE PatternSynonyms           #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE RoleAnnotations           #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeFamilyDependencies    #-}+{-# LANGUAGE TypeInType                #-}+{-# LANGUAGE TypeOperators             #-}+{-# LANGUAGE UndecidableInstances      #-}+{-# LANGUAGE UndecidableSuperClasses   #-}+{-# LANGUAGE ViewPatterns              #-}+#if __GLASGOW_HASKELL__ >= 806+{-# LANGUAGE NoStarIsType              #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dimensions.Dim+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+-- This module provides `KnownDim` class that is similar to `KnownNat` from `GHC.TypeNats`,+-- but keeps `Word`s instead of `Natural`s;+-- Also it provides `Dim` data type serving as a singleton+-- suitable for recovering an instance of the `KnownDim` class.+-- A set of utility functions provide inference functionality, so+-- that `KnownDim` can be preserved over some type-level operations.+--+-- Provides a data type @Dims ds@ to keep dimension sizes+-- for multiple-dimensional data.+-- Higher indices go first, i.e. assumed enumeration+--          is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik+-- This corresponds to row-first layout of matrices and multidimenional arrays.+--+-----------------------------------------------------------------------------++module Numeric.Dimensions.Dim+  ( -- * @Dim@ -- a @Nat@-indexed dimension+    -- ** Type level numbers that can be unknown.+    XNat (..), XN, N, XNatType (..)+    -- ** Term level dimension+  , Dim ( D, Dn, Dx+        , D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, D10, D11, D12, D13+        , D14, D15, D16, D17, D18, D19, D20, D21, D22, D23, D24, D25+        )+  , SomeDim+  , KnownDim (..), BoundedDim (..), minDim, KnownXNatType (..), FixedDim+  , dimVal, dimVal', typeableDim, someDimVal+  , sameDim, sameDim'+  , compareDim, compareDim'+  , constrainBy, relax+    -- * Simple Dim arithmetics+    --+    --   The functions below create singleton values that work as a witness+    --   of `KnownDim` instance for type-level Nat operations.+    --   For example, to show that @(a + b)@ is a @KnownDim@, one writes:+    --+    --   > case plusDim dA dB of+    --   >   D -> ... -- here we know KnownDim ( a + b )+    --+    --   There is a bug and a feature in these functions though:+    --   they are implemented in terms of @Num Word@, which means that+    --   their results are subject to integer overflow.+    --   The good side is the confidence that they behave exactly as+    --   their @Word@ counterparts.+  , plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim+    -- ** Re-export part of `Data.Type.Lits` for convenience+  , Nat, CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)+    -- ** Inferring kind of type-level dimension+  , KnownDimKind (..), DimKind (..)+    -- * @Dims@ -- a list of dimensions+  , Dims, SomeDims (..), Dimensions (..), BoundedDims (..), minDims+  , TypedList ( Dims, XDims, AsXDims, KnownDims+              , U, (:*), Empty, TypeList, Cons, Snoc, Reverse)+  , typeableDims, inferTypeableDims+  , listDims, someDimsVal, totalDim, totalDim'+  , sameDims, sameDims'+  , inSpaceOf, asSpaceOf+  , xDims, xDims'+  , stripPrefixDims, stripSuffixDims+    -- ** Type-level programming+    --   Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`)+  , AsXDims, AsDims, FixedDims, KnownXNatTypes+    -- ** Re-export type list+  , RepresentableList (..), TypeList, types+  , order, order'+  ) where+++import           Data.Bits         (countLeadingZeros, finiteBitSize)+import           Data.Coerce+import           Data.Constraint+import           Data.Data         hiding (TypeRep, typeRep, typeRepTyCon)+import           Data.Kind         (Constraint, Type)+import qualified Data.List         (stripPrefix)+import           Data.Type.List+import           Data.Type.Lits+import           GHC.Exts          (Proxy#, proxy#, unsafeCoerce#)+import qualified GHC.Generics      as G+import           Numeric.Natural   (Natural)+import           Numeric.TypedList+import qualified Text.Read         as Read+import qualified Text.Read.Lex     as Read+import           Type.Reflection+++-- | Either known or unknown at compile-time natural number+data XNat = XN Nat | N Nat+-- | Unknown natural number, known to be not smaller than the given Nat+type XN (n::Nat) = 'XN n+-- | Known natural number+type N (n::Nat) = 'N n++-- | Find out whether @XNat@ is of known or constrained type.+data XNatType :: XNat -> Type where+    -- | Given @XNat@ is known+    Nt  :: XNatType ('N n)+    -- | Given @XNat@ is constrained unknown+    XNt :: XNatType ('XN m)++-- | Same as `SomeNat`+type SomeDim = Dim ('XN 0)++-- | Singleton type to store type-level dimension value.+--+--   On the one hand, it can be used to let type-inference system know+--   relations between type-level naturals.+--   On the other hand, this is just a newtype wrapper on the @Word@ type.+--+--   Usually, the type parameter of @Dim@ is either @Nat@ or @XNat@.+--   If dimensionality of your data is known in advance, use @Nat@;+--   if you know the size of some dimensions, but do not know the size+--   of others, use @XNat@s to represent them.+newtype Dim (x :: k) = DimSing Word+  deriving ( Typeable )++-- | Type-level dimensionality.+type Dims (xs :: [k]) = TypedList Dim xs++-- | Match against this pattern to bring `KnownDim` instance into scope.+pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n+pattern D <- (dimEv -> Dict)+  where+    D = dim @n+{-# COMPLETE D #-}++-- | Statically known `XNat`+pattern Dn :: forall (xn :: XNat) . KnownXNatType xn+           => forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn+pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k)+  where+    Dn k = coerce k++-- | `XNat` that is unknown at compile time.+--   Same as `SomeNat`, but for a dimension:+--   Hide dimension size inside, but allow specifying its minimum possible value.+pattern Dx :: forall (xn :: XNat) . KnownXNatType xn+           => forall (n :: Nat) (m :: Nat)+            . (KnownDim n, m <= n, xn ~ 'XN m) => Dim n -> Dim xn+pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)+  where+    Dx k = coerce k+{-# COMPLETE Dn, Dx #-}++-- | This class provides the `Dim` associated with a type-level natural.+--+--   Note, kind of the @KnownDim@ argument is always @Nat@, because+--     it is impossible to create a unique @KnownDim (XN m)@ instance.+class KnownDim (n :: Nat) where+    -- | Get value of type-level dim at runtime.+    --+    --   Note, this function is supposed to be used with @TypeApplications@.+    --   For example, you can type:+    --+    --   >>>:set -XTypeApplications+    --   >>>:set -XDataKinds+    --   >>>:t dim @3+    --   dim @3 :: Dim 3+    --+    --   >>>:set -XTypeOperators+    --   >>>:t dim @(13 - 6)+    --   dim @(13 - 6) :: Dim 7+    --+    dim :: Dim n++-- | Get a minimal or exact bound of a @Dim@.+--+--   To satisfy the @BoundedDim@ means to be equal to @N n@ or be not less than @XN m@.+class KnownDimKind k => BoundedDim (n :: k) where+    -- | Minimal or exact bound of a @Dim@.+    --   Useful for indexing: it is safe to index something by an index less than+    --   @DimBound n@ (for both @Nat@ and @Xnat@ indexed dims).+    type family DimBound n :: Nat+    -- | Get such a minimal @Dim (DimBound n)@, that @Dim n@ is guaranteed+    --   to be not less than @dimBound@ if @n ~ XN a@,+  --     otherwise, the return @Dim@ is the same as @n@.+    dimBound :: Dim (DimBound n)+    -- | If the runtime value of @Dim y@ satisfies @dimBound @k @x@,+    --   then coerce to @Dim x@. Otherwise, return @Nothing@.+    --+    --   To satisfy the @dimBound@ means to be equal to @N n@ or be not less than @XN m@.+    constrainDim :: forall (l :: Type) (y :: l) . Dim y -> Maybe (Dim n)+++instance KnownDim n => BoundedDim (n :: Nat) where+    type DimBound n = n+    dimBound = dim @n+    {-# INLINE dimBound #-}+    constrainDim (DimSing y)+       | dimVal' @n == y = Just (DimSing y)+       | otherwise       = Nothing+    {-# INLINE constrainDim #-}++instance KnownDim n => BoundedDim ('N n) where+    type DimBound ('N n) = n+    dimBound = dim @n+    {-# INLINE dimBound #-}+    constrainDim (DimSing y)+       | dimVal' @n == y = Just (DimSing y)+       | otherwise       = Nothing+    {-# INLINE constrainDim #-}++instance KnownDim m => BoundedDim ('XN m) where+    type DimBound ('XN m) = m+    dimBound = dim @m+    {-# INLINE dimBound #-}+    constrainDim (DimSing y)+       | dimVal' @m <= y = Just (DimSing y)+       | otherwise       = Nothing+    {-# INLINE constrainDim #-}++minDim :: forall (k :: Type) (d :: k) . BoundedDim d => Dim d+minDim = coerce (dimBound @k @d)++-- | Find out the type of `XNat` constructor+class KnownXNatType (n :: XNat) where+    -- | Pattern-match against this to out the type of `XNat` constructor+    xNatType :: XNatType n++instance KnownXNatType ('N n) where+    xNatType = Nt+    {-# INLINE xNatType #-}++instance KnownXNatType ('XN n) where+    xNatType = XNt+    {-# INLINE xNatType #-}++-- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.+dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word+dimVal = coerce+{-# INLINE dimVal #-}++-- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.+dimVal' :: forall (n :: Nat) . KnownDim n => Word+dimVal' = coerce (dim @n)+{-# INLINE dimVal' #-}++-- | Construct a @Dim n@ if there is an instance of @Typeable n@ around.+typeableDim :: forall (n :: Nat) . Typeable n => Dim n+{- YES, that's right. TyCon of a Nat is a string containing the Nat value.+   There simply no place in a TyCon to keep the Nat as a number+     (check GHC.Types for the definition of TyCon).++  Here is an excert from Data.Typeable.Internal:++  -- | Used to make `'Typeable' instance for things of kind Nat+  typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep a+  typeNatTypeRep p = typeLitTypeRep (show (natVal' p)) tcNat++ -}+typeableDim = DimSing . read . tyConName . typeRepTyCon $ typeRep @n+{-# INLINE typeableDim #-}++-- | Constraints given by an XNat type on possible values of a Nat hidden inside.+type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where+    FixedDim ('N a)  b = a ~ b+    FixedDim ('XN m) b = m <= b++instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where+    {-# INLINE dim #-}+    dim = DimSing (fromIntegral (natVal' (proxy# :: Proxy# n)))++instance {-# OVERLAPPING #-} KnownDim 0  where+  { {-# INLINE dim #-}; dim = DimSing 0 }+instance {-# OVERLAPPING #-} KnownDim 1  where+  { {-# INLINE dim #-}; dim = DimSing 1 }+instance {-# OVERLAPPING #-} KnownDim 2  where+  { {-# INLINE dim #-}; dim = DimSing 2 }+instance {-# OVERLAPPING #-} KnownDim 3  where+  { {-# INLINE dim #-}; dim = DimSing 3 }+instance {-# OVERLAPPING #-} KnownDim 4  where+  { {-# INLINE dim #-}; dim = DimSing 4 }+instance {-# OVERLAPPING #-} KnownDim 5  where+  { {-# INLINE dim #-}; dim = DimSing 5 }+instance {-# OVERLAPPING #-} KnownDim 6  where+  { {-# INLINE dim #-}; dim = DimSing 6 }+instance {-# OVERLAPPING #-} KnownDim 7  where+  { {-# INLINE dim #-}; dim = DimSing 7 }+instance {-# OVERLAPPING #-} KnownDim 8  where+  { {-# INLINE dim #-}; dim = DimSing 8 }+instance {-# OVERLAPPING #-} KnownDim 9  where+  { {-# INLINE dim #-}; dim = DimSing 9 }+instance {-# OVERLAPPING #-} KnownDim 10 where+  { {-# INLINE dim #-}; dim = DimSing 10 }+instance {-# OVERLAPPING #-} KnownDim 11 where+  { {-# INLINE dim #-}; dim = DimSing 11 }+instance {-# OVERLAPPING #-} KnownDim 12 where+  { {-# INLINE dim #-}; dim = DimSing 12 }+instance {-# OVERLAPPING #-} KnownDim 13 where+  { {-# INLINE dim #-}; dim = DimSing 13 }+instance {-# OVERLAPPING #-} KnownDim 14 where+  { {-# INLINE dim #-}; dim = DimSing 14 }+instance {-# OVERLAPPING #-} KnownDim 15 where+  { {-# INLINE dim #-}; dim = DimSing 15 }+instance {-# OVERLAPPING #-} KnownDim 16 where+  { {-# INLINE dim #-}; dim = DimSing 16 }+instance {-# OVERLAPPING #-} KnownDim 17 where+  { {-# INLINE dim #-}; dim = DimSing 17 }+instance {-# OVERLAPPING #-} KnownDim 18 where+  { {-# INLINE dim #-}; dim = DimSing 18 }+instance {-# OVERLAPPING #-} KnownDim 19 where+  { {-# INLINE dim #-}; dim = DimSing 19 }+instance {-# OVERLAPPING #-} KnownDim 20 where+  { {-# INLINE dim #-}; dim = DimSing 20 }+instance {-# OVERLAPPING #-} KnownDim 21 where+  { {-# INLINE dim #-}; dim = DimSing 21 }+instance {-# OVERLAPPING #-} KnownDim 22 where+  { {-# INLINE dim #-}; dim = DimSing 22 }+instance {-# OVERLAPPING #-} KnownDim 23 where+  { {-# INLINE dim #-}; dim = DimSing 23 }+instance {-# OVERLAPPING #-} KnownDim 24 where+  { {-# INLINE dim #-}; dim = DimSing 24 }+instance {-# OVERLAPPING #-} KnownDim 25 where+  { {-# INLINE dim #-}; dim = DimSing 25 }++instance Class (KnownNat n) (KnownDim n) where+    cls = Sub $ reifyNat @_ @n (fromIntegral $ dimVal' @n) Dict++-- | Similar to `someNatVal` from `GHC.TypeNats`.+someDimVal :: Word -> SomeDim+someDimVal = coerce+{-# INLINE someDimVal #-}++-- | `constrainDim` with explicitly-passed constraining @Dim@+--   to avoid @AllowAmbiguousTypes@.+constrainBy :: forall (k :: Type) (x :: k) (p :: k -> Type) (l :: Type) (y :: l)+             . BoundedDim x => p x -> Dim y -> Maybe (Dim x)+constrainBy = const (constrainDim @k @x @l @y)+{-# INLINE constrainBy #-}++-- | Decrease minimum allowed size of a @Dim (XN x)@.+relax :: forall (m :: Nat) (n :: Nat) . (<=) m n => Dim (XN n) -> Dim (XN m)+relax = coerce+{-# INLINE relax #-}++-- | We either get evidence that this function+--   was instantiated with the same type-level numbers, or Nothing.+--+--   Note, this function works on @Nat@-indexed dimensions only,+--   because @Dim (XN x)@ does not have runtime evidence to infer @x@+--   and `KnownDim x` does not imply `KnownDim (XN x)`.+sameDim :: forall (x :: Nat) (y :: Nat)+         . Dim x -> Dim y -> Maybe (Dict (x ~ y))+sameDim (DimSing a) (DimSing b)+  | a == b    = Just (unsafeCoerceDict @(x ~ x) Dict)+  | otherwise = Nothing+{-# INLINE sameDim #-}++-- | We either get evidence that this function+--   was instantiated with the same type-level numbers, or Nothing.+sameDim' :: forall (x :: Nat) (y :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)+          . (KnownDim x, KnownDim y)+         => p x -> q y -> Maybe (Dict (x ~ y))+sameDim' = const . const $ sameDim (dim @x) (dim @y)+{-# INLINE sameDim' #-}++-- | Ordering of dimension values.+--+--   Note: `CmpNat` forces type parameters to kind `Nat`;+--         if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`.+compareDim :: forall (a :: Nat) (b :: Nat)+            . Dim a -> Dim b -> SOrdering (CmpNat a b)+compareDim a b+  = case coerce (compare :: Word -> Word -> Ordering) a b of+    LT -> unsafeCoerce# SLT+    EQ -> unsafeCoerce# SEQ+    GT -> unsafeCoerce# SGT+{-# INLINE compareDim #-}++-- | Ordering of dimension values.+--+--   Note: `CmpNat` forces type parameters to kind `Nat`;+--         if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`.+compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)+             . (KnownDim a, KnownDim b) => p a -> q b -> SOrdering (CmpNat a b)+compareDim' = const . const $ compareDim (dim @a)  (dim @b)+{-# INLINE compareDim' #-}++plusDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (n + m)+plusDim = coerce ((+) :: Word -> Word -> Word)+{-# INLINE plusDim #-}++minusDim :: forall (n :: Nat) (m :: Nat) . (<=) m n => Dim n -> Dim m -> Dim (n - m)+minusDim = coerce ((-) :: Word -> Word -> Word)+{-# INLINE minusDim #-}++minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m))+minusDimM (DimSing a) (DimSing b)+  | a >= b    = Just (coerce (a - b))+  | otherwise = Nothing+{-# INLINE minusDimM #-}++timesDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((*) n m)+timesDim = coerce ((*) :: Word -> Word -> Word)+{-# INLINE timesDim #-}++powerDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((^) n m)+powerDim = coerce ((^) :: Word -> Word -> Word)+{-# INLINE powerDim #-}++divDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Div n m)+divDim = coerce (div :: Word -> Word -> Word)++modDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Mod n m)+modDim = coerce (mod :: Word -> Word -> Word)++log2Dim :: forall (n :: Nat) . Dim n -> Dim (Log2 n)+log2Dim (DimSing 0) = undefined+log2Dim (DimSing x) = DimSing . fromIntegral $ finiteBitSize x - 1 - countLeadingZeros x+++-- | GADT to support `KnownDimKind` type class.+--   Match against its constructors to know if @k@ is @Nat@ or @XNat@+data DimKind :: Type -> Type where+    -- | Working on @Nat@.+    DimNat  :: DimKind Nat+    -- | Working on @XNat@.+    DimXNat :: DimKind XNat++-- | Figure out whether the type-level dimension is `Nat` or `XNat`.+--   Useful for generalized inference functions.+class KnownDimKind (k :: Type) where+    dimKind :: DimKind k++instance KnownDimKind Nat where+    dimKind = DimNat++instance KnownDimKind XNat where+    dimKind = DimXNat+++-- | Match @Dim n@ against a concrete @Nat@+pattern D0 :: forall (n :: Nat) . () => n ~ 0 => Dim n+pattern D0 <- (sameDim (D @0) -> Just Dict)+  where D0 = DimSing 0++-- | Match @Dim n@ against a concrete @Nat@+pattern D1 :: forall (n :: Nat) . () => n ~ 1 => Dim n+pattern D1 <- (sameDim (D @1) -> Just Dict)+  where D1 = DimSing 1++-- | Match @Dim n@ against a concrete @Nat@+pattern D2 :: forall (n :: Nat) . () => n ~ 2 => Dim n+pattern D2 <- (sameDim (D @2) -> Just Dict)+  where D2 = DimSing 2++-- | Match @Dim n@ against a concrete @Nat@+pattern D3 :: forall (n :: Nat) . () => n ~ 3 => Dim n+pattern D3 <- (sameDim (D @3) -> Just Dict)+  where D3 = DimSing 3++-- | Match @Dim n@ against a concrete @Nat@+pattern D4 :: forall (n :: Nat) . () => n ~ 4 => Dim n+pattern D4 <- (sameDim (D @4) -> Just Dict)+  where D4 = DimSing 4++-- | Match @Dim n@ against a concrete @Nat@+pattern D5 :: forall (n :: Nat) . () => n ~ 5 => Dim n+pattern D5 <- (sameDim (D @5) -> Just Dict)+  where D5 = DimSing 5++-- | Match @Dim n@ against a concrete @Nat@+pattern D6 :: forall (n :: Nat) . () => n ~ 6 => Dim n+pattern D6 <- (sameDim (D @6) -> Just Dict)+  where D6 = DimSing 6++-- | Match @Dim n@ against a concrete @Nat@+pattern D7 :: forall (n :: Nat) . () => n ~ 7 => Dim n+pattern D7 <- (sameDim (D @7) -> Just Dict)+  where D7 = DimSing 7++-- | Match @Dim n@ against a concrete @Nat@+pattern D8 :: forall (n :: Nat) . () => n ~ 8 => Dim n+pattern D8 <- (sameDim (D @8) -> Just Dict)+  where D8 = DimSing 8++-- | Match @Dim n@ against a concrete @Nat@+pattern D9 :: forall (n :: Nat) . () => n ~ 9 => Dim n+pattern D9 <- (sameDim (D @9) -> Just Dict)+  where D9 = DimSing 9++-- | Match @Dim n@ against a concrete @Nat@+pattern D10 :: forall (n :: Nat) . () => n ~ 10 => Dim n+pattern D10 <- (sameDim (D @10) -> Just Dict)+  where D10 = DimSing 10++-- | Match @Dim n@ against a concrete @Nat@+pattern D11 :: forall (n :: Nat) . () => n ~ 11 => Dim n+pattern D11 <- (sameDim (D @11) -> Just Dict)+  where D11 = DimSing 11++-- | Match @Dim n@ against a concrete @Nat@+pattern D12 :: forall (n :: Nat) . () => n ~ 12 => Dim n+pattern D12 <- (sameDim (D @12) -> Just Dict)+  where D12 = DimSing 12++-- | Match @Dim n@ against a concrete @Nat@+pattern D13 :: forall (n :: Nat) . () => n ~ 13 => Dim n+pattern D13 <- (sameDim (D @13) -> Just Dict)+  where D13 = DimSing 13++-- | Match @Dim n@ against a concrete @Nat@+pattern D14 :: forall (n :: Nat) . () => n ~ 14 => Dim n+pattern D14 <- (sameDim (D @14) -> Just Dict)+  where D14 = DimSing 14++-- | Match @Dim n@ against a concrete @Nat@+pattern D15 :: forall (n :: Nat) . () => n ~ 15 => Dim n+pattern D15 <- (sameDim (D @15) -> Just Dict)+  where D15 = DimSing 15++-- | Match @Dim n@ against a concrete @Nat@+pattern D16 :: forall (n :: Nat) . () => n ~ 16 => Dim n+pattern D16 <- (sameDim (D @16) -> Just Dict)+  where D16 = DimSing 16++-- | Match @Dim n@ against a concrete @Nat@+pattern D17 :: forall (n :: Nat) . () => n ~ 17 => Dim n+pattern D17 <- (sameDim (D @17) -> Just Dict)+  where D17 = DimSing 17++-- | Match @Dim n@ against a concrete @Nat@+pattern D18 :: forall (n :: Nat) . () => n ~ 18 => Dim n+pattern D18 <- (sameDim (D @18) -> Just Dict)+  where D18 = DimSing 18++-- | Match @Dim n@ against a concrete @Nat@+pattern D19 :: forall (n :: Nat) . () => n ~ 19 => Dim n+pattern D19 <- (sameDim (D @19) -> Just Dict)+  where D19 = DimSing 19++-- | Match @Dim n@ against a concrete @Nat@+pattern D20 :: forall (n :: Nat) . () => n ~ 20 => Dim n+pattern D20 <- (sameDim (D @20) -> Just Dict)+  where D20 = DimSing 20++-- | Match @Dim n@ against a concrete @Nat@+pattern D21 :: forall (n :: Nat) . () => n ~ 21 => Dim n+pattern D21 <- (sameDim (D @21) -> Just Dict)+  where D21 = DimSing 21++-- | Match @Dim n@ against a concrete @Nat@+pattern D22 :: forall (n :: Nat) . () => n ~ 22 => Dim n+pattern D22 <- (sameDim (D @22) -> Just Dict)+  where D22 = DimSing 22++-- | Match @Dim n@ against a concrete @Nat@+pattern D23 :: forall (n :: Nat) . () => n ~ 23 => Dim n+pattern D23 <- (sameDim (D @23) -> Just Dict)+  where D23 = DimSing 23++-- | Match @Dim n@ against a concrete @Nat@+pattern D24 :: forall (n :: Nat) . () => n ~ 24 => Dim n+pattern D24 <- (sameDim (D @24) -> Just Dict)+  where D24 = DimSing 24++-- | Match @Dim n@ against a concrete @Nat@+pattern D25 :: forall (n :: Nat) . () => n ~ 25 => Dim n+pattern D25 <- (sameDim (D @25) -> Just Dict)+  where D25 = DimSing 25++++-- | @O(1)@ Pattern-matching against this constructor brings a `Dimensions`+--   instance into the scope.+--   Thus, you can do arbitrary operations on your dims and use this pattern+--   at any time to reconstruct the class instance at runtime.+pattern Dims :: forall (ds :: [Nat]) . () => Dimensions ds => Dims ds+pattern Dims <- (dimsEv -> Dict)+  where+    Dims = dims @ds+{-# COMPLETE Dims #-}++-- | @O(Length ds)@ A heavy weapon against all sorts of type errors+pattern KnownDims :: forall (ds :: [Nat]) . ()+                  => ( All KnownDim ds, All BoundedDim ds+                     , RepresentableList ds, Dimensions ds)+                     => Dims ds+pattern KnownDims <- (patKDims -> PatKDims)+  where+    KnownDims = dims @ds+{-# COMPLETE KnownDims #-}++-- | Pattern-matching against this constructor reveals Nat-kinded list of dims,+--   pretending the dimensionality is known at compile time within the scope+--   of the pattern match.+--   This is the main recommended way to get `Dims` at runtime;+--   for example, reading a list of dimensions from a file.+--+--   In order to use this pattern, one must know @XNat@ type constructors in+--   each dimension at compile time.+pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns+              => forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns)+              => Dims ns -> Dims xns+pattern XDims ns <- (patXDims -> PatXDims ns)+  where+    XDims ns = unsafeCoerce# ns+{-# COMPLETE XDims #-}++-- | An easy way to convert Nat-indexed dims into XNat-indexed dims.+pattern AsXDims :: forall (ns :: [Nat]) . ()+                => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))+                => Dims (AsXDims ns) -> Dims ns+pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns)+  where+    AsXDims xns = unsafeCoerce# xns+{-# COMPLETE AsXDims #-}++-- | Same as SomeNat, but for Dimensions:+--   Hide all information about Dimensions inside+data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)++-- | Put runtime evidence of `Dims` value inside function constraints.+--   Similar to `KnownDim` or `KnownNat`, but for lists of numbers.+--+--   Note, kind of the @Dimensions@ list is always @Nat@, restricted by+--   @KnownDim@ being also @Nat@-indexed+--     (it is impossible to create a unique @KnownDim (XN m)@ instance).+class Dimensions (ds :: [Nat]) where+    -- | Get dimensionality of a space at runtime,+    --   represented as a list of `Dim`.+    --+    --   Note, this function is supposed to be used with @TypeApplications@.+    --   For example, you can type:+    --+    --   >>>:set -XTypeApplications+    --   >>>:set -XDataKinds+    --   >>>:t dims @'[17, 12]+    --   dims @'[17, 12] :: Dims '[17, 12]+    --+    --   >>>:t dims @'[]+    --   dims @'[] :: Dims '[]+    --+    --   >>>:t dims @(Tail '[3,2,5,7])+    --   dims @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]+    --+    dims :: Dims ds++instance Dimensions '[] where+    dims = U+    {-# INLINE dims #-}++instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where+    dims = dim :* dims+    {-# INLINE dims #-}+++-- | Get a minimal or exact bound of @Dims@.+--+--   This is a plural form of `BoundedDim`.+--+--   @BoundedDims@ is a somewhat weaker form of @Dimensions@:+--+--    * It is defined for both @[Nat]@ and @[XNat]@;+--    * Instance of @Dimensions ds@ always implies @BoundedDims ds@.+class KnownDimKind k => BoundedDims (ds :: [k]) where+    -- | Minimal or exact bound of @Dims@.+    --   This is a plural form of `DimBound`.+    type family DimsBound ds :: [Nat]+    -- | Plural form for `dimBound`+    dimsBound :: Dims (DimsBound ds)+    -- | Plural form for `constrainDim`.+    --+    --   Given a @Dims ys@, test if its runtime value satisfies constraints imposed by+    --   @BoundedDims ds@, and returns it back coerced to @Dims ds@ on success.+    --+    --   This function allows to guess safely individual dimension values,+    --   as well as the length of the dimension list.+    --   It returns @Nothing@ if @ds@ and @xds@ have different length or if any+    --   of the values in @ys@ are less than the corresponding values of @ds@.+    constrainDims :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)+    -- | BoundedDims means every element dim is @BoundedDim@ and also+    --   the length of a dim list is known.+    --+    --   Enforcing this as a superclass would complicate instance relations,+    --   so it is better to provide these dictionaries on-demand.+    inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds)+++instance Dimensions ns => BoundedDims (ns :: [Nat]) where+    type DimsBound ns = ns+    dimsBound = dims @ns+    {-# INLINE dimsBound #-}+    constrainDims ys+      | listDims ys == listDims (dims @ns)+                  = Just (unsafeCoerce# ys)+      | otherwise = Nothing+    {-# INLINE constrainDims #-}+    inferAllBoundedDims = go (dims @ns)+      where+        go :: forall (ds :: [Nat]) . Dims ds+           -> Dict (All BoundedDim ds, RepresentableList ds)+        go  U             = Dict+        go (D :* ds)+          | Dict <- go ds = Dict++instance BoundedDims ('[] :: [XNat]) where+    type DimsBound '[] = '[]+    dimsBound = U+    constrainDims = const $ Just U+    inferAllBoundedDims = Dict++instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where+    type DimsBound (n ': ns) = DimBound n ': DimsBound ns+    dimsBound = dimBound @XNat @n :* dimsBound @XNat @ns+    constrainDims U         = Nothing+    constrainDims (y :* ys) = (:*) <$> constrainDim y <*> constrainDims ys+    inferAllBoundedDims = case inferAllBoundedDims @XNat @ns of Dict -> Dict+++-- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by+--   the type signature of @Dims ds@.+minDims :: forall (k :: Type) (ds :: [k])+         . BoundedDims ds => Dims ds+minDims = unsafeCoerce# (dimsBound @k @ds)+++++-- | Construct a @Dims ds@ if there is an instance of @Typeable ds@ around.+typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds+typeableDims = case typeRep @ds of+    App (App _ (tx :: TypeRep (n :: k1))) (txs :: TypeRep (ns :: k2))+      -> case unsafeCoerceDict @(Nat ~ Nat, [Nat] ~ [Nat])+                               @(Nat ~ k1 , [Nat] ~ k2) Dict of+          Dict -> case unsafeCoerceDict @(ds ~ ds)+                                        @(ds ~ (n ': ns)) Dict of+            Dict -> withTypeable tx (typeableDim @n)+                 :* withTypeable txs (typeableDims @ns)+    Con _+      -> unsafeCoerce# U+    r -> error ("typeableDims -- impossible typeRep: " ++ show r)+{-# INLINE typeableDims #-}++-- | @Dims (ds :: [Nat])@ is always @Typeable@.+inferTypeableDims :: forall (ds :: [Nat]) . Dims ds -> Dict (Typeable ds)+inferTypeableDims U         = Dict+inferTypeableDims ((D :: Dim d) :* ds)+  | Dict <- mapDict cls (Dict @(KnownDim d))+  , Dict <- inferTypeableDims ds+    = Dict+++-- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@.+--+--   Note, for @XNat@-indexed list it returns actual content dimensions,+--   not the constraint numbers (@XN m@)+listDims :: forall (k :: Type) (xs :: [k]) . Dims xs -> [Word]+listDims = unsafeCoerce#+{-# INLINE listDims #-}++-- | Convert a plain haskell list of dimension sizes into an unknown+--   type-level dimensionality  @O(1)@.+someDimsVal :: [Word] -> SomeDims+someDimsVal = SomeDims . unsafeCoerce#+{-# INLINE someDimsVal #-}++-- | Product of all dimension sizes @O(Length xs)@.+totalDim :: forall (k :: Type) (xs :: [k]) . Dims xs -> Word+totalDim = product . listDims+{-# INLINE totalDim #-}++-- | Product of all dimension sizes @O(Length xs)@.+totalDim' :: forall (xs :: [Nat]) . Dimensions xs => Word+totalDim' = totalDim (dims @xs)+{-# INLINE totalDim' #-}++-- | Get XNat-indexed dims given their fixed counterpart.+xDims :: forall (xns :: [XNat]) (ns :: [Nat])+       . FixedDims xns ns => Dims ns -> Dims xns+xDims = unsafeCoerce#+{-# INLINE xDims #-}++-- | Get XNat-indexed dims given their fixed counterpart.+xDims' :: forall (xns :: [XNat]) (ns :: [Nat])+        . (FixedDims xns ns, Dimensions ns) => Dims xns+xDims' = xDims @xns (dims @ns)+{-# INLINE xDims' #-}++-- | Drop the given prefix from a Dims list.+--   It returns Nothing if the list did not start with the prefix given,+--    or Just the Dims after the prefix, if it does.+stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat])+                 . Dims xs -> Dims ys+                -> Maybe (Dims (StripPrefix xs ys))+stripPrefixDims = unsafeCoerce# (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word])+{-# INLINE stripPrefixDims #-}++-- | Drop the given suffix from a Dims list.+--   It returns Nothing if the list did not end with the suffix given,+--    or Just the Dims before the suffix, if it does.+stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat])+                 . Dims xs -> Dims ys+                -> Maybe (Dims (StripSuffix xs ys))+stripSuffixDims = unsafeCoerce# stripSuf+  where+    stripSuf :: [Word] -> [Word] -> Maybe [Word]+    stripSuf suf whole = go pref whole+      where+        pref = getPref suf whole+        getPref (_:as) (_:bs) = getPref as bs+        getPref [] bs         = zipWith const whole bs+        getPref _  []         = []+        go (_:as) (_:bs) = go as bs+        go  []     bs    = if suf == bs then Just pref else Nothing+        go  _      []    = Nothing+{-# INLINE stripSuffixDims #-}++-- | We either get evidence that this function was instantiated with the+--   same type-level Dimensions, or 'Nothing' @O(Length xs)@.+sameDims :: forall (as :: [Nat]) (bs :: [Nat])+          . Dims as -> Dims bs -> Maybe (Dict (as ~ bs))+sameDims as bs+  | listDims as == listDims bs+    = Just (unsafeCoerceDict @(as ~ as) Dict)+  | otherwise = Nothing+{-# INLINE sameDims #-}++-- | We either get evidence that this function was instantiated with the+--   same type-level Dimensions, or 'Nothing' @O(Length xs)@.+sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) (p :: [Nat] -> Type) (q :: [Nat] -> Type)+           . (Dimensions as, Dimensions bs)+          => p as -> q bs -> Maybe (Dict (as ~ bs))+sameDims' = const . const $ sameDims (dims @as) (dims @bs)+{-# INLINE sameDims' #-}+++-- | Similar to `const` or `asProxyTypeOf`;+--   to be used on such implicit functions as `dim`, `dimMax`, etc.+inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type)+           . p ds -> q ds -> p ds+inSpaceOf = const+{-# INLINE inSpaceOf #-}++-- | Similar to `asProxyTypeOf`,+--   Give a hint to type checker to fix the type of a function argument.+asSpaceOf :: forall (k :: Type) (ds :: [k])+                    (p :: [k] -> Type) (q :: [k] -> Type) (r :: Type)+           . p ds -> (q ds -> r) -> (q ds -> r)+asSpaceOf = const id+{-# INLINE asSpaceOf #-}++-- | Map Dims onto XDims (injective)+type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where+    AsXDims '[] = '[]+    AsXDims (n ': ns) = N n ': AsXDims ns++-- | Map XDims onto Dims (injective)+type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where+    AsDims '[] = '[]+    AsDims (N x ': xs) = x ': AsDims xs++-- | Constrain @Nat@ dimensions hidden behind @XNat@s.+type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where+    FixedDims '[] ns = (ns ~ '[])+    FixedDims (xn ': xns) ns+      = ( ns ~ (Head ns ': Tail ns)+        , FixedDim xn (Head ns)+        , FixedDims xns (Tail ns))++-- | Know the structure of each dimension+type KnownXNatTypes xns = All KnownXNatType xns+++++instance Typeable d => Data (Dim (d :: Nat)) where+    gfoldl _ = id+    gunfold _ z = const (z (typeableDim @d))+    toConstr = const $ dimNatConstr (dimVal (typeableDim @d))+    dataTypeOf = const $ dimDataType (dimVal (typeableDim @d))++dimDataType :: Word -> DataType+dimDataType = mkDataType "Numeric.Dim.Dim" . (:[]) . dimNatConstr++dimNatConstr :: Word -> Constr+dimNatConstr d = mkConstr (dimDataType d) ("D" ++ show d) [] Prefix++instance KnownDim d => G.Generic (Dim (d :: Nat)) where+    type Rep (Dim d) = G.D1+          ('G.MetaData "Dim" "Numeric.Dim" "dimensions" 'False)+          (G.C1 ('G.MetaCons (AppendSymbol "D" (ShowNat d)) 'G.PrefixI 'False) G.U1)+    from D = G.M1 (G.M1 G.U1)+    to = const (dim @d)++instance Eq (Dim (n :: Nat)) where+    (==) = const (const True)+    {-# INLINE (==) #-}+    (/=) = const (const False)+    {-# INLINE (/=) #-}++instance Eq (Dim (x :: XNat)) where+    (==) = coerce ((==) :: Word -> Word -> Bool)+    {-# INLINE (==) #-}+    (/=) = coerce ((/=) :: Word -> Word -> Bool)+    {-# INLINE (/=) #-}++instance Eq (Dims (ds :: [Nat])) where+    (==) = const (const True)+    {-# INLINE (==) #-}+    (/=) = const (const False)+    {-# INLINE (/=) #-}++instance Eq (Dims (ds :: [XNat])) where+    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)+    {-# INLINE (==) #-}+    (/=) = unsafeCoerce# ((/=) :: [Word] -> [Word] -> Bool)+    {-# INLINE (/=) #-}++instance Eq SomeDims where+    SomeDims as == SomeDims bs = listDims as == listDims bs+    {-# INLINE (==) #-}+    SomeDims as /= SomeDims bs = listDims as /= listDims bs+    {-# INLINE (/=) #-}++instance Ord (Dim (n :: Nat)) where+    compare = const (const EQ)+    {-# INLINE compare #-}++instance Ord (Dim (x :: XNat)) where+    compare = coerce (compare :: Word -> Word -> Ordering)+    {-# INLINE compare #-}++instance Ord (Dims (ds :: [Nat])) where+    compare = const (const EQ)+    {-# INLINE compare #-}++instance Ord (Dims (ds :: [XNat])) where+    compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering)+    {-# INLINE compare #-}++instance Ord SomeDims where+    compare (SomeDims as) (SomeDims bs) = compare (listDims as) (listDims bs)+    {-# INLINE compare #-}++instance Show (Dim (x :: k)) where+    showsPrec _ d = showChar 'D' . shows (dimVal d)+    {-# INLINE showsPrec #-}++instance Show (Dims (xs :: [k])) where+    showsPrec = typedListShowsPrec @k @Dim @xs showsPrec++instance Show SomeDims where+    showsPrec p (SomeDims ds)+      = showParen (p >= 10)+      $ showString "SomeDims " . showsPrec 10 ds++instance BoundedDim x => Read (Dim (x :: k)) where+    readPrec = Read.lexP >>= \case+      Read.Ident ('D':s)+        | Just d <- Read.readMaybe s+            >>= constrainDim @k @x @XNat @(XN 0) . DimSing+          -> return d+      _  -> Read.pfail+    readList = Read.readListDefault+    readListPrec = Read.readListPrecDefault++instance BoundedDims xs => Read (Dims (xs :: [k])) where+    readPrec = case inferAllBoundedDims @k @xs of+        Dict -> typedListReadPrec @k @BoundedDim ":*" Read.readPrec (tList @k @xs)+    readList = Read.readListDefault+    readListPrec = Read.readListPrecDefault++instance Read SomeDims where+    readPrec = Read.parens . Read.prec 10 $ do+      Read.lift . Read.expect $ Read.Ident "SomeDims"+      withTypedListReadPrec @Nat @Dim @SomeDims+        (\g -> (\(Dx d) -> g d) <$> Read.readPrec @(Dim (XN 0)))+        SomeDims++++-- | This function does GHC's magic to convert user-supplied `dim` function+--   to create an instance of `KnownDim` typeclass at runtime.+--   The trick is taken from Edward Kmett's reflection library explained+--   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection+reifyDim :: forall (r :: Type) (d :: Nat) . Dim d -> (KnownDim d => r) -> r+reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d+{-# INLINE reifyDim #-}+newtype MagicDim (d :: Nat) (r :: Type) = MagicDim (KnownDim d => r)++reifyNat :: forall (r :: Type) (d :: Nat) . Natural -> (KnownNat d => r) -> r+reifyNat d k = unsafeCoerce# (MagicNat k :: MagicNat d r) d+{-# INLINE reifyNat #-}+newtype MagicNat (d :: Nat) (r :: Type) = MagicNat (KnownNat d => r)++dimEv :: forall (d :: Nat) . Dim d -> Dict (KnownDim d)+dimEv d = reifyDim d Dict+{-# INLINE dimEv #-}++reifyDims :: forall (r :: Type) (ds :: [Nat]) . Dims ds -> (Dimensions ds => r) -> r+reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds+{-# INLINE reifyDims #-}+newtype MagicDims (ds :: [Nat]) (r :: Type) = MagicDims (Dimensions ds => r)++dimsEv :: forall (ds :: [Nat]) . Dims ds -> Dict (Dimensions ds)+dimsEv ds = reifyDims ds Dict+{-# INLINE dimsEv #-}+++data PatXDim (xn :: XNat) where+  PatN :: KnownDim n => Dim n -> PatXDim ('N n)+  PatXN :: (KnownDim n, m <= n) => Dim n -> PatXDim ('XN m)++dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn+dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd)+  where+    dd = DimSing @Nat @_ k+dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn)+  where+    dd = DimSing @Nat @_ k+    f :: forall (d :: Nat) (m :: Nat)+       . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m)+    f d = case unsafeCoerceDict @(m <= m) @(m <= d) Dict of+      Dict -> const (PatXN d)+{-# INLINE dimXNEv #-}++data PatXDims (xns :: [XNat])+  = forall (ns :: [Nat])+  . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)++patXDims :: forall (xns :: [XNat])+          . All KnownXNatType xns => Dims xns -> PatXDims xns+patXDims U = PatXDims U+patXDims (Dn n :* xns) = case patXDims xns of+  PatXDims ns -> PatXDims (n :* ns)+patXDims (Dx n :* xns) = case patXDims xns of+  PatXDims ns -> PatXDims (n :* ns)+{-# INLINE patXDims #-}++data PatAsXDims (ns :: [Nat])+  = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))+  => PatAsXDims (Dims (AsXDims ns))++patAsXDims :: forall (ns :: [Nat]) . Dims ns -> PatAsXDims ns+patAsXDims U = PatAsXDims U+patAsXDims (n@D :* ns) = case patAsXDims ns of+  PatAsXDims xns -> PatAsXDims (Dn n :* xns)+{-# INLINE patAsXDims #-}++data PatKDims (ns :: [Nat])+  = (All KnownDim ns, All BoundedDim ns, RepresentableList ns, Dimensions ns) => PatKDims++patKDims :: forall (ns :: [Nat]) . Dims ns -> PatKDims ns+patKDims U = PatKDims+patKDims (D :* ns) = case patKDims ns of+  PatKDims -> PatKDims+{-# INLINE patKDims #-}++unsafeCoerceDict :: forall (a :: Constraint) (b :: Constraint)+                  . Dict a -> Dict b+unsafeCoerceDict = unsafeCoerce#

@@ -0,0 +1,13 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeInType     #-}+{-# LANGUAGE TypeOperators  #-}+-- This module recursively depends on Numeric.TypedList.+-- I thought hs-boot is better than orphan instances.+module Numeric.Dimensions.Dim ( Dim, Nat, dimVal, minusDimM ) where+import Data.Kind      (Type)+import Data.Type.Lits (type (-), Nat)+newtype Dim (x :: k) = DimSing Word+dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word+minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m))

@@ -1,440 +0,0 @@-{-# OPTIONS_GHC -fno-warn-orphans      #-}-{-# LANGUAGE AllowAmbiguousTypes       #-}-{-# LANGUAGE CPP                       #-}-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE FlexibleInstances         #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE MagicHash                 #-}-{-# LANGUAGE MultiParamTypeClasses     #-}-{-# LANGUAGE PatternSynonyms           #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE RoleAnnotations           #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeFamilies              #-}-{-# LANGUAGE TypeFamilyDependencies    #-}-{-# LANGUAGE TypeInType                #-}-{-# LANGUAGE TypeOperators             #-}-{-# LANGUAGE UndecidableInstances      #-}-{-# LANGUAGE UndecidableSuperClasses   #-}-{-# LANGUAGE ViewPatterns              #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Dims--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Provides a data type `Dims ds` to keep dimension sizes--- for multiple-dimensional data.--- Lower indices go first, i.e. assumed enumeration---          is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).-----------------------------------------------------------------------------------module Numeric.Dimensions.Dims-  ( Dims, SomeDims (..), Dimensions (..), XDimensions (..)-  , TypedList ( Dims, XDims, AsXDims, KnownDims-              , U, (:*), Empty, TypeList, Cons, Snoc, Reverse)-  , listDims, someDimsVal, totalDim, totalDim'-  , sameDims, sameDims'-  , compareDims, compareDims'-  , inSpaceOf, asSpaceOf-  , xDims, xDims'-    -- * Type-level programming-    --   Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`)-  , AsXDims, AsDims, FixedDims, KnownXNatTypes, type (:<), type (>:)-    -- * Re-export type list-  , RepresentableList (..), TypeList, types-  , order, order'-    -- * Re-export single dimension type and functions-  , module Numeric.Dim-  ) where----import           GHC.Exts              (unsafeCoerce#, Constraint)-import qualified Text.Read             as Read--import           Numeric.Dim-import           Numeric.Type.Evidence-import           Numeric.Type.List-import           Numeric.TypedList     (RepresentableList (..), TypeList,-                                        TypedList (..), order, order', types)----- | Type-level dimensionality O(1).-type Dims (xs :: [k]) = TypedList Dim xs---- Starting from GHC 8.2, compiler supports specifying lists of complete--- pattern synonyms.-#if __GLASGOW_HASKELL__ >= 802-{-# COMPLETE Dims #-}-{-# COMPLETE XDims #-}-{-# COMPLETE AsXDims #-}-{-# COMPLETE KnownDims #-}-#endif---- | @O(1)@ Pattern-matching against this constructor brings a `Dimensions`---   instance into the scope.---   Thus, you can do arbitrary operations on your dims and use this pattern---   at any time to reconstruct the class instance at runtime.-pattern Dims :: forall ds . () => Dimensions ds => Dims ds-pattern Dims <- (dimsEv -> E)-  where-    Dims = dims @_ @ds---- | @O(Length ds)@ `Dimensions` and `KnownDim` for each individual dimension.-pattern KnownDims :: forall ds . ()-                  => (All KnownDim ds, Dimensions ds) => Dims ds-pattern KnownDims <- (patKDims -> PatKDims)-  where-    KnownDims = dims @_ @ds----- | Pattern-matching against this constructor reveals Nat-kinded list of dims,---   pretending the dimensionality is known at compile time within the scope---   of the pattern match.---   This is the main recommended way to get `Dims` at runtime;---   for example, reading a list of dimensions from a file.------   In order to use this pattern, one must know @XNat@ type constructors in---   each dimension at compile time.-pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns-              => forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns)-              => Dims ns -> Dims xns-pattern XDims ns <- (patXDims -> PatXDims ns)-  where-    XDims ns = unsafeCoerce# ns---- | An easy way to convert Nat-indexed dims into XNat-indexed dims.-pattern AsXDims :: forall (ns :: [Nat]) . ()-                => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))-                => Dims (AsXDims ns) -> Dims ns-pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns)-  where-    AsXDims xns = unsafeCoerce# xns---- | Same as SomeNat, but for Dimensions:---   Hide all information about Dimensions inside-data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)---- | Put runtime evidence of `Dims` value inside function constraints.---   Similar to `KnownDim` or `KnownNat`, but for lists of numbers.---   Normally, the kind paramater is `Nat` (known dimenionality)---   or `XNat` (either known or constrained dimensionality).-class Dimensions (ds :: [k]) where-    -- | Get dimensionality of a space at runtime,-    --   represented as a list of `Dim`.-    ---    --   Note, this function is supposed to be used with @TypeApplications@,-    --   and the @Dimensions@ class has varying kind of the parameter;-    --   thus, the function has two type paremeters (kind and type of @ds@).-    --   For example, you can type:-    ---    --   >>>:set -XTypeApplications-    --   >>>:set -XDataKinds-    --   >>>:t dims @_ @'[N 17, N 12]-    --   dims @_ @'[N 17, N 12] :: Dims '[N 17, N 12]-    ---    --   >>>:t dims @XNat @'[]-    --   dims @XNat @'[] :: Dims '[]-    ---    ---    --   >>>:t dims @_ @(Tail '[3,2,5,7])-    --   dims @_ @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]-    ---    dims :: Dims ds--instance Dimensions ('[] :: [k]) where-    dims = U-    {-# INLINE dims #-}--instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds :: [k]) where-    dims = dim :* dims-    {-# INLINE dims #-}---- | Analogous to `Dimensions`, but weaker and more specific (list of `XNat`).---   This class is used to check if an existing fixed `Dims` satisfy---   constraints imposed by some interface (e.g. all dimensions are greater than 2).---   It is weaker than `Dimensions` in that it only requires knowledge of constraints---   rather than exact dimension values.-class KnownXNatTypes xds => XDimensions (xds :: [XNat]) where-    -- | Given a `Dims`, test if its runtime value satisfies constraints imposed by-    --   @XDimensions@, and returns it back being `XNat`-indexed on success.-    ---    --   This function allows to guess safely individual dimension values,-    --   as well as the length of the dimension list.-    constrainDims :: Dims (ds :: [k]) -> Maybe (Dims xds)--instance XDimensions '[] where-    constrainDims U = Just U-    constrainDims _ = Nothing-    {-# INLINE constrainDims #-}--instance (XDimensions xs, KnownDim m) => XDimensions (XN m ': xs) where-    constrainDims (d :* ds) = case constrain d of-      Nothing -> Nothing-      Just xd -> (xd :*) <$> constrainDims ds-    constrainDims Empty = Nothing--instance (XDimensions xs, KnownDim n) => XDimensions (N n ': xs) where-    constrainDims (d :* ds)-      | unsafeCoerce# d == dimVal' @n = (Dn D :*) <$> constrainDims ds-      | otherwise                     = Nothing-    constrainDims Empty = Nothing----- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@.-listDims :: Dims xs -> [Word]-listDims = unsafeCoerce#-{-# INLINE listDims #-}---- | Convert a plain haskell list of dimension sizes into an unknown---   type-level dimensionality  @O(1)@.-someDimsVal :: [Word] -> SomeDims-someDimsVal = SomeDims . unsafeCoerce#-{-# INLINE someDimsVal #-}---- | Product of all dimension sizes @O(Length xs)@.-totalDim :: Dims xs -> Word-totalDim = product . listDims-{-# INLINE totalDim #-}---- | Product of all dimension sizes @O(Length xs)@.-totalDim' :: forall xs . Dimensions xs => Word-totalDim' = totalDim (dims @_ @xs)-{-# INLINE totalDim' #-}---- | Get XNat-indexed dims given their fixed counterpart.-xDims :: FixedDims xns ns => Dims ns -> Dims xns-xDims = unsafeCoerce#-{-# INLINE xDims #-}---- | Get XNat-indexed dims given their fixed counterpart.-xDims' :: forall xns ns . (FixedDims xns ns, Dimensions ns) => Dims xns-xDims' = xDims @xns (dims @Nat @ns)-{-# INLINE xDims' #-}----- | We either get evidence that this function was instantiated with the---   same type-level Dimensions, or 'Nothing' @O(Length xs)@.------   Note, this function works on @Nat@-indexed dimensions only,---   because @Dims '[XN x]@ does not have runtime evidence to infer @x@---   and `KnownDim x` does not imply `KnownDim (XN x)`.-sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs))-sameDims as bs-  | listDims as == listDims bs-    = Just (unsafeCoerce# (E @('[] ~ '[])))-  | otherwise = Nothing-{-# INLINE sameDims #-}----- | We either get evidence that this function was instantiated with the---   same type-level Dimensions, or 'Nothing' @O(Length xs)@.-sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) p q-           . (Dimensions as, Dimensions bs)-          => p as -> q bs -> Maybe (Evidence (as ~ bs))-sameDims' _ _ = sameDims (dims @Nat @as) (dims @Nat @bs)-{-# INLINE sameDims' #-}---- | Compare dimensions by their size in lexicorgaphic order---   from the last dimension to the first dimension---   (the last dimension is the most significant one).------   Literally,------   > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)-compareDims :: Dims as -> Dims bs -> Ordering-compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)-{-# INLINE compareDims #-}---- | Compare dimensions by their size in lexicorgaphic order---   from the last dimension to the first dimension---   (the last dimension is the most significant one) @O(Length xs)@.------   Literally,------   > compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)------   This is the same @compare@ rule, as for `Idxs`.-compareDims' :: forall as bs p q-              . (Dimensions as, Dimensions bs)-             => p as -> q bs -> Ordering-compareDims' _ _ = compareDims (dims @_ @as) (dims @_ @bs)-{-# INLINE compareDims' #-}----- | Similar to `const` or `asProxyTypeOf`;---   to be used on such implicit functions as `dim`, `dimMax`, etc.-inSpaceOf :: a ds -> b ds -> a ds-inSpaceOf x _ = x-{-# INLINE inSpaceOf #-}---- | Similar to `asProxyTypeOf`,---   Give a hint to type checker to fix the type of a function argument.-asSpaceOf :: a ds -> (b ds -> c) -> (b ds -> c)-asSpaceOf _ = id-{-# INLINE asSpaceOf #-}---instance Eq (Dims (ds :: [Nat])) where-    (==) _ _ = True--instance Eq (Dims (ds :: [XNat])) where-    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)--instance Eq SomeDims where-    SomeDims as == SomeDims bs = listDims as == listDims bs--instance Ord (Dims (ds :: [Nat])) where-    compare _ _ = EQ--instance Ord (Dims (ds :: [XNat])) where-    compare = compareDims--instance Ord SomeDims where-    compare (SomeDims as) (SomeDims bs) = compareDims as bs--instance Show (Dims xs) where-    show ds = "Dims " ++ show (listDims ds)-    showsPrec p ds-      = showParen (p >= 10)-      $ showString "Dims " . showsPrec p (listDims ds)--instance Show SomeDims where-    show (SomeDims ds) = "SomeDims " ++ show (listDims ds)-    showsPrec p (SomeDims ds)-      = showParen (p >= 10)-      $ showString "SomeDims " . showsPrec p (listDims ds)--instance Read SomeDims where-    readPrec = Read.parens $ Read.prec 10 $ do-      s <- Read.lexP-      if s == Read.Ident "SomeDims"-      then someDimsVal <$> Read.readPrec-      else Read.pfail--instance Dimensions ds => Bounded (Dims ds) where-    maxBound = dims-    {-# INLINE maxBound #-}-    minBound = dims-    {-# INLINE minBound #-}------ | Map Dims onto XDims (injective)-type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where-    AsXDims '[] = '[]-    AsXDims (n ': ns) = N n ': AsXDims ns---- | Map XDims onto Dims (injective)-type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where-    AsDims '[] = '[]-    AsDims (N x ': xs) = x ': AsDims xs---- | Constrain @Nat@ dimensions hidden behind @XNat@s.-type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where-    FixedDims '[] ns = (ns ~ '[])-    FixedDims (xn ': xns) ns-      = ( ns ~ (Head ns ': Tail ns)-        , FixedDim xn (Head ns)-        , FixedDims xns (Tail ns))---- | Know the structure of each dimension-type KnownXNatTypes xns = All KnownXNatType xns----- | Synonym for (:+) that treats Nat values 0 and 1 in a special way:---   it preserves the property that all dimensions are greater than 1.-type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where-    0 :< _  = '[]-    1 :< ns = ns-    n :< ns = n :+ ns-infixr 6 :<---- | Synonym for (+:) that treats Nat values 0 and 1 in a special way:---   it preserves the property that all dimensions are greater than 1.-type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where-    _  >: 0 = '[]-    ns >: 1 = ns-    ns >: n = ns +: n-infixl 6 >:------------------------------------------------------------------------------------------- | This function does GHC's magic to convert user-supplied `dims` function---   to create an instance of `Dimensions` typeclass at runtime.---   The trick is taken from Edward Kmett's reflection library explained---   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection-reifyDims :: forall r ds . Dims ds -> ( Dimensions ds => r) -> r-reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds-{-# INLINE reifyDims #-}-newtype MagicDims ds r = MagicDims (Dimensions ds => r)--dimsEv :: Dims ds -> Evidence (Dimensions ds)-dimsEv ds = reifyDims ds E-{-# INLINE dimsEv #-}---data PatXDims (xns :: [XNat])-  = forall (ns :: [Nat])-  . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)---patXDims :: All KnownXNatType xns => Dims xns -> PatXDims xns-patXDims U = PatXDims U-patXDims (Dn n :* xns) = case patXDims xns of-  PatXDims ns -> PatXDims (n :* ns)-patXDims (Dx n :* xns) = case patXDims xns of-  PatXDims ns -> PatXDims (n :* ns)-#if __GLASGOW_HASKELL__ >= 802-#else-patXDims _ = error "XDims/patXDims: impossible argument"-#endif-{-# INLINE patXDims #-}---data PatAsXDims (ns :: [Nat])-  = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))-  => PatAsXDims (Dims (AsXDims ns))---patAsXDims :: Dims ns -> PatAsXDims ns-patAsXDims U = PatAsXDims U-patAsXDims (n@D :* ns) = case patAsXDims ns of-  PatAsXDims xns -> PatAsXDims (Dn n :* xns)-#if __GLASGOW_HASKELL__ >= 802-#else-patAsXDims _ = error "AsXDims/patAsXDims: impossible argument"-#endif-{-# INLINE patAsXDims #-}----data PatKDims (ns :: [k])-  = (All KnownDim ns, Dimensions ns) => PatKDims---patKDims :: Dims ns -> PatKDims ns-patKDims U = PatKDims-patKDims (Dim :* ns) = case patKDims ns of-  PatKDims -> PatKDims-#if __GLASGOW_HASKELL__ >= 802-#else-patKDims _ = error "Dims/patKDims: impossible argument"-#endif-{-# INLINE patKDims #-}

@@ -1,334 +0,0 @@-{-# LANGUAGE PolyKinds #-}--- Workaround weird behavior of GHC 8.4-{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Fold--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Fold a function over all dimensions provided dimension indices or offsets.--- The main purpose of this module is to fold or traverse flat data arrays--- following the shape of dimensions associated with them.----------------------------------------------------------------------------------module Numeric.Dimensions.Fold-  ( overDim, overDim_, overDimIdx, overDimIdx_-  , overDimOff, overDimOff_-  , overDimReverse, overDimReverseIdx-  , foldDim, foldDimIdx, foldDimOff-  , foldDimReverse, foldDimReverseIdx-  , overDimPart, overDimPartIdx-  ) where---import           Control.Monad           ((>=>))-import           Numeric.Dimensions.Idxs---- | Go over all dimensions keeping track of index and offset-overDim :: Monad m-        => Dims ds -- ^ Shape of a space-        -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension-        -> Int -- ^ Initial offset-        -> Int -- ^ Offset step-        -> a -- ^ Initial value-        -> m a-overDim U k offset _step = k U offset-overDim (d :* ds) k offset step = overDim ds k' offset (di * step)-  where-    dw = dimVal d-    di = fromIntegral dw-    k' is = go 1-      where-        go i off-          | i > dw = return-          | otherwise = k (Idx i :* is) off >=> go (i+1) (off+step)-{-# INLINE overDim #-}---- | Go over all dimensions in reverse order keeping track of index and offset-overDimReverse :: Monad m-               => Dims ds -- ^ Shape of a space-               -> (Idxs ds -> Int -> a -> m a) -- ^ Function to call on each dimension-               -> Int -- ^ Initial offset-               -> Int -- ^ Offset step (substracted from initial offset)-               -> a -- ^ Initial value-               -> m a-overDimReverse U k offset _step = k U offset-overDimReverse (d :* ds) k offset step = overDimReverse ds k' offset (di * step)-  where-    dw = dimVal d-    di = fromIntegral dw-    k' is = go dw-      where-        go i off-          | i <= 0 = return-          | otherwise = k (Idx i :* is) off >=> go (i-1) (off-step)-{-# INLINE overDimReverse #-}---- | Go over all dimensions keeping track of index and offset-overDim_ :: Monad m-         => Dims ds -- ^ Shape of a space-         -> (Idxs ds -> Int -> m ()) -- ^ Function to call on each dimension-         -> Int -- ^ Initial offset-         -> Int -- ^ Offset step-         -> m ()-overDim_ U k offset _step = k U offset-overDim_ (d :* ds) k offset step = overDim_ ds k' offset (di * step)-  where-    dw = dimVal d-    di = fromIntegral dw-    k' is = go 1-      where-        go i off-          | i > dw = return ()-          | otherwise = k (Idx i :* is) off >> go (i+1) (off+step)-{-# INLINE overDim_ #-}---- | Go over all dimensions keeping track of index-overDimIdx :: Monad m-           => Dims ds -- ^ Shape of a space-           -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension-           -> a -- ^ Initial value-           -> m a-overDimIdx U k = k U-overDimIdx (d :* ds) k = overDimIdx ds k'-  where-    dw = dimVal d-    k' is = go 1-      where-        go i-          | i > dw = return-          | otherwise = k (Idx i :* is) >=> go (i+1)-{-# INLINE overDimIdx #-}---- | Go over all dimensions keeping track of index-overDimIdx_ :: Monad m-            => Dims ds -- ^ Shape of a space-            -> (Idxs ds -> m ()) -- ^ Function to call on each dimension-            -> m ()-overDimIdx_ U k = k U-overDimIdx_ (d :* ds) k = overDimIdx_ ds k'-  where-    dw = dimVal d-    k' is = go 1-      where-        go i-          | i > dw = return ()-          | otherwise = k (Idx i :* is) >> go (i+1)-{-# INLINE overDimIdx_ #-}----- | Go over all dimensions keeping track of total offset-overDimOff :: Monad m-           => Dims ds -- ^ Shape of a space-           -> (Int -> a -> m a) -- ^ Function to call with each offset value-           -> Int -- ^ Initial offset-           -> Int -- ^ Offset step-           -> a -- ^ Initial value-           -> m a-overDimOff ds k offset step = go (totalDim ds) offset-  where-    go i off-          | i == 0 = return-          | otherwise = k off >=> go (i-1) (off+step)-{-# INLINE overDimOff #-}---- | Go over all dimensions keeping track of total offset-overDimOff_ :: Monad m-            => Dims ds -- ^ Shape of a space-            -> (Int -> m ()) -- ^ Function to call with each offset value-            -> Int -- ^ Initial offset-            -> Int -- ^ Offset step-            -> m ()-overDimOff_ ds k offset step = go (totalDim ds) offset-  where-    go i off-          | i == 0 = return ()-          | otherwise = k off >> go (i-1) (off+step)-{-# INLINE overDimOff_ #-}----- | Go over all dimensions in reverse order keeping track of index-overDimReverseIdx :: Monad m-                  => Dims ds -- ^ Shape of a space-                  -> (Idxs ds -> a -> m a) -- ^ Function to call on each dimension-                  -> a -- ^ Initial value-                  -> m a-overDimReverseIdx U k = k U-overDimReverseIdx (d :* ds) k = overDimReverseIdx ds k'-  where-    dw = dimVal d-    k' is = go dw-      where-        go i-          | i <= 0 = return-          | otherwise = k (Idx i :* is) >=> go (i-1)-{-# INLINE overDimReverseIdx #-}------ | Fold over all dimensions keeping track of index and offset-foldDim :: Dims ds -- ^ Shape of a space-        -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension-        -> Int -- ^ Initial offset-        -> Int -- ^ Offset step-        -> a -- ^ Initial value-        -> a-foldDim U k offset _step = k U offset-foldDim (d :* ds) k offset step = foldDim ds k' offset (di * step)-  where-    dw = dimVal d-    di = fromIntegral dw-    k' is = go 1-      where-        go i off-          | i > dw = id-          | otherwise = go (i+1) (off+step) . k (Idx i :* is) off-{-# INLINE foldDim #-}---- | Fold over all dimensions in reverse order keeping track of index and offset-foldDimReverse :: Dims ds -- ^ Shape of a space-               -> (Idxs ds -> Int -> a -> a) -- ^ Function to call on each dimension-               -> Int -- ^ Initial offset-               -> Int -- ^ Offset step (substracted from initial offset)-               -> a -- ^ Initial value-               -> a-foldDimReverse U k offset _step = k U offset-foldDimReverse (d :* ds) k offset step = foldDimReverse ds k' offset (di * step)-  where-    dw = dimVal d-    di = fromIntegral dw-    k' is = go dw-      where-        go i off-          | i <= 0 = id-          | otherwise = go (i-1) (off-step) . k (Idx i :* is) off-{-# INLINE foldDimReverse #-}------ | Fold over all dimensions keeping track of index-foldDimIdx :: Dims ds -- ^ Shape of a space-           -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension-           -> a -- ^ Initial value-           -> a-foldDimIdx U k = k U-foldDimIdx (d :* ds) k = foldDimIdx ds k'-  where-    dw = dimVal d-    k' is = go 1-      where-        go i-          | i > dw = id-          | otherwise = go (i+1) . k (Idx i :* is)-{-# INLINE foldDimIdx #-}----- | Fold over all dimensions keeping track of total offset-foldDimOff :: Dims ds -- ^ Shape of a space-           -> (Int -> a -> a) -- ^ Function to call on each dimension-           -> Int -- ^ Initial offset-           -> Int -- ^ Offset step-           -> a -- ^ Initial value-           -> a-foldDimOff ds k offset step = go (totalDim ds) offset-  where-    go i off-          | i == 0 = id-          | otherwise = go (i-1) (off+step) . k off-{-# INLINE foldDimOff #-}----- | Fold over all dimensions in reverse order keeping track of index-foldDimReverseIdx :: Dims ds -- ^ Shape of a space-                  -> (Idxs ds -> a -> a) -- ^ Function to call on each dimension-                  -> a -- ^ Initial value-                  -> a-foldDimReverseIdx U k = k U-foldDimReverseIdx (d :* ds) k = foldDimReverseIdx ds k'-  where-    dw = dimVal d-    k' is = go dw-      where-        go i-          | i <= 0 = id-          | otherwise = go (i-1) . k (Idx i :* is)-{-# INLINE foldDimReverseIdx #-}----- | Traverse from the first index to the second index in each dimension.---   You can combine positive and negative traversal directions---   along different dimensions.------   Note, initial and final indices are included in the range;---   the argument function is guaranteed to execute at least once.-overDimPart :: (Dimensions ds, Monad m)-            => Idxs ds -- ^ Initial indices-            -> Idxs ds -- ^ Final indices-            -> (Idxs ds -> Int -> a -> m a)-                       -- ^ Function to call on each dimension-            -> Int     -- ^ Initial offset (at index @minBound :: Idxs ds@)-                       --   Note, this is not an offset value at initial indices.-            -> Int     -- ^ Offset step-            -> a       -- ^ initial value-            -> m a-overDimPart imin imax f offset step = overDimPart' stepSizes imin imax f offset-    where-      stepSizes = createStepSizes (dims `inSpaceOf` imin) step--      createStepSizes :: Dims ns -> Int -> TypedList StepSize ns-      createStepSizes U _ = U-      createStepSizes (d :* ds) k-        = StepSize k :* createStepSizes ds (k * fromIntegral (dimVal d))--overDimPart' :: Monad m-             => TypedList StepSize ns-             -> Idxs ds -> Idxs ds-             -> (Idxs ds -> Int -> a -> m a)-             -> Int-             -> a -> m a-overDimPart' U U U k off0 = k U off0-overDimPart' (siW :* iws) (Idx iStart :* starts) (Idx iEnd :* ends) k off0-  | iEnd >= iStart = overDimPart' iws starts ends (loop iStart) (off0 + headOff)-  | otherwise      = overDimPart' iws starts ends (looi iStart) (off0 + headOff)-  where-    StepSize iW = siW-    headOff = iW * (fromIntegral iStart - 1)-    loop i js off-      | i > iEnd = return-      | otherwise = k (Idx i :* js) off >=> loop (i+1) js (off + iW)-    looi i js off-      | i < iEnd = return-      | otherwise = k (Idx i :* js) off >=> looi (i-1) js (off - iW)---newtype StepSize n = StepSize Int---- | Traverse from the first index to the second index in each dimension.---   You can combine positive and negative traversal directions---   along different dimensions.------   Note, initial and final indices are included in the range;---   the argument function is guaranteed to execute at least once.-overDimPartIdx :: Monad m-               => Idxs ds -- ^ Initial indices-               -> Idxs ds -- ^ Final indices-               -> (Idxs ds -> a -> m a)-                          -- ^ Function to call on each dimension-               -> a       -- ^ initial value-               -> m a-overDimPartIdx U U k = k U-overDimPartIdx (start :* starts) (end :* ends) k-  | iEnd >= iStart = overDimPartIdx starts ends (loop iStart)-  | otherwise      = overDimPartIdx starts ends (looi iStart)-  where-    Idx iStart = start-    Idx iEnd   = end-    loop i is-      | i > iEnd = return-      | otherwise = k (Idx i :* is) >=> loop (i+1) is-    looi i is-      | i < iEnd = return-      | otherwise = k (Idx i :* is) >=> looi (i-1) is

@@ -0,0 +1,483 @@+{-# LANGUAGE AllowAmbiguousTypes        #-}+{-# LANGUAGE CPP                        #-}+{-# LANGUAGE ConstraintKinds            #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE DeriveDataTypeable         #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE ExistentialQuantification  #-}+{-# LANGUAGE ExplicitNamespaces         #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MagicHash                  #-}+{-# LANGUAGE PatternSynonyms            #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE UnboxedTuples              #-}+{-# LANGUAGE UndecidableInstances       #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Numeric.Dimensions.Idx+-- Copyright   :  (c) Artem Chirkin+-- License     :  BSD3+--+--+-- Provides a data type `Idx` to index `Dim` and `Idxs`+--   that enumerates through multiple dimensions.+--+-- Higher indices go first, i.e. assumed enumeration+--          is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik+-- This corresponds to row-first layout of matrices and multidimenional arrays.+--+-----------------------------------------------------------------------------++module Numeric.Dimensions.Idx+  ( -- * Data types+    Idx (Idx), Idxs+  , idxFromWord, unsafeIdxFromWord, idxToWord+  , listIdxs, idxsFromWords+  ) where+++import           Data.Coerce+import           Data.Constraint  (Dict (..))+import           Data.Data        (Data)+import           Foreign.Storable (Storable)+import           GHC.Enum+import           GHC.Generics     (Generic)+import qualified Text.Read        as P++#ifdef UNSAFE_INDICES+import GHC.Base (Int (..), Type, Word (..), int2Word#, unsafeCoerce#, word2Int#)+#else+import GHC.Base (Int (..), Type, Word (..), int2Word#, maxInt, plusWord2#,+                 timesWord2#, unsafeCoerce#, word2Int#)+#endif++import Numeric.Dimensions.Dim+import Numeric.TypedList      (typedListReadPrec, typedListShowsPrec)+++-- | This type is used to index a single dimension;+--   the range of indices is from @0@ to @n-1@.+--+newtype Idx (n :: k) = Idx' Word+  deriving ( Data, Generic, Integral, Real, Storable, Eq, Ord )+++-- | Convert between `Word` and `Idx`.+--+--   If the word is outside of the bounds, fails with an error+--     (unless @unsafeindices@ flag is turned on).+--+pattern Idx :: forall (k :: Type) (n :: k) . BoundedDim n => Word -> Idx n+pattern Idx w <- Idx' w+  where+    Idx = unsafeIdxFromWord+{-# COMPLETE Idx #-}++-- | Type-level dimensional indexing with arbitrary Word values inside.+--   Most of the operations on it require `Dimensions` constraint,+--   because the @Idxs@ itself does not store info about dimension bounds.+type Idxs (xs :: [k]) = TypedList Idx xs++-- | Convert an arbitrary Word to @Idx@.+--+--   If the word is outside of the bounds, fails with an error+--     (unless @unsafeindices@ flag is turned on).+--+unsafeIdxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Idx d+#ifdef UNSAFE_INDICES+unsafeIdxFromWord = coerce+#else+unsafeIdxFromWord w+  | w < d     = coerce w+  | otherwise = errorWithoutStackTrace+              $ "idxFromWord{" ++ showIdxType @k @d ++ "}: word "+              ++ show w ++ " is outside of index bounds."+  where+    d = dimVal (dimBound @k @d)+#endif+{-# INLINE unsafeIdxFromWord #-}++-- | Convert an arbitrary Word to @Idx@.+idxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Maybe (Idx d)+idxFromWord w+  | w < dimVal (dimBound @k @d) = Just (coerce w)+  | otherwise                   = Nothing+{-# INLINE idxFromWord #-}++-- | Get the value of an @Idx@.+idxToWord :: forall (k :: Type) (d :: k) . Idx d -> Word+idxToWord = coerce+{-# INLINE idxToWord #-}++{-# RULES+"fromIntegral/idxToWord"+  fromIntegral = idxToWord+  #-}++listIdxs :: forall (k :: Type) (xs :: [k]) . Idxs xs -> [Word]+listIdxs = unsafeCoerce#+{-# INLINE listIdxs #-}++idxsFromWords :: forall (k :: Type) (xs :: [k])+               . BoundedDims xs => [Word] -> Maybe (Idxs xs)+idxsFromWords = unsafeCoerce# . go (listDims (dimsBound @k @xs))+  where+    go :: [Word] -> [Word] -> Maybe [Word]+    go [] [] = Just []+    go (d : ds) (i : is)+      | i < d = (i:) <$> go ds is+    go _ _   = Nothing++++instance BoundedDim x => Read (Idx (x :: k)) where+    readPrec = do+      w <- P.readPrec+      if w < dimVal (dimBound @k @x)+      then return (Idx' w)+      else P.pfail+    readList = P.readListDefault+    readListPrec = P.readListPrecDefault++instance Show (Idx (x :: k)) where+    showsPrec = coerce (showsPrec :: Int -> Word -> ShowS)++instance BoundedDim n => Bounded (Idx (n :: k)) where+    minBound = 0+    {-# INLINE minBound #-}+    maxBound = coerce (dimVal(dimBound @k @n)  - 1)+    {-# INLINE maxBound #-}++instance BoundedDim n => Enum (Idx (n :: k)) where++#ifdef UNSAFE_INDICES+    succ = coerce ((+ 1) :: Word -> Word)+#else+    succ x@(Idx' i)+      | x < maxBound = coerce (i + 1)+      | otherwise = succError $ showIdxType @k @n+#endif+    {-# INLINE succ #-}++#ifdef UNSAFE_INDICES+    pred = coerce (subtract 1 :: Word -> Word)+#else+    pred x@(Idx' i)+      | x > minBound = coerce (i - 1)+      | otherwise = predError $ showIdxType @k @n+#endif+    {-# INLINE pred #-}++#ifdef UNSAFE_INDICES+    toEnum (I# i#) = coerce (W# (int2Word# i#))+#else+    toEnum i+        | i >= 0 && i' < d = coerce i'+        | otherwise        = toEnumError (showIdxType @k @n) i (0, d - 1)+      where+        d  = dimVal (dimBound @k @n)+        i' = fromIntegral i+#endif+    {-# INLINE toEnum #-}++#ifdef UNSAFE_INDICES+    fromEnum (Idx' (W# w#)) = I# (word2Int# w#)+#else+    fromEnum (Idx' x@(W# w#))+        | x <= maxIntWord = I# (word2Int# w#)+        | otherwise       = fromEnumError (showIdxType @k @n) x+        where+          maxIntWord = W# (case maxInt of I# i -> int2Word# i)+#endif+    {-# INLINE fromEnum #-}++    enumFrom (Idx' n)+      = coerce (enumFromTo n (dimVal (dimBound @k @n) - 1))+    {-# INLINE enumFrom #-}+    enumFromThen (Idx' n0) (Idx' n1)+      = coerce (enumFromThenTo n0 n1 lim)+      where+        lim = if n1 >= n0 then dimVal (dimBound @k @n) - 1 else 0+    {-# INLINE enumFromThen #-}+    enumFromTo+      = coerce (enumFromTo :: Word -> Word -> [Word])+    {-# INLINE enumFromTo #-}+    enumFromThenTo+      = coerce (enumFromThenTo :: Word -> Word -> Word -> [Word])+    {-# INLINE enumFromThenTo #-}++instance BoundedDim n => Num (Idx (n :: k)) where++#ifdef UNSAFE_INDICES+    (+) = coerce ((+) :: Word -> Word -> Word)+#else+    (Idx' a@(W# a#)) + b@(Idx' (W# b#))+        | ovf || r >= d+          = errorWithoutStackTrace+          $ "Num.(+){" ++ showIdxType @k @n ++ "}: sum of "+            ++ show a ++ " and " ++ show b+            ++ " is outside of index bounds."+        | otherwise = coerce r+      where+        (ovf, r) = case plusWord2# a# b# of+          (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# )+        d = dimVal (dimBound @k @n)+#endif+    {-# INLINE (+) #-}++#ifdef UNSAFE_INDICES+    (-) = coerce ((-) :: Word -> Word -> Word)+#else+    (Idx' a) - (Idx' b)+        | b > a+          = errorWithoutStackTrace+          $ "Num.(-){" ++ showIdxType @k @n ++ "}: difference of "+            ++ show a ++ " and " ++ show b+            ++ " is negative."+        | otherwise = coerce (a - b)+#endif+    {-# INLINE (-) #-}++#ifdef UNSAFE_INDICES+    (*) = coerce ((*) :: Word -> Word -> Word)+#else+    (Idx' a@(W# a#)) * b@(Idx' (W# b#))+        | ovf || r >= d+          = errorWithoutStackTrace+          $ "Num.(*){" ++ showIdxType @k @n ++ "}: product of "+            ++ show a ++ " and " ++ show b+            ++ " is outside of index bounds."+        | otherwise = coerce r+      where+        (ovf, r) = case timesWord2# a# b# of+          (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# )+        d = dimVal (dimBound @k @n)+#endif+    {-# INLINE (*) #-}++    negate = errorWithoutStackTrace+           $ "Num.(*){" ++ showIdxType @k @n ++ "}: cannot negate index."+    {-# INLINE negate #-}+    abs = id+    {-# INLINE abs #-}+    signum = const (Idx' 1)+    {-# INLINE signum #-}++#ifdef UNSAFE_INDICES+    fromInteger = coerce (fromInteger :: Integer -> Word)+#else+    fromInteger i+      | i >= 0 && i < d = Idx' $ fromInteger i+      | otherwise       = errorWithoutStackTrace+                        $ "Num.fromInteger{" ++ showIdxType @k @n ++ "}: integer "+                        ++ show i ++ " is outside of index bounds."+      where+        d = toInteger $ dimVal (dimBound @k @n)+#endif+    {-# INLINE fromInteger #-}+++++instance Eq (Idxs (xs :: [k])) where+    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)+    {-# INLINE (==) #-}++-- | Compare indices by their importance in lexicorgaphic order+--   from the first dimension to the last dimension+--   (the first dimension is the most significant one).+--+--   Literally,+--+--   > compare a b = compare (listIdxs a) (listIdxs b)+--+--   This is the same @compare@ rule, as for `Dims`.+--   This is also consistent with offsets:+--+--   > sort == sortOn fromEnum+--+instance Ord (Idxs (xs :: [k])) where+    compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering)+    {-# INLINE compare #-}++instance Show (Idxs (xs :: [k])) where+    showsPrec = typedListShowsPrec @k @Idx @xs showsPrec++instance BoundedDims xs => Read (Idxs (xs :: [k])) where+    readPrec = case inferAllBoundedDims @k @xs of+      Dict -> typedListReadPrec @k @BoundedDim ":*" P.readPrec (tList @k @xs)+    readList = P.readListDefault+    readListPrec = P.readListPrecDefault++-- | With this instance we can slightly reduce indexing expressions, e.g.+--+--   > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U)+--+instance BoundedDim n => Num (Idxs '[(n :: k)]) where+    (a:*U) + (b:*U) = (a+b) :* U+    {-# INLINE (+) #-}+    (a:*U) - (b:*U) = (a-b) :* U+    {-# INLINE (-) #-}+    (a:*U) * (b:*U) = (a*b) :* U+    {-# INLINE (*) #-}+    signum (a:*U)   = signum a :* U+    {-# INLINE signum #-}+    abs (a:*U)      = abs a :* U+    {-# INLINE abs #-}+    fromInteger i   = fromInteger i :* U+    {-# INLINE fromInteger #-}++instance BoundedDims ds => Bounded (Idxs (ds :: [k])) where+    maxBound = f (minDims @k @ds)+      where+        f :: forall (ns :: [k]) . Dims ns -> Idxs ns+        f U         = U+        f (d :* ds) = coerce (dimVal d - 1) :* f ds+    {-# INLINE maxBound #-}+    minBound = f (minDims @k @ds)+      where+        f :: forall (ns :: [k]) . Dims ns -> Idxs ns+        f U         = U+        f (_ :* ds) = Idx' 0 :* f ds+    {-# INLINE minBound #-}++-- @ds@ must be @[Nat]@ for @Enum (Idxs ds)@,+--   because succ and pred would break otherwise+instance Dimensions ds => Enum (Idxs (ds :: [Nat])) where++    succ idx = case go dds idx of+        (True , _ ) -> succError $ showIdxsType dds+        (False, i') -> i'+      where+        dds = dims @ds+        go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns)+        go U U = (True, U)+        go (d :* ds) (Idx' i :* is) = case go ds is of+          (True , is')+            | i + 1 == dimVal d -> (True , Idx'  0    :* is')+            | otherwise         -> (False, Idx' (i+1) :* is')+          (False, is')          -> (False, Idx'  i    :* is')+    {-# INLINE succ #-}++    pred idx = case go dds idx of+        (True , _ ) -> predError $ showIdxsType dds+        (False, i') -> i'+      where+        dds = dims @ds+        go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns)+        go U U = (True, U)+        go (d :* ds) (Idx' i :* is) = case go ds is of+          (True , is')+            | i == 0    -> (True , Idx' (dimVal d - 1) :* is')+            | otherwise -> (False, Idx' (i-1)          :* is')+          (False, is')  -> (False, Idx'  i             :* is')+    {-# INLINE pred #-}++    toEnum off0 = case go dds of+        (0, i) -> i+        _      -> toEnumError (showIdxsType dds) off0 (0, totalDim dds - 1)+      where+        dds = dims @ds+        go :: forall (ns :: [Nat]) . Dims ns -> (Word, Idxs ns)+        go  U = (fromIntegral off0, U)+        go (d :* ds)+          | (off , is) <- go ds+          , (off', i ) <- quotRem off (dimVal d)+              = (off', Idx' i :* is)+    {-# INLINE toEnum #-}++    fromEnum = fromIntegral . snd+             . foldr f (1, 0)+             . zip (listDims $ dims @ds) . listIdxs+      where+        f :: (Word, Word) -> (Word, Word) -> (Word, Word)+        f (d, i) (td, off) = (d * td, off + td * i)+    {-# INLINE fromEnum #-}++    enumFrom = unsafeCoerce# go True (dims @ds)+      where+        go :: Bool -> [Word] -> [Word] -> [[Word]]+        go b (d:ds) (i:is) =+          [ i' : is' | (b', i') <- zip (b : repeat False)+                                     $ enumFromTo (if b then i else 0) (d - 1)+                     , is' <- go b' ds is ]+        go _ _ _  = [[]]+    {-# INLINE enumFrom #-}++    enumFromTo = unsafeCoerce# go True True (dims @ds)+      where+        go :: Bool -> Bool -> [Word] -> [Word] -> [Word] -> [[Word]]+        go bl bu (d:ds) (x:xs) (y:ys) =+          [ i : is | (bl', bu', i) <- prepapp bl bu+                                    $ enumFromTo (if bl then x else 0)+                                                 (if bu then y else d - 1)+                   , is <- go bl' bu' ds xs ys ]+        go _ _ _ _ _ = [[]]+        prepapp _  _  []     = []+        prepapp bl bu [i]    = [(bl, bu, i)]+        prepapp bl bu (i:is) = (bl, False, i :: Word) : app bu is+        app _  []     = []+        app bu [i]    = [(False, bu, i :: Word)]+        app bu (i:is) = (False, False, i) : app bu is+    {-# INLINE enumFromTo #-}++    enumFromThen x0 x1 = case compare x1 x0 of+      EQ -> repeat x0+      GT -> enumFromThenTo x0 x1 maxBound+      LT -> enumFromThenTo x0 x1 minBound+    {-# INLINE enumFromThen #-}++    enumFromThenTo x0 x1 y = case dir of+        EQ -> if allYs >= allX0s then repeat x0 else []+        GT -> let (_, allDXs) = idxMinus allDs allX0s allX1s+                  repeatStep is+                    = if is <= allYs+                      then is : case idxPlus allDs is allDXs of+                        (0, is') -> repeatStep is'+                        _        -> []+                      else []+              in unsafeCoerce# (repeatStep allX0s)+        LT -> let (_, allDXs) = idxMinus allDs allX1s allX0s+                  repeatStep is+                    = if is >= allYs+                      then is : case idxMinus allDs allDXs is of+                        (0, is') -> repeatStep is'+                        _        -> []+                      else []+              in unsafeCoerce# (repeatStep allX0s)+      where+        allDs  = listDims $ dims @ds+        allX0s = listIdxs x0+        allX1s = listIdxs x1+        allYs  = listIdxs y+        dir    = compare allX1s allX0s -- succ or pred?+        -- second arg minus first arg+        idxMinus :: [Word] -> [Word] -> [Word] -> (Word, [Word])+        idxMinus (d:ds) (a:as) (b:bs)+          = let (one , xs ) = idxMinus ds as bs+                (one', x  ) = quotRem (d + b - a - one) d+            in  (1 - one', x : xs)+        idxMinus _ _ _ = (0, [])+        idxPlus :: [Word] -> [Word] -> [Word] -> (Word, [Word])+        idxPlus (d:ds) (a:as) (b:bs)+          = let (one , xs ) = idxPlus ds as bs+                (one', x  ) = quotRem (a + b + one) d+            in  (one', x : xs)+        idxPlus _ _ _ = (0, [])+    {-# INLINE enumFromThenTo #-}++++-- | Show type of Idx (for displaying nice errors).+showIdxType :: forall (k :: Type) (x :: k) . BoundedDim x => String+showIdxType = "Idx " ++ show (dimVal (dimBound @k @x))++-- | Show type of Idxs (for displaying nice errors).+showIdxsType :: Dims ns -> String+showIdxsType ds = "Idxs '" ++ show (listDims ds)

@@ -1,427 +0,0 @@-{-# LANGUAGE CPP                        #-}-{-# LANGUAGE ConstraintKinds            #-}-{-# LANGUAGE DataKinds                  #-}-{-# LANGUAGE DeriveDataTypeable         #-}-{-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE ExistentialQuantification  #-}-{-# LANGUAGE ExplicitNamespaces         #-}-{-# LANGUAGE FlexibleContexts           #-}-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE GADTs                      #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures             #-}-{-# LANGUAGE MagicHash                  #-}-{-# LANGUAGE PolyKinds                  #-}-{-# LANGUAGE ScopedTypeVariables        #-}-{-# LANGUAGE Strict                     #-}-{-# LANGUAGE TypeApplications           #-}-#if __GLASGOW_HASKELL__ >= 802-#else-{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}-#endif--------------------------------------------------------------------------------- |--- Module      :  Numeric.Dimensions.Idxs--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Provides a data type Idx that enumerates through multiple dimensions.--- Lower indices go first, i.e. assumed enumeration---          is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).--- This is also to encourage column-first matrix enumeration and array layout.-----------------------------------------------------------------------------------module Numeric.Dimensions.Idxs-  ( -- * Data types-    Idx (..), Idxs-  , idxFromWord, unsafeIdxFromWord, idxToWord-  , listIdxs, idxsFromWords-    -- * Re-export dimensions types-  , module Numeric.Dimensions.Dims-  ) where---import           Control.Arrow           (first)-import           Data.Data               (Data)-import           Foreign.Storable        (Storable)-import           GHC.Base-import           GHC.Enum-import           GHC.Generics            (Generic, Generic1)--import           Numeric.Dimensions.Dims----- | This type is used to index a single dimension;---   the range of indices is from @1@ to @n@.------   Note, this type has a weird `Enum` instance:------   >>>fromEnum (Idx 7)---   6------   The logic behind this is that the `Enum` class is used to transform---   indices to offsets. That is, element of an array at index @k :: Idx n@---   is the element taken by an offset `k - 1 :: Int`.-newtype Idx n = Idx { unIdx :: Word }-  deriving ( Data, Generic, Generic1, Integral, Real, Storable, Eq, Ord )--instance Read (Idx n) where-    readsPrec d = fmap (first Idx) . readsPrec d--instance Show (Idx n) where-    showsPrec d = showsPrec d . unIdx---instance KnownDim n => Bounded (Idx n) where-    minBound = 1-    {-# INLINE minBound #-}-    maxBound = unsafeCoerce# (dim @_ @n)-    {-# INLINE maxBound #-}----   This is a weird `Enum` instance:------   >>>fromEnum (Idx 7)---   6------   The logic behind this is that the `Enum` class is used to transform---   indices to offsets. That is, element of an array at index @k :: Idx n@---   is the element taken by an offset `k - 1 :: Int`.-instance KnownDim n => Enum (Idx n) where--#ifdef UNSAFE_INDICES-    succ = unsafeCoerce# ((+ 1) :: Word -> Word)-#else-    succ x@(Idx i)-      | x /= maxBound = Idx (i + 1)-      | otherwise = succError $ "Idx " ++ show (dim @_ @n)-#endif-    {-# INLINE succ #-}--#ifdef UNSAFE_INDICES-    pred = unsafeCoerce# ((+ (-1)) :: Word -> Word)-#else-    pred x@(Idx i)-      | x /= maxBound = Idx (i + 1)-      | otherwise = predError $ "Idx " ++ show (dim @_ @n)-#endif-    {-# INLINE pred #-}--#ifdef UNSAFE_INDICES-    toEnum (I# i#) = unsafeCoerce# (W# (int2Word# (i# +# 1#)))-#else-    toEnum i@(I# i#)-        | i >= 0 && i < dm = unsafeCoerce# (W# (int2Word# (i# +# 1#) ))-        | otherwise        = toEnumError ("Idx " ++ show d) i (0, dm)-      where-        d = unsafeCoerce# (dim @_ @n) :: Word-        dm = fromIntegral d - 1-#endif-    {-# INLINE toEnum #-}--#ifdef UNSAFE_INDICES-    fromEnum (Idx (W# w#)) = I# (word2Int# w# -# 1#)-#else-    fromEnum (Idx x@(W# w#))-        | x <= maxIntWord = I# (word2Int# w# -# 1#)-        | otherwise       = fromEnumError ("Idx " ++ show (dim @_ @n)) x-        where-          maxIntWord = W# (case maxInt of I# i -> int2Word# i)-#endif-    {-# INLINE fromEnum #-}--    enumFrom (Idx n)-      = unsafeCoerce# (enumFromTo n (unsafeCoerce# (dim @_ @n)))-    {-# INLINE enumFrom #-}-    enumFromThen (Idx n0) (Idx n1)-      = case compare n0 n1 of-          LT -> unsafeCoerce# (enumFromThenTo n0 n1 (unsafeCoerce# (dim @_ @n)))-          EQ -> unsafeCoerce# (repeat n0)-          GT -> unsafeCoerce# (enumFromThenTo n0 n1 1)-    {-# INLINE enumFromThen #-}-    enumFromTo-      = unsafeCoerce# (enumFromTo :: Word -> Word -> [Word])-    {-# INLINE enumFromTo #-}-    enumFromThenTo-      = unsafeCoerce# (enumFromThenTo :: Word -> Word -> Word -> [Word])-    {-# INLINE enumFromThenTo #-}--instance KnownDim n => Num (Idx n) where--#ifdef UNSAFE_INDICES-    (+) = unsafeCoerce# ((+) :: Word -> Word -> Word)-#else-    (Idx a) + (Idx b)-        | r > d || r < a || r < b-          = errorWithoutStackTrace-          $ "Num.(+){Idx " ++ show d ++ "}: sum of "-            ++ show a ++ " and " ++ show b-            ++ " is outside of index bounds."-        | otherwise = Idx r-      where-        r = a + b-        d = unsafeCoerce# (dim @_ @n)-#endif-    {-# INLINE (+) #-}--#ifdef UNSAFE_INDICES-    (-) = unsafeCoerce# ((-) :: Word -> Word -> Word)-#else-    (Idx a) - (Idx b)-        | b >= a-          = errorWithoutStackTrace-          $ "Num.(-){Idx " ++ show (dim @_ @n) ++ "}: difference of "-            ++ show a ++ " and " ++ show b-            ++ " is not positive."-        | otherwise = Idx (a - b)-#endif-    {-# INLINE (-) #-}--#ifdef UNSAFE_INDICES-    (*) = unsafeCoerce# ((*) :: Word -> Word -> Word)-#else-    (Idx a) * (Idx b)-        | r > d || r < a || r < b-          = errorWithoutStackTrace-          $ "Num.(*){Idx " ++ show d ++ "}: product of "-            ++ show a ++ " and " ++ show b-            ++ " is outside of index bounds."-        | otherwise = Idx r-      where-        r = a * b-        d = unsafeCoerce# (dim @_ @n)-#endif-    {-# INLINE (*) #-}--    negate = errorWithoutStackTrace-           $ "Num.(*){Idx " ++ show (dim @_ @n) ++ "}: cannot negate index."-    {-# INLINE negate #-}-    abs = id-    {-# INLINE abs #-}-    signum _ = Idx 1-    {-# INLINE signum #-}--#ifdef UNSAFE_INDICES-    fromInteger = unsafeCoerce# (fromInteger :: Integer -> Word)-#else-    fromInteger i-      | i > 0 && i <= d = Idx $ fromInteger i-      | otherwise       = errorWithoutStackTrace-                        $ "Num.fromInteger{Idx "-                        ++ show d ++ "}: integer "-                        ++ show i ++ " is outside of index bounds."-      where-        d = toInteger (unsafeCoerce# (dim @_ @n) :: Word)-#endif-    {-# INLINE fromInteger #-}---unsafeIdxFromWord :: forall d . KnownDim d => Word -> Idx d-#ifdef UNSAFE_INDICES-unsafeIdxFromWord = unsafeCoerce#-#else-unsafeIdxFromWord w-  | w > 0 && w <= d = Idx w-  | otherwise       = errorWithoutStackTrace-                    $ "idxFromWord{Idx "-                    ++ show d ++ "}: word "-                    ++ show w ++ " is outside of index bounds."-  where-    d = unsafeCoerce# (dim @_ @d)-#endif-{-# INLINE unsafeIdxFromWord #-}--idxFromWord :: forall d . KnownDim d => Word -> Maybe (Idx d)-idxFromWord w-  | w > 0 && w <= unsafeCoerce# (dim @_ @d) = Just (Idx w)-  | otherwise                                 = Nothing-{-# INLINE idxFromWord #-}---idxToWord :: Idx d -> Word-idxToWord = unsafeCoerce#-{-# INLINE idxToWord #-}--{-# RULES-"fromIntegral/idxToWord"-  fromIntegral = idxToWord-  #-}----- | Type-level dimensional indexing with arbitrary Word values inside.---   Most of the operations on it require `Dimensions` constraint,---   because the @Idxs@ itself does not store info about dimension bounds.------   Note, this type has a special `Enum` instance:---   `fromEnum` gives an offset of the index in a flat 1D array;---   this is in line with a weird `Enum` instance of `Idx` type.-type Idxs (xs :: [k]) = TypedList Idx xs---listIdxs :: Idxs xs -> [Word]-listIdxs = unsafeCoerce#-{-# INLINE listIdxs #-}---idxsFromWords :: forall ds . Dimensions ds => [Word] -> Maybe (Idx ds)-idxsFromWords = unsafeCoerce# . go (listDims (dims @_ @ds))-  where-    go [] [] = Just []-    go (d : ds) (i : is)-      | i > 0 && i <= d = (i:) <$> go ds is-    go _ _   = Nothing----instance Eq (Idxs xs) where-    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)-    {-# INLINE (==) #-}---- | Compare indices by their importance in lexicorgaphic order---   from the last dimension to the first dimension---   (the last dimension is the most significant one) @O(Length xs)@.------   Literally,------   > compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b)------   This is the same @compare@ rule, as for `Dims`.---   Another reason to reverse the list of indices is to have a consistent---   behavior when calculating index offsets:------   > sort == sortOn fromEnum----instance Ord (Idxs xs) where-    compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b)-    {-# INLINE compare #-}---instance Show (Idxs xs) where-    show ds = "Idxs " ++ show (listIdxs ds)-    showsPrec p ds-      = showParen (p >= 10)-      $ showString "Idxs " . showsPrec p (listIdxs ds)---- | With this instance we can slightly reduce indexing expressions, e.g.------   > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U)----instance KnownDim n => Num (Idxs '[n]) where-    (a:*U) + (b:*U) = (a+b) :* U-    {-# INLINE (+) #-}-    (a:*U) - (b:*U) = (a-b) :* U-    {-# INLINE (-) #-}-    (a:*U) * (b:*U) = (a*b) :* U-    {-# INLINE (*) #-}-    signum (a:*U)   = signum a :* U-    {-# INLINE signum #-}-    abs (a:*U)      = abs a :* U-    {-# INLINE abs #-}-    fromInteger i   = fromInteger i :* U-    {-# INLINE fromInteger #-}--instance Dimensions ds => Bounded (Idxs ds) where-    maxBound = f (dims @_ @ds)-      where-        f :: forall ns . Dims ns -> Idxs ns-        f U         = U-        f (d :* ds) = Idx (dimVal d) :* f ds-    {-# INLINE maxBound #-}-    minBound = f (dims @_ @ds)-      where-        f :: forall ns . Dims ns -> Idxs ns-        f U         = U-        f (_ :* ds) = Idx 1 :* f ds-    {-# INLINE minBound #-}---instance Dimensions ds => Enum (Idxs ds) where--    succ = go (dims @_ @ds)-      where-        go :: forall ns . Dims ns -> Idxs ns -> Idxs ns-        go U U = succError $ "Idxs " ++ show (listDims $ dims @_ @ds)-        go (d :* ds) (Idx i :* is)-          | i == dimVal d = Idx 1 :* go ds is-          | otherwise     = Idx (i+1) :* is-    {-# INLINE succ #-}--    pred = go (dims @_ @ds)-      where-        go :: forall ns . Dims ns -> Idxs ns -> Idxs ns-        go U U = predError $ "Idxs " ++ show (listDims $ dims @_ @ds)-        go (d :* ds) (Idx i :* is)-          | i == 1    = Idx (dimVal d) :* go ds is-          | otherwise = Idx (i-1) :* is-    {-# INLINE pred #-}--    toEnum i = go dds $ fromIntegral i-      where-        dds = dims @_ @ds-        go :: forall ns . Dims ns -> Word -> Idxs ns-        go U 0 = U-        go U _ = toEnumError ("Idxs " ++ show (listDims dds))-                             i (0, totalDim dds - 1)-        go (d :* ds) off = case divMod off (dimVal d) of-          (off', j) -> Idx (j+1) :* go ds off'-    {-# INLINE toEnum #-}--    fromEnum = fromIntegral . go 1 (dims @_ @ds)-      where-        go :: forall ns . Word -> Dims ns -> Idxs ns -> Word-        go _ U U                     = 0-        go m (d :* ds) (Idx i :* is) = m * (i - 1) + go (m * dimVal d) ds is-    {-# INLINE fromEnum #-}--    enumFrom x = take (diffIdx (dims @_ @ds) maxBound x + 1) $ iterate succ x-    {-# INLINE enumFrom #-}--    enumFromTo x y | x >= y    = take (diffIdx ds x y + 1) $ iterate pred x-                   | otherwise = take (diffIdx ds y x + 1) $ iterate succ x-      where-        ds = dims @_ @ds-    {-# INLINE enumFromTo #-}--    enumFromThen x x' = take n $ iterate (stepIdx ds dn) x-      where-        ds = dims @_ @ds-        dn = diffIdx ds x' x-        n  = 1 + if dn == 0-                 then 0-                 else if dn > 0-                      then diffIdx ds maxBound x `div` dn-                      else diffIdx ds x minBound `div` negate dn-    {-# INLINE enumFromThen #-}--    enumFromThenTo x x' y = take n $ iterate (stepIdx ds dn) x-      where-        ds = dims @_ @ds-        dn = diffIdx ds x' x-        n  = 1 + if dn == 0 then 0-                            else diffIdx ds y x `div` dn-    {-# INLINE enumFromThenTo #-}------------------------------------------------------------------------------------------ | Offset difference of two indices @idx1 - idx2@-diffIdx :: Dims xs -> Idxs xs -> Idxs xs -> Int-diffIdx U U U = 0-diffIdx (d :* ds) (Idx i1 :* is1) (Idx i2 :* is2)-  = fromIntegral i1 - fromIntegral i2-  + fromIntegral (dimVal d) * diffIdx ds is1 is2-{-# INLINE diffIdx #-}---- | Step dimension index by an Int offset-stepIdx :: Dims ds -> Int -> Idxs ds -> Idxs ds-stepIdx U _ U = U-stepIdx (d :* ds) di (Idx i :* is)-      = case divMod (di + fromIntegral i - 1) (fromIntegral (dimVal d)) of-         (0  , i') -> Idx (fromIntegral (i'+1)) :* is-         (di', i') -> Idx (fromIntegral (i'+1)) :* stepIdx ds di' is-{-# INLINE stepIdx #-}

@@ -1,23 +1,20 @@ {-# LANGUAGE BangPatterns #-}-{-# LANGUAGE CPP #-} ----------------------------------------------------------------------------- -- | -- Module      :  Numeric.Tuple -- Copyright   :  (c) Artem Chirkin -- License     :  BSD3 ----- Maintainer  :  chirkin@arch.ethz.ch ----- ----------------------------------------------------------------------------- module Numeric.Tuple     ( module TS     , toStrict, fromStrict     ) where -import Numeric.Tuple.Strict as TS-import qualified Numeric.Tuple.Lazy as TL-import Unsafe.Coerce (unsafeCoerce)+import qualified Numeric.Tuple.Lazy   as TL+import           Numeric.Tuple.Strict as TS+import           Unsafe.Coerce        (unsafeCoerce)  toStrict :: TL.Tuple xs -> TS.Tuple xs toStrict U = U@@ -25,10 +22,6 @@   = let !y = x `seq` TS.Id x         !ys = toStrict xs     in y :* ys-#if __GLASGOW_HASKELL__ >= 802-#else-toStrict _ = error "Tuple.toStrict: impossible argument"-#endif  fromStrict :: TS.Tuple xs -> TL.Tuple xs fromStrict = unsafeCoerce

@@ -10,15 +10,13 @@ {-# LANGUAGE GADTs                      #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE IncoherentInstances        #-}-{-# LANGUAGE KindSignatures             #-} {-# LANGUAGE MagicHash                  #-} {-# LANGUAGE MultiParamTypeClasses      #-} {-# LANGUAGE PatternSynonyms            #-} {-# LANGUAGE PolyKinds                  #-}-{-# LANGUAGE Rank2Types                 #-}+{-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TypeApplications           #-}-{-# LANGUAGE TypeFamilies               #-} {-# LANGUAGE TypeFamilyDependencies     #-} {-# LANGUAGE TypeOperators              #-} {-# LANGUAGE UndecidableInstances       #-}@@ -29,9 +27,7 @@ -- Copyright   :  (c) Artem Chirkin -- License     :  BSD3 ----- Maintainer  :  chirkin@arch.ethz.ch ----- ----------------------------------------------------------------------------- module Numeric.Tuple.Lazy     ( Id (..), Tuple@@ -40,56 +36,73 @@     ) where  -import           Control.Arrow         (first)+import           Control.Arrow        (first) import           Control.Monad.Fix import           Control.Monad.Zip-import           Data.Bits             (Bits, FiniteBits)+import           Data.Bits            (Bits, FiniteBits) import           Data.Coerce-import           Data.Data             (Data)+import           Data.Data            (Data) import           Data.Foldable-import           Data.Ix               (Ix)-import           Data.Monoid           (Monoid (..))-import           Data.Semigroup        (Semigroup (..))-import           Data.String           (IsString)-import           Foreign.Storable      (Storable)-import           GHC.Base              (Type)+import           Data.Functor.Classes+import           Data.Ix              (Ix)+import           Data.Monoid          as Mon (Monoid (..))+import           Data.Semigroup       as Sem (Semigroup (..))+import           Data.String          (IsString)+import           Foreign.Storable     (Storable)+import           GHC.Base             (Type) import           GHC.Exts-import           GHC.Generics          (Generic, Generic1)-import qualified GHC.Read              as Read-import qualified Text.Read             as Read+import           GHC.Generics         (Generic, Generic1)+import qualified Text.Read            as P -import           Numeric.Type.List-import           Numeric.TypedList+import Data.Type.List+import Numeric.TypedList  -- | This is an almost complete copy of `Data.Functor.Identity` --   by (c) Andy Gill 2001. newtype Id a = Id { runId :: a }     deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional              , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord-             , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable)+             , Real, RealFrac, RealFloat, Semigroup, Storable, Traversable)  -instance (Read a) => Read (Id a) where+instance Read a => Read (Id a) where     readsPrec d = fmap (first Id) . readsPrec d -instance (Show a) => Show (Id a) where+instance Show a => Show (Id a) where     showsPrec d = showsPrec d . runId +instance Read1 Id where+    liftReadPrec r _ = coerce r+    liftReadListPrec = liftReadListPrecDefault+    liftReadList     = liftReadListDefault++instance Show1 Id where+    liftShowsPrec f _ = coerce f++instance Eq1 Id where+    liftEq = coerce++instance Ord1 Id where+    liftCompare = coerce+ instance Foldable Id where     foldMap          = coerce-    elem             = (. runId) #. (==)+    elem             = k (==)+      where+        k :: (a -> a -> Bool) -> a -> Id a -> Bool+        k = coerce     foldl            = coerce     foldl'           = coerce-    foldl1 _         = runId+    foldl1 _         = coerce     foldr f z (Id x) = f x z     foldr'           = foldr-    foldr1 _         = runId+    foldr1 _         = coerce     length _         = 1-    maximum          = runId-    minimum          = runId+    maximum          = coerce+    minimum          = coerce     null _           = False-    product          = runId-    sum              = runId+    product          = coerce+    sum              = coerce     toList (Id x)    = [x]  instance Functor Id where@@ -115,15 +128,10 @@ -- | A tuple indexed by a list of types type Tuple (xs :: [Type]) = TypedList Id xs ---- Starting from GHC 8.2, compiler supports specifying lists of complete--- pattern synonyms.-#if __GLASGOW_HASKELL__ >= 802 {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-} {-# COMPLETE Empty, (:$) #-} {-# COMPLETE Empty, (:!) #-}-#endif   -- | Constructing a type-indexed list@@ -179,41 +187,21 @@ infixl 5 !*  -instance (All Semigroup xs) => Semigroup (Tuple xs) where+instance All Semigroup xs => Sem.Semigroup (Tuple xs) where     U <> U = U-    (x :$ xs) <> (y :$ ys)-      = (x <> y) *$ ( xs <> ys)-#if __GLASGOW_HASKELL__ >= 802-#else-    _ <> _ = error "(<>): impossible combination of arguments"-#endif+    (x :$ xs) <> (y :$ ys) = (x <> y) *$ ( xs <> ys) -instance ( Semigroup (Tuple xs)-         , RepresentableList xs-         , All Monoid xs) => Monoid (Tuple xs) where+instance ( RepresentableList xs+         , All Semigroup xs+         , All Monoid xs) => Mon.Monoid (Tuple xs) where     mempty = go (tList @Type @xs)       where         go :: forall (ys :: [Type])             . All Monoid ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = mempty *$ go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "mempty/go: impossible combination of arguments"-#endif-    mappend = go (tList @Type @xs)-      where-        go :: forall (ys :: [Type])-            . All Monoid ys-            => TypeList ys-            -> Tuple ys-            -> Tuple ys-            -> Tuple ys-        go U _ _ = U-        go (_ :* ts) (x :$ xs) (y :$ ys) = mappend x y *$ go ts xs ys-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ _ _ = error "mappend/go: impossible combination of arguments"+#if !(MIN_VERSION_base(4,11,0))+    mappend = (<>) #endif  @@ -224,97 +212,36 @@             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = minBound *$ go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "minBound/go: impossible combination of arguments"-#endif     maxBound = go (tList @Type @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = maxBound *$ go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "maxBound/go: impossible combination of arguments"-#endif  instance All Eq xs => Eq (Tuple xs) where     (==) U U                 = True-    (==) (x :* tx) (y :* ty) = x == y && tx == ty-#if __GLASGOW_HASKELL__ >= 802-#else-    (==) _ _ = error "(==): impossible combination of arguments"-#endif+    (==) (x :* tx) (y :* ty) = eq1 x y && tx == ty     (/=) U U                 = False-    (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty-#if __GLASGOW_HASKELL__ >= 802-#else-    (/=) _ _ = error "(/=): impossible combination of arguments"-#endif+    (/=) (x :* tx) (y :* ty) = not (eq1 x y) || tx /= ty --- | Ord instance of the Tuple implements inverse lexicorgaphic ordering.---   That is, the last element in the tuple is the most significant one.------   Note, this will never work on infinite-dimensional tuples!+-- | Lexicorgaphic ordering; same as normal Haskell lists. instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where     compare U U                 = EQ-    compare (x :* tx) (y :* ty) = compare tx ty <> compare x y-#if __GLASGOW_HASKELL__ >= 802-#else-    compare _ _ = error "compare: impossible combination of arguments"-#endif+    compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty  instance All Show xs => Show (Tuple xs) where-    show U         = "U"-    show (x :* xs) = show x ++ " :* " ++ show xs-#if __GLASGOW_HASKELL__ >= 802-#else-    show _ = error "show: impossible combination of arguments"-#endif-    showsPrec _ U = showString "U"-    showsPrec p (x :* xs) = showParen (p >= 5)-                          $ showsPrec 5 x-                          . showString " :* "-                          . showsPrec 5 xs-#if __GLASGOW_HASKELL__ >= 802-#else-    showsPrec _ _ = error "showsPrec: impossible combination of arguments"-#endif--instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where-    readPrec = go (tList @Type @xs)-      where-        go :: forall (ys :: [Type])-            . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys)-        go U = U <$ Read.expectP (Read.Symbol "U")-        go (_ :* ts) = Read.parens $ Read.prec 5 $ do-          x <- Read.step Read.readPrec-          Read.expectP (Read.Symbol ":*")-          xs <- Read.step $ go ts-          return (x :* xs)-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "readPrec/go: impossible combination of arguments"-#endif-+   showsPrec = typedListShowsPrecC @Type @Show ":$" showsPrec1 +instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where+   readPrec = typedListReadPrec @Type @Read ":$" readPrec1 (tList @Type @xs)+   readList = P.readListDefault+   readListPrec = P.readListPrecDefault  -------------------------------------------------------------------------------- -- internal -------------------------------------------------------------------------------- ---- | Internal (non-exported) 'Coercible' helper for 'elem'------ See Note [Function coercion] in "Data.Foldable" for more details.-(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c-(#.) _f = coerce- forceCons :: Tuple xs -> Tuple xs-forceCons U = U+forceCons U            = U forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs)-#if __GLASGOW_HASKELL__ >= 802-#else-forceCons _ = error "forceCons: impossible combination of arguments"-#endif

@@ -10,15 +10,13 @@ {-# LANGUAGE GADTs                      #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE IncoherentInstances        #-}-{-# LANGUAGE KindSignatures             #-} {-# LANGUAGE MagicHash                  #-} {-# LANGUAGE MultiParamTypeClasses      #-} {-# LANGUAGE PatternSynonyms            #-} {-# LANGUAGE PolyKinds                  #-}-{-# LANGUAGE Rank2Types                 #-}+{-# LANGUAGE RankNTypes                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TypeApplications           #-}-{-# LANGUAGE TypeFamilies               #-} {-# LANGUAGE TypeFamilyDependencies     #-} {-# LANGUAGE TypeOperators              #-} {-# LANGUAGE UndecidableInstances       #-}@@ -29,9 +27,7 @@ -- Copyright   :  (c) Artem Chirkin -- License     :  BSD3 ----- Maintainer  :  chirkin@arch.ethz.ch ----- ----------------------------------------------------------------------------- module Numeric.Tuple.Strict     ( Id (..), Tuple@@ -40,63 +36,80 @@     ) where  -import           Control.Arrow         (first)+import           Control.Arrow        (first) import           Control.Monad.Fix import           Control.Monad.Zip-import           Data.Bits             (Bits, FiniteBits)+import           Data.Bits            (Bits, FiniteBits) import           Data.Coerce-import           Data.Data             (Data)+import           Data.Data            (Data) import           Data.Foldable-import           Data.Ix               (Ix)-import           Data.Monoid           (Monoid (..))-import           Data.Semigroup        (Semigroup (..))-import           Data.String           (IsString)-import           Foreign.Storable      (Storable)-import           GHC.Base              (Type)+import           Data.Functor.Classes+import           Data.Ix              (Ix)+import           Data.Monoid          as Mon (Monoid (..))+import           Data.Semigroup       as Sem (Semigroup (..))+import           Data.String          (IsString)+import           Foreign.Storable     (Storable)+import           GHC.Base             (Type) import           GHC.Exts-import           GHC.Generics          (Generic, Generic1)-import qualified GHC.Read              as Read-import qualified Text.Read             as Read+import           GHC.Generics         (Generic, Generic1)+import qualified Text.Read            as P -import           Numeric.Type.List-import           Numeric.TypedList+import Data.Type.List+import Numeric.TypedList  -- | This is an almost complete copy of `Data.Functor.Identity` --   by (c) Andy Gill 2001. newtype Id a = Id { runId :: a }     deriving ( Bits, Bounded, Data, Enum, Eq, FiniteBits, Floating, Fractional              , Generic, Generic1, Integral, IsString, Ix, Monoid, Num, Ord-             , Real, RealFrac, RealFloat , Semigroup, Storable, Traversable)+             , Real, RealFrac, RealFloat, Semigroup, Storable, Traversable)  -instance (Read a) => Read (Id a) where+instance Read a => Read (Id a) where     readsPrec d = fmap (first Id) . readsPrec d -instance (Show a) => Show (Id a) where+instance Show a => Show (Id a) where     showsPrec d = showsPrec d . runId +instance Read1 Id where+    liftReadPrec r _ = coerce r+    liftReadListPrec = liftReadListPrecDefault+    liftReadList     = liftReadListDefault++instance Show1 Id where+    liftShowsPrec f _ = coerce f++instance Eq1 Id where+    liftEq = coerce++instance Ord1 Id where+    liftCompare = coerce+ instance Foldable Id where     foldMap          = coerce-    elem             = (. runId) #. (==)+    elem             = k (==)+      where+        k :: (a -> a -> Bool) -> a -> Id a -> Bool+        k = coerce     foldl            = coerce     foldl'           = coerce-    foldl1 _         = runId+    foldl1 _         = coerce     foldr f z (Id x) = f x z     foldr'           = foldr-    foldr1 _         = runId+    foldr1 _         = coerce     length _         = 1-    maximum          = runId-    minimum          = runId+    maximum          = coerce+    minimum          = coerce     null _           = False-    product          = runId-    sum              = runId+    product          = coerce+    sum              = coerce     toList (Id x)    = [x]  instance Functor Id where     fmap     = coerce  instance Applicative Id where-    pure     = Id+    pure     = coerce     (<*>)    = coerce  instance Monad Id where@@ -115,15 +128,10 @@ -- | A tuple indexed by a list of types type Tuple (xs :: [Type]) = TypedList Id xs ---- Starting from GHC 8.2, compiler supports specifying lists of complete--- pattern synonyms.-#if __GLASGOW_HASKELL__ >= 802 {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-} {-# COMPLETE Empty, (:$) #-} {-# COMPLETE Empty, (:!) #-}-#endif   -- | Constructing a type-indexed list@@ -179,41 +187,21 @@ infixl 5 !*  -instance (All Semigroup xs) => Semigroup (Tuple xs) where+instance All Semigroup xs => Sem.Semigroup (Tuple xs) where     U <> U = U-    (x :! xs) <> (y :! ys)-      = (x <> y) *! ( xs <> ys)-#if __GLASGOW_HASKELL__ >= 802-#else-    _ <> _ = error "(<>): impossible combination of arguments"-#endif+    (x :! xs) <> (y :! ys) = (x <> y) *! ( xs <> ys) -instance ( Semigroup (Tuple xs)-         , RepresentableList xs-         , All Monoid xs) => Monoid (Tuple xs) where+instance ( RepresentableList xs+         , All Semigroup xs+         , All Monoid xs) => Mon.Monoid (Tuple xs) where     mempty = go (tList @Type @xs)       where         go :: forall (ys :: [Type])             . All Monoid ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = mempty *! go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "mempty/go: impossible combination of arguments"-#endif-    mappend = go (tList @Type @xs)-      where-        go :: forall (ys :: [Type])-            . All Monoid ys-            => TypeList ys-            -> Tuple ys-            -> Tuple ys-            -> Tuple ys-        go U _ _ = U-        go (_ :* ts) (x :! xs) (y :! ys) = mappend x y *! go ts xs ys-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ _ _ = error "mappend/go: impossible combination of arguments"+#if !(MIN_VERSION_base(4,11,0))+    mappend = (<>) #endif  @@ -224,97 +212,36 @@             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = minBound *! go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "minBound/go: impossible combination of arguments"-#endif     maxBound = go (tList @Type @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = maxBound *! go xs-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "maxBound/go: impossible combination of arguments"-#endif  instance All Eq xs => Eq (Tuple xs) where     (==) U U                 = True-    (==) (x :* tx) (y :* ty) = x == y && tx == ty-#if __GLASGOW_HASKELL__ >= 802-#else-    (==) _ _ = error "(==): impossible combination of arguments"-#endif+    (==) (x :* tx) (y :* ty) = eq1 x y && tx == ty     (/=) U U                 = False-    (/=) (x :* tx) (y :* ty) = x /= y || tx /= ty-#if __GLASGOW_HASKELL__ >= 802-#else-    (/=) _ _ = error "(/=): impossible combination of arguments"-#endif+    (/=) (x :* tx) (y :* ty) = not (eq1 x y) || tx /= ty --- | Ord instance of the Tuple implements inverse lexicorgaphic ordering.---   That is, the last element in the tuple is the most significant one.------   Note, this will never work on infinite-dimensional tuples!+-- | Lexicorgaphic ordering; same as normal Haskell lists. instance (All Eq xs, All Ord xs) => Ord (Tuple xs) where     compare U U                 = EQ-    compare (x :* tx) (y :* ty) = compare tx ty <> compare x y-#if __GLASGOW_HASKELL__ >= 802-#else-    compare _ _ = error "compare: impossible combination of arguments"-#endif+    compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty  instance All Show xs => Show (Tuple xs) where-    show U         = "U"-    show (x :* xs) = show x ++ " :* " ++ show xs-#if __GLASGOW_HASKELL__ >= 802-#else-    show _ = error "show: impossible combination of arguments"-#endif-    showsPrec _ U = showString "U"-    showsPrec p (x :* xs) = showParen (p >= 5)-                          $ showsPrec 5 x-                          . showString " :* "-                          . showsPrec 5 xs-#if __GLASGOW_HASKELL__ >= 802-#else-    showsPrec _ _ = error "showsPrec: impossible combination of arguments"-#endif--instance (RepresentableList xs, All Read xs) => Read (Tuple xs) where-    readPrec = go (tList @Type @xs)-      where-        go :: forall (ys :: [Type])-            . All Read ys => TypeList ys -> Read.ReadPrec (Tuple ys)-        go U = U <$ Read.expectP (Read.Symbol "U")-        go (_ :* ts) = Read.parens $ Read.prec 5 $ do-          x <- Read.step Read.readPrec-          Read.expectP (Read.Symbol ":*")-          xs <- Read.step $ go ts-          return (x :* xs)-#if __GLASGOW_HASKELL__ >= 802-#else-        go _ = error "readPrec/go: impossible combination of arguments"-#endif-+   showsPrec = typedListShowsPrecC @Type @Show ":!" showsPrec1 +instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where+   readPrec = typedListReadPrec @Type @Read ":!" readPrec1 (tList @Type @xs)+   readList = P.readListDefault+   readListPrec = P.readListPrecDefault  -------------------------------------------------------------------------------- -- internal -------------------------------------------------------------------------------- ---- | Internal (non-exported) 'Coercible' helper for 'elem'------ See Note [Function coercion] in "Data.Foldable" for more details.-(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c-(#.) _f = coerce- forceCons :: Tuple xs -> Tuple xs-forceCons U = U+forceCons U            = U forceCons (Id x :* xs) = x `seq` xs `seq` (Id x :* xs)-#if __GLASGOW_HASKELL__ >= 802-#else-forceCons _ = error "forceCons: impossible combination of arguments"-#endif

@@ -1,59 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds       #-}-{-# LANGUAGE GADTs           #-}-{-# LANGUAGE KindSignatures  #-}-{-# LANGUAGE Rank2Types      #-}-{-# LANGUAGE PolyKinds       #-}--------------------------------------------------------------------------------- |--- Module      :  Numeric.Type.Evidence--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Construct type-level evidence at runtime----------------------------------------------------------------------------------module Numeric.Type.Evidence-  ( Evidence (..), withEvidence, sumEvs, (+!+)-  , Evidence' (..), toEvidence, toEvidence'-  ) where---import           GHC.Base (Type)-import           GHC.Exts (Constraint)----- | Bring an instance of certain class or constaint satisfaction evidence into scope.-data Evidence :: Constraint -> Type where-    E :: a => Evidence a---- | Combine evidence-sumEvs :: Evidence a -> Evidence b -> Evidence (a,b)-sumEvs E E = E-{-# INLINE sumEvs #-}--infixl 4 +!+--- | Combine evidence-(+!+) :: Evidence a -> Evidence b -> Evidence (a,b)-(+!+) = sumEvs-{-# INLINE (+!+) #-}---- | Pattern match agains evidence to get constraints info-withEvidence :: Evidence a -> (a => r) -> r-withEvidence d r = case d of E -> r-{-# INLINE withEvidence #-}---- | Same as @Evidence@, but allows to separate constraint function from---   the type it is applied to.-data Evidence' :: (k -> Constraint) -> k -> Type where-    E' :: c a => Evidence' c a--toEvidence :: Evidence' c a -> Evidence (c a)-toEvidence E' = E-{-# INLINE toEvidence #-}--toEvidence' :: Evidence (c a) -> Evidence' c a-toEvidence' E = E'-{-# INLINE toEvidence' #-}

@@ -1,222 +0,0 @@-{-# LANGUAGE CPP                    #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE ExplicitNamespaces     #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE KindSignatures         #-}-{-# LANGUAGE MultiParamTypeClasses  #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeInType             #-}-{-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-}------------------------------------------------------------------------------------ |--- Module      :  Numeric.Type.List--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Maintainer  :  chirkin@arch.ethz.ch------ Provides type-level operations on lists.-----------------------------------------------------------------------------------------module Numeric.Type.List-  ( -- * Basic operations-    type (++), type (+:), type (:+)-  , Empty, Cons, Snoc, Head-  , Tail, Init, Last, Concat, Reverse, Take, Drop, Length-  , All, Map-    -- * Working with concatenations-  , Suffix, Prefix, IsPrefix, IsSuffix-    -- * Term level functions-  , ConcatList-  ) where--import           GHC.Exts-import           GHC.TypeLits----- | Synonym for a type-level cons---     (injective, since this is just a synonym for the list constructor)-type (a :: k) :+ (as :: [k]) = a ': as-infixr 5 :+--- | Prefix-style synonym for cons-type Cons (n :: k) (ns :: [k]) = n :+ ns---- | Synonym for a type-level snoc (injective!)-type (ns :: [k]) +: (n :: k) = Snoc ns n-infixl 5 +:--- | Prefix-style synonym for snoc-type Snoc (ns :: [k]) (n :: k) = GetSnoc k (DoSnoc k ns n)----- | List concatenation-type family (as :: [k]) ++ (bs :: [k]) :: [k] where-    (++) '[] bs = bs-    (++) as '[] = as-    (++) (a :+ as) bs = a :+ (as ++ bs)-infixr 5 ++---- | Prefix-style synonym for concatenation-type Concat (as :: [k]) (bs :: [k]) = as ++ bs----- | Reverse a type-level list (injective!)-type Reverse (xs :: [k]) = Reversed k (DoReverse k xs)----- | Synonym for an empty type-level list-type Empty = '[]---type family Take (n::Nat) (xs :: [k]) :: [k] where-    Take _ '[] = '[]-    Take 0 xs = '[]-    Take n (x :+ xs) = x :+ Take (n-1) xs---type family Drop (n::Nat) (xs :: [k]) :: [k] where-    Drop _ '[] = '[]-    Drop 0 xs = xs-    Drop n (x :+ xs) = Drop (n-1) xs--type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where-    Suffix '[] bs = bs-    Suffix as as = '[]-    Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs--type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where-    Prefix '[] as = as-    Prefix bs bs = '[]-    Prefix bs asbs = Take (Length asbs - Length bs) asbs---type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where-    IsPrefix '[] _ = 'True-    IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs-    IsPrefix as as = 'True-    IsPrefix _ _= 'False--type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where-    IsSuffix '[] _ = 'True-    IsSuffix bs bs = 'True-    IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs-    IsSuffix _ _ = 'False---type family Head (xs :: [k]) :: k where-    Head (x :+ xs)  = x-    Head (KEmpty k) = TypeError ( 'Text-      "Head: empty type-level list."-      ':$$: FamErrMsg k-     )--type family Tail (xs :: [k]) :: [k] where-    Tail (x :+ xs)  = xs-    Tail (KEmpty k) = TypeError ( 'Text-      "Tail: empty type-level list."-      ':$$: FamErrMsg k-     )--type family Init (xs :: [k]) :: [k] where-    Init '[x]       = '[]-    Init (x :+ xs)  = x :+ Init xs-    Init (KEmpty k) = TypeError ( 'Text-      "Init: empty type-level list."-      ':$$: FamErrMsg k-     )--type family Last (xs :: [k]) :: k where-    Last '[x]       = x-    Last (x :+ xs)  = Last xs-    Last (KEmpty k) = TypeError ( 'Text-      "Last: empty type-level list."-      ':$$: FamErrMsg k-     )--type family Length (xs :: [k]) :: Nat where-    Length '[] = 0-    Length (_ ': xs) = 1 + Length xs---type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where-    All _ '[] = ()-    All f (x ': xs) = (f x, All f xs)--type family Map (f :: a -> b) (xs :: [a]) :: [b] where-    Map f '[] = '[]-    Map f (x ': xs) = f x ': Map f xs----- | Represent a triple of lists forming a relation `as ++ bs ~ asbs`-class ( asbs ~ Concat as bs-      , as   ~ Prefix bs asbs-      , bs   ~ Suffix as asbs-      , IsSuffix bs asbs ~ 'True-      , IsPrefix as asbs ~ 'True-      ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])-        | as bs -> asbs-        , as asbs -> bs-        , bs asbs -> as--instance ( asbs ~ Concat as bs-         , as   ~ Prefix bs asbs-         , bs   ~ Suffix as asbs-         , IsSuffix bs asbs ~ 'True-         , IsPrefix as asbs ~ 'True-         ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])----type FamErrMsg k-  = 'Text "Type-level error occured when operating on a list of kind "-    ':<>: 'ShowType [k] ':<>: 'Text "."--------------------------------------------------------------------------------------- Tricks to make some type-level operations injective--------------------------------------------------------------------------------------- | A special data type that can have either a single element,---   or more than two.---   This feature is not enforced in the type system - this is just a way to make injective Snoc.-data Snocing k    = SSingle k | SCons [k]-type SSingle k x  = 'SSingle (x :: k)-type SCons k xs   = 'SCons (xs :: [k])-type KCons k x xs = (x :: k) ': (xs :: [k])-type KEmpty k     = ('[] :: [k])-type KSingle k x  = ('[x] :: [k])--type family DoSnoc k (xs :: [k]) (z::k) = (ys :: Snocing k) | ys -> xs z where-    DoSnoc k '[]       x      = SSingle k x-    DoSnoc k (KCons k x xs) y =-      (SCons k (KCons k x (GetSnoc k (DoSnoc k xs y)) :: [k]) :: Snocing k)---type family GetSnoc k (xs :: Snocing k) = (ys :: [k]) | ys -> xs where-    GetSnoc k (SSingle k x) = KSingle k x-    GetSnoc k (SCons k (KCons k y (KCons k x xs))) =-      KCons k y (KCons k x xs)---- | Another data type to make Reverse injective.-data Reversing k    = REmpty | RReverse [k]-type REmpty    k    = 'REmpty-type RReverse  k xs = 'RReverse (xs :: [k])----type family Reversed k (ts :: Reversing k) = (rs :: [k]) | rs -> ts where-    Reversed k (REmpty k) = KEmpty k-    Reversed k (RReverse k (KCons k x xs)) = KCons k x xs---type family DoReverse k (as :: [k]) = (rs :: Reversing k) | rs -> as where-    DoReverse k '[]  = REmpty k-    DoReverse k (KCons k a as) =-      RReverse k (GetSnoc k (DoSnoc k (Reversed k (DoReverse k as)) a))

@@ -1,31 +1,31 @@-{-# LANGUAGE AllowAmbiguousTypes    #-}-{-# LANGUAGE CPP                    #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE GADTs                  #-}-{-# LANGUAGE KindSignatures         #-}-{-# LANGUAGE MagicHash              #-}-{-# LANGUAGE MultiParamTypeClasses  #-}-{-# LANGUAGE PatternSynonyms        #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE Rank2Types             #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TypeApplications       #-}-{-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-}-{-# LANGUAGE ViewPatterns           #-}+{-# LANGUAGE AllowAmbiguousTypes       #-}+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE DeriveDataTypeable        #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE MagicHash                 #-}+{-# LANGUAGE MultiParamTypeClasses     #-}+{-# LANGUAGE PatternSynonyms           #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE RankNTypes                #-}+{-# 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 ----- Maintainer  :  chirkin@arch.ethz.ch ----- -- 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.@@ -37,7 +37,9 @@ module Numeric.TypedList     ( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)     , RepresentableList (..)-    , TypeList, types, order, order'+    , Dict1 (..), DictList+    , TypeList, types, typeables,inferTypeableList+    , order, order'     , cons, snoc     , Numeric.TypedList.reverse     , Numeric.TypedList.take@@ -47,29 +49,36 @@     , 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 Numeric.Type.List+    , module Data.Type.List+      -- * Deriving Show and Read+    , typedListShowsPrecC, typedListShowsPrec+    , typedListReadPrec, withTypedListReadPrec     ) where -import           Control.Arrow         (first)-import           Data.Proxy-import           GHC.Base              (Type)+import           Control.Arrow                   (first)+import           Data.Constraint                 hiding ((***))+import           Data.Data+import           Data.Type.List+import           Data.Void+import           GHC.Base                        (Type) import           GHC.Exts--import           Numeric.Dim-import           Numeric.Type.Evidence-import           Numeric.Type.List+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 {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, Nat, dimVal, minusDimM)  -- | Type-indexed list newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]----- Starting from GHC 8.2, compiler supports specifying lists of complete--- pattern synonyms.-#if __GLASGOW_HASKELL__ >= 802+  deriving (Typeable) {-# COMPLETE TypeList #-} {-# COMPLETE EvList #-} {-# COMPLETE U, (:*) #-}@@ -79,48 +88,123 @@ {-# COMPLETE Empty, Cons #-} {-# COMPLETE Empty, Snoc #-} {-# COMPLETE Reverse #-}-#endif +-- | 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 _ z U         = z U+    gfoldl k z (x :* xs) = case inferTypeableCons @_ @xs of+      Dict -> z (:*) `k` x `k` xs+    gunfold k z _ = case typeables @k @xs of+        U      -> z U+        _ :* _ -> case inferTypeableCons @_ @xs of Dict -> k (k (z (:*)))+    toConstr U        = typedListConstrEmpty+    toConstr (_ :* _) = typedListConstrCons+    dataTypeOf _ = typedListDataType++typedListDataType :: DataType+typedListDataType = mkDataType+  "Numeric.TypedList.TypedList" [typedListConstrEmpty, typedListConstrCons]++typedListConstrEmpty :: Constr+typedListConstrEmpty = mkConstr typedListDataType "U" [] Prefix++typedListConstrCons :: Constr+typedListConstrCons = mkConstr typedListDataType ":*" [] 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 U         = M1 (L1 (M1 U1))+    from (x :* xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs))))+    to (M1 (L1 _))+      | Dict <- unsafeEqTypes @[k] @xs @'[] = U+    to (M1 (R1 xxs))+      | Dict <- unsafeEqTypes @[k] @xs @(Head xs ': Tail xs)+      , M1 (M1 (K1 x) :*: M1 (K1 xs)) <- xxs = x :* xs+ -- | A list of type proxies type TypeList (xs :: [k]) = TypedList Proxy xs +-- | 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 --- | A list of evidence for constraints-type EvidenceList (c :: k -> Constraint) (xs :: [k])-  = TypedList (Evidence' c) xs+instance (Typeable k, Typeable p, Typeable a, p a)+      => Data (Dict1 (p :: k -> Constraint) (a :: k)) where+  gfoldl _ z Dict1 = z Dict1+  toConstr _ = dictConstr+  gunfold _ z _ = z Dict1+  dataTypeOf _ = dictDataType +dictConstr :: Constr+dictConstr = mkConstr dictDataType "Dict1" [] Prefix +dictDataType :: DataType+dictDataType = mkDataType "Numeric.TypedList.Dict1" [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) (xs :: [k])+  = TypedList (Dict1 c) xs++ -- | 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 :: [k])+pattern TypeList :: forall (k :: Type) (xs :: [k])                   . () => RepresentableList xs => TypeList xs-pattern TypeList <- (mkRTL -> E)+pattern TypeList <- (mkRTL -> Dict)   where     TypeList = tList @k @xs  -- | Pattern matching against this allows manipulating lists of constraints. --   Useful when creating functions that change the shape of dimensions.-pattern EvList :: forall (c :: k -> Constraint) (xs :: [k])-                . () => (All c xs, RepresentableList xs) => EvidenceList c xs-pattern EvList <- (mkEVL -> E)+pattern EvList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])+                . () => (All c xs, RepresentableList xs) => DictList c xs+pattern EvList <- (mkEVL -> Dict)   where     EvList = _evList (tList @k @xs)  -- | Zero-length type list-pattern U :: forall (f :: k -> Type) (xs :: [k])+pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k])            . () => (xs ~ '[]) => TypedList f xs-pattern U <- (patTL @f @xs -> PatCNil)+pattern U <- (patTL @k @f @xs -> PatCNil)   where-    U = unsafeCoerce# []+    U = coerce ([] :: [Any])  -- | Zero-length type list; synonym to `U`.-pattern Empty :: forall (f :: k -> Type) (xs :: [k])+pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k])                . () => (xs ~ '[]) => TypedList f xs pattern Empty = U  -- | Constructing a type-indexed list-pattern (:*) :: forall (f :: k -> Type) (xs :: [k])+pattern (:*) :: forall (k :: Type) (f :: k -> Type) (xs :: [k])               . ()              => forall (y :: k) (ys :: [k])               . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs@@ -128,90 +212,158 @@ infixr 5 :*  -- | Constructing a type-indexed list in the canonical way-pattern Cons :: forall (f :: k -> Type) (xs :: [k])+pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k])               . ()              => forall (y :: k) (ys :: [k])               . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs-pattern Cons x xs <- (patTL @f @xs -> PatCons x xs)+pattern Cons x xs <- (patTL @k @f @xs -> PatCons x xs)   where     Cons = Numeric.TypedList.cons  -- | Constructing a type-indexed list from the other end-pattern Snoc :: forall (f :: k -> Type) (xs :: [k])+pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k])               . ()              => forall (sy :: [k]) (y :: k)               . (xs ~ (sy +: y)) => TypedList f sy -> f y -> TypedList f xs-pattern Snoc sx x <- (unsnocTL @f @xs -> PatSnoc sx x)+pattern Snoc sx x <- (unsnocTL @k @f @xs -> PatSnoc sx x)   where     Snoc = Numeric.TypedList.snoc  -- | Reverse a typed list-pattern Reverse :: forall (f :: k -> Type) (xs :: [k])+pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k])                  . ()                 => forall (sx :: [k])                  . (xs ~ Reverse sx, sx ~ Reverse xs)                 => TypedList f sx -> TypedList f xs-pattern Reverse sx <- (unreverseTL @f @xs -> PatReverse sx)+pattern Reverse sx <- (unreverseTL @k @f @xs -> PatReverse sx)   where     Reverse = Numeric.TypedList.reverse -cons :: f x -> TypedList f xs -> TypedList f (x :+ xs)-cons x xs = TypedList (unsafeCoerce# x : unsafeCoerce# xs)+cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k])+      . f x -> TypedList f xs -> TypedList f (x :+ xs)+cons x xs = TypedList (unsafeCoerce# x : coerce xs) {-# INLINE cons #-} -snoc :: TypedList f xs -> f x -> TypedList f (xs +: x)-snoc xs x = TypedList (unsafeCoerce# xs ++ [unsafeCoerce# x])+snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k)+      . TypedList f xs -> f x -> TypedList f (xs +: x)+snoc xs x = TypedList (coerce xs ++ [unsafeCoerce# x]) {-# INLINE snoc #-} -reverse :: TypedList f xs -> TypedList f (Reverse xs)-reverse (TypedList sx) = unsafeCoerce# (Prelude.reverse sx)+reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+         . TypedList f xs -> TypedList f (Reverse xs)+reverse = coerce (Prelude.reverse :: [Any] -> [Any]) {-# INLINE reverse #-} -take :: Dim n -> TypedList f xs -> TypedList f (Take n xs)-take d (TypedList xs) = unsafeCoerce# (Prelude.take (intD d) xs)-{-# INLINE take #-}--drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs)-drop d (TypedList xs) = unsafeCoerce# (Prelude.drop (intD d) xs)-{-# INLINE drop #-}--head :: TypedList f xs -> f (Head xs)+head :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+      . TypedList f xs -> f (Head xs) head (TypedList xs) = unsafeCoerce# (Prelude.head xs) {-# INLINE head #-} -tail :: TypedList f xs -> TypedList f (Tail xs)-tail (TypedList xs) = unsafeCoerce# (Prelude.tail xs)+tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+      . TypedList f xs -> TypedList f (Tail xs)+tail = coerce (Prelude.tail :: [Any] -> [Any]) {-# INLINE tail #-} -init :: TypedList f xs -> TypedList f (Init xs)-init (TypedList xs) = unsafeCoerce# (Prelude.init xs)+init :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+      . TypedList f xs -> TypedList f (Init xs)+init = coerce (Prelude.init :: [Any] -> [Any]) {-# INLINE init #-} -last :: TypedList f xs -> f (Last xs)+last :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+      . TypedList f xs -> f (Last xs) last (TypedList xs) = unsafeCoerce# (Prelude.last xs) {-# INLINE last #-} -length :: TypedList f xs -> Dim (Length xs)+take :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])+      . Dim n -> TypedList f xs -> TypedList f (Take n xs)+take = coerce (Prelude.take . dimValInt :: Dim n -> [Any] -> [Any])+{-# INLINE take #-}++drop :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])+      . Dim n -> TypedList f xs -> TypedList f (Drop n xs)+drop = coerce (Prelude.drop . dimValInt :: Dim n -> [Any] -> [Any])+{-# INLINE drop #-}++length :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+       . TypedList f xs -> Dim (Length xs) length = order {-# INLINE length #-} -splitAt :: Dim n+splitAt :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])+         . Dim n         -> TypedList f xs         -> (TypedList f (Take n xs), TypedList f (Drop n xs))-splitAt d (TypedList xs) = unsafeCoerce# (Prelude.splitAt (intD d) xs)+splitAt = coerce (Prelude.splitAt . dimValInt :: Dim n -> [Any] -> ([Any], [Any])) {-# INLINE splitAt #-} -concat :: TypedList f xs+order' :: forall (k :: Type) (xs :: [k])+        . RepresentableList xs => Dim (Length xs)+order' = order (tList @_ @xs)+{-# INLINE order' #-}++order :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+       . TypedList f xs -> Dim (Length xs)+order = unsafeCoerce# (fromIntegral . Prelude.length :: [Any] -> Word)+{-# INLINE order #-}++concat :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+        . TypedList f xs        -> TypedList f ys        -> TypedList f (xs ++ ys)-concat (TypedList xs) (TypedList ys) = unsafeCoerce# (xs ++ ys)+concat = coerce ((++) :: [Any] -> [Any] -> [Any]) {-# INLINE concat #-} +stripPrefix :: forall (k :: Type) (f :: k -> Type) (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 U ys = Just ys+stripPrefix _ U  = Nothing+stripPrefix ((x :: f x) :* xs) ((y :: f y) :* ys)+  | Just Refl <- eqT @x @y+  , x == y       = coerce (stripPrefix xs ys)+  | otherwise    = Nothing+{-# INLINE stripPrefix #-}++stripSuffix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+             . ( All Typeable xs, All Typeable ys, All Eq (Map f xs))+            => TypedList f xs+            -> TypedList f ys+            -> Maybe (TypedList f (StripSuffix xs ys))+stripSuffix U ys = Just ys+stripSuffix _ U  = Nothing+stripSuffix xs ys+  | Just n <- order ys `minusDimM` order xs+  , (zs, xs') <- Numeric.TypedList.splitAt n ys+  , EvList <- Numeric.TypedList.drop n $ _evList @_ @Typeable ys+  , Just (Refl, True) <- sameList xs xs'+                 = Just (coerce zs)+  | otherwise    = Nothing+{-# INLINE stripSuffix #-}++-- | Returns two things at once:+--   (Evidence that types of lists match, value-level equality).+sameList :: forall (k :: Type) (f :: k -> Type) (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 U U = Just (Refl, True)+sameList ((x :: f x) :* xs) ((y :: f y) :* ys)+  | Just Refl <- eqT @x @y+  , Just (Refl, b) <- sameList xs ys+    = Just (Refl, x == y && b)+  | otherwise+    = Nothing+sameList _ _ = Nothing+ -- | Map a function over contents of a typed list-map :: (forall a . f a -> g a)+map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k])+     . (forall (a :: k) . f a -> g a)     -> TypedList f xs     -> TypedList g xs-map k (TypedList xs) = unsafeCoerce# (Prelude.map k' xs)+map k = coerce (Prelude.map k')   where     k' :: Any -> Any     k' = unsafeCoerce# . k . unsafeCoerce#@@ -223,10 +375,37 @@ -- --   > case types ts of TypeList -> ... ---types :: TypedList f xs -> TypeList xs+types :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+       . TypedList f xs -> TypeList xs types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs) {-# 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 (k :: Type) (xs :: [k]) . Typeable xs => TypeList xs+typeables = case R.typeRep @xs of+    R.App (R.App _ (_ :: R.TypeRep (n :: k1))) (txs :: R.TypeRep (ns :: k2))+      -> case (unsafeCoerce# (Dict @(k1 ~ k1, k2 ~ k2))+                :: Dict (k ~ k1, [k] ~ k2)) of+          Dict -> case (unsafeCoerce# (Dict @(xs ~ xs))+                          :: Dict (xs ~ (n ': ns))) of+            Dict -> Proxy @n :* R.withTypeable txs (typeables @k @ns)+    R.Con _+      -> unsafeCoerce# U+    r -> error ("typeables -- impossible typeRep: " ++ show r)+{-# INLINE typeables #-}++-- | If all elements of a @TypedList@ are @Typeable@,+--   then the list of these elements is also @Typeable@.+inferTypeableList :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+                   . (Typeable k, All Typeable xs)+                  => TypedList f xs -> Dict (Typeable xs)+inferTypeableList U         = Dict+inferTypeableList (_ :* xs) = case inferTypeableList xs of Dict -> Dict+ -- | Representable type lists. --   Allows getting type information about list structure at runtime. class RepresentableList (xs :: [k]) where@@ -239,17 +418,68 @@ instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where   tList = Proxy @x :* tList @k @xs --order' :: forall xs . RepresentableList xs => Dim (Length xs)-order' = order (tList @_ @xs)-{-# INLINE order' #-}+-- | Generic show function for a @TypedList@.+typedListShowsPrecC :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k])+                     . All c xs+                    => String+                       -- ^ Override cons symbol+                    -> ( forall (x :: k) . c x => Int -> f x -> ShowS )+                       -- ^ How to show a single element+                    -> Int -> TypedList f xs -> ShowS+typedListShowsPrecC _ _ _ U = showChar 'U'+typedListShowsPrecC consS elShowsPrec p (x :* xs) = showParen (p >= 6)+    $ elShowsPrec 6 x+    . showChar ' ' . showString consS . showChar ' '+    . typedListShowsPrecC @k @c @f consS elShowsPrec 5 xs -order :: TypedList f xs -> Dim (Length xs)-order (TypedList xs) = unsafeCoerce# (fromIntegral (Prelude.length xs) :: Word)-{-# INLINE order #-}+-- | Generic show function for a @TypedList@.+typedListShowsPrec :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+                    . ( forall (x :: k) . Int -> f x -> ShowS )+                      -- ^ How to show a single element+                   -> Int -> TypedList f xs -> ShowS+typedListShowsPrec _ _ U = showChar 'U'+typedListShowsPrec elShowsPrec p (x :* xs) = showParen (p >= 6) $+    elShowsPrec 6 x . showString " :* " . typedListShowsPrec @k @f elShowsPrec 5 xs +-- | Generic read function for a @TypedList@.+--   Requires a "template" to enforce the structure of the type list.+typedListReadPrec :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type)+                            (xs :: [k]) (g :: k -> Type)+                   . All c xs+                  => String+                     -- ^ Override cons symbol+                  -> ( forall (x :: k) . 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 _ _ U = Read.parens $ U <$ Read.lift (Read.expect $ Read.Ident "U")+typedListReadPrec consS elReadPrec (_ :* ts) = Read.parens . Read.prec 5 $ do+    x <- Read.step elReadPrec+    Read.lift . Read.expect $ Read.Symbol consS+    xs <- typedListReadPrec @k @c consS elReadPrec ts+    return (x :* xs) +-- | Generic read function for a @TypedList@ of unknown length.+withTypedListReadPrec :: forall (k :: Type) (f :: k -> Type) (r :: Type)+                       . (forall (z :: Type) .+                            ( forall (x :: k) . f x -> z) -> Read.ReadPrec z )+                         -- ^ How to read a single element+                      -> (forall (xs :: [k]) . TypedList f xs -> r )+                         -- ^ Consume the result+                      -> Read.ReadPrec r+withTypedListReadPrec withElReadPrec use = Read.parens $+    (use U <$ Read.lift (Read.expect $ Read.Ident "U"))+    Read.++++    Read.prec 5 (do+      WithAnyTL withX <- Read.step $ withElReadPrec (\x -> WithAnyTL $ use . (x :*))+      Read.lift . Read.expect $ Read.Symbol ":*"+      withTypedListReadPrec @k @f @r withElReadPrec withX+    ) +-- Workaround impredicative polymorphism+newtype WithAnyTL (f :: k -> Type) (r :: Type)+  = WithAnyTL (forall (xs :: [k]) . TypedList f xs -> r)  -------------------------------------------------------------------------------- -- internal@@ -260,7 +490,7 @@ --   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 xs r+reifyRepList :: forall (k :: Type) (xs :: [k]) (r :: Type)               . TypeList xs              -> (RepresentableList xs => r)              -> r@@ -268,76 +498,74 @@ {-# INLINE reifyRepList #-} newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r) -data PatReverse f xs+data PatReverse (f :: k -> Type) (xs :: [k])   = forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs)   => PatReverse (TypedList f sx) -unreverseTL :: forall f xs . TypedList f xs -> PatReverse f xs+unreverseTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+             . TypedList f xs -> PatReverse f xs unreverseTL (TypedList xs)-  = case (unsafeCoerce# (E @(xs ~ xs, xs ~ xs))-           :: Evidence (xs ~ Reverse sx, sx ~ Reverse xs)+  = case (unsafeCoerce# (Dict @(xs ~ xs, xs ~ xs))+           :: Dict (xs ~ Reverse sx, sx ~ Reverse xs)          ) of-      E -> PatReverse (unsafeCoerce# (Prelude.reverse xs))+      Dict -> PatReverse (unsafeCoerce# (Prelude.reverse xs)) {-# INLINE unreverseTL #-}  -mkRTL :: forall (xs :: [k])+mkRTL :: forall (k :: Type) (xs :: [k])        . TypeList xs-      -> Evidence (RepresentableList xs)-mkRTL xs = reifyRepList xs E+      -> Dict (RepresentableList xs)+mkRTL xs = reifyRepList xs Dict {-# INLINE mkRTL #-}  -data PatSnoc f xs where+data PatSnoc (f :: k -> Type) (xs :: [k]) where   PatSNil :: PatSnoc f '[]   PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y) -unsnocTL :: forall f xs . TypedList f xs -> PatSnoc f xs+unsnocTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+          . TypedList f xs -> PatSnoc f xs unsnocTL (TypedList [])-  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of-      E -> PatSNil+  = case unsafeEqTypes @_ @xs @'[] of+      Dict -> PatSNil unsnocTL (TypedList (x:xs))-  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Init xs +: Last xs))) of-      E -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y)+  = case unsafeEqTypes @_ @xs @(Init xs +: Last xs) of+      Dict -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y)   where     (sy, y) = unsnoc x xs+    unsnoc :: Any -> [Any] -> ([Any], Any)     unsnoc t []     = ([], t)     unsnoc t (z:zs) = first (t:) (unsnoc z zs) {-# INLINE unsnocTL #-}  -data PatCons f xs where+data PatCons (f :: k -> Type) (xs :: [k]) where   PatCNil :: PatCons f '[]   PatCons :: f y -> TypedList f ys -> PatCons f (y ': ys) -patTL :: forall f xs . TypedList f xs -> PatCons f xs+patTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+       . TypedList f xs -> PatCons f xs patTL (TypedList [])-  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ '[])) of-      E -> PatCNil+  = case unsafeEqTypes @_ @xs @'[] of+      Dict -> PatCNil patTL (TypedList (x : xs))-  = case (unsafeCoerce# (E @(xs ~ xs)) :: Evidence (xs ~ (Head xs ': Tail xs))) of-      E -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs)+  = case unsafeEqTypes @_ @xs  @(Head xs ': Tail xs) of+      Dict -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs) {-# INLINE patTL #-} -intD :: Dim n -> Int-intD = (fromIntegral :: Word -> Int) . unsafeCoerce#+mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])+       . DictList c xs -> Dict (All c xs, RepresentableList xs)+mkEVL U              = Dict+mkEVL (Dict1 :* evs) = case mkEVL evs of Dict -> Dict  -mkEVL :: forall (c :: k -> Constraint) (xs :: [k])-       . EvidenceList c xs -> Evidence (All c xs, RepresentableList xs)-mkEVL U = E-mkEVL (E' :* evs) = case mkEVL evs of E -> E-#if __GLASGOW_HASKELL__ >= 802-#else-mkEVL _ = error "EvList/mkEVL: impossible argument"-#endif+_evList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]) (f :: (k -> Type))+        . All c xs => TypedList f xs -> DictList c xs+_evList U         = U+_evList (_ :* xs) = case _evList xs of evs -> Dict1 :* evs +unsafeEqTypes :: forall (k :: Type) (a :: k) (b :: k) . Dict (a ~ b)+unsafeEqTypes = unsafeCoerce# (Dict :: Dict (a ~ a)) -_evList :: forall (c :: k -> Constraint) (xs :: [k])-        . All c xs => TypeList xs -> EvidenceList c xs-_evList U = U-_evList (_ :* xs) = case _evList xs of evs -> E' :* evs-#if __GLASGOW_HASKELL__ >= 802-#else-_evList _ = error "EvList/_evList: impossible argument"-#endif+dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int+dimValInt = fromIntegral . dimVal

@@ -1,86 +0,0 @@-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TemplateHaskell           #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeOperators             #-}---- | Some GHC versions show incorrect warnings here:------   GHC 8.2 says "Pattern match has inaccessible right hand side"---    if our GADT-like patterns are matched nested:---    https://ghc.haskell.org/trac/ghc/ticket/14253------   GHC 8.0 says "Pattern match(es) are non-exhaustive"---    because it does not support COMPLETE pragmas yet.----module Numeric.DimTest (runTests) where--import           Test.QuickCheck       (quickCheckAll)--import           Numeric.Dim-import           Numeric.Type.Evidence----- | Try inference of type-level natural values via term-level binary functions.-testBinaryOp :: forall (a :: Nat) (b :: Nat) (c :: Nat)-              . (Word -> Word -> Word)-             -> (Dim a -> Dim b -> Dim c)-             -> Dim a -> Dim b -> Bool-testBinaryOp fTerm fType da db-  | a <- dimVal da-  , b <- dimVal db-  , Dx dr <- someDimVal (fTerm a b)-      -- pattern-match against @SomeDim@ to extract a type-level natural Dim.-  , True  <- fTerm a b == dimVal (fType da db)-      -- compare the term-level function and the type-level function results-      -- as regular word values.-  , Just E <- sameDim dr (fType da db)-      -- now the type system knows that @c ~ fType a b@ and-      -- we can use ordinary equality function (which is @const True@).-  = dr == fType da db-testBinaryOp _ _ _ _ = False----prop_plusDim :: Word -> Word -> Bool-prop_plusDim a b = case (someDimVal a, someDimVal b) of-  (Dx da, Dx db) -> testBinaryOp (+) plusDim da db---prop_timesDim :: Word -> Word -> Bool-prop_timesDim a b = case (someDimVal a, someDimVal b) of-  (Dx da, Dx db) -> testBinaryOp (*) timesDim da db---prop_powerDim :: Word -> Word -> Bool-prop_powerDim a b = case ( someDimVal a-                         , someDimVal b-                         ) of-  (Dx da, Dx db) -> testBinaryOp (^) powerDim da db--prop_minusDim :: Word -> Word -> Bool-prop_minusDim a' b'-  | a <- max a' b'-  , b <- min a' b'-  , xda <- someDimVal a -- this is an unknown (Dim (XN 0))-  , Dx db <- someDimVal b-  , Just (Dx da) <- constrainBy db xda -- here da >= db-  = a - b == dimVal (minusDim da db)-prop_minusDim _ _ = False-------return []-runTests :: IO Bool-runTests = $quickCheckAll

@@ -0,0 +1,159 @@+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TemplateHaskell           #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeOperators             #-}++++module Numeric.Dimensions.DimTest (runTests) where++import Data.Constraint+import Data.Typeable+import Test.QuickCheck++import           Numeric.Dimensions+import qualified Numeric.TypedList  as TL+++-- | Try inference of type-level natural values via term-level binary functions.+testBinaryOp :: forall (a :: Nat) (b :: Nat) (c :: Nat)+              . (Word -> Word -> Word)+             -> (Dim a -> Dim b -> Dim c)+             -> Dim a -> Dim b -> Bool+testBinaryOp fTerm fType da db+  | a <- dimVal da+  , b <- dimVal db+  , Dx dr <- someDimVal (fTerm a b)+      -- pattern-match against @SomeDim@ to extract a type-level natural Dim.+  , True  <- fTerm a b == dimVal (fType da db)+      -- compare the term-level function and the type-level function results+      -- as regular word values.+  , Just Dict <- sameDim dr (fType da db)+      -- now the type system knows that @c ~ fType a b@ and+      -- we can use ordinary equality function (which is @const True@).+  = dr == fType da db+testBinaryOp _ _ _ _ = False++++prop_plusDim :: Word -> Word -> Bool+prop_plusDim a b = case (someDimVal a, someDimVal b) of+  (Dx da, Dx db) -> testBinaryOp (+) plusDim da db+++prop_timesDim :: Word -> Word -> Bool+prop_timesDim a b = case (someDimVal a, someDimVal b) of+  (Dx da, Dx db) -> testBinaryOp (*) timesDim da db+++prop_powerDim :: Word -> Word -> Bool+prop_powerDim a b = case ( someDimVal a+                         , someDimVal b+                         ) of+  (Dx da, Dx db) -> testBinaryOp (^) powerDim da db++prop_minusDim :: Word -> Word -> Bool+prop_minusDim a' b'+  | a <- max a' b'+  , b <- min a' b'+  , xda <- someDimVal a -- this is an unknown (Dim (XN 0))+  , Dx (db :: Dim b) <- someDimVal b+  , Just (Dx da) <- constrainDim @_ @(XN b) xda -- here da >= db+  = a - b == dimVal (minusDim da db)+prop_minusDim _ _ = False+++-- | Matching against @Reverse@ pattern lets GHC know the reversion relation+--   at the type level.+--   That means the type system knows that reverse of reverse is the same list!+prop_reverseDims :: [Word] -> Property+prop_reverseDims xs+  | SomeDims ds <- someDimsVal xs+    = case ds of+        Reverse rds -> case rds of+          Reverse rrds -> ds === rrds+++prop_concatDims :: [Word] -> [Word] -> Property+prop_concatDims xs ys+  | SomeDims dxs <- someDimsVal xs+  , SomeDims dys <- someDimsVal ys+    = case TL.concat dxs dys of+        dxsys -> listDims dxsys === xs ++ ys+++-- | TODO: bring more evidence about list equality+prop_splitDims :: Word -> [Word] -> Property+prop_splitDims n xsys+  | SomeDims dxsys <- someDimsVal xsys+  , Dx dn <- someDimVal n+     -- TODO: hmm, this is an incomplete pattern even though+     --       Dn dn would not type check :(.+  , (xs, ys) <- splitAt (fromIntegral n) xsys+    = case TL.splitAt dn dxsys of+      (dxs, dys) -> listDims dxs === xs+               .&&. listDims dys === ys+               .&&. case stripPrefixDims dxs dxsys >>= sameDims dys of+                      Nothing   -> counterexample+                                    ("stripPrefixDims with " ++ show (dxs, dys, dxsys)) False+                      Just Dict -> property True+               .&&. case stripSuffixDims dys dxsys >>= sameDims dxs of+                      Nothing   -> counterexample+                                    ("stripSuffixDims with " ++ show (dxs, dys, dxsys)) False+                      Just Dict -> property True+                -- .&&. dxsys === TL.concat dxs dys+  | otherwise = property False+++prop_stripPrefixDims :: Int -> [Word] -> Property+prop_stripPrefixDims n l+  | SomeDims xsys@Dims <- someDimsVal l+  , SomeDims xs@Dims <- someDimsVal $ take (n `mod` (length l + 2)) l+  , Just ys@Dims  <- stripPrefixDims xs xsys+  , Dict <- dimsAllEq xs+  , Dict <- dimsAllTypeable xs+  , Dict <- dimsAllTypeable xsys+  , Just ys'@Dims <- TL.stripPrefix xs xsys+    = case sameDims ys ys' of+        Nothing -> counterexample+                      ("stripPrefix[Dims] discrepancy " ++ show (ys, ys')) False+        Just Dict -> property True+  | otherwise = counterexample "stripPrefix of take does not work!" False++prop_stripSuffixDims :: Int -> [Word] -> Property+prop_stripSuffixDims n l+  | SomeDims xsys@Dims <- someDimsVal l+  , SomeDims ys@Dims <- someDimsVal $ drop (n `mod` (length l + 2)) l+  , Just xs@Dims  <- stripSuffixDims ys xsys+  , Dict <- dimsAllEq ys+  , Dict <- dimsAllTypeable ys+  , Dict <- dimsAllTypeable xsys+  , Just xs'@Dims <- TL.stripSuffix ys xsys+    = case sameDims xs xs' of+        Nothing -> counterexample+                      ("stripSuffixDims[Dims] discrepancy " ++ show (xs, xs')) False+        Just Dict -> property True+  | otherwise = counterexample "stripSuffixDims of take does not work!" False+++dimsAllEq :: Dims (ns :: [Nat]) -> Dict (All Eq (Map Dim ns))+dimsAllEq U         = Dict+dimsAllEq (D :* ds) | Dict <- dimsAllEq ds = Dict++dimsAllTypeable :: Dims (ns :: [Nat]) -> Dict (All Typeable ns)+dimsAllTypeable U           = Dict+dimsAllTypeable ((D :: Dim n) :* ds)+  | Dict <- mapDict cls (Dict @(KnownDim n))+  , Dict <- dimsAllTypeable ds = Dict+++return []+runTests :: IO Bool+runTests = $quickCheckAll

@@ -1,67 +0,0 @@-{-# LANGUAGE ConstraintKinds           #-}-{-# LANGUAGE DataKinds                 #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces        #-}-{-# LANGUAGE FlexibleContexts          #-}-{-# LANGUAGE GADTs                     #-}-{-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE PolyKinds                 #-}-{-# LANGUAGE Rank2Types                #-}-{-# LANGUAGE ScopedTypeVariables       #-}-{-# LANGUAGE TemplateHaskell           #-}-{-# LANGUAGE TypeApplications          #-}-{-# LANGUAGE TypeOperators             #-}----module Numeric.Dimensions.DimsTest (runTests) where--import           Test.QuickCheck         (quickCheckAll)--import           Numeric.Dim-import           Numeric.Dimensions.Dims-import qualified Numeric.TypedList as TL----- | Matching against @Reverse@ pattern lets GHC know the reversion relation---   at the type level.---   That means the type system knows that reverse of reverse is the same list!-prop_reverseDims :: [Word] -> Bool-prop_reverseDims xs-  | SomeDims ds <- someDimsVal xs-  = case ds of-      Reverse rds -> case rds of-        Reverse rrds -> ds == rrds---prop_concatDims :: [Word] -> [Word] -> Bool-prop_concatDims xs ys-  | SomeDims dxs <- someDimsVal xs-  , SomeDims dys <- someDimsVal ys-  = case TL.concat dxs dys of-      dxsys -> listDims dxsys == xs ++ ys----- | TODO: bring more evidence about list equality-prop_splitDims :: Word -> [Word] -> Bool-prop_splitDims n xsys-  | SomeDims dxsys <- someDimsVal xsys-  , Dx dn <- someDimVal n -- TODO: why this causes non-exhaustive patterns in GHC 8.2?-  , (xs, ys) <- splitAt (fromIntegral n) xsys-  = case TL.splitAt dn dxsys of-      (dxs, dys) -> and-        [ listDims dxs == xs-        , listDims dys == ys-        -- , dxsys == TL.concat dxs dys-        ]---------return []-runTests :: IO Bool-runTests = $quickCheckAll

@@ -0,0 +1,165 @@+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TemplateHaskell           #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeOperators             #-}++module Numeric.Dimensions.IdxTest (runTests) where++import Control.Arrow+import Data.List+import Data.Maybe+import Test.QuickCheck (quickCheckAll)++import Numeric.Dimensions++minMaxSeq :: [(Word, Word)] -> ([Word], [Word])+minMaxSeq []          = ([], [])+minMaxSeq ((x, y):xs) = (min x y :) *** (max x y :) $ minMaxSeq xs++twoIdxsSeq :: [(Word, Word, Word)] -> ([Word], [Word], SomeDims)+twoIdxsSeq inputs = (take n is1, take n is2, someDimsVal (take n ds))+  where+    n = fst $ foldl findN (0, 1) ds+    findN (k, dd) d+      = let dd' = dd * d+        in if d <= niceLimit && dd' <= niceLimit+           then (k+1,dd') else (k, niceLimit+1)+    (is1, is2, ds) = unzip3 $ map reform inputs+    niceLimit = 100000+    reform :: (Word, Word, Word) -> (Word, Word, Word)+    reform (x, y, z)+      | z >= x && z >= y = (x, y, z + 1)+      | x >= z && x >= y = (y, z, x + 1)+      | otherwise        = (x, z, y + 1)+++-- | Check successful cases+prop_idxsFromWords1 :: [(Word, Word)] -> Bool+prop_idxsFromWords1 ins+  | (xs, ys) <- minMaxSeq ins+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , mIs <- idxsFromWords @Nat @ds xs+    = or (zipWith (==) xs ys) || isJust mIs+  | otherwise+    = error "Impossible arguments"++-- | Check failing cases+prop_idxsFromWords2 :: [(Word, Word)] -> Bool+prop_idxsFromWords2 ins+  | (xs, ys) <- minMaxSeq ins+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal xs+  , mIs <- idxsFromWords @Nat @ds ys+    = null xs || isNothing mIs+  | otherwise+    = error "Impossible arguments"++-- | Check if results of idxsFromWords are consistent with idxFromWord+prop_idxsFromWords3 :: [(Word, Word)] -> Bool+prop_idxsFromWords3 ins+  | (xs, ys) <- minMaxSeq ins+  , SomeDims (ds@KnownDims :: Dims ds) <- someDimsVal ys+  , mIs <- idxsFromWords @Nat @ds xs+    = Just False /= (go xs ds <$> mIs)+  | otherwise+    = error "Impossible arguments"+  where+    go :: forall (ns :: [Nat]) . [Word] -> Dims ns -> Idxs ns -> Bool+    go [] U U = True+    go (w:ws) (D :* ds) (i :* is)+              = Just i == idxFromWord w && go ws ds is+    go _ _ _  = False++multLimit :: Word+multLimit = floor $ sqrt (fromIntegral (maxBound :: Int) :: Double)++-- check for Word overflow+wouldNotOverflow :: [Word] -> Bool+wouldNotOverflow+  = and . snd . mapAccumR (\a e -> (a*e, a*e >= a && multLimit > a)) 1++prop_idxsFromEnum :: [(Word, Word)] -> Bool+prop_idxsFromEnum ins+  | (xs, ys) <- minMaxSeq ins+  , wouldNotOverflow ys+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , Just ids <- idxsFromWords @Nat @ds xs+    = ids == toEnum (fromEnum ids)+  | otherwise = True++prop_idxsSucc :: [(Word, Word)] -> Bool+prop_idxsSucc ins+  | (xs, ys) <- minMaxSeq ins+  , wouldNotOverflow ys+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , Just ids <- idxsFromWords @Nat @ds xs+    = ids == maxBound || fromEnum (succ ids) == succ (fromEnum ids)+  | otherwise = True++prop_idxsPred :: [(Word, Word)] -> Bool+prop_idxsPred ins+  | (xs, ys) <- minMaxSeq ins+  , wouldNotOverflow ys+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , Just ids <- idxsFromWords @Nat @ds xs+    = ids == minBound || fromEnum (pred ids) == pred (fromEnum ids)+  | otherwise = True++prop_idxsPredSucc :: [(Word, Word)] -> Bool+prop_idxsPredSucc ins+  | (xs, ys) <- minMaxSeq ins+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , Just ids <- idxsFromWords @Nat @ds xs+    =  ids == minBound || ids == maxBound+    || ( succ (pred ids) == ids && pred (succ ids) == ids )+  | otherwise = True++prop_idxsEnumFrom :: [(Word, Word)] -> Bool+prop_idxsEnumFrom ins+  | (xs, ys) <- minMaxSeq ins+  , wouldNotOverflow ys+  , product ys < 100000+  , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys+  , Just ids <- idxsFromWords @Nat @ds xs+    = [ids..] == map toEnum [fromEnum ids .. fromEnum (maxBound @(Idxs ds))]+  | otherwise = True++prop_idxsEnumFromTo :: [(Word, Word, Word)] -> Bool+prop_idxsEnumFromTo ins+  | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins+  , Just ids <- idxsFromWords @Nat @ds xs+  , Just jds <- idxsFromWords @Nat @ds ys+    = [ids..jds] == map toEnum [fromEnum ids .. fromEnum jds]+  | otherwise = True++prop_idxsEnumFromThen :: [(Word, Word, Word)] -> Bool+prop_idxsEnumFromThen ins+  | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins+  , Just ids <- idxsFromWords @Nat @ds xs+  , Just jds <- idxsFromWords @Nat @ds ys+  , lim <- if jds >= ids then maxBound else minBound :: Idxs ds+    = take 1000 [ids, jds ..]+      ==+      take 1000 (map toEnum [fromEnum ids, fromEnum jds .. fromEnum lim])+  | otherwise = True++prop_idxsEnumFromThenTo :: Bool -> [(Word, Word, Word)] -> Bool+prop_idxsEnumFromThenTo up ins+  | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins+  , Just ids <- idxsFromWords @Nat @ds xs+  , Just jds <- idxsFromWords @Nat @ds ys+  , lim <- if up then maxBound else minBound :: Idxs ds+    = take 1000 [ids, jds .. lim]+      ==+      take 1000 (map toEnum [fromEnum ids, fromEnum jds .. fromEnum lim])+  | otherwise = True++return []+runTests :: IO Bool+runTests = $quickCheckAll

@@ -1,17 +1,17 @@ module Main (tests, main) where -import           System.Exit-import           Distribution.TestSuite+import Distribution.TestSuite+import System.Exit -import qualified Numeric.DimTest-import qualified Numeric.Dimensions.DimsTest+import qualified Numeric.Dimensions.DimTest+import qualified Numeric.Dimensions.IdxTest   -- | Collection of tests in detailed-0.9 format tests :: IO [Test] tests = return-  [ test "Dim"    Numeric.DimTest.runTests-  , test "Dims"   Numeric.Dimensions.DimsTest.runTests+  [ test "Dim"   Numeric.Dimensions.DimTest.runTests+  , test "Idx"   Numeric.Dimensions.IdxTest.runTests   ]  @@ -20,16 +20,17 @@ -- | Run tests as exitcode-stdio-1.0 main :: IO () main = do+    putStrLn ""     ts <- tests     trs <- mapM (\(Test ti) ->(,) (name ti) <$> run ti) ts-    case filter (not . isGood) trs of+    case filter (not . isGood . snd) trs of        [] -> exitSuccess        xs -> do         putStrLn $ "Failed tests: " ++ unwords (fmap fst xs)         exitFailure   where-    isGood (_, Finished Pass) = True-    isGood _ = False+    isGood (Finished Pass) = True+    isGood _               = False   -- | Convert QuickCheck props into Cabal tests