Data.Binder

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.

Preliminaries

class (Monad m, Ord (Numbering m)) => MonadNumbering m where

Numbering monad.

Associated Types

type Numbering m :: Type

Methods

numbering :: m (Numbering m)

Variable and Box

data Var m a

Representation of variable for abstract syntax tree type a with base numbering monad m.

Instances

Show (Var m a)

Defined in Data.Binder

Methods

showsPrec :: Int -> Var m a -> ShowS

show :: Var m a -> String

showList :: [Var m a] -> ShowS

MonadNumbering m => Eq (Var m a)

Defined in Data.Binder

Methods

(==) :: Var m a -> Var m a -> Bool

(/=) :: Var m a -> Var m a -> Bool

MonadNumbering m => Ord (Var m a)

Defined in Data.Binder

Methods

compare :: Var m a -> Var m a -> Ordering

(<) :: Var m a -> Var m a -> Bool

(<=) :: Var m a -> Var m a -> Bool

(>) :: Var m a -> Var m a -> Bool

(>=) :: Var m a -> Var m a -> Bool

max :: Var m a -> Var m a -> Var m a

min :: Var m a -> Var m a -> Var m a

data Box m a

Representation of under-construction things having type a and containing variables.

Instances

MonadNumbering m => Applicative (Box m)

Defined in Data.Binder

Methods

pure :: a -> Box m a

(<*>) :: Box m (a -> b) -> Box m a -> Box m b

liftA2 :: (a -> b -> c) -> Box m a -> Box m b -> Box m c

(*>) :: Box m a -> Box m b -> Box m b

(<*) :: Box m a -> Box m b -> Box m a

Functor (Box m)

Defined in Data.Binder

Methods

fmap :: (a -> b) -> Box m a -> Box m b

(<$) :: a -> Box m b -> Box m a

class MkFree m a where

Typeclass for free variable constructor.

Methods

mkFree :: Var m a -> a

Variable

var'Key :: forall m a. Lens' (Var m a) (Numbering m)

var'Name :: Lens' (Var m a) Text

var'Box :: Lens' (Var m a) (Box m a)

nameOf :: Var m a -> Text

The name of variable.

boxVar :: Var m a -> Box m a

Smart constructor for Box.

newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)

Create a new variable with given name.

isClosed :: Box m a -> Bool

Box is closed if it exposes no free variables.

occur :: MonadNumbering m => Var m a -> Box m b -> Bool

Check if the variable occurs in the box.

Box

unbox :: forall m a. Box m a -> a

Pick out and complete the construction of a.

box :: MonadNumbering m => a -> Box m a

apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b

boxApply :: (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)

Variable binding

data Binder a b

Variable binding. Essentially, Binder a b means a -> b.

binder'Name :: forall a b. Lens' (Binder a b) Text

binder'Body :: forall a b a b. Lens (Binder a b) (Binder a b) (a -> b) (a -> b)

subst :: Binder a b -> a -> b

Variable substitution.

buildBinder :: Var m a -> (a -> b) -> Binder a b

Smart constructor for Binder.

bind :: (MkFree m a, MonadNumbering m) => Var m a -> Box m b -> Box m (Binder a b)

binding

unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)

unbinding

eqBinder :: (MkFree m a, MonadNumbering m) => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool

Check if two bindings are equal.

boxBinder :: (MkFree m a, MonadNumbering m) => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))