rebound 0.1.1.0 → 0.1.2.0

raw patch · 19 files changed

+607/−129 lines, 19 filesdep +HUnitdep +prettyprinterdep ~QuickCheckdep ~basedep ~containersnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: HUnit, prettyprinter

Dependency ranges changed: QuickCheck, base, containers, deepseq, fin, mtl, vec

API changes (from Hackage documentation)

Files

• README.md +13/−16
• examples/DepMatch.hs +24/−18
• examples/PTS.hs +0/−9
• rebound.cabal +36/−8
• src/Data/Fin.hs +2/−0
• src/Data/LocalName.hs +16/−2
• src/Data/Scoped/Classes.hs +1/−1
• src/Data/Scoped/Maybe.hs +1/−1
• src/Rebound/Bind/Local.hs +238/−4
• src/Rebound/Bind/Pat.hs +1/−10
• src/Rebound/Bind/PatN.hs +88/−2
• src/Rebound/Bind/Single.hs +0/−46
• src/Rebound/Env.hs +12/−6
• src/Rebound/Env/Lazy.hs +2/−2
• src/Rebound/Env/ShiftList.hs +170/−0
• src/Rebound/Env/Strict.hs +1/−1
• src/Rebound/Generics.hs +2/−1
• test/Examples/DepMatch.hs +0/−1
• test/Examples/PTS.hs +0/−1

@@ -41,67 +41,67 @@  ### Calculi -1. [Untyped lambda calculus](examples/LC.hs)+1. [Untyped lambda calculus](https://github.com/sweirich/rebound/blob/main/rebound/examples/LC.hs)     Defines the syntax and substitution functions for the untyped lambda    calculus. Uses these definitions to implement several interpreters. -2. [Untyped lambda calculus with let rec and nested lets](examples/LCLet.hs)+2. [Untyped lambda calculus with let rec and nested lets](https://github.com/sweirich/rebound/blob/main/rebound/examples/LCLet.hs)     Example of advanced binding forms: recursive definitions and sequenced    definitions. -3. [Untyped lambda calculus with pattern matching](examples/Pat.hs)+3. [Untyped lambda calculus with pattern matching](https://github.com/sweirich/rebound/blob/main/rebound/examples/Pat.hs)     Extends the lambda calculus example with pattern matching. -4. [System F](examples/SystemF.hs)+4. [System F](https://github.com/sweirich/rebound/blob/main/rebound/examples/SystemF.hs)     Working with two separate scopes (type and term variables) is tricky. This    example shows one way to do it. -5. [Pure System F](examples/PureSystemF.hs)+5. [Pure System F](https://github.com/sweirich/rebound/blob/main/rebound/examples/PureSystemF.hs)     An alternative way of defining System F, using one single syntactic class.    Also demonstrates how to use the `ScopedReader` monad for typechecking and    pretty-printing. -6. [Simple implementation of dependent types](examples/PTS.hs)+6. [Simple implementation of dependent types](https://github.com/sweirich/rebound/blob/main/rebound/examples/PTS.hs)     An implementation of a simple type checker for a dependent-type system.    Language includes Pi and Sigma types. -7. [Dependent Pattern Matching](examples/DepMatch.hs)+7. [Dependent Pattern Matching](https://github.com/sweirich/rebound/blob/main/rebound/examples/DepMatch.hs)     A dependent type system with nested, dependent pattern matching. Patterns may    also include scoped terms. -8. [Linear Lambda Calculus](examples/LinLC.hs)+8. [Linear Lambda Calculus](https://github.com/sweirich/rebound/blob/main/rebound/examples/LinLC.hs)     A linear version of the (simply typed) lambda calculus. Demonstrates how to    thread a typing context using the `ScopedState` monad.  ### Working with well-scoped expressions -1. [Scope checking](examples/ScopeCheck.hs)+1. [Scope checking](https://github.com/sweirich/rebound/blob/main/rebound/examples/ScopeCheck.hs)     Demonstrates how to convert a "named" (or _nominal_) expression to a    well-scoped expression. -2. [QuickCheck](examples/LCQC.hs)+2. [QuickCheck](https://github.com/sweirich/rebound/blob/main/rebound/examples/LCQC.hs)     Demonstrates the use of well-scoped terms with    [QuickCheck](https://hackage.haskell.org/package/QuickCheck). -3. [HOAS](examples/HOAS.hs)+3. [HOAS](https://github.com/sweirich/rebound/blob/main/rebound/examples/HOAS.hs)     Demonstrates how to layer a HOAS representation on top of a de Bruijn    representation. Based on Conor McBride's ["Classy    Hack"](https://mazzo.li/epilogue/index.html%3Fp=773.html). -4. [PatGen](examples/PatGen.hs)+4. [PatGen](https://github.com/sweirich/rebound/blob/main/rebound/examples/PatGen.hs) -   A variant of the [Pat](examples/Pat.hs) example, which demonstrates how+   A variant of the [Pat](https://github.com/sweirich/rebound/blob/main/rebound/examples/Pat.hs) example, which demonstrates how    generic programming can be used to derive some definitions.  ## Related libraries@@ -130,6 +130,3 @@   rename the bound variable in abstraction if it is already in the current   scope. -- [binder](https://hackage.haskell.org/package/binder)--  Uses HOAS.

@@ -223,22 +223,6 @@   freeVars (PAnnot p t) = freeVars p <> freeVars t  ------------------------------------------------- weakening (convenience functions)--------------------------------------------------- >>> :t weaken' s1 t00--- weaken' s1 t00 :: Exp ('S ('S N1))---- >>> weaken' s1 t00--- 0 0--weaken' :: SNat m -> Exp n -> Exp (m + n)-weaken' m = applyE @Exp (weakenE' m)--weakenBind' :: SNat m -> Bind1 Exp Exp n -> Bind1 Exp Exp (m + n)-weakenBind' m = applyE @Exp (weakenE' m)------------------------------------------------ -- strengthening ---------------------------------------------- @@ -324,6 +308,28 @@ -- >>> tmid -- λ_. (λ_. 0) +sigmaExample :: Exp (S Z)+sigmaExample = Sigma star (bind1 (Sigma (Var f1) (bind1 (Var f1))))++tyEx = Pi star (bind1 (Pi sigmaExample (bind1 (Var f1))))++-- >>> :t Pat.bind+-- Pat.bind :: (Sized pat, Subst v c) => pat -> c (Size pat + n) -> Bind v c pat n++tmEx :: Exp Z+tmEx = Match (Branch (Scoped.bind PVar+                (Match (Branch (Scoped.bind (PPair PVar (PPair PVar PVar))+                          (Var f1)) :< Nil))) :< Nil)++-- >>> tyEx+-- Pi *. (Sigma *. 1 * 1) -> 1++-- >>> tmEx +-- λ_. (λ(_, (_, _)). 1)++-- >>> (checkType zeroE tmEx tyEx :: Either Err ())+-- Right ()+ --------------------------------------------------------  -- * Show instances@@ -602,10 +608,10 @@   case axiomAssoc @p2 @p1 @n of     Refl -> do       (g', e1) <- checkPattern g p1 tyA-      let tyB' = weakenBind' (size p1) tyB+      let tyB' = shift (size p1) tyB       let tyB'' = whnf (instantiate1 tyB' e1)       (g'', e2) <- checkPattern g' p2 tyB''-      let e1' = weaken' (size p2) e1+      let e1' = shift (size p2) e1       return (g'', Pair e1' e2) checkPattern g p ty = do   (g', e, ty') <- inferPattern g p

@@ -66,15 +66,6 @@ -- False instance FV Exp where --- >>> :t weaken' s1 t00--- weaken' s1 t00 :: Exp ('S ('S N1))---- >>> weaken' s1 t00--- 0 0--weaken' :: SNat m -> Exp n -> Exp (m + n)-weaken' m = applyE @Exp (weakenE' m)- -- >>> strengthenRec s1 s1 snat t00 -- Just (0 0) 

@@ -1,12 +1,12 @@ cabal-version:  3.0 name:           rebound-version:        0.1.1.0+version:        0.1.2.0 description:    Please see the README on GitHub at <https://github.com/sweirich/rebound> homepage:       https://github.com/sweirich/rebound bug-reports:    https://github.com/sweirich/rebound/issues author:         Stephanie Weirich, Noe De Santo maintainer:     sweirich@seas.upenn.edu, ndesanto@seas.upenn.edu-copyright:      2025 Stephanie Weirich, Noe De Santo+copyright:      2026 Stephanie Weirich, Noe De Santo license:        MIT license-file:   LICENSE build-type:     Simple@@ -20,6 +20,7 @@   ghc-options:      -Wno-type-defaults      -Wincomplete-patterns+     -Wno-deprecations   default-language:     GHC2021   default-extensions:@@ -42,13 +43,13 @@   import:       common-stanza   build-depends:-      base >= 4.15 && < 5.0-    , QuickCheck >= 2.15.0.1 && < 2.16-    , containers >= 0.6.8 && < 0.7-    , deepseq >= 1.5.1 && < 1.6+      base >= 4.15 && < 5+    , containers >= 0.6.7 && < 0.8+    , deepseq >= 1.4.8 && < 1.6+    , fin >= 0.3 && < 0.4     , mtl >= 2.3.1 && < 2.4-    , fin >= 0.3.2 && < 0.4-    , vec >= 0.5.1 && < 0.6+    , QuickCheck >= 2.14.3 && < 2.16+    , vec >= 0.5 && < 0.6   exposed-modules:       Rebound     , Rebound.Classes@@ -61,6 +62,7 @@     , Rebound.Env.StrictA     , Rebound.Env.StrictB     , Rebound.Env.Functional+    , Rebound.Env.ShiftList     , Rebound.Generics     , Rebound.Lib     , Rebound.MonadNamed@@ -80,6 +82,32 @@     , Data.Scoped.Classes     , Data.Scoped.Maybe   hs-source-dirs: src++library rebound-examples+  import:+    common-stanza+  visibility: private+  build-depends:+    base >=4.15, base < 5+    , rebound+    , mtl+    , HUnit < 1.7+    , QuickCheck+    , containers+    , prettyprinter < 1.8+  exposed-modules:+      LC+    , LCQC+    , LCLet+    , PTS+    , Pat+    , DepMatch+    , ScopeCheck+    , HOAS+    , SystemF+    , PureSystemF+    , LinLC+  hs-source-dirs: examples  test-suite rebound-tests   import:

@@ -23,6 +23,7 @@   invert,   shiftN,   shift1,+  split,   weakenFin,   weakenFinRight,   weaken1Fin,@@ -236,3 +237,4 @@   -- Case: x < k, leave it alone strengthenRecFin (snat_ -> SS_ k) m n (FS x) =     FS <$> strengthenRecFin k m n x+

@@ -3,17 +3,31 @@ -- Description : Strings with an "identity" equality module Data.LocalName where +import Test.QuickCheck+ -- | A simple wrapper for strings--- All local names are equal so that when they are used as patterns+-- All local names are *equal* so that when they are used as patterns -- they will be ignored. newtype LocalName = LocalName {name :: String}  instance Eq LocalName where   x1 == x2 = True +rawEq :: LocalName -> LocalName -> Bool+rawEq n1 n2 = name n1 == name n2+ instance Show LocalName where   show (LocalName x) = x --- | A default name.+-- | A default name internalName :: LocalName internalName = LocalName "_internal"++wildcardName :: LocalName+wildcardName = LocalName "_"++instance Arbitrary LocalName where+  arbitrary = do +    str <- elements [ "x", "y", "z", "w" ]+    num <- elements [1,2,3,4,5,0]+    return (LocalName (str ++ show num))

@@ -78,7 +78,7 @@     maximum x = F.maximum @k (coerce x)      minimum :: (Ord (a n)) => f a n -> a n-    minimum x = F.maximum @k (coerce x)+    minimum x = F.minimum @k (coerce x)      sum :: (Num (a n)) => f a n -> a n     sum x = F.sum @k (coerce x)

@@ -2,7 +2,7 @@ -- Module: Data.Scoped.Maybe -- Description : Scoped maybe ----- This module defines a Maybe type indexed by a scope+-- This module defines a Maybe type indexed by a scope. -- This module should be imported qualified. Many of the operations -- in this module have the same name as prelude functions. {-# LANGUAGE DeriveAnyClass #-}

@@ -1,11 +1,15 @@ -- |--- Module       : Rebound.Bind.Single+-- Module       : Rebound.Bind.Local -- Description  : Bind a single variable, with a name ----- Single variable binder, but includes a name (represented by a 'LocalName') for pretty printing.+-- Binders that includes a name (represented by a 'LocalName') for pretty printing. -- This is a specialization of "Rebound.Bind.Pat". module Rebound.Bind.Local   ( module Rebound,+    module Data.Vec,+    module Data.LocalName,++    -- * Single binder --     type Bind,     bind,     getLocalName,@@ -17,14 +21,59 @@     applyUnder,     bindWith,     unbindWith,-    instantiateWith+    instantiateWith,++-- * single binder --+    Bind1 (..),+    bind1,+    unbind1,+    unbindl1,+    getBody1,+    instantiate1,+    bindWith1,+    unbindWith1,+    instantiateWith1,+    applyUnder1,++    -- * Double binder --+    Bind2 (..),+    bind2,+    unbind2,+    getBody2,+    getLocalName2,+    instantiate2,+    bindWith2,+    unbindWith2,+    instantiateWith2,+    applyUnder2,++    -- * N-ary binder ---+    BindN (..),+    bindN,+    unbindN,+    unbindlN,+    getBodyN,+    getLocalNameN,+    instantiateN,+    bindWithN,+    unbindWithN,+    instantiateWithN,+    applyUnderN,   ) where +import Data.Fin qualified as Fin+import Data.Vec qualified as Vec+import Data.Vec (Vec(..))+import Data.LocalName import Rebound import Rebound.Bind.Pat qualified as Pat-import Data.Fin qualified as Fin+import Rebound.Env qualified as Env +++-- * -- Single Binder+ -- | Type binding a single variable. -- This data structure includes a delayed -- substitution for the variables in the body of the binder.@@ -81,6 +130,191 @@ -- The delayed substitution is __not__ applied, but is passed to the function instead. instantiateWith :: (SubstVar v) => Bind v c n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n instantiateWith b v = Pat.instantiateWith b (oneE v)+++-- | Type binding a single variable.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+type Bind1 v c n = Bind v c n++-- | Bind a variable, using the identity substitution.+bind1 :: (Subst v c) => LocalName -> c (S n) -> Bind1 v c n+bind1 = bind++-- | Bind a variable, while suspending the provided substitution.+bindWith1 :: forall v c m n. LocalName -> Env v m n -> c (S m) -> Bind1 v c n+bindWith1 = bindWith++-- | Bind the default \"internal\" variable, while suspending the provided substitution.+internalBind1 :: (Subst v c) => c (S n) -> Bind1 v c n+internalBind1 = internalBind++-- | Retrieve the name of the bound variable.+getLocalName1 :: Bind1 v c n -> LocalName+getLocalName1 = getLocalName++-- | Retrieve the body of the binding.+getBody1 :: (Subst v c) => Bind1 v c n -> c (S n)+getBody1 = getBody++-- | Run a function on the body (and bound name), after applying the delayed substitution.+unbind1 :: (Subst v c) => Bind1 v c n -> ((LocalName, c (S n)) -> d) -> d+unbind1 = unbind++-- | Retrieve the body, as well as the bound name.+unbindl1 :: (Subst v c) => Bind1 v c n -> (LocalName, c (S n))+unbindl1 = unbindl++-- | Instantiate the body (i.e. replace the bound variable) with the provided term.+instantiate1 :: (Subst v c) => Bind1 v c n -> v n -> c n+instantiate1 = instantiate ++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder1 ::+  (Subst v c) =>+  (forall m. Env v m (S n2) -> c m -> c (S n2)) ->+  Env v n1 n2 ->+  Bind1 v c n1 ->+  Bind1 v c n2+applyUnder1 = applyUnder++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWith1 :: (SubstVar v) => Bind1 v c n -> (forall m. LocalName -> Env v m n -> c (S m) -> d) -> d+unbindWith1 = unbindWith++-- | Instantiate the body (i.e. replace the bound variable) with the provided term.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+instantiateWith1 :: (SubstVar v) => Bind1 v c n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n+instantiateWith1 = instantiateWith++++-- * -- Double Binder++-- | Type binding a single variable.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+type Bind2 v c n = Pat.Bind v c (Vec N2 LocalName) n++-- | Bind a variable, using the identity substitution.+bind2 :: (Subst v c) => LocalName -> LocalName -> c (S (S n)) -> Bind2 v c n+bind2 x y = Pat.bind (x ::: (y ::: VNil))++-- | Bind a variable, while suspending the provided substitution.+bindWith2 :: forall v c m n. LocalName -> LocalName -> Env v m n -> c (S (S m)) -> Bind2 v c n+bindWith2 x y = Pat.bindWith (x ::: (y ::: VNil))++-- | Bind the default \"internal\" variable, while suspending the provided substitution.+internalBind2 :: (Subst v c) => c (S (S n)) -> Bind2 v c n+internalBind2 = Pat.bind (internalName ::: internalName ::: VNil)++-- | Retrieve the names of the bound variable.+getLocalName2 :: Bind2 v c n -> Vec N2 LocalName+getLocalName2 = Pat.getPat++-- | Retrieve the body of the binding.+getBody2 :: (Subst v c) => Bind2 v c n -> c (S (S n))+getBody2 = Pat.getBody++-- | Run a function on the body (and bound name), after applying the delayed substitution.+unbind2 :: (Subst v c) => Bind2 v c n -> ((Vec N2 LocalName, c (S (S n))) -> d) -> d+unbind2 b f = f (getLocalName2 b, getBody2 b)++-- | Retrieve the body, as well as the bound name.+unbindl2 :: (Subst v c) => Bind2 v c n -> (Vec N2 LocalName, c (S (S n)))+unbindl2 b = (getLocalName2 b, getBody2 b)++-- | Instantiate the body (i.e. replace the bound variable) with the provided term.+instantiate2 :: (Subst v c) => Bind2 v c n -> v n -> v n -> c n+instantiate2 b e1 e2 = Pat.instantiate b (e1 .: (e2 .: zeroE))++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder2 ::+  (Subst v c) =>+  (forall m. Env v m (S (S n2)) -> c m -> c (S (S n2))) ->+  Env v n1 n2 ->+  Bind2 v c n1 ->+  Bind2 v c n2+applyUnder2 = Pat.applyUnder++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWith2 :: (SubstVar v) => Bind2 v c n -> +   (forall m. LocalName -> LocalName -> Env v m n -> c (S (S m)) -> d) -> d+unbindWith2 b f = Pat.unbindWith b (\ v e b2 -> f (v Vec.! FZ) (v Vec.! (FS FZ)) e b2)++-- | Instantiate the body (i.e. replace the bound variable) with the provided term.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+instantiateWith2 :: (SubstVar v) => +  Bind2 v c n -> v n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n+instantiateWith2 b v1 v2 = Pat.instantiateWith b (v1 .: (v2 .: zeroE))+++type BindN v c m n = Pat.Bind v c (Vec m LocalName) n+++-- | Bind a number of variables, using the identity substitution.+bindN :: forall m v c n. (Subst v c, SNatI m) => Vec m LocalName -> c (m + n) -> BindN v c m n+bindN = Pat.bind ++-- | Bind a number of variables, while suspending the provided substitution.+bindWithN :: forall p v c m n. (SNatI p) => Vec p LocalName -> Env v m n -> c (p + m) -> BindN v c p n+bindWithN = Pat.bindWith ++-- | Run a function on the body, after applying the delayed substitution.+unbindN :: forall m v c n d. (Subst v c, SNatI n, SNatI m) => +   BindN v c m n -> ((SNatI (m + n)) => Vec m LocalName -> c (m + n) -> d) -> d+unbindN bnd f = Pat.unbind bnd f++-- | Retrieve the body of the binding.+-- For this kind of binding, it is equivalent to 'getBodyN'.+unbindlN :: forall m v c n. (Subst v c, SNatI m) => BindN v c m n -> c (m + n)+unbindlN = Pat.getBody++-- | Retrieve the body of the binding.+getBodyN :: forall m v c n. (Subst v c, SNatI m) => BindN v c m n -> c (m + n)+getBodyN = Pat.getBody++getLocalNameN :: BindN v c m n -> Vec m LocalName+getLocalNameN = Pat.getPat++-- | Instantiate the body (i.e. replace the bound variables) with the provided terms.+instantiateN :: (Subst v c, SNatI m) => BindN v c m n -> Vec m (v n) -> c n+instantiateN b v = Pat.instantiate b (fromVec v)++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWithN ::+  (SubstVar v, SNatI m) =>+  BindN v c m n ->+  (forall m1. Env v m1 n -> c (m + m1) -> d) ->+  d+unbindWithN b f = Pat.unbindWith b (const f)++-- | Instantiate the body (i.e. replace the bound variable) with the provided terms.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+instantiateWithN ::+  forall m v c d n.+  (SubstVar v, SNatI n, SNatI m) =>+  BindN v c m n ->+  Vec m (v n) ->+  (forall m. Env v m n -> c m -> d n) ->+  d n+instantiateWithN b v f =+  unbindWithN b (f . appendE (snat @m) (fromVec v))++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnderN ::+  (Subst v c2, SNatI k) =>+  (forall m. Env v m (k + n2) -> c1 m -> c2 (k + n2)) ->+  Env v n1 n2 ->+  BindN v c1 k n1 ->+  BindN v c2 k n2+applyUnderN = Pat.applyUnder   -- Example

@@ -188,7 +188,7 @@   appearsFree n (Rebind p1 p2) = appearsFree (Fin.shiftN (size p1) n) p2    freeVars :: (Sized p1, FV p2) => Rebind p1 p2 n -> Set (Fin n)-  freeVars = undefined+  freeVars (Rebind p1 p2) = rescope (size p1) (freeVars p2)  instance (Sized p1, Strengthen p2) => Strengthen (Rebind p1 p2) where   strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) (Rebind (p1 :: p1) p2) =@@ -235,12 +235,3 @@     Refl <- patEq ps1 ps2     return Refl   patEq _ _ = Nothing---- instance---   (forall p n. WithData v (pat p) n) =>---   WithData v (PatList pat p) n---   where---   extendWithData PNil = id---   extendWithData (PCons (p1 :: pat p1') (ps :: PatList pat ps')) =---     case axiomAssoc @ps' @p1' @n of---       Refl -> extendWithData @v ps . extendWithData @v p1

@@ -9,6 +9,19 @@      PatN(..), +    -- * single binder (no suffix) --+    Bind (..),+    bind,+    unbind,+    unbindl,+    getBody,+    instantiate,+    bindWith,+    unbindWith,+    instantiateWith,+    applyUnder,++     -- * single binder --     Bind1 (..),     bind1,@@ -52,8 +65,6 @@ import Data.Fin qualified as Fin import Data.Vec qualified as Vec -- ---------------------------------------------------------------- -- N-ary patterns ----------------------------------------------------------------@@ -204,6 +215,81 @@   Bind1 v c1 n1 ->   Bind1 v c2 n2 applyUnder1 = Pat.applyUnder+++----------------------------------------------------------------+-- Single binder (other names)+----------------------------------------------------------------++-- | Type binding 1 variable.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+type Bind v c n = Bind1 v c n ++-- | Bind 1 variable, using the identity substitution.+bind :: (Subst v c) => c (S n) -> Bind v c n+bind = bind1++-- | Bind 1 variable, while suspending the provided substitution.+bindWith :: forall v c m n. Env v m n -> c (S m) -> Bind v c n+bindWith = bindWith1++-- | Run a function on the body, after applying the delayed substitution.+unbind ::+  forall v c n d.+  (SNatI n, Subst v c) =>+  Bind v c n ->+  ((SNatI (S n)) => c (S n) -> d) ->+  d+unbind = unbind1++-- | Retrieve the body of the binding.+-- For this kind of binding, it is equivalent to 'getBody1'.+unbindl :: forall v c n. (Subst v c) => Bind v c n -> c (S n)+unbindl = unbindl1++-- | Retrieve the body of the binding.+getBody ::+  forall v c n.+  (Subst v c) =>+  Bind1 v c n ->+  c (S n)+getBody = getBody1++-- | Instantiate the body (i.e. replace the bound variable) with the provided term.+instantiate :: (Subst v c) => Bind v c n -> v n -> c n+instantiate = instantiate1++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWith ::+  (SubstVar v) =>+  Bind v c n ->+  (forall m. Env v m n -> c (S m) -> d) ->+  d+unbindWith = unbindWith1++-- | Instantiate the body (i.e. replace the bound variable) with the provided terms.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+instantiateWith ::+  (SubstVar v) =>+  Bind v c n ->+  v n ->+  (forall m. Env v m n -> c m -> d n) ->+  d n+instantiateWith = instantiateWith1+++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder ::+  (Subst v c2) =>+  (forall m. Env v m (S n2) -> c1 m -> c2 (S n2)) ->+  Env v n1 n2 ->+  Bind v c1 n1 ->+  Bind v c2 n2+applyUnder = applyUnder1+  ---------------------------------------------------------------- -- Double binder

@@ -22,49 +22,3 @@ import Rebound import Rebound.Bind.PatN import Rebound.Classes---- | Type binding a single variable.--- This data structure includes a delayed--- substitution for the variables in the body of the binder.-type Bind v c n = Bind1 v c n---- | Bind a variable, using the identity substitution.-bind :: (Subst v c) => c (S n) -> Bind v c n-bind = bind1---- | Bind a variable, while suspending the provided substitution.-bindWith :: forall v c m n. Env v m n -> c (S m) -> Bind v c n-bindWith = bindWith1---- | Run a function on the body, after applying the delayed substitution.-unbind :: forall v c n d. (SNatI n, Subst v c) => Bind v c n -> ((SNatI (S n)) => c (S n) -> d) -> d-unbind = unbind1---- | Retrieve the body of the binding.--- For this kind of binding, it is equivalent to 'getBody'.-unbindl :: (Subst v c) => Bind v c n -> c (S n)-unbindl = unbindl1---- | Retrieve the body of the binding.-getBody :: forall v c n. (Subst v c) => Bind v c n -> c (S n)-getBody = getBody1---- | Instantiate the body (i.e. replace the bound variable) with the provided term.-instantiate :: (Subst v c) => Bind v c n -> v n -> c n-instantiate = instantiate1---- | Run a function on the body.--- The delayed substitution is __not__ applied, but is passed to the function instead.-unbindWith :: (SubstVar v) => Bind v c n -> (forall m. Env v m n -> c (S m) -> d) -> d-unbindWith = unbindWith1---- | Instantiate the body (i.e. replace the bound variable) with the provided term.--- The delayed substitution is __not__ applied, but is passed to the function instead.-instantiateWith :: (SubstVar v) => Bind v c n -> v n -> (forall m. Env v m n -> c m -> d n) -> d n-instantiateWith = instantiateWith1---- | Apply a function under the binder.--- The delayed substitution is __not__ applied, but is passed to the function instead.-applyUnder :: (Subst v c2) => (forall m. Env v m (S n2) -> c1 m -> c2 (S n2)) -> Env v n1 n2 -> Bind v c1 n1 -> Bind v c2 n2-applyUnder = applyUnder1-

@@ -38,9 +38,9 @@     toVec,     tabulate,     fromTable,-    weakenE',     weakenER,     shiftFromApplyE,+    skip   ) where @@ -84,8 +84,10 @@ idE :: (SubstVar v) => Env v n n idE = shiftNE s0 --- | Append two environments.---++++-- | append two environments -- The `SNatI` constraint is a runtime witness for the length -- of the domain of the first environment. (.++) ::@@ -124,10 +126,14 @@ shift1E :: (SubstVar v) => Env v n (S n) shift1E = shiftNE s1 --- | Increment all free variables by @p@.+-- | rename then increment by 1+skip :: SubstVar v => Env v m n -> Env v m (S n)+skip e = e .>> shift1E++-- | Shift an environment by size `p` upN ::   forall v p m n.-  (Subst v v) =>+  (SubstVar v) =>   SNat p ->   Env v m n ->   Env v (p + m) (p + n)@@ -137,7 +143,7 @@     base = MkUpN id     step :: forall p1. UpN v m n p1 -> UpN v m n (S p1)     step (MkUpN r) = MkUpN $-      \e -> var Fin.f0 .: (r e .>> shiftNE s1)+      \e -> var Fin.f0 .: (skip (r e))  newtype UpN v m n p = MkUpN {getUpN :: Env v m n -> Env v (p + m) (p + n)} 

@@ -1,6 +1,6 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE UndecidableSuperClasses #-}-{-# OPTIONS_HADDOCK hide #-}+-- | The concrete implementation of environments module Rebound.Env.Lazy where  -- "Defunctionalized" representation of environment@@ -115,7 +115,7 @@ {-# INLINEABLE weakenE' #-}  -- | Shift the term, increasing every free variable as well as the bound by the provided amount.-shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n) shiftNE = Inc {-# INLINEABLE shiftNE #-} 

@@ -0,0 +1,170 @@+-- This implementation is adapted from+-- https://mathisbd.github.io/blog/esubstitutions.html+-- TODO: still missing weakenER, but should be able to test and run it now+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+module Rebound.Env.ShiftList where++import Data.Nat+import Data.Fin++import Rebound.Lib +import GHC.Generics hiding (S)+import Control.DeepSeq (NFData (..))++------------------------------------------------------------------------------+-- Substitution class declarations+------------------------------------------------------------------------------+-- | Well-scoped types that can be the range of+-- an environment. This should generally be the @Var@+-- constructor from the syntax.+class (Subst v v) => SubstVar (v :: Nat -> Type) where+  var :: Fin n -> v n+++-- | Apply the environment throughout a term of+-- type `c n`, replacing variables with values+-- of type `v m`+class (SubstVar v) => Subst v c where+  applyE :: Env v n m -> c n -> c m+  default applyE :: (Generic1 c, GSubst v (Rep1 c), SubstVar v) => Env v m n -> c m -> c n+  applyE = gapplyE+  {-# INLINE applyE #-}+  isVar :: c n -> Maybe (v :~: c, Fin n)+  isVar _ = Nothing+  {-# INLINE isVar #-}++-- | Generic programming variant of 'applyE'.+gapplyE :: forall c v m n. (Generic1 c, GSubst v (Rep1 c), Subst v c) => Env v m n -> c m -> c n+gapplyE r e | Just (Refl, x) <- isVar @v @c e = applyEnv r x+gapplyE r e = applyOpt (\s x -> to1 $ gsubst s (from1 x)) r e+{-# INLINEABLE gapplyE #-}++-- | Generic programming support for 'Subst'.+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n+++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------++-- The 'SNat k' in this representation is an embedded shift +-- that means that 'Inc k' is the same as 'Inc k'+data Env a m n where+    Zero :: Env a Z n+    Inc  :: !(SNat k) -> Env a n (k + n)+    Cons :: !(SNat k) -> a m -> (Env a n m) -> Env a (S n) (k + m)++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf :: (forall (n1 :: Nat). NFData (a n1)) => Env a n m -> ()+  rnf Zero = ()+  rnf (Inc x) = rnf x +  rnf (Cons x a xs) = rnf x `seq` rnf a `seq` rnf xs ++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++weaken :: forall a k n. Subst a a => SNat k -> a n -> a (k + n)+weaken k t = applyE @a (shiftNE k) t++applyEnv ::  SubstVar a => Env a n m -> Fin n -> a m+applyEnv s i = applyRec @N0 snat s i+{-# INLINEABLE applyEnv #-}++-- | Build an optimized version of applyE.+-- Checks to see if we are applying the identity substitution first.+applyOpt :: (Env v n m -> c n -> c m) -> (Env v n m -> c n -> c m)+applyOpt f (Inc SZ) x = x+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++-- | As we traverse the list, accumulate the shifting amount and +-- apply it all at once.+applyRec :: forall acc a n m . SubstVar a => +    SNat acc -> Env a n m -> Fin n -> a (acc + m)+applyRec acc s i = +    case s of +        Zero -> case i of {}+        Inc (k :: SNat k) -- renaming+              | Refl <- axiomPlusZ @m+              , Refl <- axiomAssoc @acc @k @n+              -> var (shiftN (sPlus acc k) i)+        Cons (k :: SNat k) (t :: a m1) s +              | Refl <- axiomAssoc @acc @k @m1 +              -> case i of +                   FZ   -> weaken (sPlus acc k) t  -- substitution+                   FS j -> applyRec (sPlus acc k) s j+++zeroE :: Env a Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- TODO: add weakenER to this definition+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = undefined++shiftNE :: SNat k -> Env a n (k + n)+shiftNE k = Inc k+{-# INLINEABLE shiftNE #-}++(.:) :: a m -> Env a n m -> Env a (S n) m+(.:) = Cons SZ +{-# INLINEABLE (.:) #-}+++-- | inverse of @cons@ -- remove the first mapping+tail :: (SubstVar v) => Env v (S n) m -> Env v n m+tail x = shiftNE s1 .>> x+{-# INLINEABLE tail #-}++-- Compose a substitution with shifting, just add the shifting amount +-- to the head of the substitution+-- skip k s == s .>> Inc k +skip0 :: forall k0 a n m. SNatI k0 => Env a n m -> Env a n (k0 + m)+skip0 s = case s of+              Zero -> Zero+              (Inc (k :: SNat k)) +                | Refl <- axiomAssoc @k0 @k @n+                    -> Inc (sPlus (snat @k0) k)+              (Cons (k :: SNat k) (t :: a m1) s)+                | Refl <- axiomAssoc @k0 @k @m1+                    -> Cons (sPlus (snat @k0) k) t s+{-# INLINEABLE skip0 #-}++up :: forall a n m. SubstVar a => Env a n m -> Env a (S n) (S m)+up s = var f0 .: (skip0 @N1 s)++-- NB: there is a generic definition of upN in Env.hs, but I don't know +-- how efficient it is.++-- | Compose two environments, applying them in sequence (left then right).+(.>>) :: (SubstVar v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | look at the two arguments and compose them together smartly+comp :: forall a m n p. (SubstVar a) =>+         Env a m n -> Env a n p -> Env a m p+comp Zero s = Zero    +-- if the second argument is a shift, we can use skip    +comp s (Inc (k :: SNat k)) = withSNat k $ skip0 @k s+-- if the first argument is a shift, we can drop substitutions in the second+-- argument+comp (Inc SZ) s = s+comp (Inc (snat_ -> SS_ m1)) (Cons (k :: SNat k) _ xs) = +    comp (Inc m1) (withSNat k $ skip0 @k xs)+-- for the Cons/Cons case, we need to apply the second substitution +-- to 'x' (after it has been shifted by k)+comp (Cons (k :: SNat k) (x :: a n1) xs) s = Cons SZ head tail where+    head = applyE @a (comp (Inc k) s) x+    tail = comp (withSNat k $ skip0 @k xs) s++-- | Map the range of an environment. Has to preserve the scope of the range.+transform :: (SubstVar b) => +   (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Inc k) = Inc k+transform f (Cons k x xs) = Cons k (f x) (transform f xs)

@@ -113,7 +113,7 @@ {-# INLINEABLE weakenE' #-}  -- | increment all free variables by m-shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n) shiftNE = Inc {-# INLINEABLE shiftNE #-} 

@@ -29,6 +29,7 @@   {-# INLINE gsubst #-}  instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where+  gsubst :: (GSubst b f, GSubst b g) => Env b m n -> (:*:) f g m -> (:*:) f g n   gsubst s (f :*: g) = gsubst s f :*: gsubst s g   {-# INLINE gsubst #-} @@ -76,7 +77,7 @@   {-# INLINE gfreeVars #-}  instance (GFV f, GFV g) => GFV (f :*: g) where-  gappearsFree s (f :*: g) = gappearsFree s f && gappearsFree s g+  gappearsFree s (f :*: g) = gappearsFree s f || gappearsFree s g   {-# INLINE gappearsFree #-}   gfreeVars (f :*: g) = gfreeVars f <> gfreeVars g   {-# INLINE gfreeVars #-}

@@ -21,7 +21,6 @@         ((snat,) <$> patternMatch pat0 tm0) @?= Just (snat @N2, sig Star (Var f0) .: (Star .: zeroE)),       testCase "Is f0 free in t00?" $ appearsFree f0 t00 @?= True,       testCase "Is f1 free in t00?" $ appearsFree f1 t00 @?= False,-      testCase "Weaken t00 by 1" $ weaken' s1 t00 @?= (Var f0 `App` Var f0),       testCase "Strengthen t00 by 1/1" $ strengthenRec s1 s1 snat t00 @?= Just (Var f0 `App` Var f0),       testCase "Strengthen t01 by 1/1" $ strengthenRec s1 s1 snat t01 @?= Nothing,       testCase "Pretty-print t0" $ show t0 @?= "λ_. 0",

@@ -22,7 +22,6 @@     "PTS"     [ testCase "Is f0 free in t00?" $ appearsFree f0 t00 @?= True,       testCase "Is f1 free in t00?" $ appearsFree f1 t00 @?= False,-      testCase "Weaken t00 by 1" $ weaken' s1 t00 @?= App (Var f0) (Var f0),       testCase "Strengthen t00 by 1/1" $         strengthenRec s1 s1 snat t00 @?= Just (App (Var f0) (Var f0)),       testCase "Strengthen t01 by 1/1" $ strengthenRec s1 s1 snat t01 @?= Nothing,