Safe Haskell	Safe
Language	Haskell2010

DeBruijn.Ren

Contents

Renamings
- Category
Applicative renamings
Renamable things

Synopsis

newtype Ren ctx ctx' = MkRen (Env ctx (Idx ctx'))
renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'
keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')
skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')
absurdRen :: Ren EmptyCtx ctx
wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
idRen :: Size ctx -> Ren ctx ctx
compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
newtype RenA f ctx ctx' = MkRenA (Env ctx (f (Idx ctx')))
renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx
class Applicative f => IdxMapping f t | t -> f where
- mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')
- keep :: t ctx ctx' -> t (S ctx) (S ctx')
- weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''
keepAdd :: IdxMapping f m => Add arity ctxA ctxA' -> m ctxA ctxB -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r) -> r
class Renamable t where
- rename :: Ren n m -> t n -> t m
- weaken :: Wk n m -> t n -> t m
class Renamable t => RenamableA t where
- 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')
defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m
defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m

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.

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.

Renamings

Instances

Category

Applicative renamings

Instances

Renamable things

Instances

Instances

Instances