DeBruijn.Ren

Renamings

newtype Ren ctx ctx'

Renamings are mappings of de Bruijn indices.

One possible representation is just Idx ctx -> Idx ctx', but using Env makes this representation inspectable and (hopefully) makes renameIdx perform better.

On the other hand, idRen requires Size ctx. However this isn't an issue, as either there is Size or using Wk is an option.

Constructors

MkRen (Env ctx (Idx ctx'))

Instances

IdxMapping Identity Ren

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Idx ctx -> Identity (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''

Renamable (Ren n)

Defined in DeBruijn.Ren

Methods

rename :: forall (n0 :: Ctx) (m :: Ctx). Ren n0 m -> Ren n n0 -> Ren n m

weaken :: forall (n0 :: Ctx) (m :: Ctx). Wk n0 m -> Ren n n0 -> Ren n m

renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'

Rename de Bruijn index.

keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')

Lift renaming (used when going under a binder).

skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')

absurdRen :: Ren EmptyCtx ctx

It's simple to have no indices in any context.

wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'

Convert Wk to Ren.

Note post and precompositions won't need Size.

Category

idRen :: Size ctx -> Ren ctx ctx

Identity renaming.

compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''

Renaming composition.

Applicative renamings

newtype RenA f ctx ctx'

Constructors

MkRenA (Env ctx (f (Idx ctx')))

Instances

Applicative f => IdxMapping f (RenA f)

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). RenA f ctx ctx' -> RenA f (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> RenA f ctx' ctx'' -> RenA f ctx ctx''

renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')

keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')

Lift renaming (used when going under a binder).

unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx

Renamable things

class Applicative f => IdxMapping f t | t -> f where

IdxMapping generalizes over various index mappings, also effectful ones.

Methods

mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')

IdxMapping action.

keep :: t ctx ctx' -> t (S ctx) (S ctx')

keep is often called lift, but we stick with Wk terminology. One benefit is that the name keep is less likely to clash.

weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''

Compose weakening with an index mapping.

This is useful when you have explicit weakening in your terms. (a similar idea as in bound's Scope possibly lifting whole term).

Instances

IdxMapping Identity Ren

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Idx ctx -> Identity (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''

IdxMapping Identity Wk

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Idx ctx -> Identity (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Wk (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx''

Applicative f => IdxMapping f (RenA f)

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). RenA f ctx ctx' -> RenA f (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> RenA f ctx' ctx'' -> RenA f ctx ctx''

keepAdd :: IdxMapping f m => Add arity ctxA ctxA' -> m ctxA ctxB -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r) -> r

keep IdxMapping arity times.

class Renamable t where

Renamable things.

For most terms it's enough to define a single traversal: an instance of RenamableA type-class, and then define Renamable as:

instance Renamable Term where rename = defaultRename; weaken = defaultWeaken

Methods

rename :: Ren n m -> t n -> t m

weaken :: Wk n m -> t n -> t m

Instances

Renamable Idx

Defined in DeBruijn.Ren

Methods

rename :: forall (n :: Ctx) (m :: Ctx). Ren n m -> Idx n -> Idx m

weaken :: forall (n :: Ctx) (m :: Ctx). Wk n m -> Idx n -> Idx m

Renamable (Proxy :: Ctx -> Type)

Defined in DeBruijn.Ren

Methods

rename :: forall (n :: Ctx) (m :: Ctx). Ren n m -> Proxy n -> Proxy m

weaken :: forall (n :: Ctx) (m :: Ctx). Wk n m -> Proxy n -> Proxy m

Renamable (Ren n)

Defined in DeBruijn.Ren

Methods

rename :: forall (n0 :: Ctx) (m :: Ctx). Ren n0 m -> Ren n n0 -> Ren n m

weaken :: forall (n0 :: Ctx) (m :: Ctx). Wk n0 m -> Ren n n0 -> Ren n m

class Renamable t => RenamableA t where

Effectful renamings.

An common example is checking whether a binding is used:

Just t' <- renameA unusedIdx t

Minimal complete definition

grename

Methods

renameA :: forall f ctx ctx'. Applicative f => RenA f ctx ctx' -> t ctx -> f (t ctx')

grename :: forall m f ctx ctx'. IdxMapping f m => m ctx ctx' -> t ctx -> f (t ctx')

Generic renaming of a term t using any IdxMapping.

Instances

RenamableA Idx

Defined in DeBruijn.Ren

Methods

renameA :: forall f (ctx :: Ctx) (ctx' :: Ctx). Applicative f => RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')

grename :: forall m f (ctx :: Ctx) (ctx' :: Ctx). IdxMapping f m => m ctx ctx' -> Idx ctx -> f (Idx ctx')

RenamableA (Proxy :: Ctx -> Type)

Defined in DeBruijn.Ren

Methods

renameA :: forall f (ctx :: Ctx) (ctx' :: Ctx). Applicative f => RenA f ctx ctx' -> Proxy ctx -> f (Proxy ctx')

grename :: forall m f (ctx :: Ctx) (ctx' :: Ctx). IdxMapping f m => m ctx ctx' -> Proxy ctx -> f (Proxy ctx')

defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m

rename implementation using grename.

defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m

weaken implementation using grename.