Copyright	(c) 2023 Keito Kajitani
License	MIT
Maintainer	Keito Kajitani <ijaketak@gmail.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Binder

Contents

Preliminaries
Variable and Box
- Variable
- Box
Variable binding
List
Variable list
Binder for list

Description

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.

Synopsis

class (Monad m, Ord (Numbering m)) => MonadNumbering m where
- type Numbering m :: Type
- numbering :: m (Numbering m)
data Var m a
data Box m a
var'Key :: forall m a. Lens' (Var m a) (Numbering m)
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)
nameOf :: Var m a -> Text
boxVar :: Var m a -> Box m a
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)
isClosed :: Box m a -> Bool
occur :: MonadNumbering m => Var m a -> Box m b -> Bool
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)
data Binder a m b
binder'Name :: forall a m b. Lens' (Binder a m b) Text
binder'mkFree :: forall a m b. Lens' (Binder a m b) (Var m a -> m a)
binder'Body :: forall a m b b. Lens (Binder a m b) (Binder a m b) (a -> m b) (a -> m b)
subst :: Binder a m b -> a -> m b
buildBinder :: Var m a -> (a -> m b) -> Binder a m b
bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b)
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)
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]
namesOf :: VarList m a -> [Text]
boxVarList :: VarList m a -> [Box m a]
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)
data BinderList a m b
binderList'Names :: forall a m b. Lens' (BinderList a m b) [Text]
binderList'Body :: forall a m b b. Lens (BinderList a m b) (BinderList a m b) ([a] -> m b) ([a] -> m b)
binderList'mkFree :: forall a m b. Lens' (BinderList a m b) (Var m a -> m a)
binderList'Arity :: Getter (BinderList a m b) Int
substList :: BinderList a m b -> [a] -> m b
eqBinderList :: MonadNumbering m => (b -> b -> m Bool) -> BinderList a m b -> BinderList a m b -> m Bool
bindList :: MonadNumbering m => VarList m a -> Box m b -> Box m (BinderList a m b)
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)

Preliminaries

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

Numbering monad.

Associated Types

type Numbering m :: Type Source #

Methods

numbering :: m (Numbering m) Source #

Variable and Box

data Var m a Source #

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

Instances

Instances details

Show (Var m a) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

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

Instances

Instances details

MonadNumbering m => Applicative (Box m) Source #
Instance details 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 m => Functor (Box m) Source #
Instance details Defined in Data.Binder Methods fmap :: (a -> b) -> Box m a -> Box m b # (<$) :: a -> Box m b -> Box m a #

Variable

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

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

var'mkFree :: Lens' (Var m a) (Var m a -> m a) Source #

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

nameOf :: Var m a -> Text Source #

The name of variable.

boxVar :: Var m a -> Box m a Source #

Smart constructor for Box.

newVar :: MonadNumbering m => Text -> (Var m a -> m a) -> m (Var m a) Source #

Create a new variable with given name.

copyVar :: MonadNumbering m => Var m b -> (Var m a -> m a) -> m (Var m a) Source #

isClosed :: Box m a -> Bool Source #

Box is closed if it exposes no free variables.

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

Check if the variable occurs in the box.

Box

unbox :: forall m a. Monad m => Box m a -> m a Source #

Pick out and complete the construction of a.

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

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

boxApply :: Functor m => (a -> b) -> Box m a -> Box m b Source #

boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c Source #

boxApply3 :: MonadNumbering m => (a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d Source #

boxApply4 :: MonadNumbering m => (a -> b -> c -> d -> e) -> Box m a -> Box m b -> Box m c -> Box m d -> Box m e Source #

boxPair :: MonadNumbering m => Box m a -> Box m b -> Box m (a, b) Source #

boxTriple :: MonadNumbering m => Box m a -> Box m b -> Box m c -> Box m (a, b, c) Source #

boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a) Source #

boxList :: MonadNumbering m => [Box m a] -> Box m [a] Source #

boxJoin :: MonadNumbering m => Box m (m a) -> m (Box m a) Source #

Variable binding

data Binder a m b Source #

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

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

binder'mkFree :: forall a m b. Lens' (Binder a m b) (Var m a -> m a) Source #

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

subst :: Binder a m b -> a -> m b Source #

Variable substitution.

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

Smart constructor for Binder.

bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b) Source #

binding

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

unbinding

unbind2 :: MonadNumbering m => Binder a m b1 -> Binder a m b2 -> m (Var m a, b1, b2) Source #

eqBinder :: MonadNumbering m => (b -> b -> m Bool) -> Binder a m b -> Binder a m b -> m Bool Source #

Check if two bindings are equal.

boxBinder :: MonadNumbering m => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b)) Source #

bindApply :: MonadNumbering m => Box m (Binder a m b) -> Box m a -> m (Box m b) Source #

List

Variable list

type VarList m a = [Var m a] Source #

varList'Keys :: Getter (VarList m a) [Numbering m] Source #

varList'Names :: Getter (VarList m a) [Text] Source #

varList'Boxes :: Getter (VarList m a) [Box m a] Source #

namesOf :: VarList m a -> [Text] Source #

The names of variables.

boxVarList :: VarList m a -> [Box m a] Source #

Smart constructor for a list of Box.

newVarList :: MonadNumbering m => [Text] -> (Var m a -> m a) -> m (VarList m a) Source #

Create new variables with given names.

copyVarList :: MonadNumbering m => VarList m b -> (Var m a -> m a) -> m (VarList m a) Source #

Binder for list

data BinderList a m b Source #

Essentially, BinderList a m b means [a] -> m b.

binderList'Names :: forall a m b. Lens' (BinderList a m b) [Text] Source #

binderList'Body :: forall a m b b. Lens (BinderList a m b) (BinderList a m b) ([a] -> m b) ([a] -> m b) Source #

binderList'mkFree :: forall a m b. Lens' (BinderList a m b) (Var m a -> m a) Source #

binderList'Arity :: Getter (BinderList a m b) Int Source #

substList :: BinderList a m b -> [a] -> m b Source #

Variable substitution.

eqBinderList :: MonadNumbering m => (b -> b -> m Bool) -> BinderList a m b -> BinderList a m b -> m Bool Source #

Check if two bindings are equal.

bindList :: MonadNumbering m => VarList m a -> Box m b -> Box m (BinderList a m b) Source #

binding

unbindList :: MonadNumbering m => BinderList a m b -> m (VarList m a, b) Source #

unbinding

unbind2List :: MonadNumbering m => BinderList a m b1 -> BinderList a m b2 -> m (VarList m a, b1, b2) Source #

boxBinderList :: MonadNumbering m => (b -> m (Box m b)) -> BinderList a m b -> m (Box m (BinderList a m b)) Source #

bindListApply :: MonadNumbering m => Box m (BinderList a m b) -> Box m [a] -> m (Box m b) Source #