Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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
- 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
- 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
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
.
However this isn't an issue, as either there is Size
ctxSize
or using Wk
is an option.
Instances
IdxMapping Identity Ren Source # | |
Defined in DeBruijn.Ren 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 # | |
keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx') Source #
Lift renaming (used when going under a binder).
Category
Applicative renamings
newtype RenA f ctx ctx' Source #
Instances
Applicative f => IdxMapping f (RenA f) Source # | |
Defined in DeBruijn.Ren 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 # |
keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx') Source #
Lift renaming (used when going under a binder).
Renamable things
class Applicative f => IdxMapping f t | t -> f where Source #
IdxMapping
generalizes over various index mappings, also effectful ones.
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
IdxMapping Identity Ren Source # | |
Defined in DeBruijn.Ren 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 # | |
Defined in DeBruijn.Ren 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 # | |
Defined in DeBruijn.Ren 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:
instanceRenamable
Term whererename
=defaultRename
;weaken
=defaultWeaken
class Renamable t => RenamableA t where Source #
Effectful renamings.
An common example is checking whether a binding is used:
Just t' <-renameA
unusedIdx
t
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
RenamableA Idx Source # | |
RenamableA (Proxy :: Ctx -> Type) Source # | |
defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m Source #
defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m Source #