-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A library for canonically representing terms with binding -- -- A library for canonically representing terms with binding via a -- constructor for introducing fresh names and a restricted API that -- avoids the need for alpha-equivalence. @package hobbits @version 1.3 -- | Using the haskell-src-meta package to parse Haskell patterns. module Data.Binding.Hobbits.PatternParser parsePattern :: String -> String -> Either String Pat -- | A right list, or RList, is a list where cons adds to the -- end, or the right-hand side, of a list. This is useful conceptually -- for contexts of name-bindings, where the most recent name-binding is -- intuitively at the end of the context. module Data.Type.RList -- | A form of lists where elements are added to the right instead of the -- left data RList a RNil :: RList a (:>) :: RList a -> a -> RList a -- | Append two RLists at the type level type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k infixr 5 :++: -- | A Member ctx a is a "proof" that the type a is in -- the type list ctx, meaning that ctx equals -- -- 
--   t0 ':>' a ':>' t1 ':>' ... ':>' tn
--
-- -- for some types t0,t1,...,tn. data Member (ctx :: RList k1) (a :: k2) [Member_Base] :: Member (ctx :> a) a [Member_Step] :: Member ctx a -> Member (ctx :> b) a -- | Weaken a Member proof by prepending another context to the -- context it proves membership in weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a -- | An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 -- :++: ctx2. data Append ctx1 ctx2 ctx [Append_Base] :: Append ctx RNil ctx [Append_Step] :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a) -- | Make an Append proof from any RAssign vector for the -- second argument of the append. mkAppend :: RAssign f c2 -> Append c1 c2 (c1 :++: c2) -- | A version of mkAppend that takes in a Proxy argument. mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2) -- | The inverse of mkAppend, that builds an RAssign from an -- Append proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2 -- | An RAssign f r an assignment of an f a for each -- a in the RList r data RAssign (f :: k -> *) (c :: RList k) [MNil] :: RAssign f RNil [:>:] :: RAssign f c -> f a -> RAssign f (c :> a) -- | Create an empty RAssign vector. empty :: RAssign f RNil -- | Create a singleton RAssign vector. singleton :: f a -> RAssign f (RNil :> a) -- | Look up an element of an RAssign vector using a Member -- proof get :: Member c a -> RAssign f c -> f a -- | Heterogeneous type application, including a proof that the input kind -- of the function equals the kind of the type argument data HApply (f :: k1 -> Type) (a :: k2) [HApply] :: forall (f :: k -> Type) (a :: k). f a -> HApply f a -- | Look up an element of an RAssign vector using a Member -- proof at what GHC thinks might be a different kind, i.e., -- heterogeneously hget :: forall (f :: k1 -> Type) (c :: RList k1) (a :: k2). Member c a -> RAssign f c -> HApply f a -- | Modify an element of an RAssign vector using a Member -- proof. modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c -- | Set an element of an RAssign vector using a Member -- proof. set :: Member c a -> f a -> RAssign f c -> RAssign f c -- | Test if an object is in an RAssign, returning a Member -- proof if it is memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a) -- | Map a function on all elements of an RAssign vector. map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c -- | An alternate name for map that does not clash with the prelude mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c -- | Map a binary function on all pairs of elements of two RAssign -- vectors. map2 :: (forall x. f x -> g x -> h x) -> RAssign f c -> RAssign g c -> RAssign h c -- | Take the tail of an RAssign tail :: RAssign f (ctx :> a) -> RAssign f ctx -- | Convert a monomorphic RAssign to a list toList :: RAssign (Constant a) c -> [a] -- | Map a function with monomorphic output type across an RAssign -- to create a standard list: -- -- 
--   mapToList f = toList . map (Constant . f)
--
mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b] -- | Append two RAssign vectors. append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2) -- | Perform a right fold across an RAssign foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r -- | Split an RAssign vector into two pieces. The first argument is -- a phantom argument that gives the form of the first list piece. split :: c ~ (c1 :++: c2) => prx c1 -> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2) -- | Create a vector of proofs that each type in c is a -- Member of c. members :: RAssign f c -> RAssign (Member c) c -- | A type-class which ensures that ctx is a valid context, i.e., has | -- the form (RNil :> t1 :> ... :> tn) for some types t1 through -- tn class TypeCtx ctx typeCtxProxies :: TypeCtx ctx => RAssign Proxy ctx instance Data.Type.RList.TypeCtx 'Data.Type.RList.RNil instance forall k (ctx :: Data.Type.RList.RList k) (a :: k). Data.Type.RList.TypeCtx ctx => Data.Type.RList.TypeCtx (ctx 'Data.Type.RList.:> a) instance forall k2 k1 (r :: Data.Type.RList.RList k1) (a :: k2). GHC.Show.Show (Data.Type.RList.Member r a) instance forall k k1 (ctx :: Data.Type.RList.RList k1). Data.Type.Equality.TestEquality (Data.Type.RList.Member ctx) instance forall k2 k1 (ctx :: Data.Type.RList.RList k1) (a :: k2). GHC.Classes.Eq (Data.Type.RList.Member ctx a) -- | This module defines the typeclass NuMatching a, which -- allows pattern-matching on the bodies of multi-bindings when their -- bodies have type a. To ensure adequacy, the actual machinery of how -- this works is hidden from the user, but, for any given (G)ADT -- a, the user can use the Template Haskell function -- mkNuMatching to create a NuMatching instance for -- a. module Data.Binding.Hobbits.NuMatching -- | Instances of the NuMatching a class allow -- pattern-matching on multi-bindings whose bodies have type a, -- i.e., on multi-bindings of type Mb ctx a. The -- structure of this class is mostly hidden from the user; see -- mkNuMatching to see how to create instances of the -- NuMatching class. class NuMatching a nuMatchingProof :: NuMatching a => MbTypeRepr a -- | Template Haskell function for creating NuMatching instances for -- (G)ADTs. Typical usage is to include the following line in the source -- file for (G)ADT T (here assumed to have two type arguments): -- -- 
--   $(mkNuMatching [t| forall a b . T a b |])
--
-- -- The mkNuMatching call here will create an instance declaration -- for NuMatching (T a b). It is also possible to include -- a context in the forall type; for example, if we define the -- ID data type as follows: -- -- 
--   data ID a = ID a
--
-- -- then we can create a NuMatching instance for it like this: -- -- 
--   $( mkNuMatching [t| NuMatching a => ID a |])
--
-- -- Note that, when a context is included, the Haskell parser will add the -- forall a for you. mkNuMatching :: Q Type -> Q [Dec] -- | This type states that it is possible to replace free names with fresh -- names in an object of type a. This type essentially just -- captures a representation of the type a as either a Name type, a -- multi-binding, a function type, or a (G)ADT. In order to be sure that -- only the "right" proofs are used for (G)ADTs, however, this type is -- hidden from the user, and can only be constructed with -- mkNuMatching. data MbTypeRepr a -- | Build an MbTypeRepr for type a by using an isomorphism -- with an already-representable type b. This is useful for -- building NuMatching instances for, e.g., Integral types, -- by mapping to and from Integer, without having to define -- instances for each one in this module. isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a -- | Builds an MbTypeRepr proof for use in a NuMatching -- instance. This proof is unsafe because it does no renaming of fresh -- names, so should only be used for types that are guaranteed not to -- contain any Name or Mb values. unsafeMbTypeRepr :: MbTypeRepr a -- | Typeclass for lifting the NuMatching constraint to functors on -- arbitrary kinds that do not require any constraints on their input -- types class NuMatchingAny1 (f :: k -> Type) nuMatchingAny1Proof :: NuMatchingAny1 f => MbTypeRepr (f a) instance forall k (f :: k -> *) (a :: k). Data.Binding.Hobbits.NuMatching.NuMatchingAny1 f => Data.Binding.Hobbits.NuMatching.NuMatching (f a) instance Data.Binding.Hobbits.NuMatching.NuMatchingAny1 Data.Binding.Hobbits.Internal.Name.Name instance forall k (a :: k). Data.Binding.Hobbits.NuMatching.NuMatchingAny1 ((Data.Type.Equality.:~:) a) instance Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatchingAny1 (Data.Functor.Constant.Constant a) instance forall k (f :: k -> *) (ctx :: Data.Type.RList.RList k). Data.Binding.Hobbits.NuMatching.NuMatchingAny1 f => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Type.RList.RAssign f ctx) instance forall k (a :: k). Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Internal.Name.Name a) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Internal.Closed.Closed a) instance (Data.Binding.Hobbits.NuMatching.NuMatching a, Data.Binding.Hobbits.NuMatching.NuMatching b) => Data.Binding.Hobbits.NuMatching.NuMatching (a -> b) instance forall k a (ctx :: Data.Type.RList.RList k). Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Internal.Mb.Mb ctx a) instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Bool instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Int instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Integer.Type.Integer instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Char instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Natural.Natural instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Float instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Double instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Types.Word instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Word.Word8 instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Word.Word16 instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Word.Word32 instance Data.Binding.Hobbits.NuMatching.NuMatching GHC.Word.Word64 instance Data.Binding.Hobbits.NuMatching.NuMatching () instance (Data.Binding.Hobbits.NuMatching.NuMatching a, Data.Binding.Hobbits.NuMatching.NuMatching b) => Data.Binding.Hobbits.NuMatching.NuMatching (a, b) instance (Data.Binding.Hobbits.NuMatching.NuMatching a, Data.Binding.Hobbits.NuMatching.NuMatching b, Data.Binding.Hobbits.NuMatching.NuMatching c) => Data.Binding.Hobbits.NuMatching.NuMatching (a, b, c) instance (Data.Binding.Hobbits.NuMatching.NuMatching a, Data.Binding.Hobbits.NuMatching.NuMatching b, Data.Binding.Hobbits.NuMatching.NuMatching c, Data.Binding.Hobbits.NuMatching.NuMatching d) => Data.Binding.Hobbits.NuMatching.NuMatching (a, b, c, d) instance Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching [a] instance Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Vector.Vector a) -- | Defines a quasi-quoter for writing patterns that match the bodies of -- Mb multi-bindings. Uses the haskell-src-exts parser. [nuP| -- P ] defines a pattern that will match a multi-binding whose body -- matches P. Any variables matched by P will remain -- inside the binding; thus, for example, in the pattern [nuP| x -- |], x matches the entire multi-binding. -- -- Examples: -- -- 
--   case (nu Left) of [nuP| Left x |] -> x  ==  nu id
--
-- -- [clP| P |] does the same for the Closed type, and -- [clNuP| P |] works for both simultaneously: Closed -- (Mb ctx a). module Data.Binding.Hobbits.QQ -- | Quasi-quoter for patterns that match over Mb nuP :: QuasiQuoter -- | Quasi-quoter for patterns that match over Closed, built using -- clKit clP :: QuasiQuoter -- | Quasi-quoter for patterns that match over Closed (Mb -- ctx a) clNuP :: QuasiQuoter -- | This module defines multi-bindings as the type Mb, as well as a -- number of operations on multi-bindings. See the paper E. Westbrook, N. -- Frisby, P. Brauner, "Hobbits for Haskell: A Library for Higher-Order -- Encodings in Functional Programming Languages" for more information. module Data.Binding.Hobbits.Mb -- | A Name a is a bound name that is associated with type -- a. data Name (a :: k) -- | A Binding is simply a multi-binding that binds one name type Binding (a :: k) = Mb (RNil :> a) -- | An Mb ctx b is a multi-binding that binds one name for each -- type in ctx, where ctx has the form RNil -- :> t1 :> ... :> tn. Internally, -- multi-bindings are represented either as "fresh functions", which are -- functions that quantify over all fresh names that have not been used -- before and map them to the body of the binding, or as "fresh pairs", -- which are pairs of a list of names that are guaranteed to be fresh -- along with a body. Note that fresh pairs must come with an -- MbTypeRepr for the body type, to ensure that the names given in -- the pair can be relaced by fresher names. data Mb (ctx :: RList k) b -- | nu f creates a binding which binds a fresh name n -- and whose body is the result of f n. nu :: forall (a :: k1) (b :: *). (Name a -> b) -> Binding a b -- | The expression nuMulti p f creates a multi-binding of zero or -- more names, one for each element of the vector p. The bound -- names are passed the names to f, which returns the body of -- the multi-binding. The argument p, of type RAssign -- f ctx, acts as a "phantom" argument, used to reify the list of -- types ctx at the term level; thus it is unimportant what the -- type function f is. nuMulti :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b -- | 
--   nus = nuMulti
--
nus :: () => RAssign f ctx -> (RAssign (Name :: k -> Type) ctx -> b) -> Mb ctx b -- | Creates an empty binding that binds 0 names. emptyMb :: a -> Mb RNil a -- | Extend the context of a name-binding by adding a single type extMb :: Mb ctx a -> Mb (ctx :> tp) a -- | Extend the context of a name-binding with multiple types extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a -- | cmpName n m compares names n and m of types -- Name a and Name b, respectively. When they are -- equal, Some e is returned for e a proof of type -- a :~: b that their types are equal. Otherwise, None -- is returned. -- -- For example: -- -- 
--   nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
--   nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
--
cmpName :: Name a -> Name b -> Maybe (a :~: b) -- | Heterogeneous comparison of names, that could be at different kinds hcmpName :: forall (a :: k1) (b :: k2). Name a -> Name b -> Maybe (a :~~: b) -- | Checks if a name is bound in a multi-binding, returning Left -- mem when the name is bound, where mem is a proof that -- the type of the name is in the type list for the multi-binding, and -- returning Right n when the name is not bound, where -- n is the name. -- -- For example: -- -- 
--   nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base
--   nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n
--
mbNameBoundP :: forall (a :: k1) (ctx :: RList k2). Mb ctx (Name a) -> Either (Member ctx a) (Name a) -- | Compares two names inside bindings, taking alpha-equivalence into -- account; i.e., if both are the ith name, or both are the same -- name not bound in their respective multi-bindings, then they compare -- as equal. The return values are the same as for cmpName, so -- that Some Refl is returned when the names are equal and -- Nothing is returned when they are not. mbCmpName :: forall (a :: k1) (b :: k1) (c :: RList k2). Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b) -- | Eliminates an empty binding, returning its body. Note that -- elimEmptyMb is the inverse of emptyMb. elimEmptyMb :: Mb RNil a -> a -- | Combines a binding inside another binding into a single binding. mbCombine :: forall (c1 :: RList k) (c2 :: RList k) a b. Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b -- | Separates a binding into two nested bindings. The first argument, of -- type RAssign any c2, is a "phantom" argument to -- indicate how the context c should be split. mbSeparate :: forall (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a. RAssign any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a) -- | Returns a proxy object that enumerates all the types in ctx. mbToProxy :: forall (ctx :: RList k) (a :: *). Mb ctx a -> RAssign Proxy ctx -- | Take a multi-binding inside another multi-binding and move the outer -- binding inside the ineer one. mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a) -- | Put a value inside a multi-binding mbPure :: RAssign f ctx -> a -> Mb ctx a -- | Applies a function in a multi-binding to an argument in a -- multi-binding that binds the same number and types of names. mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b -- | Lift a binary function function to Mbs mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c -- | asdfasdf -- -- The expression nuWithElimMulti args f takes a sequence -- args of one or more multi-bindings (it is a runtime error to -- pass an empty sequence of arguments), each of type Mb ctx ai -- for the same type context ctx of bound names, and a function -- f and does the following: -- -- -- -- For example, here is an alternate way to implement mbApply: -- -- 
--   mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
--   mbApply' f a =
--       nuWithElimMulti ('MNil' :>: f :>: a)
--                       (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
--
nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b) -> RAssign (Mb ctx) args -> Mb ctx b -- | Similar to nuMultiWithElim but binds only one name. Note that -- the argument list here is allowed to be empty. nuWithElim :: (Name a -> RAssign Identity args -> b) -> RAssign (Mb (RNil :> a)) args -> Binding a b -- | Similar to nuMultiWithElim but takes only one argument nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b -- | Similar to nuMultiWithElim but takes only one argument that -- binds a single name. nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b instance forall k a (c :: Data.Type.RList.RList k). GHC.Show.Show a => GHC.Show.Show (Data.Binding.Hobbits.Internal.Mb.Mb c a) instance forall k (ctx :: Data.Type.RList.RList k). GHC.Base.Functor (Data.Binding.Hobbits.Internal.Mb.Mb ctx) instance forall k (ctx :: Data.Type.RList.RList k). Data.Type.RList.TypeCtx ctx => GHC.Base.Applicative (Data.Binding.Hobbits.Internal.Mb.Mb ctx) -- | Provides a set of instances of NuMatching for standard types -- using the template Haskell mkNuMatching function module Data.Binding.Hobbits.NuMatchingInstances instance forall k a (b :: k). Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Functor.Constant.Constant a b) instance forall k (a :: k) (b :: k). Data.Binding.Hobbits.NuMatching.NuMatching (a Data.Type.Equality.:~: b) instance forall k (a :: k). Data.Binding.Hobbits.NuMatching.NuMatching (Data.Proxy.Proxy a) instance forall k2 k1 (ctx :: Data.Type.RList.RList k1) (a :: k2). Data.Binding.Hobbits.NuMatching.NuMatching (Data.Type.RList.Member ctx a) instance (Data.Binding.Hobbits.NuMatching.NuMatching a, Data.Binding.Hobbits.NuMatching.NuMatching b) => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Either.Either a b) instance Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching (GHC.Maybe.Maybe a) -- | Implements mappings from Names to some associated data, using -- Strict. Note that these mappings are strict. -- -- All of the functions in this module operate in an identical manner as -- those of the same name in the Strict module. module Data.Binding.Hobbits.NameMap -- | A heterogeneous map from Names of arbitrary type a to -- elements of f a data NameMap (f :: k -> *) -- | A pair of a Name of some type a along with an element -- of type f a data NameAndElem f [NameAndElem] :: Name a -> f a -> NameAndElem f -- | The empty NameMap empty :: NameMap f -- | The singleton NameMap with precisely one Name and -- corresponding value singleton :: Name a -> f a -> NameMap f -- | Build a NameMap from a list of pairs of names and values they -- map to fromList :: [NameAndElem f] -> NameMap f -- | Insert a Name and a value it maps to into a NameMap insert :: Name a -> f a -> NameMap f -> NameMap f -- | Delete a Name and the value it maps to from a NameMap delete :: Name a -> NameMap f -> NameMap f -- | Apply a function to the value mapped to by a Name adjust :: (f a -> f a) -> Name a -> NameMap f -> NameMap f -- | Update the value mapped to by a Name, possibly deleting it update :: (f a -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f -- | Apply a function to the optional value associated with a Name, -- where Nothing represents the Name not being present in -- the NameMap alter :: (Maybe (f a) -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f -- | Look up the value associated with a Name, returning -- Nothing if there is none lookup :: Name a -> NameMap f -> Maybe (f a) -- | Synonym for lookup with the argument order reversed (!) :: NameMap f -> Name a -> f a -- | Test if a Name has a value in a NameMap member :: Name a -> NameMap f -> Bool -- | Test if a NameMap is empty null :: NameMap f -> Bool -- | Return the number of Names in a NameMap size :: NameMap f -> Int -- | Union two NameMaps union :: NameMap f -> NameMap f -> NameMap f -- | Remove all bindings in the first NameMap for Names in -- the second difference :: NameMap f -> NameMap f -> NameMap f -- | Infix synonym for difference (\\) :: NameMap f -> NameMap f -> NameMap f -- | Intersect two NameMaps intersection :: NameMap f -> NameMap f -> NameMap f -- | Map a function across the values associated with each Name map :: (forall a. f a -> g a) -> NameMap f -> NameMap g -- | Perform a right fold across all values in a NameMap foldr :: (forall a. f a -> b -> b) -> b -> NameMap f -> b -- | Perform a left fold across all values in a NameMap foldl :: (forall b. a -> f b -> a) -> a -> NameMap f -> a -- | Return all Names in a NameMap with their associated -- values assocs :: NameMap f -> [NameAndElem f] -- | Lift a NameMap out of a name-binding using a "partial lifting -- function" that can lift some values in the NameMap out of the -- binding. The resulting NameMap contains those names and -- associated values where the names were not bound by the name-binding -- and the partial lifting function was able to lift their associated -- values. liftNameMap :: forall ctx f a. NuMatchingAny1 f => (forall a. Mb ctx (f a) -> Maybe (f a)) -> Mb ctx (NameMap f) -> NameMap f instance forall k (f :: k -> *). Data.Binding.Hobbits.NuMatching.NuMatchingAny1 f => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.NameMap.NameAndElem f) -- | This module uses Template Haskell to distinguish closed terms, so that -- the library can trust such functions to not contain any Name -- values in their closure. module Data.Binding.Hobbits.Closed -- | The type Closed a represents a closed term of type -- a, i.e., an expression of type a with no free -- (Haskell) variables. Since this cannot be checked directly in the -- Haskell type system, the Closed data type is hidden, and the -- user can only create closed terms using Template Haskell, through the -- mkClosed operator. data Closed a -- | Extract the value of a Closed object unClosed :: Closed a -> a -- | mkClosed is used with Template Haskell quotations to create -- closed terms of type Closed. A quoted expression is closed if -- all of the names occuring in it are either: -- -- 1) bound globally or 2) bound within the quotation or 3) also of type -- Closed. mkClosed :: Q Exp -> Q Exp -- | noClosedNames encodes the hobbits guarantee that no name can -- escape its multi-binding. noClosedNames :: Closed (Name a) -> b -- | Closed terms are closed (sorry) under application. clApply :: Closed (a -> b) -> Closed a -> Closed b -- | Closed multi-bindings are also closed under application. clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) -> Closed (Mb ctx b) -- | When applying a closed function, the argument can be viewed as locally -- closed clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b -- | Mark an object as closed without actually traversing it. This is -- unsafe if the object does in fact contain any names. unsafeClose :: a -> Closed a -- | Typeclass for inherently closed types class Closable a toClosed :: Closable a => a -> Closed a instance Data.Binding.Hobbits.Closed.ClosableAny1 Data.Proxy.Proxy instance forall k k1 (ctx :: Data.Type.RList.RList k1). Data.Binding.Hobbits.Closed.ClosableAny1 (Data.Type.RList.Member ctx) instance forall k (f :: k -> *) (ctx :: Data.Type.RList.RList k). Data.Binding.Hobbits.Closed.ClosableAny1 f => Data.Binding.Hobbits.Closed.Closable (Data.Type.RList.RAssign f ctx) instance Data.Binding.Hobbits.Closed.Closable GHC.Integer.Type.Integer instance forall k2 k1 (ctx :: Data.Type.RList.RList k1) (a :: k2). Data.Binding.Hobbits.Closed.Closable (Data.Type.RList.Member ctx a) instance forall k (a :: k). Data.Binding.Hobbits.Closed.Closable (Data.Proxy.Proxy a) instance Data.Binding.Hobbits.Closed.Closable (Data.Binding.Hobbits.Internal.Closed.Closed a) instance Data.Binding.Hobbits.Closed.Closable GHC.Types.Bool instance Data.Binding.Hobbits.Closed.Closable GHC.Types.Char instance Data.Binding.Hobbits.Closed.Closable GHC.Types.Int instance Data.Binding.Hobbits.Closed.Closable a => Data.Binding.Hobbits.Closed.Closable [a] -- | This module defines the type-class Liftable for lifting -- non-binding-related data out of name-bindings. Note that this code is -- not "trusted", i.e., it is not part of the name-binding abstraction: -- instead, it is all written using the primitives exported by the Mb module Data.Binding.Hobbits.Liftable -- | The class Liftable a gives a "lifting function" for a, which -- can take any data of type a out of a multi-binding of type -- Mb ctx a. class NuMatching a => Liftable a mbLift :: Liftable a => Mb ctx a -> a -- | Lift a list (but not its elements) out of a multi-binding mbList :: NuMatching a => Mb c [a] -> [Mb c a] instance Data.Binding.Hobbits.Liftable.Liftable GHC.Types.Char instance Data.Binding.Hobbits.Liftable.Liftable GHC.Types.Int instance Data.Binding.Hobbits.Liftable.Liftable GHC.Integer.Type.Integer instance Data.Binding.Hobbits.Liftable.Liftable (Data.Binding.Hobbits.Internal.Closed.Closed a) instance Data.Binding.Hobbits.Liftable.Liftable GHC.Natural.Natural instance forall k2 k1 (c :: Data.Type.RList.RList k1) (a :: k2). Data.Binding.Hobbits.Liftable.Liftable (Data.Type.RList.Member c a) instance (GHC.Real.Integral a, Data.Binding.Hobbits.Liftable.Liftable a) => Data.Binding.Hobbits.Liftable.Liftable (GHC.Real.Ratio a) instance Data.Binding.Hobbits.Liftable.Liftable a => Data.Binding.Hobbits.Liftable.Liftable [a] instance Data.Binding.Hobbits.Liftable.Liftable () instance (Data.Binding.Hobbits.Liftable.Liftable a, Data.Binding.Hobbits.Liftable.Liftable b) => Data.Binding.Hobbits.Liftable.Liftable (a, b) instance Data.Binding.Hobbits.Liftable.Liftable GHC.Types.Bool instance Data.Binding.Hobbits.Liftable.Liftable a => Data.Binding.Hobbits.Liftable.Liftable (GHC.Maybe.Maybe a) instance (Data.Binding.Hobbits.Liftable.Liftable a, Data.Binding.Hobbits.Liftable.Liftable b) => Data.Binding.Hobbits.Liftable.Liftable (Data.Either.Either a b) instance forall k (a :: k) (b :: k). Data.Binding.Hobbits.Liftable.Liftable (a Data.Type.Equality.:~: b) instance forall k (a :: k). Data.Binding.Hobbits.Liftable.Liftable (Data.Proxy.Proxy a) instance forall k a (ctx :: Data.Type.RList.RList k). GHC.Classes.Eq a => GHC.Classes.Eq (Data.Binding.Hobbits.Internal.Mb.Mb ctx a) instance (GHC.Real.Integral a, Data.Binding.Hobbits.NuMatching.NuMatching a) => Data.Binding.Hobbits.NuMatching.NuMatching (GHC.Real.Ratio a) -- | Implements sets of Names using Strict. Note that these -- mappings are strict. module Data.Binding.Hobbits.NameSet -- | A set of Names whose types all have kind k data NameSet k -- | A Name of some unknown type of kind k data SomeName k SomeName :: Name a -> SomeName k -- | The empty NameSet empty :: NameSet k -- | The singleton NameSet singleton :: Name (a :: k) -> NameSet k -- | Convert a list of names to a NameSet fromList :: [SomeName k] -> NameSet k -- | Convert a NameSet to a list toList :: NameSet k -> [SomeName k] -- | Insert a name into a NameSet insert :: Name (a :: k) -> NameSet k -> NameSet k -- | Delete a name from a NameSet delete :: Name (a :: k) -> NameSet k -> NameSet k -- | Test if a name is in a NameSet member :: Name (a :: k) -> NameSet k -> Bool -- | Test if a NameSet is empty null :: NameSet k -> Bool -- | Compute the cardinality of a NameSet size :: NameSet k -> Int -- | Take the union of two NameSets union :: NameSet k -> NameSet k -> NameSet k -- | Take the union of a list of NameSets unions :: Foldable f => f (NameSet k) -> NameSet k -- | Take the set of all elements of the first NameSet not in the -- second difference :: NameSet k -> NameSet k -> NameSet k -- | Another name for difference (\\) :: NameSet k -> NameSet k -> NameSet k -- | Take the intersection of two NameSets intersection :: NameSet k -> NameSet k -> NameSet k -- | Map a function across all elements of a NameSet map :: (forall (a :: k). Name a -> Name a) -> NameSet k -> NameSet k -- | Perform a right fold of a function across all elements of a -- NameSet foldr :: (forall (a :: k). Name a -> r -> r) -> r -> NameSet k -> r -- | Perform a left fold of a function across all elements of a -- NameSet foldl :: (forall (a :: k). r -> Name a -> r) -> r -> NameSet k -> r -- | Lift a NameSet out of a name-binding by lifting all names not -- bound by the name-binding and then forming a NameSet from those -- lifted names liftNameSet :: Mb ctx (NameSet (k :: Type)) -> NameSet k instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.NameSet.SomeName k) -- | This module defines monads that are compatible with the notion of -- name-binding, where a monad is compatible with name-binding iff it can -- intuitively run computations that are inside name-bindings. More -- formally, a binding monad is a monad with an operation -- mbM that commutes name-binding with the monadic operations, -- meaning: -- -- 
--   'mbM' ('nuMulti' $ \ns -> 'return' a) == 'return' ('nuMulti' $ \ns -> a)
--   'mbM' ('nuMulti' $ \ns -> m >>= f)
--     == 'mbM' ('nuMulti' $ \ns -> m) >>= \mb_x ->
--        'mbM' (('nuMulti' $ \ns x -> f x) `'mbApply'` mb_x)
--
module Data.Binding.Hobbits.MonadBind -- | The class of name-binding monads class Monad m => MonadBind m mbM :: (MonadBind m, NuMatching a) => Mb ctx (m a) -> m (Mb ctx a) -- | A version of MonadBind that does not require a -- NuMatching instance on the element type of the multi-binding in -- the monad class MonadBind m => MonadStrongBind m strongMbM :: MonadStrongBind m => Mb ctx (m a) -> m (Mb ctx a) instance Data.Binding.Hobbits.MonadBind.MonadClosed Data.Functor.Identity.Identity instance (Data.Binding.Hobbits.MonadBind.MonadClosed m, Data.Binding.Hobbits.Closed.Closable s) => Data.Binding.Hobbits.MonadBind.MonadClosed (Control.Monad.Trans.State.Lazy.StateT s m) instance Data.Binding.Hobbits.MonadBind.BindState (Data.Binding.Hobbits.Internal.Closed.Closed s) instance (Data.Binding.Hobbits.MonadBind.MonadBind m, Data.Binding.Hobbits.MonadBind.BindState s) => Data.Binding.Hobbits.MonadBind.MonadBind (Control.Monad.Trans.State.Lazy.StateT s m) instance (Data.Binding.Hobbits.MonadBind.MonadStrongBind m, Data.Binding.Hobbits.MonadBind.BindState s) => Data.Binding.Hobbits.MonadBind.MonadStrongBind (Control.Monad.Trans.State.Lazy.StateT s m) instance Data.Binding.Hobbits.MonadBind.MonadStrongBind Data.Functor.Identity.Identity instance Data.Binding.Hobbits.MonadBind.MonadStrongBind m => Data.Binding.Hobbits.MonadBind.MonadStrongBind (Control.Monad.Trans.Reader.ReaderT r m) instance Data.Binding.Hobbits.MonadBind.MonadBind Data.Functor.Identity.Identity instance Data.Binding.Hobbits.MonadBind.MonadBind GHC.Maybe.Maybe instance Data.Binding.Hobbits.MonadBind.MonadBind m => Data.Binding.Hobbits.MonadBind.MonadBind (Control.Monad.Trans.Reader.ReaderT r m) -- | This library implements multi-bindings as described in the paper E. -- Westbrook, N. Frisby, P. Brauner, "Hobbits for Haskell: A Library for -- Higher-Order Encodings in Functional Programming Languages". module Data.Binding.Hobbits -- | A form of lists where elements are added to the right instead of the -- left data RList a RNil :: RList a (:>) :: RList a -> a -> RList a -- | An RAssign f r an assignment of an f a for each -- a in the RList r data RAssign (f :: k -> *) (c :: RList k) [MNil] :: RAssign f RNil [:>:] :: RAssign f c -> f a -> RAssign f (c :> a) -- | A Member ctx a is a "proof" that the type a is in -- the type list ctx, meaning that ctx equals -- -- 
--   t0 ':>' a ':>' t1 ':>' ... ':>' tn
--
-- -- for some types t0,t1,...,tn. data Member (ctx :: RList k1) (a :: k2) [Member_Base] :: Member (ctx :> a) a [Member_Step] :: Member ctx a -> Member (ctx :> b) a -- | Append two RLists at the type level type family (r1 :: RList k) :++: (r2 :: RList k) :: RList k infixr 5 :++: -- | An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 -- :++: ctx2. data Append ctx1 ctx2 ctx [Append_Base] :: Append ctx RNil ctx [Append_Step] :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a) module Data.Binding.Hobbits.Examples.LambdaLifting.Terms data L a data D a data Term :: * -> * [Var] :: Name (L a) -> Term a [Lam] :: Binding (L b) (Term a) -> Term (b -> a) [App] :: Term (b -> a) -> Term b -> Term a lam :: (Term a -> Term b) -> Term (a -> b) data DTerm :: * -> * [TVar] :: Name (L a) -> DTerm a [TDVar] :: Name (D a) -> DTerm a [TApp] :: DTerm (a -> b) -> DTerm a -> DTerm b data Decl :: * -> * [Decl_One] :: Binding (L a) (DTerm b) -> Decl (a -> b) [Decl_Cons] :: Binding (L a) (Decl b) -> Decl (a -> b) data Decls :: * -> * [Decls_Base] :: DTerm a -> Decls a [Decls_Cons] :: Decl b -> Binding (D b) (Decls a) -> Decls a instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Decls a) instance GHC.Show.Show (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.DTerm a) instance GHC.Show.Show (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Decls a) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Decl a) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.DTerm a) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Term a) instance GHC.Show.Show (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Term a) module Data.Binding.Hobbits.Examples.LambdaLifting.Examples ex1 :: Term ((b1 -> b) -> b1 -> b) ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b) ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b) ex4 :: Term (((b1 -> b) -> b2 -> b) -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1) ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b) ex6 :: Binding (L ((b -> b) -> a)) (Term a) ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b)) exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b) -- | The lambda lifting example from the paper E. Westbrook, N. Frisby, P. -- Brauner, "Hobbits for Haskell: A Library for Higher-Order Encodings in -- Functional Programming Languages". module Data.Binding.Hobbits.Examples.LambdaLifting lambdaLift :: Term a -> Decls a mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)