-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Variable binding for abstract syntax tree
--
-- binder is purely functional implementation of Ocaml's bindlib.
-- It follows the style of higher-order abstract syntax, and offers the
-- representation of abstract syntax tree.
@package binder
@version 0.3
-- | binder is purely functional implementation of Ocaml's bindlib. It
-- follows the style of higher-order abstract syntax, and offers the
-- representation of abstract syntax tree.
module Data.Binder
-- | Numbering monad.
class (Monad m, Ord (Numbering m)) => MonadNumbering m where {
type Numbering m :: Type;
}
numbering :: MonadNumbering m => m (Numbering m)
-- | Representation of variable for abstract syntax tree type a
-- with base numbering monad m.
data Var m a
-- | Representation of under-construction things having type a and
-- containing variables.
data Box m a
var'Key :: forall m_a6Yp a_a6Yq. Lens' (Var m_a6Yp a_a6Yq) (Numbering m_a6Yp)
var'Name :: Lens' (Var m a) Text
var'mkFree :: Lens' (Var m a) (Var m a -> m a)
var'Box :: Lens' (Var m a) (Box m a)
-- | The name of variable.
nameOf :: Var m a -> Text
-- | Smart constructor for Box.
boxVar :: Var m a -> Box m a
-- | Create a new variable with given name.
newVar :: MonadNumbering m => Text -> (Var m a -> m a) -> m (Var m a)
copyVar :: MonadNumbering m => Var m b -> (Var m a -> m a) -> m (Var m a)
-- | Box is closed if it exposes no free variables.
isClosed :: Box m a -> Bool
-- | Check if the variable occurs in the box.
occur :: MonadNumbering m => Var m a -> Box m b -> Bool
-- | Pick out and complete the construction of a.
unbox :: forall m a. Monad m => Box m a -> m a
box :: MonadNumbering m => a -> Box m a
apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b
boxApply :: Functor m => (a -> b) -> Box m a -> Box m b
boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c
boxApply3 :: MonadNumbering m => (a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d
boxApply4 :: MonadNumbering m => (a -> b -> c -> d -> e) -> Box m a -> Box m b -> Box m c -> Box m d -> Box m e
boxPair :: MonadNumbering m => Box m a -> Box m b -> Box m (a, b)
boxTriple :: MonadNumbering m => Box m a -> Box m b -> Box m c -> Box m (a, b, c)
boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a)
boxList :: MonadNumbering m => [Box m a] -> Box m [a]
boxJoin :: MonadNumbering m => Box m (m a) -> m (Box m a)
-- | Variable binding. Essentially, Binder a m b means a ->
-- m b.
data Binder a m b
binder'Name :: forall a_a8HL m_a8HM b_a8HN. Lens' (Binder a_a8HL m_a8HM b_a8HN) Text
binder'mkFree :: forall a_a8HL m_a8HM b_a8HN. Lens' (Binder a_a8HL m_a8HM b_a8HN) (Var m_a8HM a_a8HL -> m_a8HM a_a8HL)
binder'Body :: forall a_a8HL m_a8HM b_a8HN b_a9vI. Lens (Binder a_a8HL m_a8HM b_a8HN) (Binder a_a8HL m_a8HM b_a9vI) (a_a8HL -> m_a8HM b_a8HN) (a_a8HL -> m_a8HM b_a9vI)
-- | Variable substitution.
subst :: Binder a m b -> a -> m b
-- | Smart constructor for Binder.
buildBinder :: Var m a -> (a -> m b) -> Binder a m b
-- | binding
bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b)
-- | unbinding
unbind :: MonadNumbering m => Binder a m b -> m (Var m a, b)
unbind2 :: MonadNumbering m => Binder a m b1 -> Binder a m b2 -> m (Var m a, b1, b2)
-- | Check if two bindings are equal.
eqBinder :: MonadNumbering m => (b -> b -> m Bool) -> Binder a m b -> Binder a m b -> m Bool
boxBinder :: MonadNumbering m => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b))
bindApply :: MonadNumbering m => Box m (Binder a m b) -> Box m a -> m (Box m b)
type VarList m a = [Var m a]
varList'Keys :: Getter (VarList m a) [Numbering m]
varList'Names :: Getter (VarList m a) [Text]
varList'Boxes :: Getter (VarList m a) [Box m a]
-- | The names of variables.
namesOf :: VarList m a -> [Text]
-- | Smart constructor for a list of Box.
boxVarList :: VarList m a -> [Box m a]
-- | Create new variables with given names.
newVarList :: MonadNumbering m => [Text] -> (Var m a -> m a) -> m (VarList m a)
copyVarList :: MonadNumbering m => VarList m b -> (Var m a -> m a) -> m (VarList m a)
-- | Essentially, BinderList a m b means [a] -> m b.
data BinderList a m b
binderList'Names :: forall a_a9wm m_a9wn b_a9wo. Lens' (BinderList a_a9wm m_a9wn b_a9wo) [Text]
binderList'Body :: forall a_a9wm m_a9wn b_a9wo b_a9Uq. Lens (BinderList a_a9wm m_a9wn b_a9wo) (BinderList a_a9wm m_a9wn b_a9Uq) ([a_a9wm] -> m_a9wn b_a9wo) ([a_a9wm] -> m_a9wn b_a9Uq)
binderList'mkFree :: forall a_a9wm m_a9wn b_a9wo. Lens' (BinderList a_a9wm m_a9wn b_a9wo) (Var m_a9wn a_a9wm -> m_a9wn a_a9wm)
binderList'Arity :: Getter (BinderList a m b) Int
-- | Variable substitution.
substList :: BinderList a m b -> [a] -> m b
-- | Check if two bindings are equal.
eqBinderList :: MonadNumbering m => (b -> b -> m Bool) -> BinderList a m b -> BinderList a m b -> m Bool
-- | binding
bindList :: MonadNumbering m => VarList m a -> Box m b -> Box m (BinderList a m b)
-- | unbinding
unbindList :: MonadNumbering m => BinderList a m b -> m (VarList m a, b)
unbind2List :: MonadNumbering m => BinderList a m b1 -> BinderList a m b2 -> m (VarList m a, b1, b2)
boxBinderList :: MonadNumbering m => (b -> m (Box m b)) -> BinderList a m b -> m (Box m (BinderList a m b))
bindListApply :: MonadNumbering m => Box m (BinderList a m b) -> Box m [a] -> m (Box m b)
instance GHC.Show.Show (Data.Binder.Var m a)
instance GHC.Show.Show (Data.Binder.VarBody m a)
instance GHC.Show.Show (Data.Binder.AnyVar m)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Binder.Box m)
instance Data.Binder.MonadNumbering m => GHC.Base.Applicative (Data.Binder.Box m)
instance Data.Binder.MonadNumbering m => GHC.Classes.Eq (Data.Binder.Var m a)
instance Data.Binder.MonadNumbering m => GHC.Classes.Ord (Data.Binder.Var m a)
instance GHC.Base.Functor m => GHC.Base.Functor (Data.Binder.Closure m)
instance GHC.Base.Applicative m => GHC.Base.Applicative (Data.Binder.Closure m)