packages feed

rebound (empty) → 0.1.0.0

raw patch · 53 files changed

+7861/−0 lines, 53 filesdep +QuickCheckdep +basedep +containers

Dependencies added: QuickCheck, base, containers, deepseq, fin, mtl, rebound, tasty, tasty-hunit, tasty-quickcheck, vec

Files

+ ChangeLog.md view
@@ -0,0 +1,1 @@+2025-08-01: initial version
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2025 Stephanie Weirich, Noe De Santo++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ README.md view
@@ -0,0 +1,135 @@+# Rebound+++`Rebound` is a variable binding library based on well-scoped de Bruijn indices+and environments.++This library is represents variables using the index type `Fin n`; a type of+bounded natural numbers. The key way to manipulate these indices is using an+*environment*, a simultaneous substitutions similar to a function of type `Fin n+-> Exp m`. Applying an environment converts an expression in scope `n` to one in+scope `m`.++## Design goals++The goal of this library is to be an effective tool for language+experimentation. Say you want to implement a new language idea that you have+read about in a PACMPL paper? This library will help you put together a+prototype implementation quickly.++1. *Correctness*: This library uses Dependent Haskell to statically track the+    scopes of bound variables. Because variables are represented by de Bruijn+    indices, scopes are represented by natural numbers, bounding the indices+    that can be used. If the scope is 0, then the term must be closed.++2. *Convenience*: The library is based on a type-directed approach to binding,+    where AST terms can indicate binding structure through the use of types+    defined in this library. As a result the library provides a clean, uniform,+    and automatic interface to common operations such as substitution,+    alpha-equality, and scope change.++3. *Efficiency*: Behind the scenes, the library uses explicit substitutions+    (environments) to delay the execution of operations such as shifting and+    substitution. However, these environments are accessible to library users+    who would like fine control over when these operations.++4. *Accessibility*: This library comes with several examples demonstrating how+    to use it effectively. Many of these are also examples of programming with+    Dependent Haskell.++## Examples++### Calculi++1. [Untyped lambda calculus](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)++   Example of advanced binding forms: recursive definitions and sequenced+   definitions.++3. [Untyped lambda calculus with pattern matching](examples/Pat.hs)++   Extends the lambda calculus example with pattern matching.++4. [System F](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)++   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)++   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)++   A dependent type system with nested, dependent pattern matching. Patterns may+   also include scoped terms.++8. [Linear Lambda Calculus](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)++   Demonstrates how to convert a "named" (or _nominal_) expression to a+   well-scoped expression.++2. [QuickCheck](examples/LCQC.hs)++   Demonstrates the use of well-scoped terms with+   [QuickCheck](https://hackage.haskell.org/package/QuickCheck).++3. [HOAS](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)++   A variant of the [Pat](examples/Pat.hs) example, which demonstrates how+   generic programming can be used to derive some definitions.++## Related libraries++- [Bound](https://hackage.haskell.org/package/bound)++  `Bound` is the most closely related library. Like `Rebound`, it is a+  scope-safe approach to de Bruijn indices in Haskell. The key difference is+  that `bound` requires fewer language extensions by using nested datatypes+  instead of GADTs. Use this library if you would like to avoid extensions such+  as `GADTs`, `DataKinds`, and `TypeFamilies`.++- [Unbound-Generics](https://hackage.haskell.org/package/unbound-generics)++  The `Unbound` library uses a locally-nameless reprsentation. `Rebound` draws+  inspiration for its design from the type-directed approach to the binding+  interface found in `Unbound`. However, `Unbound` is not not-scope safe. As a+  result it is easier to get started. However, working with a locally nameless+  representation requires a monad for fresh name generation. It also can be+  slow.++- [Foil and Free Foil](https://hackage.haskell.org/package/free-foil)++  GHC internally uses a *nominal* representation of binding, where both bound+  and free variables are represented by names. In this approach, users must+  rename the bound variable in abstraction if it is already in the current+  scope.++- [binder](https://hackage.haskell.org/package/binder)++  Uses HOAS.
+ examples/DepMatch.hs view
@@ -0,0 +1,707 @@+-- | A dependent type system, with nested dependent pattern matching for Sigma types.+-- This is an advanced usage of the binding library, demonstrating the use of Scoped patterns.+-- It doesn't correspond to any current system, but has its own elegance++{-# LANGUAGE OverloadedLists #-}+module DepMatch where++import Rebound+import Rebound.Context+++import qualified Rebound.Bind.Pat as Pat+import qualified Rebound.Bind.Scoped as Scoped+import Rebound.Bind.PatN as PN++import Control.Monad (guard, zipWithM_)+import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)+import Data.Fin+import Data.Maybe qualified as Maybe+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Vec qualified+import Data.Scoped.List (List, pattern Nil, pattern (:<))+import Data.Scoped.List qualified as List+import GHC.Generics (Generic1)++-- In this system, `Match` introduces a Pi type and generalizes+-- dependent functions+-- If the pattern is a single variable, or an annotated variable,+-- then the `Match` term is just a normal lambda expression.+-- But the pattern could be more structured than that, supporting+-- a general form of pattern matching. In this simple language,+-- only type that supports pattern matching is a Sigma type. So+-- every match expression should have a single branch. But, for+-- generality, we pretend that more are possible.+data Exp (n :: Nat)+  = Star+  | Pi (Exp n) (Bind1 Exp Exp n)+  | Var (Fin n)+  | Match (List Branch n)  -- case lambda+  | App (Exp n) (Exp n)+  | Sigma (Exp n) (Bind1 Exp Exp n)+  | Pair (Exp n) (Exp n)+  | Annot (Exp n) (Exp n)+      deriving (Generic1)++-- | A single branch in a match expression+data Branch (n :: Nat)+  = forall p. Branch (Scoped.Bind Exp Exp (Pat p) n)+++-- | Patterns, which may include embedded type annotations+-- `p` is the number of variables bound by the pattern+-- `n` is the number of free variables in type annotations in the pattern+data Pat (p :: Nat) (n :: Nat) where+  PVar :: Pat N1 n+  -- Patterns are "telescopic"+  -- In Pair pattern, we increase the scope so that variables+  -- bound in the left subterm can be referred to in the right subterm+  PPair :: Pat p1 n -> Pat p2 (p1 + n) -> Pat (p2 + p1) n+  -- Patterns can also include type annotations.+  PAnnot :: Pat p n -> Exp n -> Pat p n+++-- This definitions support telescopes: variables bound earlier in the pattern+-- can appear later.  For example, the pattern for a type paired with+-- a term of that type can look like this+--     (x, (y :: x))++pat0 :: Pat N2 N0+pat0 = PPair PVar (PAnnot PVar (Var f0))++-- The type of this pattern is+--     Sigma x:Star.x+ty0 :: Exp Z+ty0 = Sigma Star (bind1 (Var f0))++-------------------------------------------------------+-- definitions for pattern matching+-------------------------------------------------------++instance Sized (Pat p n) where+  type Size (Pat p n) = p+  size :: Pat p n -> SNat p+  size PVar = s1+  size (PPair p1 p2) = sPlus (size p2) (size p1)+  size (PAnnot p _) = size p++-- Because Pat is a scope-indexed pattern, we need to also +-- instantiate the `ScopedSized` class+instance Scoped.ScopedSized (Pat p) where+  type ScopedSize (Pat p) = p++-- A term that matches the "(x,(y:x))" and has type exists x:*. x+tm0 :: Exp Z+tm0 = Pair Star ty0++-- >>> patternMatch pat0 tm0+-- Just [(0,Sigma *. 0),(1,*)]++-- | Compare a pattern with an expression, potentially+-- producing a substitution for all of the variables+-- bound in the pattern+patternMatch :: Pat p n -> Exp n -> Maybe (Env Exp p n)+patternMatch PVar e = Just $ oneE e+patternMatch (PPair p1 p2) (Pair e1 e2) =+  -- two append operations require implicit sizes in the context+  withSNat (size p1) $ withSNat (size p2) $ do+    env1 <- patternMatch p1 e1+    -- NOTE: substitute in p2 with env1 before pattern matching+    env2 <- patternMatch (applyE (env1 .++ idE) p2) e2+    return (env2 .++ env1)+-- ignore type annotates when pattern matching+patternMatch (PAnnot p _) e = patternMatch p e+patternMatch p (Annot e _) = patternMatch p e+patternMatch _ _ = Nothing++findBranch :: Exp n -> List Branch n -> Maybe (Exp n)+findBranch e Nil = Nothing+findBranch e (Branch (bnd :: Scoped.Bind Exp Exp (Pat p) n) :< brs) =+  case patternMatch (Scoped.getPat bnd) e of+    Just r -> Just $ Scoped.instantiate bnd r+    Nothing -> findBranch e brs++----------------------------------------------+-- * Subst instances++instance SubstVar Exp where+  var = Var++instance Shiftable Exp where+  shift = shiftFromApplyE @Exp++instance Subst Exp Exp where+  isVar (Var x) = Just (Refl, x)+  isVar _ = Nothing++  {-+  -- The generic definition above is equivalent to this code+  applyE r Star = Star+  applyE r (Pi a b) = Pi (applyE r a) (applyE r b)+  applyE r (Var x) = applyEnv r x+  applyE r (App e1 e2) = App (applyE r e1) (applyE r e2)+  applyE r (Sigma a b) = Sigma (applyE r a) (applyE r b)+  applyE r (Pair a b) = Pair (applyE r a) (applyE r b)+  applyE r (Match brs) = Match (List.map (applyE r) brs)+  applyE r (Annot a t) = Annot (applyE r a) (applyE r t)+  -}++instance Shiftable (Pat p) where+  shift = shiftFromApplyE @Exp++-- This definition cannot be generic because Pat is a GADT+instance Subst Exp (Pat p) where+  applyE :: Env Exp n m -> Pat p n -> Pat p m+  applyE r PVar = PVar+  -- need to account for new pattern variables from p1 bound in p2+  applyE r (PPair p1 p2) = PPair (applyE r p1) (applyE (upN (size p1) r) p2)+  applyE r (PAnnot p t) = PAnnot (applyE r p) (applyE r t)+++instance Shiftable Branch where+  shift = shiftFromApplyE @Exp++-- This definition also cannot be generic due to the existential+instance Subst Exp Branch where+  applyE :: Env Exp n m -> Branch n -> Branch m+  applyE r (Branch b) = Branch (applyE r b)+++----------------------------------------------+-- Free variable calculation+----------------------------------------------++t00 :: Exp N2+t00 = App (Var f0) (Var f0)++t01 :: Exp N2+t01 = App (Var f0) (Var f1)++-- >>> appearsFree f0 t00+-- True++-- >>> appearsFree f1 t00+-- False++instance FV Exp where+  {-+  -- Generic programming produces the following definitions:+  appearsFree n (Var x) = n == x+  appearsFree n Star = False+  appearsFree n (Pi a b) = appearsFree n a || appearsFree (FS n) (getBody1 b)+  appearsFree n (App a b) = appearsFree n a || appearsFree n b+  appearsFree n (Sigma a b) = appearsFree n a || appearsFree (FS n) (getBody1 b)+  appearsFree n (Pair a b) = appearsFree n a || appearsFree n b+  appearsFree n (Match b) = List.any (appearsFree n) b+  appearsFree n (Annot a t) = appearsFree n a || appearsFree n t++  freeVars :: Exp n -> Set (Fin n)+  freeVars (Var x) = Set.singleton x+  freeVars Star = Set.empty+  freeVars (Pi a b) = freeVars a <> rescope s1 (freeVars (getBody1 b))+  freeVars (App a b) = freeVars a <> freeVars b+  freeVars (Sigma a b) = freeVars a <> rescope s1 (freeVars (getBody1 b))+  freeVars (Pair a b) = freeVars a <> freeVars b+  freeVars (Match b) = List.foldMap freeVars b+  freeVars (Annot a t) = freeVars a <> freeVars t+  -}++-- cannot be generic+instance FV Branch where+  appearsFree n (Branch bnd) = appearsFree n bnd+  freeVars (Branch bnd)= freeVars bnd++-- cannot be generic+instance FV (Pat p) where+  appearsFree n PVar = False+  appearsFree n (PPair p1 p2) = appearsFree n p1 || appearsFree (shiftN (size p1) n) p2+  appearsFree n (PAnnot p t) = appearsFree n p || appearsFree n t++  freeVars PVar = Set.empty+  freeVars (PPair p1 p2) = freeVars p1 <> rescope (size p1) (freeVars p2)+  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+----------------------------------------------++-- >>> strengthenRec s1 s1 snat t00+-- Just (0 0)++-- >>> strengthenRec s1 s1 snat t01+-- Nothing++instance Strengthen Exp where+  {-+  strengthenRec k m n (Var x) = Var <$> strengthenRec k m n x+  strengthenRec k m n Star = pure Star+  strengthenRec k m n (Pi a b) = Pi <$> strengthenRec k m n a <*> strengthenRec k m n b+  strengthenRec k m n (App a b) = App <$> strengthenRec k m n a <*> strengthenRec k m n b+  strengthenRec k m n (Pair a b) = Pair <$> strengthenRec k m n a <*> strengthenRec k m n b+  strengthenRec k m n (Sigma a b) = Sigma <$> strengthenRec k m n a <*> strengthenRec k m n b+  strengthenRec k m n (Match b) = Match <$> List.mapM (strengthenRec k m n) b+  strengthenRec k m n (Annot a t) = Annot <$> strengthenRec k m n a <*> strengthenRec k m n t+  -}++instance Strengthen (Pat p) where+  strengthenRec k m n PVar = pure PVar+  strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) (PPair (p1 :: Pat p1 (k + (m + n)))+    (p2 :: Pat p2 (p1 + (k + (m + n))))) =+      case (axiomAssoc @p1 @k @(m + n),+            axiomAssoc @p1 @k @n) of+       (Refl, Refl) ->+         let r = strengthenRec (sPlus (size p1) k) m n p2 in+         PPair <$> strengthenRec k m n p1 <*> r+  strengthenRec k m n (PAnnot p1 e2) = PAnnot <$> strengthenRec k m n p1 <*> strengthenRec k m n e2++instance Strengthen Branch where+  strengthenRec k m n (Branch bnd) = Branch <$> strengthenRec k m n bnd+----------------------------------------------+-- Some Examples+----------------------------------------------++star :: Exp n+star = Star++-- No annotation on the binder+lam :: Exp (S n) -> Exp n+lam b = Match [Branch (Scoped.bind PVar b)]++-- Annotation on the binder+alam :: Exp n -> Exp (S n) -> Exp n+alam t b = Match [Branch (Scoped.bind (PAnnot PVar t) b)]++-- The identity function "λ x. x". With de Bruijn indices+-- we write it as "λ. 0", though with `Match` it looks a bit different+t0 :: Exp Z+t0 = lam (Var f0)++-- A larger term "λ x. λy. x (λ z. z z)"+-- λ. λ. 1 (λ. 0 0)+t1 :: Exp Z+t1 =+  lam+    ( lam+        (Var f1 `App` lam (Var f0 `App` Var f0))+    )++-- To show lambda terms, we can write a simple recursive instance of+-- Haskell's `Show` type class. In the case of a binder, we use the `unbind`+-- operation to access the body of the lambda expression.++-- >>> t0+-- λ_. 0++-- >>> t1+-- λ_. (λ_. (1 (λ_. (0 0))))++-- Polymorphic identity function and its type++tyid = Pi star (bind1 (Pi (Var f0) (bind1 (Var f1))))++tmid = lam (lam (Var f0))++-- >>> tyid+-- Pi *. 0 -> 1++-- >>> tmid+-- λ_. (λ_. 0)++--------------------------------------------------------++-- * Show instances++--------------------------------------------------------+++instance Show (Exp n) where+  showsPrec :: Int -> Exp n -> String -> String+  showsPrec _ Star = showString "*"+  showsPrec d (Pi a b)+    | appearsFree FZ (getBody1 b) =+        showParen (d > 9) $+          showString "Pi "+            . shows a+            . showString ". "+            . shows (getBody1 b)+    | otherwise =+        showParen (d > 9) $+          showsPrec 11 a+            . showString " -> "+            . showsPrec 9 (getBody1 b)+  showsPrec d (Sigma a b)+    | appearsFree FZ (getBody1 b) =+        showParen (d > 9) $+          showString "Sigma "+            . shows a+            . showString ". "+            . shows (getBody1 b)+    | otherwise =+        showParen (d > 9) $+          showsPrec 11 a+            . showString " * "+            . showsPrec 9 (getBody1 b)+  showsPrec _ (Var x) = shows x+  showsPrec d (App e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString " "+        . showsPrec 11 e2+  showsPrec d (Pair e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString ", "+        . showsPrec 11 e2+  showsPrec d (Match [b]) =+    showParen (d > 9) $+      showString "λ"+        . showsPrec 9 b+  showsPrec d (Match b) =+    showParen (d > 10) $+      showString "match"+        . showsPrec 10 b+  showsPrec d (Annot a t) =+    showParen (d > 10) $+      showsPrec 10 a+        . showString " : "+        . showsPrec 10 t++instance Show (Branch b) where+  showsPrec d (Branch b) =+    showsPrec 10 (Scoped.getPat b)+      . showString ". "+      . showsPrec 11 (Scoped.getBody b)++instance Show (Pat p n) where+  showsPrec d PVar = showString "_"+  showsPrec d (PPair e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString ", "+        . showsPrec 11 e2+  showsPrec d (PAnnot e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString " : "+        . showsPrec 11 e2++--------------------------------------------------------++-- * Alpha equivalence++--------------------------------------------------------+++-- The derivable equality instance is alpha-equivalence+deriving instance (Eq (Exp n))++instance PatEq (Pat p1 n) (Pat p2 n) where+  patEq :: Pat p1 n -> Pat p2 n -> Maybe (p1 :~: p2)+  patEq PVar PVar = Just Refl+  patEq (PPair p1 p2) (PPair p1' p2') = do+    Refl <- patEq p1 p1'+    Refl <- patEq p2 p2'+    return Refl+  patEq (PAnnot p1 p2) (PAnnot p1' p2') = do+    Refl <- patEq p1 p1'+    guard (p2 == p2')+    return Refl+  patEq _ _ = Nothing++-- This equality is not derivable+instance Eq (Branch n) where+  (==) :: Branch n -> Branch n -> Bool+  (Branch (p1 :: Scoped.Bind Exp Exp (Pat m1) n))+    == (Branch (p2 :: Scoped.Bind Exp Exp (Pat m2) n)) =+      case testEquality+        (size (Scoped.getPat p1) :: SNat m1)+        (size (Scoped.getPat p2) :: SNat m2) of+        Just Refl -> p1 == p2+        Nothing -> False+++--------------------------------------------------------++-- * big-step evaluation++--------------------------------------------------------++-- We can write the usual operations for evaluating+-- lambda terms to values++-- >>> eval t1+-- λ_. (λ_. (1 (λ_. (0 0))))++-- >>> eval (t1 `App` t0)+-- λ_. ((λ_. 0) (λ_. (0 0)))++eval :: Exp n -> Exp n+eval (Var x) = Var x+eval (Match b) = Match b+eval (App e1 e2) =+  let v = eval e2+   in case eval e1 of+        Match b -> case findBranch v b of+          Just e -> eval e+          Nothing -> error "pattern match failure"+        t -> App t v+eval Star = Star+eval (Pi a b) = Pi a b+eval (Sigma a b) = Sigma a b+eval (Annot a t) = eval a+eval (Pair a b) = Pair a b++-- small-step evaluation++-- >>> step (t1 `App` t0)+-- Just (λ_. (λ_. 0 (λ_. (0 0))))++step :: Exp n -> Maybe (Exp n)+step (Var x) = Nothing+step (Match b) = Nothing+step (App (Match bs) e2)+  | Just r <- findBranch e2 bs =+      Just r+step (App e1 e2)+  | Just e1' <- step e1 = Just (App e1' e2)+  | Just e2' <- step e2 = Just (App e1 e2')+  | otherwise = Nothing+step Star = Nothing+step (Pi a b) = Nothing+step (Sigma a b) = Nothing+step (Pair a b) = Nothing+step (Annot a t) = step a++eval' :: Exp n -> Exp n+eval' e+  | Just e' <- step e = eval' e'+  | otherwise = e++----------------------------------------------------------------+-- Check for equality+----------------------------------------------------------------+data Err where+  NotEqual :: Exp n -> Exp n -> Err+  PiExpected :: Exp n -> Err+  PiExpectedPat :: Pat p1 n1 -> Err+  SigmaExpected :: Exp n -> Err+  VarEscapes :: Exp n -> Err+  PatternMismatch :: Pat p1 n1 -> Pat p2 n2 -> Err+  PatternTypeMismatch :: Pat p1 n1 -> Exp n1 -> Err+  AnnotationNeeded :: Exp n -> Err+  AnnotationNeededPat :: Pat p1 n1 -> Err++deriving instance (Show Err)++-- find the head form+whnf :: Exp n -> Exp n+whnf (App a1 a2) = case whnf a1 of+  Match bs -> case findBranch (eval a2) bs of+    Just b -> whnf b+    Nothing -> App (Match bs) a2+  t -> App t a2+whnf (Annot a t) = whnf a+whnf a = a++equate :: (MonadError Err m) => Exp n -> Exp n -> m ()+equate t1 t2 = do+  let n1 = whnf t1+      n2 = whnf t2+  equateWHNF n1 n2++equatePat ::+  (MonadError Err m) =>+  Pat p1 n ->+  Pat p2 n ->+  m ()+equatePat PVar PVar = pure ()+equatePat (PPair p1 p1') (PPair p2 p2')+  | Just Refl <- testEquality (size p1) (size p2) =+        equatePat p1 p2 >> equatePat p1' p2'+equatePat (PAnnot p1 e1) (PAnnot p2 e2) =+  equatePat p1 p2 >> equate e1 e2+equatePat p1 p2 = throwError (PatternMismatch p1 p2)++equateBranch :: (MonadError Err m) => Branch n -> Branch n -> m ()+equateBranch (Branch b1) (Branch b2) =+  let p1 = Scoped.getPat b1+      p2 = Scoped.getPat b2+      body1 = Scoped.getBody b1+      body2 = Scoped.getBody b2 +  in+      case testEquality (size p1) (size p2) of+        Just Refl ->+          equatePat p1 p2 >> equate body1 body2+        Nothing ->+          throwError (PatternMismatch (Scoped.getPat b1) (Scoped.getPat b2))++equateWHNF :: (MonadError Err m) => Exp n -> Exp n -> m ()+equateWHNF n1 n2 =+  case (n1, n2) of+    (Star, Star) -> pure ()+    (Var x, Var y) | x == y -> pure ()+    (Match b1, Match b2) ->+      List.zipWithM_ equateBranch b1 b2+    (App a1 a2, App b1 b2) -> do+      equateWHNF a1 b1+      equate a2 b2+    (Pi tyA1 b1, Pi tyA2 b2) -> do+      equate tyA1 tyA2+      equate (getBody1 b1) (getBody1 b2)+    (Sigma tyA1 b1, Sigma tyA2 b2) -> do+      equate tyA1 tyA2+      equate (getBody1 b1) (getBody1 b2)+    (_, _) -> throwError (NotEqual n1 n2)++----------------------------------------------------------------++-- * Type checking++----------------------------------------------------------------+++inferPattern ::+  (MonadError Err m) =>+  Ctx Exp n -> -- input context+  Pat p n -> -- pattern to check+  m (Ctx Exp (p + n), Exp (p + n), Exp n)+inferPattern g (PAnnot p ty) = do+  (g', e) <- checkPattern g p ty+  pure (g', e, ty)+inferPattern g p = throwError (AnnotationNeededPat p)++-- | type check a pattern and produce an extended typing context,+-- plus expression form of the pattern (for dependent pattern matching)+checkPattern ::+  (MonadError Err m) =>+  Ctx Exp n -> -- input context+  Pat p n -> -- pattern to check+  Exp n -> -- expected type of pattern (should be in whnf)+  m (Ctx Exp (p + n), Exp (p + n))+checkPattern g PVar a = do+  pure (g +++ a, var f0)+checkPattern g (PPair (p1 :: Pat p1 n) (p2 :: Pat p2 (p1 + n))) (Sigma tyA tyB) = do+  -- need to know that Plus is associative+  case axiomAssoc @p2 @p1 @n of+    Refl -> do+      (g', e1) <- checkPattern g p1 tyA+      let tyB' = weakenBind' (size p1) tyB+      let tyB'' = whnf (instantiate1 tyB' e1)+      (g'', e2) <- checkPattern g' p2 tyB''+      let e1' = weaken' (size p2) e1+      return (g'', Pair e1' e2)+checkPattern g p ty = do+  (g', e, ty') <- inferPattern g p+  equate ty ty'+  return (g', e)++-----------------------------------------------------------+-- Checking branches+-----------------------------------------------------------++--      G |- p : A => G'      G' |- b : B { p / x}+--   ----------------------------------------------+--       G |- p => b : Pi x : A . B++checkBranch ::+  (MonadError Err m) =>+  Ctx Exp n ->+  Exp n ->+  Branch n ->+  m ()+checkBranch g (Pi tyA tyB) (Branch bnd) = do+    let pat  = Scoped.getPat bnd+    let body = Scoped.getBody bnd+    let p    = size pat++    -- find the extended context and pattern expression+    (g', a) <- checkPattern g pat tyA++    -- shift tyB to the scope of the pattern and instantiate it with 'a'+    -- must be done simultaneously because 'a' is from a larger scope+    let tyB' = applyE (a .: shiftNE p) (getBody1 tyB)++    -- check the body of the branch in the scope of the pattern+    checkType g' body tyB'+checkBranch g t e = throwError (PiExpected t)++-- should only check with a type in whnf+checkType ::+  (MonadError Err m) =>+  Ctx Exp n ->+  Exp n ->+  Exp n ->+  m ()+checkType g (Pair a b) ty = do+  tyA <- inferType g a+  tyB <- inferType g b+  case ty of+    (Sigma tyA tyB) -> do+      checkType g a tyA+      checkType g b (instantiate1 tyB a)+    _ -> throwError (SigmaExpected ty)+checkType g (Match bs) ty = do+  List.mapM_ (checkBranch g ty) bs+checkType g e t1 = do+  t2 <- inferType g e+  equate (whnf t2) t1++-- | infer the type of an expression. This type may not+-- necessarily be in whnf+inferType ::+  (MonadError Err m) =>+  Ctx Exp n ->+  Exp n ->+  m (Exp n)+inferType g (Var x) = pure (applyEnv g x)+inferType g Star = pure star+inferType g (Pi a b) = do+  checkType g a star+  checkType (g +++ a) (getBody1 b) star+  pure star+inferType g (App a b) = do+  tyA <- inferType g a+  case whnf tyA of+    Pi tyA1 tyB1 -> do+      checkType g b tyA1+      pure $ instantiate1 tyB1 b+    t -> throwError (PiExpected t)+inferType g (Sigma a b) = do+  checkType g a star+  checkType (g +++ a) (getBody1 b) star+  pure star+inferType g a =+  throwError (AnnotationNeeded a)++-- >>> tmid+-- λ_. (λ_. 0)++-- >>> tyid+-- Pi *. 0 -> 1++-- >>> :t tyid+-- tyid :: Exp n++-- >>> (checkType zeroE tmid tyid :: Either Err ())+-- Right ()+++-- >>> (inferType zeroE (App tmid tyid) :: Either Err (Exp N0))+-- Left (AnnotationNeeded (λ_. (λ_. 0)))
+ examples/HOAS.hs view
@@ -0,0 +1,93 @@++module HOAS where++{-+This module demonstrates how to layer a HOAS-based representation+on top of a de Bruijn representation, to make it easier to generate well scoped+lambda terms.++It is based on Conor McBride's "Classy Hack"+https://mazzo.li/epilogue/index.html%3Fp=773.html++-}++import LC qualified+import Data.Fin+import Rebound.Bind.Single+import Rebound++-- Here are some HOAS lambda calculus terms++tru :: Tm Z+tru = Lam $ \x -> Lam $ \y -> Var x++fls :: Tm Z+fls = Lam $ \x -> Lam $ \y -> Var y++app :: Tm Z+app = Lam $ \f -> Lam $ \x -> App (Var f) (Var x)++omega :: Tm Z+omega = App delta delta where+    delta = Lam $ \x -> App (Var x) (Var x)++-- We can convert them to a de Bruijn-indexed+-- representation easily++-- >>> cvt tru+-- (λ. (λ. 1))++-- >>> cvt fls+-- (λ. (λ. 0))++-- >>> cvt app+-- (λ. (λ. (1 0)))++-- >>> cvt omega+-- ((λ. (0 0)) (λ. (0 0)))+++-- These terms are elements of the following datatype+-- that uses a form of "weak higher-order abstract syntax"+-- for variable binding. A type class constraint in the variable+-- constructor constructs the appropriate de Bruijn index.+data Tm (a :: Nat) where+  Var :: (b ⊆ a) => Proxy b -> Tm a+  App :: Tm a -> Tm a -> Tm a+  Lam :: (Proxy (S a) -> Tm (S a)) -> Tm a++instance Cvt Tm LC.Exp where+  cvt :: Tm m -> LC.Exp m+  cvt (Var x)   = LC.Var (cvtVar x)+  cvt (App a b) = LC.App (cvt a) (cvt b)+  cvt (Lam f)   = LC.Lam (cvtBind f)++------------------------------------------------------------+-- The rest of this file is independent of the language that we are using+-- and can be called reusable "library" code+-- It depends on overlapping instances++-- Conversion type class+class Cvt t u | t -> u where+  cvt :: t m -> u m++class (b :: Nat) ⊆ (a :: Nat) where+    inj :: Fin b -> Fin a+instance {-# OVERLAPPING #-} n ⊆ n where inj = id+instance {-# OVERLAPPING #-} (o ~ S n, m ⊆ n) => m ⊆ o where inj = FS . inj++-- Note: you don't actually need overlapping instances for this example:+--- instance n ⊆ n where inj = id+--- instance n ⊆ S n where inj = FS+-- would work just as well++newtype Proxy b = P (Fin b)++zeroVar :: Proxy (S b)+zeroVar = P FZ++cvtVar :: (b ⊆ a) => Proxy b -> Fin a+cvtVar (P x) = inj x++cvtBind :: (Subst v u, Cvt t u) => (Proxy (S a) -> t (S a)) -> Bind v u a+cvtBind f = bind (cvt (f zeroVar))
+ examples/LC.hs view
@@ -0,0 +1,268 @@+-- |+-- Module      : LC+-- Description : Untyped lambda calculus+-- Stability   : experimental+--+-- An implementation of the untyped lambda calculus including evaluation+-- and small-step reduction.+--+-- This module demonstrates the use of well-scoped lambda calculus terms using `Rebound`.+-- The natural number index `n` is the scoping level -- a bound on the number+-- of free variables that can appear in the term. If `n` is 0, then the+-- term must be closed.+module LC where++import Data.Fin+import Data.Vec qualified+import Rebound+import Rebound.Bind.Single+import Data.Fin+import Data.Vec qualified+import qualified Data.Maybe as Maybe++-- | Datatype of well-scoped lambda-calculus expressions+--+-- The @Var@ constructor of this datatype takes an index that must+-- be strictly less than the bound. Note that the type `Fin (S n)`+-- has `n` different elements.++-- The @Lam@ constructor binds a variable, using the the type `Bind`+-- from the library. The type arguments state that the binder is+-- for a single expression variable, inside an expression term, that may+-- have at most `n` free variables.+data Exp (n :: Nat) where+  Var :: Fin n -> Exp n+  Lam :: Bind Exp Exp n -> Exp n+  App :: Exp n -> Exp n -> Exp n+    deriving (Generic1)++ ++----------------------------------------------+-- Example lambda-calculus expressions+----------------------------------------------++-- To make it easier to construct lambda calculus+-- expressions, we'll first define some helper+-- definitions++-- | a lambda expression+lam :: Exp (S n) -> Exp n+lam = Lam . bind+-- | an application expression+(@@) :: Exp n -> Exp n -> Exp n+(@@) = App+-- | variable with index 0+v0 :: Exp (S n)+v0 = Var f0+-- | variable with index 1+v1 :: Exp (S (S n))+v1 = Var f1+++-- | The identity function "λ x. x".+-- With de Bruijn indices we write it as "λ. 0"+t0 :: Exp Z+t0 = lam v0++-- >>> t0+-- (λ. 0)+++-- For example, we can write+-- (λx. ((x ((λy. y) x)) (λz. z)))+-- using this term with de Bruijn indices+-- (λ. ((0 ((λ. 0) 0)) (λ. 0)))+-- and then construct it with the definitions above+t :: Exp Z+t = lam ((v0 @@ ((lam v0) @@ v0)) @@ (lam v0))++----------------------------------------------+-- (Alpha-)Equivalence+----------------------------------------------++-- The nice thing about de Bruijn indices is that+-- we can use structural equality as alpha equivalence.+-- The built-in Eq instance for Bind, makes sure that +-- the delayed substitutions are not observable here.+deriving instance Eq (Exp n)+++----------------------------------------------+-- Substitution+----------------------------------------------++-- To work with this library, we need two type class instances.+-- First, we tell the library how to construct variables in the expression+-- type. This class is necessary to construct an indentity+-- substitution---one that maps each variable to itself.+instance SubstVar Exp where+  var :: Fin n -> Exp n+  var = Var++-- Second, the operation `applyE` applies an environment+-- (explicit substitution) to an expression, and can be+-- automatically generated by the `Subst` type class, as+-- long as it can identify the variable constructor.+-- (Insead of generic programming, this operation can also+-- be written explicitly.)++instance Subst Exp Exp where+  isVar (Var x) = Just (Refl, x)+  isVar _ = Nothing+++----------------------------------------------+-- Display (Show)+----------------------------------------------++-- | To show lambda terms, we use a simple recursive instance of+-- Haskell's `Show` type class. In the case of a binder, we use the `getBody`+-- operation to access the body of the lambda expression.+instance Show (Exp n) where+  showsPrec :: Int -> Exp n -> String -> String+  showsPrec _ (Var x) = shows x+  showsPrec d (App e1 e2) =+    showParen True $+      showsPrec 10 e1+        . showString " "+        . showsPrec 11 e2+  showsPrec d (Lam b) =+    showParen True $+      showString "λ. "+        . shows (getBody b)++-----------------------------------------------+-- (big-step) evaluation+-----------------------------------------------++-- | Calculate the value of a lambda-calculus expression+-- This function looks like it uses call-by-value evaluation:+-- in an application it evaluates the argument `e2` before+-- using the `instantiate` function from the library to substitute+-- the bound variable of `Bind` by v. However, this is Haskell,+-- a lazy language, so that result won't be evaluated unless the+-- function actually uses its argument.+eval :: Exp Z -> Exp Z+eval (Var x) = case x of {}+eval (Lam b) = Lam b+eval (App e1 e2) =+  let v = eval e2+   in case eval e1 of+        Lam b -> eval (instantiate b v)+        t -> App t v+++-- >>> t0+-- (λ. 0)++-- >>> eval (t `App` t0)+-- (λ. 0)++-- ((λ. (λ. 1)) ((λ. 0) (λ. 0)))++t2 = App (Lam (bind (Lam (bind (Var f1)))))+         (App (Lam (bind (Var f0))) (Lam (bind (Var f0))))++-- >>> t2+-- ((λ. (λ. 1)) ((λ. 0) (λ. 0)))++-- >>> eval t2+-- (λ. (λ. 0))++----------------------------------------------+-- small-step evaluation+----------------------------------------------++-- | Do one step of evaluation, if possible+-- If the function is already a value or is stuck+-- this function returns `Nothing`+step :: Exp n -> Maybe (Exp n)+step (Var x) = Nothing+step (Lam b) = Nothing+step (App (Lam b) e2) = Just (instantiate b e2)+step (App e1 e2)+  | Just e1' <- step e1 = Just (App e1' e2)+  | Just e2' <- step e2 = Just (App e1 e2')+  | otherwise = Nothing++-- | Evaluate the term as much as possible+eval' :: Int -> Exp n -> Maybe (Exp n)+eval' 0 e = Nothing+eval' k e = case step e of+              Just e' -> eval' (k - 1) e'+              Nothing -> Just e++-- >>> step (t0 `App` t0)+-- Just (λ. 0)++-- >>> eval' 5 (t `App` t0)+-- Just (λ. 0)+++--------------------------------------------------------+-- full normalization+--------------------------------------------------------++-- | Calculate the normal form of a lambda expression. This+-- is like evaluation except that it also reduces underneath+-- the binders of @Lam@ expressions. There, we must first `getBody`+-- the binder and then rebind when finished+nf :: Exp n -> Exp n+nf (Var x) = Var x+nf (Lam b) = Lam (bind (nf (getBody b)))+nf (App e1 e2) =+  case nf e1 of+    Lam b -> nf (instantiate b e2)+    t -> App t (nf e2)++--------------------------------------------------------+-- weak-head normalization / full reduction+--------------------------------------------------------++nf1 :: Exp n -> Exp n+nf1 (Var x) = Var x+nf1 (Lam b) = Lam (bind (nf1 (getBody b)))+nf1 (App e1 e2) =+  case whnf e1 of+    Lam b -> nf1 (instantiate b (whnf e2))+    t -> App t (nf e2)++whnf :: Exp n -> Exp n+whnf (Var x) = Var x+whnf (Lam b) = Lam b+whnf (App e1 e2) =+  case nf e1 of+    Lam b -> nf (instantiate b (whnf e2))+    t -> App t (nf e2)++--------------------------------------------------------+-- environment based evaluation / normalization+--------------------------------------------------------++-- invariant: expressions in the range of the environment are in whnf+whnfEnv :: Env Exp m n -> Exp m -> Exp n+whnfEnv r (Var x) = applyEnv r x+whnfEnv r (Lam b) = applyE r (Lam b)+whnfEnv r (App f a) =+  case whnfEnv r f of+     Lam b ->+       instantiateWith b (whnfEnv r a) whnfEnv+        -- unbindWith b (\r' e' -> whnfEnv (whnfrEnv r a .: r') e')+     f' -> App f' (applyE r a)++-- >>> whnfEnv zeroE t     -- start with "empty environment"+-- (λ. ((0 ((λ. 0) 0)) (λ. 0)))++-- For full reduction, we need to normalize under the binder too.+nfEnv :: Exp n -> Exp n+nfEnv (Var x) = Var x+nfEnv (Lam b) = Lam (bind (nfEnv (getBody b)))+nfEnv (App f a) =+   case whnfEnv idE f of+        Lam b -> nfEnv (instantiate b (whnfEnv idE a))+        f' -> App (nfEnv f') (nfEnv a)++++----------------------------------------------------------------
+ examples/LCLet.hs view
@@ -0,0 +1,279 @@+-- |+-- Module      : LC+-- Description : Untyped lambda calculus+-- Stability   : experimental+--+-- An implementation of the untyped lambda calculus including let, letrec,+-- mutual letrec and let* expressions.+-- TODO: add example terms and fix Show instance+module LCLet where++import Rebound+import Rebound.Bind.Single+import qualified Rebound.Bind.Pat as Pat+import Rebound.Bind.PatN as PatN (BindN, bindN, instantiateN, getBodyN)+import Data.Fin+import Data.Vec qualified as Vec++-- | Datatype of well-scoped lambda-calculus expressions+data Exp (n :: Nat) where+  Var :: Fin n -> Exp n+  Lam :: Bind Exp Exp n -> Exp n+  App :: Exp n -> Exp n -> Exp n+  Let ::+    -- | single let expression+    -- "let x = e1 in e2" where x is bound in e2+    Exp n ->+    (Bind Exp Exp n) ->+    Exp n+  LetRec ::+    -- | "let rec x = e1 in e2" where x is bound in both e1 and e2+    Rec n ->+    Exp n+  LetTele ::+    -- | sequence of nested lets, where each one may depend on+    -- the previous binding+    -- "let x1 = e1 in x2 = e2 in ... in e" where x1 is bound+    -- in e2, e3 ... and e, x2 is bound in e3 and e, etc.+    Tele n ->+    Exp n+  LetMutRec ::+    -- | mutual recursive lets, where each one may depend on+    -- any other variable+    -- "let x1 = e1 in x2 = e2 in ... in e" where x1 ... xn+    -- are bound in e1, e2, e3 ... and e+    MutRec n ->+    Exp n++data Rec n =+  Rec { rec_rhs  :: Bind Exp Exp n,   -- single RHS+        rec_body :: Bind Exp Exp n }  -- body of let++data MutRec n = forall m. SNatI m =>+  MutRec { mutrec_rhss :: Vec m (BindN Exp Exp m n), -- Vector of RHSs+           mutrec_body :: BindN Exp Exp m n  -- body of let+           }++data Tele n where+  LetStar :: Exp n -> Bind Exp Tele n -> Tele n+  Body :: Exp n -> Tele n++----------------------------------------------+-- Example lambda-calculus expressions+----------------------------------------------++-- some variables+v0 :: Exp (S n)+v0 = Var f0+v1 :: Exp (S (S n))+v1 = Var f1+v2 :: Exp (S (S (S n)))+v2 = Var f2+-- | an application expression+(@@) :: Exp n -> Exp n -> Exp n+(@@) = App+-- | a lambda expression+lam :: Exp (S n) -> Exp n+lam = Lam . bind++letrec :: Exp (S n) -> Exp (S n) -> Exp n+letrec e1 e2 = LetRec (Rec (bind e1) (bind e2))++letstar :: Exp n -> Tele (S n) -> Tele n+letstar e t = LetStar e (bind t)++-- | The identity function "λ x. x".+-- With de Bruijn indices we write it as "λ. 0"+-- The `bind` function creates the binder+-- t0 :: Exp Z+t0 = lam v0++-- >>> t0+-- (λ. 0)++-- | A larger term "λ x. λy. x ((λ z. z) y)"+-- λ. λ. 1 ((λ. 0) 0))+t1 :: Exp Z+t1 = lam (lam (v1 @@ ((lam v0) @@ v0)))++-- >>> t1+-- (λ. (λ. (1 ((λ. 0) 0))))++-- let x = \y.y in x x+t2 :: Exp Z+t2 = Let t0 (bind (App v0 v0))++-- >>> t2+-- (let (λ. 0) in (0 0))++-- let rec fix = \f. f (fix f) in f+t3 :: Exp Z+t3 = letrec (lam (v0 @@(v1 @@ v0))) v0+-- >>> t3+-- (let rec (λ. (0 (1 0))) in 0)++-- let* x1 = \x.x ; x2 = x1 x1 ; x3 = x2 s1 in x3 x2 x1+t4 = LetTele+       (letstar t0+         (letstar (v0 @@ v0)+            (letstar (v0 @@ v1)+              (Body ((v0 @@ v1) @@ v2)))))++-- >>> t4+-- <let-tele>++----------------------------------------------+-- (Alpha-)Equivalence+----------------------------------------------++-- | The derivable equality instance+-- is alpha-equivalence+deriving instance (Eq (Exp n))++deriving instance (Eq (Tele n))++deriving instance (Eq (Rec n))++instance Eq (MutRec n) where+  (==) :: MutRec n -> MutRec n -> Bool+  MutRec { mutrec_rhss= (rhss1 :: Vec m1 t1), mutrec_body=body1} ==+    MutRec { mutrec_rhss= (rhss2 :: Vec m2 t2), mutrec_body=body2}+    = case testEquality (snat @m1) (snat @m2) of+       Just Refl -> Vec.all2 (==) rhss1 rhss2 && body1 == body2+       Nothing -> False+----------------------------------------------+-- Substitution+----------------------------------------------++-- To work with this library, we need two type class instances.++-- | Tell the library how to construct variables in the expression+-- type. This class is necessary to construct an indentity+-- substitution---one that maps each variable to itself.+instance SubstVar Exp where+  var :: Fin n -> Exp n+  var = Var++-- The library represents a substitution using an "Environment".+-- The type `Env Exp n m` is a substitution that can be applied to+-- indices bounded by n. It produces a result `Exp` with indices+-- bounded by m. The function `applyEnv` looks up a mapping in+-- an environment.++-- | The operation `applyE` applies an environment+-- (explicit substitution) to an expression.+--+-- The implementation of this operation applies the environment to+-- variable index in the variable case. All other caseas follow+-- via recursion. The library includes a type class instance for+-- the Bind type which handles the variable lifting needed under+-- the binder.+instance Shiftable Exp where+  shift = shiftFromApplyE @Exp+instance Subst Exp Exp where+  applyE :: Env Exp n m -> Exp n -> Exp m+  applyE r (Var x) = applyEnv r x+  applyE r (Lam b) = Lam (applyE r b)+  applyE r (App e1 e2) = App (applyE r e1) (applyE r e2)+  applyE r (Let e1 e2) = Let (applyE r e1) (applyE r e2)+  applyE r (LetRec e) = LetRec (applyE r e)+  applyE r (LetTele e) = LetTele (applyE r e)+  applyE r (LetMutRec e) = LetMutRec (applyE r e)++instance Subst Exp Rec where+  applyE r (Rec rhs body) = Rec (applyE r rhs) (applyE r body)++instance Shiftable Tele where+  shift = shiftFromApplyE @Exp+instance Subst Exp Tele where+  applyE r (Body e) = Body (applyE r e)+  applyE r (LetStar e1 e2) = LetStar (applyE r e1) (applyE r e2)++instance Subst Exp MutRec where+  applyE r (MutRec rhss body) =+    MutRec (fmap (applyE r) rhss) (applyE r body)++----------------------------------------------+-- Display (Show)+----------------------------------------------++-- | To show lambda terms, we use a simple recursive instance of+-- Haskell's `Show` type class. In the case of a binder, we use the `getBody`+-- operation to access the body of the lambda expression.+instance Show (Exp n) where+  showsPrec :: Int -> Exp n -> String -> String+  showsPrec _ (Var x) = shows x+  showsPrec d (App e1 e2) =+    showParen True $+      showsPrec 10 e1+        . showString " "+        . showsPrec 11 e2+  showsPrec d (Lam b) =+    showParen True $+      showString "λ. "+        . shows (getBody b)+  showsPrec d (Let e1 e2) =+    showParen True $+      showString "let "+        . showsPrec 10 e1+        . showString " in "+        . shows (getBody e2)+  showsPrec d (LetRec (Rec{rec_rhs=rhs,rec_body=body})) =+    showParen True $+      showString "let rec "+        . shows (getBody rhs)+        . showString " in "+        . shows (getBody body)+  showsPrec d (LetTele e) = showString "<let-tele>"+  showsPrec d (LetMutRec (MutRec {mutrec_rhss=rhss, mutrec_body=body})) =+    showParen True $+      showString "let rec "+        . showString " rhss " -- (getBodyN e1)+        . showString " in "+        . shows (getBodyN body)+-----------------------------------------------+-- (big-step) evaluation+-----------------------------------------------++-- >>> eval t1+-- (λ. (λ. (1 ((λ. 0) 0))))++-- >>> eval (t1 @@ t0)+-- (λ. ((λ. 0) ((λ. 0) 0)))++-- >>> eval t2+-- (λ. 0)++-- This one is an infinite loop+-- >>> eval t3+-- ProgressCancelledException++-- >>> eval t4+-- (λ. 0)++eval :: Exp n -> Exp n+eval (Var x) = Var x+eval (Lam b) = Lam b+eval (App e1 e2) =+  let v = eval e2+   in case eval e1 of+        Lam b -> eval (instantiate b v)+        t -> App t v+eval (Let e1 e2) =+  eval (instantiate e2 (eval e1))+eval (LetRec e) =+  -- use a Haskell recursive definition+  -- to tie the knot for a recursive definition+  -- in the object language+  let v = instantiate (rec_rhs e) v+   in eval (instantiate (rec_body e) v)+eval (LetTele e) = evalTele e+eval (LetMutRec (MutRec { mutrec_rhss = rhss, mutrec_body = body})) =+  -- use a Haskell recursive definition+  let vs = fmap (\b -> instantiateN b vs) rhss+  in eval (instantiateN body vs)++evalTele :: Tele n -> Exp n+evalTele (Body e) = eval e+evalTele (LetStar e t) =+  evalTele (instantiate t (eval e))
+ examples/LCQC.hs view
@@ -0,0 +1,86 @@+-- |+-- Module      : LCQC+-- Description : Generators for well-scoped lambda calculus terms+-- Stability   : experimental+--+-- This module demonstrates the use of well-scoped lambda calculus terms+-- with QuickCheck. It then demonstrates how to use QC to test the normalization+-- functions in the `LC` module.+module LCQC where++import LC+import Test.QuickCheck+import Rebound+import Rebound.Bind.Single+import Data.Fin+import Data.Maybe as Maybe++----------------------------------------------+-- Generating well-scoped expressions+----------------------------------------------++-- | Generate an expression in scope `n`, using+-- size parameter sz+-- >>> sample' (genExp s3 10)+-- [(λ. (λ. (0 2))),(((λ. 0) (1 2)) ((0 2) 2)),(((2 1) 0) (1 1)),1,((λ. 2) (2 (λ. 1))),(λ. 2),2,0,((λ. (0 1)) (λ. (1 3))),(((1 2) 2) (λ. (0 2))),(λ. 2)]+genExp :: forall n. SNat n -> Int -> Gen (Exp n)+genExp n sz =+    let+        genLam = Lam <$> (bind <$> genExp (next n) (sz `div` 2))+        genApp = App <$> genExp n (sz `div` 2) <*> genExp n (sz `div` 2)+    in+    case snat_ n of+       SZ_ -> if sz <= 1+                then pure $ Lam (bind (Var 0))  -- smallest closed term+                else oneof [genLam, genApp]     -- closed term, no vars+       SS_ x ->+         let+            genVar = withSNat x $ elements $ map Var universe+         in+            if sz <= 1+              then genVar+              else oneof [genVar, genLam, genApp]++-- | shrink a lambda calculus term, maintaining the same scope.+shrinkExp :: SNatI n => Exp n -> [Exp n]+shrinkExp (Var FZ) = []+shrinkExp (Var x ) = [ Var (pred x) ]+shrinkExp (Lam t)  = [ Lam (bind t') | t' <- shrinkExp (getBody t) ]+shrinkExp (App f a) =+  [f,a] ++ [ App f' a | f' <- shrinkExp f]+        ++ [ App f a' | a' <- shrinkExp a]++-- | arbitrary instance for lambda calculus terms+instance SNatI n => Arbitrary (Exp n) where+  arbitrary :: SNatI n => Gen (Exp n)+  arbitrary = sized (genExp snat)+  shrink :: SNatI n => Exp n -> [Exp n]+  shrink = shrinkExp+++----------------------------------------------+-- Property-based testing example+----------------------------------------------++{-++Let's use QuickCheck to make sure that our various+normalization functions for the lambda calculus all produce the+same result.++However, we need to deal with the fact that not all lambda+calculus terms normalize. Therefore, we will instruct QC to discard+the test case if the expression does not normalize within 0.1 seconds.+We will also discard expressions that are already in normal form.+-}++prop_normalize :: (Exp n -> Exp n) -> Exp n -> Property+prop_normalize f e = discardAfter 100000 $+    e /= e' ==> e' == f e+   where e' = nf e++prop_nf1 :: Exp Z -> Property+prop_nf1 = prop_normalize nf1++prop_nfEnv :: Exp Z -> Property+prop_nfEnv = prop_normalize nfEnv
+ examples/LinLC.hs view
@@ -0,0 +1,214 @@+-- |+-- Module       : LinLC+-- Description  : Linear simply typed lambda calculus+-- Stability    : experimental+--+-- A typechecker for a linear lambda calculus. This module demonstrates the+-- usage of the `ScopedState` monad, which can be used when a typing context+-- has to be threaded during typechecking.+module LinLC where++import Control.Monad+import Control.Monad.Except+import Data.Fin+import Data.Vec as Vec hiding (bind)+import Rebound hiding (rescope)+import Rebound.Bind.Single hiding (rescope)+import Rebound.MonadScoped+import Prelude++-- | Run a monadic computation, then another, and return the result of the+-- first. Or, put another way: the reverse of `<<`.+(<<) :: (Monad m) => m a -> m b -> m a+l << r = do+  vl <- l+  r+  return vl++--------------------------------------------------------------------------------+--- Basic definitions+--------------------------------------------------------------------------------++-- | Represent the (current) usage of a variable.+data Usage where+  Unused :: Usage+  Used :: Usage+  deriving (Show, Eq)++-- | Representation of types.+data Ty where+  TyUnit :: Ty+  TyArrow :: Ty -> Ty -> Ty+  deriving (Show, Eq)++-- | Representation of terms.+data Exp (n :: Nat) where+  Var :: Fin n -> Exp n+  CUnit :: Exp n+  Lam :: Bind Exp Exp n -> Exp n+  App :: Exp n -> Exp n -> Exp n+  deriving (Eq, Generic1)++-- Some instances required by rebound. See LC.hs for more explanations.++instance SubstVar Exp where var = Var++instance Subst Exp Exp where+  isVar (Var x) = Just (Refl, x)+  isVar _ = Nothing++--------------------------------------------------------------------------------+--- Some helper-constructors+--------------------------------------------------------------------------------++-- | a lambda expression+lam :: Exp (S n) -> Exp n+lam = Lam . bind++-- | an application expression+(@@) :: Exp n -> Exp n -> Exp n+(@@) = App++-- | variable with index 0+v0 :: Exp (S n)+v0 = Var f0++-- | variable with index 1+v1 :: Exp (S (S n))+v1 = Var f1++-- | Notation for the arrow type+(~>) :: Ty -> Ty -> Ty+(~>) = TyArrow++infixr 8 ~>++--------------------------------------------------------------------------------+--- Typechecking infrastructure+--------------------------------------------------------------------------------++-- | A typing environment has to keep track of two things about variables:+-- 1. What their type is (`types`).+-- 2. Whether they've already been used or not (`usages`).+data TCEnv n = TCEnv+  { types :: Vec n Ty,+    usages :: Vec n Usage+  }++-- | The typechecking monad.+--+-- Unlike other calculi, the typing environment is not local. When two+-- sub-expressions have to be typechecked, the second sub-expression has to be+-- typechecked in the environment generated by the first sub-expression. Note+-- that this new environment will not include any new binding, but typing the+-- first sub-expression may have altered the usage of variables. This means that+-- `ScopedReader` cannot be used, as any changes done to the context are+-- forgotten when the scope is reverted. Hence, the `ScopedState` monad must be+-- used instead.+type TC n a = ScopedStateT TCEnv (Except String) n a++-- | Attempt to "consume" a variable, returning its type. Fails if the variable+-- was already used.+consumeVar :: Fin n -> TC n Ty+consumeVar i = setUsage i >> getsS ((! i) . types)+  where+    -- \| Set a variable to `Used`. Fails if the variable was already used.+    setUsage :: Fin n -> TC n ()+    setUsage i = do+      current <- getsS usages+      let (new, old) = set i Used current+      unless (old == Unused) $ throwError "Variable has already been used."+      modifyS $ \s -> s {usages = new}++    -- \| Set a value in the vector. Return the updated vector as well as the+    -- previous value.+    set :: Fin n -> t -> Vec n t -> (Vec n t, t)+    set FZ v (h ::: t) = (v ::: t, h)+    set (FS i) v (h ::: t) =+      let (t', v') = set i v t+       in (h ::: t', v')++-- | Add a variable to the scope.+--+-- Since the typing environment is threaded rather than passed down, as would be+-- the case with `ScopedReader`'s `localS`, we need to provide functions to both+-- enter a new scope, as with `localS`, and to leave it. Additionally, we need+-- to check that variables were used when they go out of scope.+addBinder :: Ty -> TC (S n) a -> TC n a+addBinder ty m = rescope enter leave (m << checkUsed FZ)+  where+    checkUsed :: Fin n -> TC n ()+    checkUsed i = do+      u <- getsS ((! i) . usages)+      unless (u == Used) $ throwError "Variable was not used."++    -- \| Add the binding in the scope.+    enter :: TCEnv n -> TCEnv (S n)+    enter e = e {types = ty ::: types e, usages = Unused ::: usages e}++    -- \| And remove it.+    leave :: TCEnv (S n) -> TCEnv n+    leave e = e {types = Vec.tail $ types e, usages = Vec.tail $ usages e}++-- | Run a computation in the typechecking monad, assuming that all free+-- variables need to be used.+runTC :: forall n a. (SNatI n) => Vec n Ty -> TC n a -> Either String a+runTC ts c = runExcept $ evalScopedStateT (c << checkAllUsed) initEnv+  where+    -- \| The initial environment, in which all variables are unused.+    initEnv :: TCEnv n+    initEnv = TCEnv {types = ts, usages = Vec.tabulate $ const Unused}++    -- \| Checks that all values are tagged as used.+    checkAllUsed :: TC n ()+    checkAllUsed = do+      us <- getsS usages+      let r = Vec.foldr (\u acc -> u == Used && acc) True us+      unless r $ throwError "Some variables in the initial scope were not used."++--------------------------------------------------------------------------------+--- Bi-directional typechecking+--------------------------------------------------------------------------------++-- Most of the unusual stuff about linear type systems is contained in the+-- handling of variables, which was implemented above. Hence the following code+-- should be rather unsurprising.++inferType :: Exp n -> TC n Ty+inferType (Var i) = consumeVar i+inferType CUnit = return TyUnit+inferType _ = throwError "Cannot infer type of this construct."++checkType :: Exp n -> Ty -> TC n ()+checkType (Lam bnd) ty = do+  let t = unbindl bnd+  (xTy, tTy) <- ensureArrow ty+  addBinder xTy $ checkType t tTy+  where+    ensureArrow :: Ty -> TC n (Ty, Ty)+    ensureArrow (TyArrow l r) = return (l, r)+    ensureArrow _ = throwError "Type is not arrow."+checkType (App f a) rTy = do+  aTy <- inferType a+  checkType f (TyArrow aTy rTy)+checkType t ty = do+  ty' <- inferType t+  unless (ty == ty') $ throwError "Inferred type does not match expected type."++-- >>> runTC empty $ checkType (lam $ v0) (TyUnit ~> TyUnit)+-- Right ()++-- >>> runTC empty $ checkType (lam $ lam $ v0 @@ v1) (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit)+-- Right ()++-- >>> runTC empty $ checkType (lam $ lam $ v1) (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit)+-- Left "Variable was not used."++-- >>> runTC empty $ checkType (lam $ lam $ v0) (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit)+-- Left "Inferred type does not match expected type."++-- >>> runTC empty $ checkType (lam $ lam $ v0) (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit ~> TyUnit)+-- Left "Variable was not used."++-- >>> runTC (TyUnit ::: (TyUnit ~> TyUnit) ::: TyUnit ::: Vec.empty) $ checkType (v1 @@ v0) (TyUnit)+-- Left "Some variables in the initial scope were not used."
+ examples/PTS.hs view
@@ -0,0 +1,439 @@+-- Pure-type system-like example+-- Includes Pi/Sigma, untyped equivalence+module PTS where++import Rebound++import qualified Rebound.Bind.Pat as Pat+import Rebound.Bind.PatN as PatN+import Rebound.Context+import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)+import Data.Fin(Fin(..), f0,f1,f2)+import Data.Fin qualified as Fin+import Data.Vec qualified as Vec+import GHC.Generics (Generic1)++-- In a pure type system, terms and types are combined+-- into the same syntactic class.++data Exp (n :: Nat) where+  -- | sort+  Star :: Exp n+  -- | dependent type `Pi x : A . B`+  Pi :: Exp n -> Bind1 Exp Exp n -> Exp n+  -- | variable+  Var :: Fin n -> Exp n+  -- | lambda expression, with type annotation  `lambda x:A.B`+  Lam :: Exp n -> Bind1 Exp Exp n -> Exp n+  -- | application+  App :: Exp n -> Exp n -> Exp n+  -- | dependent pair `Sigma x:A . B`+  Sigma :: Exp n -> Bind1 Exp Exp n -> Exp n+  -- | construct a pair, third argument is type annotation+  Pair :: Exp n -> Exp n -> Exp n -> Exp n+  -- | elimination form for pairs. `split e1 as (x,y) in e2`+  -- Binds two variables to+  -- the two components of the pair+  Split :: Exp n -> Bind2 Exp Exp n -> Exp n++deriving instance (Generic1 Exp)+----------------------------------------------++instance SubstVar Exp where+  var :: Fin n -> Exp n+  var = Var++instance Shiftable Exp where+  shift = shiftFromApplyE @Exp++instance Subst Exp Exp where+  isVar (Var x) = Just (Refl, x)+  isVar _ = Nothing+----------------------------------------------++t00 :: Exp N2+t00 = App (Var f0) (Var f0)++t01 :: Exp N2+t01 = App (Var f0) (Var f1)++-- Does a variable appear free in a term?++-- >>> appearsFree f0 t00+-- True++-- >>> appearsFree f1 t00+-- 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)++-- >>> strengthenRec s1 s1 snat t01+-- Nothing++instance Strengthen Exp where++----------------------------------------------+-- Examples++-- The identity function "λ x. x". With de Bruijn indices+-- we write it as "λ. 0"+t0 :: Exp Z+t0 = Lam Star (bind1 (Var f0))++-- A larger term "λ x. λy. x (λ z. z z)"+-- λ. λ. 1 (λ. 0 0)+t1 :: Exp Z+t1 =+  Lam+    Star+    ( bind1+        ( Lam+            Star+            ( bind1+                ( Var f1+                    `App` (Lam Star (bind1 (Var f0)) `App` Var f0)+                )+            )+        )+    )++-- To show lambda terms, we can write a simple recursive instance of+-- Haskell's `Show` type class. In the case of a binder, we use the `unbind1`+-- operation to access the body of the lambda expression.++-- >>> t0+-- λ *. 0++-- >>> t1+-- λ *. λ *. 1 ((λ *. 0) 0)++-- Polymorphic identity function and its type++tyid = Pi Star (bind1 (Pi (Var f0) (bind1 (Var f1))))++tmid = Lam Star (bind1 (Lam (Var f0) (bind1 (Var f0))))++-- >>> tyid+-- Pi *. 0 -> 1++-- >>> tmid+-- λ *. λ 0. 0++instance Show (Exp n) where+  showsPrec :: Int -> Exp n -> String -> String+  showsPrec _ Star = showString "*"+  showsPrec d (Pi a b)+    | appearsFree FZ (getBody1 b) =+        showParen (d > 9) $+          showString "Pi "+            . shows a+            . showString ". "+            . shows (getBody1 b)+    | otherwise =+        showParen (d > 9) $+          showsPrec 11 a+            . showString " -> "+            . showsPrec 9 (getBody1 b)+  showsPrec d (Sigma a b)+    | appearsFree FZ (getBody1 b) =+        showParen (d > 9) $+          showString "Sigma "+            . shows a+            . showString ". "+            . shows (getBody1 b)+    | otherwise =+        showParen (d > 9) $+          showsPrec 11 a+            . showString " * "+            . showsPrec 9 (getBody1 b)+  showsPrec _ (Var x) = shows x+  showsPrec d (App e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString " "+        . showsPrec 11 e2+  showsPrec d (Lam t b) =+    showParen (d > 9) $+      showString "λ "+        . shows t+        . showString ". "+        . shows (getBody1 b)+  showsPrec d (Pair e1 e2 t) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString ", "+        . showsPrec 11 e2+  showsPrec d (Split t b) =+    showParen (d > 10) $+      showString "split"+        . showsPrec 10 t+        . showString " in "+        . shows (getBody2 b)++-- With the instance above the derivable equality instance+-- is alpha-equivalence+deriving instance (Eq (Exp n))++--------------------------------------------------------++{- We can write the usual operations for evaluating+   lambda terms to values -}++-- big-step evaluation++-- >>> eval t1+-- λ *. λ *. 1 ((λ *. 0) 0)++-- >>> eval (t1 `App` t0)+-- λ *. (λ *. 0) ((λ *. 0) 0)++eval :: Exp n -> Exp n+eval (Var x) = Var x+eval (Lam a b) = Lam a b+eval (App e1 e2) =+  let v = eval e2+   in case eval e1 of+        Lam a b -> eval (instantiate1 b v)+        t -> App t v+eval Star = Star+eval (Pi a b) = Pi a b+eval (Sigma a b) = Sigma a b+eval (Pair a b t) = Pair a b t+eval (Split a b) =+  case eval a of+    Pair a1 a2 _ ->+      eval (instantiate2 b (eval a1) (eval a2))+    t -> Split t b++-- small-step evaluation++-- >>> step (t1 `App` t0)+-- Just (λ *. λ *. 0 (λ *. 0 0))++step :: Exp n -> Maybe (Exp n)+step (Var x) = Nothing+step (Lam a b) = Nothing+step (App (Lam a b) e2) = Just (instantiate1 b e2)+step (App e1 e2)+  | Just e1' <- step e1 = Just (App e1' e2)+  | Just e2' <- step e2 = Just (App e1 e2')+  | otherwise = Nothing+step Star = Nothing+step (Pi a b) = Nothing+step (Sigma a b) = Nothing+step (Pair a b _) = Nothing+step (Split (Pair a1 a2 _) b) = Just (PatN.instantiate2 b a1 a2)+step (Split a b)+  | Just a' <- step a = Just (Split a' b)+  | otherwise = Nothing++eval' :: Exp n -> Exp n+eval' e+  | Just e' <- step e = eval' e'+  | otherwise = e++-- normalization+-- to normalize under a lambda expression, we must first unbind+-- it and then rebind it when finished++-- >>> nf t1+-- λ. λ. 1 0++-- >>> nf (t1 `App` t0)+-- λ *. 0++-- reduce the term everywhere, as much as possible+nf :: Exp n -> Exp n+nf (Var x) = Var x+nf (Lam a b) = Lam a (bind1 (nf (getBody1 b)))+nf (App e1 e2) =+  case nf e1 of+    Lam a b -> nf (instantiate1 b e2)+    t -> App t (nf e2)+nf Star = Star+nf (Pi a b) = Pi (nf a) (bind1 (nf (getBody1 b)))+nf (Sigma a b) = Sigma (nf a) (bind1 (nf (getBody1 b)))+nf (Pair a b t) = Pair (nf a) (nf b) (nf t)+nf (Split a b) =+  case nf a of+    Pair a1 a2 _ -> nf (PatN.instantiate2 b a1 a2)+    t -> Split t (PatN.bind2 (nf (getBody2 b)))++-- first find the head form+whnf :: Exp n -> Exp n+whnf (App a1 a2) = case whnf a1 of+  Lam a b -> whnf (instantiate1 b a1)+  t -> App t a2+whnf (Split a b) = case whnf a of+  Pair a1 a2 _ -> whnf (PatN.instantiate2 b a1 a2)+  t -> Split t b+-- all other terms are already in head form+whnf a = a++norm :: Exp n -> Exp n+norm a = case whnf a of+  Lam a b -> Lam (norm a) (bind1 (norm (getBody1 b)))+  Pi a b -> Pi (norm a) (bind1 (norm (getBody1 b)))+  Sigma a b -> Sigma (norm a) (bind1 (norm (getBody1 b)))+  Pair a b t -> Pair (norm a) (norm b) (norm t)+  Star -> Star+  App a b -> App a (norm b)+  Split a b -> Split a (PatN.bind2 (norm (getBody2 b)))+  Var x -> Var x++--------------------------------------------------------+-- We can also write functions that manipulate the+-- environment explicitly++-- >>> evalEnv idE t1+-- λ *. λ *. 1 ((λ *. 0) 0)++-- Below, if n is 0, then this function acts like an+-- "environment-based" bigstep evaluator. The result of+-- evaluating a lambda expression is a closure --- the body+-- of the lambda paired with its environment. That is exactly+-- what the implementation of bind1 does.++-- In the case of beta-reduction, the `unBindWith` operation+-- applies its argument to the environment and subterm in the+-- closure. In other words, this function calls `evalEnv`+-- recursively with the saved environment and body of the lambda term.++evalEnv :: Env Exp m n -> Exp m -> Exp n+evalEnv r (Var x) = applyEnv r x+evalEnv r (Lam a b) = applyE r (Lam a b)+evalEnv r (App e1 e2) =+  let v = evalEnv r e2+   in case evalEnv r e1 of+        Lam a b ->+          unbindWith1 b (\r' e' -> evalEnv (v .: r') e')+        t -> App t v+evalEnv r Star = Star+evalEnv r (Pi a b) = applyE r (Pi a b)+evalEnv r (Sigma a b) = applyE r (Sigma a b)+evalEnv r (Pair a b t) = applyE r (Pair a b t)+evalEnv r (Split a b) =+  case evalEnv r a of+    Pair a1 a2 _ ->+      PatN.unbindWith2 b ( \r' e' -> evalEnv (a1 .: (a2 .: (r' .>> r))) e')+    t -> Split t (applyE r b)++----------------------------------------------------------------+data Err where+  Equate :: Exp n -> Exp n -> Err+  PiExpected :: Exp n -> Err+  SigmaExpected :: Exp n -> Err+  VarEscapes :: Exp n -> Err++deriving instance (Show Err)++equate :: (MonadError Err m) => Exp n -> Exp n -> m ()+equate t1 t2 = do+  let n1 = whnf t1+      n2 = whnf t2+  equateWHNF n1 n2++equateWHNF :: (MonadError Err m) => Exp n -> Exp n -> m ()+equateWHNF n1 n2 =+  case (n1, n2) of+    (Star, Star) -> pure ()+    (Var x, Var y) | x == y -> pure ()+    (Lam _ b1, Lam _ b2) -> equate (getBody1 b1) (getBody1 b2)+    (App a1 a2, App b1 b2) -> do+      equateWHNF a1 b1+      equate a2 b2+    (Pi tyA1 b1, Pi tyA2 b2) -> do+      equate tyA1 tyA2+      equate (getBody1 b1) (getBody1 b2)+    (Pair a1 a2 _, Pair b1 b2 _) -> do+      equate a1 b1+      equate a2 b2+    (Split a1 b1, Split a2 b2) -> do+      equateWHNF a1 a2+      equate (getBody2 b1) (getBody2 b2)+    (Sigma tyA1 b1, Sigma tyA2 b2) -> do+      equate tyA1 tyA2+      equate (getBody1 b1) (getBody1 b2)+    (_, _) -> throwError (Equate n1 n2)++----------------------------------------------------------------++checkType ::+  forall n m.+  (MonadError Err m, SNatI n) =>+  Ctx Exp n ->+  Exp n ->+  Exp n ->+  m ()+checkType g e t1 = do+  t2 <- inferType g e+  equate (whnf t2) t1++inferType ::+  forall n m.+  (MonadError Err m, SNatI n) =>+  Ctx Exp n ->+  Exp n ->+  m (Exp n)+inferType g (Var x) = pure (applyEnv g x)+inferType g Star = pure Star+inferType g (Pi a b) = do+  checkType g a Star+  checkType (g +++ a) (getBody1 b) Star+  pure Star+inferType g (Lam tyA b) = do+  checkType g tyA Star+  tyB <- inferType (g +++ tyA) (getBody1 b)+  return $ Pi tyA (bind1 tyB)+inferType g (App a b) = do+  tyA <- inferType g a+  case whnf tyA of+    Pi tyA1 tyB1 -> do+      checkType g b tyA1+      pure $ instantiate1 tyB1 b+    t -> throwError (PiExpected t)+inferType g (Sigma a b) = do+  checkType g a Star+  checkType (g +++ a) (getBody1 b) Star+  pure Star+inferType g (Pair a b ty) = do+  tyA <- inferType g a+  tyB <- inferType g b+  case ty of+    (Sigma tyA tyB) -> do+      checkType g a tyA+      checkType g b (instantiate1 tyB a)+      pure ty+    _ -> throwError (SigmaExpected ty)+inferType g (Split a b) = do+  tyA <- inferType g a+  case whnf tyA of+    Sigma tyA' tyB' -> do+      let g' :: Ctx Exp (S (S n))+          g' = g +++ tyA' +++ getBody1 tyB'+      ty <- inferType g' (getBody2 b)+      let ty' = whnf ty+      case strengthenN s2 ty' of+        Nothing -> throwError (VarEscapes ty)+        Just ty'' -> pure ty''+    _ -> throwError (SigmaExpected tyA)+++-- >>> inferType zeroE tmid :: Either Err (Exp N0)+-- Right (Pi *. 0 -> 1)+++-- >>> inferType zeroE (App tmid tyid) :: Either Err (Exp N0)+-- Right ((Pi *. 0 -> 1) -> Pi *. 0 -> 1)+
+ examples/Pat.hs view
@@ -0,0 +1,535 @@+-- \| The untyped lambda calculus with pattern matching+--++-- |+-- Module      : Pat+-- Description : Untyped lambda calculus, with pattern matching+-- Stability   : experimental+--+-- An implementation of the untyped lambda calculus with pattern matching.+--+-- This example extends the lambda calculus with constants (like 'nil and 'cons)+-- and arbitrary pattern matching. Case expressions include a list of branches,+-- where each branch is a pattern and a right-hand side. The pattern can bind+-- multiple variables and the index ensures that the rhs matches the number of+-- variables bound in the pattern.+-- +-- This example also includes pairs and "irrefutable patterns" i.e. let binding+-- that can deeply deconstruct cons pairs (only).+module Pat where++import Rebound++import Rebound.Bind.PatN as PatN+import qualified Rebound.Bind.Pat as Pat+import Rebound.Bind.Scoped qualified as Scoped+import Data.Maybe qualified as Maybe+import Data.Type.Equality+import Data.Fin ( Fin, f0, f1 )+import Data.Fin qualified as Fin+import Data.Vec qualified as Vec++----------------------------------------------++-- * Syntax++----------------------------------------------++-- The untyped lambda calculus extended with+-- symbols ("con"stants) and pattern matching+-- expression (case)+-- A constant applied to any number of arguments+-- is a value+data Exp (n :: Nat) where+  Var :: Fin n -> Exp n+  Lam :: Bind1 Exp Exp n -> Exp n+  App :: Exp n -> Exp n -> Exp n+  LetPair  :: Exp n -> Branch PairPat n -> Exp n+  -- ^ deep pattern matching against pairs (only)+  Con :: String -> Exp n+  -- ^ constant (or symbol) like 'cons or 'nil'+  Case :: Exp n -> [Branch Pat n] -> Exp n+  -- ^ deep pattern matching against any pattern+   ++-- Each branch in a case expression is a pattern binding,+-- i.e. a data structure that binds m variables in some+-- expression body with scope n+-- Here, the variable m does not appear+-- in the result type `Branch pat n`, so is an existential.+data Branch pat (n :: Nat) where+  Branch :: SNatI m => Pat.Bind Exp Exp (pat m) n -> Branch pat n++-- Patterns for case expressions.+-- The index `m` in the pattern is the number of occurrences of+-- PVar, i.e. the number variables bound by the pattern.+-- These variables are ordered left to right.+-- For example (PCon "cons" `PApp` PVar `PApp` PVar) is the+-- representation of the pattern "cons x y", which binds two+-- variables.+-- To prevent patterns of the form "x y z", this type is split+-- into top level patterns (Pat) and applications of constants (ConApp)+data Pat (m :: Nat) where+  PVar :: Pat N1 -- binds exactly one variable+  PHead :: ConApp m -> Pat m++data ConApp (m :: Nat) where+  PCon :: String -> ConApp N0 -- binds zero variables+  PApp :: ConApp m1 -> Pat m2 -> ConApp (m2 + m1)++-- Patterns for pairs only, a special case of the above+data PairPat (m :: Nat) where+  PPVar :: PairPat N1+  PPair :: PairPat m1 -> PairPat m2 -> PairPat (m2 + m1)++----------------------------------------------++-- * Sized instance++----------------------------------------------++-- Any type that is used as a pattern must be an+-- instance of the `Sized` type class, so that the library+-- can determine the number of binding variables both+-- statically and dynamically.++-- The `Pat` type tells us how many variables are bound+-- the pattern with the index `n`. We can also recover+-- that number from the pattern itself by counting the number+-- of occurrences of `PVar`.++instance Sized (Pat m) where+  type Size (Pat m) = m++  size :: Pat m -> SNat (Size (Pat m))+  size PVar = s1+  size (PHead p) = size p+++instance Sized (ConApp m) where+  type Size (ConApp m) = m++  size :: ConApp m -> SNat (Size (ConApp m))+  size (PApp p1 p2) = sPlus (size p2) (size p1)+  size (PCon s) = s0+++instance Sized (PairPat m) where+  type Size (PairPat m) = m++  size :: PairPat m -> SNat (Size (PairPat m))+  size PPVar = s1+  size (PPair p1 p2) = sPlus (size p2) (size p1)+++----------------------------------------------++-- * Substitution++----------------------------------------------++instance SubstVar Exp where+  var :: Fin n -> Exp n+  var = Var++instance Shiftable Exp where+  shift = shiftFromApplyE @Exp++instance Subst Exp Exp where+  applyE :: Env Exp n m -> Exp n -> Exp m+  applyE r (Var x) = applyEnv r x+  applyE r (Lam b) = Lam (applyE r b)+  applyE r (App e1 e2) = App (applyE r e1) (applyE r e2)+  applyE r (Con s) = Con s+  applyE r (Case e brs) = Case (applyE r e) (map (applyE r) brs)+  applyE r (LetPair e1 b) = LetPair (applyE r e1) (applyE r b)+++instance Shiftable (Branch pat) where+  shift = shiftFromApplyE @Exp++instance Subst Exp (Branch pat) where+  applyE :: Env Exp n m -> Branch pat n -> Branch pat m+  applyE r (Branch bnd) = Branch (applyE r bnd)+++----------------------------------------------+-- Example terms+----------------------------------------------++-- The identity function "λ x. x". With de Bruijn indices+-- we write it as "λ. 0"+t0 :: Exp Z+t0 = Lam (bind1 (Var f0))++-- A larger term "λ x. λy. x (λ z. z z)"+-- λ. λ. 1 (λ. 0 0)+t1 :: Exp Z+t1 =+  Lam+    ( bind1+        ( Lam+            ( bind1+                ( Var f1+                    `App` (Lam (bind1 (Var f0)) `App` Var f0)+                )+            )+        )+    )++-- "head function"+-- \x -> case x of [nil -> x ; cons y z -> y]+t2 :: Exp Z+t2 =+  Lam+    ( bind1+        ( Case+            (Var f0)+            [ Branch+                ( Pat.bind @(Pat N0)+                    (PHead (PCon "Nil"))+                    (Var f0)+                ),+              Branch+                ( Pat.bind @(Pat N2)+                    (PHead (PCon "Cons" `PApp` PVar `PApp` PVar))+                    (Var f0)+                )+            ]+        )+    )++-- a "list"  ['a','b']+t3 :: Exp Z+t3 = Con "cons" `App` Con "a" `App` (Con "cons" `App` Con "b" `App` Con "nil")++--------------------------------------------------------------++-- * Show implementation++--------------------------------------------------------------++-- >>> t0+-- λ. 0++-- >>> t1+-- λ. λ. 1 (λ. 0 0)++-- >>> t2+-- λ. case 0 of [Nil => 0,(Cons V) V => 0]++-- >>> t3+-- (cons a) ((cons b) nil)+++instance Show (Exp n) where+  showsPrec :: Int -> Exp n -> String -> String+  showsPrec _ (Var x) = shows x+  showsPrec d (App e1 e2) =+    showParen (d > 0) $+      showsPrec 10 e1+        . showString " "+        . showsPrec 11 e2+  showsPrec d (Lam b) =+    showParen (d > 10) $+      showString "λ. "+        . shows (getBody1 b)+  showsPrec d (Con s) = showString s+  showsPrec d (Case e brs) =+    showParen (d > 10) $+      showString "case "+        . shows e+        . showString " of "+        . shows brs+  showsPrec d (LetPair e (Branch b)) = +    showString "let "+    . shows (Pat.getPat b)+    . showString " = "+    . shows e+    . showString " in "+    . showsPrec d (Pat.getBody b)++instance Show (PairPat m) where+  showsPrec :: Int -> PairPat m -> String -> String+  showsPrec d PPVar = showString "V"+  showsPrec d (PPair p1 p2) =+    showParen True $+      shows p1+        . showString ","+        . shows p2++instance Show (Pat m) where+  showsPrec :: Int -> Pat m -> String -> String+  showsPrec d PVar = showString "V"+  showsPrec d (PHead p) = showsPrec d p++instance Show (ConApp m) where+  showsPrec d (PApp p1 p2) =+    showParen (d > 0) $+      showsPrec 10 p1+        . showString " "+        . showsPrec 11 p2+  showsPrec d (PCon s) = showString s+++-- In a `PatBind` term, we can access the pattern with `getPat`+-- and the RHS with `getBody`+instance Show (Branch Pat n) where+  showsPrec :: Int -> Branch Pat n -> String -> String+  showsPrec d (Branch bnd) =+    shows (Pat.getPat bnd)+      . showString " => "+      . showsPrec d (Pat.getBody bnd)++--------------------------------------------------------------++-- * Eq implementation++--------------------------------------------------------------++-- We would like to derive equality for patterns, i.e. +-- +--     deriving instance (Eq (Pat m))+-- +-- but because of the application case, this process fails.+-- We don't know that each subpattern binds the same+-- number of variables!+++-- Therefore to compare Pats for equality, we generalize the+-- `testEquality` function from Data.Type.Equality. (This+-- class is often used for comparisons between indexed types.+-- but only works if the index is the last type parameter.+-- In our case, we need to produce an equality for the+-- first type parameter.)+-- This function can be applied, even if the number of+-- pattern-bound variables are not known to be equal.+-- (cf. m1 and m2 below). If the patterns are indeed equal,+-- then `patEq` *also* returns a proof that the indices+-- are equal. (The type `a :~: b` is a GADT with a single+-- constructor `Refl` that can only be used when a and be are+-- equal. Pattern matching on this GADT brings an equality+-- between a and b into the context of the term.)++instance PatEq (Pat m1) (Pat m2) where+  patEq PVar PVar = Just Refl+  patEq (PHead p1) (PHead p2) = do+    Refl <- patEq p1 p2+    return Refl+  patEq _ _ = Nothing++instance PatEq (ConApp m1) (ConApp m2) where+  patEq (PApp p1 p2) (PApp p1' p2') = do+    Refl <- patEq p1 p1'+    Refl <- patEq p2 p2'+    return Refl+  patEq (PCon s1) (PCon s2) | s1 == s2 = Just Refl+  patEq _ _ = Nothing++instance PatEq (PairPat m1) (PairPat m2) where+  patEq (PPair p1 p2) (PPair p1' p2') = do+    Refl <- patEq p1 p1'+    Refl <- patEq p2 p2'+    return Refl+  patEq PPVar PPVar = Just Refl+  patEq _ _ = Nothing+++-- the generalized equality can be used for the usual equality+instance Eq (Pat m) where+  p1 == p2 = Maybe.isJust (patEq p1 p2)++instance Eq (PairPat m) where+  p1 == p2 = Maybe.isJust (patEq p1 p2)++instance SizeIndex PairPat p+instance SizeIndex Pat p+++-- Because the Branch type is parameterized by a pattern type, `pat` of kind +-- `Nat -> Type` we need to make some assumptions about that type to construct+-- the `Eq` instance. (1) we need to be able to test patterns for equality+-- no matter what their size is. (2) we need to know that the index *is* the +-- size of the pattern, i.e. Size (pat m) ~ m. The `SizeIndex` class captures+-- this relationship in a way that can be quantifed over all m.+-- If we did not parameterize the `Branch` type by the pattern type, we would not+-- need this complexity.++instance (forall m. Eq (pat m),                    -- 1+          forall m. SizeIndex pat m)               -- 2+          => Eq (Branch pat n) where+  (==) :: Branch pat n -> Branch pat n -> Bool+  (Branch (p1 :: Pat.Bind Exp Exp (pat m1) n))+    == (Branch (p2 :: Pat.Bind Exp Exp (pat m2) n)) =+      case testEquality+        (size (Pat.getPat p1) :: SNat m1)+        (size (Pat.getPat p2) :: SNat m2) of+        Just Refl -> p1 == p2+        Nothing -> False+++-- With the instance above the derivable equality instance+-- is alpha-equivalence+deriving instance (Eq (Exp n))+++--------------------------------------------------------+-- Pattern matching code+--------------------------------------------------------++p1 :: Pat N2+p1 = PHead $ PApp (PApp (PCon "C") PVar) PVar++p2 :: Pat N2+p2 = PHead $ PApp (PApp (PCon "D") PVar) PVar++e1 :: Exp N0+e1 = App (App (Con "C") (Con "A")) (Con "B")++e2 :: Exp N0+e2 = App (App (Con "D") (Con "A")) (Con "C")++-- >>> patternMatch p1 e1+-- Just [(0,B),(1,A)]++-- >>> patternMatch p2 e1+-- Nothing++-- >>> patternMatch p1 e2+-- Nothing++-- >>> patternMatch p2 e2+-- Just [(0,C),(1,A)]+++-- | Compare a "pair" pattern with a pair pattern, potentially+-- producing a substitution for all of the variables bound in the pattern.+ppatternMatch :: PairPat p -> Exp m -> Maybe (Env Exp p m)+ppatternMatch PPVar e = Just $ oneE e+ppatternMatch (PPair p1 p2) (App (App (Con "cons") e1) e2) = do+  env1 <- ppatternMatch p1 e1+  env2 <- ppatternMatch p2 e2+  withSNat (size p2) $ return (env2 .++ env1)+ppatternMatch _ _ = Nothing++-- | Compare a pattern with an expression, potentially+-- producing a substitution for all of the variables bound in the pattern.+patternMatch :: Pat p -> Exp m -> Maybe (Env Exp p m)+patternMatch PVar e = Just $ oneE e+patternMatch (PHead p) e = patternMatchApp p e++patternMatchApp :: ConApp p -> Exp m -> Maybe (Env Exp p m)+patternMatchApp (PApp p1 p2) (App e1 e2) = do+  env1 <- patternMatchApp p1 e1+  env2 <- patternMatch p2 e2+  withSNat (size p2) $ return (env2 .++ env1)+patternMatchApp (PCon s1) (Con s2) =+  if s1 == s2 then Just zeroE else Nothing+patternMatchApp _ _ = Nothing++-- Compare the scrutinee against multiple patterns and return +-- the matching branch+findBranch :: Exp n -> [Branch Pat n] -> Maybe (Exp n)+findBranch e [] = Nothing+findBranch e (Branch bind : brs) =+  case patternMatch (Pat.getPat bind) e of+    Just r -> Just $ Pat.instantiate bind r+    Nothing -> findBranch e brs+++++--------------------------------------------------------+-- Eval and step+--------------------------------------------------------++{- We can write the usual operations for evaluating+   lambda terms to values -}+-- big-step evaluation+-- >>> eval t1+-- λ. λ. 1 (λ. 0 0)+-- >>> eval (t1 `App` t0)+-- λ. λ. 0 (λ. 0 0)+t4 = t2 `App` t3++-- >>> t4+-- λ. case 0 of [Nil => 0,(Cons V) V => 0] ((cons a) ((cons b) nil))+-- >>> eval t4+-- case (cons a) ((cons b) nil) of [Nil => (cons a) ((cons b) nil),(Cons V) V => 0]+eval :: Exp n -> Exp n+eval (Var x) = Var x+eval (Lam b) = Lam b+eval (App e1 e2) =+  let v = eval e2+   in case eval e1 of+        Lam b -> eval (instantiate1 b v)+        t -> App t v -- if cannot reduce, return neutral term+eval (Con s) = Con s+eval (Case e brs) =+  let v = eval e+   in case findBranch v brs of+        Just br -> eval br+        Nothing -> Case v brs -- if cannot reduce, return neutral term+eval (LetPair e (Branch b)) = +  case ppatternMatch (Pat.getPat b) (eval e) of+    Just r -> eval (Pat.instantiate b r)+    Nothing -> error "No match!"++-- | small-step evaluation+-- >>> step (t1 `App` t0)+-- Just (λ. λ. 0 (λ. 0 0))+step :: Exp n -> Maybe (Exp n)+step (Var x) = Nothing+step (Lam b) = Nothing+step (App (Lam b) e2) = Just (instantiate1 b e2)+step (App e1 e2)+  | Just e1' <- step e1 = Just (App e1' e2)+  | Just e2' <- step e2 = Just (App e1 e2')+  | otherwise = Nothing+step (LetPair a (Branch b)) +  | Just r <- ppatternMatch (Pat.getPat b) a+  = Just (Pat.instantiate b r)+step (LetPair e b) +  | Just e' <- step e = Just (LetPair e' b)+  | otherwise = Nothing+step (Con s) = Nothing+step (Case e brs)+  | Just br <- findBranch e brs = Just br+  | Just e' <- step e = Just (Case e' brs)+  | otherwise = Nothing++eval' :: Exp n -> Exp n+eval' e+  | Just e' <- step e = eval' e'+  | otherwise = e++-- full normalization+-- to normalize under a lambda expression, we must first unbind+-- it and then rebind it when finished++-- >>> nf t1+-- λ. λ. 1 0+-- >>> nf (t1 `App` t0)+-- λ. λ. 0 0+nf :: Exp n -> Exp n+nf (Var x) = Var x+nf (Lam b) = Lam (bind1 (nf (getBody1 b)))+nf (App e1 e2) =+  case nf e1 of+    Lam b -> instantiate1 b (nf e2)+    t -> App t (nf e2)+nf (Con s) = Con s+nf (Case e brs) =+  let v = nf e+   in case findBranch v brs of+        Just b -> nf b+        Nothing -> Case e (map nfBr brs)+nf (LetPair e br@(Branch b)) = +  let v = nf e in+  case ppatternMatch (Pat.getPat b) v of +    Just r -> nf (Pat.instantiate b r)+    Nothing -> LetPair (nf e) (nfBr br)++nfBr :: (forall n. Sized (pat n)) => Branch pat n -> Branch pat n+nfBr (Branch bnd) =+  Branch (Pat.bind (Pat.getPat bnd) (nf (Pat.getBody bnd)))
+ examples/PureSystemF.hs view
@@ -0,0 +1,277 @@+-- | An implementation of System F as a (quasi) Pure Type System.+module PureSystemF where++import Control.Monad (unless)+import Control.Monad.Except (Except (..), MonadError (..), runExcept)+import Data.Fin (f0, f1, f2)+import Data.Vec ((!))+import Data.Vec qualified as Vec+import Rebound+import Rebound.Bind.Local+import Rebound.MonadNamed qualified as Scoped+import Rebound.MonadScoped (MonadScopedReader (..), ScopedReader, ScopedReaderT (..), asksS, runScopedReader)+import Rebound.MonadScoped qualified as Scoped+import Text.Read (Lexeme (String))++-- | We represent both terms and types using one single+-- syntactic class. We use one single constructor for variables,+-- regardless of whether they stand for a term or a+-- variable. We also use an additional constructor, 'Kind',+-- which is used to represent the type of types.+data Exp (n :: Nat) where+  Var :: Fin n -> Exp n+  Kind :: Exp n+  -- Types+  TAll :: Bind Ty Ty n -> Ty n+  TArr :: Ty n -> Ty n -> Ty n+  -- Terms+  Abs :: Ty n -> Bind Exp Exp n -> Exp n+  App :: Exp n -> Exp n -> Exp n+  TAbs :: Bind Ty Exp n -> Exp n+  TApp :: Exp n -> Ty n -> Exp n+  deriving (Eq)++-- | An alias used for readability.+type Ty = Exp++--------------------------------------------------------------------------------+--- Instances required by Rebound+--------------------------------------------------------------------------------++instance SubstVar Exp where+  var = Var++instance Subst Exp Exp where+  applyE :: forall n m. Env Exp n m -> Exp n -> Exp m+  applyE env t = case t of+    Var x -> applyEnv env x+    Kind -> Kind+    TAll bnd -> TAll (r bnd)+    TArr t1 t2 -> TArr (r t1) (r t2)+    Abs ty bnd -> Abs (r ty) (r bnd)+    App t1 t2 -> App (r t1) (r t2)+    TAbs bnd -> TAbs (r bnd)+    TApp t1 t2 -> TApp (r t1) (r t2)+    where+      r :: forall t. (Subst Exp t) => t n -> t m+      r = applyE env++-- We will be needing strengthening in the type-checker;+-- more on that later.+instance Strengthen Exp where+  strengthenRec ::+    forall k m n.+    SNat k ->+    SNat m ->+    SNat n ->+    Exp (k + (m + n)) ->+    Maybe (Exp (k + n))+  strengthenRec k m n t = case t of+    Var x -> Var <$> strengthenRec k m n x+    Kind -> return Kind+    TAll bnd -> TAll <$> r bnd+    TArr t1 t2 -> TArr <$> r t1 <*> r t2+    Abs ty bnd -> Abs <$> r ty <*> r bnd+    App t1 t2 -> App <$> r t1 <*> r t2+    TAbs bnd -> TAbs <$> r bnd+    TApp t1 t2 -> TApp <$> r t1 <*> r t2+    where+      r :: (Strengthen t) => t (k + (m + n)) -> Maybe (t (k + n))+      r = strengthenRec k m n++--------------------------------------------------------------------------------+--- Typechecking+--------------------------------------------------------------------------------++-- | An environment mapping (de Bruijn) variables to+-- a user-defined name and its type.+data TcEnv n = TcEnv+  { names :: Vec n LocalName,+    types :: Ctx Exp n+  }++emptyEnv :: TcEnv Z+emptyEnv = TcEnv {names = Vec.empty, types = zeroE}++-- | Add a new binding to the environment+extendE :: (LocalName, Exp n) -> TcEnv n -> TcEnv (S n)+extendE (n, t) (TcEnv ns ts) =+  TcEnv (n ::: ns) (ts +++ t)++-- | Search for a binding. Lookup cannot fail+-- thanks to extrinsic scoping.+lookupE :: TcEnv n -> Fin n -> (LocalName, Exp n)+lookupE (TcEnv ns ts) i = (ns ! i, applyEnv ts i)++type Error = String++-- | Typechecking monad.+newtype TC n a = TC (ScopedReaderT TcEnv (Except Error) n a)+  deriving (Functor, Applicative, Monad, MonadError Error)++-- Trivial lifting through a newtype.+instance MonadScopedReader TcEnv TC where+  askS = TC askS+  localS f (TC m) = TC (localS f m)++-- | Run the type-checking monad. Returns+-- either the result, or an error.+runTC :: TcEnv n -> TC n a -> Either Error a+runTC env (TC m) = runExcept $ runScopedReaderT m env++-- | Extend the current (latent) scope with a new binding.+push :: LocalName -> Exp n -> TC (S n) a -> TC n a+push n t = Scoped.localS $ extendE (n, t)++-- | Lookup a binding in the (latent) scope.+get :: Fin n -> TC n (LocalName, Exp n)+get i = readerS (`lookupE` i)++-- | Checks that a given type is indeed a (valid) type,+-- by ensuring that its own type is 'Kind'.+ensureType :: (SNatI n) => Ty n -> TC n ()+ensureType Kind = return ()+ensureType ty = do+  k <- inferType ty+  unless (k == Kind) $ throwError "Not a type"++-- | Infer the type of an expression.+inferType :: (SNatI n) => Exp n -> TC n (Ty n)+inferType (Var x) = do+  (_, ty) <- get x+  ensureType ty+  return ty+inferType Kind =+  -- Kind is used internally to represent a well-formed+  -- type, but should not be used otherwise.+  throwError "Cannot type 'Kind'"+-- Types+inferType (TAll bnd) = do+  let (x, t) = unbindl bnd+  push x Kind $ ensureType t+  return Kind+inferType (TArr l r) =+  ensureType l >> ensureType r >> return Kind+-- Terms+inferType (Abs xTy bnd) = do+  let (x, t) = unbindl bnd+  ensureType xTy+  tTy <- push x xTy $ inferType t+  -- Because the type system is not dependent, we cannot+  -- allow 'x' to occur in 'tTy'. Ensuring this and bringing+  -- 'tTy' into the outer scope is done using 'strengthenN'.+  case strengthenN s1 tTy of+    Just tTy' -> return $ TArr xTy tTy'+    Nothing -> throwError "Term variable occurs in type"+inferType (App l r) = do+  lTy <- inferType l+  rTy <- inferType r+  case lTy of+    TArr rTy' retTy -> do+      unless (rTy == rTy') $ throwError "Argument mismatch"+      return retTy+    _ -> throwError "Left hand-side of application is not an arrow"+inferType (TAbs bnd) = do+  let (x, t) = unbindl bnd+  tTy <- push x Kind $ inferType t+  return $ TAll $ bind x tTy+inferType (TApp l r) = do+  lTy <- inferType l+  ensureType r+  case lTy of+    TAll bnd -> return $ instantiate bnd r+    _ -> throwError "Left hand-side is not a forall"++--------------------------------------------------------------------------------+--- (Pretty) Printing+--------------------------------------------------------------------------------++-- | An environment mapping variables to their (user-defined) name.+data PpEnv n = PpEnv+  { ppnames :: Vec n String,+    pplevel :: Int+  }++-- | Pretty-print a term.+pp :: Vec n LocalName -> Exp n -> String+pp s e = runScopedReader (pp' e) (PpEnv {ppnames = fmap name s, pplevel = 0})+  where+    setLevel :: Int -> ScopedReader PpEnv n String -> ScopedReader PpEnv n String+    setLevel newLevel = localS (\e -> e {pplevel = newLevel})++    atLevel :: Int -> ScopedReader PpEnv n String -> ScopedReader PpEnv n String+    atLevel newLevel m = do+      level <- asksS pplevel+      let m' = if level <= newLevel then m else (\s -> "(" ++ s ++ ")") <$> m+      setLevel newLevel m'++    push n = localS (\e -> e {ppnames = n ::: ppnames e})++    pp' :: Exp n -> ScopedReader PpEnv n String+    pp' (Var f) = asksS (\e -> ppnames e ! f)+    pp' Kind = return "Kind"+    pp' (TAll bnd) = atLevel 0 $ do+      let (LocalName x, b) = unbindl bnd+      b' <- push x $ pp' b+      return $ "∀" ++ x ++ ". " ++ b'+    pp' (TArr l r) = atLevel 1 $ do+      l' <- atLevel 2 $ pp' l+      r' <- pp' r+      return $ l' ++ " -> " ++ r'+    pp' (Abs ty bnd) = atLevel 0 $ do+      let (LocalName x, b) = unbindl bnd+      b' <- push x $ pp' b+      return $ "λ" ++ x ++ ". " ++ b'+    pp' (App l r) = atLevel 2 $ do+      l' <- pp' l+      r' <- atLevel 3 $ pp' r+      return $ l' ++ " " ++ r'+    pp' (TAbs bnd) = atLevel 0 $ do+      let (LocalName x, b) = unbindl bnd+      b' <- push x $ pp' b+      return $ "Λ" ++ x ++ ". " ++ b'+    pp' (TApp l r) = atLevel 2 $ do+      l' <- pp' l+      r' <- setLevel 0 $ pp' r+      return $ l' ++ " [" ++ r' ++ "]"++instance Show (Exp Z) where+  show = pp Vec.empty++t0, t1, t2 :: Exp Z+t0 = TAbs (bind (LocalName "X") $ Abs (var f0) (bind (LocalName "x") $ var f0))+-- >>> t0+-- >>> runTC emptyEnv $ inferType t0+-- ΛX. λx. x+-- Right ∀X. X -> X++t1 = TAbs (bind (LocalName "X") $ Abs (TAll (bind (LocalName "Y") $ TArr (var f0) (var f0))) (bind (LocalName "f") $ Abs (var f1) (bind (LocalName "x") $ App (TApp (var f1) (var f2)) (var f0))))+-- >>> t1+-- >>> runTC emptyEnv $ inferType t1+-- ΛX. λf. λx. f [X] x+-- Right ∀X. (∀Y. Y -> Y) -> X -> X++t2 = Abs Kind (bind (LocalName "X") $ Abs (var f0) (bind (LocalName "x") (var f0)))+-- >>> t2+-- >>> runTC emptyEnv $ inferType t2+-- λX. λx. x+-- Left "Term variable occurs in type"++bbn0, bbn1, bbn2 :: Exp Z+bbn0 = TAbs (bind (LocalName "X") $ Abs (TArr (var f0) (var f0)) (bind (LocalName "f") $ Abs (var f1) (bind (LocalName "z") $ (var f0))))+bbn1 = TAbs (bind (LocalName "X") $ Abs (TArr (var f0) (var f0)) (bind (LocalName "f") $ Abs (var f1) (bind (LocalName "z") $ App (var f1) (var f0))))+bbn2 = TAbs (bind (LocalName "X") $ Abs (TArr (var f0) (var f0)) (bind (LocalName "f") $ Abs (var f1) (bind (LocalName "z") $ App (var f1) (App (var f1) (var f0)))))+-- >>> bbn0+-- >>> runTC emptyEnv $ inferType bbn0+-- ΛX. λf. λz. z+-- Right ∀X. (X -> X) -> X -> X++-- >>> bbn1+-- >>> runTC emptyEnv $ inferType bbn1+-- ΛX. λf. λz. f z+-- Right ∀X. (X -> X) -> X -> X++-- >>> bbn2+-- >>> runTC emptyEnv $ inferType bbn2+-- ΛX. λf. λz. f (f z)+-- Right ∀X. (X -> X) -> X -> X
+ examples/ScopeCheck.hs view
@@ -0,0 +1,64 @@+-- |+-- Module      : ScopeCheck+-- Description : Scope checking the Untyped lambda calculus+-- Stability   : experimental+--+-- This module demonstrates a translation from unscoped to well-scoped terms++module ScopeCheck where++import Rebound+import Rebound.Bind.Single+import Data.Maybe (fromJust)+import LC qualified+import Rebound.Lib++-- | Named representation for the untyped lambda calculus+-- The type parameter 'a' is the variable type+data Exp (a :: Type) where+  Var :: a -> Exp a+  Lam :: a -> Exp a -> Exp a+  App :: Exp a -> Exp a -> Exp a++-- | Convert a named expression to deBruijn indices, checking to make+-- sure that the expression is well scoped+scopeCheck :: (Eq a) => Exp a -> Maybe (LC.Exp Z)+scopeCheck = to []+  where+    to :: (Eq a) => [(a, Fin n)] -> Exp a -> Maybe (LC.Exp n)+    to vs (Var v) = do+      x <- lookup v vs+      return $ LC.Var x+    to vs (Lam v b) = do+      b' <- to ((v, FZ) : map (fmap FS) vs) b+      return $ LC.Lam (bind b')+    to vs (App f a) = do+      f' <- to vs f+      a' <- to vs a+      return $ LC.App f' a'+++----------------------------------------------+-- Examples+----------------------------------------------++-- | Identity function+idExp :: Exp String+idExp = Lam "x" (Var "x")++-- | "True"+trueExp :: Exp String+trueExp = Lam "x" (Lam "y" (Var "x"))++-- | An ill-scoped term (`y` is never bound)+illScoped :: Exp String+illScoped = Lam "x" (Var "y")++-- >>> scopeCheck idExp+-- Just (λ. 0)++-- >>> scopeCheck trueExp+-- Just (λ. (λ. 1))++-- >>> scopeCheck illScoped+-- Nothing
+ examples/SystemF.hs view
@@ -0,0 +1,103 @@+-- | This is an example of the use of the library with two separate variable types+module SystemF where++{- One issue with this example is that we only store one sort of environment at each binder. +   However, terms are subject to two different forms of substitution --- either for terms or types.+   So, applying the "wrong" sort through a binder means that we don't gain any advantage from +   the caching --- we need to bind and unbind the to propagate.++-}++import Prelude hiding (lookup)+import Rebound+import Rebound.Bind.Single+++data Ty (n :: Nat) where+    TVar :: Fin n -> Ty n+    TAll :: Bind Ty Ty n -> Ty n+    TArr :: Ty n -> Ty n -> Ty n+      deriving (Eq)++-- swap the order of the scopes so that we can talk about +-- substituting a type inside of an expression+newtype TyExp n m = TyExp { unTyExp :: Exp m n }++data Exp (m :: Nat) (n :: Nat) where+    EVar  :: Fin n -> Exp m n+    ELam  :: Ty m -> Bind (Exp m) (Exp m) n -> Exp m n +    EApp  :: Exp m n -> Exp m n -> Exp m n+    ETLam :: Bind Ty (TyExp n) m -> Exp m n+    ETApp :: Exp m n -> Ty m -> Exp m n++instance SubstVar Ty where+    var = TVar +instance Subst Ty Ty where+    applyE r (TVar x) = applyEnv r x+    applyE r (TAll b) = TAll (applyE r b)+    applyE r (TArr t1 t2) = TArr (applyE r t1) (applyE r t2)++instance SubstVar (Exp m) where+    var = EVar++-- apply type substitution to an expression, using the newtype+substTy :: Env Ty m1 m2 -> Exp m1 n -> Exp m2 n+substTy r e = unTyExp (applyE r (TyExp e))++instance Subst Ty (TyExp n) where+    applyE :: forall m1 m2 n. Env Ty m1 m2 -> TyExp n m1 -> TyExp n m2+    applyE r (TyExp (EVar x)) = TyExp (EVar x)+    applyE r (TyExp (ELam ty b)) = +        let q = substTy r (getBody b)+        in TyExp (ELam (applyE r ty) (bind q))+    applyE r (TyExp (EApp e1 e2)) = TyExp (EApp (substTy r e1) (substTy r e2))+    applyE r (TyExp (ETLam b)) = +        let q = applyE (up r) (getBody b)+        in TyExp (ETLam (bind q))+    applyE r (TyExp (ETApp e1 t2)) = +        TyExp (ETApp (substTy r e1) (applyE r t2))++-- | shift the type scope in the range of a term substiution+upTyScope :: Env (Exp m) n1 n2 -> Env (Exp (S m)) n1 n2+upTyScope = transform (substTy shift1E)+    +instance Subst (Exp m) (Exp m) where+    applyE :: forall m n1 n2. Env (Exp m) n1 n2 -> Exp m n1 -> Exp m n2+    applyE r (EVar x) = applyEnv r x+    applyE r (ELam ty b) = ELam ty (applyE r b)+    applyE r (EApp t1 t2) = EApp (applyE r t1) (applyE r t2)+    applyE r (ETLam b) =+        let (TyExp te) = getBody b +        in ETLam (bind (TyExp (applyE (upTyScope r) te)))+    applyE r (ETApp e t) = ETApp (applyE r e) t    ++-- System F context+data FCtx m n where+    Empty     :: FCtx Z Z+    ConsTmVar :: Ty m -> FCtx m n -> FCtx m (S n)+    ConsTyVar :: FCtx m n -> FCtx (S m) n++lookup :: Fin n -> FCtx m n -> Ty m+lookup FZ (ConsTmVar ty _) = ty+lookup FZ (ConsTyVar g) = applyE @Ty shift1E $ lookup FZ g+lookup (FS x) (ConsTmVar _ g) = lookup x g+lookup (FS x) (ConsTyVar g) = applyE @Ty shift1E $ lookup (FS x) g++tc :: FCtx m n -> Exp m n -> Maybe (Ty m)+tc g (EVar x) = return $ lookup x g+tc g (ELam ty b) = tc (ConsTmVar ty g) (getBody b)+tc g (EApp a b) = do +    t1 <- tc g a+    t2 <- tc g b+    case t1 of +        TArr t11 t12 -> if t1 == t2 then return t12 else Nothing+        _ -> Nothing+tc g (ETLam b) = do+    t1 <- tc (ConsTyVar g) (unTyExp (getBody b))+    return (TAll (bind t1))+tc g (ETApp a ty) = do +    t1 <- tc g a +    case t1 of +        TAll tb -> return $ instantiate tb ty+        _ -> Nothing+
+ rebound.cabal view
@@ -0,0 +1,122 @@+cabal-version:  3.0+name:           rebound+version:        0.1.0.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+license:        MIT+license-file:   LICENSE+build-type:     Simple+extra-doc-files:+    README.md+    ChangeLog.md+category:       Language+synopsis:       A variable binding library based on well-scoped de Bruijn indices.++common common-stanza+  ghc-options:+     -Wno-type-defaults+     -Wincomplete-patterns+  default-language:+    GHC2021+  default-extensions:+    KindSignatures+    , DataKinds+    , GADTs+    , StandaloneDeriving+    , LambdaCase+    , QuantifiedConstraints+    , TypeFamilies+    , AllowAmbiguousTypes+    , UndecidableInstances+    , FunctionalDependencies+    , ViewPatterns+    , PatternSynonyms+    , PackageImports+    , DerivingStrategies++library+  import:+      common-stanza+  build-depends:+      base >= 4.15 && < 5.0+    , containers >= 0.6.7 && < 0.7+    , deepseq >= 1.4.8 && < 1.5+    , fin >= 0.3 && < 0.4+    , mtl >= 2.3.1 && < 2.4+    , QuickCheck >= 2.14.3 && < 2.15+    , vec >= 0.5 && < 0.6+  exposed-modules:+      Rebound+    , Rebound.Classes+    , Rebound.Context+    , Rebound.Env+    , Rebound.Env.Strict+    , Rebound.Env.Lazy+    , Rebound.Env.LazyA+    , Rebound.Env.LazyB+    , Rebound.Env.StrictA+    , Rebound.Env.StrictB+    , Rebound.Env.Functional+    , Rebound.Generics+    , Rebound.Lib+    , Rebound.MonadNamed+    , Rebound.MonadScoped+    , Rebound.Bind.Single+    , Rebound.Bind.Local+    , Rebound.Bind.PatN+    , Rebound.Bind.Pat+    , Rebound.Bind.Scoped+    , Rebound.Refinement+    , Data.SNat+    , Data.Fin+    , Data.Vec+    , Data.LocalName+    , Data.Scoped.Telescope+    , Data.Scoped.List+    , Data.Scoped.Classes+    , Data.Scoped.Maybe+  hs-source-dirs: src++test-suite rebound-tests+  import:+    common-stanza+  build-depends:+      base+    , rebound+    , containers+    , mtl+    , QuickCheck+    , tasty+    , tasty-hunit+    , tasty-quickcheck+  type:+    exitcode-stdio-1.0+  hs-source-dirs:+    examples+    test+  main-is:+    All.hs+  other-modules:+    LC+    LCQC+    LCLet+    PTS+    Pat+    DepMatch+    ScopeCheck+    HOAS+    SystemF+    PureSystemF+    LinLC+    Utils+    Examples.LC+    Examples.LCLet+    Examples.Pat+    Examples.PureSystemF+    Examples.PTS+    Examples.DepMatch+    Examples.LinLC
+ src/Data/Fin.hs view
@@ -0,0 +1,238 @@+-- |+-- Module      : Data.Fin+-- Description : Bounded natural numbers+--+-- This file re-exports definitions from [fin](https://hackage.haskell.org/package/fin)'s+-- [Data.Fin](https://hackage.haskell.org/package/fin-0.3.2/docs/Data-Fin.html), while adding a few more+-- that are relevant to this context. Like [Data.Fin](https://hackage.haskell.org/package/fin-0.3.2/docs/Data-Fin.html),+-- it is meant to be used qualified.+--+-- @+-- import 'Fin' ('Fin' (..))+-- import qualified 'Fin' as 'Fin'+-- @+{-# LANGUAGE PackageImports #-}+module Data.Fin(+  Nat(..), SNat(..),+  Fin(..),+  toNat, fromNat, toInteger,+  mirror,+  absurd,+  universe,+  f0,f1,f2,f3,+  invert,+  shiftN,+  shift1,+  weakenFin,+  weakenFinRight,+  weaken1Fin,+  weaken1FinRight,+  strengthen1Fin,+  strengthenRecFin+ ) where++import Data.Nat+import Data.SNat+import "fin" Data.Fin hiding (cata)+import Data.Proxy (Proxy (..))+-- for efficient rescoping+import Unsafe.Coerce (unsafeCoerce)++-------------------------------------------------------------------------------+-- toInt+-------------------------------------------------------------------------------++-- | The `toInteger` instance for Fin has an unnecessary+-- type class constraint (NatI n) for Fin. So we+-- also include this class for simple conversion.+instance ToInt (Fin n) where+  toInt :: Fin n -> Int+  toInt FZ = 0+  toInt (FS x) = 1 + toInt x++-- >>> [minBound .. maxBound] :: [Fin N3]+-- [0,1,2]++-- | List all numbers up to some size+-- >>> universe :: [Fin N3]+-- [0,1,2]++-- | Convert an "index" Fin to a "level" Fin and vice versa.+invert :: forall n. (SNatI n) => Fin n -> Fin n+invert f = case snat @n of+  SZ -> case f of {}+  SS -> maxBound - f++-------------------------------------------------------------------------------+-- * Shifting+-------------------------------------------------------------------------------++-- We use the term "Weakening" to mean: Adding a new binding to the front of+-- the typing context without changing existing indices.+-- In contrast, "Shifting" means: Adjusting the indices of free variables+-- within a term to reflect a new binding added to the end of the context.+--+-- Shifting functions add some specified amount to the given+-- `Fin` value, also incrementing its type.+--+-- Shifting is implemented in the Data.Fin libary using the `weakenRight`+-- function, which changes the value of a Fin and its type.+-- >>> :t weakenRight+-- weakenRight :: SNatI n => Proxy n -> Fin m -> Fin (Plus n m)+--+-- >>> weakenRight (Proxy :: Proxy N1) (f1 :: Fin N2) :: Fin N3+-- 2+--+-- In this module, we call the same operation `shiftN` and give+-- it a slightly more convenient interface.+-- >>> shiftN s1 (f1 :: Fin N2)+-- 2+--+-- | Increment by a fixed amount (on the left).+shiftN :: forall n m. SNat n -> Fin m -> Fin (n + m)+shiftN p f = withSNat p $ weakenRight (Proxy :: Proxy n) f++-- | Increment by one.+shift1 :: Fin m -> Fin (S m)+shift1 = shiftN s1++-- We could also include a dual function, which increments on the right+-- but we haven't needed that operation anywhere.++-------------------------------------------------------------------------------+-- * Weakening+-------------------------------------------------------------------------------++-- | Weaken the bound of a 'Fin' by an arbitrary amount, without+-- changing its index.++-- | Weakenening changes the bound of a nat-indexed type without changing+-- its value.+-- These operations can either be defined for the n-ary case (as in Fin below)+-- or be defined in terms of a single-step operation.+-- However, as both of these operations are identity functions,+-- it is justified to use unsafeCoerce.+--+-- The corresponding function in the Data.Fin library is `weakenLeft`.+--+-- @+-- -- >>> :t weakenLeft+-- weakenLeft :: SNatI n => Proxy m -> Fin n -> Fin (Plus n m)+-- @+--+-- This function does not change the value, it only changes its type.+--+-- @+-- -- >>> weakenLeft (Proxy :: Proxy N1) (f1 :: Fin N2) :: Fin N3+-- 1+-- @+--+-- We could use the following definition:+--+-- @+-- weakenFin m f = withSNat m $ weakenLeft (Proxy :: Proxy m) f+-- @+--+-- But, by using an 'unsafeCoerce' implementation, we can avoid the+-- @'SNatI' n@ constraint in the type of this operation.+--+-- @+-- -- >>> weakenFin (Proxy :: Proxy N1) (f1 :: Fin N2) :: Fin N3+-- 1+-- @+weakenFin :: proxy m -> Fin n -> Fin (m + n)+weakenFin _ f = unsafeCoerce f++-- | Weaken the bound of a 'Fin' by 1.+weaken1Fin :: Fin n -> Fin (S n)+weaken1Fin = weakenFin s1++-- | Weaken the bound of of a 'Fin' by an arbitrary amount on the right.+-- This is also an identity function+-- >>> weakenFinRight (s1 :: SNat N1) (f1 :: Fin N2) :: Fin N3+-- 1+weakenFinRight :: proxy m -> Fin n -> Fin (n + m)+weakenFinRight m f = unsafeCoerce f++-- | Weaken the bound of a 'Fin' by 1.+weaken1FinRight :: Fin n -> Fin (n + N1)+weaken1FinRight = weakenFinRight s1++-------------------------------------------------------------------------------+-- * Aliases+-------------------------------------------------------------------------------++-- Convenient names for fin values. These have polymorphic types so they+-- will work in any scope. (These are also called fin0, fin1, fin2, etc+-- in Data.Fin)++-- | 0.+f0 :: Fin (S n)+f0 = FZ++-- | 1.+f1 :: Fin (S (S n))+f1 = FS f0++-- | 2.+f2 :: Fin (S (S (S n)))+f2 = FS f1++-- | 3.+f3 :: Fin (S (S (S (S n))))+f3 = FS f2++-- >>> f2+-- 2++-------------------------------------------------------------------------------+-- * Strengthening+-------------------------------------------------------------------------------++-- | With strengthening, we make sure that variable f0 is not used,+-- and we decrement all other indices by 1. This allows us to+-- also decrement the scope by one.+--- >>> strengthen1Fin (f0 :: Fin (S N3)) :: Maybe (Fin N3)+-- Nothing+-- >>> strengthen1Fin (f1 :: Fin (S N3)) :: Maybe (Fin N3)+-- Just 0+-- >>> strengthen1Fin (f2 :: Fin (S N3)) :: Maybe (Fin N3)+-- Just 1+strengthen1Fin :: forall n. SNatI n => Fin (S n) -> Maybe (Fin n)+strengthen1Fin = strengthenRecFin s0 s1 undefined++-- | We implement strengthening with the following operation that+-- generalizes the induction hypothesis, so that we can strengthen+-- in the middle of the scope. The scope of the Fin should have the form+-- @k + (m + n)@+--+-- Indices in the middle part of the scope @m@ are "strengthened" away.+--+--- >>> strengthenRecFin s1 s1 s2 (f1 :: Fin (N1 + N1 + N2)) :: Maybe (Fin (N1 + N2))+-- Nothing+--+-- Variables that are in the first part of the scope @k@ (the ones that have+-- most recently entered the context) do not change when strengthening.+--+--- >>> strengthenRecFin s1 s1 s2 (f0 :: Fin (N1 + N1 + N2))+-- Just 0+--+-- Variables in the last part of the scope @n@ are decremented by strengthening+--+-- >>> strengthenRecFin s1 s1 s2 (f2 :: Fin (N1 + N1 + N2)) :: Maybe (Fin N3)+-- Just 1+--+-- >>> strengthenRecFin s1 s1 s2 (f3 :: Fin (N1 + N1 + N2)) :: Maybe (Fin N3)+-- Just 2+--+strengthenRecFin ::+   SNat k -> SNat m -> proxy n -> Fin (k + (m + n)) -> Maybe (Fin (k + n))+strengthenRecFin SZ SZ n x = Just x  -- Base case: k = 0, m = 0+strengthenRecFin SZ (snat_ -> SS_ m) n FZ = Nothing+  -- Case: k = 0, m > 0, and x is in the `m` range+strengthenRecFin SZ (snat_ -> SS_ m) n (FS x) =+    strengthenRecFin SZ m n x+strengthenRecFin (snat_ -> SS_ k) m n FZ = Just FZ+  -- Case: x < k, leave it alone+strengthenRecFin (snat_ -> SS_ k) m n (FS x) =+    FS <$> strengthenRecFin k m n x
+ src/Data/LocalName.hs view
@@ -0,0 +1,19 @@+-- |+-- Module      : Data.LocalName+-- Description : Strings with an "identity" equality+module Data.LocalName where++-- | A simple wrapper for strings+-- 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++instance Show LocalName where+  show (LocalName x) = x++-- | A default name.+internalName :: LocalName+internalName = LocalName "_internal"
+ src/Data/SNat.hs view
@@ -0,0 +1,133 @@+-- |+-- Module      : Data.SNat+-- Description : Singleton naturals+--+-- Runtime data that connects to type-level nats.+module Data.SNat(+  Nat(..), toNatural, fromNatural,+  SNat(..),  snatToNat,+  SNatI(..), snat, withSNat, reify, reflect,+  type (+),+  N0, N1, N2, N3,+  s0, s1, s2, s3,+  sPlus,+  axiomPlusZ,+  axiomAssoc,+  SNat_(..), snat_,+  prev,+  next,+  ToInt(..),+ ) where++-- Singleton nats are purely runtime++import Data.Type.Equality+import Data.Type.Nat+import Test.QuickCheck+import Unsafe.Coerce (unsafeCoerce)+import Prelude hiding (pred, succ)++-----------------------------------------------------+-- axioms (use unsafeCoerce)+-----------------------------------------------------++-- | '0' is identity element for @+@+axiomPlusZ :: forall m. m + Z :~: m+axiomPlusZ = unsafeCoerce Refl++-- | @+@ is associative.+axiomAssoc :: forall p m n. p + (m + n) :~: (p + m) + n+axiomAssoc = unsafeCoerce Refl++-----------------------------------------------------+-- Nats (singleton nats and implicit singletons)+-----------------------------------------------------++-- | 0.+type N0 = Z++-- | 1.+type N1 = S N0++-- | 2.+type N2 = S N1++-- | 3.+type N3 = S N2++---------------------------------------------------------+-- Singletons and instances+---------------------------------------------------------++-- | 0.+s0 :: SNat N0+s0 = snat++-- | 1.+s1 :: SNat N1+s1 = snat++-- | 2.+s2 :: SNat N2+s2 = snat++-- | 3.+s3 :: SNat N3+s3 = snat++instance (SNatI n) => Arbitrary (SNat n) where+  arbitrary :: (SNatI n) => Gen (SNat n)+  arbitrary = pure snat++-- | Conversion to 'Int'.+class ToInt a where+  toInt :: a -> Int++instance ToInt (SNat n) where+  toInt :: SNat n -> Int+  toInt = fromInteger . toInteger . snatToNat++---------------------------------------------------------+-- Addition+---------------------------------------------------------++-- | Notation for the addition of naturals.+type family (n :: Nat) + (m :: Nat) :: Nat where+  m + n = Plus m n++-- | Addition of singleton naturals.+sPlus :: forall n1 n2. SNat n1 -> SNat n2 -> SNat (n1 + n2)+sPlus SZ n = n+sPlus x@SS y = withSNat (sPlus (prev x) y) SS++-- >>> reflect $ sPlus s3 s1+-- 4++---------------------------------------------------------+-- View pattern access to the predecessor+---------------------------------------------------------++-- | View pattern allowing pattern matching on naturals.+-- See 'snat_'.+data SNat_ n where+  SZ_ :: SNat_ Z+  SS_ :: SNat n -> SNat_ (S n)++-- | View pattern allowing pattern matching on naturals.+--+-- @+-- f :: forall p. SNat p -> ...+-- f SZ = ...+-- f (snat_ -> SS_ m) = ...+-- @+snat_ :: SNat n -> SNat_ n+snat_ SZ = SZ_+snat_ SS = SS_ snat++-- | Predecessor of a natural.+prev :: SNat (S n) -> SNat n+prev SS = snat++-- | Successor of a natural.+next :: SNat n -> SNat (S n)+next x = withSNat x SS
+ src/Data/Scoped/Classes.hs view
@@ -0,0 +1,131 @@+-- |+-- Module      : Data.Scoped.Classes+-- Description : Structures for scoped types+-- +-- These classes provide access to scoped versions of higher-kinded classes+-- such as 'Functor'/'Foldable' etc.+-- All instances of this class should be coercible to existing instances of +-- these classes. (Which are used in the default definitions.)++module Data.Scoped.Classes(+    type (~>)(..),+    ScopedFunctor(..),+    ScopedFoldable(..),+    ScopedTraversable(..),+    ScopedApplicative(..),+    ScopedMonad(..)+) where++import Data.Coerce+import Control.Monad as M+import Data.Kind (Type)+import GHC.Generics+import Test.QuickCheck+import Control.DeepSeq++import Data.Foldable qualified as F+import Data.Traversable qualified as T++-- | A scoped function (i.e., a function whose input & output are scoped).+newtype (~>) a b n = MkArr (a n -> b n) +    deriving newtype (Semigroup, Monoid, Arbitrary, CoArbitrary, Testable, NFData)+    deriving stock (Generic)++-- | Scoped 'Functor'.+class (forall a n. Coercible (f a n) (k (a n)), Functor k) => ScopedFunctor k f | f -> k where+    fmap :: Functor k => (a n -> b n) -> f a n -> f b n+    fmap f = coerce (M.fmap @k f)++-- | Scoped 'Foldable'.+class (forall a n. Coercible (f a n) (k (a n)), Foldable k) => ScopedFoldable k f | f -> k where+    fold :: (Monoid (a n)) => f a n -> a n+    fold x = F.fold @k (coerce x)++    foldMap :: (Monoid m) => (a n -> m) -> f a n -> m+    foldMap f x = F.foldMap @k f (coerce x)++    foldMap' :: (Monoid m) => (a n -> m) -> f a n -> m+    foldMap' f x = F.foldMap' @k f (coerce x)++    foldr :: (a n -> b -> b) -> b -> f a n -> b+    foldr f b x = F.foldr @k f b (coerce x)++    foldr' :: (a n -> b -> b) -> b -> f a n -> b+    foldr' f b x = F.foldr' @k f b (coerce x)++    foldl ::  (b -> a n -> b) -> b -> f a n -> b+    foldl f b x = F.foldl @k f b (coerce x)++    foldl' ::  (b -> a n -> b) -> b -> f a n -> b+    foldl' f b x = F.foldl @k f b (coerce x)++    foldr1 ::  (a n -> a n -> a n) -> f a n -> a n+    foldr1 f x = F.foldr1 @k f (coerce x)++    foldl1 :: (a n -> a n -> a n) -> f a n -> a n+    foldl1 f x = F.foldl1 @k f (coerce x)++    null :: forall a n. f a n -> Bool+    null x = F.null (coerce x :: k (a n))++    length :: forall a n. f a n -> Int+    length x = F.length @k (coerce x :: k (a n))++    elem :: (Eq (a n)) => a n -> f a n -> Bool +    elem a x = F.elem @k a (coerce x)++    maximum :: (Ord (a n)) => f a n -> a n+    maximum x = F.maximum @k (coerce x)++    minimum :: (Ord (a n)) => f a n -> a n+    minimum x = F.maximum @k (coerce x)++    sum :: (Num (a n)) => f a n -> a n+    sum x = F.sum @k (coerce x)++    product :: (Num (a n)) => f a n -> a n+    product x = F.product @k (coerce x)++    any :: (a n -> Bool) -> f a n -> Bool+    any f x = F.any @k f (coerce x)++    all :: (a n -> Bool) -> f a n -> Bool+    all f x = F.all @k f (coerce x)++    mapM_ :: (Monad m) => (a n -> m b) -> f a n -> m ()+    mapM_ f x = M.mapM_ @k f (coerce x)++-- | Scoped 'Applicative'.+class (forall a n. Coercible (t a n) (k (a n)), Applicative k) => ScopedApplicative k t | t -> k where+    pure  :: a n -> t a n+    pure x = coerce (Prelude.pure @k x) ++    (<*>) :: forall a b n. t (a ~> b) n -> t a n -> t b n  +    f <*> x = coerce (fk Prelude.<*> coerce x) where+        fk :: k (a n -> b n)+        fk = coerce <$> (coerce f :: k ((a ~> b) n))++-- | Scoped 'Monad'.+class (forall a n. Coercible (t a n) (k (a n)), Monad k, ScopedApplicative k t) => +       ScopedMonad k t | t -> k where+    return :: a n -> t a n+    return = Data.Scoped.Classes.pure++    (>>=) :: forall a n b m. t a n -> (a n -> t b m) -> t b m+    ma >>= kb = coerce r where+        r :: k (b m)+        r = (M.>>=) (coerce ma :: k (a n)) (coerce kb)++-- The default definitions do not have 0-cost coercions due to role limitations+-- | Scoped 'Traversable'.+class (forall a n. Coercible (t a n) (k (a n)), Traversable k) => ScopedTraversable k t | t -> k where+   traverse :: forall a b n f. Applicative f => (a n -> f (b n)) -> t a n -> f (t b n)+   traverse f x = coerce <$> T.traverse @k f (coerce x)+   +   mapM :: Monad m => (a n -> m (b n)) -> t a n -> m (t b n)+   mapM f x = coerce <$> T.mapM @k f (coerce x)+   +   -- TODO ???+   -- sequenceA :: Applicative f => t (f n) -> f (t a)+   -- sequence :: Monad m => t (m a) -> m (t a)+
+ src/Data/Scoped/List.hs view
@@ -0,0 +1,108 @@+-- |+-- Module: Data.Scoped.List+-- Description : Scoped lists+--+-- This module defines a type of lists indexed by a scope+-- The lists are homogenous, and every type in the list must be indexed+-- by the same scope.+-- This module is intended to be imported qualified and used with the+-- OverloadedLists Haskell language extension. Many of the operations+-- in this module have the same name as prelude functions.+{-# LANGUAGE DerivingStrategies, DeriveAnyClass #-}+module Data.Scoped.List (List,+      pattern Nil, pattern (:<),+      Data.Scoped.List.uncons,+      (Data.Scoped.List.++),+      Data.Scoped.List.concat,+      Data.Scoped.List.filter,+      Data.Scoped.List.zipWith,+      Data.Scoped.List.zipWithM_,+      IsList(..),+      module Data.Scoped.Classes) where++import Data.Nat ( Nat )+import Data.Kind ( Type )+import GHC.IsList ( IsList(..) )+import GHC.Generics+import Test.QuickCheck ( Arbitrary )+import Control.DeepSeq ( NFData )+import Data.Coerce ( coerce )+import Control.Monad qualified as M+import Data.Scoped.Classes++-- | Lists where every element has type (a n)+-- Note: the @n@ is *not* the length of the list, it is a common scope+-- for all elements in the list.+newtype List a n = MkList [a n]+    deriving newtype (Eq, Ord, Read, Show, Semigroup, Monoid, Generic, Arbitrary, NFData)+    deriving anyclass (ScopedFoldable [], ScopedTraversable [],+                        ScopedFunctor [], ScopedApplicative [], ScopedMonad [])++-- | Separate the head of the list from its tail, if applicable.+uncons :: List a n -> Maybe (a n, List a n)+uncons x = case coerce x of+      [] -> Nothing+      x:xs -> Just (x,coerce xs)++{-# COMPLETE (:<), Nil #-}+-- | Pattern for the empty list.+pattern Nil :: forall a n. List a n+pattern Nil <- (uncons -> Nothing)+ where+   Nil = coerce ([] :: [a n])++-- | Pattern for a cons-ed list.+pattern (:<) :: a n -> List a n -> List a n+pattern x :< xs <- (uncons -> Just (x,xs))+  where+    x :< xs = coerce (x : coerce xs)++-- * Prelude / Control.Monad list operations++-- | See 'Prelude.++'.+(++) :: forall t n. List t n -> List t n -> List t n+(++) = coerce ((Prelude.++):: [t n] -> [t n] -> [t n])++-- | Lists flattening / Monadic join.+concat :: List (List t) n -> List t n+concat = Data.Scoped.Classes.foldr (Data.Scoped.List.++) Nil++-- | See 'Prelude.filter'.+filter :: (a n -> Bool) -> List a n -> List a n+filter f = coerce (Prelude.filter f)++-- | See 'Prelude.zipWith'.+zipWith :: (a n -> b n -> c n) -> List a n -> List b n -> List c n+zipWith f = coerce (Prelude.zipWith f)++-- | See 'Prelude.zipWithM_'.+zipWithM_ :: forall m k f1 f2 a b c n. (Applicative m)+    => (a n -> b n -> m c) -> List a n -> List b n -> m ()+zipWithM_ f = coerce (M.zipWithM_ f)++-- | A general conversion to the standard list type.+instance IsList (List v n) where+   type Item (List v n) = v n++   fromList :: [Item (List v n)] -> List v n+   fromList = coerce++   toList :: List v n -> [Item (List v n)]+   toList = coerce++-- | Enable generic programming for the `List` type+-- We can't derive the `Data.Generic1` instance for `List`+-- using newtype deriving because the kinds differ.+-- Therefore we need to write it by hand.+instance Generic1 (List a :: Nat -> Type) where+   type Rep1 (List a) =+      U1 :+: (Rec1 a :*: Rec1 (List a))++   from1 :: List a n -> Rep1 (List a) n+   from1 (MkList []) = L1 U1+   from1 (MkList (x:xs)) = R1 (Rec1 x :*: Rec1 (MkList xs))++   to1 :: Rep1 (List a) n -> List a n+   to1 (L1 U1) = MkList []+   to1 (R1 (Rec1 x :*: Rec1 (MkList xs))) = MkList (x : xs)+
+ src/Data/Scoped/Maybe.hs view
@@ -0,0 +1,76 @@+-- |+-- Module: Data.Scoped.Maybe+-- Description : Scoped maybe+--+-- 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 #-}+module Data.Scoped.Maybe where++import Data.Nat ( Nat )+import Data.Kind ( Type )+import GHC.Generics+import GHC.Stack.Types (HasCallStack)+import Data.Maybe qualified as M+import Prelude hiding (Maybe(..), maybe)++import Data.Coerce ( coerce )+import Test.QuickCheck (Arbitrary)+import Control.DeepSeq (NFData)+import Data.Scoped.Classes++-- | 'M.Maybe' whose (hypothetical) content is scoped.+newtype Maybe a n = MkMaybe (M.Maybe (a n))+    deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Generic, Arbitrary, NFData)+    deriving anyclass (ScopedFoldable M.Maybe, ScopedTraversable M.Maybe,+        ScopedFunctor M.Maybe, ScopedApplicative M.Maybe, ScopedMonad M.Maybe)++{-# COMPLETE Nothing, Just #-}+-- | Pattern for 'M.Nothing'.+pattern Nothing :: Maybe a n+pattern Nothing = MkMaybe M.Nothing++-- | Pattern for 'M.Just'.+pattern Just :: a n -> Maybe a n+pattern Just a = MkMaybe (M.Just a)++-- | See 'M.maybe'.+maybe :: b -> (a n -> b) -> Maybe a n -> b+maybe b f = coerce (M.maybe b f)++-- | See 'M.isJust'.+isJust :: forall a n. Maybe a n -> Bool+isJust = coerce (M.isJust :: M.Maybe (a n) -> Bool)++-- | See 'M.isNothing'.+isNothing :: forall a n. Maybe a n -> Bool+isNothing = coerce (M.isNothing :: M.Maybe (a n) -> Bool)++-- | See 'M.fromJust'.+fromJust :: forall a n. HasCallStack => Maybe a n -> a n+fromJust = coerce (M.fromJust :: M.Maybe (a n) -> a n)++-- | See 'M.fromMaybe'.+fromMaybe :: forall a n. a n -> Maybe a n -> a n+fromMaybe = coerce (M.fromMaybe :: a n -> M.Maybe (a n) -> a n)++-- | See 'M.maybeToList'.+maybeToList  :: forall a n. Maybe a n -> [a n]+maybeToList = coerce (M.maybeToList :: M.Maybe (a n) -> [a n])++-- | See 'M.listToMaybe'.+listToMaybe :: forall a n. [a n] -> Maybe a n+listToMaybe = coerce (M.listToMaybe :: [a n] -> M.Maybe (a n))++instance Generic1 (Maybe a :: Nat -> Type) where+   type Rep1 (Maybe a) =+      U1 :+: Rec1 a++   from1 :: Maybe a n -> Rep1 (Maybe a) n+   from1 Nothing = L1 U1+   from1 (Just x) = R1 (Rec1 x)++   to1 :: Rep1 (Maybe a) n -> Maybe a n+   to1 (L1 U1) = Nothing+   to1 (R1 (Rec1 x)) = Just x
+ src/Data/Scoped/Telescope.hs view
@@ -0,0 +1,72 @@+-- |+-- Stability: experimental+{-# OPTIONS_HADDOCK hide #-}+module Data.Scoped.Telescope {-# WARNING "This module is experimental" #-} where++import Rebound.Classes+import Rebound.Env (Shiftable (..))+import Data.Fin (Fin)+import Data.Nat+import Data.Type.Equality ((:~:) (..))+import Data.Type.Nat+import Data.Vec.Lazy qualified as Vec+import Rebound.Lib (axiomAssoc, axiomPlusZ)+import Data.SNat++-- | Unlike 'Scoped.TeleList', this datatype does not nest: it is effectively a+-- 'List.List'/'Data.Vec.Vec' but with extra scoping inside.+data Telescope u s n m where+  TNil :: Telescope u s Z m+  TCons :: (u, s (n + m)) -> !(Telescope u s n m) -> Telescope u s (S n) m++tmap :: (forall k. u -> s k -> (u', s' k)) -> Telescope u s n m -> Telescope u' s' n m+tmap f TNil = TNil+tmap f (TCons (u, s) xs) = TCons (f u s) (tmap f xs)++empty :: Telescope u s Z m+empty = TNil++singleton :: (u, s n) -> Telescope u s (S Z) n+singleton h = TCons h TNil++append :: forall u s nl nr m. Telescope u s nl (nr + m) -> Telescope u s nr m -> (SNat nl, Telescope u s (nl + nr) m)+append TNil r = (SZ, r)+append (TCons l ls) r =+  case axiomAssoc @nl @nr @m of+    Refl -> let (k, ls') = append ls r in withSNat k (SS, TCons l ls')++toTelescope :: forall p n u s. (Shiftable s) => Vec.Vec p (u, s n) -> Telescope u s p n+toTelescope = snd . iter+  where+    iter :: forall p. Vec.Vec p (u, s n) -> (SNat p, Telescope u s p n)+    iter Vec.VNil = (SZ, TNil)+    iter ((Vec.:::) @_ @p' (u, s) xs) =+      let (sp', sc') :: (SNat p', Telescope u s p' n) = iter xs+          s' :: s (p' + n) = shift sp' s+       in (withSNat sp' SS, TCons (u, s') sc')++-- fromTelescope :: forall s u p n. (Shiftable s) => Telescope u s p n -> (SNat p, Vec.Vec p (u, s (p + n)))+-- fromTelescope = iter SZ+--   where+--     iter :: forall u s k n m. (Shiftable s) => SNat k -> Telescope u s n m -> (SNat (k + n), Vec.Vec n (u, s (k + n + m)))+--     iter sk TNil = case axiomPlusZ @k of Refl -> (sk, Vec.empty)+--     iter sk (TCons @_ @_ @n' (u, s) sc) =+--       case axiomSus @k @n' of+--         Refl ->+--           let x' :: (u, s (k + n + m)) = case axiomAssoc @k @n' @m of Refl -> (u, shift (addOne sk) s)+--               (sn', sc') :: (SNat (k + n), Vec.Vec n' (u, s (k + n + m))) = iter (addOne sk) sc+--            in (sn', x' Vec.::: sc')++--     addOne :: SNat k -> SNat (S k)+--     addOne k = withSNat k SS++emptyTelescope = TNil++-- nth :: forall s n m u. (Shiftable s) => Fin n -> Telescope u s n m -> (u, s (n + m))+-- nth i s = snd (fromTelescope s) Vec.! i++instance Sized (Telescope u s n m) where+  type Size (Telescope u s n m) = n+  size :: Telescope u s n m -> SNat n+  size TNil = s0+  size (TCons _ t) = withSNat (size t) SS
+ src/Data/Vec.hs view
@@ -0,0 +1,63 @@+-- |+-- Module      : Data.Vec+-- Description : Vectors, or length-indexed lists+--+-- This file re-exports definitions from [vec](https://hackage.haskell.org/package/vec)'s+-- [Data.Vec.Lazy](https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html).+--+-- @+-- import 'Vec' ('Vec' (..))+-- import qualified 'Vec' as 'Vec'+-- @+module Data.Vec+  ( module Data.Vec.Lazy,+    vlength,+    append,+    setAt,+    all2+ ) where++-- based on+-- https://hackage.haskell.org/package/fin+++import Data.Fin (Fin (..))+import Data.Fin qualified+import Data.Nat+import Data.SNat+import Data.Type.Equality+import Data.Vec.Lazy+import Test.QuickCheck+import Prelude hiding (lookup, repeat, zipWith)++-----------------------------------------------------+-- Vectors (additional definitions)+-----------------------------------------------------++-- | Update a vector value at a given index+setAt :: Fin n -> Vec n a -> a -> Vec n a+setAt FZ (_ ::: vs) w = w ::: vs+setAt (FS x) (w1 ::: env) w2 = w1 ::: setAt x env w2++-- | Concatenate two vectors+append :: forall n m a. Vec n a -> Vec m a -> Vec (n + m) a+append = (Data.Vec.Lazy.++)++-- | Access elements by position+lookup :: Fin n -> Vec n a -> a+lookup = flip (!)++-- | Calculate length as a singleton value+vlength :: Vec n a -> SNat n+vlength VNil = SZ+vlength (_ ::: v) = withSNat (vlength v) SS+++-- >>> all (\x -> x > 3) (4 ::: 5 ::: VNil)+-- True++-- | Ensure that a binary predicate holds for+-- corresponding elements in two vectors+all2 :: (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool+all2 f (x ::: xs) (y ::: ys) = f x y && all2 f xs ys+all2 f VNil VNil = True
+ src/Rebound.hs view
@@ -0,0 +1,29 @@+-- |+-- Module      : Rebound+-- Description : Efficient, Expressive, and Well-Scoped Binding+--+-- This top level module re-exports the core of the library.+-- It should be used in conjunction with one (or more) module+-- in "Rebound.Bind".+module Rebound+  (module Rebound.Classes,+   module Rebound.Env,+   module Rebound.Refinement,+   module Rebound.Generics,+   module Rebound.Lib,+   module Rebound.Context,+   module Data.LocalName,+   Generic(..),+   Generic1(..))+where++import Rebound.Classes+import Rebound.Context+import Rebound.Env+import Rebound.Refinement+import Rebound.Generics+import Rebound.Lib+import Data.LocalName+import GHC.Generics(Generic(..),Generic1(..))++
+ src/Rebound/Bind/Local.hs view
@@ -0,0 +1,100 @@+-- |+-- Module       : Rebound.Bind.Single+-- Description  : Bind a single variable, with a name+--+-- Single variable binder, but includes a name (represented by a 'LocalName') for pretty printing.+-- This is a specialization of "Rebound.Bind.Pat".+module Rebound.Bind.Local+  ( module Rebound,+    type Bind,+    bind,+    getLocalName,+    internalBind,+    getBody,+    unbind,+    unbindl,+    instantiate,+    applyUnder,+    bindWith,+    unbindWith,+    instantiateWith+  )+where++import Rebound+import Rebound.Bind.Pat qualified as Pat+import Data.Fin qualified as Fin++-- | 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 = Pat.Bind v c LocalName n++-- | Bind a variable, using the identity substitution.+bind :: (Subst v c) => LocalName -> c (S n) -> Bind v c n+bind = Pat.bind++-- | Bind a variable, while suspending the provided substitution.+bindWith :: forall v c m n. LocalName -> Env v m n -> c (S m) -> Bind v c n+bindWith = Pat.bindWith++-- | Bind the default \"internal\" variable, while suspending the provided substitution.+internalBind :: (Subst v c) => c (S n) -> Bind v c n+internalBind = Pat.bind internalName++-- | Retrieve the name of the bound variable.+getLocalName :: Bind v c n -> LocalName+getLocalName = Pat.getPat++-- | Retrieve the body of the binding.+getBody :: (Subst v c) => Bind v c n -> c (S n)+getBody = Pat.getBody++-- | Run a function on the body (and bound name), after applying the delayed substitution.+unbind :: (Subst v c) => Bind v c n -> ((LocalName, c (S n)) -> d) -> d+unbind b f = f (getLocalName b, getBody b)++-- | Retrieve the body, as well as the bound name.+unbindl :: (Subst v c) => Bind v c n -> (LocalName, c (S n))+unbindl b = (getLocalName b, getBody b)++-- | 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 b e = Pat.instantiate b (oneE e)++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder ::+  (Subst v c) =>+  (forall m. Env v m (S n2) -> c m -> c (S n2)) ->+  Env v n1 n2 ->+  Bind v c n1 ->+  Bind v c n2+applyUnder = Pat.applyUnder++-- | 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. LocalName -> Env v m n -> c (S m) -> d) -> d+unbindWith = Pat.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.+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)+++-- Example++data Exp n = Var (Fin n) | App (Exp n) (Exp n) | Lam (Bind Exp Exp n)+  deriving (Eq,Generic1)+instance SubstVar Exp where var = Var+instance Subst Exp Exp where+  isVar (Var x) = Just (Refl,x)+  isVar _ = Nothing+t1 :: Exp Z+t1 = Lam (bind (LocalName "x") (Var Fin.f0))+t2 :: Exp Z+t2 = Lam (bind (LocalName "y") (Var Fin.f0))++-- >>> t1 == t2+-- True
+ src/Rebound/Bind/Pat.hs view
@@ -0,0 +1,246 @@+-- |+-- Module       : Rebound.Bind.Pat+-- Description  : Bind variables according to a pattern+--+-- Bind variables according to a user-defined pattern.+module Rebound.Bind.Pat+  ( module Rebound,+    type Bind,+    bind,+    unbind,+    unbindl,+    getPat,+    getBody,+    instantiate,+    bindWith,+    unbindWith,+    instantiateWith,+    applyUnder,+    type Rebind (..),+    type PatList (..),+    lengthPL,+  )+where++import Rebound++import qualified Data.Fin as Fin+import qualified Data.Vec as Vec+import Data.Set (Set)+import qualified Data.Set as Set++----------------------------------------------------------+-- * Bind type+----------------------------------------------------------++-- | Type binding 'Size pat' variables.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+data Bind v c (pat :: Type) (n :: Nat) where+  Bind :: pat -> Env v m n -> c (Size pat + m) -> Bind v c pat n++-- | To compare pattern binders, we need to unbind, but also+-- first make sure that the patterns are equal.+instance (Eq pat, Sized pat, forall n. Eq (c n), Subst v c) => Eq (Bind v c pat n) where+  b1 == b2 =+    getPat b1 == getPat b2+      && getBody b1 == getBody b2++-- | Bind a pattern, using the identity substitution.+bind ::+  (Sized pat, Subst v c) =>+  pat ->+  c (Size pat + n) ->+  Bind v c pat n+bind pat = Bind pat idE++-- | Bind a pattern, while suspending the provided substitution.+bindWith :: pat -> Env v m n -> c (Size pat + m) -> Bind v c pat n+bindWith = Bind++-- | Retrieve the pattern of the binding.+getPat :: Bind v c pat n -> pat+getPat (Bind pat env t) = pat++-- | Retrieve the body of the binding.+getBody ::+  forall v c pat n.+  (Sized pat, Subst v c) =>+  Bind v c pat n ->+  c (Size pat + n)+getBody (Bind (pat :: pat) (env :: Env v m n) t) =+  applyOpt applyE (upN (size pat) env) t++-- | Run a function on the body (and pattern), after applying the delayed substitution.+-- The size of the (current) scope is made available at runtime.+unbind ::+  forall v c pat n d.+  (SNatI n, Sized pat, Subst v v, Subst v c) =>+  Bind v c pat n ->+  ((SNatI (Size pat + n)) => pat -> c (Size pat + n) -> d) ->+  d+unbind bnd f =+  withSNat (sPlus (size (getPat bnd)) (snat @n)) $+    f (getPat bnd) (getBody bnd)++-- | Retrieve the body, as well as the bound pattern.+unbindl :: (Sized pat, Subst v c) => Bind v c pat n -> (pat, c (Size pat + n))+unbindl bnd = (getPat bnd, getBody bnd)++-- | Instantiate the body (i.e. replace the bound variables) with the provided terms.+instantiate ::+  forall v c pat n.+  (Sized pat, Subst v c) =>+  Bind v c pat n ->+  Env v (Size pat) n ->+  c n+instantiate b e =+  unbindWith+    b+    (\p r t -> applyOpt applyE (withSNat (size p) $ e .++ r) t)++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder ::+  (Sized pat, Subst v c2) =>+  (forall m. Env v m (Size pat + n2) -> c1 m -> c2 (Size pat + n2)) ->+  Env v n1 n2 ->+  Bind v c1 pat n1 ->+  Bind v c2 pat n2+applyUnder f r2 (Bind p r1 t) =+  Bind p idE (f r' t)+  where+    r' = upN (size p) (r1 .>> r2)++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWith ::+  (Sized pat, SubstVar v) =>+  Bind v c pat n ->+  (forall m. pat -> Env v m n -> c (Size pat + m) -> d) ->+  d+unbindWith (Bind pat (r :: Env v m n) t) f =+  f pat r t++-- | 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 ::+  (Sized pat, SubstVar v) =>+  Bind v c pat n ->+  Env v (Size pat) n ->+  (forall m. Env v m n -> c m -> c n) ->+  c n+instantiateWith b v f = unbindWith b (\p r e -> withSNat (size p) $ f (v .++ r) e)++-----------------------------------------------------------------+-- instances for Bind (Subst, FV, Strengthen)+-----------------------------------------------------------------++-- | The substitution operation composes the explicit+-- substitution with the one stored at the binder+instance (SubstVar v) => Shiftable (Bind v c p) where+  shift = shiftFromApplyE @v++instance (SubstVar v) => Subst v (Bind v c p) where+  applyE :: Env v n m -> Bind v c p n -> Bind v c p m+  applyE env1 (Bind p env2 m) = Bind p (env2 .>> env1) m++instance (Subst v c, Sized p, FV c) => FV (Bind v c p) where+  appearsFree :: Fin n -> Bind v c p n -> Bool+  appearsFree n b =+    appearsFree (Fin.shiftN (size (getPat b)) n) (getBody b)+  freeVars :: forall n. Bind v c p n -> Set (Fin n)+  freeVars b = rescope (size (getPat b)) (freeVars (getBody b))+++instance (Sized p, Subst v c, Strengthen c) => Strengthen (Bind v c p) where+  strengthenRec ::+    SNat k ->+    SNat m ->+    SNat n ->+    Bind v c p (k + (m + n)) ->+    Maybe (Bind v c p (k + n))+  strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) bnd =+    withSNat (sPlus k (sPlus m n)) $+      unbind bnd $ \(p :: p) t' ->+        case ( axiomAssoc @(Size p) @k @(m + n),+               axiomAssoc @(Size p) @k @n+             ) of+          (Refl, Refl) ->+            bind p <$> strengthenRec (sPlus (size p) k) m n t'++-----------------------------------------------------------------+-- * Rebind type+---------------------------------------------------------------++data Rebind pat p2 n where+  Rebind :: pat -> p2 (Size pat + n) -> Rebind pat p2 n++instance (SubstVar v, Sized p1, Subst v p2) => Shiftable (Rebind p1 p2) where+  shift = shiftFromApplyE @v++instance (SubstVar v, Sized p1, Subst v p2) => Subst v (Rebind p1 p2) where+  applyE :: Env v n m -> Rebind p1 p2 n -> Rebind p1 p2 m+  applyE r (Rebind p1 p2) = Rebind p1 (applyE (upN (size p1) r) p2)++instance (Sized p1, FV p2) => FV (Rebind p1 p2) where+  appearsFree :: (Sized p1, FV p2) => Fin n -> Rebind p1 p2 n -> Bool+  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++instance (Sized p1, Strengthen p2) => Strengthen (Rebind p1 p2) where+  strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) (Rebind (p1 :: p1) p2) =+    case ( axiomAssoc @(Size p1) @k @(m + n),+           axiomAssoc @(Size p1) @k @n+         ) of+      (Refl, Refl) ->+        Rebind p1 <$> strengthenRec (sPlus (size p1) k) m n p2++--------------------------------------------------------------+-- * Lists of patterns+--------------------------------------------------------------++-- | lists of patterns where variables at each position bind+-- later in the pattern+data PatList (pat :: Nat -> Type) p where+  PNil :: PatList pat N0+  PCons ::+    (Size (pat p1) ~ p1) =>+    pat p1 ->+    PatList pat p2 ->+    PatList pat (p2 + p1)++-- | The length of a pattern list is the number of patterns,+-- not the number of variables that it binds+lengthPL :: PatList pat p -> Int+lengthPL PNil = 0+lengthPL (PCons _ ps) = 1 + lengthPL ps++instance (forall n. Sized (pat n)) => Sized (PatList pat p) where+  type Size (PatList pat p) = p+  size PNil = s0+  size (PCons (p1 :: pat p1) (p2 :: PatList pat p2)) =+    sPlus @p2 @(Size (pat p1)) (size p2) (size p1)++instance+  (forall p1 p2. PatEq (pat p1) (pat p2)) =>+  PatEq (PatList pat p1) (PatList pat p2)+  where+  patEq :: PatList pat p1 -> PatList pat p2 -> Maybe (p1 :~: p2)+  patEq PNil PNil = Just Refl+  patEq (PCons p1 ps1) (PCons p2 ps2) = do+    Refl <- patEq p1 p2+    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
+ src/Rebound/Bind/PatN.hs view
@@ -0,0 +1,280 @@+-- |+-- Module       : Rebound.Bind.PatN+-- Description  : Bind a number of variables, without metadata+--+-- Bind a number of variables, with no other information stored with the binder.+-- This is a specialization of "Rebound.Bind.Pat".+module Rebound.Bind.PatN+  ( module Rebound,++    PatN(..),++    -- * single binder --+    Bind1 (..),+    bind1,+    unbind1,+    unbindl1,+    getBody1,+    instantiate1,+    bindWith1,+    unbindWith1,+    instantiateWith1,+    applyUnder1,++    -- * double binder --+    Bind2 (..),+    bind2,+    unbind2,+    getBody2,+    instantiate2,+    bindWith2,+    unbindWith2,+    instantiateWith2,+    applyUnder2,++    -- * N-ary binder ---+    BindN (..),+    bindN,+    unbindN,+    unbindlN,+    getBodyN,+    instantiateN,+    bindWithN,+    unbindWithN,+    instantiateWithN,+    applyUnderN,+  )+where++import Rebound.Bind.Pat qualified as Pat+import Rebound++import Data.Fin qualified as Fin+import Data.Vec qualified as Vec++++----------------------------------------------------------------+-- N-ary patterns+----------------------------------------------------------------++-- | A pattern that binds @p@ variables.+newtype PatN (p :: Nat) where+  PatN :: SNat p -> PatN p++deriving instance (Eq (PatN p))+deriving instance (TestEquality PatN)++instance SNatI p => SizeIndex PatN p++instance (SNatI p) => Sized (PatN p) where+  type Size (PatN p) = p+  size (PatN sn) = sn++-- | Type binding a number of variables.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+type BindN v c m n = Pat.Bind v c (PatN m) n++-- | Bind a number of variables, using the identity substitution.+bindN :: forall m v c n. (Subst v c, SNatI m) => c (m + n) -> BindN v c m n+bindN = Pat.bind (PatN (snat @m))++-- | Bind a number of variables, while suspending the provided substitution.+bindWithN :: forall p v c m n. (SNatI p) => Env v m n -> c (p + m) -> BindN v c p n+bindWithN = Pat.bindWith (PatN (snat @p))++-- | 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)) => c (m + n) -> d) -> d+unbindN bnd f = Pat.unbind bnd (const 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++-- | 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++----------------------------------------------------------------+-- Single binder+----------------------------------------------------------------++-- | Type binding 1 variable.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+type Bind1 v c n = Pat.Bind v c (PatN N1) n++-- | Bind 1 variable, using the identity substitution.+bind1 :: (Subst v c) => c (S n) -> Bind1 v c n+bind1 = Pat.bind (PatN s1)++-- | Bind 1 variable, while suspending the provided substitution.+bindWith1 :: forall v c m n. Env v m n -> c (S m) -> Bind1 v c n+bindWith1 = Pat.bindWith (PatN s1)++-- | Run a function on the body, after applying the delayed substitution.+unbind1 ::+  forall v c n d.+  (SNatI n, Subst v c) =>+  Bind1 v c n ->+  ((SNatI (S n)) => c (S n) -> d) ->+  d+unbind1 b f = f (Pat.getBody b)++-- | Retrieve the body of the binding.+-- For this kind of binding, it is equivalent to 'getBody1'.+unbindl1 :: forall v c n. (Subst v c) => Bind1 v c n -> c (S n)+unbindl1 = Pat.getBody++-- | Retrieve the body of the binding.+getBody1 ::+  forall v c n.+  (Subst v c) =>+  Bind1 v c n ->+  c (S n)+getBody1 = Pat.getBody++-- | 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 b v1 = Pat.instantiate b (v1 .: zeroE)++-- | 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. Env v m n -> c (S m) -> d) ->+  d+unbindWith1 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.+instantiateWith1 ::+  (SubstVar v) =>+  Bind1 v c n ->+  v n ->+  (forall m. Env v m n -> c m -> d n) ->+  d n+instantiateWith1 b v1 f =+  unbindWith1 b (\r e -> f (v1 .: r) e)++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder1 ::+  (Subst v c2) =>+  (forall m. Env v m (S n2) -> c1 m -> c2 (S n2)) ->+  Env v n1 n2 ->+  Bind1 v c1 n1 ->+  Bind1 v c2 n2+applyUnder1 = Pat.applyUnder++----------------------------------------------------------------+-- Double binder+----------------------------------------------------------------++-- | Type binding 2 variables.+-- 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 (PatN N2) n++-- | Bind 2 variables, using the identity substitution.+bind2 :: (Subst v c) => c (S (S n)) -> Bind2 v c n+bind2 = Pat.bind (PatN s2)++-- | Bind 2 variables, while suspending the provided substitution.+bindWith2 :: forall v c m n. Env v m n -> c (S (S m)) -> Bind2 v c n+bindWith2 = Pat.bindWith (PatN s2)++-- | Run a function on the body, after applying the delayed substitution.+unbind2 ::+  forall v c n d.+  (Subst v c) =>+  Bind2 v c n ->+  (c (S (S n)) -> d) ->+  d+unbind2 b f = f (getBody2 b)++-- | Retrieve the body of the binding.+-- For this kind of binding, it is equivalent to 'getBody2'.+unbindl2 :: forall v c n. (Subst v c) => Bind2 v c n -> c (S (S n))+unbindl2 = Pat.getBody++-- | Retrieve the body of the binding.+getBody2 ::+  forall v c n.+  (Subst v c) =>+  Bind2 v c n ->+  c (S (S n))+getBody2 = Pat.getBody++-- | 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 v1 v2 = Pat.instantiate b (v1 .: (v2 .: zeroE))++-- | 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. Env v m n -> c (S (S m)) -> d) ->+  d+unbindWith2 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.+instantiateWith2 ::+  (SubstVar v, SNatI n) =>+  Bind2 v c n ->+  v n ->+  v n ->+  (forall m. Env v m n -> c m -> d n) ->+  d n+instantiateWith2 b v1 v2 f =+  unbindWith2 b (\r e -> f (v1 .: (v2 .: r)) e)++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder2 ::+  (Subst v c2) =>+  (forall m. Env v m (S (S n2)) -> c1 m -> c2 (S (S n2))) ->+  Env v n1 n2 ->+  Bind2 v c1 n1 ->+  Bind2 v c2 n2+applyUnder2 = Pat.applyUnder
+ src/Rebound/Bind/Scoped.hs view
@@ -0,0 +1,473 @@+-- | +-- Module       : Rebound.Bind.Scoped+-- Description  : Bind variables while referring to them+--+-- A "Scoped" pattern binds variables but can also include subterms that+-- reference free variables that are already in scope. This is useful for type+-- annotations and telescopes. The pattern type typically has kind+-- @'Nat' -> 'Type'@, the 'Nat' is used to track the (initial) number of free+-- variables. For a simpler interface, see 'Rebound.Bind.Pat.Pat'.+module Rebound.Bind.Scoped (+    module Rebound,+    Bind,+    bind,+    getPat,+    getBody,+    unbind,+    unbindl,+    instantiate,+    unbindWith,+    instantiateWith,+    applyUnder,+    instantiateWeakenEnv,++    -- * Number of binding vars in pats+    ScopedSized(..),+    scopedSize,+    scopedPatEq,+    EqSized,+    EqScopedSized,+    +    -- * Telescopes+    -- IScoped make sense, but are never used anywhere; should be remove it?+    IScopedSized,+    iscopedSize,+    iscopedPatEq,+    TeleList(..),+    lengthTele,+    nil, (<:>),(<++>),+  ) where++import Rebound+import Rebound.Bind.Pat qualified as Pat++import Data.Set (Set)+import Data.Set qualified as Set+import Data.Maybe qualified as Maybe+import Data.Fin qualified as Fin+import Data.Vec qualified as Vec++----------------------------------------------------------+-- Sized type class for patterns+----------------------------------------------------------++-- | Constrain 'ScopedSized' to agree with 'Sized'.+class (Sized (t p), Size (t p) ~ ScopedSize t) => EqSized t p++instance (Sized (t p), Size (t p) ~ ScopedSize t) => EqSized t p++-- | Type class for the size of scoped patterns.+-- The size it returns must be the same as the one returned by 'Sized'.+--+-- This type class is there to force the size of the pattern to be independent+-- of the number of variables in scope. This technique is described by:+-- https://blog.poisson.chat/posts/2022-09-21-quantified-constraint-trick.html+class (forall p. EqSized pat p) => ScopedSized pat where+  type ScopedSize (pat :: Nat -> Type) :: Nat++-- | 'Rebound.Classes.size', but with a type referring to 'ScopedSize'.+scopedSize :: forall pat p. (ScopedSized pat) => pat p -> SNat (ScopedSize pat)+scopedSize = size++-- | Compare two patterns for equality. Provide a proof of equality of their+-- size in case of success.+scopedPatEq ::+  (ScopedSized pat1, ScopedSized pat2, PatEq (pat1 p1) (pat2 p2)) =>+  pat1 p1 ->+  pat2 p2 ->+  Maybe (ScopedSize pat1 :~: ScopedSize pat2)+scopedPatEq = patEq++-- This file uses `ScopedSize`, `scopedSize`, and `scopedNames`,+-- instead of `Size`, `size`, and `names` throughout.++----------------------------------------------------------+-- Scoped Pattern binding+----------------------------------------------------------++-- | The `Bind` type binds (ScopedSize p) variables.+-- Patterns can also include free occurrences of variables, so+-- the type is indexed by a scope level.+-- This data structure includes a delayed+-- substitution for the variables in the body of the binder.+data Bind v c (pat :: Nat -> Type) (n :: Nat) where+  Bind ::+    pat n ->+    Env v m n ->+    c (ScopedSize pat + m) ->+    Bind v c pat n++-- | To compare pattern binders, we need to unbind, but also+-- first make sure that the patterns are equal.+instance (forall n. Eq (c n), +    PatEq (pat m n) (pat m n), +    ScopedSized (pat m), +    Subst v c) => Eq (Bind v c (pat m) n) where+  b1 == b2 =+    Maybe.isJust (patEq (getPat b1) (getPat b2))+      && getBody b1 == getBody b2++-- | Bind a pattern, using the identity substitution.+bind ::+  forall v c pat n.+  (ScopedSized pat, Subst v c) =>+  pat n ->+  c (ScopedSize pat + n) ->+  Bind v c pat n+bind pat = Bind pat idE++-- | Bind a pattern, while suspending the provided substitution.+bindWith ::+  (ScopedSized pat, Subst v c) =>+  pat n -> Env v m n -> c (ScopedSize pat + m) -> Bind v c pat n+bindWith = Bind++-- | Retrieve the pattern of the binding.+getPat :: Bind v c pat n -> pat n+getPat (Bind pat env t) = pat++-- | Retrieve the body of the binding.+getBody ::+  forall v c pat n.+  (ScopedSized pat, Subst v v, Subst v c) =>+  Bind v c pat n ->+  c (ScopedSize pat + n)+getBody (Bind (pat :: pat n) (env :: Env v m n) t) =+  applyE @v @c @(ScopedSize pat + m) (upN (scopedSize pat) env) t++-- | Run a function on the body (and pattern), after applying the delayed substitution.+-- The size of the (current) scope is made available at runtime.+unbind ::+  forall v c pat n d.+  (SNatI n, forall n. ScopedSized pat, Subst v v, Subst v c) =>+  Bind v c pat n ->+  ((SNatI (ScopedSize pat + n)) => pat n -> c (ScopedSize pat + n) -> d) ->+  d+unbind bnd f =+  withSNat (sPlus (scopedSize (getPat bnd)) (snat @n)) $+    f (getPat bnd) (getBody bnd)++-- | Retrieve the body, as well as the bound pattern.+unbindl :: (SNatI n, Subst v c, ScopedSized pat) => Bind v c pat n -> (pat n, c (ScopedSize pat + n))+unbindl bnd = (getPat bnd, getBody bnd)++-- | Instantiate the body (i.e. replace the bound variables) with the provided terms.+instantiate ::+  forall v c pat n.+  (forall n. ScopedSized pat, Subst v c) =>+  Bind v c pat n ->+  Env v (ScopedSize pat) n ->+  c n+instantiate b e =+  unbindWith+    b+    (\p r t -> withSNat (scopedSize p) $ applyE (e .++ r) t)++-- | Apply a function under the binder.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+applyUnder ::+  forall pat v c n1 n2.+  (ScopedSized pat, Subst v v, Subst v c, Subst v pat) =>+  (forall m. Env v m (ScopedSize pat + n2) -> c m -> c (ScopedSize pat + n2)) ->+  Env v n1 n2 ->+  Bind v c pat n1 ->+  Bind v c pat n2+applyUnder f r2 (Bind p r1 t) =+  Bind p' idE (f r' t)+  where+    r' = upN sp' (r1 .>> r2)+    sp' :: SNat (ScopedSize pat)+    sp' = size p'+    p' :: pat n2+    p' = applyE r2 p++-- | Run a function on the body.+-- The delayed substitution is __not__ applied, but is passed to the function instead.+unbindWith ::+  (forall n. Sized (pat n), SubstVar v) =>+  Bind v c pat n ->+  (forall m. pat n -> Env v m n -> c (ScopedSize pat + m) -> d) ->+  d+unbindWith (Bind pat r t) f = f pat r t++-- | 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 ::+  (ScopedSized pat, SubstVar v) =>+  Bind v c pat n ->+  Env v (ScopedSize pat) n ->+  (forall m. Env v m n -> c m -> c n) ->+  c n+instantiateWith b v f =+  unbindWith b (\p r e -> withSNat (scopedSize p) $ f (v .++ r) e)++-- | Map variable 0 to given value, and shift everything else+-- in the environment.+instantiateWeakenEnv ::+  forall p n v c.+  (SubstVar v, Subst v v) =>+  SNat p ->+  SNat n ->+  v (p + n) ->+  Env v (S n) (p + n)+instantiateWeakenEnv p n a =+  a .: shiftNE p++-----------------------------------------------------------------+-- instances for Bind+-----------------------------------------------------------------++instance (ScopedSized pat, Subst v pat, Subst v v) => Shiftable (Bind v c pat) where+  shift = shiftFromApplyE @v++instance (ScopedSized pat, Subst v pat, Subst v v) => Subst v (Bind v c pat) where+  applyE (env1 :: Env v n m) (Bind (pat :: pat n) (env2 :: Env v m1 n) m) =+    Bind (applyE env1 pat) (env2 .>> env1) m++instance+  ( Subst v c,+    ScopedSized p,+    FV p,+    FV c+  ) =>+  FV (Bind v c p)+  where+  appearsFree n b =+    let pat = getPat b+     in appearsFree n pat+          || appearsFree (Fin.shiftN (scopedSize pat) n) (getBody b)++  freeVars :: forall n. (Subst v c, ScopedSized p, FV p, FV c) =>+     Bind v c p n -> Set (Fin n)+  freeVars b =+    let pat = getPat b+        body = getBody b+    in+       freeVars pat <> rescope (scopedSize pat) (freeVars body)+++instance (ScopedSized p, SubstVar v, Subst v v, Subst v c, Strengthen c, Strengthen p) =>+  Strengthen (Bind v c p)+  where+  strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) bnd =+    withSNat (sPlus k (sPlus m n)) $+      unbind bnd $ \(p :: p (k + (m + n))) t' ->+        case ( axiomAssoc @(ScopedSize p) @k @(m + n),+               axiomAssoc @(ScopedSize p) @k @n+             ) of+          (Refl, Refl) ->+            let p' :: Maybe (p (k + n))+                p' = strengthenRec k m n p++                r :: Maybe (c (ScopedSize p + (k + n)))+                r = strengthenRec (sPlus (scopedSize p) k) m n t'+             in bind <$> p' <*> r++-----------------------------------------------------------------+-- Telescopes+---------------------------------------------------------------++-- Telescopes are parameterized by scoped patterns, with kinds+-- `pat :: Nat -> Nat -> Type`. For these types, we need to know+-- that the first argument is the number of binding variables,+-- (i.e. Size or ScopedSize) so we need yet *another* type class+-- to make this constraint.++-- | Constrain 'IScopedSized' to agree with 'ScopedSized'.+class (ScopedSize (t p) ~ p) => EqScopedSized t p++instance (ScopedSize (t p) ~ p) => EqScopedSized t p++-- | An indexed 'ScopedSized'.+class+  ( forall p. ScopedSized (pat p),+    forall p. EqScopedSized pat p+  ) =>+  IScopedSized pat++-- | 'Rebound.Classes.size', but with a type referring to 'IScopedSized'.+iscopedSize :: (IScopedSized pat) => pat p n -> SNat p+iscopedSize = scopedSize++-- | Compare two patterns for equality. Provide a proof of equality of their+-- size in case of success.+iscopedPatEq ::+  (IScopedSized pat1, IScopedSized pat2, PatEq (pat1 p1 n1) (pat2 p2 n2)) =>+  pat1 p1 n1 ->+  pat2 p2 n2 ->+  Maybe (p1 :~: p2)+iscopedPatEq = scopedPatEq++-- | A telescope binds a linear sequence of variables. Each variable can have+-- metadata attached, and that metadata can be indexed. Each piece of metadata+-- can refer to every variable initially in scope, as well as every variables+-- previously introduced by the telescope itself.+-- +-- The type parameters are+-- - @p@ is the number of variables introduced by the telescope+-- - @n@ is the number of free variables for @A1@ (and @A2@ has @S n@, etc.)+--+-- We include some arithmetic properties with each constructors, so that these+-- get brought in scope when pattern matching. Smart constructors 'nil'+-- and '<:>' can be used to easily construct 'TeleList'.+data TeleList (pat :: Nat -> Nat -> Type) p n where+  TNil :: ( n + N0 ~ n) =>+    TeleList pat N0 n+  TCons ::+    ( IScopedSized pat,+      p2 + (p1 + n) ~ (p2 + p1) + n+    ) =>+    pat p1 n ->+    TeleList pat p2 (p1 + n) ->+    TeleList pat (p2 + p1) n++-- | Length of a 'TeleList'.+lengthTele :: TeleList pat p n -> Int+lengthTele TNil = 0+lengthTele (TCons _ ps) = 1 + lengthTele ps++-- | Smart constructor for 'TNil'.+nil :: forall pat n. TeleList pat N0 n+nil = case axiomPlusZ @n of Refl -> TNil++-- | Smart constructor for 'TCons'.+(<:>) ::+  forall p1 p2 pat n.+  (IScopedSized pat) =>+  pat p1 n ->+  TeleList pat p2 (p1 + n) ->+  TeleList pat (p2 + p1) n+e <:> t = case axiomAssoc @p2 @p1 @n of Refl -> TCons e t++-- | Append two telescopes.+(<++>) ::+  forall p1 p2 pat n.+  (IScopedSized pat) =>+  TeleList pat p1 n ->+  TeleList pat p2 (p1 + n) ->+  TeleList pat (p2 + p1) n+TNil <++> t = case axiomPlusZ @p2 of Refl -> t+(TCons @_ @p12 @p11 h t) <++> t' = case axiomAssoc @p2 @p12 @p11 of Refl -> h <:> (t <++> t')++infixr 9 <:>++instance IScopedSized (TeleList pat)++instance ScopedSized (TeleList pat p) where+  type ScopedSize (TeleList pat p) = p++instance Sized (TeleList pat p n) where+  type Size (TeleList pat p n) = p+  size TNil = s0+  size (TCons p1 p2) = sPlus (size p2) (iscopedSize p1)++instance (IScopedSized pat, Subst v v, forall p. Subst v (pat p)) => Shiftable (TeleList pat p) where+  shift = shiftFromApplyE @v++instance+  (IScopedSized pat, Subst v v, forall p. Subst v (pat p)) =>+  Subst v (TeleList pat p)+  where+  applyE r TNil = nil+  applyE r (TCons p1 p2) =+    applyE r p1 <:> applyE (upN (iscopedSize p1) r) p2++instance (IScopedSized pat, forall p. FV (pat p)) => FV (TeleList pat p) where+  appearsFree ::+    forall n.+    (IScopedSized pat, forall p1. FV (pat p1)) =>+    Fin n ->+    TeleList pat p n ->+    Bool+  appearsFree n TNil = False+  appearsFree n (TCons p1 p2) = appearsFree n p1 || appearsFree (Fin.shiftN (iscopedSize p1) n) p2++  freeVars :: TeleList pat p n -> Set (Fin n)+  freeVars TNil = Set.empty+  freeVars (TCons p1 p2) = freeVars p1 <> rescope (iscopedSize p1) (freeVars p2)++instance (forall p1. Strengthen (pat p1)) => Strengthen (TeleList pat p) where+  strengthenRec k m n TNil = Just nil+  strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) (TCons (p1 :: pat p1 (k + (m + n))) p2) =+    case ( axiomAssoc @p1 @k @(m + n),+           axiomAssoc @p1 @k @n+         ) of+      (Refl, Refl) ->+        (<:>)+          <$> strengthenRec k m n p1+          <*> strengthenRec (sPlus (iscopedSize p1) k) m n p2++instance+  (forall p1 p2 n1 n2. PatEq (pat p1 n1) (pat p2 n2), IScopedSized pat) =>+  PatEq (TeleList pat p1 n1) (TeleList pat p2 n2)+  where+  patEq TNil TNil = Just Refl+  patEq (TCons p1 p2) (TCons p1' p2')+    | Just Refl <- iscopedPatEq p1 p1',+      Just Refl <- iscopedPatEq p2 p2' =+        Just Refl+  patEq _ _ = Nothing++-----------------------------------------------------------------+-- Rebind+-- TODO: this is the binary version of a telescope.+-- Captures the left-to-right relationship between two patterns+-- without the list.+---------------------------------------------------------------+{-+data Rebind p1 p2 n where+  Rebind ::+    Plus (Size (p2 n)) (Plus (Size (p1 n)) n) ~ Plus (Plus (Size (p2 n)) (Size (p1 n))) n =>+    p1 n -> p2 (Plus (Size (p1 n)) n) -> Rebind p1 p2 n++rebind :: forall p1 p2 n. p1 n -> p2 (Plus (Size (p1 n)) n) -> Rebind p1 p2 n+rebind p1 p2 =+  case axiomAssoc @(Size (p2 n)) @(Size (p1 n)) @n of+    Refl -> Rebind p1 p2++instance (ScopedSized p1, ScopedSized p2) => Sized (Rebind p1 p2 n) where+    type Size (Rebind p1 p2 n) = Plus (Size (p2 n)) (Size (p1 n))+    size (Rebind p1 p2) = sPlus @(Size (p2 n)) @(Size (p1 n)) (size p2) (size p1)++-- instance (Sized p1, Sized p2) => Sized (Rebind p1 p2) where+--  type Size (Rebind p1 p2) = Plus (Size p2) (Size p1)+--  size (Rebind p1 p2) = sPlus (size p2) (size p1)++instance+  (Subst v v, forall n. ScopedSized p1, Subst v p1, Subst v p2) =>+  Subst v (Rebind p1 p2)+  where+  applyE ::+    (Subst v v, ScopedSized p1, Subst v p2) =>+    Env v n m ->+    Rebind p1 p2 n ->+    Rebind p1 p2 m+  applyE r (Rebind p1 p2) =+    rebind (applyE r p1) (applyE (upN (size p1) r) p2)++instance (forall n. ScopedSized p1, FV p2) => FV (Rebind p1 p2) where+  appearsFree :: (ScopedSized p1, FV p2) => Fin n -> Rebind p1 p2 n -> Bool+  appearsFree n (Rebind p1 p2) = appearsFree (shiftN (size p1) n) p2++unRebind ::+  forall p1 p2 n c.+  (ScopedSized p1, ScopedSized p2, SNatI n) =>+  Rebind p1 p2 n ->+  ( ( SNatI (Size (p1 n)),+      SNatI (Size (p2 n)),+      SNatI (Plus (Size (p1 n)) n),+      Plus (Size (p2 n)) (Plus (Size (p1 n)) n) ~ Plus (Plus (Size (p2 n)) (Size (p1 n))) n+    ) =>+    p1 n ->+    p2 (Plus (Size (p1 n)) n) ->+    c+  ) ->+  c+unRebind (Rebind p1 p2) f =+  case axiomAssoc @(Size (p2 n)) @(Size (p1 n)) @n of+    Refl ->+      withSNat (size p1) $+        withSNat (size p2) $+          withSNat (sPlus (size p1) (snat @n)) $+            f p1 p2+-}
+ src/Rebound/Bind/Single.hs view
@@ -0,0 +1,70 @@+-- |+-- Module       : Rebound.Bind.Single+-- Description  : Bind a single variable, without metadata+--+-- Simplest form of binding: a single variable with no other information stored with the binder.+-- This is a specialization of "Rebound.Bind.PatN".+module Rebound.Bind.Single+  ( module Rebound,+    Bind (..),+    bind,+    unbind,+    unbindl,+    getBody,+    instantiate,+    bindWith,+    unbindWith,+    instantiateWith,+    applyUnder,+  )+where++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+
+ src/Rebound/Classes.hs view
@@ -0,0 +1,211 @@+-- |+-- Module      : Rebound.Classes+-- Description : Type class definitions+--+-- Main typeclasses used by the library.++{-# LANGUAGE DefaultSignatures #-}+module Rebound.Classes where++import Rebound.Lib+import Data.LocalName+import Data.Scoped.List(List, pattern Nil, pattern (:<))+import Data.Scoped.List qualified as List++import Data.Foldable+import Data.Vec qualified as Vec+import Data.Fin qualified as Fin+import Data.Set (Set)+import Data.Set qualified as Set++import GHC.Generics (Generic1(..))++----------------------------------------------------------+-- Indices/variables shifting+----------------------------------------------------------++-- | Bring a scoped type into a new, bigger, scope, through variable shifting.+-- +-- This class is used for types which are scoped, yet do not allow+-- substitution in general. Typical examples are data-structures which+-- associate metadata to variables.+-- See 'Rebound.Refinement.Refinement' for an example. +class Shiftable t where+  shift :: SNat k -> t n -> t (k + n)+  -- a good default implementation of this is `shiftFromApply`. But the +  -- `Subst` class is not yet in scope.  +  +----------------------------------------------------------+-- Free variables+----------------------------------------------------------++-- | Computes the set of free variables in a term.+class FV (t :: Nat -> Type) where+  -- | Does a particular variable appear free?+  appearsFree :: Fin n -> t n -> Bool+  default appearsFree :: (Generic1 t, GFV (Rep1 t)) => Fin n -> t n -> Bool+  appearsFree x e = gappearsFree x (from1 e)+  {-# INLINE appearsFree #-}++  -- | Calculate all of the free variables in a term.+  freeVars :: t n -> Set (Fin n)+  default freeVars :: (Generic1 t, GFV (Rep1 t)) => t n -> Set (Fin n)+  freeVars e = gfreeVars (from1 e)+  {-# INLINE freeVars #-}++-- | Generic programming support for 'FV'.+class GFV (t :: Nat -> Type) where+  gappearsFree :: Fin n -> t n -> Bool+  gfreeVars :: t n -> Set (Fin n)++----------------------------------------------------------+-- * Strengthening+----------------------------------------------------------++-- Strengthening cannot be implemented through substitution because it+-- must fail if the term uses invalid variables. Therefore, we make a+-- class of scoped types that can be strengthened.++-- | Eliminates the most recently bound variable from the term (if unused).+strengthen :: forall n t. (Strengthen t, SNatI n) => t (S n) -> Maybe (t n)+strengthen = strengthenRec s0 s1 (snat :: SNat n)++-- | Eliminates the @n@ most recently bound variables from the term (if unused).+strengthenN :: forall m n t. (Strengthen t, SNatI n) => SNat m -> t (m + n) -> Maybe (t n)+strengthenN m = strengthenRec s0 m (snat :: SNat n)++-- | Bring scoped terms into a smaller scope, if possible.+--+-- Strengthening is only possible if the term only refers to variable which+-- are in the smaller scope.+class Strengthen t where+  -- generalize strengthening -- remove m variables from the middle of the scope+  strengthenRec :: SNat k -> SNat m -> SNat n -> t (k + (m + n)) -> Maybe (t (k + n))+  default strengthenRec :: (Generic1 t, GStrengthen (Rep1 t)) =>+     SNat k -> SNat m -> SNat n -> t (k + (m + n)) -> Maybe (t (k + n))+  strengthenRec k m n t = to1 <$> gstrengthenRec k m n (from1 t)++  -- Remove a single variable from the middle of the scope+  strengthenOneRec :: forall k n. SNat k -> SNat n -> t (k + S n) -> Maybe (t (k + n))+  strengthenOneRec k = strengthenRec k s1++-- | Generic programming support for 'Strengthen'.+class GStrengthen (t :: Nat -> Type) where+  gstrengthenRec :: SNat k -> SNat m -> SNat n -> t (k + (m + n)) -> Maybe (t (k + n))++----------------------------------------------------------+-- FV and Strengthen instances for Data.Scoped.List+---------------------------------------------------------++instance FV t => FV (List t) where+  appearsFree :: Fin n -> List t n -> Bool+  appearsFree x = List.any (appearsFree x)++  freeVars :: List t n -> Set (Fin n)+  freeVars = List.foldr (\x s -> freeVars x `Set.union` s) Set.empty++instance Strengthen t => Strengthen (List t) where+  strengthenRec :: SNat k -> SNat m -> SNat n -> List t (k + (m + n)) -> Maybe (List t (k + n))+  strengthenRec k m n Nil = Just Nil+  strengthenRec k m n (x :< xs) = (:<) <$> strengthenRec k m n x <*> strengthenRec k m n xs++----------------------------------------------------------+-- FV and Strengthen instances for Fin+---------------------------------------------------------++instance FV Fin where+  appearsFree = (==)+  freeVars = Set.singleton++instance Strengthen Fin where+  strengthenRec :: SNat k -> SNat m -> SNat n-> Fin (k + (m + n)) -> Maybe (Fin (k + n))+  strengthenRec = Fin.strengthenRecFin++-- | Update a set of free variables to a new scope through strengthening+rescope :: forall n k. SNat k -> Set (Fin (k + n)) -> Set (Fin n)+rescope k = foldMap g where+   g :: Fin (k + n) -> Set (Fin n)+   g x = maybe+     Set.empty Set.singleton+     (Fin.strengthenRecFin s0 k (undefined :: SNat n) x)++----------------------------------------------------------+-- Type classes for patterns+----------------------------------------------------------++-- | Calculate the number of binding variables in the pattern+-- This number does not need to be an explicit parameter of the type+-- so that we have flexibility about what types we can use as+-- patterns.+class Sized (t :: Type) where+  -- Retrieve size from the type (number of variables bound by the pattern)+  type Size t :: Nat+  -- Access size as a term+  size :: t -> SNat (Size t)++-- | Pairs of types that can be compared with each other as patterns+class PatEq (t1 :: Type) (t2 :: Type) where+    patEq :: t1 -> t2 -> Maybe (Size t1 :~: Size t2)++-- | Class of patterns that are indexed by a natural number+-- where the size is that index directly+class (Sized (t p), Size (t p) ~ p) => SizeIndex t p+++---------------------------------------------------------+-- Pattern Class Instances for Prelude and Lib Types+---------------------------------------------------------++-- ** LocalNames++instance Sized LocalName where+  type Size LocalName = N1+  size _ = s1++instance PatEq LocalName LocalName where+  patEq p1 p2 = Just Refl++-- ** SNats+instance Sized (SNat n) where+  type Size (SNat n) = n+  size n = n++instance PatEq (SNat n1) (SNat n2) where+  patEq = testEquality+++-- ** Vectors++instance Sized (Vec n a) where+  type Size (Vec n a) = n+  size = Vec.vlength++instance Eq a => PatEq (Vec n1 a) (Vec n2 a) where+  patEq VNil VNil = Just Refl+  patEq (x ::: xs) (y ::: ys) | x == y,+    Just Refl <- patEq xs ys+    = Just Refl+  patEq _ _ = Nothing++-- ** Unit (trivial)++instance Sized () where { type Size () = N0 ;  size _ = SZ }++instance PatEq () () where patEq _ _ = Just Refl++-- ** Pairs++instance (Sized a, Sized b) => Sized (a,b) where+   type Size (a,b) = Size a + Size b+   size (x,y) = sPlus (size x) (size y)++instance (PatEq a1 a2, PatEq b1 b2) => PatEq (a1, b1) (a2, b2) where+   patEq (x1,y1) (x2,y2)+     | Just Refl <- patEq x1 x2+     , Just Refl <- patEq y1 y2+     = Just Refl+   patEq _ _ = Nothing++------------------------------------------++
+ src/Rebound/Context.hs view
@@ -0,0 +1,57 @@+-- |+-- Module       : Rebound.Context+-- Description  : Typing contexts+module Rebound.Context(Ctx, emptyC, (+++), (++++)) where++import Rebound.Lib+import Rebound.Env+import Rebound.Classes++----------------------------------------------------------------+-- Typing context utilities for dependently-typed languages+----------------------------------------------------------------++-- | A typing context maps indices to type in the same scope.+type Ctx v n = Env v n n++-- This is not weakening --- it increments all variables by one+shiftC :: forall v n. (SubstVar v) => v n -> v (S n)+shiftC = applyE @v shift1E++shiftCtx :: (SubstVar v) => Env v n n -> Env v n (S n)+shiftCtx g = g .>> shift1E++-- | An empty context, that includes no variable assumptions+emptyC :: Ctx v N0+emptyC = zeroE++-- | "Snoc" a new definition to the end of the context+-- All existing types in the context need to be shifted (lazily)+(+++) :: forall v n. (SubstVar v) => Ctx v n -> v n -> Ctx v (S n)+g +++ a = applyE @v shift1E a .: (g .>> shift1E)+++-- | Append contexts. Shifts all indices in the first argument by the length+-- of the second.+(++++) :: forall v n n' m. (SNatI n', SubstVar v) => Env v n m -> Env v n' (n' + m) -> Env v (n' + n) (n' + m)+l ++++ r =+  let p = snat @n'+   in r .++ (l .>> shiftNE p)+++-- Example usage++data Exp n = Star | Var (Fin n) deriving Show+instance SubstVar Exp where var = Var+instance Subst Exp Exp where+    applyE s Star = Star+    applyE s (Var x) = applyEnv s x+++-- c :: Ctx Exp N4+-- x : * , y : x, z : x , w : *+c = emptyC +++ Star +++ Var FZ +++ Var (FS FZ) +++ Star++-- >>> applyEnv c (FS FZ)+-- Var 3+
+ src/Rebound/Env.hs view
@@ -0,0 +1,211 @@+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternSynonyms #-}++-- |+-- Module      : Rebound.Env+-- Description : Environments, or mappings from variables to terms+--+-- Environments, also called _parallel substitutions_ or _multi-substitutions_,+-- map all variables in a scope to terms in another scope.+++module Rebound.Env+  ( Env,+    applyEnv,+    SubstVar (..),+    Subst (..),+    Shiftable (..),+    GSubst (..),+    gapplyE,+    applyOpt,+    transform,+    zeroE,+    oneE,+    singletonE,+    idE,+    (.>>),+    (.:),+    (.++),+    head,+    tail,+    appendE,+    up,+    upN,+    shift1E,+    shiftNE,+    fromVec,+    toVec,+    tabulate,+    fromTable,+    weakenE',+    weakenER,+    shiftFromApplyE,+  )+where++-- The concrete implementation of environments can be changed by replacing+-- this import with an alternative one.+import Rebound.Env.Lazy++import Rebound.Classes (Shiftable (..))+import Rebound.Lib+import Control.Monad+import Data.Scoped.List (List, pattern Nil, pattern (:<))++import Data.Fin qualified as Fin+import Data.Map qualified as Map+import Data.Vec qualified as Vec+import GHC.Generics hiding (S)+import Prelude hiding (head, tail)++----------------------------------------------+-- operations on environments/substitutions+----------------------------------------------++-- | Convert a function into an environment.+env :: forall m v n. (SubstVar v, SNatI m) => (Fin m -> v n) -> Env v m n+env f = fromVec v+  where+    v :: Vec m (v n)+    v = Vec.tabulate f++-- | A singleton environment (single index domain),+-- which maps that single variable to the provided term.+oneE :: (SubstVar v) => v n -> Env v (S Z) n+oneE v = v .: zeroE++-- | An environment that maps index 0 to the provided term, and maps+-- all other indices to themselves.+singletonE :: (SubstVar v) => v n -> Env v (S n) n+singletonE v = v .: idE++-- | An identity environment, which maps all indices to themselves.+idE :: (SubstVar v) => Env v n n+idE = shiftNE s0++-- | Append two environments.+--+-- The `SNatI` constraint is a runtime witness for the length+-- of the domain of the first environment.+(.++) ::+  (SNatI p, SubstVar v) =>+  Env v p n ->+  Env v m n ->+  Env v (p + m) n+(.++) = appendE snat+-- By using a class constraint, this can be an infix operation.++-- | Append two environments, with the length @SNat p@ explicitly required.+--+-- If the length is implicitly available, '.++' might be preferable.+appendE ::+  (SubstVar v) =>+  SNat p ->+  Env v p n ->+  Env v m n ->+  Env v (p + m) n+appendE SZ e1 e2 = e2+appendE (snat_ -> SS_ p1) e1 e2 =+  head e1 .: appendE p1 (tail e1) e2++newtype AppendE v m n p = MkAppendE+  { getAppendE ::+      Env v p n ->+      Env v m n ->+      Env v (p + m) n+  }++-- | Access the term at index 0.+head :: (SubstVar v) => Env v (S n) m -> v m+head f = applyEnv f FZ++-- | Increment all free variables in image by 1.+shift1E :: (SubstVar v) => Env v n (S n)+shift1E = shiftNE s1++-- | Increment all free variables by @p@.+upN ::+  forall v p m n.+  (Subst v v) =>+  SNat p ->+  Env v m n ->+  Env v (p + m) (p + n)+upN p = getUpN @_ @_ @_ @p (withSNat p (induction base step))+  where+    base :: UpN v m n Z+    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)++newtype UpN v m n p = MkUpN {getUpN :: Env v m n -> Env v (p + m) (p + n)}++-- | Allow to implement 'Shiftable' using 'Subst'.+shiftFromApplyE :: forall v c k n. (SubstVar v, Subst v c) => SNat k -> c n -> c (k + n)+shiftFromApplyE k = applyE @v (shiftNE k)++----------------------------------------------------+-- Create an environment from a length-indexed+-- vector of scoped values++-- | Convert an environment to a 'Vec'.+fromVec :: (SubstVar v) => Vec m (v n) -> Env v m n+fromVec VNil = zeroE+fromVec (x ::: vs) = x .: fromVec vs++-- | Convert a 'Vec' to an environment.+toVec :: (SubstVar v) => SNat m -> Env v m n -> Vec m (v n)+toVec SZ r = VNil+toVec m@(snat_ -> SS_ m') r = head r ::: toVec m' (tail r)++----------------------------------------------------------------+-- show for environments+----------------------------------------------------------------++instance (SNatI n, Show (v m), SubstVar v) => Show (Env v n m) where+  show x = show (tabulate x)++-- | Convert an environment to an association list.+tabulate :: (SNatI n, Subst v v) => Env v n m -> [(Fin n, v m)]+tabulate r = map (\f -> (f, applyEnv r f)) Fin.universe++-- | Convert an association list to an environment.+fromTable ::+  forall n v.+  (SNatI n, SubstVar v) =>+  [(Fin n, v n)] ->+  Env v n n+fromTable rho =+  env $ \f -> case lookup f rho of+    Just t -> t+    Nothing -> var f++++----------------------------------------------------------------+-- Subst instances for List and Fin+----------------------------------------------------------------++-- Scoped List++instance Subst v t => Subst v (List t) where+  applyE r Nil = Nil+  applyE r (x :< xs) = applyE r x :< applyE r xs++-- Fin++instance Shiftable Fin where+  shift = Fin.shiftN++instance SubstVar Fin where+  var x = x++instance {-# OVERLAPS #-} Subst Fin Fin where+  applyE = applyEnv++instance {-# OVERLAPPABLE #-} (SubstVar v) => Subst v Fin where+  applyE = error "BUG: missing isVar definition?"++instance GSubst b Fin where+  gsubst s f = error "BUG: missing isVar definition?"
+ src/Rebound/Env/Functional.hs view
@@ -0,0 +1,121 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use lambda-case" #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.Functional where++-- Represents the environment using a function+++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+import GHC.Generics hiding (S)+++------------------------------------------------------------------------------+-- 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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++gapplyE :: forall v c 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 #-}++------------------------------------------------------------------------------+-- Environment representation as finite function+------------------------------------------------------------------------------++newtype Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) =+    Env { applyEnv :: Fin n -> a m }++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Build an optimized version of applyE (does nothing here)+applyOpt :: (Env v n m -> c n -> c m) -> (Env v n m -> c n -> c m)+applyOpt f = f+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Env $ \ x -> case x of {}+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER m = Env $ \x -> var (Fin.weakenFinRight m x)+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' m = Env $ \x -> var (Fin.weakenFin m x)+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE m = Env $ \x -> var (Fin.shiftN m x)+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: SubstVar v => v m -> Env v n m -> Env v (S n) m+ty .: s = Env $ \y -> case y of+                 FZ -> ty+                 FS x -> applyEnv s x+{-# 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 #-}++-- | composition: do f then g+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | smart constructor for composition+comp :: forall a m n p. SubstVar a =>+         Env a m n -> Env a n p -> Env a m p+comp s1 s2 = Env $ \x -> applyE s2 (applyEnv s1 x)+{-# INLINEABLE comp #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+up e = var Fin.f0 .: comp e (shiftNE s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f g = Env $ \x -> f (applyEnv g x)+{-# INLINEABLE transform #-}
+ src/Rebound/Env/Lazy.hs view
@@ -0,0 +1,191 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.Lazy where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is strict+-- Includes optimized composition (Inc and Cons cancel)+-- Includes Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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+------------------------------------------------------------------------------++-- | Maps variables in scope @n@ to terms (of type @a@) in scope @m@.+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: (SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: (SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: (SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> (Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: (Env a m n) -> (Env a n p) -> Env a m p --  compose substitutions+++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s++applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = Fin.absurd x+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- | Increase the bound on free variables (on the right), without changing any free variable.+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- | Increase the bound on free variables (on the left), without changing any free variable.+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# 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 = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ an environment, adding a new mapping+-- for index '0'. All keys are shifted over.+(.:) :: v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# INLINEABLE (.:) #-}++-- | @uncons@ an environment, removing the mapping for index '0'.+-- All other keys are shifted back.+tail :: (SubstVar v) => Env v (S n) m -> Env v n m+tail x = shiftNE s1 .>> x+{-# INLINEABLE tail #-}++-- | Compose two environments, applying them in sequence (left then right).+-- Some optimizations will be applied to optimize the resulting environment.+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | Compose two environments, applying them in sequence (left then right).+-- Some optimizations will be applied to optimize the resulting environment.+--+-- Some of the applied optimizations are:+-- - Identity environments (e.g., @'shiftNE' SZ@) are eliminated+-- - Absorbing environments on the right (i.e., 'zeroE') are eliminated+-- - Compatible environments are fused (e.g., @'weakenER' n@ and @'weakenER' m)+comp :: forall a m n p. SubstVar a =>+         Env a m n -> Env a n p -> Env a m p+comp Zero s = Zero+comp (Weak (k1 :: SNat m1)) (Weak (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Weak (sPlus k2 k1)+comp (Weak SZ) s = s+comp s (Weak SZ) = s+comp (WeakR (k1 :: SNat m1)) (WeakR (k2 :: SNat m2))  =+  case axiomAssoc @m @m1 @m2 of+    Refl -> WeakR (sPlus k1 k2)+comp (WeakR SZ) s =+  case axiomPlusZ @m of+    Refl -> s+comp s (WeakR SZ) =+  case axiomPlusZ @n of+    Refl -> s+comp (Inc (k1 :: SNat m1)) (Inc (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Inc (sPlus k2 k1)+comp s (Inc SZ) = s+comp (Inc SZ) s = s+comp (Inc (snat_ -> SS_ p1)) (Cons _t p) = comp (Inc p1) p+comp (s1 :<> s2) s3 = comp s1 (comp s2 s3)+comp (Cons t s1) s2 = Cons (applyE s2 t) (comp s1 s2)+comp s1 s2 = s1 :<> s2+{-# INLINEABLE comp #-}++-- | Adapt an environment to go under a binder.+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ+up e = var Fin.f0 .: comp e (Inc s1)+{-# INLINEABLE up #-}++-- | 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 (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Env/LazyA.hs view
@@ -0,0 +1,182 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.LazyA where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is strict+-- Includes optimized composition (Inc and Cons cancel)+-- does not include Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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 #-}++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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: (SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: (SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: (SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> (Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: (Env a m n) -> (Env a n p) -> Env a m p --  compose substitutions++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s+applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = case x of {}+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x -}+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# 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 #-}++-- | composition: do f then g+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | smart constructor for composition+comp :: forall a m n p. SubstVar a =>+         Env a m n -> Env a n p -> Env a m p+comp Zero s = Zero+comp (Weak (k1 :: SNat m1)) (Weak (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Weak (sPlus k2 k1)+comp (Weak SZ) s = s+comp s (Weak SZ) = s+comp (WeakR (k1 :: SNat m1)) (WeakR (k2 :: SNat m2))  =+  case axiomAssoc @m @m1 @m2 of+    Refl -> WeakR (sPlus k1 k2)+comp (WeakR SZ) s =+  case axiomPlusZ @m of+    Refl -> s+comp s (WeakR SZ) =+  case axiomPlusZ @n of+    Refl -> s+comp (Inc (k1 :: SNat m1)) (Inc (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Inc (sPlus k2 k1)+comp s (Inc SZ) = s+comp (Inc SZ) s = s+comp (Inc (snat_ -> SS_ p1)) (Cons _t p) = comp (Inc p1) p+comp (s1 :<> s2) s3 = comp s1 (comp s2 s3)+comp (Cons t s1) s2 = Cons (applyE s2 t) (comp s1 s2)+comp s1 s2 = s1 :<> s2+{-# INLINEABLE comp #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+{- up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ  -}+up e = var Fin.f0 .: comp e (Inc s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Env/LazyB.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.LazyB where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is lazy+-- No optimized composition (Inc and Cons cancel)+-- No Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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 #-}++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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: (SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: (SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: (SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> (Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: (Env a m n) -> (Env a n p) -> Env a m p --  compose substitutions+++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s+applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = case x of {}+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: (SubstVar v) => v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# 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 #-}++-- | composition: do f then g+-- No optimizations here+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = (:<>)+{-# INLINEABLE (.>>) #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ+up e = var Fin.f0 .: (e :<> Inc s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Env/Strict.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.Strict where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is strict+-- Includes optimized composition (Inc and Cons cancel)+-- Includes Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++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 #-}++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: !(SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: !(SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: !(SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> !(Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: !(Env a m n) -> !(Env a n p) -> Env a m p --  compose substitutions++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s++applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = Fin.absurd x+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# 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 #-}++-- | composition: do f then g+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | smart constructor for composition+-- Names of some cases are taken from Abadi et. al "Explicit Substitutions"+comp :: forall a m n p. SubstVar a =>+         Env a m n -> Env a n p -> Env a m p+comp Zero s = Zero+comp (Weak (k1 :: SNat m1)) (Weak (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Weak (sPlus k2 k1)+comp (Weak SZ) s = s+comp s (Weak SZ) = s+comp (WeakR (k1 :: SNat m1)) (WeakR (k2 :: SNat m2))  =+  case axiomAssoc @m @m1 @m2 of+    Refl -> WeakR (sPlus k1 k2)+comp (WeakR SZ) s =+  case axiomPlusZ @m of+    Refl -> s+comp s (WeakR SZ) =+  case axiomPlusZ @n of+    Refl -> s+comp (Inc (k1 :: SNat m1)) (Inc (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Inc (sPlus k2 k1)+-- (sort of) ShiftId+comp s (Inc SZ) = s+-- IdL+comp (Inc SZ) s = s+-- ShiftCons+comp (Inc (snat_ -> SS_ p1)) (Cons _t p) = comp (Inc p1) p+-- Ass+comp (s1 :<> s2) s3 = comp s1 (comp s2 s3)+-- Map+comp (Cons t s1) s2 = Cons (applyE s2 t) (comp s1 s2)+comp s1 s2 = s1 :<> s2+{-# INLINEABLE comp #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ+up e = var Fin.f0 .: comp e (Inc s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Env/StrictA.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.StrictA where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is strict+-- Includes optimized composition (Inc and Cons cancel)+-- does not include Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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 #-}++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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: !(SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: !(SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: !(SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> !(Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: !(Env a m n) -> !(Env a n p) -> Env a m p --  compose substitutions++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2++------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s+applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = case x of {}+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x -}+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# 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 #-}++-- | composition: do f then g+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = comp+{-# INLINEABLE (.>>) #-}++-- | smart constructor for composition+comp :: forall a m n p. SubstVar a =>+         Env a m n -> Env a n p -> Env a m p+comp Zero s = Zero+comp (Weak (k1 :: SNat m1)) (Weak (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Weak (sPlus k2 k1)+comp (Weak SZ) s = s+comp s (Weak SZ) = s+comp (WeakR (k1 :: SNat m1)) (WeakR (k2 :: SNat m2))  =+  case axiomAssoc @m @m1 @m2 of+    Refl -> WeakR (sPlus k1 k2)+comp (WeakR SZ) s =+  case axiomPlusZ @m of+    Refl -> s+comp s (WeakR SZ) =+  case axiomPlusZ @n of+    Refl -> s+comp (Inc (k1 :: SNat m1)) (Inc (k2 :: SNat m2))  =+  case axiomAssoc @m2 @m1 @m of+    Refl -> Inc (sPlus k2 k1)+comp s (Inc SZ) = s+comp (Inc SZ) s = s+comp (Inc (snat_ -> SS_ p1)) (Cons _t p) = comp (Inc p1) p+comp (s1 :<> s2) s3 = comp s1 (comp s2 s3)+comp (Cons t s1) s2 = Cons (applyE s2 t) (comp s1 s2)+comp s1 s2 = s1 :<> s2+{-# INLINEABLE comp #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+{- up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ  -}+up e = var Fin.f0 .: comp e (Inc s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Env/StrictB.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_HADDOCK hide #-}+module Rebound.Env.StrictB where++-- "Defunctionalized" representation of environment+-- stored values are lazy+-- *rest* of the environment is strict+-- No optimized composition (Inc and Cons cancel)+-- No Wadler's optimizations for the empty environment++import Rebound.Lib+import Data.Fin (Fin(..))+import qualified Data.Fin as Fin+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 #-}++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+class GSubst v (e :: Nat -> Type) where+  gsubst :: Env v m n -> e m -> e n++------------------------------------------------------------------------------+-- Environment representation+------------------------------------------------------------------------------+data Env (a :: Nat -> Type) (n :: Nat) (m :: Nat) where+  Zero  :: Env a Z n+  WeakR :: !(SNat m) -> Env a n (n + m) --  weaken values in range by m+  Weak  :: !(SNat m) -> Env a n (m + n) --  weaken values in range by m+  Inc   :: !(SNat m) -> Env a n (m + n) --  increment values in range (shift) by m+  Cons  :: (a m) -> !(Env a n m) -> Env a ('S n) m --  extend a substitution (like cons)+  (:<>) :: !(Env a m n) -> !(Env a n p) -> Env a m p --  compose substitutions++instance (forall n. NFData (a n)) => NFData (Env a n m) where+  rnf Zero = ()+  rnf (WeakR m) = rnf m+  rnf (Weak m) = rnf m+  rnf (Inc m) = rnf m+  rnf (Cons x r) = rnf x `seq` rnf r+  rnf (r1 :<> r2) = rnf r1 `seq` rnf r2+------------------------------------------------------------------------------+-- Application+------------------------------------------------------------------------------++-- | Value of the index x in the substitution s+applyEnv :: SubstVar a => Env a n m -> Fin n -> a m+applyEnv Zero x = case x of {}+applyEnv (Inc m) x = var (Fin.shiftN m x)+applyEnv (WeakR m) x = var (Fin.weakenFinRight m x)+applyEnv (Weak m) x = var (Fin.weakenFin m x)+applyEnv (Cons ty _s) FZ = ty+applyEnv (Cons _ty s) (FS x) = applyEnv s x+applyEnv (s1 :<> s2) x = applyE s2 (applyEnv s1 x)+{-# 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 (Weak SZ) x = x+applyOpt f (WeakR SZ) (x :: c m) =+  case axiomPlusZ @m of Refl -> x+applyOpt f r x = f r x+{-# INLINEABLE applyOpt #-}++------------------------------------------------------------------------------+-- Construction and modification+------------------------------------------------------------------------------++-- | The empty environment (zero domain)+zeroE :: Env v Z n+zeroE = Zero+{-# INLINEABLE zeroE #-}++-- make the bound bigger, on the right, but do not change any indices.+-- this is an identity function+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)+weakenER = WeakR+{-# INLINEABLE weakenER #-}++-- make the bound bigger, on the left, but do not change any indices.+-- this is an identity function+weakenE' :: forall m v n. (SubstVar v) => SNat m -> Env v n (m + n)+weakenE' = Weak+{-# INLINEABLE weakenE' #-}++-- | increment all free variables by m+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)+shiftNE = Inc+{-# INLINEABLE shiftNE #-}++-- | @cons@ -- extend an environment with a new mapping+-- for index '0'. All existing mappings are shifted over.+(.:) :: (SubstVar v) => v m -> Env v n m -> Env v (S n) m+(.:) = Cons+{-# 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 #-}++-- | composition: do f then g+-- No optimizations here+(.>>) :: (Subst v v) => Env v p n -> Env v n m -> Env v p m+(.>>) = (:<>)+{-# INLINEABLE (.>>) #-}++-- | modify an environment so that it can go under a binder+up :: (SubstVar v) => Env v m n -> Env v (S m) (S n)+up (Inc SZ) = Inc SZ+up (Weak SZ) = Weak SZ+up (WeakR SZ) = WeakR SZ+up e = var Fin.f0 .: (e :<> Inc s1)+{-# INLINEABLE up #-}++-- | mapping operation for range of the environment+transform :: (SubstVar b) => (forall m. a m -> b m) -> Env a n m -> Env b n m+transform f Zero = Zero+transform f (Weak x) = Weak x+transform f (WeakR x) = WeakR x+transform f (Inc x) = Inc x+transform f (Cons a r) = Cons (f a) (transform f r)+transform f (r1 :<> r2) = transform f r1 :<> transform f r2+
+ src/Rebound/Generics.hs view
@@ -0,0 +1,125 @@+{-# OPTIONS_HADDOCK hide #-}++module Rebound.Generics where+    +import GHC.Generics hiding (S)+import Rebound.Env+import Rebound.Classes+import Data.Set qualified as Set++--------------------------------------------+-- Generic implementation of Subst class+--------------------------------------------++-- Constant types+instance GSubst v (K1 i c) where+  gsubst s (K1 c) = K1 c+  {-# INLINE gsubst #-}++instance GSubst v U1 where+  gsubst _s U1 = U1+  {-# INLINE gsubst #-}++instance (GSubst b f) => GSubst b (M1 i c f) where+  gsubst s = M1 . gsubst s . unM1+  {-# INLINE gsubst #-}++instance GSubst b V1 where+  gsubst _s = error "BUG: void type"+  {-# INLINE gsubst #-}++instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where+  gsubst s (f :*: g) = gsubst s f :*: gsubst s g+  {-# INLINE gsubst #-}++instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where+  gsubst s (L1 f) = L1 $ gsubst s f+  gsubst s (R1 g) = R1 $ gsubst s g+  {-# INLINE gsubst #-}++instance (Subst b g) => GSubst b (Rec1 g) where+  gsubst s (Rec1 f) = Rec1 (applyE s f)+  {-# INLINE gsubst #-}++--------------------------------------------+-- Generic implementation of FV class+--------------------------------------------++instance (FV t) => GFV (Rec1 t) where+  gappearsFree s (Rec1 f) = appearsFree s f+  {-# INLINE gappearsFree #-}+  gfreeVars (Rec1 f) = freeVars f+  {-# INLINE gfreeVars #-}++-- Constant types+instance GFV (K1 i c) where+  gappearsFree s (K1 c) = False+  {-# INLINE gappearsFree #-}+  gfreeVars (K1 c) = Set.empty+  {-# INLINE gfreeVars #-}++instance GFV U1 where+  gappearsFree _s U1 = False+  {-# INLINE gappearsFree #-}+  gfreeVars U1 = Set.empty++instance GFV f => GFV (M1 i c f) where+  gappearsFree s = gappearsFree s . unM1+  {-# INLINE gappearsFree #-}+  gfreeVars = gfreeVars . unM1+  {-# INLINE gfreeVars #-}++instance GFV V1 where+  gappearsFree _s = error "BUG: void type"+  {-# INLINE gappearsFree #-}+  gfreeVars v = error "BUG: void type"+  {-# INLINE gfreeVars #-}++instance (GFV f, GFV g) => GFV (f :*: g) where+  gappearsFree s (f :*: g) = gappearsFree s f && gappearsFree s g+  {-# INLINE gappearsFree #-}+  gfreeVars (f :*: g) = gfreeVars f <> gfreeVars g+  {-# INLINE gfreeVars #-}++instance (GFV f, GFV g) => GFV (f :+: g) where+  gappearsFree s (L1 f) = gappearsFree s f+  gappearsFree s (R1 g) = gappearsFree s g+  {-# INLINE gappearsFree #-}++  gfreeVars (L1 f) = gfreeVars f+  gfreeVars (R1 g) = gfreeVars g+  {-# INLINE gfreeVars #-}++------------------------------------------------+-- Generic implementation of Strengthening class+------------------------------------------------++++instance GStrengthen (K1 i c) where+  gstrengthenRec m n k (K1 c) = pure (K1 c)+  {-# INLINE gstrengthenRec #-}++instance GStrengthen U1 where+  gstrengthenRec m n k U1 = pure U1+  {-# INLINE gstrengthenRec #-}++instance GStrengthen f => GStrengthen (M1 i c f) where+  gstrengthenRec m n k x = M1 <$> gstrengthenRec m n k (unM1 x)+  {-# INLINE gstrengthenRec #-}++instance GStrengthen V1 where+  gstrengthenRec m n k = error "BUG: void type"+  {-# INLINE gstrengthenRec #-}++instance (GStrengthen f, GStrengthen g) => GStrengthen (f :*: g) where+  gstrengthenRec m n k (f :*: g) = (:*:) <$> gstrengthenRec m n k f <*> gstrengthenRec m n k g+  {-# INLINE gstrengthenRec #-}++instance (GStrengthen f, GStrengthen g) => GStrengthen (f :+: g) where+  gstrengthenRec m n k (L1 f) = L1 <$> gstrengthenRec m n k f+  gstrengthenRec m n k (R1 g) = R1 <$> gstrengthenRec m n k g+  {-# INLINE gstrengthenRec #-}++instance Strengthen t => GStrengthen (Rec1 t) where+  gstrengthenRec k m n (Rec1 t) = Rec1 <$> strengthenRec k m n t
+ src/Rebound/Lib.hs view
@@ -0,0 +1,30 @@+-- |+-- Description: Library for dependent types+--+-- Imports and re-exports libraries for Dependent Haskell+-- Because 'Fin' and 'Vec' include definitions with the same+-- name as Prelude functions, clients of this module should also+-- import them this way:+--+-- @+-- import 'Data.Fin' qualified as 'Fin'+-- import 'Data.Vec' qualified as 'Vec'+-- @+module Rebound.Lib+  (+    type Type,+    module Data.Type.Equality,+    Fin (..),+    Vec (..),+    ToInt (..),+    module Data.Nat,+    module Data.SNat,+  )+where++import Data.Fin (Fin (..))+import Data.Kind (Type)+import Data.Nat+import Data.SNat+import Data.Type.Equality+import Data.Vec (Vec (..))
+ src/Rebound/MonadNamed.hs view
@@ -0,0 +1,86 @@+-- |+-- Description: Monads supporting scopes of names+-- Stability: experimental+--+-- This is a simplified version of 'Rebound.MonadScoped.MonadScopedReader',+-- where the environment is restricted to a vector of names.++module Rebound.MonadNamed+  ( Sized (..),+    S.MonadScopedReader,+    Scope,+    ScopedReader (..),+    ScopedReaderT (..),+    scope,+    pushVec,+    push,+    LocalName (..),+    runScopedReader,+    runScopedReaderT,+  )+where++import Rebound hiding (fromVec)+import Data.SNat as SNat+import Data.Vec as Vec+import qualified Rebound.MonadScoped as S+import Rebound.MonadScoped (MonadScopedReader(..))+import Data.LocalName++-----------------------------------------------------------------------+-- Scopes+-----------------------------------------------------------------------++-- | A mapping from variables in scope to a name.+newtype Scope name n = Scope {names :: Vec n name}+  deriving (Eq, Show)++emptyScope :: Scope name Z+emptyScope = Scope VNil++fromVec :: Vec p name -> Scope name p+fromVec v = Scope v++extendScope ::+  forall p n name.+  (SNatI p) =>+  Vec p name ->+  Scope name n ->+  Scope name (p + n)+extendScope v (Scope s) = Scope $ Vec.append v s++-----------------------------------------------------------------------+-- MonadScoped class+-----------------------------------------------------------------------++-- | Get the name of variables in scope.+scope :: MonadScopedReader (Scope name) m => m n (Vec n name)+scope = readerS names++-- | Add a new variable to the scope.+push :: (MonadScopedReader (Scope name) m)+  => name -> m (S n) a -> m n a+push n = localS (extendScope (n ::: VNil))++-- | Add a vector of new variables to the scope.+pushVec :: (MonadScopedReader (Scope name) m)+  => Vec p name -> m (p + n) a -> m n a+pushVec v = withSNat (vlength v) $ localS (extendScope v)++-----------------------------------------------------------------------+-- ScopedReader monad+-----------------------------------------------------------------------++-- | A monad transformer to keep track of the name of variables in scope.+type ScopedReaderT name m n a = S.ScopedReaderT (Scope name) m n a++-- | A monad to keep track of the name of variables in scope.+type ScopedReader name n a = S.ScopedReader (Scope name) n a++-- | Run the computation with the provided vector of names.+runScopedReaderT :: forall m n name a. ScopedReaderT name m n a -> Vec n name -> m a+runScopedReaderT c v = S.runScopedReaderT c (Scope v)++-- | Run the computation with the provided vector of names.+runScopedReader :: forall n name a. ScopedReader name n a -> Vec n name -> a+runScopedReader c v = S.runScopedReader c (Scope v)
+ src/Rebound/MonadScoped.hs view
@@ -0,0 +1,195 @@+-- |+-- Description: Scoped variants of some monads+--+-- Provides scoped variants of monads from [mtl](https://hackage.haskell.org/package/mtl).++module Rebound.MonadScoped+  ( MonadScopedReader (..),+    ScopedReader (..),+    ScopedReaderT (..),+    asksS,+    runScopedReader,+    MonadScopedState (..),+    ScopedState (..),+    ScopedStateT (..),+    evalScopedState,+    evalScopedStateT,+    execScopedState,+    execScopedStateT,+    modifyS,+    getsS+  )+where++import Control.Monad (liftM2, (>=>))+import Control.Monad.Error.Class (MonadError (..))+import Control.Monad.Identity (Identity (runIdentity))+import Control.Monad.Reader (MonadReader (ask, local), asks)+import Control.Monad.Writer (MonadWriter (..))+import Data.Kind (Type)+import Data.Nat (Nat (S))+import Data.SNat (type (+))++-----------------------------------------------------------------------+-- Reader class+-----------------------------------------------------------------------++-- | Scoped variant of 'Control.Monad.Reader.MonadReader'.+--+-- __Note__: the "environment" mentioned here as nothing to do with 'Rebound.Env.Env'!+class (forall n. Monad (m n)) => MonadScopedReader e m | m -> e where+  {-# MINIMAL (askS | readerS), localS #-}+  -- | Retrieve the environment.+  askS :: m n (e n)+  askS = readerS id+  -- | Run a function in an altered environment.+  localS :: (e n -> e n') -> m n' a -> m n a+  -- | Retrieve a function of the environment.+  readerS :: (e n -> a) -> m n a+  readerS f = f <$> askS++-- | Retrieve the environment.+asksS :: (MonadScopedReader e m) => (e n -> a) -> m n a+asksS = readerS++-----------------------------------------------------------------------+-- Reader monad+-----------------------------------------------------------------------++-- | Computations that need a (read-only) environment.+type ScopedReader e n a = ScopedReaderT e Identity n a++-- | Run the computation with the provided environment.+runScopedReader :: ScopedReader e n a -> e n -> a+runScopedReader c m = runIdentity $ runScopedReaderT c m++-----------------------------------------------------------------------+-- Reader transformer+-----------------------------------------------------------------------++-- | A scoped variant of 'Control.Monad.Reader.ReaderT'.+newtype ScopedReaderT e m n a = ScopedReaderT {runScopedReaderT :: e n -> m a}+  deriving (Functor)++instance (Applicative m) => Applicative (ScopedReaderT e m n) where+  pure f = ScopedReaderT $ \x -> pure f+  ScopedReaderT f <*> ScopedReaderT x = ScopedReaderT (\e -> f e <*> x e)++instance (Monad m) => Monad (ScopedReaderT e m n) where+  ScopedReaderT m >>= k = ScopedReaderT $ \e ->+    m e >>= (\v -> let x = k v in runScopedReaderT x e)++instance (MonadReader r m) => MonadReader r (ScopedReaderT e m n) where+  ask = ScopedReaderT $ const ask+  local f m = ScopedReaderT (local f . runScopedReaderT m)++instance (MonadError e m) => MonadError e (ScopedReaderT se m n) where+  throwError e = ScopedReaderT $ const (throwError e)+  catchError m k = ScopedReaderT $ \s -> runScopedReaderT m s `catchError` (\err -> runScopedReaderT (k err) s)++instance (MonadWriter w m) => MonadWriter w (ScopedReaderT e m n) where+  writer w = ScopedReaderT $ const (writer w)+  listen m = ScopedReaderT $ \s -> listen $ runScopedReaderT m s+  pass m = ScopedReaderT $ \s -> pass $ runScopedReaderT m s++instance (Monad m) => MonadScopedReader e (ScopedReaderT e m) where+  askS = ScopedReaderT return+  localS f (ScopedReaderT g) = ScopedReaderT $ g . f++-----------------------------------------------------------------------+-- State class+-----------------------------------------------------------------------++-- | Scoped variant of 'Control.Monad.State.MonadState'.+class (forall n. Monad (m n)) => MonadScopedState s m | m -> s where+  {-# MINIMAL rescope, (stateS | (getS, putS)) #-}+  -- | Change the scope of the environment, run a function, and change back the scope.+  rescope :: (s n -> s n') -> (s n' -> s n) -> m n' a -> m n a++  -- | Retrieve the state.+  getS :: m n (s n)+  getS = stateS $ \s -> (s, s)++  -- | Set the state.+  putS :: s n -> m n ()+  putS s = stateS $ const ((), s)++  -- | Lift a function into a monadic computation.+  stateS :: (s n -> (a, s n)) -> m n a+  stateS f = do+    s <- getS+    let (v, s') = f s+    putS s'+    return v++-- | Apply a function to the state.+modifyS :: (MonadScopedState s m) => (s n -> s n) -> m n ()+modifyS f = do+  s <- getS+  putS $ f s++-- | Retrieve a function of the state.+getsS :: (MonadScopedState s m) => (s n -> a) -> m n a+getsS f = f <$> getS++-----------------------------------------------------------------------+-- State monad+-----------------------------------------------------------------------++-- | Computations that need a state.+type ScopedState s n a = ScopedStateT s Identity n a++-- | Run the computation with the provided state, and return the result as well as the final state.+runScopedState :: ScopedState s n a -> s n -> (a, s n)+runScopedState m s = runIdentity $ runScopedStateT m s++-- | Run the computation with the provided state, and return the result.+evalScopedState :: ScopedState s n a -> s n -> a+evalScopedState m s = runIdentity $ evalScopedStateT m s++-- | Run the computation with the provided state, and return the final state.+execScopedState :: ScopedState s n a -> s n -> s n+execScopedState m s = runIdentity $ execScopedStateT m s++-----------------------------------------------------------------------+-- State transformer+-----------------------------------------------------------------------++-- | A scoped variant of 'Control.Monad.State.StateT'.+newtype ScopedStateT s m n a = ScopedStateT {runScopedStateT :: s n -> m (a, s n)}+  deriving (Functor)++-- | Run the computation with the provided state, and return the result.+evalScopedStateT :: (Functor m) => ScopedStateT s m n a -> s n -> m a+evalScopedStateT m s = fst <$> runScopedStateT m s++-- | Run the computation with the provided state, and return the final state.+execScopedStateT :: (Functor m) => ScopedStateT s m n a -> s n -> m (s n)+execScopedStateT m s = snd <$> runScopedStateT m s++-- A bit disappointing, but mtl does also require m to be a monad...+instance (Monad m) => Applicative (ScopedStateT s m n) where+  pure f = ScopedStateT $ \s -> pure (f, s)+  (<*>) = liftM2 (\f a -> f a)++instance (Monad m) => Monad (ScopedStateT s m n) where+  ScopedStateT m >>= k = ScopedStateT $ m >=> (\ (m', s') -> runScopedStateT (k m') s')++instance (MonadReader r m) => MonadReader r (ScopedStateT s m n) where+  ask = ScopedStateT $ \s -> asks (,s)+  local f m = ScopedStateT (local f . runScopedStateT m)++instance (MonadError e m) => MonadError e (ScopedStateT se m n) where+  throwError e = ScopedStateT $ const (throwError e)+  catchError m k = ScopedStateT $ \s -> runScopedStateT m s `catchError` (\err -> runScopedStateT (k err) s)++instance (MonadWriter w m) => MonadWriter w (ScopedStateT s m n) where+  writer w = ScopedStateT $ \s -> (,s) <$> writer w+  listen m = ScopedStateT $ \s -> (\((m, s'), w) -> ((m, w), s')) <$> listen (runScopedStateT m s)+  pass m = ScopedStateT $ \s -> pass ((\((m, r), s') -> ((m, s'), r)) <$> runScopedStateT m s)++instance (Monad m) => MonadScopedState s (ScopedStateT s m) where+  stateS f = ScopedStateT $ pure . f+  rescope up low m = ScopedStateT $ \s -> do+    (r, s') <- runScopedStateT m (up s)+    return (r, low s')
+ src/Rebound/Refinement.hs view
@@ -0,0 +1,85 @@+-- |+-- Module: Rebound.Refinement+-- Description : Refinement from variables to terms+--+-- Refinements map variables in a scope to terms which live in the same scope.++module Rebound.Refinement(+    Refinement(..),+    emptyR,+    joinR,+    singletonR,+    toEnvironment,+    fromEnvironment,+    refine,+    domain)+ where++import Rebound.Lib ( SNatI, SNat, type (+), Fin )+import Rebound.Env+import Data.Map as Map+import Control.Monad+import Data.Fin as Fin++-- | A refinement is a special kind of substitution that does not+-- change the scope, it just replaces all uses of a particular variable+-- with some other term, which lives in the same scope.+newtype Refinement v n = Refinement (Map (Fin n) (v n))++-- | The empty refinement. Maps every variable to itself.+emptyR :: Refinement v n+emptyR = Refinement Map.empty++-- | Join/merge/meld two refinements.+-- Fails if the two refinements have overlapping domains.+joinR ::+  forall v n.+  (SNatI n, Subst v v, Eq (v n)) =>+  Refinement v n ->+  Refinement v n ->+  Maybe (Refinement v n)+joinR (Refinement xs) (Refinement ys) =+  Refinement <$> foldM f ys xs'+  where+    xs' = Map.toList xs+    r = fromTable xs'+    f :: Map.Map (Fin n) (v n) -> (Fin n, v n) -> Maybe (Map.Map (Fin n) (v n))+    f m (k, v)+      | Map.member k ys = Nothing+      | otherwise =+          let v' = applyE r v+           in Just $ if v' == var k then m else Map.insert k (applyE r v) m++-- | A singleton refinement.+-- Maps the specified variable to the specified term, and every other variable+-- gets mapped to itself.+singletonR :: (SubstVar v, Eq (v n)) => (Fin n, v n) -> Refinement v n+singletonR (x, t) =+  if t == var x then emptyR else Refinement (Map.singleton x t)++instance (Shiftable v) => Shiftable (Refinement v) where+  shift :: forall k n. SNat k -> Refinement v n -> Refinement v (k + n)+  shift k (Refinement (r :: Map.Map (Fin n) (v n))) = Refinement g'+    where+      f' = Map.mapKeysMonotonic (Fin.shiftN @k @n k) r+      g' = Map.map (shift k) f'++-- | Convert a refinement into an environment.+toEnvironment :: (SNatI n, SubstVar v) => Refinement v n -> Env v n n+toEnvironment (Refinement x) = fromTable (Map.toList x)++-- | Convert a refinement to an environment.+fromEnvironment :: (SNatI n, SubstVar v) => Env v n n -> Refinement v n+fromEnvironment r = Refinement (Map.fromList (tabulate r))++-- | Checks whether this refinement refines a variable.+refines :: forall n v. (SNatI n, Subst v v, Eq (v n)) => Refinement v n -> Fin n -> Bool+refines r i = applyE (toEnvironment r) (var @v i) /= var @v i++-- | Apply the refinement to a variable.+refine :: (SNatI n, Subst v c) => Refinement v n -> c n -> c n+refine r = applyE (toEnvironment r)++-- | Returns the domain of the environment (i.e., the list of refined variables).+domain :: Refinement v n -> [Fin n]+domain (Refinement m) = Map.keys m
+ test/All.hs view
@@ -0,0 +1,26 @@+import Examples.DepMatch qualified as DepMatch+import Examples.LC qualified as LC+import Examples.LCLet qualified as LCLet+import Examples.PTS qualified as PTS+import Examples.Pat qualified as Pat+import Examples.PureSystemF qualified as PureSystemF+import Examples.LinLC qualified as LinLC+import Test.Tasty++main :: IO ()+main = do+  defaultMain $+    testGroup+      "All"+      [ LC.all,+        LCLet.all,+        Pat.all,+        testGroup+          "System F"+          [ -- TODO: add System F tests+            PureSystemF.all+          ],+        PTS.all,+        DepMatch.all,+        LinLC.all+      ]
+ test/Examples/DepMatch.hs view
@@ -0,0 +1,40 @@+module Examples.DepMatch where++import Data.Fin (f0, f1)+import DepMatch+import Rebound (N2, Nat (S), appearsFree, s1, snat, strengthenRec, zeroE, (.:))+import Rebound.Bind.PatN (bind1)+import Test.Tasty+import Test.Tasty.HUnit+import Utils++instance Eq Err where _ == _ = False++sig :: Exp n -> Exp (S n) -> Exp n+sig l r = Sigma l (bind1 r)++all :: TestTree+all =+  testGroup+    "DepMatch"+    [ testCase "Pattern-match tm0 with pat0" $+        ((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",+      testCase "Pretty-print t1" $ show t1 @?= "λ_. (λ_. (1 (λ_. (0 0))))",+      testCase "Pretty-print tyid" $ show tyid @?= "Pi *. 0 -> 1",+      testCase "Pretty-print tmid" $ show tmid @?= "λ_. (λ_. 0)",+      testCase "Eval t1" $ eval t1 @?= lam (lam $ Var f1 `App` lam (Var f0 `App` Var f0)),+      testCase "Eval application" $+        eval (t1 `App` t0) @?= lam (lam (Var f0) `App` lam (Var f0 `App` Var f0)),+      testCase "Step application" $+        step (t1 `App` t0) @?= Just (lam (lam (Var f0) `App` lam (Var f0 `App` Var f0))),+      testCase "Check tmid : tyid" $ checkType zeroE tmid tyid @?= Right (),+      testCase "Type (tmid tyid)" $ case inferType zeroE (tmid `App` tyid) of+        Left (AnnotationNeeded err) -> err @?= lam (lam (Var f0))+        _ -> assertFailure "Expected an `AnnotationNeeded` error."+    ]
+ test/Examples/LC.hs view
@@ -0,0 +1,42 @@+module Examples.LC where++import HOAS qualified+import LC+import LCQC qualified+import Rebound (zeroE)+import ScopeCheck qualified+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck qualified as QC++all :: TestTree+all =+  testGroup+    "LC"+    [ testCase "Pretty-print t0" $ show t0 @?= "(λ. 0)",+      testCase "Eval application" $ eval (t `App` t0) @?= t0,+      testCase "Pretty-print t2" $ show t2 @?= "((λ. (λ. 1)) ((λ. 0) (λ. 0)))",+      testCase "Eval t2" $ show (eval t2) @?= "(λ. (λ. 0))",+      testCase "Step application" $ step (t0 `App` t0) @?= Just t0,+      testCase "Eval' application" $ eval' 5 (t `App` t0) @?= Just t0,+      testCase "WHNF" $ show (whnfEnv zeroE t) @?= "(λ. ((0 ((λ. 0) 0)) (λ. 0)))",+      localOption (QC.QuickCheckTests 10) $+        testGroup+          "LCQC"+          [ QC.testProperty "nf1 normalizes" LCQC.prop_nf1,+            QC.testProperty "nfEnv normalizes" LCQC.prop_nfEnv+          ],+      testGroup+        "ScopeCheck"+        [ testCase "Scope idExp" $ ScopeCheck.scopeCheck ScopeCheck.idExp @?= Just t0,+          testCase "Scope trueExp" $ ScopeCheck.scopeCheck ScopeCheck.trueExp @?= Just (lam $ lam v1),+          testCase "Scope ill-scoped" $ ScopeCheck.scopeCheck ScopeCheck.illScoped @?= Nothing+        ],+      testGroup+        "HOAS"+        [ testCase "Convert tru" $ HOAS.cvt HOAS.tru @?= lam (lam v1),+          testCase "Convert tru" $ HOAS.cvt HOAS.fls @?= lam (lam v0),+          testCase "Convert app" $ HOAS.cvt HOAS.app @?= lam (lam $ v1 @@ v0),+          testCase "Convert omega" $ HOAS.cvt HOAS.omega @?= (lam (v0 @@ v0) @@ lam (v0 @@ v0))+        ]+    ]
+ test/Examples/LCLet.hs view
@@ -0,0 +1,21 @@+module Examples.LCLet where++import LCLet+import Test.Tasty+import Test.Tasty.HUnit++all :: TestTree+all =+  testGroup+    "LCLet"+    [ testCase "Pretty-print t0" $ show t0 @?= "(λ. 0)",+      testCase "Pretty-print t1" $ show t1 @?= "(λ. (λ. (1 ((λ. 0) 0))))",+      testCase "Pretty-print t2" $ show t2 @?= "(let (λ. 0) in (0 0))",+      testCase "Pretty-print t3" $ show t3 @?= "(let rec (λ. (0 (1 0))) in 0)",+      testCase "Pretty-print t4" $ show t4 @?= "<let-tele>",+      testCase "Eval t1" $ show (eval t1) @?= "(λ. (λ. (1 ((λ. 0) 0))))",+      testCase "Eval application" $ show (eval (t1 @@ t0)) @?= "(λ. ((λ. 0) ((λ. 0) 0)))",+      testCase "Eval t2" $ show (eval t2) @?= "(λ. 0)",+      -- testCase "Eval t3" $ show (eval t3) @?= <Infinite loop>,+      testCase "Eval t4" $ show (eval t4) @?= "(λ. 0)"+    ]
+ test/Examples/LinLC.hs view
@@ -0,0 +1,41 @@+module Examples.LinLC where++import Data.Vec (Vec ((:::)), empty)+import LinLC+import Rebound (Nat (Z))+import Test.Tasty+import Test.Tasty.HUnit++tcS :: Exp Z -> Ty -> Assertion+tcS t ty = runTC empty (checkType t ty) @?= Right ()++tcF :: Exp Z -> Ty -> String -> Assertion+tcF t ty msg = runTC empty (checkType t ty) @?= Left msg++all :: TestTree+all =+  testGroup+    "LinLC"+    [ testCase "Check id" $+        tcS (lam v0) (TyUnit ~> TyUnit),+      testCase "Check app" $+        tcS (lam $ lam $ v0 @@ v1) (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit),+      testCase "Check 1 unused" $+        tcF+          (lam $ lam v1)+          (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit)+          "Variable was not used.",+      testCase "Check type mismatch" $+        tcF+          (lam $ lam v0)+          (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit)+          "Inferred type does not match expected type.",+      testCase "Check 2 unused" $+        tcF+          (lam $ lam v0)+          (TyUnit ~> (TyUnit ~> TyUnit) ~> TyUnit ~> TyUnit)+          "Variable was not used.",+      testCase "Initial scope must be used" $+        runTC (TyUnit ::: (TyUnit ~> TyUnit) ::: TyUnit ::: empty) (checkType (v1 @@ v0) TyUnit)+          @?= Left "Some variables in the initial scope were not used."+    ]
+ test/Examples/PTS.hs view
@@ -0,0 +1,50 @@+module Examples.PTS where++import Data.Fin (f0, f1)+import PTS+import Rebound (Nat (S), appearsFree, idE, s1, snat, strengthenRec, zeroE)+import Rebound.Bind.PatN+import Test.Tasty+import Test.Tasty.HUnit+import Prelude hiding (pi)++lam :: Exp n -> Exp (S n) -> Exp n+lam tTy t = Lam tTy (bind1 t)++pi :: Exp n -> Exp (S n) -> Exp n+pi tTy t = Pi tTy (bind1 t)++instance Eq Err where _ == _ = False++all :: TestTree+all =+  testGroup+    "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,+      testCase "Pretty-print t0" $ show t0 @?= "λ *. 0",+      testCase "Pretty-print t1" $ show t1 @?= "λ *. λ *. 1 ((λ *. 0) 0)",+      testCase "Pretty-print tyid" $ show tyid @?= "Pi *. 0 -> 1",+      testCase "Pretty-print tmid" $ show tmid @?= "λ *. λ 0. 0",+      testCase "Eval t1" $+        eval t1 @?= lam Star (lam Star (Var f1 `App` (lam Star (Var f0) `App` Var f0))),+      testCase "Eval application" $+        eval (t1 `App` t0)+          @?= lam Star (lam Star (Var f0) `App` (lam Star (Var f0) `App` Var f0)),+      testCase "Step application" $+        step (t1 `App` t0)+          @?= Just (lam Star (lam Star (Var f0) `App` (lam Star (Var f0) `App` Var f0))),+      testCase "Normalize t1" $ nf t1 @?= lam Star (lam Star (Var f1 `App` Var f0)),+      testCase "Normalize application" $+        nf (t1 `App` t0) @?= lam Star (Var f0),+      testCase "EvalEnv t1" $+        evalEnv idE t1 @?= lam Star (lam Star (Var f1 `App` (lam Star (Var f0) `App` Var f0))),+      testCase "Type tmid" $ inferType zeroE tmid @?= Right (pi Star $ pi (Var f0) (Var f1)),+      testCase "Type application" $+        inferType zeroE (tmid `App` tyid)+          @?= Right (pi (pi Star (pi (Var f0) (Var f1))) (pi Star (pi (Var f0) (Var f1))))+    ]
+ test/Examples/Pat.hs view
@@ -0,0 +1,30 @@+module Examples.Pat where++import Pat+import Rebound (N2, Nat (Z), snat, zeroE, (.:))+import Test.Tasty+import Test.Tasty.HUnit+import Utils++all :: TestTree+all =+  testGroup+    "Pat"+    [ testCase "Pretty-print t0" $ show t0 @?= "λ. 0",+      testCase "Pretty-print t1" $ show t1 @?= "λ. λ. 1 (λ. 0 0)",+      testCase "Pretty-print t2" $ show t2 @?= "λ. case 0 of [Nil => 0,(Cons V) V => 0]",+      testCase "Pretty-print t3" $ show t3 @?= "(cons a) ((cons b) nil)",+      testCase "Pretty-print t4" $ show t4 @?= "λ. case 0 of [Nil => 0,(Cons V) V => 0] ((cons a) ((cons b) nil))",+      testCase "Pattern-match e1 with p1" $+        ((snat @N2,) <$> patternMatch p1 e1) @?= Just (snat @N2, Con "B" .: (Con "A" .: zeroE @_ @Z)),+      testCase "Pattern-match e1 with p2" $ ((snat @N2,) <$> patternMatch p2 e1) @?= Nothing,+      testCase "Pattern-match e2 with p1" $ ((snat @N2,) <$> patternMatch p1 e2) @?= Nothing,+      testCase "Pattern-match e2 with p2" $+        ((snat @N2,) <$> patternMatch p2 e2) @?= Just (snat @N2, Con "C" .: (Con "A" .: zeroE @_ @Z)),+      testCase "Eval t1" $ show (eval t1) @?= "λ. λ. 1 (λ. 0 0)",+      testCase "Eval application" $ show (eval (t1 `App` t0)) @?= "λ. λ. 0 (λ. 0 0)",+      testCase "Eval t4" $ show (eval t4) @?= "case (cons a) ((cons b) nil) of [Nil => (cons a) ((cons b) nil),(Cons V) V => 0]",+      testCase "Step application" $ show (step (t1 `App` t0)) @?= "Just (λ. λ. 0 (λ. 0 0))",+      testCase "Normalize t1" $ show (nf t1) @?= "λ. λ. 1 0",+      testCase "Normalize application" $ show (nf (t1 `App` t0)) @?= "λ. λ. 0 0"+    ]
+ test/Examples/PureSystemF.hs view
@@ -0,0 +1,46 @@+module Examples.PureSystemF where++import Data.Fin (f0, f1)+import PureSystemF+import Rebound (LocalName (..))+import Rebound.Bind.Local (bind)+import Test.Tasty+import Test.Tasty.HUnit++pureTC t = runTC emptyEnv $ inferType t++bbNat = TAll $ bind (LocalName "X") $ TArr (TArr (Var f0) (Var f0)) (TArr (Var f0) (Var f0))++all :: TestTree+all =+  testGroup+    "SystemF"+    [ testGroup+        "Diadic"+        -- TODO: add test cases+        [],+      testGroup+        "Pure"+        [ testCase "Pretty-print t0" $ show t0 @?= "ΛX. λx. x",+          testCase "Pretty-print t1" $ show t1 @?= "ΛX. λf. λx. f [X] x",+          testCase "Pretty-print t2" $ show t2 @?= "λX. λx. x",+          testCase "Infer t0" $+            pureTC t0+              @?= Right (TAll $ bind (LocalName "X") (TArr (Var f0) (Var f0))),+          testCase "Infer t1" $+            pureTC t1+              @?= Right+                ( TAll $+                    bind+                      (LocalName "X")+                      ( TArr+                          (TAll $ bind (LocalName "Y") (TArr (Var f0) (Var f0)))+                          (TArr (Var f0) (Var f0))+                      )+                ),+          testCase "Infer t2" $ pureTC t2 @?= Left "Term variable occurs in type",+          testCase "Infer Boehm-Berarducci Nat 0" $ pureTC bbn0 @?= Right bbNat,+          testCase "Infer Boehm-Berarducci Nat 1" $ pureTC bbn1 @?= Right bbNat,+          testCase "Infer Boehm-Berarducci Nat 2" $ pureTC bbn2 @?= Right bbNat+        ]+    ]
+ test/Utils.hs view
@@ -0,0 +1,17 @@+module Utils where++import Rebound (Env, SNat (..), SNatI, SubstVar, head, snat, tail, withSNat)+import Prelude hiding (head, tail)++envEq ::+  forall v n m.+  (SNatI n, forall k. Eq (v k), SubstVar v) =>+  Env v n m ->+  Env v n m ->+  Bool+envEq l r = case snat @n of+  SZ -> True+  SS -> head l == head r && envEq (tail l) (tail r)++instance {-# OVERLAPPING #-} (forall k. Eq (v k), SubstVar v) => Eq (SNat n, Env v n m) where+  (n, l) == (_, r) = withSNat n $ envEq l r