debruijn-safe-0.1: de Bruijn indices and levels
Safe HaskellSafe
LanguageHaskell2010

DeBruijn.Ren

Synopsis

Renamings

newtype Ren ctx ctx' Source #

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

Instances details
IdxMapping Identity Ren Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

Renamable (Ren n) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

Rename de Bruijn index.

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

Lift renaming (used when going under a binder).

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

absurdRen :: Ren EmptyCtx ctx Source #

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

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

Convert Wk to Ren.

Note post and precompositions won't need Size.

Category

idRen :: Size ctx -> Ren ctx ctx Source #

Identity renaming.

compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx'' Source #

Renaming composition.

Applicative renamings

newtype RenA f ctx ctx' Source #

Constructors

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

Instances

Instances details
Applicative f => IdxMapping f (RenA f) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

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

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

Lift renaming (used when going under a binder).

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

Renamable things

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

IdxMapping generalizes over various index mappings, also effectful ones.

Methods

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

IdxMapping action.

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

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

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

Instances details
IdxMapping Identity Ren Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

IdxMapping Identity Wk Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

Applicative f => IdxMapping f (RenA f) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

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

keep IdxMapping arity times.

class Renamable t where Source #

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 Source #

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

Instances

Instances details
Renamable Idx Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

Renamable (Proxy :: Ctx -> Type) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

Renamable (Ren n) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

class Renamable t => RenamableA t where Source #

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') Source #

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

Generic renaming of a term t using any IdxMapping.

Instances

Instances details
RenamableA Idx Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

RenamableA (Proxy :: Ctx -> Type) Source # 
Instance details

Defined in DeBruijn.Ren

Methods

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

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

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

rename implementation using grename.

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

weaken implementation using grename.