h**&5      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz { | } ~                                                   0.1Safe"()*169:;< debruijn%And context extension is a successor. debruijnEmpty context is zero. debruijnContext counts variables, in other words context is just a natural number.  Unsafe"()*169:;< debruijnde Bruijn indices.IS (IS (IS IZ))3debruijnConvert index to .debruijn,Derive anything from index into empty scope.Note: don't use  EmptyCase on  . as it doesn't work for unsafe representation.debruijnCase on  . (compare to ).      Trustworthy"()*169:;<  Unsafe"()*169:;<?debruijn,Term level witness of the size of a context.SZ0 SS (SS SZ)2,debruijnUnapply *1. Occasionally more useful than pattern matching.-debruijnConvert  to 'Int.+* ,-)('&%$#"!+* +*,-)('&%$#"!Unsafe"()*169:;< 7debruijn EnvironmentEmptyEnv :> 'a' :> 'b'EmptyEnv :> 'a' :> 'b';debruijnLookup in the context.%lookupEnv IZ (EmptyEnv :> 'a' :> 'b')'b'<debruijnSize of the environment. sizeEnv (EmptyEnv :> 'a' :> 'b')2=debruijnCreate 7 by creating elements given an  .tabulateEnv S4 idEmptyEnv :> 3 :> 2 :> 1 :> 0?debruijn"traverse print (tabulateEnv S3 id)210EmptyEnv :> () :> () :> ()@debruijntoList (tabulateEnv S3 id)[2,1,0]7:98;<= 7:98:9;<=95 Trustworthy"()*169:;< 7:9;<=7:9:9;<=Unsafe"()*169:;< Y BdebruijnB n m p is an evidence that  n + m = p.Useful when you have an arity n$ thing and need to extend a context ctx with: B n ctx ctx'.Using a type representing a graph of a type function is often more convenient than defining type-family to begin with.HdebruijnAdd n to some context ctx.adding (SS (SS SZ))Some 2Idebruijn  n + 0 D 0Jdebruijn n + 0 D m C n D mKdebruijn  0 + n D 0Ldebruijn 0 + n D m C n D mMdebruijn n + m D p C n + S m D S pNdebruijn n + S m D S p C n + m D pOdebruijn n + m D p C S n + m D S pPdebruijn S n + m D S p C n + m D pQdebruijn n + S m D p C S n + m D pRdebruijn S n + m D p C n + S m D pBEDCFGHIJKLMNOPQRBEDCEDFGHIJKLMNOPQR Trustworthy"()*169:;< BEDFGHIJKLMNOPQRBEDEDFGHIJKLMNOPQR Safe-Inferred"()*169:;<(UdebruijnU ctx ctx' is evidence that ctx' is smaller than of ctx, less-than-or-equal, and produced by simple skipping only, i.e. nothing is inserted into ctx, only appended to the end.UVWUVWUnsafe"()*169:;< Xdebruijn.Sinkable terms can be weakened (sunk) cheaply.Zdebruijnde Bruijn levels.\debruijnConvert level to index.lvlToIdx S2 (lvlZ S1)0^debruijn Last level.lvlZ S11lvlZ S55_debruijnSink Z into a larger context.sinkLvl (lvlZ S3)3sink (lvlZ S3)3mapLvl (LS LZ) (lvlZ S3)3`debruijn Sink term.adebruijn8Sink term from empty context to a context of given size.bdebruijn Essentially  `cdebruijn Essentially  . aZ[\]^_XY`bacdeZ[\]^_XY`bacde Trustworthy"()*169:;< Z\^]XY`adbce Z\^]XY`adbce Trustworthy"()*169:;<W+*,-)('&%$#"!+*+*,-)('&%$#"!Safe"()*169:;<M kdebruijn(Weakenings, order preserving embeddings.Wk n m could be represented as m bit field with popCount of n.Constructor names make sense when you look at the implementation of t.#Note: usually 'ViewWk is defined as data Wk ctx ctx' where WkNil :: Wk EmptyCtx EmptyCtx KeepWk :: Wk ctx ctx' -> Wk (S ctx) (S ctx') SkipWk :: Wk ctx ctx' -> Wk ctx (S ctx') 2However that representation doesn't allow to make wkId :: 'ViewWk ctx ctx without knowing the size of context. Therefore we morally use a representation closer to data k ctx ctx' where l :: Wk ctx ctx n, :: Wk ctx ctx' -> Wk (S ctx) (S ctx') m( :: Wk ctx ctx' -> Wk ctx (S ctx') But we keep an invariant that identity weakenings are always represented by l. KeepWk IdWkIdWkAnd n. pattern doesn't match on identity weakenings.case IdWk :: Wk Ctx2 Ctx2 of { KeepWk _ -> "keep"; SkipWk _ -> "skip"; IdWk -> "id" } :: String"id"debruijnKeep variable.debruijnSkip variable.odebruijnWeaken by one. o = m l.pdebruijnWeakening composition.qdebruijnWeaken  0, i.e. map index from smaller to larger context.rdebruijnWeaken .tdebruijn Contract 7( i.e. drop elements from larger context.This function explains the n and m constructor names:weakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b' :> 'c' :> 'd' :> 'e')$EmptyEnv :> 'a' :> 'b' :> 'c' :> 'e'udebruijnu and t together form a lens.setWeakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b') (EmptyEnv :> 'x' :> 'y' :> 'z')EmptyEnv :> 'a' :> 'y' :> 'b'vdebruijnSetter made from u and t.overWeakenEnv (IdWk & SkipWk & KeepWk) (fmap toUpper) (EmptyEnv :> 'a' :> 'x' :> 'y' :> 'z')$EmptyEnv :> 'A' :> 'X' :> 'y' :> 'Z' klmnopqrstuvklmnmnopqrstuv Trustworthy"()*169:;< Safe"()*169:;<"zdebruijnEffectful renamings.8An common example is checking whether a binding is used:  Just t' <- {  t |debruijnGeneric renaming of a term t using any .}debruijnRenamable things.For most terms it's enough to define a single traversal: an instance of z type-class, and then define } as:  instance } Term where ~ = ;  =  debruijn> generalizes over various index mappings, also effectful ones.debruijn action.debruijn is often called lift, but we stick with k, terminology. One benefit is that the name  is less likely to clash.debruijn(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).debruijn,Renamings are mappings of de Bruijn indices.$One possible representation is just Idx ctx -> Idx ctx' , but using 7> makes this representation inspectable and (hopefully) makes  perform better.On the other hand,  requires  ctx3. However this isn't an issue, as either there is  or using k is an option.debruijnRename de Bruijn index.debruijnIdentity renaming.debruijn/Lift renaming (used when going under a binder).debruijnConvert k to .)Note post and precompositions won't need .debruijnRenaming composition.debruijn.It's simple to have no indices in any context.debruijn/Lift renaming (used when going under a binder).debruijn  arity times.debruijn~ implementation using |.debruijn implementation using |.}~z|{}~z|{  Safe-Inferred"()*169:;<$-debruijn"Terms which we can subsitute into.debruijn)Terms which contain indices as variables.debruijnSubstitutions.debruijnSubstitute index.debruijn Substitution from empty context.debruijn Precompose  with weakening.debruijnIdentity substitutiondebruijnSubstitution composition. Trustworthy"()*169:;<%1debruijn(Weaken closed term to arbitrary context.+Note: this has different requirements than sinkSize.  Safe-Inferred"()*169:;<%  79:;<=ZXY\^]`adbce+*)('&%$#"!,-klmnopqrstuv}~z|{BEDFGHIJKLMNOPQR !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                      #debruijn-0.1-JbU4uPwmnro6kPsL9abtLP DeBruijn.CtxDeBruijn.Internal.IdxDeBruijn.Internal.SizeDeBruijn.Internal.EnvDeBruijn.Internal.Add DeBruijn.LteDeBruijn.Internal.Lvl DeBruijn.Wk DeBruijn.Ren DeBruijn.SubDeBruijndebruijn DeBruijn.Idx DeBruijn.Env DeBruijn.Add DeBruijn.Lvl DeBruijn.SizeTrustworthyCompatDeBruijn.RenExtrasCtx9Ctx8Ctx7Ctx6Ctx5Ctx4Ctx3Ctx2Ctx1SEmptyCtxCtxIdx UnsafeIdxI9I8I7I6I5I4I3I2I1ISIZidxToInt absurdIdxunIdx $fShowIdx$fOrdIdx$fEqIdxSize UnsafeSizeS9S8S7S6S5S4S3S2S1SSSZunSS sizeToInt$fTestEqualityNatSize$fGCompareNatSize $fGEqNatSize $fOrdPNatSize $fEqPNatSize $fOrdSize$fEqSize$fGShowNatSize $fShowSizeEnv UnsafeEnv:>EmptyEnv lookupEnvsizeEnv tabulateEnv $fShowEnv$fTraversableEnv $fFoldableEnv $fFunctorEnvAdd UnsafeAddASAZaddToInt addToSizeaddingrzeroAdd unrzeroAddlzeroAdd unlzeroAddrsuccAdd unrsuccAddlsuccAdd unlsuccAddswapAdd unswapAdd $fGShowNatAdd $fShowAddLteLZLSSinkablemapLvlLvl UnsafeLvllvlToIdxidxToLvllvlZsinkLvlsinksinkSizemapSink mapSinkSizesinkAdd mapSinkAdd $fShowLvl$fSinkableProxy $fSinkableLvl$fEqLvl$fOrdLvlWkIdWkSkipWkKeepWkwk1compWk weakenIdx weakenSize contractSize weakenEnv setWeakenEnv overWeakenEnv$fShowWk$fEqWk1$fEqWk RenamableArenameAgrename Renamablerenameweaken IdxMappingmapIdxkeepweakenIdxMappingRenAMkRenARenMkRen renameIdxidRenkeepRenskipRenwkToRencompRen absurdRenkeepRenA unusedIdxkeepAdd renameIdxA defaultRename defaultWeaken$fIdxMappingfRenA$fIdxMappingIdentityRen$fIdxMappingIdentityWk$fRenamableRen$fRenamableIdx$fRenamableProxy$fRenamableAIdx$fRenamableAProxySubstsubstVarvarSubMkSubunSubsubstIdxemptySubsnocSubkeepSub weakenSubnameMeidSubcompSub$fVarIdx $fVarProxy $fSubstIdx $fSubstProxyweakenUsingSizeghc-prim GHC.TypesIntbase Data.MaybemaybeGHC.BasefmapkeepWkskipWkGHC.Primcoerce