packages feed

debruijn-safe (empty) → 0.1

raw patch · 15 files changed

+1278/−0 lines, 15 filesdep +basedep +deepseqdep +fin

Dependencies added: base, deepseq, fin, some

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-safe.cabal view
@@ -0,0 +1,75 @@+cabal-version: 2.4+name:          debruijn-safe+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 "safe", but slow implementation.++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-safe++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++  -- rest of the dependencies+  build-depends:+    , fin   ^>=0.3+    , 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++  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,123 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Add (+    Add (AZ, AS),+    addToInt,+    addToSize,+    adding,+    -- * Lemmas+    rzeroAdd,+    unrzeroAdd,+    lzeroAdd,+    unlzeroAdd,+    rsuccAdd,+    unrsuccAdd,+    lsuccAdd,+    unlsuccAdd,+    swapAdd,+    unswapAdd,+) where++import Data.GADT.Show     (GShow (..))+import Data.Kind          (Type)+import Data.Some          (Some (..))+import Data.Type.Equality ((:~:) (..))++import DeBruijn.Ctx+import DeBruijn.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+data Add n m p where+    AZ :: Add EmptyCtx ctx ctx+    AS :: !(Add n ctx ctx') -> Add (S n) ctx (S ctx')++addToInt :: Add n m p -> Int+addToInt = go 0 where+    go :: Int -> Add n m p -> Int+    go !n AZ     = n+    go !n (AS a) = go (n + 1) a++addToSize :: Add n m p -> Size n+addToSize AZ     = SZ+addToSize (AS a) = SS (addToSize a)++instance Show (Add n m p) where+    showsPrec d a = showsPrec d (addToInt a)++instance GShow (Add n m) where+    gshowsPrec = showsPrec++-- | Add @n@ to some context @ctx@.+--+-- >>> adding (SS (SS SZ))+-- Some 2+--+adding :: Size n -> Some (Add n ctx)+adding SZ     = Some AZ+adding (SS s) = case adding s of Some a -> Some (AS a)++-------------------------------------------------------------------------------+-- Lemmas: zero+-------------------------------------------------------------------------------++-- | @n + 0 ≡ 0@+rzeroAdd :: Size n -> Add n EmptyCtx n+rzeroAdd SZ     = AZ+rzeroAdd (SS s) = AS (rzeroAdd s)++-- | @n + 0 ≡ m → n ≡ m@+unrzeroAdd :: Add n EmptyCtx m -> n :~: m+unrzeroAdd AZ     = Refl+unrzeroAdd (AS a) = case unrzeroAdd a of Refl -> 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 AZ     = AZ+rsuccAdd (AS a) = AS $ rsuccAdd a++-- | @n + S m ≡ S p → n + m ≡ p@+unrsuccAdd :: Add n (S m) (S p) -> Add n m p+unrsuccAdd AZ     = AZ+unrsuccAdd (AS a) = swapAdd a++-- | @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 AZ     = AS AZ+swapAdd (AS a) = AS $ swapAdd a++-- | @S n + m ≡ p → n + S m ≡ p@+unswapAdd :: Add (S n) m p -> Add n (S m) p+unswapAdd (AS a) = rsuccAdd a
+ src/DeBruijn/Env.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Env (+    Env (EmptyEnv, (:>)),+    lookupEnv,+    sizeEnv,+    tabulateEnv,+) where++import Data.Kind (Type)++import DeBruijn.Ctx+import DeBruijn.Idx+import DeBruijn.Size++-- $setup+-- >>> import DeBruijn+-- >>> import Data.Foldable (toList)++-------------------------------------------------------------------------------+-- Environment+-------------------------------------------------------------------------------++-- | Environment+--+-- >>> EmptyEnv :> 'a' :> 'b'+-- EmptyEnv :> 'a' :> 'b'+--+type Env :: Ctx -> Type -> Type+data Env ctx a where+    EmptyEnv :: Env EmptyCtx a+    (:>)     :: Env ctx a -> a -> Env (S ctx) a++infixl 5 :>++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++deriving instance Functor (Env ctx)++-- |+--+-- >>> toList (tabulateEnv S3 id)+-- [2,1,0]+--+deriving instance Foldable (Env ctx)++-- |+--+-- >>> traverse print (tabulateEnv S3 id)+-- 2+-- 1+-- 0+-- EmptyEnv :> () :> () :> ()+--+deriving instance Traversable (Env ctx)++instance Show a => Show (Env ctx a) where+    showsPrec _ EmptyEnv = showString "EmptyEnv"+    showsPrec d (xs :> x) = showParen (d > 5)+        $ showsPrec 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 IZ     (_  :> x)  = x+lookupEnv (IS n) (xs :> _) = lookupEnv n xs++-- | Size of the environment.+--+-- >>> sizeEnv (EmptyEnv :> 'a' :> 'b')+-- 2+--+sizeEnv :: Env n a -> Size n+sizeEnv EmptyEnv  = SZ+sizeEnv (xs :> _) = SS (sizeEnv xs)++tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a+tabulateEnv SZ     _ = EmptyEnv+tabulateEnv (SS s) f = tabulateEnv s (f . IS) :> f IZ
+ src/DeBruijn/Idx.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE Safe #-}+-- | 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 Data.Kind    (Type)+import DeBruijn.Ctx++-------------------------------------------------------------------------------+-- de Bruijn indices+-------------------------------------------------------------------------------++-- | de Bruijn indices.+--+-- >>> IS (IS (IS IZ))+-- 3+--+type Idx :: Ctx -> Type+type role Idx nominal++data Idx n where+    IZ :: Idx (S n)+    IS :: !(Idx n) -> Idx (S n)++-------------------------------------------------------------------------------+-- Combinators+-------------------------------------------------------------------------------++-- | Convert index to 'Int'.+idxToInt :: Idx n -> Int+idxToInt = go 0 where+    go :: Int -> Idx j -> Int+    go !acc IZ = acc+    go acc (IS n) = go (acc + 1) n++-- | Derive anything from index into empty scope.+--+-- Note: don't use @EmptyCase@ as it doesn't work for unsafe representation.+absurdIdx :: Idx EmptyCtx -> a+absurdIdx x = x `seq` error "absurd: Idx Z"++-------------------------------------------------------------------------------+-- 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/Lvl.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Lvl (+    Lvl,+    lvlToIdx,+    lvlZ,+    sinkLvl,+    Sinkable (..),+    sink,+    mapSink,+    sinkSize,+    mapSinkSize,+    sinkAdd,+    mapSinkAdd,+) where++import Data.Kind (Constraint, Type)++import DeBruijn.Add+import DeBruijn.Ctx+import DeBruijn.Idx+import DeBruijn.Lte+import DeBruijn.Size++-- $setup+-- >>> import DeBruijn+-- >>> import DeBruijn.Lte++-------------------------------------------------------------------------------+-- de Bruijn levels+-------------------------------------------------------------------------------++-- | de Bruijn levels.+--+--+type Lvl :: Ctx -> Type+type role Lvl nominal+data Lvl ctx = MkLvl !Int !(Idx ctx)+  deriving (Eq, Ord)++-- Note: we need an integer field for Show instance.++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (Lvl ctx) where+    showsPrec d (MkLvl i _) = showsPrec d i++-------------------------------------------------------------------------------+-- Helpers+-------------------------------------------------------------------------------++-- | Convert level to index.+--+-- >>> lvlToIdx S2 (lvlZ S1)+-- 0+--+lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx+lvlToIdx _ (MkLvl _ x) = x++-- | Last level.+--+-- >>> lvlZ S1+-- 1+--+-- >>> lvlZ S5+-- 5+--+lvlZ :: Size ctx -> Lvl (S ctx)+lvlZ s = MkLvl (sizeToInt s) IZ++-- | Sink 'Lvl' into a larger context.+--+-- >>> sinkLvl (lvlZ S3)+-- 3+--+-- >>> sink (lvlZ S3)+-- 3+--+-- >>> mapLvl (LS LZ) (lvlZ S3)+-- 3+--+--+sinkLvl :: Lvl ctx -> Lvl (S ctx)+sinkLvl (MkLvl s i) = MkLvl s (IS i)++-------------------------------------------------------------------------------+-- Sinkable+-------------------------------------------------------------------------------++-- | Sinkable terms can be weakened (sunk) cheaply.+-- (when 'Lvl' is implemented as newtype over 'Int').+type Sinkable :: (Ctx -> Type) -> Constraint+class Sinkable t where+    mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'++lteLvl :: Lte ctx ctx' -> Lvl ctx -> Lvl ctx'+lteLvl LZ     t           = t+lteLvl (LS l) (MkLvl s i) = MkLvl s (lteIdx (LS l) i)++lteIdx :: Lte ctx ctx' -> Idx ctx -> Idx ctx'+lteIdx LZ     i = i+lteIdx (LS s) i = IS (lteIdx s i)++instance Sinkable Lvl where mapLvl = lteLvl++sink :: Sinkable t => t ctx -> t (S ctx)+sink = mapLvl (LS LZ)++mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))+mapSink = fmap sink++sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx+sinkSize SZ     t = t+sinkSize (SS n) t = sink (sinkSize n t)++mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)+mapSinkSize = fmap . sinkSize++sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'+sinkAdd AZ t = t+sinkAdd (AS s) t = sink (sinkAdd s t)++mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')+mapSinkAdd = fmap . sinkAdd
+ src/DeBruijn/RenExtras.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE Safe #-}+module DeBruijn.RenExtras (+    weakenUsingSize,+) where++import DeBruijn.Ctx+import DeBruijn.Ren+import DeBruijn.Size+import DeBruijn.Wk++-- | Weaken closed term to arbitrary context.+--+-- Note: this has different requirements than 'sinkSize'.+weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx+weakenUsingSize s0 = weaken (go s0) where+    go :: Size ctx -> Wk EmptyCtx ctx+    go SZ     = IdWk+    go (SS s) = SkipWk (go s)
+ src/DeBruijn/Size.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE Safe #-}+module DeBruijn.Size (+    Size (SZ, SS),+    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 (..), defaultCompare, defaultEq)+import Data.GADT.Show     (GShow (..))+import Data.Kind          (Type)+import Data.OrdP          (OrdP (..))+import Data.Type.Equality (TestEquality (testEquality), (:~:) (Refl))++import DeBruijn.Ctx++-- | Term level witness of the size of the context.+--+-- >>> SZ+-- 0+--+-- >>> SS (SS SZ)+-- 2+--+type Size :: Ctx -> Type+data Size ctx where+    SZ :: Size EmptyCtx+    SS :: !(Size ctx) -> Size (S ctx)++-------------------------------------------------------------------------------+-- Helpers+-------------------------------------------------------------------------------++unSS :: Size (S ctx) -> Size ctx+unSS (SS x) = x++sizeToInt :: Size ctx -> Int+sizeToInt = go 0 where+    go :: Int -> Size ctx -> Int+    go !n SZ     = n+    go  n (SS s) = go (n + 1) s++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Show (Size ctx) where+    showsPrec d s = showsPrec d (sizeToInt s)++instance GShow Size where+    gshowsPrec = showsPrec++instance Eq (Size ctx) where+    _ == _ = True++instance Ord (Size ctx) where+    compare _ _ = EQ+    _ <= _ = True+    _ >= _ = True+    _ < _ = False+    _ > _ = False+    min x _ = x+    max x _ = x++instance EqP Size where+    eqp = defaultEq++instance OrdP Size where+    comparep = defaultCompare++instance GEq Size where+    geq SZ     SZ     = Just Refl+    geq (SS n) (SS m) = do+        Refl <- geq n m+        Just Refl+    geq _      _      = Nothing++instance GCompare Size where+    gcompare SZ     SZ     = GEQ+    gcompare SZ     (SS _) = GLT+    gcompare (SS _) SZ     = GGT+    gcompare (SS n) (SS m) = case gcompare n m of+        GLT -> GLT+        GEQ -> GEQ+        GGT -> GGT++instance TestEquality Size where+    testEquality = geq++-------------------------------------------------------------------------------+-- 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