diff --git a/dimensions.cabal b/dimensions.cabal --- a/dimensions.cabal +++ b/dimensions.cabal @@ -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 +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 diff --git a/src/Data/Type/List.hs b/src/Data/Type/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List.hs @@ -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 diff --git a/src/Data/Type/List/InjectiveSnoc.hs b/src/Data/Type/List/InjectiveSnoc.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/InjectiveSnoc.hs @@ -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 diff --git a/src/Data/Type/List/Internal.hs b/src/Data/Type/List/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/Internal.hs @@ -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] diff --git a/src/Data/Type/Lits.hs b/src/Data/Type/Lits.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Lits.hs @@ -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 + ) diff --git a/src/Numeric/Dim.hs b/src/Numeric/Dim.hs deleted file mode 100644 --- a/src/Numeric/Dim.hs +++ /dev/null @@ -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 #-} diff --git a/src/Numeric/Dimensions.hs b/src/Numeric/Dimensions.hs --- a/src/Numeric/Dimensions.hs +++ b/src/Numeric/Dimensions.hs @@ -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 diff --git a/src/Numeric/Dimensions/Dim.hs b/src/Numeric/Dimensions/Dim.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Dim.hs @@ -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# diff --git a/src/Numeric/Dimensions/Dim.hs-boot b/src/Numeric/Dimensions/Dim.hs-boot new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Dim.hs-boot @@ -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)) diff --git a/src/Numeric/Dimensions/Dims.hs b/src/Numeric/Dimensions/Dims.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Dims.hs +++ /dev/null @@ -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 #-} diff --git a/src/Numeric/Dimensions/Fold.hs b/src/Numeric/Dimensions/Fold.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Fold.hs +++ /dev/null @@ -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 diff --git a/src/Numeric/Dimensions/Idx.hs b/src/Numeric/Dimensions/Idx.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Dimensions/Idx.hs @@ -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) diff --git a/src/Numeric/Dimensions/Idxs.hs b/src/Numeric/Dimensions/Idxs.hs deleted file mode 100644 --- a/src/Numeric/Dimensions/Idxs.hs +++ /dev/null @@ -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 #-} diff --git a/src/Numeric/Tuple.hs b/src/Numeric/Tuple.hs --- a/src/Numeric/Tuple.hs +++ b/src/Numeric/Tuple.hs @@ -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 diff --git a/src/Numeric/Tuple/Lazy.hs b/src/Numeric/Tuple/Lazy.hs --- a/src/Numeric/Tuple/Lazy.hs +++ b/src/Numeric/Tuple/Lazy.hs @@ -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 diff --git a/src/Numeric/Tuple/Strict.hs b/src/Numeric/Tuple/Strict.hs --- a/src/Numeric/Tuple/Strict.hs +++ b/src/Numeric/Tuple/Strict.hs @@ -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 diff --git a/src/Numeric/Type/Evidence.hs b/src/Numeric/Type/Evidence.hs deleted file mode 100644 --- a/src/Numeric/Type/Evidence.hs +++ /dev/null @@ -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' #-} diff --git a/src/Numeric/Type/List.hs b/src/Numeric/Type/List.hs deleted file mode 100644 --- a/src/Numeric/Type/List.hs +++ /dev/null @@ -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)) diff --git a/src/Numeric/TypedList.hs b/src/Numeric/TypedList.hs --- a/src/Numeric/TypedList.hs +++ b/src/Numeric/TypedList.hs @@ -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 diff --git a/test/Numeric/DimTest.hs b/test/Numeric/DimTest.hs deleted file mode 100644 --- a/test/Numeric/DimTest.hs +++ /dev/null @@ -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 diff --git a/test/Numeric/Dimensions/DimTest.hs b/test/Numeric/Dimensions/DimTest.hs new file mode 100644 --- /dev/null +++ b/test/Numeric/Dimensions/DimTest.hs @@ -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 diff --git a/test/Numeric/Dimensions/DimsTest.hs b/test/Numeric/Dimensions/DimsTest.hs deleted file mode 100644 --- a/test/Numeric/Dimensions/DimsTest.hs +++ /dev/null @@ -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 diff --git a/test/Numeric/Dimensions/IdxTest.hs b/test/Numeric/Dimensions/IdxTest.hs new file mode 100644 --- /dev/null +++ b/test/Numeric/Dimensions/IdxTest.hs @@ -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 diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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