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''

Rename (Ren n)

Defined in DeBruijn.Ren

Methods

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

Weaken (Ren n)

Defined in DeBruijn.Ren

Methods

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

Renameble 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 Weaken t where

Renameble things.

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

instance Renameble Term where rename = defaultRename; weaken = defaultWeaken

Methods

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

Instances

Weaken Idx

Defined in DeBruijn.Ren

Methods

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

Weaken (Proxy :: Ctx -> Type)

Defined in DeBruijn.Ren

Methods

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

Weaken (Ren n)

Defined in DeBruijn.Ren

Methods

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

class Weaken t => Rename t where

Methods

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

Instances

Rename Idx

Defined in DeBruijn.Ren

Methods

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

Rename (Proxy :: Ctx -> Type)

Defined in DeBruijn.Ren

Methods

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

Rename (Ren n)

Defined in DeBruijn.Ren

Methods

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

class Rename t => RenameA 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

RenameA 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')

RenameA (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. RenameA t => Ren n m -> t n -> t m

rename implementation using grename.

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

weaken implementation using grename.