abt-0.1.0.1: Abstract binding trees for Haskell

Safe HaskellNone
LanguageHaskell2010

Abt.Concrete.LocallyNameless

Synopsis

Documentation

data Tm o n where Source

Locally nameless terms with operators in o at order n.

Constructors

Free :: Var -> Tm0 o 
Bound :: Int -> Tm0 o 
Abs :: Tm o n -> Tm o (S n) 
App :: o ns -> Rec (Tm o) ns -> Tm0 o 

Instances

Show1 [Nat] o => Abt Var o (Tm o) 
HEq1 [Nat] o => HEq1 Nat (Tm o) 

type Tm0 o = Tm o Z Source

First order terms (i.e. terms not headed by abstractions).

data Var Source

A variable is a De Bruijn index, optionally decorated with a display name.

Constructors

Var 

Fields

_varName :: !(Maybe String)
 
_varIndex :: !Int
 

Instances

Eq Var 
Ord Var 
Show Var 
MonadVar Var M

Check out the source to see fresh variable generation.

Show1 [Nat] o => Abt Var o (Tm o) 
MonadVar Var m => MonadVar Var (StepT m) 

varName :: Functor f => (Maybe String -> f (Maybe String)) -> Var -> f Var Source

A lens for _varName.

varName ∷ Lens' Var (Maybe String)

varIndex :: Functor f => (Int -> f Int) -> Var -> f Var Source

A lens for _varIndex.

varIndex ∷ Lens' Var Int