Abt.Concrete.LocallyNameless

Documentation

data Tm o n where

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)

Typeable (([Nat] -> *) -> Nat -> *) Tm

type Tm0 o = Tm o Z

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

_TmOp :: (Choice p, Applicative f, HEq1 o) => o ns -> p (Rec (Tm o) ns) (f (Rec (Tm o) ns)) -> p (Tm0 o) (f (Tm0 o))

A prism to extract arguments from a proposed operator.

_TmOp ∷ HEq1 o ⇒ o ns → Prism' (Tm0 o) (Rec (Tm0 o) ns)

data Var

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

Typeable * 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 (JudgeT m)

MonadVar Var m => MonadVar Var (StepT m)

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

A lens for _varName.

varName ∷ Lens' Var (Maybe String)

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

A lens for _varIndex.

varIndex ∷ Lens' Var Int