packages feed

debruijn (empty) → 0.1

raw patch · 20 files changed

+1456/−0 lines, 20 filesdep +basedep +deepseqdep +fin

Dependencies added: base, deepseq, fin, skew-list, some, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2023, Oleg Grenrus++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Oleg Grenrus nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ debruijn.cabal view
@@ -0,0 +1,86 @@+cabal-version: 2.4+name:          debruijn+version:       0.1+license:       BSD-3-Clause+license-file:  LICENSE+category:      Development+synopsis:      de Bruijn indices and levels+description:+  de Bruijn indices and levels for well-scoped terms.+  .+  This is "unsafe" (as it uses 'unsafeCoerce') implementation, but it's fast.+  The API is the same as in @debruin-safe@ package.++author:        Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:    Oleg Grenrus <oleg.grenrus@iki.fi>+build-type:    Simple+tested-with:   GHC ==9.2.8 || ==9.4.8 || ==9.6.4 || ==9.8.1++source-repository head+  type:     git+  location: https://github.com/phadej/debruijn.git+  subdir:   debruijn++library+  default-language:   Haskell2010+  ghc-options:        -Wall -Wno-unticked-promoted-constructors+  hs-source-dirs:     src src-common++  -- GHC-boot libraries+  build-depends:+    , base          ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0+    , deepseq       ^>=1.4.6.1  || ^>=1.5.0.0+    , transformers  ^>=0.5.6.2  || ^>=0.6.1.0++  -- rest of the dependencies+  build-depends:+    , fin        ^>=0.3+    , skew-list  ^>=0.1+    , some       ^>=1.0.5++  exposed-modules:+    DeBruijn+    DeBruijn.Add+    DeBruijn.Ctx+    DeBruijn.Env+    DeBruijn.Idx+    DeBruijn.Lte+    DeBruijn.Lvl+    DeBruijn.Ren+    DeBruijn.Size+    DeBruijn.Sub+    DeBruijn.Wk++  -- These modules are exported, but shouldn't be used directly.+  exposed-modules:+    DeBruijn.Internal.Add+    DeBruijn.Internal.Env+    DeBruijn.Internal.Idx+    DeBruijn.Internal.Lvl+    DeBruijn.Internal.Size++  other-modules:+    DeBruijn.RenExtras+    TrustworthyCompat++  default-extensions:+    BangPatterns+    DataKinds+    DeriveGeneric+    DeriveTraversable+    DerivingStrategies+    EmptyCase+    FlexibleInstances+    FunctionalDependencies+    GADTs+    OverloadedStrings+    PatternSynonyms+    QuantifiedConstraints+    RankNTypes+    RoleAnnotations+    ScopedTypeVariables+    StandaloneDeriving+    StandaloneKindSignatures+    TypeApplications+    TypeOperators+    ViewPatterns
+ src-common/DeBruijn.hs view
@@ -0,0 +1,38 @@+module DeBruijn (+    -- * Basic building blocks+    -- |+    --+    -- @+    -- data 'Ctx'  :: Kind                   -- contexts+    -- data 'Idx'  :: 'Ctx' -> Type            -- de Bruijn indices+    -- data 'Env'  :: 'Ctx' -> Type -> Type    -- environments+    -- data 'Lvl'  :: 'Ctx' -> Type            -- de Bruijn levels+    -- data 'Size' :: 'Ctx' -> Type            -- context size+    -- @+    --+    module DeBruijn.Ctx,+    module DeBruijn.Idx,+    module DeBruijn.Env,+    module DeBruijn.Lvl,+    module DeBruijn.Size,+    -- * Weakenings, renamings and substitutions+    module DeBruijn.Wk,+    module DeBruijn.Ren,+    module DeBruijn.Sub,+    weakenUsingSize,+    -- * Size addition and less-than-equal predicate+    module DeBruijn.Add,+    -- | Module "DeBruijn.Lte" is not exported,+    -- as it's not that useful in general.+) where++import DeBruijn.Add+import DeBruijn.Ctx+import DeBruijn.Env+import DeBruijn.Idx+import DeBruijn.Lvl+import DeBruijn.Ren+import DeBruijn.RenExtras+import DeBruijn.Size+import DeBruijn.Sub+import DeBruijn.Wk
+ src-common/DeBruijn/Ctx.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Ctx (+    Ctx,+    EmptyCtx,+    S,+    Ctx1, Ctx2, Ctx3, Ctx4, Ctx5, Ctx6, Ctx7, Ctx8, Ctx9,+) where++import Data.Kind (Type)+import Data.Nat  (Nat (..))++-- | Context counts variables, in other words context is just a natural number.+type Ctx :: Type+type Ctx = Nat++-- | Empty context is zero.+type EmptyCtx :: Ctx+type EmptyCtx = Z++-- | And context extension is a successor.+type S :: Ctx -> Ctx+type S = 'S++type Ctx1 = S EmptyCtx+type Ctx2 = S Ctx1+type Ctx3 = S Ctx2+type Ctx4 = S Ctx3+type Ctx5 = S Ctx4+type Ctx6 = S Ctx5+type Ctx7 = S Ctx6+type Ctx8 = S Ctx7+type Ctx9 = S Ctx8
+ src-common/DeBruijn/Lte.hs view
@@ -0,0 +1,17 @@+module DeBruijn.Lte (+    Lte (..),+) where++import Data.Kind (Type)++import DeBruijn.Ctx++-- | @'Lte' 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.+--+type Lte :: Ctx -> Ctx -> Type+type role Lte nominal nominal+data Lte ctx ctx' where+    LZ :: Lte ctx ctx+    LS :: !(Lte ctx ctx') -> Lte ctx (S ctx')
+ src-common/DeBruijn/Ren.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Ren (+    -- * Renamings+    Ren (..),+    renameIdx,+    keepRen,+    skipRen,+    absurdRen,+    wkToRen,+    -- ** Category+    idRen,+    compRen,+    -- * Applicative renamings+    RenA (..),+    renameIdxA,+    keepRenA,+    unusedIdx,+    -- * Renamable things+    IdxMapping (..),+    keepAdd,+    Renamable (..),+    RenamableA (..),+    defaultRename,+    defaultWeaken,+) where++import Data.Functor.Identity (Identity (..))+import Data.Kind             (Constraint, Type)+import Data.Proxy            (Proxy (..))++import DeBruijn.Add+import DeBruijn.Ctx+import DeBruijn.Env+import DeBruijn.Idx+import DeBruijn.Size+import DeBruijn.Wk++import TrustworthyCompat (coerce)++-------------------------------------------------------------------------------+-- 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 @'Size' ctx@.+-- However this isn't an issue, as either there is 'Size' or using 'Wk' is an option.+type Ren :: Ctx -> Ctx -> Type+newtype Ren ctx ctx' = MkRen (Env ctx (Idx ctx'))++-- | Rename de Bruijn index.+renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'+renameIdx (MkRen js) i = lookupEnv i js++-- | Identity renaming.+idRen :: Size ctx -> Ren ctx ctx+idRen s = MkRen $ tabulateEnv s id++-- | Lift renaming (used when going under a binder).+keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')+keepRen (MkRen js) = MkRen (fmap IS js :> IZ)++skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')+skipRen (MkRen js) = MkRen (fmap IS js)++-- | Convert 'Wk' to 'Ren'.+--+-- Note post and precompositions won't need 'Size'.+wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'+wkToRen s      IdWk       = idRen s+wkToRen s      (SkipWk w) = skipRen (wkToRen s w)+wkToRen (SS s) (KeepWk w) = keepRen (wkToRen s w)++-- | Renaming composition.+compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''+compRen (MkRen r) r' = MkRen (fmap (rename r') r)++-- | It's simple to have no indices in any context.+absurdRen :: Ren EmptyCtx ctx+absurdRen = MkRen EmptyEnv++-------------------------------------------------------------------------------+-- Applicative renamings+-------------------------------------------------------------------------------++type RenA :: (Type -> Type) -> Ctx -> Ctx -> Type+newtype RenA f ctx ctx' = MkRenA (Env ctx (f (Idx ctx')))++-- | Lift renaming (used when going under a binder).+keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')+keepRenA (MkRenA js) = MkRenA (fmap (fmap IS) js :> pure IZ)++unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx+unusedIdx s = MkRenA $ tabulateEnv (SS s) $ unIdx Nothing Just++-------------------------------------------------------------------------------+-- Renamable & RenamableA+-------------------------------------------------------------------------------++-- | 'IdxMapping' generalizes over various index mappings, also effectful ones.+type IdxMapping :: (Type -> Type) -> (Ctx -> Ctx -> Type) -> Constraint+class Applicative f => IdxMapping f t | t -> f where+    -- | 'IdxMapping' action.+    mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')++    -- | 'keep' is often called @lift@, but we stick with 'Wk' terminology.+    -- One benefit is that the name 'keep' is less likely to clash.+    keep   :: t ctx ctx' -> t (S ctx) (S 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).+    weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''++-- | 'keep' 'IdxMapping' @arity@ times.+keepAdd+    :: IdxMapping f m+    => Add arity ctxA ctxA'+    -> m ctxA ctxB+    -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)+    -> r+keepAdd AZ     w kont = kont AZ w+keepAdd (AS a) w kont = keepAdd a w $ \a' w' -> kont (AS a') (keep w')++instance IdxMapping Identity Wk where+    keep = KeepWk+    mapIdx w x = Identity (weakenIdx w x)+    weakenIdxMapping = compWk++instance IdxMapping Identity Ren where+    keep = keepRen+    mapIdx w x = Identity (renameIdx w x)+    weakenIdxMapping w (MkRen is) = MkRen (weakenEnv w is)++instance Applicative f => IdxMapping f (RenA f) where+    keep = keepRenA+    mapIdx = renameIdxA+    weakenIdxMapping w (MkRenA is) = MkRenA (weakenEnv w is)++renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')+renameIdxA (MkRenA js) i = lookupEnv i js++-- | 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'+-- @+--+class Renamable t where+    rename :: Ren n m -> t n -> t m+    weaken :: Wk n m -> t n -> t m++-- | 'rename' implementation using 'grename'.+defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m+defaultRename = coerce (grename @t @Ren @Identity @n @m)++-- | 'weaken' implementation using 'grename'.+defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m+defaultWeaken = coerce (grename @t @Wk @Identity @n @m)++-- | Effectful renamings.+--+-- An common example is checking whether a binding is used:+--+-- @+-- Just t' <- 'renameA' 'unusedIdx' t+-- @+--+class Renamable t => RenamableA t where+    renameA :: forall f ctx ctx'. Applicative f => RenA f ctx ctx' -> t ctx -> f (t ctx')+    renameA = grename++    -- | Generic renaming of a term @t@ using any 'IdxMapping'.+    grename :: forall m f ctx ctx'. IdxMapping f m => m ctx ctx' -> t ctx -> f (t ctx')++instance Renamable Proxy where+    rename _ _ = Proxy+    weaken _ _ = Proxy++instance RenamableA Proxy where+    grename _ _ = pure Proxy++instance Renamable Idx where+    rename = renameIdx+    weaken = weakenIdx++instance RenamableA Idx where+    grename = mapIdx++instance Renamable (Ren n) where+    rename r r' = compRen r' r+    weaken w (MkRen js) = MkRen (fmap (weaken w) js)
+ src-common/DeBruijn/Sub.hs view
@@ -0,0 +1,95 @@+module DeBruijn.Sub (+    -- * Substitution+    Sub (..),+    unSub,+    substIdx,+    emptySub,+    snocSub,+    keepSub,+    weakenSub,+    nameMe,+    -- ** Category+    idSub,+    compSub,+    -- * Classes+    Var (..),+    Subst (..),+) where++import Data.Coerce (coerce)+import Data.Kind   (Constraint, Type)+import Data.Proxy  (Proxy (..))++import DeBruijn.Ctx+import DeBruijn.Env+import DeBruijn.Idx+import DeBruijn.Ren+import DeBruijn.Size+import DeBruijn.Wk++-- | Substitutions.+type Sub :: (Ctx -> Type) -> Ctx -> Ctx -> Type+newtype Sub t ctx ctx' = MkSub (Env ctx (t ctx'))++unSub :: Sub t ctx ctx' -> Env ctx (t ctx')+unSub = coerce++-- | Substitute index.+substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx'+substIdx (MkSub ts) i = lookupEnv i ts++-- | Substitution from empty context.+emptySub :: Sub t EmptyCtx ctx'+emptySub = MkSub EmptyEnv++snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'+snocSub (MkSub s) t = MkSub (s :> t)++keepSub :: (Renamable t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')+keepSub (MkSub ts) = MkSub (fmap (weaken wk1) ts :> var IZ)++-- | Precompose 'Sub' with weakening.+weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''+weakenSub w (MkSub ts) = MkSub (weakenEnv w ts)++-- TODO:+nameMe :: Renamable t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''+nameMe (MkSub ts) w = MkSub (fmap (weaken w) ts)++-------------------------------------------------------------------------------+-- Classes+-------------------------------------------------------------------------------++-- | Terms which contain indices as variables.+type Var :: (Ctx -> Type) -> Constraint+class Var t where+    var :: Idx ctx -> t ctx++-- | Terms which we can subsitute into.+type Subst :: (Ctx -> Type) -> Constraint+class Var t => Subst t where+    subst :: Sub t ctx ctx' -> t ctx -> t ctx'++instance Var Proxy where+    var _ = Proxy++instance Subst Proxy where+    subst _ _ = Proxy++instance Var Idx where+    var = id++instance Subst Idx where+    subst = substIdx++-------------------------------------------------------------------------------+-- Category+-------------------------------------------------------------------------------++-- | Identity substitution+idSub :: Var t => Size ctx -> Sub t ctx ctx+idSub s = MkSub $ tabulateEnv s var++-- | Substitution composition.+compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''+compSub (MkSub s) s' = MkSub (fmap (subst s') s)
+ src-common/DeBruijn/Wk.hs view
@@ -0,0 +1,201 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Wk (+    Wk(IdWk, SkipWk, KeepWk),+    -- * Combinators+    wk1,+    compWk,+    -- * Index weakening+    weakenIdx,+    -- * Size weakening+    weakenSize,+    contractSize,+    -- * Environment contraction+    weakenEnv,+    setWeakenEnv,+    overWeakenEnv,+) where++import Data.Kind (Type)++import DeBruijn.Ctx+import DeBruijn.Env+import DeBruijn.Idx+import DeBruijn.Size++-- $setup+-- >>> :set -XGADTs+-- >>> import DeBruijn+-- >>> import Data.Function ((&))+-- >>> import Data.Char (toUpper)++-- | 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 'weakenEnv'.+--+-- 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')+-- @+--+-- However 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 'Wk' ctx ctx' where+--     'IdWk'   :: Wk ctx ctx+--     'KeepWk' :: Wk ctx ctx' -> Wk (S ctx)  (S ctx')+--     'SkipWk' :: Wk ctx ctx' -> Wk    ctx   (S ctx')+-- @+--+-- But we keep an invariant that identity weakenings are always represented by 'IdWk'.+--+-- >>> KeepWk IdWk+-- IdWk+--+-- And 'KeepWk' pattern doesn't match on identity weakenings.+--+-- >>> case IdWk :: Wk Ctx2 Ctx2 of { KeepWk _ -> "keep"; SkipWk _ -> "skip"; IdWk -> "id" } :: String+-- "id"+--+type Wk :: Ctx -> Ctx -> Type+type role Wk nominal nominal+data Wk ctx ctx' where+    IdWk :: Wk ctx ctx+    NeWk :: Wk1 ctx ctx' -> Wk ctx ctx'++type Wk1 :: Ctx -> Ctx -> Type+data Wk1 ctx ctx' where+    Wk1     ::                 Wk1    ctx   (S ctx)+    KeepWk1 :: Wk1 ctx ctx' -> Wk1 (S ctx)  (S ctx')+    SkipWk1 :: Wk1 ctx ctx' -> Wk1    ctx   (S ctx')++deriving instance Eq (Wk ctx ctx')+deriving instance Eq (Wk1 ctx ctx')++-- | Keep variable.+keepWk :: Wk ctx ctx' -> Wk (S ctx) (S ctx')+keepWk IdWk     = IdWk+keepWk (NeWk w) = NeWk (KeepWk1 w)++-- | Skip variable.+skipWk :: Wk ctx ctx' -> Wk ctx (S ctx')+skipWk IdWk     = wk1+skipWk (NeWk w) = NeWk (SkipWk1 w)++viewWk :: Wk ctx ctx' -> ViewWk ctx ctx'+viewWk IdWk               = IdWk'+viewWk (NeWk Wk1)         = SkipWk' IdWk+viewWk (NeWk (SkipWk1 w)) = SkipWk' (NeWk w)+viewWk (NeWk (KeepWk1 w)) = KeepWk' (NeWk w)++type ViewWk :: Ctx -> Ctx -> Type+data ViewWk ctx ctx' where+    IdWk'   :: ViewWk ctx ctx+    SkipWk' :: Wk ctx ctx' -> ViewWk    ctx  (S ctx')+    KeepWk' :: Wk ctx ctx' -> ViewWk (S ctx) (S ctx')++pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b+pattern KeepWk w <- (viewWk -> KeepWk' w)+  where KeepWk w = keepWk w++pattern SkipWk :: () => (b ~ S b') => Wk a b' -> Wk a b+pattern SkipWk w <- (viewWk -> SkipWk' w)+  where SkipWk w = skipWk w++{-# COMPLETE IdWk, SkipWk, KeepWk #-}++instance Show (Wk ctx ctx') where+    showsPrec _ IdWk       = showString "IdWk"+    showsPrec d (KeepWk w) = showParen (d > 10) $ showString "KeepWk " . showsPrec 11 w+    showsPrec d (SkipWk w) = showParen (d > 10) $ showString "SkipWk " . showsPrec 11 w++-- | Weaken by one. @'wk1' = 'SkipWk' 'IdWk'@.+wk1 :: Wk ctx (S ctx)+wk1 = NeWk Wk1++-- | Weakening composition.+compWk :: Wk a b -> Wk b c -> Wk a c+compWk IdWk     w'        = w'+compWk (NeWk w) IdWk      = NeWk w+compWk (NeWk w) (NeWk w') = NeWk (compWk1 w w')++compWk1 :: Wk1  a b -> Wk1 b c -> Wk1 a c+compWk1 w           Wk1          = SkipWk1 w+compWk1 w           (SkipWk1 w') = SkipWk1 (compWk1 w w')+compWk1 Wk1         (KeepWk1 w') = SkipWk1 w'+compWk1 (SkipWk1 w) (KeepWk1 w') = SkipWk1 (compWk1 w w')+compWk1 (KeepWk1 w) (KeepWk1 w') = KeepWk1 (compWk1 w w')++-- | Weaken 'Idx', i.e. map index from smaller to larger context.+weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'+weakenIdx IdWk     x = x+weakenIdx (NeWk w) x = weaken1Idx w x++weaken1Idx :: Wk1 ctx ctx' -> Idx ctx -> Idx ctx'+weaken1Idx Wk1         x      = IS x+weaken1Idx (SkipWk1 w) x      = IS (weaken1Idx w x)+weaken1Idx (KeepWk1 _) IZ     = IZ+weaken1Idx (KeepWk1 w) (IS x) = IS (weaken1Idx w x)++-- | Weaken 'Size'.+weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'+weakenSize IdWk     x = x+weakenSize (NeWk w) x = weaken1Size w x++weaken1Size :: Wk1 ctx ctx' -> Size ctx -> Size ctx'+weaken1Size Wk1         x      = SS x+weaken1Size (SkipWk1 w) x      = SS (weaken1Size w x)+weaken1Size (KeepWk1 w) (SS x) = SS (weaken1Size w x)++contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx+contractSize IdWk     x = x+contractSize (NeWk w) x = contract1Size w x++contract1Size :: Wk1 ctx ctx' -> Size ctx' -> Size ctx+contract1Size Wk1         (SS x) = x+contract1Size (SkipWk1 w) (SS x) = contract1Size w x+contract1Size (KeepWk1 w) (SS x) = SS (contract1Size w x)++-- | Contract 'Env' i.e. drop elements from larger context.+--+-- This function explains the 'KeepWk' and 'SkipWk' constructor names:+--+-- >>> weakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b' :> 'c' :> 'd' :> 'e')+-- EmptyEnv :> 'a' :> 'b' :> 'c' :> 'e'+--+weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a+weakenEnv IdWk     xs = xs+weakenEnv (NeWk w) xs = weaken1Env w xs++weaken1Env :: Wk1 ctx ctx' -> Env ctx' a -> Env ctx a+weaken1Env Wk1         (xs :> _) = xs+weaken1Env (SkipWk1 w) (xs :> _) = weaken1Env w xs+weaken1Env (KeepWk1 w) (xs :> x) = weaken1Env w xs :> x++-- | 'setWeakenEnv' and 'weakenEnv' together form a lens.+--+-- >>> setWeakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b') (EmptyEnv :> 'x' :> 'y' :> 'z')+-- EmptyEnv :> 'a' :> 'y' :> 'b'+--+setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a+setWeakenEnv IdWk     env _    = env+setWeakenEnv (NeWk w) env env' = setWeaken1Env w env env'++-- | Setter made from 'setWeakenEnv' and 'weakenEnv'.+--+-- >>> overWeakenEnv (IdWk & SkipWk & KeepWk) (fmap toUpper) (EmptyEnv :> 'a' :> 'x' :> 'y' :> 'z')+-- EmptyEnv :> 'A' :> 'X' :> 'y' :> 'Z'+--+overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a+overWeakenEnv w f env = setWeakenEnv w (f (weakenEnv w env)) env++setWeaken1Env :: Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a+setWeaken1Env Wk1         xs        (_ :> y)  = xs :> y+setWeaken1Env (SkipWk1 w) xs        (ys :> y) = setWeaken1Env w xs ys :> y+setWeaken1Env (KeepWk1 w) (xs :> x) (ys :> _) = setWeaken1Env w xs ys :> x
+ src-common/TrustworthyCompat.hs view
@@ -0,0 +1,6 @@+{-# LANGUAGE Trustworthy #-}+module TrustworthyCompat (+    coerce,+) where++import Data.Coerce (coerce)
+ src/DeBruijn/Add.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE Trustworthy #-}+module DeBruijn.Add (+    Add (AZ, AS),+    addToInt,+    addToSize,+    adding,+    -- * Lemmas+    rzeroAdd,+    unrzeroAdd,+    lzeroAdd,+    unlzeroAdd,+    rsuccAdd,+    unrsuccAdd,+    lsuccAdd,+    unlsuccAdd,+    swapAdd,+    unswapAdd,+) where++import DeBruijn.Internal.Add
+ src/DeBruijn/Env.hs view
@@ -0,0 +1,9 @@+{-# LANGUAGE Trustworthy #-}+module DeBruijn.Env (+    Env (EmptyEnv, (:>)),+    lookupEnv,+    sizeEnv,+    tabulateEnv,+) where++import DeBruijn.Internal.Env
+ src/DeBruijn/Idx.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE Trustworthy #-}+-- | de Bruijn indices for well-scoped terms.+module DeBruijn.Idx (+    -- * de Bruijn indices+    Idx (IZ, IS),+    absurdIdx,+    unIdx,+    idxToInt,+    -- * Common indices+    pattern I1,+    pattern I2,+    pattern I3,+    pattern I4,+    pattern I5,+    pattern I6,+    pattern I7,+    pattern I8,+    pattern I9,+) where+++import DeBruijn.Internal.Idx
+ src/DeBruijn/Internal/Add.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE Unsafe #-}+module DeBruijn.Internal.Add (+    Add (AZ, AS, UnsafeAdd),+    addToInt,+    addToSize,+    adding,+    -- * Lemmas+    rzeroAdd,+    unrzeroAdd,+    lzeroAdd,+    unlzeroAdd,+    rsuccAdd,+    unrsuccAdd,+    lsuccAdd,+    unlsuccAdd,+    swapAdd,+    unswapAdd,+) where+++import Data.Coerce        (coerce)+import Data.GADT.Show     (GShow (..))+import Data.Kind          (Type)+import Data.Some          (Some (..))+import Data.Type.Equality ((:~:) (Refl))+import Unsafe.Coerce      (unsafeCoerce)++import DeBruijn.Ctx+import DeBruijn.Internal.Size++-- $setup+-- >>> import DeBruijn++-- | @'Add' 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: @'Add' n ctx ctx'@.+--+-- Using a type representing a graph of a type function is often more convenient than defining type-family to begin with.+--+type Add :: Ctx -> Ctx -> Ctx -> Type+type role Add nominal nominal nominal++newtype Add n m p = UnsafeAdd { _addToInt :: Int }++addToInt :: Add n m p -> Int+addToInt = _addToInt++addToSize :: Add n m p -> Size n+addToSize (UnsafeAdd n) = UnsafeSize n++instance Show (Add n m p) where+    showsPrec d a = showsPrec d (addToInt a)++instance GShow (Add n m) where+    gshowsPrec = showsPrec++type ViewAdd :: Ctx -> Ctx -> Ctx -> Type+type role ViewAdd nominal nominal nominal+data ViewAdd n m p where+    AZ' :: ViewAdd EmptyCtx ctx ctx+    AS' :: !(Add n ctx ctx') -> ViewAdd (S n) ctx (S ctx')++viewAdd :: Add n m p -> ViewAdd n m p+viewAdd (UnsafeAdd n)+    | n <= 0    = unsafeCoerce AZ'+    | otherwise = unsafeCoerce (AS' (UnsafeAdd (n - 1)))++pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p+pattern AZ <- (viewAdd -> AZ')+  where AZ = UnsafeAdd 0++pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p+pattern AS a <- (viewAdd -> AS' a)+  where AS a = UnsafeAdd (_addToInt a + 1)++{-# COMPLETE AZ, AS #-}++-- | Add @n@ to some context @ctx@.+--+-- >>> adding (SS (SS SZ))+-- Some 2+--+adding :: Size n -> Some (Add n ctx)+adding (UnsafeSize n) = Some (UnsafeAdd n)++-------------------------------------------------------------------------------+-- Lemmas: zero+-------------------------------------------------------------------------------++-- | @n + 0 ≡ 0@+rzeroAdd :: Size n -> Add n EmptyCtx n+rzeroAdd (UnsafeSize n) = UnsafeAdd n++-- | @n + 0 ≡ m → n ≡ m@+unrzeroAdd :: Add n EmptyCtx m -> n :~: m+unrzeroAdd (UnsafeAdd !_) = unsafeCoerce Refl++-- | @0 + n ≡ 0@+lzeroAdd :: Size n -> Add EmptyCtx n n+lzeroAdd _ = AZ++-- | @0 + n ≡ m → n ≡ m@+unlzeroAdd :: Add EmptyCtx n m -> n :~: m+unlzeroAdd AZ = Refl++-------------------------------------------------------------------------------+-- Lemmas: succ+-------------------------------------------------------------------------------++-- | @n + m ≡ p → n + S m ≡ S p@+rsuccAdd :: Add n m p -> Add n (S m) (S p)+rsuccAdd = coerce++-- | @n + S m ≡ S p → n + m ≡ p@+unrsuccAdd :: Add n (S m) (S p) -> Add n m p+unrsuccAdd = coerce++-- | @n + m ≡ p → S n + m ≡ S p@+lsuccAdd :: Add n m p -> Add (S n) m (S p)+lsuccAdd = AS++-- | @S n + m ≡ S p → n + m ≡ p@+unlsuccAdd :: Add (S n) m (S p) -> Add n m p+unlsuccAdd (AS a)= a++-------------------------------------------------------------------------------+-- Lemmas: swap+-------------------------------------------------------------------------------++-- | @n + S m ≡ p → S n + m ≡ p@+swapAdd :: Add n (S m) p -> Add (S n) m p+swapAdd (UnsafeAdd n) = UnsafeAdd (n + 1)++-- | @S n + m ≡ p → n + S m ≡ p@+unswapAdd :: Add (S n) m p -> Add n (S m) p+unswapAdd (UnsafeAdd n) = UnsafeAdd (n - 1)
+ src/DeBruijn/Internal/Env.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE Unsafe #-}+module DeBruijn.Internal.Env (+    Env (EmptyEnv, (:>), UnsafeEnv),+    lookupEnv,+    sizeEnv,+    tabulateEnv,+) where++import Data.Coerce          (coerce)+import Data.Functor.Reverse (Reverse (..))+import Data.Kind            (Type)+import Data.SkewList.Lazy   (SkewList)+import Unsafe.Coerce        (unsafeCoerce)++import qualified Data.SkewList.Lazy as SL++import DeBruijn.Ctx+import DeBruijn.Internal.Idx+import DeBruijn.Internal.Size++-- $setup+-- >>> import DeBruijn+-- >>> import Data.Foldable (toList)++-------------------------------------------------------------------------------+-- Environment+-------------------------------------------------------------------------------++-- | Environment+--+-- >>> EmptyEnv :> 'a' :> 'b'+-- EmptyEnv :> 'a' :> 'b'+--+type Env :: Ctx -> Type -> Type+type role Env nominal representational+newtype Env ctx a = UnsafeEnv { unEnv :: SkewList a }++-------------------------------------------------------------------------------+-- Pattern synonyms+-------------------------------------------------------------------------------++-- We need a GADT to implement pattern synonyms.+type ViewEnv :: Ctx -> Type -> Type+type role ViewEnv nominal representational+data ViewEnv ctx a where+    EmptyViewEnv :: ViewEnv EmptyCtx a+    (:>>)     :: Env ctx a -> a -> ViewEnv (S ctx) a++viewEnv :: Env ctx a -> ViewEnv ctx a+viewEnv (UnsafeEnv env) = case SL.uncons env of+    Nothing      -> unsafeCoerce EmptyViewEnv+    Just (x, xs) -> unsafeCoerce (UnsafeEnv xs :>> x)++pattern EmptyEnv :: () => (ctx ~ EmptyCtx) => Env ctx a+pattern EmptyEnv <- (viewEnv -> EmptyViewEnv)+  where EmptyEnv = UnsafeEnv SL.Nil++infixl 5 :>+pattern (:>) :: () => (ctx ~ S ctx') => Env ctx' a -> a -> Env ctx a+pattern xs :> x <- (viewEnv -> xs :>> x)+  where xs :> x = UnsafeEnv (SL.cons x (unEnv xs))++{-# COMPLETE EmptyEnv, (:>) #-}++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++deriving instance Functor (Env ctx)++-- |+--+-- >>> toList (tabulateEnv S3 id)+-- [2,1,0]+--+instance Foldable (Env ctx) where+    foldMap f (UnsafeEnv xs) = foldMap f (Reverse xs)++-- |+--+-- >>> traverse print (tabulateEnv S3 id)+-- 2+-- 1+-- 0+-- EmptyEnv :> () :> () :> ()+--+instance Traversable (Env ctx) where+    traverse f (UnsafeEnv xs) = fmap (UnsafeEnv . getReverse) (traverse f (Reverse xs))++instance Show a => Show (Env ctx a) where+    showsPrec d0 (UnsafeEnv xs0) = go d0 xs0 where+        go d ys = case SL.uncons ys of+            Nothing      -> showString "EmptyEnv"+            Just (x, xs) -> showParen (d > 5)+                $ go 5 xs+                . showString " :> "+                . showsPrec 6 x++-------------------------------------------------------------------------------+-- Combinators+-------------------------------------------------------------------------------++-- | Lookup in the context.+--+-- >>> lookupEnv IZ (EmptyEnv :> 'a' :> 'b')+-- 'b'+--+lookupEnv :: Idx ctx -> Env ctx a -> a+lookupEnv (UnsafeIdx i) (UnsafeEnv xs) = xs SL.! i++-- | Size of the environment.+--+-- >>> sizeEnv (EmptyEnv :> 'a' :> 'b')+-- 2+--+sizeEnv :: Env n a -> Size n+sizeEnv (UnsafeEnv xs) = UnsafeSize (length xs)++-- | Create 'Env' by creating elements given an 'Idx'.+--+-- >>> tabulateEnv S4 id+-- EmptyEnv :> 3 :> 2 :> 1 :> 0+--+tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a+tabulateEnv (UnsafeSize s) f = UnsafeEnv $ SL.fromList $ map (coerce f) [0 .. s - 1]
+ src/DeBruijn/Internal/Idx.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE Unsafe #-}+-- | de Bruijn indices for well-scoped terms.+module DeBruijn.Internal.Idx (+    -- * de Bruijn indices+    Idx (IZ, IS, UnsafeIdx),+    absurdIdx,+    unIdx,+    idxToInt,+    -- * Common indices+    pattern I1,+    pattern I2,+    pattern I3,+    pattern I4,+    pattern I5,+    pattern I6,+    pattern I7,+    pattern I8,+    pattern I9,+) where++import Data.Kind    (Type)+import DeBruijn.Ctx++import Unsafe.Coerce (unsafeCoerce)++-------------------------------------------------------------------------------+-- de Bruijn indices+-------------------------------------------------------------------------------++-- | de Bruijn indices.+--+-- >>> IS (IS (IS IZ))+-- 3+--+type Idx :: Ctx -> Type+type role Idx nominal++newtype Idx j = UnsafeIdx { _idxToInt :: Int }++-------------------------------------------------------------------------------+-- Combinators+-------------------------------------------------------------------------------++-- | Convert index to 'Int'.+idxToInt :: Idx ctx -> Int+idxToInt = _idxToInt++-- | Derive anything from index into empty scope.+--+-- Note: don't use @EmptyCase@ on 'Idx' as it doesn't work for unsafe representation.+--+absurdIdx :: Idx EmptyCtx -> a+absurdIdx x = x `seq` error "absurd: Idx Z"++-------------------------------------------------------------------------------+-- Pattern synonyms+-------------------------------------------------------------------------------++-- We need a GADT to implement pattern synonyms.+type ViewIdx :: Ctx -> Type+type role ViewIdx nominal+data ViewIdx n where+    IZ' :: ViewIdx (S n)+    IS' :: Idx n -> ViewIdx (S n)++viewIdx :: Idx n -> ViewIdx n+viewIdx (UnsafeIdx 0) = unsafeCoerce IZ'+viewIdx (UnsafeIdx n) = unsafeCoerce (IS' (UnsafeIdx (n - 1)))++pattern IZ :: () => (m ~ S n) => Idx m+pattern IZ <- (viewIdx -> IZ')+  where IZ = UnsafeIdx 0++pattern IS :: () => (m ~ S n) => Idx n -> Idx m+pattern IS n <- (viewIdx -> IS' n)+  where IS n = UnsafeIdx (idxToInt n + 1)++{-# COMPLETE IZ, IS #-}++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++deriving instance Eq (Idx n)+deriving instance Ord (Idx n)++instance Show (Idx j) where+    showsPrec d = showsPrec d . idxToInt++-------------------------------------------------------------------------------+-- Common Combinators+-------------------------------------------------------------------------------++-- | Case on 'Idx'. (compare to 'maybe').+unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a+unIdx z _ IZ     = z+unIdx _ s (IS x) = s x++pattern I1 :: () => (m ~ S (S n)) => Idx m+pattern I1 = IS IZ++pattern I2 :: () => (m ~ S (S (S n))) => Idx m+pattern I2 = IS I1++pattern I3 :: () => (m ~ S (S (S (S n)))) => Idx m+pattern I3 = IS I2++pattern I4 :: () => (m ~ S (S (S (S (S n))))) => Idx m+pattern I4 = IS I3++pattern I5 :: () => (m ~ S (S (S (S (S (S n)))))) => Idx m+pattern I5 = IS I4++pattern I6 :: () => (m ~ S (S (S (S (S (S (S n))))))) => Idx m+pattern I6 = IS I5++pattern I7 :: () => (m ~ S (S (S (S (S (S (S (S n)))))))) => Idx m+pattern I7 = IS I6++pattern I8 :: () => (m ~ S (S (S (S (S (S (S (S (S n))))))))) => Idx m+pattern I8 = IS I7++pattern I9 :: () => (m ~ S (S (S (S (S (S (S (S (S (S n)))))))))) => Idx m+pattern I9 = IS I8
+ src/DeBruijn/Internal/Lvl.hs view
@@ -0,0 +1,123 @@+{-# LANGUAGE Unsafe #-}+-- | de Bruijn levels for well-scoped terms.+module DeBruijn.Internal.Lvl (+    -- * Levels+    Lvl (UnsafeLvl),+    lvlToIdx,+    idxToLvl,+    lvlZ,+    sinkLvl,+    Sinkable (..),+    sink,+    mapSink,+    sinkSize,+    mapSinkSize,+    sinkAdd,+    mapSinkAdd,+) where++import Data.Coerce   (coerce)+import Data.Kind     (Constraint, Type)+import Data.Proxy    (Proxy (..))+import Unsafe.Coerce (unsafeCoerce)++import DeBruijn.Add+import DeBruijn.Ctx+import DeBruijn.Internal.Idx+import DeBruijn.Internal.Size+import DeBruijn.Lte++-- $setup+-- >>> import DeBruijn+-- >>> import DeBruijn.Lte++-------------------------------------------------------------------------------+-- de Bruijn levels+-------------------------------------------------------------------------------++-- | de Bruijn levels.+type Lvl :: Ctx -> Type+type role Lvl nominal+newtype Lvl ctx = UnsafeLvl { _unLvl :: Int }+  deriving (Eq, Ord)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (Lvl ctx) where+    showsPrec d (UnsafeLvl i) = showsPrec d i++-------------------------------------------------------------------------------+-- Helpers+-------------------------------------------------------------------------------++-- | Convert level to index.+--+-- >>> lvlToIdx S2 (lvlZ S1)+-- 0+--+lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx+lvlToIdx (UnsafeSize ctx) (UnsafeLvl lvl) = UnsafeIdx (ctx - lvl - 1)++idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx+idxToLvl (UnsafeSize ctx) (UnsafeIdx idx) = UnsafeLvl (ctx - idx - 1)++-- | Last level.+--+-- >>> lvlZ S1+-- 1+--+-- >>> lvlZ S5+-- 5+--+lvlZ :: Size ctx -> Lvl (S ctx)+lvlZ (UnsafeSize s) = UnsafeLvl s++-- | Sink 'Lvl' into a larger context.+--+-- >>> sinkLvl (lvlZ S3)+-- 3+--+-- >>> sink (lvlZ S3)+-- 3+--+-- >>> mapLvl (LS LZ) (lvlZ S3)+-- 3+--+sinkLvl :: Lvl n -> Lvl (S n)+sinkLvl = coerce++-------------------------------------------------------------------------------+-- Sinkable+-------------------------------------------------------------------------------++-- | Sinkable terms can be weakened (sunk) cheaply.+type Sinkable :: (Ctx -> Type) -> Constraint+class Sinkable t where+    mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'++instance Sinkable Lvl where mapLvl _ = coerce+instance Sinkable Proxy where mapLvl _ = coerce++-- | Sink term.+sink :: Sinkable t => t ctx -> t (S ctx)+sink = unsafeCoerce++-- | Sink term from empty context to a context of given size.+sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx+sinkSize _ = unsafeCoerce++-- | Essentially @'fmap' 'sink'@+mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))+mapSink = unsafeCoerce++-- | Essentially @'fmap' . 'sinkSize'@+mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)+mapSinkSize _ = unsafeCoerce++sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'+sinkAdd _ = unsafeCoerce++mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')+mapSinkAdd _ = unsafeCoerce
+ src/DeBruijn/Internal/Size.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE Unsafe #-}+module DeBruijn.Internal.Size (+    Size (SZ, SS, UnsafeSize),+    unSS,+    sizeToInt,+    pattern S1,+    pattern S2,+    pattern S3,+    pattern S4,+    pattern S5,+    pattern S6,+    pattern S7,+    pattern S8,+    pattern S9,+) where++import Data.EqP           (EqP (..))+import Data.GADT.Compare  (GCompare (..), GEq (..), GOrdering (..))+import Data.GADT.Show     (GShow (..))+import Data.Kind          (Type)+import Data.OrdP          (OrdP (..))+import Data.Type.Equality (TestEquality (testEquality), (:~:) (Refl))+import Unsafe.Coerce      (unsafeCoerce)++import DeBruijn.Ctx++-- | Term level witness of the size of a context.+--+-- >>> SZ+-- 0+--+-- >>> SS (SS SZ)+-- 2+--+type Size :: Ctx -> Type+type role Size nominal++newtype Size ctx = UnsafeSize { _sizeToInt :: Int }++-------------------------------------------------------------------------------+-- Helpers+-------------------------------------------------------------------------------++-- | Unapply 'SS'. Occasionally more useful than pattern matching.+unSS :: Size (S ctx) -> Size ctx+unSS (SS x) = x++-- | Convert 'Size' to 'Int.+sizeToInt :: Size ctx -> Int+sizeToInt = _sizeToInt++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (Size ctx) where+    showsPrec d (UnsafeSize i) = showsPrec d i++instance GShow Size where+    gshowsPrec = showsPrec++instance Eq (Size ctx) where+    _ == _ = True++instance Ord (Size ctx) where+    compare _ _ = EQ++instance EqP Size where+    eqp (UnsafeSize n) (UnsafeSize m) = n == m++instance OrdP Size where+    comparep (UnsafeSize n) (UnsafeSize m) = compare n m++instance GEq Size where+    geq (UnsafeSize n) (UnsafeSize m) =+        if n == m then Just (unsafeCoerce Refl) else Nothing++instance GCompare Size where+    gcompare (UnsafeSize n) (UnsafeSize m) = case compare n m of+        LT -> GLT+        EQ -> unsafeCoerce GEQ+        GT -> GGT++instance TestEquality Size where+    testEquality = geq++-------------------------------------------------------------------------------+-- Pattern synonyms+-------------------------------------------------------------------------------++-- We need a GADT to implement pattern synonyms.+type ViewSize :: Ctx -> Type+type role ViewSize nominal+data ViewSize ctx where+    SZ' :: ViewSize EmptyCtx+    SS' :: Size n -> ViewSize (S n)++viewSize :: Size n -> ViewSize n+viewSize (UnsafeSize 0) = unsafeCoerce SZ'+viewSize (UnsafeSize n) = unsafeCoerce (SS' (UnsafeSize (n - 1)))++pattern SZ :: () => (m ~ EmptyCtx) => Size m+pattern SZ <- (viewSize -> SZ')+  where SZ = UnsafeSize 0++pattern SS :: () => (m ~ S n) => Size n -> Size m+pattern SS n <- (viewSize -> SS' n)+  where SS n = UnsafeSize (_sizeToInt n + 1)++{-# COMPLETE SZ, SS #-}++-------------------------------------------------------------------------------+-- Sizes+-------------------------------------------------------------------------------++pattern S1 :: () => (m ~ Ctx1) => Size m+pattern S1 = SS SZ++pattern S2 :: () => (m ~ Ctx2) => Size m+pattern S2 = SS S1++pattern S3 :: () => (m ~ Ctx3) => Size m+pattern S3 = SS S2++pattern S4 :: () => (m ~ Ctx4) => Size m+pattern S4 = SS S3++pattern S5 :: () => (m ~ Ctx5) => Size m+pattern S5 = SS S4++pattern S6 :: () => (m ~ Ctx6) => Size m+pattern S6 = SS S5++pattern S7 :: () => (m ~ Ctx7) => Size m+pattern S7 = SS S6++pattern S8 :: () => (m ~ Ctx8) => Size m+pattern S8 = SS S7++pattern S9 :: () => (m ~ Ctx9) => Size m+pattern S9 = SS S8
+ src/DeBruijn/Lvl.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE Trustworthy #-}+module DeBruijn.Lvl (+    Lvl,+    lvlToIdx,+    lvlZ,+    idxToLvl,+    -- * Sinking+    Sinkable (..),+    sink,+    sinkSize,+    sinkAdd,+    mapSink,+    mapSinkSize,+    mapSinkAdd,+) where++import DeBruijn.Internal.Lvl
+ src/DeBruijn/RenExtras.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE Trustworthy #-}+module DeBruijn.RenExtras (+    weakenUsingSize,+) where++import DeBruijn.Ctx+import DeBruijn.Ren+import DeBruijn.Size++import Unsafe.Coerce (unsafeCoerce)++-- | Weaken closed term to arbitrary context.+--+-- Note: this has different requirements than 'sinkSize'.+weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx+weakenUsingSize _ = unsafeCoerce
+ src/DeBruijn/Size.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE Trustworthy #-}+module DeBruijn.Size (+    Size (SZ, SS),+    unSS,+    sizeToInt,+    -- * Common sizes+    pattern S1,+    pattern S2,+    pattern S3,+    pattern S4,+    pattern S5,+    pattern S6,+    pattern S7,+    pattern S8,+    pattern S9,+) where++import DeBruijn.Internal.Size