packages feed

parameterized-utils 1.0.0 → 1.0.1

raw patch · 12 files changed

+572/−275 lines, 12 filesdep ~base

Dependency ranges changed: base

Files

parameterized-utils.cabal view
@@ -1,5 +1,5 @@ Name:          parameterized-utils-Version:       1.0.0+Version:       1.0.1 Author:        Galois Inc. Maintainer:    jhendrix@galois.com Build-type:    Simple@@ -30,7 +30,7 @@  library   build-depends:-    base >= 4.7 && < 4.11,+    base >= 4.7 && < 4.12,     th-abstraction >=0.1 && <0.3,     containers,     deepseq,
src/Data/Parameterized/Classes.hs view
@@ -39,6 +39,7 @@   , fromOrdering     -- * Typeclass generalizations   , ShowF(..)+  , showsF   , HashableF(..)   , CoercibleF(..)     -- * Optics generalizations@@ -211,8 +212,13 @@   showF :: forall tp . f tp -> String   showF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (show x) -  showsF :: forall tp . f tp -> String -> String-  showsF x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (shows x)+  -- | Like 'showsPrec', the precedence argument is /one more/ than the+  -- precedence of the enclosing context.+  showsPrecF :: forall tp. Int -> f tp -> String -> String+  showsPrecF p x = withShow (Proxy :: Proxy f) (Proxy :: Proxy tp) (showsPrec p x)++showsF :: ShowF f => f tp -> String -> String+showsF x = showsPrecF 0 x  instance Show x => ShowF (Const x)
src/Data/Parameterized/Context.hs view
@@ -33,60 +33,102 @@ module Data.Parameterized.Context  ( #ifdef UNSAFE_OPS-   module Data.Parameterized.Context.Unsafe+    module Data.Parameterized.Context.Unsafe #else-   module Data.Parameterized.Context.Safe+    module Data.Parameterized.Context.Safe #endif- , singleton- , toVector- , pattern (:>)- , pattern Empty-   -- * Context extension and embedding utilities- , CtxEmbedding(..)- , ExtendContext(..)- , ExtendContext'(..)- , ApplyEmbedding(..)- , ApplyEmbedding'(..)- , identityEmbedding- , extendEmbeddingRightDiff- , extendEmbeddingRight- , extendEmbeddingBoth- , ctxeSize- , ctxeAssignment--   -- * Static indexing and lenses for assignments- , Idx- , getCtx- , setCtx- , field- , natIndex- , natIndexProxy--   -- * Currying and uncurrying for assignments- , CurryAssignment- , CurryAssignmentClass(..)- ) where--import Prelude hiding (null)+  , singleton+  , toVector+  , pattern (:>)+  , pattern Empty+  , decompose+  , Data.Parameterized.Context.null+  , Data.Parameterized.Context.init+  , Data.Parameterized.Context.last+  , Data.Parameterized.Context.view+  , forIndexM+  , generateSome+  , generateSomeM+  , fromList+    -- * Context extension and embedding utilities+  , CtxEmbedding(..)+  , ExtendContext(..)+  , ExtendContext'(..)+  , ApplyEmbedding(..)+  , ApplyEmbedding'(..)+  , identityEmbedding+  , extendEmbeddingRightDiff+  , extendEmbeddingRight+  , extendEmbeddingBoth+  , ctxeSize+  , ctxeAssignment -import GHC.TypeLits (Nat, type (-))+    -- * Static indexing and lenses for assignments+  , Idx+  , field+  , natIndex+  , natIndexProxy+    -- * Currying and uncurrying for assignments+  , CurryAssignment+  , CurryAssignmentClass(..)+    -- * Size and Index values+  , size1, size2, size3, size4, size5, size6+  , i1of2, i2of2+  , i1of3, i2of3, i3of3+  , i1of4, i2of4, i3of4, i4of4+  , i1of5, i2of5, i3of5, i4of5, i5of5+  , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6+  ) where -import Control.Lens hiding (Index, view, (:>), Empty)+import           Control.Lens hiding (Index, (:>), Empty) import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV+import           GHC.TypeLits (Nat, type (-)) +import           Data.Parameterized.Classes+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC+ #ifdef UNSAFE_OPS-import Data.Parameterized.Context.Unsafe+import           Data.Parameterized.Context.Unsafe #else-import Data.Parameterized.Context.Safe+import           Data.Parameterized.Context.Safe #endif -import Data.Parameterized.TraversableFC  -- | Create a single element context. singleton :: f tp -> Assignment f (EmptyCtx ::> tp) singleton = (empty :>) +-- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.+forIndexM :: forall ctx m+           . Applicative m+          => Size ctx+          -> (forall tp . Index ctx tp -> m ())+          -> m ()+forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ())++-- | Generate an assignment with some context type that is not known.+generateSome :: forall f+              . Int+             -> (Int -> Some f)+             -> Some (Assignment f)+generateSome n f = go n+  where go :: Int -> Some (Assignment f)+        go 0 = Some empty+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1))++-- | Generate an assignment with some context type that is not known.+generateSomeM :: forall m f+              .  Applicative m+              => Int+              -> (Int -> m (Some f))+              -> m (Some (Assignment f))+generateSomeM n f = go n+  where go :: Int -> m (Some (Assignment f))+        go 0 = pure (Some empty)+        go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1)+ -- | Convert the assignment to a vector. toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e toVector a f = V.create $ do@@ -97,6 +139,56 @@ {-# INLINABLE toVector #-}  --------------------------------------------------------------------------------+-- Patterns++-- | Pattern synonym for the empty assignment+pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx+pattern Empty <- (viewAssign -> AssignEmpty)+  where Empty = empty++infixl :>++-- | Pattern synonym for extending an assignment on the right+pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'+pattern (:>) a v <- (viewAssign -> AssignExtend a v)+  where a :> v = extend a v++-- The COMPLETE pragma was not defined until ghc 8.2.*+#if MIN_VERSION_base(4,10,0)+{-# COMPLETE (:>), Empty :: Assignment  #-}+#endif++--------------------------------------------------------------------------------+-- | Views++-- | Return true if assignment is empty.+null :: Assignment f ctx -> Bool+null a =+  case viewAssign a of+    AssignEmpty -> True+    AssignExtend{} -> False++decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)+decompose x = (Data.Parameterized.Context.init x, Data.Parameterized.Context.last x)++-- | Return assignment with all but the last block.+init :: Assignment f (ctx '::> tp) -> Assignment f ctx+init x =+  case viewAssign x of+    AssignExtend t _ -> t++-- | Return the last element in the assignment.+last :: Assignment f (ctx '::> tp) -> f tp+last x =+  case viewAssign x of+    AssignExtend _ e -> e++{-# DEPRECATED view "Use viewAssign or the Empty and :> patterns instead." #-}+-- | View an assignment as either empty or an assignment with one appended.+view :: forall f ctx . Assignment f ctx -> AssignView f ctx+view = viewAssign++-------------------------------------------------------------------------------- -- | Context embedding.  -- This datastructure contains a proof that the first context is@@ -169,38 +261,13 @@     updated :: CtxEmbedding ctx (ctx' ::> tp)     updated = extendEmbeddingRight ctxe --- | Pattern synonym for the empty assignment-pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx-pattern Empty <- (view -> AssignEmpty)-  where Empty = empty--infixl :>---- | Pattern synonym for extending an assignment on the right-pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'-pattern (:>) a v <- (view -> AssignExtend a v)-  where a :> v = extend a v---- The COMPLETE pragma was not defined until ghc 8.2.*-#if MIN_VERSION_base(4,10,0)-{-# COMPLETE (:>), Empty :: Assignment  #-}-#endif- -------------------------------------------------------------------------------- -- Static indexing based on type-level naturals --- | Get an element from an 'Assignment' by zero-based, left-to-right position.--- The position must be specified using @TypeApplications@ for the @n@ parameter.-getCtx :: forall n ctx f r. Idx n ctx r => Assignment f ctx -> f r-getCtx asgn = asgn ! natIndex @n--setCtx :: forall n ctx f r. Idx n ctx r => f r -> Assignment f ctx -> Assignment f ctx-setCtx = update (natIndex @n)- -- | Get a lens for an position in an 'Assignment' by zero-based, left-to-right position. -- The position must be specified using @TypeApplications@ for the @n@ parameter. field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)-field f = adjustM f (natIndex @n)+field = ixF' (natIndex @n)  -- | Constraint synonym used for getting an 'Index' into a 'Ctx'. -- @n@ is the zero-based, left-counted index into the list of types@@ -234,7 +301,7 @@ instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) =>   Idx' n (xs '::> x) r where -  natIndex' = skip (natIndex' @_ @(n-1))+  natIndex' = skipIndex (natIndex' @_ @(n-1))   --------------------------------------------------------------------------------@@ -270,5 +337,93 @@ instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where   curryAssignment k = curryAssignment (\asgn a -> k (asgn :> a))   uncurryAssignment k asgn =-    case view asgn of+    case viewAssign asgn of       AssignExtend asgn' x -> uncurryAssignment k asgn' x++-- | Create an assignment from a list of values.+fromList :: [Some f] -> Some (Assignment f)+fromList = go empty+  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)+        go prev [] = Some prev+        go prev (Some g:next) = (go $! prev `extend` g) next++--------------------------------------------------------------------------------+-- Size and Index values++size1 :: Size (EmptyCtx ::> a)+size1 = incSize zeroSize++size2 :: Size (EmptyCtx ::> a ::> b)+size2 = incSize size1++size3 :: Size (EmptyCtx ::> a ::> b ::> c)+size3 = incSize size2++size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)+size4 = incSize size3++size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)+size5 = incSize size4++size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)+size6 = incSize size5++i1of2 :: Index (EmptyCtx ::> a ::> b) a+i1of2 = skipIndex baseIndex++i2of2 :: Index (EmptyCtx ::> a ::> b) b+i2of2 = nextIndex size1++i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a+i1of3 = skipIndex i1of2++i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b+i2of3 = skipIndex i2of2++i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c+i3of3 = nextIndex size2++i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a+i1of4 = skipIndex i1of3++i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b+i2of4 = skipIndex i2of3++i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c+i3of4 = skipIndex i3of3++i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d+i4of4 = nextIndex size3++i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a+i1of5 = skipIndex i1of4++i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b+i2of5 = skipIndex i2of4++i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c+i3of5 = skipIndex i3of4++i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d+i4of5 = skipIndex i4of4++i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e+i5of5 = nextIndex size4++i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a+i1of6 = skipIndex i1of5++i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b+i2of6 = skipIndex i2of5++i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c+i3of6 = skipIndex i3of5++i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d+i4of6 = skipIndex i4of5++i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e+i5of6 = skipIndex i5of5++i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f+i6of6 = nextIndex size5
src/Data/Parameterized/Context/Safe.hs view
@@ -24,6 +24,7 @@ -- 'Data.Coerce.coerce' to understand indexes in a new context without -- actually breaking things. --------------------------------------------------------------------------+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-}@@ -39,9 +40,12 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeInType #-} module Data.Parameterized.Context.Safe   ( module Data.Parameterized.Ctx+    -- * Size   , Size   , sizeInt   , zeroSize@@ -56,39 +60,36 @@   , Diff   , noDiff   , extendRight-  , KnownDiff(..)   , DiffView(..)   , viewDiff+  , KnownDiff(..)     -- * Indexing   , Index   , indexVal-  , base-  , skip+  , baseIndex+  , skipIndex   , lastIndex   , nextIndex   , extendIndex   , extendIndex'   , forIndex+  , forIndexRange   , intIndex     -- * Assignments   , Assignment   , size-  , replicate+  , Data.Parameterized.Context.Safe.replicate   , generate   , generateM   , empty-  , null   , extend-  , update   , adjust+  , update   , adjustM-  , init   , AssignView(..)-  , view-  , decompose+  , viewAssign   , (!)   , (!^)-  , toList   , zipWith   , zipWithM   , (<++>)@@ -104,6 +105,7 @@ import Data.Maybe (listToMaybe) import Data.Type.Equality import Prelude hiding (init, map, null, replicate, succ, zipWith)+import Data.Kind(Type)  #if !MIN_VERSION_base(4,8,0) import Data.Functor@@ -121,7 +123,7 @@ -- | An indexed singleton type representing the size of a context. data Size (ctx :: Ctx k) where   SizeZero :: Size 'EmptyCtx-  SizeSucc :: Size ctx -> Size (ctx '::> tp)+  SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)  -- | Convert a context size to an 'Int'. sizeInt :: Size ctx -> Int@@ -225,7 +227,7 @@ -- context. data Index (ctx :: Ctx k) (tp :: k) where   IndexHere :: Size ctx -> Index (ctx '::> tp) tp-  IndexThere :: Index ctx tp -> Index (ctx '::> tp') tp+  IndexThere :: !(Index ctx tp) -> Index (ctx '::> tp') tp  -- | Convert an index to an 'Int', where the index of the left-most type in the context is 0. indexVal :: Index ctx tp -> Int@@ -254,12 +256,12 @@   compareF (IndexThere idx1) (IndexThere idx2) = lexCompareF idx1 idx2 $ EQF  -- | Index for first element in context.-base :: Index ('EmptyCtx '::> tp) tp-base = IndexHere SizeZero+baseIndex :: Index ('EmptyCtx '::> tp) tp+baseIndex = IndexHere SizeZero  -- | Increase context while staying at same index.-skip :: Index ctx x -> Index (ctx '::> y) x-skip idx = IndexThere idx+skipIndex :: Index ctx x -> Index (ctx '::> y) x+skipIndex idx = IndexThere idx  -- | Return the index of an element one past the size. nextIndex :: Size ctx -> Index (ctx '::> tp) tp@@ -291,7 +293,44 @@        go _ SizeZero = id        go g (SizeSucc sz) = \r -> go (\i -> g (IndexThere i)) sz  $ f r (g (IndexHere sz)) +data LDiff (l :: Ctx k) (r :: Ctx k) where+ LDiffHere :: LDiff a a+ LDiffThere :: !(LDiff (a::>x) b) -> LDiff a b +ldiffIndex :: Index a tp -> LDiff a b -> Index b tp+ldiffIndex i LDiffHere = i+ldiffIndex i (LDiffThere d) = ldiffIndex (IndexThere i) d++forIndexLDiff :: Size a+              -> LDiff a b+              -> (forall tp . Index b tp -> r -> r)+              -> r+              -> r+forIndexLDiff _ LDiffHere _ r = r+forIndexLDiff sz (LDiffThere d) f r =+  forIndexLDiff (SizeSucc sz) d f (f (ldiffIndex (IndexHere sz) d) r)++forIndexRangeImpl :: Int+                  -> Size a+                  -> LDiff a b+                  -> (forall tp . Index b tp -> r -> r)+                  -> r+                  -> r+forIndexRangeImpl 0 sz d f r = forIndexLDiff sz d f r+forIndexRangeImpl _ SizeZero _ _ r = r+forIndexRangeImpl i (SizeSucc sz) d f r =+  forIndexRangeImpl (i-1) sz (LDiffThere d) f r++-- | Given an index 'i', size 'n', a function 'f', value 'v', and a function 'f',+-- 'forIndex i n f v' is equivalent to 'v' when 'i >= sizeInt n', and+-- 'f i (forIndexRange (i+1) n v0)' otherwise.+forIndexRange :: Int+              -> Size ctx+              -> (forall tp . Index ctx tp -> r -> r)+              -> r+              -> r+forIndexRange i sz f r = forIndexRangeImpl i sz LDiffHere f r+ indexList :: forall ctx. Size ctx -> [Some (Index ctx)] indexList sz_top = go id [] sz_top  where go :: (forall tp. Index ctx' tp -> Index ctx tp)@@ -315,21 +354,18 @@  -- | An assignment is a sequence that maps each index with type 'tp' to -- a value of type 'f tp'.-data Assignment (f :: k -> *) (ctx :: Ctx k) where+data Assignment (f :: k -> Type) (ctx :: Ctx k) where   AssignmentEmpty :: Assignment f EmptyCtx   AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)  -- | View an assignment as either empty or an assignment with one appended.-data AssignView (f :: k -> *) (ctx :: Ctx k) where+data AssignView (f :: k -> Type) (ctx :: Ctx k) where   AssignEmpty :: AssignView f EmptyCtx   AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp) -view :: forall f ctx . Assignment f ctx -> AssignView f ctx-view AssignmentEmpty = AssignEmpty-view (AssignmentExtend asgn x) = AssignExtend asgn x--decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)-decompose (AssignmentExtend a v) = (a,v)+viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx+viewAssign AssignmentEmpty = AssignEmpty+viewAssign (AssignmentExtend asgn x) = AssignExtend asgn x  instance NFData (Assignment f ctx) where   rnf AssignmentEmpty = ()@@ -377,20 +413,17 @@ empty :: Assignment f 'EmptyCtx empty = AssignmentEmpty --- | Return true if assignment is empty.-null :: Assignment f ctx -> Bool-null AssignmentEmpty = True-null _ = False- extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp) extend asgn e = AssignmentExtend asgn e -update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx-update idx e asgn = adjust (\_ -> e) idx asgn-+{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-} adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx-adjust f idx m = runIdentity (adjustM (Identity . f) idx m)+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn) +{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}+update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx+update i v a = adjust (\_ -> v) i a+ adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) adjustM f = go (\x -> x)  where@@ -404,22 +437,17 @@   go _ _ _ = error "SafeTypeContext.adjustM: impossible!" #endif -type instance IndexF   (Assignment (f :: k -> *) ctx) = Index ctx-type instance IxValueF (Assignment (f :: k -> *) ctx) = f+type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx+type instance IxValueF (Assignment (f :: k -> Type) ctx) = f -instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where+instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where   ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)   ixF idx f = adjustM f idx -instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where+instance forall (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where   ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)   ixF' idx f = adjustM f idx ---- | Return assignment with all but the last block.-init :: Assignment f (ctx '::> tp) -> Assignment f ctx-init (AssignmentExtend asgn _) = asgn- idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp idxlookup f (AssignmentExtend _   x) (IndexHere _) = f x idxlookup f (AssignmentExtend ctx _) (IndexThere idx) = idxlookup f ctx idx@@ -511,7 +539,7 @@ map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c map = fmapFC -traverseF :: forall (f:: k -> *) (g::k -> *) (m:: * -> *) (c::Ctx k)+traverseF :: forall (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)            . Applicative m           => (forall tp . f tp -> m (g tp))           -> Assignment f c@@ -572,7 +600,7 @@ type MyZ = 'MyZ type MyS = 'MyS -data MyNatRepr :: MyNat -> * where+data MyNatRepr :: MyNat -> Type where   MyZR :: MyNatRepr MyZ   MySR :: MyNatRepr n -> MyNatRepr (MyS n) @@ -581,7 +609,7 @@   StrongCtxUpdate MyZ     (ctx::>x)    z = ctx ::> z   StrongCtxUpdate (MyS n) (ctx::>x)    z = (StrongCtxUpdate n ctx z) ::> x -type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> *) :: * where+type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> Type) :: Type where   MyNatLookup n       EmptyCtx  f = ()   MyNatLookup MyZ     (ctx::>x) f = f x   MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f
src/Data/Parameterized/Context/Unsafe.hs view
@@ -12,9 +12,13 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeInType #-} module Data.Parameterized.Context.Unsafe   ( module Data.Parameterized.Ctx+  , KnownContext(..)+    -- * Size   , Size   , sizeInt   , zeroSize@@ -24,26 +28,24 @@   , addSize   , SizeView(..)   , viewSize-  , KnownContext(..)     -- * Diff   , Diff   , noDiff   , extendRight-  , KnownDiff(..)   , DiffView(..)   , viewDiff+  , KnownDiff(..)     -- * Indexing   , Index   , indexVal-  , base-  , skip+  , baseIndex+  , skipIndex   , lastIndex   , nextIndex   , extendIndex   , extendIndex'   , forIndex   , forIndexRange-  , forIndexM   , intIndex     -- ** IndexRange   , IndexRange@@ -54,32 +56,24 @@     -- * Assignments   , Assignment   , size-  , replicate+  , Data.Parameterized.Context.Unsafe.replicate   , generate   , generateM-  , generateSome-  , generateSomeM   , empty-  , null   , extend-  , update   , adjust+  , update   , adjustM-  , init-  , last   , AssignView(..)-  , view-  , decompose-  , fromList+  , viewAssign   , (!)   , (!^)-  , zipWith+  , Data.Parameterized.Context.Unsafe.zipWith   , zipWithM   , (<++>)   , traverseWithIndex   ) where -import           Control.Applicative hiding (empty) import qualified Control.Category as Cat import           Control.DeepSeq import           Control.Exception@@ -91,9 +85,7 @@ import           Data.List (intercalate) import           Data.Proxy import           Unsafe.Coerce--import           Prelude hiding (init, last, map, null, replicate, succ, zipWith, (++))-import qualified Prelude+import           Data.Kind(Type)  import           Data.Parameterized.Classes import           Data.Parameterized.Ctx@@ -105,8 +97,14 @@ -- Size  -- | Represents the size of a context.-newtype Size (ctx :: Ctx k) = Size { sizeInt :: Int }+newtype Size (ctx :: Ctx k) = Size Int +type role Size nominal++-- | Convert a context size to an 'Int'.+sizeInt :: Size ctx -> Int+sizeInt (Size n) = n+ -- | The size of an empty context. zeroSize :: Size 'EmptyCtx zeroSize = Size 0@@ -199,6 +197,8 @@ -- context. newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int } +type role Index nominal nominal+ instance Eq (Index ctx tp) where   Index i == Index j = i == j @@ -217,12 +217,12 @@     | otherwise = GTF  -- | Index for first element in context.-base :: Index ('EmptyCtx '::> tp) tp-base = Index 0+baseIndex :: Index ('EmptyCtx '::> tp) tp+baseIndex = Index 0  -- | Increase context while staying at same index.-skip :: Index ctx x -> Index (ctx '::> y) x-skip (Index i) = Index i+skipIndex :: Index ctx x -> Index (ctx '::> y) x+skipIndex (Index i) = Index i  -- | Return the index of a element one past the size. nextIndex :: Size ctx -> Index (ctx ::> tp) tp@@ -265,14 +265,6 @@   | i >= n = r   | otherwise = f (Index i) (forIndexRange (i+1) (Size n) f r) --- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.-forIndexM :: forall ctx m-           . Applicative m-          => Size ctx-          -> (forall tp . Index ctx tp -> m ())-          -> m ()-forIndexM sz f = forIndexRange 0 sz (\i r -> f i *> r) (pure ())- -- | Return index at given integer or nothing if integer is out of bounds. intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx)) intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))@@ -323,7 +315,7 @@ -- -- The first parameter is the height of the tree. -- The second is the parameterized value.-data BalancedTree h (f :: k -> *) (p :: Ctx k) where+data BalancedTree h (f :: k -> Type) (p :: Ctx k) where   BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)   BalPair :: !(BalancedTree h f x)           -> !(BalancedTree h f y)@@ -474,7 +466,7 @@ ------------------------------------------------------------------------ -- BinomialTree -data BinomialTree (h::Height) (f :: k -> *) :: Ctx k -> * where+data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where   Empty :: BinomialTree h f EmptyCtx    -- Contains size of the subtree, subtree, then element.@@ -607,18 +599,11 @@ ------------------------------------------------------------------------ -- Dropping -type family InitCtx (x :: Ctx k) :: Ctx k-type instance InitCtx (x ::> y) = x--type family LastCtx (x :: Ctx k) :: k-type instance LastCtx (x ::> y) = y---- data DropResult f (ctx :: Ctx k) where   DropEmpty :: DropResult f EmptyCtx-  DropExt   :: BinomialTree 'Zero f (InitCtx ctx)-            -> f (LastCtx ctx)-            -> DropResult f ctx+  DropExt   :: BinomialTree 'Zero f x+            -> f y+            -> DropResult f (x ::> y)  -- | 'bal_drop x y' returns the tree formed 'append x (init y)' bal_drop :: forall h f x y@@ -703,13 +688,17 @@ ------------------------------------------------------------------------ -- Assignment -type role Assignment representational nominal- -- | An assignment is a sequence that maps each index with type 'tp' to -- a value of type 'f tp'.-newtype Assignment (f :: k -> *) (ctx :: Ctx k)+--+-- This assignment implementation uses a binomial tree implementation+-- that offers lookups and updates in time and space logarithmic with+-- respect to the number of elements in the context.+newtype Assignment (f :: k -> Type) (ctx :: Ctx k)       = Assignment (BinomialTree 'Zero f ctx) +type role Assignment nominal nominal+ instance NFData (Assignment f ctx) where   rnf a = seq a () @@ -717,27 +706,6 @@ size :: Assignment f ctx -> Size ctx size (Assignment t) = Size (tsize t) --- | Generate an assignment with some context type that is not known.-generateSome :: forall f-              . Int-             -> (Int -> Some f)-             -> Some (Assignment f)-generateSome n f = go n-  where go :: Int -> Some (Assignment f)-        go 0 = Some empty-        go i = (\(Some a) (Some e) -> Some (a `extend` e)) (go (i-1)) (f (i-1))---- | Generate an assignment with some context type that is not known.-generateSomeM :: forall m f-              .  Applicative m-              => Int-              -> (Int -> m (Some f))-              -> m (Some (Assignment f))-generateSomeM n f = go n-  where go :: Int -> m (Some (Assignment f))-        go 0 = pure (Some empty)-        go i = (\(Some a) (Some e) -> Some (a `extend` e)) <$> go (i-1) <*> f (i-1)- -- | @replicate n@ make a context with different copies of the same -- polymorphic value. replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx@@ -763,11 +731,6 @@ empty :: Assignment f EmptyCtx empty = Assignment Empty --- | Return true if assignment is empty.-null :: Assignment f ctx -> Bool-null (Assignment Empty) = True-null (Assignment _) = False- extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x) extend (Assignment x) y = Assignment $ append x (BalLeaf y) @@ -823,6 +786,14 @@  instance ShowF f => ShowF (Assignment f) +{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}+adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx+adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)++{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}+update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx+update i v a = adjust (\_ -> v) i a+ -- | Modify the value of an assignment at a particular index. adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx) adjustM f (Index i) (Assignment a) = Assignment <$> (unsafe_bin_adjust f a i 0)@@ -831,22 +802,12 @@ type instance IndexF       (Assignment f ctx) = Index ctx type instance IxValueF     (Assignment f ctx) = f -instance forall (f :: k -> *) ctx. IxedF k (Assignment f ctx) where-  ixF :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)-  ixF idx f = adjustM f idx--instance forall (f :: k -> *) ctx. IxedF' k (Assignment f ctx) where+instance forall (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) ctx) where   ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)   ixF' idx f = adjustM f idx ---- | Modify the value of an assignment at a particular index.-adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx-adjust f idx asgn = runIdentity (adjustM (Identity . f) idx asgn)---- | Update the assignment at a particular index.-update :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx-update i v a = adjust (\_ -> v) i a+instance forall (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where+  ixF = ixF'  -- This is an unsafe version of update that changes the type of the expression. unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'@@ -860,26 +821,11 @@                -> AssignView f (ctx::>tp)  -- | View an assignment as either empty or an assignment with one appended.-view :: forall f ctx . Assignment f ctx -> AssignView f ctx-view (Assignment x) =+viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx+viewAssign (Assignment x) =   case bin_drop x of     DropEmpty -> AssignEmpty-    DropExt t v -> unsafeCoerce $ AssignExtend (Assignment (unsafeCoerce t)) v---- | Return assignment with all but the last block.-init :: Assignment f (ctx '::> tp) -> Assignment f ctx-init (Assignment x) =-  case bin_drop x of-    DropExt t _ -> Assignment t---- | Return the last element in the assignment.-last :: Assignment f (ctx '::> tp) -> f tp-last x =-  case view x of-    AssignExtend _ e -> e--decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)-decompose x = case view x of AssignExtend a v -> (a,v)+    DropExt t v -> AssignExtend (Assignment t) v  zipWith :: (forall x . f x -> g x -> h x)         -> Assignment f a@@ -913,13 +859,6 @@                   -> Assignment f ctx                   -> m (Assignment g ctx) traverseWithIndex f a = generateM (size a) $ \i -> f i (a ! i)---- | Create an assignment from a list of values.-fromList :: [Some f] -> Some (Assignment f)-fromList = go empty-  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)-        go prev [] = Some prev-        go prev (Some g:next) = (go $! prev `extend` g) next  ------------------------------------------------------------------------ -- Appending
src/Data/Parameterized/List.hs view
@@ -29,6 +29,7 @@   , indexed   , imap   , ifoldr+  , izipWith   , itraverse     -- * Constants   , index0@@ -51,8 +52,13 @@ infixr 5 :<  instance ShowF f => Show (List f sh) where-  show Nil = "Nil"-  show (elt :< rest) = showF elt ++ " :< " ++ show rest+  showsPrec _ Nil = showString "Nil"+  showsPrec p (elt :< rest) = showParen (p > precCons) $+    -- Unlike a derived 'Show' instance, we don't print parens implied+    -- by right associativity.+    showsPrecF (precCons+1) elt . showString " :< " . showsPrec 0 rest+    where+      precCons = 5  instance ShowF f => ShowF (List f) @@ -202,6 +208,24 @@       case ops of         Nil -> b         a :< rest -> f (g IndexHere) a (go (\ix -> g (IndexThere ix)) rest b)++-- | Zip up two lists with a zipper function, which can use the index.+izipWith :: forall a b c sh . (forall tp. Index sh tp -> a tp -> b tp -> c tp)+         -> List a sh+         -> List b sh+         -> List c sh+izipWith f = go id+  where+    go :: forall sh' .+          (forall tp . Index sh' tp -> Index sh tp)+       -> List a sh'+       -> List b sh'+       -> List c sh'+    go g as bs =+      case (as, bs) of+        (Nil, Nil) -> Nil+        (a :< as', b :< bs') ->+          f (g IndexHere) a b :< go (g . IndexThere) as' bs'  -- | Traverse with an additional index. itraverse :: forall a b sh t
src/Data/Parameterized/Map.hs view
@@ -21,6 +21,7 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-} module Data.Parameterized.Map   ( MapF     -- * Construction@@ -69,6 +70,7 @@ import Control.Monad.Identity import Data.List (intercalate, foldl') import Data.Maybe ()+import Data.Kind(Type)  import Data.Parameterized.Classes import Data.Parameterized.Some@@ -105,7 +107,7 @@ -- MapF  -- | A map from parameterized keys to values with the same paramter type.-data MapF (k :: v -> *) (a :: v -> *) where+data MapF (k :: v -> Type) (a :: v -> Type) where   Bin :: {-# UNPACK #-}          !Size -- Number of elements in tree.       -> !(k x)@@ -205,12 +207,12 @@ type instance IxValueF (MapF k v) = v  -- | Turn a map key into a traversal that visits the indicated element in the map, if it exists.-instance forall (k:: a -> *) v. OrdF k => IxedF a (MapF k v) where+instance forall (k:: a -> Type) v. OrdF k => IxedF a (MapF k v) where   ixF :: k x -> Traversal' (MapF k v) (v x)   ixF i f m = updatedValue <$> updateAtKey i (pure Nothing) (\x -> Set <$> f x) m  -- | Turn a map key into a lens that points into the indicated position in the map.-instance forall (k:: a -> *) v. OrdF k => AtF a (MapF k v) where+instance forall (k:: a -> Type) v. OrdF k => AtF a (MapF k v) where   atF :: k x -> Lens' (MapF k v) (Maybe (v x))   atF i f m = updatedValue <$> updateAtKey i (f Nothing) (\x -> maybe Delete Set <$> f (Just x)) m @@ -425,7 +427,7 @@  -- | Generate a map from a foldable collection of keys and a -- function from keys to values.-fromKeys :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *)+fromKeys :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)           .  (Monad m, Foldable t, OrdF a)             => (forall tp . a tp -> m (v tp))             -- ^ Function for evaluating a register value.@@ -438,7 +440,7 @@  -- | Generate a map from a foldable collection of keys and a monadic -- function from keys to values.-fromKeysM :: forall m (t :: * -> *) (a :: k -> *) (v :: k -> *)+fromKeysM :: forall m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type)           .  (Monad m, Foldable t, OrdF a)            => (forall tp . a tp -> m (v tp))            -- ^ Function for evaluating a register value.
src/Data/Parameterized/NatRepr.hs view
@@ -26,6 +26,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-} #if MIN_VERSION_base(4,9,0) {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} #endif@@ -43,6 +44,7 @@   , incNat   , addNat   , subNat+  , divNat   , halfNat   , withDivModNat   , natMultiply@@ -78,16 +80,24 @@   , leqAdd   , leqSub   , leqMulPos+  , leqAddPos   , addIsLeq   , withAddLeq   , addPrefixIsLeq   , withAddPrefixLeq   , addIsLeqLeft1   , dblPosIsPos+  , leqMulMono     -- * Arithmetic proof   , plusComm+  , mulComm   , plusMinusCancel+  , minusPlusCancel+  , addMulDistribRight   , withAddMulDistribRight+  , withSubMulDistribRight+  , mulCancelR+  , mul2Plus     -- * Re-exports typelists basics --  , NatK   , type (+)@@ -140,17 +150,17 @@ -- | Result of comparing two numbers. data NatComparison m n where   -- First number is less than second.-  NatLT :: !(NatRepr y) -> NatComparison x (x+(y+1))+  NatLT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison x (x+(y+1))   NatEQ :: NatComparison x x   -- First number is greater than second.-  NatGT :: !(NatRepr y) -> NatComparison (x+(y+1)) x+  NatGT :: x+1 <= x+(y+1) => !(NatRepr y) -> NatComparison (x+(y+1)) x  compareNat :: NatRepr m -> NatRepr n -> NatComparison m n compareNat m n =   case compare (natValue m) (natValue n) of-    LT -> unsafeCoerce $ NatLT (NatRepr (natValue n - natValue m - 1))-    EQ -> unsafeCoerce $ NatEQ-    GT -> unsafeCoerce $ NatGT (NatRepr (natValue m - natValue n - 1))+    LT -> unsafeCoerce (NatLT @0 @0) (NatRepr (natValue n - natValue m - 1))+    EQ -> unsafeCoerce  NatEQ+    GT -> unsafeCoerce (NatGT @0 @0) (NatRepr (natValue m - natValue n - 1))  instance OrdF NatRepr where   compareF x y =@@ -215,6 +225,9 @@ subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m-n) subNat (NatRepr m) (NatRepr n) = NatRepr (m-n) +divNat :: (1 <= n) => NatRepr (m * n) -> NatRepr n -> NatRepr m+divNat (NatRepr x) (NatRepr y) = NatRepr (div x y)+ withDivModNat :: forall n m a.                  NatRepr n               -> NatRepr m@@ -264,7 +277,7 @@   where i = i0 .&. maxUnsigned w  -- | @unsignedClamp w i@ rounds @i@ to the nearest value between--- @0@ and @2^w-i@ (inclusive).+-- @0@ and @2^w-1@ (inclusive). unsignedClamp :: NatRepr w -> Integer -> Integer unsignedClamp w i   | i < minUnsigned w = minUnsigned w@@ -272,7 +285,7 @@   | otherwise         = i  -- | @signedClamp w i@ rounds @i@ to the nearest value between--- @-2^(w-1)@ and @2^(w-1)-i@ (inclusive).+-- @-2^(w-1)@ and @2^(w-1)-1@ (inclusive). signedClamp :: (1 <= w) => NatRepr w -> Integer -> Integer signedClamp w i   | i < minSigned w = minSigned w@@ -299,16 +312,41 @@ plusComm :: forall f m g n . f m -> g n -> m+n :~: n+m plusComm _ _ = unsafeCoerce (Refl :: m+n :~: m+n) +-- | Produce evidence that * is commutative.+mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)+mulComm _ _ = unsafeCoerce Refl++mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)+mul2Plus n = case addMulDistribRight (Proxy @1) (Proxy @1) n of+               Refl -> Refl+ -- | Cancel an add followed b a subtract plusMinusCancel :: forall f m g n . f m -> g n -> (m + n) - n :~: m plusMinusCancel _ _ = unsafeCoerce (Refl :: m :~: m) +minusPlusCancel :: forall f m g n . (n <= m) => f m -> g n -> (m - n) + n :~: m+minusPlusCancel _ _ = unsafeCoerce (Refl :: m :~: m)++addMulDistribRight :: forall n m p f g h. f n -> g m -> h p+                    -> ((n * p) + (m * p)) :~: ((n + m) * p)+addMulDistribRight _n _m _p = unsafeCoerce Refl+++ withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p                     -> ( (((n * p) + (m * p)) ~ ((n + m) * p)) => a) -> a-withAddMulDistribRight _n _m _p f =+withAddMulDistribRight n m p f =+  case addMulDistribRight n m p of+    Refl -> f++withSubMulDistribRight :: forall n m p f g h a. (m <= n) => f n -> g m -> h p+                    -> ( (((n * p) - (m * p)) ~ ((n - m) * p)) => a) -> a+withSubMulDistribRight _n _m _p f =   case unsafeCoerce (Refl :: 0 :~: 0) of-    (Refl :: (((n * p) + (m * p)) :~: ((n + m) * p)) ) -> f+    (Refl :: (((n * p) - (m * p)) :~: ((n - m) * p)) ) -> f ++ ------------------------------------------------------------------------ -- LeqProof @@ -379,7 +417,7 @@ -- LeqProof combinators  -- | Create a leqProof using two proxies-leqProof :: (m <= n) => f m -> f n -> LeqProof m n+leqProof :: (m <= n) => f m -> g n -> LeqProof m n leqProof _ _ = LeqProof  withLeqProof :: LeqProof m n -> ((m <= n) => a) -> a@@ -406,11 +444,17 @@           -> LeqProof 1 (x*y) leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y) +leqMulMono :: (1 <= x) => p x -> q y -> LeqProof y (x * y)+leqMulMono x y = leqMulCongr (leqProof (Proxy :: Proxy 1) x) (leqRefl y)+ -- | Produce proof that adding a value to the larger element in an LeqProof -- is larger leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p) leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p) +leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)+leqAddPos m n = leqAdd (leqProof (Proxy :: Proxy 1) m) n+ -- | Produce proof that subtracting a value from the smaller element is smaller. leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p)@@ -477,3 +521,7 @@     go n' = case isZeroNat n' of               ZeroNat    -> f0               NonZeroNat -> let n'' = predNat n' in ih n'' (go n'')++mulCancelR ::+  (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> (n1 :~: n2)+mulCancelR _ _ _ = unsafeCoerce Refl
src/Data/Parameterized/TH/GADT.hs view
@@ -14,7 +14,9 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE EmptyCase #-} module Data.Parameterized.TH.GADT-  ( structuralEquality+  ( -- * Instance generators+    -- $typePatterns+  structuralEquality   , structuralTypeEquality   , structuralTypeOrd   , structuralTraversal@@ -71,6 +73,9 @@ ------------------------------------------------------------------------ -- TypePat +-- | A type used to describe (and match) types appearing in generated pattern+-- matches inside of the TH generators in this module ('structuralEquality',+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal') data TypePat    = TypeApp TypePat TypePat -- ^ The application of a type.    | AnyType       -- ^ Match any type.@@ -117,7 +122,7 @@ typeVars = Set.fromList . freeVariables  --- | @declareStructuralEquality@ declares a structural equality predicate.+-- | @structuralEquality@ declares a structural equality predicate. structuralEquality :: TypeQ -> [(TypePat,ExpQ)] -> ExpQ structuralEquality tpq pats =   [| \x y -> isJust ($(structuralTypeEquality tpq pats) x y) |]@@ -208,7 +213,7 @@     then [| \x -> case x of {} |]     else [| \x y -> $(caseE [| x |] (trueEqs [| y |])) |] --- | @structuralTypeEquality f@ returns a function with the type:+-- | @structuralTypeOrd f@ returns a function with the type: --   forall x y . f x -> f y -> OrderingF x y -- -- This implementation avoids matching on both the first and second@@ -441,3 +446,43 @@  matchShowCtor :: ExpQ -> ConstructorInfo -> MatchQ matchShowCtor p con = showCon p (constructorName con) (length (constructorFields con))++-- $typePatterns+--+-- The Template Haskell instance generators 'structuralEquality',+-- 'structuralTypeEquality', 'structuralTypeOrd', and 'structuralTraversal'+-- employ heuristics to generate valid instances in the majority of cases.  Most+-- failures in the heuristics occur on sub-terms that are type indexed.  To+-- handle cases where these functions fail to produce a valid instance, they+-- take a list of exceptions in the form of their second parameter, which has+-- type @[('TypePat', 'ExpQ')]@.  Each 'TypePat' is a /matcher/ that tells the+-- TH generator to use the 'ExpQ' to process the matched sub-term.  Consider the+-- following example:+--+-- > data T a b where+-- >   C1 :: NatRepr n -> T () n+-- >+-- > instance TestEquality (T a) where+-- >   testEquality = $(structuralTypeEquality [t|T|]+-- >                    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])+-- >                    ])+--+-- The exception list says that 'structuralTypeEquality' should use+-- 'testEquality' to compare any sub-terms of type @'NatRepr' n@ in a value of+-- type @T@.+--+-- * 'AnyType' means that the type parameter in that position can be instantiated as any type+--+-- * @'DataArg' n@ means that the type parameter in that position is the @n@-th+--   type parameter of the GADT being traversed (@T@ in the example)+--+-- * 'TypeApp' is type application+--+-- * 'ConType' specifies a base type+--+-- The exception list could have equivalently (and more precisely) have been specified as:+--+-- > [(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]+--+-- The use of 'DataArg' says that the type parameter of the 'NatRepr' must+-- be the same as the second type parameter of @T@.
src/Data/Parameterized/TraversableF.hs view
@@ -24,11 +24,10 @@ import Control.Applicative import Control.Monad.Identity import Data.Coerce-import Data.Functor.Const import Data.Monoid import GHC.Exts (build) --- | A parameterized type that is a function on all instances.+-- | A parameterized type that is a functor on all instances. class FunctorF m where   fmapF :: (forall x . f x -> g x) -> m f -> m g @@ -38,7 +37,7 @@ ------------------------------------------------------------------------ -- FoldableF --- | This is a coercision used to avoid overhead associated+-- | This is a coercion used to avoid overhead associated -- with function composition. (#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c) (#.) _f = coerce
src/Data/Parameterized/TraversableFC.hs view
@@ -38,9 +38,9 @@ import Data.Parameterized.Classes  -- | A parameterized type that is a function on all instances.-class FunctorFC m where-  fmapFC :: forall f g. (forall x . f x -> g x) ->-                        (forall x . m f x -> m g x)+class FunctorFC (t :: (k -> *) -> l -> *) where+  fmapFC :: forall f g. (forall x. f x -> g x) ->+                        (forall x. t f x -> t g x)  -- | A parameterized class for types which can be shown, when given --   functions to show parameterized subterms.@@ -89,74 +89,73 @@    -- | Map each element of the structure to a monoid,   -- and combine the results.-  foldMapFC :: Monoid m => (forall s . e s -> m) -> t e c -> m+  foldMapFC :: forall f m. Monoid m => (forall x. f x -> m) -> (forall x. t f x -> m)   foldMapFC f = foldrFC (mappend . f) mempty    -- | Right-associative fold of a structure.-  foldrFC :: (forall s . e s -> b -> b) -> b -> t e c -> b+  foldrFC :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)   foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z    -- | Left-associative fold of a structure.-  foldlFC :: (forall s . b -> e s -> b) -> b -> t e c -> b+  foldlFC :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)   foldlFC f z t = appEndo (getDual (foldMapFC (\e -> Dual (Endo (\r -> f r e))) t)) z    -- | Right-associative fold of a structure,   -- but with strict application of the operator.-  foldrFC' :: (forall s . e s -> b -> b) -> b -> t e c -> b+  foldrFC' :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)   foldrFC' f0 z0 xs = foldlFC (f' f0) id xs z0     where f' f k x z = k $! f x z    -- | Left-associative fold of a parameterized structure   -- with a strict accumulator.-  foldlFC' :: (forall s . b -> e s -> b) -> b -> t e c -> b+  foldlFC' :: forall f b. (forall x. b -> f x -> b) -> (forall x. b -> t f x -> b)   foldlFC' f0 z0 xs = foldrFC (f' f0) id xs z0     where f' f x k z = k $! f z x    -- | Convert structure to list.-  toListFC :: (forall tp . f tp -> a) -> t f c -> [a]+  toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])   toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)  -- | Return 'True' if all values satisfy predicate.-allFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool+allFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool) allFC p = getAll #. foldMapFC (All #. p)  -- | Return 'True' if any values satisfy predicate.-anyFC :: FoldableFC t => (forall tp . f tp -> Bool) -> t f c -> Bool+anyFC :: FoldableFC t => (forall x. f x -> Bool) -> (forall x. t f x -> Bool) anyFC p = getAny #. foldMapFC (Any #. p)  -- | Return number of elements in list.-lengthFC :: FoldableFC t => t e c -> Int+lengthFC :: FoldableFC t => t f x -> Int lengthFC = foldrFC (const (+1)) 0  ------------------------------------------------------------------------ -- TraversableF -class (FunctorFC t, FoldableFC t) => TraversableFC t where-  traverseFC :: Applicative m-             => (forall s . e s -> m (f s))-             -> t e c-             -> m (t f c)+class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> *) -> l -> *) where+  traverseFC :: forall f g m. Applicative m+             => (forall x. f x -> m (g x))+             -> (forall x. t f x -> m (t g x))  -- | This function may be used as a value for `fmapF` in a `FunctorF` -- instance.-fmapFCDefault :: TraversableFC t => (forall s . e s -> f s) -> t e c -> t f c+fmapFCDefault :: TraversableFC t => forall f g. (forall x. f x -> g x) -> (forall x. t f x -> t g x) fmapFCDefault = \f -> runIdentity . traverseFC (Identity . f) {-# INLINE fmapFCDefault #-}  -- | This function may be used as a value for `Data.Foldable.foldMap` -- in a `Foldable` instance.-foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall s . e s -> m) -> t e c -> m+foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m) foldMapFCDefault = \f -> getConst . traverseFC (Const . f) {-# INLINE foldMapFCDefault #-}  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-traverseFC_ :: (FoldableFC t, Applicative f) => (forall s . e s  -> f ()) -> t e c -> f ()+traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m ()) -> (forall x. t f x -> m ()) traverseFC_ f = foldrFC (\e r -> f e *> r) (pure ()) {-# INLINE traverseFC_ #-}  -- | Map each element of a structure to an action, evaluate -- these actions from left to right, and ignore the results.-forMFC_ :: (FoldableFC t, Applicative f) => t e c -> (forall s . e s  -> f ()) -> f ()+forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m ()) -> m () forMFC_ v f = traverseFC_ f v {-# INLINE forMFC_ #-}
test/Test/Context.hs view
@@ -11,6 +11,7 @@ import Test.QuickCheck import Test.Tasty.QuickCheck +import Control.Lens import Data.Parameterized.Classes import Data.Parameterized.TraversableFC import Data.Parameterized.Some@@ -90,8 +91,8 @@          Some a <- return $ mkUAsgn vals          let vals' = toListFC Some a          return (vals == vals')-   , testProperty "adjust_test" $ \v vs i -> ioProperty $ do-         let vals = v:vs+   , testProperty "adjust test monadic" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array          Some x <- return $ mkUAsgn vals          Some y <- return $ mkSAsgn vals          let i' = min (max 0 i) (length vals - 1)@@ -99,10 +100,61 @@          Just (Some idx_x) <- return $ U.intIndex i' (U.size x)          Just (Some idx_y) <- return $ S.intIndex i' (S.size y) -         let x' = U.adjust twiddle idx_x x-         let y' = S.adjust twiddle idx_y y+         x' <- U.adjustM (return . twiddle) idx_x x+         y' <- S.adjustM (return . twiddle) idx_y y           return (toListFC Some x' == toListFC Some y')++   , testProperty "adjust test" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array+         Some x <- return $ mkUAsgn vals+         Some y <- return $ mkSAsgn vals+         let i' = min (max 0 i) (length vals - 1)++         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++         let x' = over (ixF idx_x) twiddle x+             y' = (ixF idx_y) %~ twiddle $ y+             x'' = U.adjust twiddle idx_x x+             y'' = S.adjust twiddle idx_y y++         return (toListFC Some x' == toListFC Some y' &&+                 -- adjust actually modified the entry+                 toListFC Some x /= toListFC Some x' &&+                 toListFC Some y /= toListFC Some y' &&+                 -- verify new version is equivalent to older deprecated version+                 toListFC Some x'' == toListFC Some x' &&+                 toListFC Some y'' == toListFC Some y')++   , testProperty "update test" $ \v vs i -> ioProperty $ do+         let vals = v:vs  -- ensures vals is not an empty array+         Some x <- return $ mkUAsgn vals+         Some y <- return $ mkSAsgn vals+         let i' = min (max 0 i) (length vals - 1)++         Just (Some idx_x) <- return $ U.intIndex i' (U.size x)+         Just (Some idx_y) <- return $ S.intIndex i' (S.size y)++         let x' = over (ixF idx_x) twiddle x+             y' = (ixF idx_y) %~ twiddle $ y+             updX = set (ixF idx_x) (x' U.! idx_x) x+             updY = (ixF idx_y) .~  (y' S.! idx_y) $ y+             updX' = U.update idx_x (x' U.! idx_x) x+             updY' = S.update idx_y (y' S.! idx_y) y++         return (toListFC Some updX == toListFC Some updY &&+                 -- update actually modified the entry+                 toListFC Some x /= toListFC Some updX &&+                 toListFC Some y /= toListFC Some updY &&+                 -- update modified the expected entry+                 toListFC Some x' == toListFC Some updX &&+                 toListFC Some y' == toListFC Some updY &&+                 -- verify new version is equivalent to older deprecated version+                 toListFC Some updX == toListFC Some updX' &&+                 toListFC Some updY == toListFC Some updY'+                )+    , testProperty "safe_eq" $ \vals1 vals2 -> ioProperty $ do          Some x <- return $ mkSAsgn vals1          Some y <- return $ mkSAsgn vals2