-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Classes and data structures for working with data-kind indexed types
--
-- This package contains collection classes and type representations used
-- for working with values that have a single parameter. It's intended
-- for things like expression libraries where one wishes to leverage the
-- Haskell type-checker to improve type-safety by encoding the object
-- language type system into data kinds.
@package parameterized-utils
@version 2.1.8.0
-- | An unsafe module that provides functionality for constructing equality
-- proofs that GHC cannot prove on its own.
module Data.Parameterized.Axiom
-- | Assert a proof of equality between two types. This is unsafe if used
-- improperly, so use this with caution!
unsafeAxiom :: forall a b. a :~: b
-- | Assert a proof of heterogeneous equality between two types. This is
-- unsafe if used improperly, so use this with caution!
unsafeHeteroAxiom :: forall a b. a :~~: b
-- | Utilities for working with Data.Functor.Compose.
--
-- NB: This module contains an orphan instance. It will be included in
-- GHC 8.10, see
-- https://gitlab.haskell.org/ghc/ghc/merge_requests/273 and also
-- https:/github.comhaskell-compatbase-orphansissues/49.
module Data.Parameterized.Compose
-- | The deduction (via generativity) that if g x :~: g y then
-- x :~: y.
--
-- See https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
testEqualityComposeBare :: forall k l (f :: k -> Type) (g :: l -> k) x y. (forall w z. f w -> f z -> Maybe (w :~: z)) -> Compose f g x -> Compose f g y -> Maybe (x :~: y)
-- | This module declares classes for working with types with the kind
-- k -> * for any kind k. These are generalizations
-- of the Data.Functor.Classes types as they work with any kind
-- k, and are not restricted to *.
module Data.Parameterized.Classes
-- | This class contains types where you can learn the equality of two
-- types from information contained in terms.
--
-- The result should be Just Refl if and only if the types
-- applied to f are equal:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
--
--
-- Typically, only singleton types should inhabit this class. In that
-- case type argument equality coincides with term equality:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
--
--
--
-- isJust (testEquality x y) = x == y
--
--
-- Singleton types are not required, however, and so the latter two
-- would-be laws are not in fact valid in general.
class () => TestEquality (f :: k -> Type)
-- | Conditionally prove the equality of a and b.
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data () => (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
-- | EqF provides a method eqF for testing whether two
-- parameterized types are equal.
--
-- Unlike TestEquality, this only works when the type arguments
-- are the same, and does not provide a proof that the types have the
-- same type when they are equal. Thus this can be implemented over
-- parameterized types that are unable to provide evidence that their
-- type arguments are equal.
class EqF (f :: k -> Type)
eqF :: EqF f => f a -> f a -> Bool
-- | A polymorphic equality operator that generalizes TestEquality.
class PolyEq u v
polyEqF :: PolyEq u v => u -> v -> Maybe (u :~: v)
polyEq :: PolyEq u v => u -> v -> Bool
-- | The OrdF class is a total ordering over parameterized types so
-- that types with different parameters can be compared.
--
-- Instances of OrdF are expected to satisfy the following laws:
--
--
-- - Transitivity if leqF x y && leqF y
-- z = True, then leqF x = z = True
-- - Reflexivity leqF x x = True
-- - Antisymmetry if leqF x y && leqF y
-- x = True, then testEquality x y = Just
-- Refl
--
--
-- Note that the following operator interactions are expected to hold:
--
--
-- - geqF x y iff leqF y x
-- - ltF x y iff leqF x y && testEquality x y =
-- Nothing
-- - gtF x y iff ltF y x
-- - ltF x y iff compareF x y == LTF
-- - gtF x y iff compareF x y == GTF
-- - isJust (testEquality x y) iff compareF x y ==
-- EQF
--
--
-- Furthermore, when x and y both have type (k
-- tp), we expect:
--
--
-- - toOrdering (compareF x y) equals compare x y
-- when Ord (k tp) has an instance.
-- - isJust (testEquality x y) equals x == y when
-- Eq (k tp) has an instance.
--
--
-- Minimal complete definition: either compareF or leqF.
-- Using compareF can be more efficient for complex types.
class TestEquality ktp => OrdF (ktp :: k -> Type)
compareF :: OrdF ktp => ktp x -> ktp y -> OrderingF x y
leqF :: OrdF ktp => ktp x -> ktp y -> Bool
ltF :: OrdF ktp => ktp x -> ktp y -> Bool
geqF :: OrdF ktp => ktp x -> ktp y -> Bool
gtF :: OrdF ktp => ktp x -> ktp y -> Bool
-- | Compare two values, and if they are equal compare the next values,
-- otherwise return LTF or GTF
lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k). OrdF f => f a -> f b -> (a ~ b => OrderingF c d) -> OrderingF c d
-- | Ordering over two distinct types with a proof they are equal.
data OrderingF x y
[LTF] :: OrderingF x y
[EQF] :: OrderingF x x
[GTF] :: OrderingF x y
-- | joinOrderingF x y first compares on x, returning an
-- equivalent value if it is not EQF. If it is EQF, it
-- returns y.
joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d
orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
-- | Convert OrderingF to standard ordering.
toOrdering :: OrderingF x y -> Ordering
-- | Convert standard ordering to OrderingF.
fromOrdering :: Ordering -> OrderingF x x
-- | If the "outer" functor has an OrdF instance, then one can be
-- generated for the "inner" functor. The type-level evidence of equality
-- is deduced via generativity of g, e.g. the inference g x
-- ~ g y implies x ~ y.
ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y. (forall w z. f w -> f z -> OrderingF w z) -> Compose f g x -> Compose f g y -> OrderingF x y
-- | A parameterized type that can be shown on all instances.
--
-- To implement ShowF g, one should implement an instance
-- Show (g tp) for all argument types tp, then
-- write an empty instance instance ShowF g.
class ShowF (f :: k -> Type)
-- | Provides a show instance for each type.
withShow :: ShowF f => p f -> q tp -> (Show (f tp) => a) -> a
-- | Provides a show instance for each type.
withShow :: (ShowF f, Show (f tp)) => p f -> q tp -> (Show (f tp) => a) -> a
showF :: forall tp. ShowF f => f tp -> String
-- | Like showsPrec, the precedence argument is one more than
-- the precedence of the enclosing context.
showsPrecF :: forall tp. ShowF f => Int -> f tp -> String -> String
showsF :: ShowF f => f tp -> String -> String
-- | A parameterized type that is hashable on all instances.
class HashableF (f :: k -> Type)
hashWithSaltF :: HashableF f => Int -> f tp -> Int
-- | Hash with default salt.
hashF :: HashableF f => f tp -> Int
-- | An instance of CoercibleF gives a way to coerce between all the
-- types of a family. We generally use this to witness the fact that the
-- type parameter to rtp is a phantom type by giving an
-- implementation in terms of Data.Coerce.coerce.
class CoercibleF (rtp :: k -> Type)
coerceF :: CoercibleF rtp => rtp a -> rtp b
-- | Captures the value obtained from applying a type to a function so that
-- we can use parameterized class instance to provide unparameterized
-- instances for specific types.
--
-- This is the same as Ap from Control.Applicative, but
-- we introduce our own new type to avoid orphan instances.
newtype TypeAp (f :: k -> Type) (tp :: k)
TypeAp :: f tp -> TypeAp (f :: k -> Type) (tp :: k)
type family IndexF (m :: Type) :: k -> Type
type family IxValueF (m :: Type) :: k -> Type
-- | Parameterized generalization of the lens Ixed class.
class IxedF k m
-- | Given an index into a container, build a traversal that visits the
-- given element in the container, if it exists.
ixF :: forall (x :: k). IxedF k m => IndexF m x -> Traversal' m (IxValueF m x)
-- | Parameterized generalization of the lens Ixed class, but with
-- the guarantee that indexes exist in the container.
class IxedF k m => IxedF' k m
-- | Given an index into a container, build a lens that points into the
-- given element in the container.
ixF' :: forall (x :: k). IxedF' k m => IndexF m x -> Lens' m (IxValueF m x)
-- | Parameterized generalization of the lens At class.
class IxedF k m => AtF k m
-- | Given an index into a container, build a lens that points into the
-- given position in the container, whether or not it currently exists.
-- Setting values of atF to a Just value will insert
-- the value if it does not already exist.
atF :: forall (x :: k). AtF k m => IndexF m x -> Lens' m (Maybe (IxValueF m x))
-- | This class is parameterized by a kind k (typically a data
-- kind), a type constructor f of kind k -> *
-- (typically a GADT of singleton types indexed by k), and an
-- index parameter ctx of kind k.
class KnownRepr (f :: k -> Type) (ctx :: k)
knownRepr :: KnownRepr f ctx => f ctx
-- | The class of types that can be converted to a hash value.
--
-- Minimal implementation: hashWithSalt.
--
-- Note: the hash is not guaranteed to be stable across library
-- versions, operating systems or architectures. For stable hashing use
-- named hashes: SHA256, CRC32 etc.
--
-- If you are looking for Hashable instance in time
-- package, check time-compat
class Eq a => Hashable a
-- | Return a hash value for the argument, using the given salt.
--
-- The general contract of hashWithSalt is:
--
--
-- - If two values are equal according to the == method, then
-- applying the hashWithSalt method on each of the two values
-- must produce the same integer result if the same salt is used
-- in each case.
-- - It is not required that if two values are unequal according
-- to the == method, then applying the hashWithSalt method
-- on each of the two values must produce distinct integer results.
-- However, the programmer should be aware that producing distinct
-- integer results for unequal values may improve the performance of
-- hashing-based data structures.
-- - This method can be used to compute different hash values for the
-- same input by providing a different salt in each application of the
-- method. This implies that any instance that defines
-- hashWithSalt must make use of the salt in its
-- implementation.
-- - hashWithSalt may return negative Int values.
--
hashWithSalt :: Hashable a => Int -> a -> Int
-- | Like hashWithSalt, but no salt is used. The default
-- implementation uses hashWithSalt with some default salt.
-- Instances might want to implement this method to provide a more
-- efficient implementation than the default implementation.
hash :: Hashable a => a -> Int
infixl 0 `hashWithSalt`
-- | The isJust function returns True iff its argument is of
-- the form Just _.
--
-- Examples
--
-- Basic usage:
--
--
-- >>> isJust (Just 3)
-- True
--
--
--
-- >>> isJust (Just ())
-- True
--
--
--
-- >>> isJust Nothing
-- False
--
--
-- Only the outer constructor is taken into consideration:
--
--
-- >>> isJust (Just Nothing)
-- True
--
isJust :: Maybe a -> Bool
instance forall k (ctx :: k). Data.Parameterized.Classes.KnownRepr Data.Proxy.Proxy ctx
instance forall k (f :: k -> *) (tp :: k). Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Classes.TypeAp f tp)
instance forall k (f :: k -> *) (tp :: k). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Classes.TypeAp f tp)
instance forall k (f :: k -> *) (tp :: k). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Classes.TypeAp f tp)
instance forall k (f :: k -> *) (tp :: k). (Data.Parameterized.Classes.HashableF f, Data.Type.Equality.TestEquality f) => Data.Hashable.Class.Hashable (Data.Parameterized.Classes.TypeAp f tp)
instance Data.Hashable.Class.Hashable a => Data.Parameterized.Classes.HashableF (Data.Functor.Const.Const a)
instance GHC.Show.Show x => Data.Parameterized.Classes.ShowF (Data.Functor.Const.Const x)
instance Data.Parameterized.Classes.ShowF Data.Proxy.Proxy
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> k1). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Functor.Compose.Compose f g)
instance GHC.Classes.Eq a => Data.Parameterized.Classes.EqF (Data.Functor.Const.Const a)
instance Data.Parameterized.Classes.EqF Data.Proxy.Proxy
instance Data.Parameterized.Classes.CoercibleF (Data.Functor.Const.Const x)
-- | This module defines type-level lists used for representing the type of
-- variables in a context.
--
-- A Ctx is never intended to be manipulated at the value level;
-- it is used purely as a type-level list, just like '[]. To see
-- how it is used, see the module header for
-- Data.Parameterized.Context.
module Data.Parameterized.Ctx
-- | Kind Ctx k comprises lists of types of kind
-- k.
data Ctx k
EmptyCtx :: Ctx k
(::>) :: Ctx k -> k -> Ctx k
type EmptyCtx = 'EmptyCtx
type SingleCtx x = EmptyCtx ::> x
type (c :: Ctx k) ::> (a :: k) = c '::> a
-- | Append two type-level contexts.
type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k
-- | This type family computes the number of elements in a Ctx
type family CtxSize (a :: Ctx k) :: Nat
-- | Lookup the value in a context by number, from the left. Produce a type
-- error if the index is out of range.
type CtxLookup (n :: Nat) (ctx :: Ctx k) = CtxLookupRight (FromLeft ctx n) ctx
-- | Update the value in a context by number, from the left. If the index
-- is out of range, the context is unchanged.
type CtxUpdate (n :: Nat) (x :: k) (ctx :: Ctx k) = CtxUpdateRight (FromLeft ctx n) x ctx
-- | Lookup the value in a context by number, from the right
type family CtxLookupRight (n :: Nat) (ctx :: Ctx k) :: k
-- | Update the value in a context by number, from the right. If the index
-- is out of range, the context is unchanged.
type family CtxUpdateRight (n :: Nat) (x :: k) (ctx :: Ctx k) :: Ctx k
-- | Flatten a nested context
type family CtxFlatten (ctx :: Ctx (Ctx a)) :: Ctx a
-- | Helper type family used to generate descriptive error messages when an
-- index is larger than the length of the Ctx being indexed.
type family CheckIx (ctx :: Ctx k) (n :: Nat) (b :: Bool) :: Constraint
-- | A constraint that checks that the nat n is a valid index into
-- the context ctx, and raises a type error if not.
type ValidIx (n :: Nat) (ctx :: Ctx k) = CheckIx ctx n (n + 1 <=? CtxSize ctx)
-- | Ctx is a snoc-list. In order to use the more intuitive
-- left-to-right ordering of elements the desired index is subtracted
-- from the total number of elements.
type FromLeft ctx n = CtxSize ctx - 1 - n
-- | This reflects type level proofs involving contexts.
module Data.Parameterized.Ctx.Proofs
leftId :: p x -> (EmptyCtx <+> x) :~: x
assoc :: p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
-- | This defines a class DecidableEq, which represents decidable
-- equality on a type family.
--
-- This is different from GHC's TestEquality in that it provides
-- evidence of non-equality. In fact, it is a superclass of
-- TestEquality.
module Data.Parameterized.DecidableEq
-- | Decidable equality.
class DecidableEq f
decEq :: DecidableEq f => f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)
-- | This module provides a simple generator of new indexes in the ST
-- monad. It is predictable and not intended for cryptographic purposes.
--
-- NOTE: the TestEquality and OrdF instances for the
-- Nonce type simply compare the generated nonce values and then
-- assert to the compiler (via unsafeCoerce) that the types
-- ascribed to the nonces are equal if their values are equal. This is
-- only OK because of the discipline by which nonces should be used: they
-- should only be generated from a NonceGenerator (i.e., should
-- not be built directly), and nonces from different generators must
-- never be compared! Arranging to compare Nonces from different origins
-- would allow users to build unsafeCoerce via the
-- testEquality function.
--
-- This module is deprecated, and should not be used in new code. Clients
-- of this module should migrate to use Data.Parameterized.Nonce.
-- | Deprecated: Migrate to use Data.Parameterized.Nonce instead, this
-- module will be removed soon.
module Data.Parameterized.Nonce.Unsafe
-- | A simple type that for getting fresh indices in the ST monad.
-- The type parameter s is used for the ST monad
-- parameter.
data NonceGenerator s
-- | Create a new counter.
newNonceGenerator :: ST s (NonceGenerator s)
-- | Get a fresh index and increment the counter.
freshNonce :: NonceGenerator s -> ST s (Nonce tp)
-- | Return true if counter has reached the limit, and can't be incremented
-- without risk of error.
atLimit :: NonceGenerator s -> ST s Bool
-- | An index generated by the counter.
data Nonce (tp :: k)
indexValue :: Nonce tp -> Word64
instance forall k (tp :: k). GHC.Show.Show (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance forall k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Unsafe.Nonce tp)
instance Data.Type.Equality.TestEquality Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.OrdF Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Nonce.Unsafe.Nonce
instance Data.Parameterized.Classes.ShowF Data.Parameterized.Nonce.Unsafe.Nonce
-- | This module declares template Haskell primitives so that it is easier
-- to work with GADTs that have many constructors.
module Data.Parameterized.TH.GADT
-- | structuralEquality declares a structural equality predicate.
structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
-- | structuralTypeEquality f returns a function with the type:
-- forall x y . f x -> f y -> Maybe (x :~: y)
structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
-- | 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
-- parameters in a simple case expression in order to avoid stressing
-- GHC's coverage checker. In the case that the first and second
-- parameters have unique constructors, a simple numeric comparison is
-- done to compute the result.
structuralTypeOrd :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
-- | structuralTraversal tp generates a function that applies a
-- traversal f to the subterms with free variables in
-- tp.
structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
-- | structuralShow tp generates a function with the type tp
-- -> ShowS that shows the constructor.
structuralShowsPrec :: TypeQ -> ExpQ
-- | structuralHash tp generates a function with the type Int
-- -> tp -> Int that hashes type.
--
-- All arguments use hashable, and structuralHashWithSalt
-- can be used instead as it allows user-definable patterns to be used at
-- specific types.
-- | Deprecated: Use structuralHashWithSalt
structuralHash :: TypeQ -> ExpQ
-- | structuralHashWithSalt tp generates a function with the type
-- Int -> tp -> Int that hashes type.
--
-- The second arguments is for generating user-defined patterns to
-- replace hashWithSalt for specific types.
structuralHashWithSalt :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
-- | A polymorphic equality operator that generalizes TestEquality.
class PolyEq u v
polyEqF :: PolyEq u v => u -> v -> Maybe (u :~: v)
polyEq :: PolyEq u v => u -> v -> Bool
-- | Generate a "repr" or singleton type from a data kind. For nullary
-- constructors, this works as follows:
--
--
-- data T1 = A | B | C
-- $(mkRepr ''T1)
-- ======>
-- data T1Repr (tp :: T1)
-- where
-- ARepr :: T1Repr 'A
-- BRepr :: T1Repr 'B
-- CRepr :: T1Repr 'C
--
--
-- For constructors with fields, we assume each field type T
-- already has a corresponding repr type TRepr :: T -> *.
--
--
-- data T2 = T2_1 T1 | T2_2 T1
-- $(mkRepr ''T2)
-- ======>
-- data T2Repr (tp :: T2)
-- where
-- T2_1Repr :: T1Repr tp -> T2Repr ('T2_1 tp)
-- T2_2Repr :: T1Repr tp -> T2Repr ('T2_2 tp)
--
--
-- Constructors with multiple fields work fine as well:
--
--
-- data T3 = T3 T1 T2
-- $(mkRepr ''T3)
-- ======>
-- data T3Repr (tp :: T3)
-- where
-- T3Repr :: T1Repr tp1 -> T2Repr tp2 -> T3Repr ('T3 tp1 tp2)
--
--
-- This is generally compatible with other "repr" types provided by
-- parameterized-utils, such as NatRepr and
-- PeanoRepr:
--
--
-- data T4 = T4_1 Nat | T4_2 Peano
-- $(mkRepr ''T4)
-- ======>
-- data T4Repr (tp :: T4)
-- where
-- T4Repr :: NatRepr tp1 -> PeanoRepr tp2 -> T4Repr ('T4 tp1 tp2)
--
--
-- The data kind must be "simple", i.e. it must be monomorphic and only
-- contain user-defined data constructors (no lists, tuples, etc.). For
-- example, the following will not work:
--
--
-- data T5 a = T5 a
-- $(mkRepr ''T5)
-- ======>
-- Foo.hs:1:1: error:
-- Exception when trying to run compile-time code:
-- mkRepr cannot be used on polymorphic data kinds.
--
--
-- Similarly, this will not work:
--
--
-- data T5 = T5 [Nat]
-- $(mkRepr ''T5)
-- ======>
-- Foo.hs:1:1: error:
-- Exception when trying to run compile-time code:
-- mkRepr cannot be used on this data kind.
--
--
-- Note that at a minimum, you will need the following extensions to use
-- this macro:
--
--
-- {-# LANGUAGE DataKinds #-}
-- {-# LANGUAGE GADTs #-}
-- {-# LANGUAGE KindSignatures #-}
-- {-# LANGUAGE TemplateHaskell #-}
--
mkRepr :: Name -> DecsQ
-- | Generate KnownRepr instances for each constructor of a data
-- kind. Given a data kind T, we assume a repr type TRepr (t
-- :: T) is in scope with structure that perfectly matches
-- T (using mkRepr to generate the repr type will
-- guarantee this).
--
-- Given data kinds T1, T2, and T3 from the
-- documentation of mkRepr, and the associated repr types
-- T1Repr, T2Repr, and T3Repr, we can use
-- mkKnownReprs to generate these instances like so:
--
--
-- $(mkKnownReprs ''T1)
-- ======>
-- instance KnownRepr T1Repr 'A where
-- knownRepr = ARepr
-- instance KnownRepr T1Repr 'B where
-- knownRepr = BRepr
-- instance KnownRepr T1Repr 'C where
-- knownRepr = CRepr
--
--
--
-- $(mkKnownReprs ''T2)
-- ======>
-- instance KnownRepr T1Repr tp =>
-- KnownRepr T2Repr ('T2_1 tp) where
-- knownRepr = T2_1Repr knownRepr
--
--
--
-- $(mkKnownReprs ''T3)
-- ======>
-- instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) =>
-- KnownRepr T3Repr ('T3_1 tp1 tp2) where
-- knownRepr = T3_1Repr knownRepr knownRepr
--
--
-- The same restrictions that apply to mkRepr also apply to
-- mkKnownReprs. The data kind must be "simple", i.e. it must be
-- monomorphic and only contain user-defined data constructors (no lists,
-- tuples, etc.).
--
-- Note that at a minimum, you will need the following extensions to use
-- this macro:
--
--
-- {-# LANGUAGE DataKinds #-}
-- {-# LANGUAGE GADTs #-}
-- {-# LANGUAGE KindSignatures #-}
-- {-# LANGUAGE MultiParamTypeClasses #-}
-- {-# LANGUAGE TemplateHaskell #-}
--
--
-- Also, mkKnownReprs must be used in the same module as the
-- definition of the repr type (not necessarily for the data kind).
mkKnownReprs :: Name -> DecsQ
type DataD = DatatypeInfo
lookupDataType' :: Name -> Q DatatypeInfo
asTypeCon :: String -> Type -> Q Name
-- | Given a constructor and string, this generates a pattern for matching
-- the expression, and the names of variables bound by pattern in order
-- they appear in constructor.
conPat :: ConstructorInfo -> String -> Q (Pat, [Name])
-- | 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
-- | The application of a type.
TypeApp :: TypePat -> TypePat -> TypePat
-- | Match any type.
AnyType :: TypePat
-- | Match the i'th argument of the data type we are traversing.
DataArg :: Int -> TypePat
-- | Match a ground type.
ConType :: TypeQ -> TypePat
-- | The dataParamTypes function returns the list of Type arguments for the
-- constructor. For example, if passed the DatatypeInfo for a newtype
-- Id a = MkId a then this would return [SigT
-- (VarT a) StarT]. Note that there may be type
-- *variables* not referenced in the returned array; this simply returns
-- the type *arguments*.
dataParamTypes :: DatatypeInfo -> [Type]
-- | Find value associated with first pattern that matches given pat if
-- any.
assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)
module Data.Parameterized.DataKind
data PairRepr (f :: k1 -> Type) (g :: k2 -> Type) (p :: (k1, k2))
[PairRepr] :: f a -> g b -> PairRepr f g '(a, b)
type family Fst (pair :: (k1, k2))
type family Snd (pair :: (k1, k2))
fst :: PairRepr f g p -> f (Fst p)
snd :: PairRepr f g p -> g (Snd p)
instance forall k1 k2 (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g b)) => GHC.Classes.Eq (Data.Parameterized.DataKind.PairRepr f g '(a, b))
instance forall k1 k2 (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2). (GHC.Classes.Ord (f a), GHC.Classes.Ord (g b)) => GHC.Classes.Ord (Data.Parameterized.DataKind.PairRepr f g '(a, b))
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *) (p :: (k1, k2)). (Data.Parameterized.Classes.ShowF f, Data.Parameterized.Classes.ShowF g) => GHC.Show.Show (Data.Parameterized.DataKind.PairRepr f g p)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Parameterized.Classes.ShowF f, Data.Parameterized.Classes.ShowF g) => Data.Parameterized.Classes.ShowF (Data.Parameterized.DataKind.PairRepr f g)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Type.Equality.TestEquality f, Data.Type.Equality.TestEquality g) => Data.Type.Equality.TestEquality (Data.Parameterized.DataKind.PairRepr f g)
instance forall k1 k2 (f :: k1 -> *) (g :: k2 -> *). (Data.Parameterized.Classes.OrdF f, Data.Parameterized.Classes.OrdF g) => Data.Parameterized.Classes.OrdF (Data.Parameterized.DataKind.PairRepr f g)
-- | This module declares classes for working with structures that accept a
-- parametric type parameter followed by some fixed kind.
module Data.Parameterized.TraversableFC
-- | A parameterized class for types which can be tested for parameterized
-- equality, when given an equality test for subterms.
class TestEqualityFC (t :: (k -> Type) -> l -> Type)
testEqualityFC :: forall f. TestEqualityFC t => (forall x y. f x -> f y -> Maybe (x :~: y)) -> forall x y. t f x -> t f y -> Maybe (x :~: y)
-- | A parameterized class for types which can be tested for parameterized
-- ordering, when given an comparison test for subterms.
class TestEqualityFC t => OrdFC (t :: (k -> Type) -> l -> Type)
compareFC :: forall f. OrdFC t => (forall x y. f x -> f y -> OrderingF x y) -> forall x y. t f x -> t f y -> OrderingF x y
-- | A parameterized class for types which can be shown, when given
-- functions to show parameterized subterms.
class ShowFC (t :: (k -> Type) -> l -> Type)
showFC :: forall f. ShowFC t => (forall x. f x -> String) -> forall x. t f x -> String
showsPrecFC :: forall f. ShowFC t => (forall x. Int -> f x -> ShowS) -> forall x. Int -> t f x -> ShowS
-- | A parameterized class for types which can be hashed, when given
-- functions to hash parameterized subterms.
class HashableFC (t :: (k -> Type) -> l -> Type)
hashWithSaltFC :: forall f. HashableFC t => (forall x. Int -> f x -> Int) -> forall x. Int -> t f x -> Int
-- | A parameterized type that is a functor on all instances.
--
-- Laws:
--
--
class FunctorFC (t :: (k -> Type) -> l -> Type)
fmapFC :: forall f g. FunctorFC t => (forall x. f x -> g x) -> forall x. t f x -> t g x
-- | This is a generalization of the Foldable class to structures
-- over parameterized terms.
class FoldableFC (t :: (k -> Type) -> l -> Type)
-- | Map each element of the structure to a monoid, and combine the
-- results.
foldMapFC :: forall f m. (FoldableFC t, Monoid m) => (forall x. f x -> m) -> forall x. t f x -> m
-- | Right-associative fold of a structure.
foldrFC :: forall f b. FoldableFC t => (forall x. f x -> b -> b) -> forall x. b -> t f x -> b
-- | Left-associative fold of a structure.
foldlFC :: forall f b. FoldableFC t => (forall x. b -> f x -> b) -> forall x. b -> t f x -> b
-- | Right-associative fold of a structure, but with strict application of
-- the operator.
foldrFC' :: forall f b. FoldableFC t => (forall x. f x -> b -> b) -> forall x. b -> t f x -> b
-- | Left-associative fold of a parameterized structure with a strict
-- accumulator.
foldlFC' :: forall f b. FoldableFC t => (forall x. b -> f x -> b) -> forall x. b -> t f x -> b
-- | Convert structure to list.
toListFC :: forall f a. FoldableFC t => (forall x. f x -> a) -> forall x. t f x -> [a]
-- | Monadic fold over the elements of a structure from left to right.
foldlMFC :: (FoldableFC t, Monad m) => (forall x. b -> f x -> m b) -> b -> t f c -> m b
-- | Monadic strict fold over the elements of a structure from left to
-- right.
foldlMFC' :: (FoldableFC t, Monad m) => (forall x. b -> f x -> m b) -> b -> t f c -> m b
-- | Monadic fold over the elements of a structure from right to left.
foldrMFC :: (FoldableFC t, Monad m) => (forall x. f x -> b -> m b) -> b -> t f c -> m b
-- | Monadic strict fold over the elements of a structure from right to
-- left.
foldrMFC' :: (FoldableFC t, Monad m) => (forall x. f x -> b -> m b) -> b -> t f c -> m b
class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> Type) -> l -> Type)
traverseFC :: forall f g m. (TraversableFC t, Applicative m) => (forall x. f x -> m (g x)) -> forall x. t f x -> m (t g x)
-- | Map each element of a structure to an action, evaluate these actions
-- from left to right, and ignore the results.
traverseFC_ :: (FoldableFC t, Applicative m) => (forall x. f x -> m a) -> forall x. t f x -> m ()
-- | Map each element of a structure to an action, evaluate these actions
-- from left to right, and ignore the results.
-- | Deprecated: Use forFC_
forMFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
-- | Map each element of a structure to an action, evaluate these actions
-- from left to right, and ignore the results.
forFC_ :: (FoldableFC t, Applicative m) => t f c -> (forall x. f x -> m a) -> m ()
-- | Flipped traverseFC
forFC :: (TraversableFC t, Applicative m) => t f x -> (forall y. f y -> m (g y)) -> m (t g x)
-- | This function may be used as a value for fmapF in a
-- FunctorF instance.
fmapFCDefault :: TraversableFC t => forall f g. (forall x. f x -> g x) -> forall x. t f x -> t g x
-- | This function may be used as a value for foldMap in a
-- Foldable instance.
foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> forall x. t f x -> m
-- | Return True if all values satisfy predicate.
allFC :: FoldableFC t => (forall x. f x -> Bool) -> forall x. t f x -> Bool
-- | Return True if any values satisfy predicate.
anyFC :: FoldableFC t => (forall x. f x -> Bool) -> forall x. t f x -> Bool
-- | Return number of elements that we fold over.
lengthFC :: FoldableFC t => t f x -> Int
-- | This module declares classes for working with structures that accept a
-- single parametric type parameter.
module Data.Parameterized.TraversableF
-- | A parameterized type that is a functor on all instances.
class FunctorF m
fmapF :: FunctorF m => (forall x. f x -> g x) -> m f -> m g
-- | This is a generalization of the Foldable class to structures
-- over parameterized terms.
class FoldableF (t :: (k -> Type) -> Type)
-- | Map each element of the structure to a monoid, and combine the
-- results.
foldMapF :: (FoldableF t, Monoid m) => (forall s. e s -> m) -> t e -> m
-- | Right-associative fold of a structure.
foldrF :: FoldableF t => (forall s. e s -> b -> b) -> b -> t e -> b
-- | Left-associative fold of a structure.
foldlF :: FoldableF t => (forall s. b -> e s -> b) -> b -> t e -> b
-- | Right-associative fold of a structure, but with strict application of
-- the operator.
foldrF' :: FoldableF t => (forall s. e s -> b -> b) -> b -> t e -> b
-- | Left-associative fold of a parameterized structure with a strict
-- accumulator.
foldlF' :: FoldableF t => (forall s. b -> e s -> b) -> b -> t e -> b
-- | Convert structure to list.
toListF :: FoldableF t => (forall tp. f tp -> a) -> t f -> [a]
-- | Monadic fold over the elements of a structure from left to right.
foldlMF :: (FoldableF t, Monad m) => (forall x. b -> f x -> m b) -> b -> t f -> m b
-- | Monadic strict fold over the elements of a structure from left to
-- right.
foldlMF' :: (FoldableF t, Monad m) => (forall x. b -> f x -> m b) -> b -> t f -> m b
-- | Monadic fold over the elements of a structure from right to left.
foldrMF :: (FoldableF t, Monad m) => (forall x. f x -> b -> m b) -> b -> t f -> m b
-- | Monadic strict fold over the elements of a structure from right to
-- left.
foldrMF' :: (FoldableF t, Monad m) => (forall x. f x -> b -> m b) -> b -> t f -> m b
class (FunctorF t, FoldableF t) => TraversableF t
traverseF :: (TraversableF t, Applicative m) => (forall s. e s -> m (f s)) -> t e -> m (t f)
-- | Map each element of a structure to an action, evaluate these actions
-- from left to right, and ignore the results.
traverseF_ :: (FoldableF t, Applicative f) => (forall s. e s -> f a) -> t e -> f ()
-- | Map each element of a structure to an action, evaluate these actions
-- from left to right, and ignore the results.
forF_ :: (FoldableF t, Applicative m) => t f -> (forall x. f x -> m a) -> m ()
-- | Flipped traverseF
forF :: (TraversableF t, Applicative m) => t e -> (forall s. e s -> m (f s)) -> m (t f)
-- | This function may be used as a value for fmapF in a
-- FunctorF instance.
fmapFDefault :: TraversableF t => (forall s. e s -> f s) -> t e -> t f
-- | This function may be used as a value for foldMap in a
-- Foldable instance.
foldMapFDefault :: (TraversableF t, Monoid m) => (forall s. e s -> m) -> t e -> m
-- | Return True if all values satisfy the predicate.
allF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool
-- | Return True if any values satisfy the predicate.
anyF :: FoldableF t => (forall tp. f tp -> Bool) -> t f -> Bool
-- | Return number of elements that we fold over.
lengthF :: FoldableF t => t f -> Int
instance Data.Parameterized.TraversableF.TraversableF (Data.Functor.Const.Const x)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.FoldableF (Data.Functor.Compose.Compose s t)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.TraversableF s, Data.Parameterized.TraversableFC.TraversableFC t) => Data.Parameterized.TraversableF.TraversableF (Data.Functor.Compose.Compose s t)
instance Data.Parameterized.TraversableF.FoldableF (Data.Functor.Const.Const x)
instance Data.Parameterized.TraversableF.FunctorF (Data.Functor.Const.Const x)
instance forall k (s :: (k -> *) -> *) l (t :: (l -> *) -> k -> *). (Data.Parameterized.TraversableF.FunctorF s, Data.Parameterized.TraversableFC.FunctorFC t) => Data.Parameterized.TraversableF.FunctorF (Data.Functor.Compose.Compose s t)
-- | This module provides Some, a GADT that hides a type parameter.
module Data.Parameterized.Some
data Some (f :: k -> Type)
Some :: f x -> Some (f :: k -> Type)
-- | Project out of Some.
viewSome :: (forall tp. f tp -> r) -> Some f -> r
-- | Apply function to inner value.
mapSome :: (forall tp. f tp -> g tp) -> Some f -> Some g
-- | Modify the inner value.
traverseSome :: Functor m => (forall tp. f tp -> m (g tp)) -> Some f -> m (Some g)
-- | Modify the inner value.
traverseSome_ :: Functor m => (forall tp. f tp -> m ()) -> Some f -> m ()
-- | A lens that is polymorphic in the index may be used on a value with an
-- existentially-quantified index.
someLens :: (forall tp. Lens' (f tp) a) -> Lens' (Some f) a
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => GHC.Classes.Eq (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => GHC.Classes.Ord (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). (Data.Parameterized.Classes.HashableF f, Data.Type.Equality.TestEquality f) => Data.Hashable.Class.Hashable (Data.Parameterized.Some.Some f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.Some.Some f)
instance Data.Parameterized.TraversableF.FunctorF Data.Parameterized.Some.Some
instance Data.Parameterized.TraversableF.FoldableF Data.Parameterized.Some.Some
instance Data.Parameterized.TraversableF.TraversableF Data.Parameterized.Some.Some
-- | This defines a type family SymbolRepr for representing a
-- type-level string (AKA symbol) at runtime. This can be used to branch
-- on a type-level value.
--
-- The TestEquality and OrdF instances for
-- SymbolRepr are implemented using unsafeCoerce. This
-- should be typesafe because we maintain the invariant that the string
-- value contained in a SymbolRepr value matches its static type.
--
-- At the type level, symbols have very few operations, so SymbolRepr
-- correspondingly has very few functions that manipulate them.
module Data.Parameterized.SymbolRepr
-- | A runtime representation of a GHC type-level symbol.
data SymbolRepr (nm :: Symbol)
-- | The underlying text representation of the symbol
symbolRepr :: SymbolRepr nm -> Text
-- | Generate a value representative for the type level symbol.
knownSymbol :: KnownSymbol s => SymbolRepr s
-- | Generate a symbol representative at runtime. The type-level symbol
-- will be abstract, as it is hidden by the Some constructor.
someSymbol :: Text -> Some SymbolRepr
-- | The SomeSym hides a Symbol parameter but preserves a KnownSymbol
-- constraint on the hidden parameter.
data SomeSym (c :: Symbol -> Type)
SomeSym :: c s -> SomeSym (c :: Symbol -> Type)
-- | Projects a value out of a SomeSym into a function, re-ifying the
-- Symbol type parameter to the called function, along with the
-- KnownSymbol constraint on that Symbol value.
viewSomeSym :: (forall (s :: Symbol). KnownSymbol s => c s -> r) -> SomeSym c -> r
-- | (Kind) This is the kind of type-level symbols.
data () => Symbol
-- | This class gives the string associated with a type-level symbol. There
-- are instances of the class for every concrete literal: "hello", etc.
class () => KnownSymbol (n :: Symbol)
instance GHC.TypeLits.KnownSymbol s => Data.Parameterized.Classes.KnownRepr Data.Parameterized.SymbolRepr.SymbolRepr s
instance Data.Type.Equality.TestEquality Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.SymbolRepr.SymbolRepr
instance GHC.Classes.Eq (Data.Parameterized.SymbolRepr.SymbolRepr x)
instance GHC.Classes.Ord (Data.Parameterized.SymbolRepr.SymbolRepr x)
instance Data.Parameterized.Classes.HashableF Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Hashable.Class.Hashable (Data.Parameterized.SymbolRepr.SymbolRepr nm)
instance GHC.Show.Show (Data.Parameterized.SymbolRepr.SymbolRepr nm)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.SymbolRepr.SymbolRepr
-- | This module provides a simple generator of new indexes in the
-- ST monad. It is predictable and not intended for cryptographic
-- purposes.
--
-- This module also provides a global nonce generator that will generate
-- 2^64 nonces before repeating.
--
-- NOTE: The TestEquality and OrdF instances for the
-- Nonce type simply compare the generated nonce values and then
-- assert to the compiler (via unsafeCoerce) that the types
-- ascribed to the nonces are equal if their values are equal.
module Data.Parameterized.Nonce
-- | Provides a monadic action for getting fresh typed names.
--
-- The first type parameter m is the monad used for generating
-- names, and the second parameter s is used for the counter.
data NonceGenerator (m :: Type -> Type) (s :: Type)
freshNonce :: forall m s k (tp :: k). NonceGenerator m s -> m (Nonce s tp)
-- | The number of nonces generated so far by this generator. Only really
-- useful for profiling.
countNoncesGenerated :: NonceGenerator m s -> m Integer
-- | An index generated by the counter.
data Nonce (s :: Type) (tp :: k)
indexValue :: Nonce s tp -> Word64
-- | Create a new nonce generator in the ST monad.
newSTNonceGenerator :: ST t (Some (NonceGenerator (ST t)))
-- | Create a new nonce generator in the IO monad.
newIONonceGenerator :: IO (Some (NonceGenerator IO))
-- | Run an IO computation with a new nonce generator in the
-- IO monad.
withIONonceGenerator :: (forall s. NonceGenerator IO s -> IO r) -> IO r
-- | Run an ST computation with a new nonce generator in the
-- ST monad.
withSTNonceGenerator :: (forall s. NonceGenerator (ST t) s -> ST t r) -> ST t r
-- | This combines runST and newSTNonceGenerator to create a
-- nonce generator that shares the same phantom type parameter as the
-- ST monad.
--
-- This can be used to reduce the number of type parameters when we know
-- a ST computation only needs a single NonceGenerator.
runSTNonceGenerator :: (forall s. NonceGenerator (ST s) s -> ST s a) -> a
-- | Create a new counter.
withGlobalSTNonceGenerator :: (forall t. NonceGenerator (ST t) t -> ST t r) -> r
data GlobalNonceGenerator
-- | A nonce generator that uses a globally-defined counter.
globalNonceGenerator :: NonceGenerator IO GlobalNonceGenerator
instance forall s k (tp :: k). GHC.Show.Show (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). Data.Hashable.Class.Hashable (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). GHC.Classes.Ord (Data.Parameterized.Nonce.Nonce s tp)
instance forall s k (tp :: k). GHC.Classes.Eq (Data.Parameterized.Nonce.Nonce s tp)
instance Data.Type.Equality.TestEquality (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.OrdF (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.HashableF (Data.Parameterized.Nonce.Nonce s)
instance Data.Parameterized.Classes.ShowF (Data.Parameterized.Nonce.Nonce s)
-- | This module provides a typeclass and monad transformers for generating
-- nonces.
module Data.Parameterized.Nonce.Transformers
-- | A MonadNonce is a monad that can generate fresh Nonces
-- in a given set (where we view the phantom type parameter of
-- Nonce as a designator of the set that the Nonce came
-- from).
class Monad m => MonadNonce m where {
type NonceSet m :: Type;
}
freshNonceM :: forall k (tp :: k). MonadNonce m => m (Nonce (NonceSet m) tp)
-- | This transformer adds a nonce generator to a given monad.
newtype NonceT s m a
NonceT :: ReaderT (NonceGenerator m s) m a -> NonceT s m a
[runNonceT] :: NonceT s m a -> ReaderT (NonceGenerator m s) m a
-- | Helper type to build a MonadNonce from the ST monad.
type NonceST t s = NonceT s (ST t)
-- | Helper type to build a MonadNonce from the IO monad.
type NonceIO s = NonceT s IO
-- | Return the actual NonceGenerator used in an ST
-- computation.
getNonceSTGen :: NonceST t s (NonceGenerator (ST t) s)
-- | Run a NonceST computation with a fresh NonceGenerator.
runNonceST :: (forall t s. NonceST t s a) -> a
-- | Run a NonceIO computation with a fresh NonceGenerator
-- inside IO.
runNonceIO :: (forall s. NonceIO s a) -> IO a
instance GHC.Base.Monad m => GHC.Base.Monad (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Base.Applicative m => GHC.Base.Applicative (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance Control.Monad.Trans.Class.MonadTrans (Data.Parameterized.Nonce.Transformers.NonceT s)
instance GHC.Base.Monad m => Data.Parameterized.Nonce.Transformers.MonadNonce (Data.Parameterized.Nonce.Transformers.NonceT s m)
instance Data.Parameterized.Nonce.Transformers.MonadNonce m => Data.Parameterized.Nonce.Transformers.MonadNonce (Control.Monad.Trans.State.Lazy.StateT s m)
-- | This defines a type NatRepr for representing a type-level
-- natural at runtime. This can be used to branch on a type-level value.
-- For each n, NatRepr n contains a single value
-- containing the value n. This can be used to help use
-- type-level variables on code with data dependendent types.
--
-- The TestEquality and DecidableEq instances for
-- NatRepr are implemented using unsafeCoerce, as is the
-- isZeroNat function. This should be typesafe because we maintain
-- the invariant that the integer value contained in a NatRepr value
-- matches its static type.
module Data.Parameterized.NatRepr
-- | A runtime presentation of a type-level Nat.
--
-- This can be used for performing dynamic checks on a type-level natural
-- numbers.
data NatRepr (n :: Nat)
-- | The underlying natural value of the number.
natValue :: NatRepr n -> Natural
intValue :: NatRepr n -> Integer
-- | This generates a NatRepr from a type-level context.
knownNat :: forall n. KnownNat n => NatRepr n
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
data IsZeroNat n
[ZeroNat] :: IsZeroNat 0
[NonZeroNat] :: IsZeroNat (n + 1)
isZeroNat :: NatRepr n -> IsZeroNat n
-- | Every nat is either zero or >= 1.
isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
-- | Result of comparing two numbers.
data NatComparison m n
[NatLT] :: (x + 1) <= (x + (y + 1)) => !NatRepr y -> NatComparison x (x + (y + 1))
[NatEQ] :: NatComparison x x
[NatGT] :: (x + 1) <= (x + (y + 1)) => !NatRepr y -> NatComparison (x + (y + 1)) x
compareNat :: NatRepr m -> NatRepr n -> NatComparison m n
-- | Decrement a NatRepr
decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)
-- | Get the predecessor of a nat
predNat :: NatRepr (n + 1) -> NatRepr n
-- | Increment a NatRepr
incNat :: NatRepr n -> NatRepr (n + 1)
addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)
subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)
divNat :: 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m
halfNat :: NatRepr (n + n) -> NatRepr n
withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a
natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)
-- | Turn an Integral value into a NatRepr. Returns
-- Nothing if the given value is negative.
someNat :: Integral a => a -> Maybe (Some NatRepr)
-- | Turn a Natural into the corresponding NatRepr
mkNatRepr :: Natural -> Some NatRepr
-- | Return the maximum of two nat representations.
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
-- | Recursor for natural numbeers.
natRec :: forall p f. NatRepr p -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f p
-- | Strong induction variant of the recursor.
natRecStrong :: forall p f. NatRepr p -> f 0 -> (forall n. NatRepr n -> (forall m. m <= n => NatRepr m -> f m) -> f (n + 1)) -> f p
-- | Bounded recursor for natural numbers.
--
-- If you can prove: - Base case: f 0 - Inductive step: if n <= h and
-- (f n) then (f (n + 1)) You can conclude: for all n <= h, (f (n +
-- 1)).
natRecBounded :: forall m h f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall n. n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1)
-- | A version of natRecBounded which doesn't require the type index
-- of the result to be greater than 0 and provides a strict
-- inequality constraint.
natRecStrictlyBounded :: forall m f. NatRepr m -> f 0 -> (forall n. (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m
-- | Apply a function to each element in a range; return the list of values
-- obtained.
natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a]
-- | Apply a function to each element in a range starting at zero; return
-- the list of values obtained.
natFromZero :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> [a]
data NatCases m n
[NatCaseLT] :: LeqProof (m + 1) n -> NatCases m n
[NatCaseEQ] :: NatCases m m
[NatCaseGT] :: LeqProof (n + 1) m -> NatCases m n
testNatCases :: forall m n. NatRepr m -> NatRepr n -> NatCases m n
-- | The strict order (<), defined by n < m <-> n + 1 <= m,
-- is irreflexive.
lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
-- | The strict order on the naturals is asymmetric
lessThanAsymmetric :: forall m f n. LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void
-- | Return the value of the nat representation.
widthVal :: NatRepr n -> Int
-- | Return minimum unsigned value for bitvector with given width (always
-- 0).
minUnsigned :: NatRepr w -> Integer
-- | Return maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> Integer
-- | Return minimum value for bitvector in two's complement with given
-- width.
minSigned :: 1 <= w => NatRepr w -> Integer
-- | Return maximum value for bitvector in two's complement with given
-- width.
maxSigned :: 1 <= w => NatRepr w -> Integer
-- | toUnsigned w i maps i to a i mod
-- 2^w.
toUnsigned :: NatRepr w -> Integer -> Integer
-- | toSigned w i interprets the least-significant w bits
-- in i as a signed number in two's complement notation and
-- returns that value.
toSigned :: 1 <= w => NatRepr w -> Integer -> Integer
-- | unsignedClamp w i rounds i to the nearest value
-- between 0 and 2^w-1 (inclusive).
unsignedClamp :: NatRepr w -> Integer -> Integer
-- | signedClamp w i rounds i to the nearest value
-- between -2^(w-1) and 2^(w-1)-1 (inclusive).
signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer
-- | LeqProof m n is a type whose values are only inhabited when
-- m is less than or equal to n.
data LeqProof (m :: Nat) (n :: Nat)
[LeqProof] :: m <= n => LeqProof m n
-- | (<=) is a decidable relation on nats.
decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
-- | x testLeq y checks whether x is less than or
-- equal to y.
testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testStrictLeq :: forall m n. m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)
-- | Apply reflexivity to LeqProof
leqRefl :: forall f n. f n -> LeqProof n n
leqSucc :: forall f z. f z -> LeqProof z (z + 1)
-- | Apply transitivity to LeqProof
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
-- | Zero is less than or equal to any Nat.
leqZero :: LeqProof 0 n
-- | Add both sides of two inequalities
leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
-- | Subtract sides of two inequalities.
leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
-- | Congruence rule for multiplication
leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
-- | Create a leqProof using two proxies
leqProof :: m <= n => f m -> g n -> LeqProof m n
withLeqProof :: LeqProof m n -> (m <= n => a) -> a
-- | Test whether natural number is positive.
isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)
-- | 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)
-- | 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
-- | Multiplying two positive numbers results in a positive number.
leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)
leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
addIsLeq :: f n -> g m -> LeqProof n (n + m)
withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a
addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)
withAddPrefixLeq :: NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a
addIsLeqLeft1 :: forall n n' m. LeqProof (n + n') m -> LeqProof n m
dblPosIsPos :: forall n. LeqProof 1 n -> LeqProof 1 (n + n)
leqMulMono :: 1 <= x => p x -> q y -> LeqProof y (x * y)
-- | Produce evidence that + is commutative.
plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m)
-- | Produce evidence that + is associative.
plusAssoc :: forall f m g n h o. f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
-- | Produce evidence that * is commutative.
mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
-- | Cancel an add followed by a subtract
plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m
minusPlusCancel :: forall f m g n. n <= m => f m -> g n -> ((m - n) + n) :~: m
addMulDistribRight :: forall n m p f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)
withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a
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
mulCancelR :: (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2
mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)
-- | Used in Vector
lemmaMul :: 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
-- | Addition of type-level naturals.
type family (a :: Natural) + (b :: Natural) :: Natural
infixl 6 +
-- | Subtraction of type-level naturals.
type family (a :: Natural) - (b :: Natural) :: Natural
infixl 6 -
-- | Multiplication of type-level naturals.
type family (a :: Natural) * (b :: Natural) :: Natural
infixl 7 *
-- | Comparison (<=) of comparable types, as a constraint.
type (x :: t) <= (y :: t) = Assert x <=? y LeErrMsg x y :: Constraint
infix 4 <=
-- | This class contains types where you can learn the equality of two
-- types from information contained in terms.
--
-- The result should be Just Refl if and only if the types
-- applied to f are equal:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
--
--
-- Typically, only singleton types should inhabit this class. In that
-- case type argument equality coincides with term equality:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
--
--
--
-- isJust (testEquality x y) = x == y
--
--
-- Singleton types are not required, however, and so the latter two
-- would-be laws are not in fact valid in general.
class () => TestEquality (f :: k -> Type)
-- | Conditionally prove the equality of a and b.
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data () => (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
data Some (f :: k -> Type)
-- | Fin n is a finite type with exactly n
-- elements. Essentially, they bundle a NatRepr that has an
-- existentially-quantified type parameter with a proof that its
-- parameter is less than some fixed natural.
--
-- They are useful in combination with types of a fixed size. For example
-- Fin is used as the index in the FunctorWithIndex
-- instance for Vector. As another example, a Map (Fin
-- n) a is a Map that naturally has a fixed size bound of
-- n.
module Data.Parameterized.Fin
-- | The type Fin n has exactly n inhabitants.
data Fin n
mkFin :: forall i n. (i + 1) <= n => NatRepr i -> Fin n
buildFin :: forall m. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)) -> Fin (m + 1)
-- | Count all of the numbers up to m that meet some condition.
countFin :: NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Bool) -> Fin (m + 1)
viewFin :: (forall i. (i + 1) <= n => NatRepr i -> r) -> Fin n -> r
finToNat :: Fin n -> Natural
embed :: forall n m. n <= m => Fin n -> Fin m
tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
-- | The smallest element of Fin n
minFin :: 1 <= n => Fin n
incFin :: forall n. Fin n -> Fin (n + 1)
fin0Void :: Iso' (Fin 0) Void
fin1Unit :: Iso' (Fin 1) ()
fin2Bool :: Iso' (Fin 2) Bool
instance GHC.Classes.Eq (Data.Parameterized.Fin.Fin n)
instance GHC.Classes.Ord (Data.Parameterized.Fin.Fin n)
instance (1 Data.Type.Ord.<= n, GHC.TypeNats.KnownNat n) => GHC.Enum.Bounded (Data.Parameterized.Fin.Fin n)
instance GHC.Show.Show (Data.Parameterized.Fin.Fin n)
-- | This module provides a ST-based hashtable for parameterized
-- keys and values.
--
-- NOTE: This API makes use of unsafeCoerce to implement the
-- parameterized hashtable abstraction. This should be type-safe provided
-- that the TestEquality instance on the key type is implemented
-- soundly.
module Data.Parameterized.HashTable
-- | A hash table mapping nonces to values.
data HashTable s (key :: k -> Type) (val :: k -> Type)
-- | Create a new empty table.
new :: ST s (HashTable s key val)
-- | Create a new empty table to hold n elements.
newSized :: Int -> ST s (HashTable s k v)
-- | Create a hash table that is a copy of the current one.
clone :: (HashableF key, TestEquality key) => HashTable s key val -> ST s (HashTable s key val)
-- | Lookup value of key in table.
lookup :: (HashableF key, TestEquality key) => HashTable s key val -> key tp -> ST s (Maybe (val tp))
-- | Insert new key and value mapping into table.
insert :: (HashableF key, TestEquality key) => HashTable s (key :: k -> Type) (val :: k -> Type) -> key tp -> val tp -> ST s ()
-- | Return true if the key is in the hash table.
member :: (HashableF key, TestEquality key) => HashTable s (key :: k -> Type) (val :: k -> Type) -> key (tp :: k) -> ST s Bool
-- | Delete an element from the hash table.
delete :: (HashableF key, TestEquality key) => HashTable s (key :: k -> Type) (val :: k -> Type) -> key (tp :: k) -> ST s ()
clear :: (HashableF key, TestEquality key) => HashTable s (key :: k -> Type) (val :: k -> Type) -> ST s ()
-- | A parameterized type that is hashable on all instances.
class HashableF (f :: k -> Type)
hashWithSaltF :: HashableF f => Int -> f tp -> Int
-- | Hash with default salt.
hashF :: HashableF f => f tp -> Int
-- | RealWorld is deeply magical. It is primitive, but it is
-- not unlifted (hence ptrArg). We never manipulate
-- values of type RealWorld; it's only used in the type system, to
-- parameterise State#.
data RealWorld
-- | This module declares classes for working with types with the kind
-- (k -> *) -> * for any kind k.
--
-- These classes generally require type-level evidence for operations on
-- their subterms, but don't actually provide it themselves (because
-- their types are not themselves parameterized, unlike those in
-- Data.Parameterized.TraversableFC).
--
-- Note that there is still some ambiguity around naming conventions, see
-- issue 23.
module Data.Parameterized.ClassesC
class TestEqualityC (t :: (k -> Type) -> Type)
testEqualityC :: TestEqualityC t => (forall x y. f x -> f y -> Maybe (x :~: y)) -> t f -> t f -> Bool
class TestEqualityC t => OrdC (t :: (k -> Type) -> Type)
compareC :: OrdC t => (forall x y. f x -> g y -> OrderingF x y) -> t f -> t g -> Ordering
instance Data.Parameterized.ClassesC.OrdC Data.Parameterized.Some.Some
instance Data.Parameterized.ClassesC.TestEqualityC Data.Parameterized.Some.Some
module Data.Parameterized.BoolRepr
-- | A Boolean flag
data BoolRepr (b :: Bool)
[FalseRepr] :: BoolRepr 'False
[TrueRepr] :: BoolRepr 'True
-- | conditional
ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
-- | negation
notRepr :: BoolRepr b -> BoolRepr (Not b)
-- | Conjunction
(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
infixr 3 %&&
-- | Disjunction
(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
infixr 2 %||
type KnownBool = KnownRepr BoolRepr
someBool :: Bool -> Some BoolRepr
-- | This class contains types where you can learn the equality of two
-- types from information contained in terms.
--
-- The result should be Just Refl if and only if the types
-- applied to f are equal:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
--
--
-- Typically, only singleton types should inhabit this class. In that
-- case type argument equality coincides with term equality:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
--
--
--
-- isJust (testEquality x y) = x == y
--
--
-- Singleton types are not required, however, and so the latter two
-- would-be laws are not in fact valid in general.
class () => TestEquality (f :: k -> Type)
-- | Conditionally prove the equality of a and b.
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data () => (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
data Some (f :: k -> Type)
instance Data.Hashable.Class.Hashable (Data.Parameterized.BoolRepr.BoolRepr n)
instance GHC.Classes.Eq (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Type.Equality.TestEquality Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.PolyEq (Data.Parameterized.BoolRepr.BoolRepr m) (Data.Parameterized.BoolRepr.BoolRepr n)
instance GHC.Show.Show (Data.Parameterized.BoolRepr.BoolRepr m)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.HashableF Data.Parameterized.BoolRepr.BoolRepr
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.True
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.BoolRepr.BoolRepr 'GHC.Types.False
-- | This module defines a 2-tuple where both elements are parameterized
-- over the same existentially quantified parameter.
module Data.Parameterized.Pair
-- | Like a 2-tuple, but with an existentially quantified parameter that
-- both of the elements share.
data Pair (a :: k -> Type) (b :: k -> Type)
[Pair] :: !a tp -> !b tp -> Pair a b
-- | Extract the first element of a pair.
fstPair :: Pair a b -> Some a
-- | Extract the second element of a pair.
sndPair :: Pair a b -> Some b
-- | Project out of Pair.
viewPair :: (forall tp. a tp -> b tp -> c) -> Pair a b -> c
instance forall k (a :: k -> *) (b :: k -> *). (Data.Type.Equality.TestEquality a, Data.Parameterized.Classes.EqF b) => GHC.Classes.Eq (Data.Parameterized.Pair.Pair a b)
instance forall k (a :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Pair.Pair a)
instance forall k (a :: k -> *). Data.Parameterized.TraversableF.FoldableF (Data.Parameterized.Pair.Pair a)
-- | This module provides All, a GADT that encodes universal
-- quantification/parametricity over a type variable.
--
-- The following is an example of a situation in which it might be
-- necessary to use All (though it is a bit contrived):
--
--
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE GADTs #-}
--
-- data F (x :: Bool) where
-- FTrue :: F 'True
-- FFalse :: F 'False
-- FIndeterminate :: F b
--
-- data Value =
-- VAllF (All F)
--
-- class Valuable a where
-- valuation :: a -> Value
--
-- instance Valuable (All F) where
-- valuation = VAllF
--
-- val1 :: Value
-- val1 = valuation (All FIndeterminate)
--
--
-- For a less contrived but more complex example, see this blog post:
-- http://comonad.com/reader/2008/rotten-bananas/
module Data.Parameterized.All
newtype All (f :: k -> Type)
All :: (forall x. f x) -> All (f :: k -> Type)
[getAll] :: All (f :: k -> Type) -> forall x. f x
allConst :: a -> All (Const a)
instance Data.Parameterized.TraversableF.FunctorF Data.Parameterized.All.All
instance Data.Parameterized.TraversableF.FoldableF Data.Parameterized.All.All
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.All.All f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.EqF f => GHC.Classes.Eq (Data.Parameterized.All.All f)
module Data.Parameterized
-- | As in the package indexed-traversable.
module Data.Parameterized.TraversableFC.WithIndex
class FunctorFC t => FunctorFCWithIndex (t :: (k -> Type) -> l -> Type)
-- | Like fmapFC, but with an index.
--
--
-- fmapFC f ≡ imapFC (const f)
--
imapFC :: forall f g z. FunctorFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
class (FoldableFC t, FunctorFCWithIndex t) => FoldableFCWithIndex (t :: (k -> Type) -> l -> Type)
-- | Like foldMapFC, but with an index.
--
--
-- foldMapFC f ≡ ifoldMapFC (const f)
--
ifoldMapFC :: forall f m z. (FoldableFCWithIndex t, Monoid m) => (forall x. IndexF (t f z) x -> f x -> m) -> t f z -> m
-- | Like foldrFC, but with an index.
ifoldrFC :: forall z f b. FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> b -> b) -> b -> t f z -> b
-- | Like foldlFC, but with an index.
ifoldlFC :: forall f b z. FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> b -> f x -> b) -> b -> t f z -> b
-- | Like ifoldrFC, but with an index.
ifoldrFC' :: forall f b z. FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> b -> b) -> b -> t f z -> b
-- | Like ifoldlFC, but with an index.
ifoldlFC' :: forall f b. FoldableFCWithIndex t => (forall x. b -> f x -> b) -> forall x. b -> t f x -> b
-- | Convert structure to list.
itoListFC :: forall f a z. FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> a) -> t f z -> [a]
-- | Like foldlMFC, but with an index.
ifoldlMFC :: FoldableFCWithIndex t => Monad m => (forall x. IndexF (t f z) x -> b -> f x -> m b) -> b -> t f z -> m b
-- | Like foldrMFC, but with an index.
ifoldrMFC :: FoldableFCWithIndex t => Monad m => (forall x. IndexF (t f z) x -> f x -> b -> m b) -> b -> t f z -> m b
-- | Like allFC, but with an index.
iallFC :: FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> Bool) -> t f z -> Bool
-- | Like anyFC, but with an index.
ianyFC :: FoldableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> Bool) -> t f z -> Bool
class (TraversableFC t, FoldableFCWithIndex t) => TraversableFCWithIndex (t :: (k -> Type) -> l -> Type)
-- | Like traverseFC, but with an index.
--
--
-- traverseFC f ≡ itraverseFC (const f)
--
itraverseFC :: forall m z f g. (TraversableFCWithIndex t, Applicative m) => (forall x. IndexF (t f z) x -> f x -> m (g x)) -> t f z -> m (t g z)
imapFCDefault :: forall t f g z. TraversableFCWithIndex t => (forall x. IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
ifoldMapFCDefault :: forall t m z f. TraversableFCWithIndex t => Monoid m => (forall x. IndexF (t f z) x -> f x -> m) -> t f z -> m
-- | This module defines a list over two parameters. The first is a fixed
-- type-level function k -> * for some kind k, and
-- the second is a list of types with kind k that provide the
-- indices for the values in the list.
--
-- This type is closely related to the Assignment type in
-- Data.Parameterized.Context.
--
-- Motivating example - the List type
--
-- For this example, we need the following extensions:
--
--
-- {-# LANGUAGE DataKinds #-}
-- {-# LANGUAGE GADTs #-}
-- {-# LANGUAGE KindSignatures #-}
-- {-# LANGUAGE TypeOperators #-}
--
--
-- We also require the following imports:
--
--
-- import Data.Parameterized
-- import Data.Parameterized.List
-- import GHC.TypeLits
--
--
-- Suppose we have a bitvector type:
--
--
-- data BitVector (w :: Nat) :: * where
-- BV :: NatRepr w -> Integer -> BitVector w
--
--
-- This type contains a NatRepr, a value-level representative of
-- the vector width, and an Integer, containing the actual value
-- of the bitvector. We can create values of this type as follows:
--
--
-- BV (knownNat @8) 0xAB
--
--
-- We can also create a smart constructor to handle the NatRepr
-- automatically, when the width is known from the type context:
--
--
-- bitVector :: KnownNat w => Integer -> BitVector w
-- bitVector x = BV knownNat x
--
--
-- Note that this does not check that the value can be represented in the
-- given number of bits; that is not important for this example.
--
-- If we wish to construct a list of BitVectors of a particular
-- length, we can do:
--
--
-- [bitVector 0xAB, bitVector 0xFF, bitVector 0] :: BitVector 8
--
--
-- However, what if we wish to construct a list of BitVectors of
-- different lengths? We could try:
--
--
-- [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
--
--
-- However, this gives us an error:
--
--
-- <interactive>:3:33: error:
-- • Couldn't match type ‘16’ with ‘8’
-- Expected type: BitVector 8
-- Actual type: BitVector 16
-- • In the expression: bitVector 0x1234 :: BitVector 16
-- In the expression:
-- [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
-- In an equation for ‘it’:
-- it
-- = [bitVector 0xAB :: BitVector 8, bitVector 0x1234 :: BitVector 16]
--
--
-- A vanilla Haskell list cannot contain two elements of different types,
-- and even though the two elements here are both BitVectors,
-- they do not have the same type! One solution is to use the Some
-- type:
--
--
-- [Some (bitVector 0xAB :: BitVector 8), Some (bitVector 0x1234 :: BitVector 16)]
--
--
-- The type of the above expression is [Some BitVector], which
-- may be perfectly acceptable. However, there is nothing in this type
-- that tells us what the widths of the bitvectors are, or what the
-- length of the overall list is. If we want to actually track that
-- information on the type level, we can use the List type from
-- this module.
--
--
-- (bitVector 0xAB :: BitVector 8) :< (bitVector 0x1234 :: BitVector 16) :< Nil
--
--
-- The type of the above expression is List BitVector '[8, 16]
-- -- That is, a two-element list of BitVectors, where the first
-- element has width 8 and the second has width 16.
--
-- Summary
--
-- In general, if we have a type constructor Foo of kind k
-- -> * (in our example, Foo is just BitVector,
-- and we want to create a list of Foos where the parameter
-- k varies, and we wish to keep track of what each value
-- of k is inside the list at compile time, we can use the
-- List type for this purpose.
module Data.Parameterized.List
-- | Parameterized list of elements.
data List :: (k -> Type) -> [k] -> Type
[Nil] :: List f '[]
[:<] :: f tp -> List f tps -> List f (tp : tps)
infixr 5 :<
-- | Map from list of Some to Some list
fromSomeList :: [Some f] -> Some (List f)
-- | Apply function to list to yield a parameterized list.
fromListWith :: forall a f. (a -> Some f) -> [a] -> Some (List f)
-- | Apply monadic action to list to yield a parameterized list.
fromListWithM :: forall a f m. Monad m => (a -> m (Some f)) -> [a] -> m (Some (List f))
-- | Represents an index into a type-level list. Used in place of integers
-- to 1. ensure that the given index *does* exist in the list 2.
-- guarantee that it has the given kind
data Index :: [k] -> k -> Type
[IndexHere] :: Index (x : r) x
[IndexThere] :: !Index r y -> Index (x : r) y
-- | Return the index as an integer.
indexValue :: Index l tp -> Integer
-- | Return the value in a list at a given index
(!!) :: List f l -> Index l x -> f x
-- | Update the List at an index
update :: List f l -> Index l s -> (f s -> f s) -> List f l
-- | Provides a lens for manipulating the element at the given index.
indexed :: Index l x -> Lens' (List f l) (f x)
-- | Map over the elements in the list, and provide the index into each
-- element along with the element itself.
--
-- This is a specialization of imapFC.
imap :: forall f g l. (forall x. Index l x -> f x -> g x) -> List f l -> List g l
-- | Left fold with an additional index.
ifoldlM :: forall sh a b m. Monad m => (forall tp. b -> Index sh tp -> a tp -> m b) -> b -> List a sh -> m b
-- | Right-fold with an additional index.
--
-- This is a specialization of ifoldrFC.
ifoldr :: forall sh a b. (forall tp. Index sh tp -> a tp -> b -> b) -> b -> List a sh -> 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
-- | Traverse with an additional index.
--
-- This is a specialization of itraverseFC.
itraverse :: forall a b sh t. Applicative t => (forall tp. Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh)
-- | Index 0
index0 :: Index (x : r) x
-- | Index 1
index1 :: Index (x0 : (x1 : r)) x1
-- | Index 2
index2 :: Index (x0 : (x1 : (x2 : r))) x2
-- | Index 3
index3 :: Index (x0 : (x1 : (x2 : (x3 : r)))) x3
instance forall k (l :: [k]) (x :: k). GHC.Classes.Eq (Data.Parameterized.List.Index l x)
instance forall k (l :: [k]) (x :: k). GHC.Show.Show (Data.Parameterized.List.Index l x)
instance forall k (l :: [k]). Data.Parameterized.Classes.ShowF (Data.Parameterized.List.Index l)
instance forall k (l :: [k]). Data.Type.Equality.TestEquality (Data.Parameterized.List.Index l)
instance forall k (l :: [k]). Data.Parameterized.Classes.OrdF (Data.Parameterized.List.Index l)
instance forall k (sh :: [k]) (x :: k). GHC.Classes.Ord (Data.Parameterized.List.Index sh x)
instance forall k (l :: [k]) (x :: k). Data.Hashable.Class.Hashable (Data.Parameterized.List.Index l x)
instance forall k (f :: k -> *) (sh :: [k]). Data.Parameterized.Classes.ShowF f => GHC.Show.Show (Data.Parameterized.List.List f sh)
instance forall k (f :: k -> *). Data.Parameterized.Classes.ShowF f => Data.Parameterized.Classes.ShowF (Data.Parameterized.List.List f)
instance Data.Parameterized.TraversableFC.FunctorFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.FoldableFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.TraversableFC Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.WithIndex.FunctorFCWithIndex Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.WithIndex.FoldableFCWithIndex Data.Parameterized.List.List
instance Data.Parameterized.TraversableFC.WithIndex.TraversableFCWithIndex Data.Parameterized.List.List
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.OrdF f => Data.Parameterized.Classes.OrdF (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) '[]
instance forall a (f :: a -> *) (s :: a) (sh :: [a]). (Data.Parameterized.Classes.KnownRepr f s, Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) sh) => Data.Parameterized.Classes.KnownRepr (Data.Parameterized.List.List f) (s : sh)
-- | This module reexports either Data.Parameterized.Context.Safe or
-- Data.Parameterized.Context.Unsafe depending on the the
-- unsafe-operations compile-time flag.
--
-- It also defines some utility typeclasses for transforming between
-- curried and uncurried versions of functions over contexts.
--
-- The Assignment type is isomorphic to the List type,
-- except Assignments construct lists from the right-hand side,
-- and instead of using type-level '[]-style lists, an
-- Assignment is indexed by a type-level Ctx. The
-- implementation of Assignments is also more efficent than
-- List for lists of many elements, as it uses a balanced binary
-- tree representation rather than a linear-time list. For a motivating
-- example, see List.
module Data.Parameterized.Context
-- | A context that can be determined statically at compiler time.
class KnownContext (ctx :: Ctx k)
knownSize :: KnownContext ctx => Size ctx
-- | Represents the size of a context.
data Size (ctx :: Ctx k)
-- | Convert a context size to an Int.
sizeInt :: Size ctx -> Int
-- | The size of an empty context.
zeroSize :: Size 'EmptyCtx
-- | Increment the size to the next value.
incSize :: Size ctx -> Size (ctx '::> tp)
decSize :: Size (ctx '::> tp) -> Size ctx
-- | Extend the size by a given difference.
extSize :: Size l -> Diff l r -> Size r
-- | The total size of two concatenated contexts.
addSize :: Size x -> Size y -> Size (x <+> y)
-- | Allows interpreting a size.
data SizeView (ctx :: Ctx k)
[ZeroSize] :: SizeView 'EmptyCtx
[IncSize] :: !Size ctx -> SizeView (ctx '::> tp)
-- | Project a size
viewSize :: Size ctx -> SizeView ctx
-- | Convert a Size into a NatRepr.
sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
-- | Difference in number of elements between two contexts. The first
-- context must be a sub-context of the other.
data Diff (l :: Ctx k) (r :: Ctx k)
-- | The identity difference. Identity element of Category
-- instance.
noDiff :: Diff l l
-- | The addition of differences. Flipped binary operation of
-- Category instance.
addDiff :: Diff a b -> Diff b c -> Diff a c
-- | Extend the difference to a sub-context of the right side.
extendRight :: Diff l r -> Diff l (r '::> tp)
appendDiff :: Size r -> Diff l (l <+> r)
data DiffView a b
[NoDiff] :: DiffView a a
[ExtendRightDiff] :: Diff a b -> DiffView a (b ::> r)
viewDiff :: Diff a b -> DiffView a b
-- | A difference that can be automatically inferred at compile time.
class KnownDiff (l :: Ctx k) (r :: Ctx k)
knownDiff :: KnownDiff l r => Diff l r
-- | Proof that r = l + app for some app
data IsAppend l r
[IsAppend] :: Size app -> IsAppend l (l <+> app)
-- | If l is a sub-context of r then extract out their
-- "contextual difference", i.e., the app such that r = l
-- + app
diffIsAppend :: Diff l r -> IsAppend l r
-- | An index is a reference to a position with a particular type in a
-- context.
data Index (ctx :: Ctx k) (tp :: k)
indexVal :: Index ctx tp -> Int
-- | Index for first element in context.
baseIndex :: Index ('EmptyCtx '::> tp) tp
-- | Increase context while staying at same index.
skipIndex :: Index ctx x -> Index (ctx '::> y) x
-- | Return the last index of a element.
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
-- | Return the index of a element one past the size.
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
-- | Adapts an index in the left hand context of an append operation.
leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp
-- | Adapts an index in the right hand context of an append operation.
rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
-- | Compute an Index into a context r from an Index
-- into a sub-context l of r.
extendIndex' :: Diff l r -> Index l tp -> Index r tp
-- | Compute an Index into an appended context from an Index
-- into its suffix.
extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
-- | Given a size n, a function f, and an initial value
-- v0, the expression forIndex n f v0 is equivalent to
-- v0 when n is zero, and f (forIndex (n-1) f v0)
-- n otherwise. Unlike the safe version, which starts from
-- Index 0 and increments Index values, this
-- version starts at Index (n-1) and decrements
-- Index values to Index 0.
forIndex :: forall ctx r. Size ctx -> (forall tp. r -> Index ctx tp -> r) -> r -> r
-- | Given an index i, size n, a function f, and
-- a value v, the expression forIndex i n f v is
-- equivalent to v when i >= sizeInt n, and f i
-- (forIndexRange (i+1) n f v) otherwise.
forIndexRange :: forall ctx r. Int -> Size ctx -> (forall tp. Index ctx tp -> r -> r) -> r -> r
-- | Return index at given integer or nothing if integer is out of bounds.
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
-- | View of indexes as pointing to the last element in the index range or
-- pointing to an earlier element in a smaller range.
data IndexView ctx tp
[IndexViewLast] :: !Size ctx -> IndexView (ctx '::> t) t
[IndexViewInit] :: !Index ctx t -> IndexView (ctx '::> u) t
-- | Project an index
viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
-- | This represents a contiguous range of indices.
data IndexRange (ctx :: Ctx k) (sub :: Ctx k)
-- | Return a range containing all indices in the context.
allRange :: Size ctx -> IndexRange ctx ctx
-- | indexOfRange returns the only index in a range.
indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
-- | dropHeadRange r n drops the first n elements in
-- r.
dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
-- | dropTailRange r n drops the last n elements in
-- r.
dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
-- | An assignment is a sequence that maps each index with type tp
-- to a value of type f tp.
--
-- 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.
data Assignment (f :: k -> Type) (ctx :: Ctx k)
-- | Return number of elements in assignment.
size :: Assignment f ctx -> Size ctx
-- | replicate n make a context with different copies of the same
-- polymorphic value.
replicate :: Size ctx -> (forall tp. f tp) -> Assignment f ctx
-- | Generate an assignment
generate :: Size ctx -> (forall tp. Index ctx tp -> f tp) -> Assignment f ctx
-- | Generate an assignment in an Applicative context
generateM :: Applicative m => Size ctx -> (forall tp. Index ctx tp -> m (f tp)) -> m (Assignment f ctx)
-- | Return empty assignment
empty :: Assignment f EmptyCtx
-- | Extend an indexed vector with a new entry.
extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
-- | Deprecated: 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
-- | Deprecated: 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
-- | 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)
-- | Represent an assignment as either empty or an assignment with one
-- appended.
data AssignView f ctx
[AssignEmpty] :: AssignView f EmptyCtx
[AssignExtend] :: Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
-- | View an assignment as either empty or an assignment with one appended.
viewAssign :: forall f ctx. Assignment f ctx -> AssignView f ctx
-- | Return value of assignment.
(!) :: Assignment f ctx -> Index ctx tp -> f tp
-- | Return value of assignment, where the index is into an initial
-- sequence of the assignment.
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
zipWith :: (forall x. f x -> g x -> h x) -> Assignment f a -> Assignment g a -> Assignment h a
zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Assignment f a -> Assignment g a -> m (Assignment h a)
(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
traverseWithIndex :: Applicative m => (forall tp. Index ctx tp -> f tp -> m (g tp)) -> Assignment f ctx -> m (Assignment g ctx)
-- | Create a single element context.
singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
-- | Convert the assignment to a vector.
toVector :: Assignment f tps -> (forall tp. f tp -> e) -> Vector e
-- | Pattern synonym for extending an assignment on the right
pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
infixl 9 :>
-- | Pattern synonym for the empty assignment
pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
-- | Return true if assignment is empty.
null :: Assignment f ctx -> Bool
-- | Return assignment with all but the last block.
init :: Assignment f (ctx '::> tp) -> Assignment f ctx
-- | Return the last element in the assignment.
last :: Assignment f (ctx '::> tp) -> f tp
-- | View an assignment as either empty or an assignment with one appended.
-- | Deprecated: Use viewAssign or the Empty and :> patterns
-- instead.
view :: forall f ctx. Assignment f ctx -> AssignView f ctx
-- | Return the prefix of an appended Assignment
take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
-- | Return the suffix of an appended Assignment
drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
-- | '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 ()
-- | Generate an assignment with some context type that is not known.
generateSome :: forall f. Int -> (Int -> Some f) -> Some (Assignment f)
-- | 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))
-- | Create an assignment from a list of values.
fromList :: [Some f] -> Some (Assignment f)
-- | Visit each of the elements in an Assignment in order from
-- left to right and collect the results using the provided
-- Monoid.
traverseAndCollect :: (Monoid w, Applicative m) => (forall tp. Index ctx tp -> f tp -> m w) -> Assignment f ctx -> m w
-- | Visit each of the elements in an Assignment in order from
-- left to right, executing an action with each.
traverseWithIndex_ :: Applicative m => (forall tp. Index ctx tp -> f tp -> m ()) -> Assignment f ctx -> m ()
-- | Utility function for testing if xs is an assignment with
-- prefix as a prefix, and computing the tail of xs not in the
-- prefix, if so.
dropPrefix :: forall f xs prefix a. TestEquality f => Assignment f xs -> Assignment f prefix -> a -> (forall addl. xs ~ (prefix <+> addl) => Assignment f addl -> a) -> a
-- | Unzip an assignment of pairs into a pair of assignments.
--
-- This is the inverse of zipWith Pair.
unzip :: Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)
-- | Flattens a nested assignment over a context of contexts ctxs ::
-- Ctx (Ctx a) into a flat assignment over the flattened context
-- CtxFlatten ctxs.
flattenAssignment :: Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
-- | Given the size of each context in ctxs, returns the size of
-- CtxFlatten ctxs. You can obtain the former from any nested
-- assignment Assignment (Assignment f) ctxs, by calling
-- fmapFC size.
flattenSize :: Assignment Size ctxs -> Size (CtxFlatten ctxs)
-- | This datastructure contains a proof that the first context is
-- embeddable in the second. This is useful if we want to add extend an
-- existing term under a larger context.
data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)
CtxEmbedding :: Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)
[_ctxeSize] :: CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) -> Size ctx'
[_ctxeAssignment] :: CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k) -> Assignment (Index ctx') ctx
class ExtendContext (f :: Ctx k -> Type)
extendContext :: ExtendContext f => Diff ctx ctx' -> f ctx -> f ctx'
class ExtendContext' (f :: Ctx k -> k' -> Type)
extendContext' :: ExtendContext' f => Diff ctx ctx' -> f ctx v -> f ctx' v
class ApplyEmbedding (f :: Ctx k -> Type)
applyEmbedding :: ApplyEmbedding f => CtxEmbedding ctx ctx' -> f ctx -> f ctx'
class ApplyEmbedding' (f :: Ctx k -> k' -> Type)
applyEmbedding' :: ApplyEmbedding' f => CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
extendEmbeddingRightDiff :: forall ctx ctx' ctx''. Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
-- | Prove that the prefix of an appended context is embeddable in it
appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
-- | Prove that the suffix of an appended context is embeddable in it
appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx') (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)
-- | Constraint synonym used for getting an Index into a Ctx.
-- n is the zero-based, left-counted index into the list of
-- types ctx which has the type r.
type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)
-- | 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)
-- | Compute an Index value for a particular position in a
-- Ctx. The TypeApplications extension will be needed to
-- disambiguate the choice of the type n.
natIndex :: forall n ctx r. Idx n ctx r => Index ctx r
-- | This version of natIndex is suitable for use without the
-- TypeApplications extension.
natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r
-- | This type family is used to define currying/uncurrying operations on
-- assignments. It is best understood by seeing its evaluation on several
-- examples:
--
--
-- CurryAssignment EmptyCtx f x = x
-- CurryAssignment (EmptyCtx ::> a) f x = f a -> x
-- CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
-- CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x
--
type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) (x :: Type) :: Type
-- | This class implements two methods that witness the isomorphism between
-- curried and uncurried functions.
class CurryAssignmentClass (ctx :: Ctx k)
-- | Transform a function that accepts an assignment into one with a
-- separate variable for each element of the assignment.
curryAssignment :: CurryAssignmentClass ctx => (Assignment f ctx -> x) -> CurryAssignment ctx f x
-- | Transform a curried function into one that accepts an assignment
-- value.
uncurryAssignment :: CurryAssignmentClass ctx => CurryAssignment ctx f x -> Assignment f ctx -> x
size1 :: Size (EmptyCtx ::> a)
size2 :: Size ((EmptyCtx ::> a) ::> b)
size3 :: Size (((EmptyCtx ::> a) ::> b) ::> c)
size4 :: Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
size5 :: Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size6 :: Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
i1of2 :: Index ((EmptyCtx ::> a) ::> b) a
i2of2 :: Index ((EmptyCtx ::> a) ::> b) b
i1of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) a
i2of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) b
i3of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) c
i1of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
i2of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
i3of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
i4of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
i1of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
i2of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
i3of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
i4of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
i5of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
i1of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i2of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i3of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i4of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i5of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i6of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
instance forall k (m :: k -> *) (w :: k). GHC.Base.Functor (Data.Parameterized.Context.Collector m w)
instance (GHC.Base.Applicative m, GHC.Base.Monoid w) => GHC.Base.Applicative (Data.Parameterized.Context.Collector m w)
instance Data.Parameterized.Context.CurryAssignmentClass Data.Parameterized.Ctx.EmptyCtx
instance forall k (ctx :: Data.Parameterized.Ctx.Ctx k) (a :: k). Data.Parameterized.Context.CurryAssignmentClass ctx => Data.Parameterized.Context.CurryAssignmentClass (ctx Data.Parameterized.Ctx.::> a)
instance forall k (xs :: Data.Parameterized.Ctx.Ctx k) (x :: k). Data.Parameterized.Context.Unsafe.KnownContext xs => Data.Parameterized.Context.Idx' 0 (xs 'Data.Parameterized.Ctx.::> x) x
instance forall k (xs :: Data.Parameterized.Ctx.Ctx k) (n :: GHC.Num.Natural.Natural) (r :: k) (x :: k). (Data.Parameterized.Context.Unsafe.KnownContext xs, Data.Parameterized.Context.Idx' (n GHC.TypeNats.- 1) xs r) => Data.Parameterized.Context.Idx' n (xs 'Data.Parameterized.Ctx.::> x) r
instance Data.Parameterized.Context.ExtendContext' Data.Parameterized.Context.Unsafe.Index
instance Data.Parameterized.Context.ApplyEmbedding' Data.Parameterized.Context.Unsafe.Index
-- | This defines a type Peano and PeanoRepr for representing
-- a type-level natural at runtime. These type-level numbers are defined
-- inductively instead of using GHC.TypeLits.
--
-- As a result, type-level computation defined recursively over these
-- numbers works more smoothly. (For example, see the type-level function
-- Repeat below.)
--
-- Note: as in NatRepr, in UNSAFE mode, the runtime representation
-- of these type-level natural numbers is Word64.
module Data.Parameterized.Peano
-- | Unary representation for natural numbers
data Peano
-- | Peano zero
type Z = 'Z
-- | Peano successor
type S = 'S
-- | Addition
type family Plus (a :: Peano) (b :: Peano) :: Peano
-- | Subtraction
type family Minus (a :: Peano) (b :: Peano) :: Peano
-- | Multiplication
type family Mul (a :: Peano) (b :: Peano) :: Peano
-- | Maximum
type family Max (a :: Peano) (b :: Peano) :: Peano
-- | Minimum
type family Min (a :: Peano) (b :: Peano) :: Peano
-- | Addition
plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
-- | Subtraction
minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
-- | Multiplication
mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
-- | Maximum
maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
-- | Minimum
minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
-- | Zero
zeroP :: PeanoRepr Z
-- | Successor, Increment
succP :: PeanoRepr n -> PeanoRepr (S n)
-- | Get the predecessor (decrement)
predP :: PeanoRepr (S n) -> PeanoRepr n
-- | Apply a constructor f n-times to an argument s
type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k
-- | Calculate the size of a context
type family CtxSizeP (ctx :: Ctx k) :: Peano
-- | Apply a constructor f n-times to an argument s
repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
-- | Calculate the size of a context
ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
-- | Less-than-or-equal
type family Le (a :: Peano) (b :: Peano) :: Bool
-- | Less-than
type family Lt (a :: Peano) (b :: Peano) :: Bool
-- | Greater-than
type family Gt (a :: Peano) (b :: Peano) :: Bool
-- | Greater-than-or-equal
type family Ge (a :: Peano) (b :: Peano) :: Bool
-- | Less-than-or-equal-to
leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
-- | Less-than
ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
-- | Greater-than
gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
-- | Greater-than-or-equal-to
geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
-- | Implicit runtime representation
type KnownPeano = KnownRepr PeanoRepr
-- | The run time value, stored as an Word64 As these are unary numbers, we
-- don't worry about overflow.
data PeanoRepr (n :: Peano)
-- | When we have optimized the runtime representation, we need to have a
-- "view" that decomposes the representation into the standard form.
data PeanoView (n :: Peano)
[ZRepr] :: PeanoView Z
[SRepr] :: PeanoRepr n -> PeanoView (S n)
-- | Test whether a number is Zero or Successor
peanoView :: PeanoRepr n -> PeanoView n
-- | convert the view back to the runtime representation
viewRepr :: PeanoView n -> PeanoRepr n
-- | Convert a Word64 to a PeanoRepr
mkPeanoRepr :: Word64 -> Some PeanoRepr
peanoValue :: PeanoRepr n -> Word64
-- | Turn an Integral value into a PeanoRepr. Returns
-- Nothing if the given value is negative.
somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
-- | Return the maximum of two representations.
maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
-- | Return the minimum of two representations.
minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
-- | List length as a Peano number
peanoLength :: [a] -> Some PeanoRepr
-- | Context size commutes with context append
plusCtxSizeAxiom :: forall t1 t2 f. Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
-- | Minus distributes over plus
minusPlusAxiom :: forall n t t'. PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t
-- | We can reshuffle minus with less than
ltMinusPlusAxiom :: forall n t t'. Lt t (Minus n t') ~ 'True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: 'True
-- | This class contains types where you can learn the equality of two
-- types from information contained in terms.
--
-- The result should be Just Refl if and only if the types
-- applied to f are equal:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
--
--
-- Typically, only singleton types should inhabit this class. In that
-- case type argument equality coincides with term equality:
--
--
-- testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
--
--
--
-- isJust (testEquality x y) = x == y
--
--
-- Singleton types are not required, however, and so the latter two
-- would-be laws are not in fact valid in general.
class () => TestEquality (f :: k -> Type)
-- | Conditionally prove the equality of a and b.
testEquality :: forall (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b)
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data () => (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
data Some (f :: k -> Type)
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr Data.Parameterized.Peano.Z
instance Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr n => Data.Parameterized.Classes.KnownRepr Data.Parameterized.Peano.PeanoRepr (Data.Parameterized.Peano.S n)
instance Data.Hashable.Class.Hashable (Data.Parameterized.Peano.PeanoRepr n)
instance GHC.Classes.Eq (Data.Parameterized.Peano.PeanoRepr m)
instance Data.Type.Equality.TestEquality Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.DecidableEq.DecidableEq Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.OrdF Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.PolyEq (Data.Parameterized.Peano.PeanoRepr m) (Data.Parameterized.Peano.PeanoRepr n)
instance GHC.Show.Show (Data.Parameterized.Peano.PeanoRepr p)
instance Data.Parameterized.Classes.ShowF Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.Classes.HashableF Data.Parameterized.Peano.PeanoRepr
module Data.Parameterized.Utils.BinTree
-- | A strict version of Maybe
data MaybeS v
JustS :: !v -> MaybeS v
NothingS :: MaybeS v
fromMaybeS :: a -> MaybeS a -> a
-- | Updated a contains a value that has been flagged on whether
-- it was modified by an operation.
data Updated a
Updated :: !a -> Updated a
Unchanged :: !a -> Updated a
updatedValue :: Updated a -> a
data TreeApp e t
BinTree :: !e -> !t -> !t -> TreeApp e t
TipTree :: TreeApp e t
class IsBinTree t e | t -> e
asBin :: IsBinTree t e => t -> TreeApp e t
tip :: IsBinTree t e => t
bin :: IsBinTree t e => e -> t -> t -> t
size :: IsBinTree t e => t -> Int
-- | balanceL p l r returns a balanced tree for the sequence l
-- ++ [p] ++ r.
--
-- It assumes that l and r are close to being balanced,
-- and that only l may contain too many elements.
balanceL :: IsBinTree c e => e -> c -> c -> c
-- | balanceR p l r returns a balanced tree for the sequence l
-- ++ [p] ++ r.
--
-- It assumes that l and r are close to being balanced,
-- and that only r may contain too many elements.
balanceR :: IsBinTree c e => e -> c -> c -> c
-- | glue l r concatenates l and r.
--
-- It assumes that l and r are already balanced with
-- respect to each other.
glue :: IsBinTree c e => c -> c -> c
-- | Concatenate two trees that are ordered with respect to each other.
merge :: IsBinTree c e => c -> c -> c
-- | Returns only entries that are less than predicate with respect to the
-- ordering and Nothing if no elements are discarded.
filterGt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
-- | filterLt k m returns submap of m that only contains
-- entries that are smaller than k. If no entries are deleted
-- then return Nothing.
filterLt :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
-- | insert p m inserts the binding into m. It returns an
-- Unchanged value if the map stays the same size and an updated value if
-- a new entry was inserted.
insert :: IsBinTree c e => (e -> e -> Ordering) -> e -> c -> Updated c
delete :: IsBinTree c e => (e -> Ordering) -> c -> MaybeS c
-- | Union two sets
union :: IsBinTree c e => (e -> e -> Ordering) -> c -> c -> c
-- | link is called to insert a key and value between two disjoint
-- subtrees.
link :: IsBinTree c e => e -> c -> c -> c
-- | A Strict pair
data PairS f s
PairS :: !f -> !s -> PairS f s
instance GHC.Base.Functor Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Base.Alternative Data.Parameterized.Utils.BinTree.MaybeS
instance GHC.Base.Applicative Data.Parameterized.Utils.BinTree.MaybeS
-- | This module defines finite maps where the key and value types are
-- parameterized by an arbitrary kind.
--
-- Some code was adapted from containers.
module Data.Parameterized.Map
-- | A map from parameterized keys to values with the same parameter type.
data MapF (k :: v -> Type) (a :: v -> Type)
-- | Return empty map
empty :: MapF k a
-- | Return map containing a single element
singleton :: k tp -> a tp -> MapF k a
-- | Insert a binding into the map, replacing the existing binding if
-- needed.
insert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a
-- | insertWith f new m inserts the binding into m.
--
-- It inserts f new old if m already contains an
-- equivalent value old, and new otherwise. It returns
-- an Unchanged value if the map stays the same size and an
-- Updated value if a new entry was inserted.
insertWith :: OrdF k => (a tp -> a tp -> a tp) -> k tp -> a tp -> MapF k a -> MapF k a
-- | Delete a value from the map if present.
delete :: OrdF k => k tp -> MapF k a -> MapF k a
-- | Left-biased union of two maps. The resulting map will contain the
-- union of the keys of the two arguments. When a key is contained in
-- both maps the value from the first map will be preserved.
union :: OrdF k => MapF k a -> MapF k a -> MapF k a
-- | Applies a function to the pairwise common elements of two maps.
--
-- Formally, we have that intersectWithKeyMaybe f x y contains a
-- binding from a key k to a value v if and only if
-- x and y bind k to x_k and
-- y_k and f x_k y_k = Just v.
intersectWithKeyMaybe :: OrdF k => (forall tp. k tp -> a tp -> b tp -> Maybe (c tp)) -> MapF k a -> MapF k b -> MapF k c
-- | Return true if map is empty
null :: MapF k a -> Bool
-- | Lookup value in map.
lookup :: OrdF k => k tp -> MapF k a -> Maybe (a tp)
-- | findWithDefault d k m returns the value bound to k
-- in the map m, or d if k is not bound in the
-- map.
findWithDefault :: OrdF k => a tp -> k tp -> MapF k a -> a tp
-- | Return true if key is bound in map.
member :: OrdF k => k tp -> MapF k a -> Bool
-- | Return true if key is not bound in map.
notMember :: OrdF k => k tp -> MapF k a -> Bool
size :: IsBinTree t e => t -> Int
-- | Return all keys of the map in ascending order.
keys :: MapF k a -> [Some k]
-- | Return all elements of the map in the ascending order of their keys.
elems :: MapF k a -> [Some a]
-- | Create a Map from a list of pairs.
fromList :: OrdF k => [Pair k a] -> MapF k a
-- | Return list of key-values pairs in map.
toList :: MapF k a -> [Pair k a]
-- | Return list of key-values pairs in map in ascending order.
toAscList :: MapF k a -> [Pair k a]
-- | Return list of key-values pairs in map in descending order.
toDescList :: MapF k a -> [Pair k a]
-- | Generate a map from a foldable collection of keys and a function from
-- keys to values.
fromKeys :: forall k m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type). (Monad m, Foldable t, OrdF a) => (forall tp. a tp -> m (v tp)) -> t (Some a) -> m (MapF a v)
-- | Generate a map from a foldable collection of keys and a monadic
-- function from keys to values.
fromKeysM :: forall k m (t :: Type -> Type) (a :: k -> Type) (v :: k -> Type). (Monad m, Foldable t, OrdF a) => (forall tp. a tp -> m (v tp)) -> t (Some a) -> m (MapF a v)
-- | Return entries with values that satisfy a predicate.
filter :: (forall tp. f tp -> Bool) -> MapF k f -> MapF k f
-- | Return key-value pairs that satisfy a predicate.
filterWithKey :: (forall tp. k tp -> f tp -> Bool) -> MapF k f -> MapF k f
-- | filterGt k m returns submap of m that only contains
-- entries that are larger than k.
filterGt :: OrdF k => k tp -> MapF k v -> MapF k v
-- | filterLt k m returns submap of m that only contains
-- entries that are smaller than k.
filterLt :: OrdF k => k tp -> MapF k v -> MapF k v
-- | Perform a left fold with the key also provided.
foldlWithKey :: (forall s. b -> k s -> a s -> b) -> b -> MapF k a -> b
-- | Perform a strict left fold with the key also provided.
foldlWithKey' :: (forall s. b -> k s -> a s -> b) -> b -> MapF k a -> b
-- | Perform a right fold with the key also provided.
foldrWithKey :: (forall s. k s -> a s -> b -> b) -> b -> MapF k a -> b
-- | Perform a strict right fold with the key also provided.
foldrWithKey' :: (forall s. k s -> a s -> b -> b) -> b -> MapF k a -> b
-- | Fold the keys and values using the given monoid.
foldMapWithKey :: Monoid m => (forall s. k s -> a s -> m) -> MapF k a -> m
-- | A monadic left-to-right fold over keys and values in the map.
foldlMWithKey :: Monad m => (forall s. b -> k s -> a s -> m b) -> b -> MapF k a -> m b
-- | A monadic right-to-left fold over keys and values in the map.
foldrMWithKey :: Monad m => (forall s. k s -> a s -> b -> m b) -> b -> MapF k a -> m b
-- | Modify elements in a map
map :: (forall tp. f tp -> g tp) -> MapF ktp f -> MapF ktp g
-- | Apply function to all elements in map.
mapWithKey :: (forall tp. ktp tp -> f tp -> g tp) -> MapF ktp f -> MapF ktp g
-- | Map elements and collect Just results.
mapMaybe :: (forall tp. f tp -> Maybe (g tp)) -> MapF ktp f -> MapF ktp g
-- | Map keys and elements and collect Just results.
mapMaybeWithKey :: (forall tp. k tp -> f tp -> Maybe (g tp)) -> MapF k f -> MapF k g
-- | Traverse elements in a map
traverseWithKey :: Applicative m => (forall tp. ktp tp -> f tp -> m (g tp)) -> MapF ktp f -> m (MapF ktp g)
-- | Traverse elements in a map without returning result.
traverseWithKey_ :: Applicative m => (forall tp. ktp tp -> f tp -> m ()) -> MapF ktp f -> m ()
-- | Traverse keys/values and collect the Just results.
traverseMaybeWithKey :: Applicative f => (forall tp. k tp -> a tp -> f (Maybe (b tp))) -> MapF k a -> f (MapF k b)
-- | UpdateRequest tells what to do with a found value
data UpdateRequest v
-- | Keep the current value.
Keep :: UpdateRequest v
-- | Set the value to a new value.
Set :: !v -> UpdateRequest v
-- | Delete a value.
Delete :: UpdateRequest v
-- | Updated a contains a value that has been flagged on whether
-- it was modified by an operation.
data Updated a
Updated :: !a -> Updated a
Unchanged :: !a -> Updated a
updatedValue :: Updated a -> a
-- | Log-time algorithm that allows a value at a specific key to be added,
-- replaced, or deleted.
updateAtKey :: (OrdF k, Functor f) => k tp -> f (Maybe (a tp)) -> (a tp -> f (UpdateRequest (a tp))) -> MapF k a -> f (Updated (MapF k a))
-- | Merge bindings in two maps to get a third.
--
-- The first function is used to merge elements that occur under the same
-- key in both maps. Return Just to add an entry into the resulting map
-- under this key or Nothing to remove this key from the resulting map.
--
-- The second function will be applied to submaps of the first map
-- argument where no keys overlap with the second map argument. The
-- result of this function must be a map with a subset of the keys of its
-- argument. This means the function can alter the values of its argument
-- and it can remove key-value pairs from it, but it can break
-- MapF ordering invariants if it introduces new keys.
--
-- Third function is analogous to the second function except that it
-- applies to the second map argument of mergeWithKeyM instead of
-- the first.
--
-- Common examples of the two functions include id when
-- constructing a union or const empty when constructing an
-- intersection.
mergeWithKey :: forall k a b c. OrdF k => (forall tp. k tp -> a tp -> b tp -> Maybe (c tp)) -> (MapF k a -> MapF k c) -> (MapF k b -> MapF k c) -> MapF k a -> MapF k b -> MapF k c
-- | Merge bindings in two maps using monadic actions to get a third.
--
-- The first function is used to merge elements that occur under the same
-- key in both maps. Return Just to add an entry into the resulting map
-- under this key or Nothing to remove this key from the resulting map.
--
-- The second function will be applied to submaps of the first map
-- argument where no keys overlap with the second map argument. The
-- result of this function must be a map with a subset of the keys of its
-- argument. This means the function can alter the values of its argument
-- and it can remove key-value pairs from it, but it can break
-- MapF ordering invariants if it introduces new keys.
--
-- Third function is analogous to the second function except that it
-- applies to the second map argument of mergeWithKeyM instead of
-- the first.
--
-- Common examples of the two functions include id when
-- constructing a union or const empty when constructing an
-- intersection.
mergeWithKeyM :: forall k a b c m. (Applicative m, OrdF k) => (forall tp. k tp -> a tp -> b tp -> m (Maybe (c tp))) -> (MapF k a -> m (MapF k c)) -> (MapF k b -> m (MapF k c)) -> MapF k a -> MapF k b -> m (MapF k c)
-- | Like a 2-tuple, but with an existentially quantified parameter that
-- both of the elements share.
data Pair (a :: k -> Type) (b :: k -> Type)
[Pair] :: !a tp -> !b tp -> Pair a b
instance forall a (k :: a -> *) (v :: a -> *). Data.Parameterized.Classes.OrdF k => Data.Parameterized.Classes.IxedF a (Data.Parameterized.Map.MapF k v)
instance forall a (k :: a -> *) (v :: a -> *). Data.Parameterized.Classes.OrdF k => Data.Parameterized.Classes.AtF a (Data.Parameterized.Map.MapF k v)
instance forall k1 (k2 :: k1 -> *) (a :: k1 -> *). Data.Parameterized.Utils.BinTree.IsBinTree (Data.Parameterized.Map.MapF k2 a) (Data.Parameterized.Pair.Pair k2 a)
instance forall v (k :: v -> *) (a :: v -> *). (Data.Type.Equality.TestEquality k, Data.Parameterized.Classes.EqF a) => GHC.Classes.Eq (Data.Parameterized.Map.MapF k a)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.FunctorF (Data.Parameterized.Map.MapF ktp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.FoldableF (Data.Parameterized.Map.MapF ktp)
instance forall k (ktp :: k -> *). Data.Parameterized.TraversableF.TraversableF (Data.Parameterized.Map.MapF ktp)
instance forall v (ktp :: v -> *) (rtp :: v -> *). (Data.Parameterized.Classes.ShowF ktp, Data.Parameterized.Classes.ShowF rtp) => GHC.Show.Show (Data.Parameterized.Map.MapF ktp rtp)
module Data.Parameterized.Utils.Endian
-- | Determines the composition of smaller numeric values into larger
-- values.
--
-- BigEndian = most significant values in the lowest index location /
-- first LittleEndian = least significant values in the lowest index
-- location / first
--
-- Value: 0x01020304 BigEndian = [ 0x01, 0x02, 0x03, 0x04 ] LittleEndian
-- = [ 0x04, 0x03, 0x02, 0x01 ]
data Endian
LittleEndian :: Endian
BigEndian :: Endian
instance GHC.Classes.Ord Data.Parameterized.Utils.Endian.Endian
instance GHC.Show.Show Data.Parameterized.Utils.Endian.Endian
instance GHC.Classes.Eq Data.Parameterized.Utils.Endian.Endian
-- | A fixed-size vector of typed elements.
--
-- NB: This module contains an orphan instance. It will be included in
-- GHC 8.10, see
-- https://gitlab.haskell.org/ghc/ghc/merge_requests/273.
module Data.Parameterized.Vector
-- | Fixed-size non-empty vectors.
data Vector n a
-- | Make a vector of the given length and element type. Returns
-- Nothing if the input list does not have the right number of
-- elements. O(n).
fromList :: 1 <= n => NatRepr n -> [a] -> Maybe (Vector n a)
-- | Get the elements of the vector as a list, lowest index first.
toList :: Vector n a -> [a]
-- | Convert a non-empty Assignment to a fixed-size Vector.
--
-- This function uses the same ordering convention as toVector.
fromAssignment :: forall f ctx tp e. (forall tp'. f tp' -> e) -> Assignment f (ctx ::> tp) -> Vector (CtxSize (ctx ::> tp)) e
-- | Convert a Vector into a Assignment.
--
-- This function uses the same ordering convention as toVector.
toAssignment :: Size ctx -> (forall tp. Index ctx tp -> e -> f tp) -> Vector (CtxSize ctx) e -> Assignment f ctx
-- | Length of the vector. O(1)
length :: Vector n a -> NatRepr n
-- | Proof that the length of this vector is not 0.
nonEmpty :: Vector n a -> LeqProof 1 n
-- | The length of the vector as an Int.
lengthInt :: Vector n a -> Int
elemAt :: (i + 1) <= n => NatRepr i -> Vector n a -> a
-- | Get the element at the given index. O(1)
elemAtMaybe :: Int -> Vector n a -> Maybe a
-- | Get the element at the given index. Raises an exception if the element
-- is not in the vector's domain. O(1)
elemAtUnsafe :: Int -> Vector n a -> a
indicesUpTo :: NatRepr n -> Vector (n + 1) (Fin (n + 1))
indicesOf :: Vector n a -> Vector n (Fin n)
-- | Insert an element at the given index. O(n).
insertAt :: (i + 1) <= n => NatRepr i -> a -> Vector n a -> Vector n a
-- | Insert an element at the given index. Return Nothing if the
-- element is outside the vector bounds. O(n).
insertAtMaybe :: Int -> a -> Vector n a -> Maybe (Vector n a)
-- | Remove the first element of the vector, and return the rest, if any.
uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
-- | Remove the last element of the vector, and return the rest, if any.
unsnoc :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
-- | Extract a subvector of the given vector.
slice :: ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> Vector n a -> Vector w a
-- | Take the front (lower-indexes) part of the vector.
take :: forall n x a. 1 <= n => NatRepr n -> Vector (n + x) a -> Vector n a
-- | Replace a sub-section of a vector with the given sub-vector.
replace :: ((i + w) <= n, 1 <= w) => NatRepr i -> Vector w a -> Vector n a -> Vector n a
-- | Scope a function to a sub-section of the given vector.
mapAt :: ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> Vector w a) -> Vector n a -> Vector n a
-- | Scope a monadic function to a sub-section of the given vector.
mapAtM :: Monad m => ((i + w) <= n, 1 <= w) => NatRepr i -> NatRepr w -> (Vector w a -> m (Vector w a)) -> Vector n a -> m (Vector n a)
-- | Zip two vectors, potentially changing types. O(n)
zipWith :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipWithM :: Monad m => (a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
zipWithM_ :: Monad m => (a -> b -> m ()) -> Vector n a -> Vector n b -> m ()
-- | Interleave two vectors. The elements of the first vector are at even
-- indexes in the result, the elements of the second are at odd indexes.
interleave :: forall n a. 1 <= n => Vector n a -> Vector n a -> Vector (2 * n) a
-- | Move the elements around, as specified by the given function. * Note:
-- the reindexing function says where each of the elements in the new
-- vector come from. * Note: it is OK for the same input element to end
-- up in mulitple places in the result. O(n)
shuffle :: (Int -> Int) -> Vector n a -> Vector n a
-- | Reverse the vector.
reverse :: forall a n. 1 <= n => Vector n a -> Vector n a
-- | Rotate "left". The first element of the vector is on the "left", so
-- rotate left moves all elemnts toward the corresponding smaller index.
-- Elements that fall off the beginning end up at the end.
rotateL :: Int -> Vector n a -> Vector n a
-- | Rotate "right". The first element of the vector is on the "left", so
-- rotate right moves all elemnts toward the corresponding larger index.
-- Elements that fall off the end, end up at the beginning.
rotateR :: Int -> Vector n a -> Vector n a
-- | Move all elements towards smaller indexes. Elements that fall off the
-- front are ignored. Empty slots are filled in with the given element.
-- O(n).
shiftL :: Int -> a -> Vector n a -> Vector n a
-- | Move all elements towards the larger indexes. Elements that "fall" off
-- the end are ignored. Empty slots are filled in with the given element.
-- O(n).
shiftR :: Int -> a -> Vector n a -> Vector n a
-- | Vector with exactly one element
singleton :: forall a. a -> Vector 1 a
-- | Add an element to the head of a vector
cons :: forall n a. a -> Vector n a -> Vector (n + 1) a
-- | Add an element to the tail of a vector
snoc :: forall n a. Vector n a -> a -> Vector (n + 1) a
-- | Apply a function to each element in a range starting at zero; return
-- the a vector of values obtained. cf. both natFromZero and
-- Data.Vector.generate
generate :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> Vector (h + 1) a
-- | Since Vector is traversable, we can pretty trivially sequence
-- natFromZeroVec inside a monad.
generateM :: forall m h a. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> m a) -> m (Vector (h + 1) a)
-- | Construct a vector with exactly h + 1 elements by repeatedly
-- applying a generator function to a seed value.
--
-- c.f. Data.Vector.unfoldrExactN
unfoldr :: forall h a b. NatRepr h -> (b -> (a, b)) -> b -> Vector (h + 1) a
-- | Monadically construct a vector with exactly h + 1 elements by
-- repeatedly applying a generator function to a seed value.
--
-- c.f. Data.Vector.unfoldrExactNM
unfoldrM :: forall m h a b. Monad m => NatRepr h -> (b -> m (a, b)) -> b -> m (Vector (h + 1) a)
-- | Unfold a vector, with access to the current index.
--
-- c.f. Data.Vector.unfoldrExactN
unfoldrWithIndex :: forall h a b. NatRepr h -> (forall n. n <= h => NatRepr n -> b -> (a, b)) -> b -> Vector (h + 1) a
-- | Monadically unfold a vector, with access to the current index.
--
-- c.f. Data.Vector.unfoldrExactNM
unfoldrWithIndexM :: forall m h a b. Monad m => NatRepr h -> (forall n. n <= h => NatRepr n -> b -> m (a, b)) -> b -> m (Vector (h + 1) a)
-- | Build a vector by repeatedly applying a function to a seed value.
--
-- Compare to iterateN
iterateN :: NatRepr n -> (a -> a) -> a -> Vector (n + 1) a
-- | Build a vector by repeatedly applying a monadic function to a seed
-- value.
--
-- Compare to iterateNM.
iterateNM :: Monad m => NatRepr n -> (a -> m a) -> a -> m (Vector (n + 1) a)
-- | Monadically join a vector of values, using the given function. This
-- functionality can sometimes be reproduced by creating a newtype
-- wrapper and using joinWith, this implementation is provided
-- for convenience.
joinWithM :: forall m f n w. (1 <= w, Monad m) => (forall l. 1 <= l => NatRepr l -> f w -> f l -> m (f (w + l))) -> NatRepr w -> Vector n (f w) -> m (f (n * w))
-- | Join a vector of vectors, using the given function to combine the
-- sub-vectors.
joinWith :: forall f n w. 1 <= w => (forall l. 1 <= l => NatRepr l -> f w -> f l -> f (w + l)) -> NatRepr w -> Vector n (f w) -> f (n * w)
-- | Split a vector into a vector of vectors.
--
-- The Endian parameter determines the ordering of the inner
-- vectors. If LittleEndian, then less significant bits go into
-- smaller indexes. If BigEndian, then less significant bits go
-- into larger indexes. See the documentation for split for more
-- details.
splitWith :: forall f w n. (1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w) -> NatRepr n -> NatRepr w -> f (n * w) -> Vector n (f w)
-- | An applicative version of splitWith.
splitWithA :: forall f g w n. (Applicative f, 1 <= w, 1 <= n) => Endian -> (forall i. (i + w) <= (n * w) => NatRepr (n * w) -> NatRepr i -> g (n * w) -> f (g w)) -> NatRepr n -> NatRepr w -> g (n * w) -> f (Vector n (g w))
-- | Split a vector into a vector of vectors. The default ordering of the
-- outer result vector is LittleEndian.
--
-- For example: let wordsize = knownNat :: NatRepr 3 vecsize =
-- knownNat :: NatRepr 12 numwords = knownNat :: NatRepr 4 (12 / 3) Just
-- inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ] in
-- show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9],
-- [10,11,12] ]" whereas a BigEndian result would have been [
-- [10,11,12], [7,8,9], [4,5,6], [1,2,3] ]
split :: (1 <= w, 1 <= n) => NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
-- | Join a vector of vectors into a single vector. Assumes an
-- append/LittleEndian join strategy: the order of the inner
-- vectors is preserved in the result vector.
--
--
-- let innersize = knownNat :: NatRepr 4
-- Just inner1 = fromList innersize [ 1, 2, 3, 4 ]
-- Just inner2 = fromList innersize [ 5, 6, 7, 8 ]
-- Just inner3 = fromList innersize [ 9, 10, 11, 12 ]
-- outersize = knownNat :: NatRepr 3
-- Just outer = fromList outersize [ inner1, inner2, inner3 ]
-- in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]
--
--
-- a prepend/BigEndian join strategy would have the result: [
-- 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ]
join :: 1 <= w => NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
-- | Append two vectors. The first one is at lower indexes in the result.
append :: Vector m a -> Vector n a -> Vector (m + n) a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.Vector.Vector n a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Parameterized.Vector.Vector n a)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)
instance WithIndex.TraversableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.Vector.Vector n)
instance GHC.Base.Functor (Data.Parameterized.Vector.Vector n)
instance Data.Foldable.Foldable (Data.Parameterized.Vector.Vector n)
instance Data.Traversable.Traversable (Data.Parameterized.Vector.Vector n)
-- | See Data.Parameterized.FinMap.
module Data.Parameterized.FinMap.Unsafe
-- | FinMap n a is a map with Fin n keys
-- and a values.
data FinMap (n :: Nat) a
-- | O(1). Is the map empty?
null :: FinMap n a -> Bool
-- | O(min(n,W)). Fetch the value at the given key in the map.
lookup :: Fin n -> FinMap n a -> Maybe a
-- | O(1). Number of elements in the map.
size :: forall n a. FinMap n a -> Fin (n + 1)
-- | O(1). Increase maximum key/size by 1.
--
-- This does not alter the key-value pairs in the map, but rather
-- increases the maximum number of key-value pairs that the map can hold.
-- See Data.Parameterized.FinMap for more information.
--
-- Requires n + 1 < (maxBound :: Int).
incMax :: FinMap n a -> FinMap (n + 1) a
-- | O(1). Increase maximum key/size.
--
-- Requires m < (maxBound :: Int).
embed :: n <= m => NatRepr m -> FinMap n a -> FinMap m a
-- | O(1). The empty map.
empty :: KnownNat n => FinMap n a
-- | O(1). A map with one element.
singleton :: a -> FinMap 1 a
-- | O(min(n,W)).
insert :: Fin n -> a -> FinMap n a -> FinMap n a
buildFinMap :: forall m a. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a
-- | O(min(n,W)).
append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
-- | O(min(n,W)).
delete :: Fin n -> FinMap n a -> FinMap n a
-- | Decrement the key/size, removing the item at key n + 1 if
-- present.
decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
-- | O(n+m).
unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
-- | O(n+m).
unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
-- | O(n+m). Left-biased union, i.e. (union ==
-- unionWith const).
union :: FinMap n a -> FinMap n a -> FinMap n a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Base.Semigroup (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.TypeNats.KnownNat n => GHC.Base.Monoid (Data.Parameterized.FinMap.Unsafe.FinMap n a)
instance GHC.Base.Functor (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance Data.Foldable.Foldable (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance Data.Traversable.Traversable (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Unsafe.FinMap n)
instance GHC.Show.Show a => GHC.Show.Show (Data.Parameterized.FinMap.Unsafe.FinMap n a)
-- | FinMap n a conceptually (see NOTE) a map with
-- Fin n keys, implying a maximum size of n.
-- Here's how FinMap compares to other map-like types:
--
--
-- - FinMap n a is conceptually isomorphic to a
-- Vector n (Maybe a), but can be more
-- space-efficient especially if n is large and the vector is
-- populated with a small number of Just values.
-- - FinMap is less general than Map, because it
-- has a fixed key type (Fin n).
-- - FinMap n a is similar to IntMap a,
-- but it provides a static guarantee of a maximum size, and its
-- operations (such as size) allow the recovery of more type-level
-- information.
-- - FinMap is dissimilar from
-- Data.Parameterized.Map.MapF in that neither the key nor value
-- type of FinMap is parameterized.
--
--
-- The type parameter n doesn't track the current number
-- of key-value pairs in a FinMap n (i.e., the size of
-- the map), but rather an upper bound. insert and
-- delete don't alter n, whereas incMax does -
-- despite the fact that it has no effect on the keys and values in the
-- FinMap.
--
-- The FinMap interface has two implementations:
--
--
--
-- The implementation in FinMap is property tested against that in
-- FinMap to ensure they have the same behavior.
--
-- In this documentation, W is used in big-O notations the same
-- way as in the Data.IntMap documentation.
--
-- NOTE: Where the word "conceptually" is used, it implies that this
-- correspondence is not literally true, but is true modulo some details
-- such as differences between bounded types like Int and
-- unbounded types like Integer.
--
-- Several of the functions in both implementations are marked
-- INLINE or INLINABLE. There are three reasons for
-- this:
--
--
-- - Some of these just have very small definitions and so inlining is
-- likely more beneficial than harmful.
-- - Some participate in RULES relevant to functions used in
-- their implementations.
-- - They are thin wrappers (often just newtype wrappers) around
-- functions marked INLINE, which should therefore also be
-- inlined.
--
module Data.Parameterized.FinMap
-- | See Data.Parameterized.FinMap.
module Data.Parameterized.FinMap.Safe
-- | FinMap n a is a map with Fin n keys
-- and a values.
data FinMap (n :: Nat) a
-- | O(1). Is the map empty?
null :: FinMap n a -> Bool
-- | O(log n). Fetch the value at the given key in the map.
lookup :: Fin n -> FinMap n a -> Maybe a
-- | O(nlog(n)). Number of elements in the map.
--
-- This operation is much slower than size because its
-- implementation must provide significant evidence to the type-checker,
-- and the easiest way to do that is fairly inefficient. If speed is a
-- concern, use Data.Parameterized.FinMap.Unsafe.
size :: forall n a. FinMap n a -> Fin (n + 1)
-- | O(n log n). Increase maximum key/size by 1.
--
-- This does not alter the key-value pairs in the map, but rather
-- increases the maximum number of key-value pairs that the map can hold.
-- See Data.Parameterized.FinMap for more information.
--
-- Requires n + 1 < (maxBound :: Int).
incMax :: forall n a. FinMap n a -> FinMap (n + 1) a
-- | O(n log n). Increase maximum key/size.
--
-- Requires m < (maxBound :: Int).
embed :: n <= m => NatRepr m -> FinMap n a -> FinMap m a
-- | O(1). The empty map.
empty :: KnownNat n => FinMap n a
-- | O(1). A map with one element.
singleton :: a -> FinMap 1 a
-- | O(log n).
insert :: Fin n -> a -> FinMap n a -> FinMap n a
buildFinMap :: forall m a. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> FinMap n a -> FinMap (n + 1) a) -> FinMap m a
-- | O(min(n,W)).
append :: NatRepr n -> a -> FinMap n a -> FinMap (n + 1) a
fromVector :: forall n a. Vector n (Maybe a) -> FinMap n a
-- | O(log n).
delete :: Fin n -> FinMap n a -> FinMap n a
-- | Decrement the key/size, removing the item at key n + 1 if
-- present.
decMax :: NatRepr n -> FinMap (n + 1) a -> FinMap n a
mapWithKey :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b
-- | O(n+m).
unionWithKey :: (Fin n -> a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
-- | O(n+m).
unionWith :: (a -> a -> a) -> FinMap n a -> FinMap n a -> FinMap n a
-- | O(n+m). Left-biased union, i.e. (union ==
-- unionWith const).
union :: FinMap n a -> FinMap n a -> FinMap n a
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Base.Semigroup (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.TypeNats.KnownNat n => GHC.Base.Monoid (Data.Parameterized.FinMap.Safe.FinMap n a)
instance GHC.Base.Functor (Data.Parameterized.FinMap.Safe.FinMap n)
instance Data.Foldable.Foldable (Data.Parameterized.FinMap.Safe.FinMap n)
instance Data.Traversable.Traversable (Data.Parameterized.FinMap.Safe.FinMap n)
instance WithIndex.FunctorWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Safe.FinMap n)
instance WithIndex.FoldableWithIndex (Data.Parameterized.Fin.Fin n) (Data.Parameterized.FinMap.Safe.FinMap n)
instance GHC.Show.Show a => GHC.Show.Show (Data.Parameterized.FinMap.Safe.FinMap n a)
-- | This module declares a class with a single method that can be used to
-- derive a KnownRepr constraint from an explicit Repr
-- argument. Clients of this method need only create an empty instance.
-- The default implementation suffices.
--
-- For example, suppose we have defined a Repr type for
-- Peano numbers:
--
--
-- data Peano = Z | S Peano
--
-- data PeanoRepr p where
-- ZRepr :: PeanoRepr Z
-- SRepr :: PeanoRepr p -> PeanoRepr (S p)
--
-- -- KnownRepr instances
--
--
-- Then the instance for this class instance IsRepr PeanoRepr
--
-- means that functions with KnownRepr constraints can be used
-- after pattern matching.
--
--
-- f :: KnownRepr PeanoRepr a => ...
--
-- example :: PeanoRepr n -> ...
-- example ZRepr = ...
-- example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...
--
--
-- NOTE: The type f must be a *singleton* type--- i.e. for a
-- given type a there should be only one value that inhabits 'f
-- a'. If that is not the case, this operation can be used to subvert
-- coherence.
--
-- Credit: the unsafe implementation of withRepr is taken from the
-- withSingI function in the singletons library
-- http://hackage.haskell.org/package/singletons-2.5.1/. Packaging
-- this method in a class here makes it more flexible---we do not have to
-- define a dedicated Sing type, but can use any convenient
-- singleton as a Repr.
--
-- NOTE: if this module is compiled without 1, the default method will
-- not be available.
module Data.Parameterized.WithRepr
-- | Turn an explicit Repr value into an implict KnownRepr constraint
class IsRepr (f :: k -> Type)
withRepr :: IsRepr f => f a -> (KnownRepr f a => r) -> r
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.NatRepr.Internal.NatRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.SymbolRepr.SymbolRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.Peano.PeanoRepr
instance Data.Parameterized.WithRepr.IsRepr Data.Parameterized.BoolRepr.BoolRepr
instance forall k (f :: k -> *). Data.Parameterized.WithRepr.IsRepr f => Data.Parameterized.WithRepr.IsRepr (Data.Parameterized.List.List f)
instance forall k (f :: k -> *). Data.Parameterized.WithRepr.IsRepr f => Data.Parameterized.WithRepr.IsRepr (Data.Parameterized.Context.Unsafe.Assignment f)