-- 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.2.2 -- | 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 data RList a RNil :: RList a (:>) :: (RList a) -> a -> RList a proxyCons :: Proxy r -> f a -> Proxy (r :> 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 a Member_Base :: Member (ctx :> a) a Member_Step :: Member ctx a -> Member (ctx :> b) a showsPrecMember :: Bool -> Member ctx a -> ShowS weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b) -- | 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) -- | A MapRList f r is a vector with exactly one element of type -- f a for each type a in the type RList -- r. data MapRList f c MNil :: MapRList f RNil (:>:) :: MapRList f c -> f a -> MapRList f (c :> a) -- | Create an empty MapRList vector. empty :: MapRList f RNil -- | Create a singleton MapRList vector. singleton :: f a -> MapRList f (RNil :> a) -- | Look up an element of a MapRList vector using a Member -- proof. mapRListLookup :: Member c a -> MapRList f c -> f a -- | Map a function on all elements of a MapRList vector. mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c -- | Map a binary function on all pairs of elements of two MapRList -- vectors. mapMapRList2 :: (forall x. f x -> g x -> h x) -> MapRList f c -> MapRList g c -> MapRList h c -- | Append two MapRList vectors. appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2) -- | Make an Append proof from any MapRList vector for the -- second argument of the append. mkAppend :: MapRList f c2 -> Append c1 c2 (c1 :++: c2) -- | A version of mkAppend that takes in a Proxy argument. mkMonoAppend :: Proxy c1 -> MapRList f c2 -> Append c1 c2 (c1 :++: c2) -- | The inverse of mkAppend, that builds an MapRList from an -- Append proxiesFromAppend :: Append c1 c2 c -> MapRList Proxy c2 -- | Split an MapRList vector into two pieces. The first argument is -- a phantom argument that gives the form of the first list piece. splitMapRList :: (c ~ (c1 :++: c2)) => Proxy c1 -> MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2) -- | Create a vector of proofs that each type in c is a -- Member of c. members :: MapRList f c -> MapRList (Member c) c -- | Convert an MapRList to a list mapRListToList :: MapRList (Constant a) c -> [a] -- | 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 => MapRList Proxy ctx instance GHC.Show.Show (Data.Type.RList.Member r a) instance Data.Type.RList.TypeCtx 'Data.Type.RList.RNil instance Data.Type.RList.TypeCtx ctx => Data.Type.RList.TypeCtx (ctx 'Data.Type.RList.:> a) -- | 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 -- | A Binding is simply a multi-binding that binds one name type Binding a = 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 b -- | nu f creates a binding which binds a fresh name n -- and whose body is the result of f n. nu :: (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 -- MapRList 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 :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b -- | 
--   nus = nuMulti
--
nus :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b -- | Creates an empty binding that binds 0 names. emptyMb :: a -> Mb RNil 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) -- | 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 :: 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 :: 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 :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b -- | Separates a binding into two nested bindings. The first argument, of -- type MapRList any c2, is a "phantom" argument to -- indicate how the context c should be split. mbSeparate :: MapRList any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a) -- | Returns a proxy object that enumerates all the types in ctx. mbToProxy :: Mb ctx a -> MapRList 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) -- | 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 -- | The expression nuWithElimMulti args f takes a sequence -- args of zero or more multi-bindings, each of type Mb ctx -- ai for the same type context ctx of bound names, and a -- function f and does the following: -- -- -- -- Note that the types in args must each have a -- NuMatching instance; this is represented with the -- NuMatchingList type class. -- -- Here are some examples: -- -- 
--   (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
--   (<*>) f a =
--       nuWithElimMulti ('MNil' :>: f :>: a)
--                       (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')
--
nuMultiWithElim :: TypeCtx ctx => (MapRList Name ctx -> MapRList Identity args -> b) -> MapRList (Mb ctx) args -> Mb ctx b -- | Similar to nuMultiWithElim but binds only one name. nuWithElim :: (Name a -> MapRList Identity args -> b) -> MapRList (Mb (RNil :> a)) args -> Binding a b -- | Similar to nuMultiWithElim but takes only one argument nuMultiWithElim1 :: TypeCtx ctx => (MapRList 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 GHC.Show.Show a => GHC.Show.Show (Data.Binding.Hobbits.Internal.Mb.Mb c a) instance GHC.Base.Functor (Data.Binding.Hobbits.Internal.Mb.Mb ctx) instance Data.Type.RList.TypeCtx ctx => GHC.Base.Applicative (Data.Binding.Hobbits.Internal.Mb.Mb ctx) -- | 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 Cl 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 Cl data type is hidden, and the user can only -- create closed terms using Template Haskell, through the cl -- operator. data Cl a -- | cl is used with Template Haskell quotations to create closed -- terms of type Cl. A quoted expression is closed if all of the -- names occuring in it are -- -- 1) bound globally or 2) bound within the quotation or 3) also of type -- Cl. cl :: Q Exp -> Q Exp -- | Closed terms are closed (sorry) under application. clApply :: Cl (a -> b) -> Cl a -> Cl b unCl :: Cl a -> a -- | noClosedNames encodes the hobbits guarantee that no name can -- escape its multi-binding. noClosedNames :: Cl (Name a) -> b -- | 
--   mkClosed = cl
--
mkClosed :: Q Exp -> Q Exp -- | 
--   Closed = Cl
--
type Closed = Cl -- | 
--   unClosed = unCl
--
unClosed :: Cl a -> 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] class NuMatchingList args nuMatchingListProof :: NuMatchingList args => MapRList NuMatchingObj args class NuMatching1 f nuMatchingProof1 :: (NuMatching1 f, NuMatching a) => NuMatchingObj (f a) -- | 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 instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Internal.Name.Name a) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Internal.Closed.Cl a) 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 (Data.Binding.Hobbits.Internal.Mb.Mb ctx a) 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 () 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 b) => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Either.Either a b) instance Data.Binding.Hobbits.NuMatching.NuMatching a => Data.Binding.Hobbits.NuMatching.NuMatching [a] instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Type.RList.Member c a) instance Data.Binding.Hobbits.NuMatching.NuMatchingList 'Data.Type.RList.RNil instance (Data.Binding.Hobbits.NuMatching.NuMatchingList args, Data.Binding.Hobbits.NuMatching.NuMatching a) => Data.Binding.Hobbits.NuMatching.NuMatchingList (args 'Data.Type.RList.:> a) instance (Data.Binding.Hobbits.NuMatching.NuMatching1 f, Data.Binding.Hobbits.NuMatching.NuMatchingList ctx) => Data.Binding.Hobbits.NuMatching.NuMatching (Data.Type.RList.MapRList f ctx) -- | 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
--
-- -- module Data.Binding.Hobbits.QQ -- | Quasi-quoter for patterns that match over Mb nuP :: QuasiQuoter -- | Quasi-quoter for patterns that match over Cl, built using -- clKit clP :: QuasiQuoter -- | Quasi-quoter for patterhs that match over Cl (Mb ctx -- a) clNuP :: QuasiQuoter -- | 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.Closed.Closed a) instance Data.Binding.Hobbits.Liftable.Liftable (Data.Type.RList.Member c 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) -- | 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 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 a0) 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 a0) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.DTerm a0) instance Data.Binding.Hobbits.NuMatching.NuMatching (Data.Binding.Hobbits.Examples.LambdaLifting.Terms.Term a0) 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)