blanks 0.4.2 → 0.5.0

raw patch · 25 files changed

+1183/−636 lines, 25 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +0/−1
• blanks.cabal +15/−7
• src/Blanks.hs +5/−2
• src/Blanks/Conversion.hs +27/−0
• src/Blanks/Core.hs +40/−0
• src/Blanks/Interface.hs +0/−209
• src/Blanks/LocScope.hs +111/−21
• src/Blanks/Located.hs +2/−2
• src/Blanks/Name.hs +2/−2
• src/Blanks/Scope.hs +126/−14
• src/Blanks/ScopeW.hs +78/−48
• src/Blanks/Split.hs +107/−0
• src/Blanks/Tracked.hs +85/−0
• src/Blanks/Under.hs +69/−0
• src/Blanks/UnderScope.hs +0/−119
• test/Main.hs +4/−2
• test/Test/Blanks/Exp.hs +254/−0
• test/Test/Blanks/ExpTest.hs +51/−0
• test/Test/Blanks/LocScopeTest.hs +0/−164
• test/Test/Blanks/Parsing.hs +5/−5
• test/Test/Blanks/ScopeTest.hs +20/−40
• test/Test/Blanks/SimpleScope.hs +43/−0
• test/Test/Blanks/SplitScope.hs +45/−0
• test/Test/Blanks/SplitTest.hs +70/−0
• test/Test/Blanks/TrackedTest.hs +24/−0

@@ -19,6 +19,5 @@ bound variables), but if you stick to the provided combinators, things will work out fine.  You'll get most of what you want by just importing this module unqualified.-See the `Blanks` class definition and related methods to manipulate variables and abstractions. See `Scope` for the basic wrapper and `LocScope` for a wrapper with annotations you can use for source locations and the like. See the test suite for examples.

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: bce7c1157ad17dfb08bdd82fd1d9cef7f5aead112c1349019b6dbfed38de7959+-- hash: 3e66404b6e808993a99490ba1327e8e872e5dee4cfb34980b7cd5f84ce47aba6  name:           blanks-version:        0.4.2+version:        0.5.0 synopsis:       Fill-in-the-blanks - A library factoring out substitution from ASTs description:    Please see the README on GitHub at <https://github.com/ejconlon/blanks#readme> category:       Language@@ -29,20 +29,23 @@ library   exposed-modules:       Blanks-      Blanks.Interface+      Blanks.Conversion+      Blanks.Core       Blanks.Located       Blanks.LocScope       Blanks.Name       Blanks.NatNewtype       Blanks.Scope       Blanks.ScopeW+      Blanks.Split       Blanks.Sub-      Blanks.UnderScope+      Blanks.Tracked+      Blanks.Under   other-modules:       Paths_blanks   hs-source-dirs:       src-  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds   build-depends:       adjunctions >=4.4 && <5@@ -58,13 +61,18 @@   main-is: Main.hs   other-modules:       Test.Blanks.Assertions-      Test.Blanks.LocScopeTest+      Test.Blanks.Exp+      Test.Blanks.ExpTest       Test.Blanks.Parsing       Test.Blanks.ScopeTest+      Test.Blanks.SimpleScope+      Test.Blanks.SplitScope+      Test.Blanks.SplitTest+      Test.Blanks.TrackedTest       Paths_blanks   hs-source-dirs:       test-  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N   build-depends:       adjunctions >=4.4 && <5

@@ -1,14 +1,17 @@ -- | You'll get most of what you want by just importing this module unqualified.--- See the 'Blanks' class definition and related methods to manipulate variables and abstractions. -- See 'Scope' for the basic wrapper and 'LocScope' for a wrapper with annotations you can use -- for source locations and the like. See the test suite for examples. module Blanks   ( module Blanks+  , BinderScope (..)   ) where -import Blanks.Interface as Blanks+import Blanks.Conversion as Blanks+import Blanks.Core (BinderScope (..)) import Blanks.Located as Blanks import Blanks.LocScope as Blanks import Blanks.Name as Blanks import Blanks.Scope as Blanks+import Blanks.Split as Blanks import Blanks.Sub as Blanks+import Blanks.Tracked as Blanks

@@ -0,0 +1,27 @@+module Blanks.Conversion+  ( locScopeForget+  , scopeAnno+  ) where++import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed,+                        pattern LocScopeFree)+import Blanks.Scope (Scope, pattern ScopeBinder, pattern ScopeBound, pattern ScopeEmbed, pattern ScopeFree)++-- | Forget all the annotations and yield a plain 'Scope'.+locScopeForget :: Functor f => LocScope l n f a -> Scope n f a+locScopeForget ls =+  case ls of+    LocScopeBound _ b -> ScopeBound b+    LocScopeFree _ a -> ScopeFree a+    LocScopeBinder _ r x e -> ScopeBinder r x (locScopeForget e)+    LocScopeEmbed _ fe -> ScopeEmbed (fmap locScopeForget fe)++-- | Annotate every location in the 'Scope' with a given value as a 'LocScope'.+scopeAnno :: Functor f => l -> Scope n f a -> LocScope l n f a+scopeAnno l = go where+  go s =+    case s of+      ScopeBound b -> LocScopeBound l b+      ScopeFree a -> LocScopeFree l a+      ScopeBinder r x e -> LocScopeBinder l r x (go e)+      ScopeEmbed fe -> LocScopeEmbed l (fmap go fe)

@@ -0,0 +1,40 @@+{-# LANGUAGE DeriveAnyClass #-}++-- | Internals.+module Blanks.Core+  ( BoundScope (..)+  , FreeScope (..)+  , BinderScope (..)+  , EmbedScope (..)+  ) where++import Control.DeepSeq (NFData)+import GHC.Generics (Generic)++newtype BoundScope =+  BoundScope+    { unBoundScope :: Int+    }+  deriving newtype (Eq, Show, NFData)++newtype FreeScope a =+  FreeScope+    { unFreeScope :: a+    }+  deriving stock (Eq, Show, Functor, Foldable, Traversable)+  deriving newtype (NFData)++data BinderScope n e =+  BinderScope+    { binderScopeArity :: !Int+    , binderScopeInfo :: !n+    , binderScopeBody :: e+    }+  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)+  deriving anyclass (NFData)++newtype EmbedScope f e =+  EmbedScope+    { unEmbedScope :: f e+    }+  deriving newtype (Eq, Show, Functor, NFData)

@@ -1,209 +0,0 @@-module Blanks.Interface-  ( Blank-  , BlankLeft-  , BlankRight-  , BlankInfo-  , BlankFunctor-  , BlankRawFold-  , BlankFold-  , BlankPair-  , blankFree-  , blankEmbed-  , blankAbstract-  , blankAbstract1-  , blankUnAbstract-  , blankUnAbstract1-  , blankInstantiate-  , blankInstantiate1-  , blankApply-  , blankApply1-  , blankApplyThrow-  , blankApply1Throw-  , blankBind-  , blankBindOpt-  , blankLift-  , blankRawFold-  , blankFold-  , blankLiftAnno-  , blankHoistAnno-  , blankMapAnno-  ) where--import Blanks.NatNewtype (NatNewtype)-import Blanks.ScopeW-import Blanks.Sub (SubError, ThrowSub, rethrowSub)-import Blanks.UnderScope (UnderScopeFold)-import Data.Functor.Adjunction (Adjunction)-import Data.Kind (Type)-import Data.Sequence (Seq)-import qualified Data.Sequence as Seq---- | The left adjoint functor used by 'g'.-type family BlankLeft (g :: Type -> Type) :: Type -> Type---- | The right adjoint functor used by 'g'-type family BlankRight (g :: Type -> Type) :: Type -> Type---- | The binder info used by 'g'.-type family BlankInfo (g :: Type -> Type) :: Type---- | The expression functor used by 'g'.-type family BlankFunctor (g :: Type -> Type) :: Type -> Type--type BlankRawFold (g :: Type -> Type) (a :: Type) (r :: Type) = UnderScopeFold (BlankInfo g) (BlankFunctor g) (g a) a r-type BlankFold (g :: Type -> Type) (a :: Type) (r :: Type) = BlankRawFold g a (BlankRight g r)---- | Indicates that 'g' is a "scope" functor we can use for name-binding. (Behind-the-scenes, 'g' must--- be a newtype wrapper over the 'ScopeW' datatype.) Most of the time you will use 'Scope' or 'LocScope'--- directly, which are instances of this class.------ We use the pair of adjoint functors indexed by 'g' to shift the burden of operating in context--- where it is more convenient. For example, 'LocScope' uses a pair of functors that are--- essentially 'Env' and 'Reader'. The left adjoint 'Env' lets us annotate every level of our--- expression tree with a location, and the right adjoint 'Reader' informs us of that location--- so we don't have to make one up out of thin air!------ 'Scope' uses the pair of functors 'Identity' and 'Identity', which means there is--- no ability to store any additional information in the tree, but there's also no additional--- burden to provide that information.-class-  ( Adjunction (BlankLeft g) (BlankRight g)-  , Applicative (BlankRight g)-  , Functor (BlankFunctor g)-  , NatNewtype (ScopeW (BlankLeft g) (BlankInfo g) (BlankFunctor g) g) g-  ) => Blank (g :: Type -> Type)---- | A pair of 'Blank' functors that index the same info and embedded functors. Used to change adjoint functors.-type BlankPair g h = (Blank g, Blank h, BlankInfo g ~ BlankInfo h, BlankFunctor g ~ BlankFunctor h)---- | Creates a free variable in context.-blankFree ::-  Blank g-  => a -- ^ The name of the free variable-  -> BlankRight g (g a)-blankFree = scopeWFree-{-# INLINE blankFree #-}---- | Embeds an expression functor in context.-blankEmbed ::-  Blank g-  => BlankFunctor g (g a) -- ^ An expression-  -> BlankRight g (g a)-blankEmbed = scopeWEmbed-{-# INLINE blankEmbed #-}---- | Binds free variables in an expression and returns a binder.-blankAbstract ::-  (Blank g, Eq a)-  => BlankInfo g -- ^ Annotation specific to your expression functor.-                 -- Might contain original variable names and types, or might-                 -- mark this as a "let" vs a "lambda".-  -> Seq a -- ^ Free variables to bind, like the names of function parameters-  -> g a -- ^ The expression to bind in, like the body of a function-  -> BlankRight g (g a)-blankAbstract = scopeWAbstract-{-# INLINE blankAbstract #-}---- | 'blankAbstract' for a single argument.-blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a)-blankAbstract1 n k = scopeWAbstract n (Seq.singleton k)-{-# INLINE blankAbstract1 #-}---- | Un-bind free variables in an expression. Basically the inverse of--- 'blankAbstract'. Take care to match the arity of the binder! ('blankApply' is safer.)-blankUnAbstract ::-  Blank g-  => Seq a -- ^ The names of the variables you're freeing-  -> g a -- ^ The expression to substitutue in (typically a binder)-  -> g a-blankUnAbstract = scopeWUnAbstract-{-# INLINE blankUnAbstract #-}---- 'blankUnAbstract' for a single argument.-blankUnAbstract1 :: Blank g => a -> g a -> g a-blankUnAbstract1 = scopeWUnAbstract . Seq.singleton-{-# INLINE blankUnAbstract1 #-}---- | Instantiate the bound variables in an expression with other expressions.--- Take care to match the arity of the binder! ('blankApply' is safer.)-blankInstantiate ::-  Blank g-  => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars-  -> g a -- ^ The expression to substitute in (typically a binder)-  -> g a-blankInstantiate = scopeWInstantiate-{-# INLINE blankInstantiate #-}---- | 'blankInstantiate' for a single argument.-blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a-blankInstantiate1 = scopeWInstantiate . Seq.singleton-{-# INLINE blankInstantiate1 #-}---- | Instantiates the bound variables in an expression with other expressions.--- Throws errors on mismatched arity, non binder expression, unbound vars, etc.--- A version of 'blankInstantiate' that fails loudly instead of silently!-blankApply ::-  Blank g-  => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars-  -> g a -- ^ The binder expression to substitute in-  -> Either SubError (g a)-blankApply = scopeWApply-{-# INLINE blankApply #-}---- | 'blankApply' for a single argument.-blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a)-blankApply1 = scopeWApply . Seq.singleton-{-# INLINE blankApply1 #-}---- | A 'ThrowSub' version of 'blankApply'.-blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a)-blankApplyThrow ks = rethrowSub . scopeWApply ks-{-# INLINE blankApplyThrow #-}---- | A 'ThrowSub' version of 'blankApply1'.-blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a)-blankApply1Throw k = rethrowSub . scopeWApply (Seq.singleton k)-{-# INLINE blankApply1Throw #-}---- | Substitution as a kind of monadic bind.-blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b-blankBind = scopeWBind-{-# INLINE blankBind #-}---- | Optional substitution as another kind of monadic bind.-blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a-blankBindOpt = scopeWBindOpt-{-# INLINE blankBindOpt #-}---- | Lift an expression functor into the scope functor.-blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a)-blankLift = scopeWLift-{-# INLINE blankLift #-}---- | Pattern match all cases of the scope functor.-blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r-blankRawFold = scopeWRawFold-{-# INLINE blankRawFold #-}---- | Pattern match all cases of the scope functor, and eliminate the adjoints.-blankFold :: Blank g => BlankFold g a r -> g a -> r-blankFold = scopeWFold-{-# INLINE blankFold #-}---- | Lift a value of your left adjoint functor (annotating the tree) into your--- scope functor.-blankLiftAnno :: Blank g => BlankLeft g a -> g a-blankLiftAnno = scopeWLiftAnno-{-# INLINE blankLiftAnno #-}---- | Apply a natural transformation to your left adjoint functor (annotating the tree) to--- change scope functors.-blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a-blankHoistAnno = scopeWHoistAnno-{-# INLINE blankHoistAnno #-}---- | Apply a function to the free variables in scope in the context of the left adjoint functor.--- (Allows you to read annotations when fmapping.)-blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b-blankMapAnno = scopeWMapAnno-{-# INLINE blankMapAnno #-}

@@ -7,34 +7,46 @@   , pattern LocScopeBinder   , pattern LocScopeEmbed   , locScopeLocation-  , locScopeForget+  , locScopeFree+  , locScopeEmbed+  , locScopeFromInnerBinder+  , locScopeBind+  , locScopeBindOpt+  , locScopeLift+  , locScopeInnerBinder+  , locScopeInnerBinder1+  , locScopeAbstract+  , locScopeAbstract1+  , locScopeUnAbstract+  , locScopeUnAbstract1+  , locScopeInstantiate+  , locScopeInstantiate1+  , locScopeApply+  , locScopeApply1+  , locScopeLiftAnno+  , locScopeHoistAnno+  , locScopeMapAnno   ) where -import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankHoistAnno, blankMapAnno)+import Blanks.Core (BinderScope) import Blanks.Located (Colocated, Located (..), askColocated) import Blanks.NatNewtype (NatNewtype)-import Blanks.Scope (Scope (..))-import Blanks.ScopeW (ScopeW (..))-import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,-                          pattern UnderScopeFree)+import Blanks.ScopeW (ScopeW (..), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind,+                      scopeWBindOpt, scopeWEmbed, scopeWFree, scopeWFromInnerBinder, scopeWHoistAnno, scopeWInnerBinder,+                      scopeWInnerBinder1, scopeWInstantiate, scopeWInstantiate1, scopeWLift, scopeWLiftAnno,+                      scopeWMapAnno, scopeWUnAbstract, scopeWUnAbstract1)+import Blanks.Sub (SubError)+import Blanks.Under (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, pattern UnderScopeFree) import Control.DeepSeq (NFData (..)) import Control.Monad (ap)-import Control.Monad.Identity (Identity (..)) import Control.Monad.Writer (MonadWriter (..))+import Data.Sequence (Seq)  -- | A 'Scope' annotated with some information between constructors.--- See 'Blank' for usage, and see the patterns in this module for easy manipulation--- and inspection. newtype LocScope l n f a = LocScope   { unLocScope :: ScopeW (Located l) n f (LocScope l n f) a   } deriving stock (Functor, Foldable, Traversable) -type instance BlankLeft (LocScope l n f) = Located l-type instance BlankRight (LocScope l n f) = Colocated l-type instance BlankInfo (LocScope l n f) = n-type instance BlankFunctor (LocScope l n f) = f--instance Functor f => Blank (LocScope l n f) instance NatNewtype (ScopeW (Located l) n f (LocScope l n f)) (LocScope l n f)  instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n f a))) => NFData (LocScope l n f a) where@@ -69,14 +81,14 @@  instance (Monoid l, Functor f) => Monad (LocScope l n f) where   return = pure-  s >>= f = blankBind go s where+  s >>= f = locScopeBind go s where     go a = fmap (\l1 -> let LocScope (ScopeW (Located l2 b)) = f a in LocScope (ScopeW (Located (l1 <> l2) b))) askColocated  instance (Monoid l, Functor f) => MonadWriter l (LocScope l n f) where   writer (a, l) = LocScopeFree l a   tell l = LocScopeFree l ()-  listen = blankMapAnno (\(Located l a) -> Located l (a, l))-  pass = blankMapAnno (\(Located l (a, f)) -> Located (f l) a)+  listen = locScopeMapAnno (\(Located l a) -> Located l (a, l))+  pass = locScopeMapAnno (\(Located l (a, f)) -> Located (f l) a)  instance (Eq (f (LocScope l n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where   LocScope su == LocScope sv = su == sv@@ -84,6 +96,84 @@ instance (Show (f (LocScope l n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where   showsPrec d (LocScope (ScopeW tu)) = showString "LocScope " . showsPrec (d+1) tu --- | Forget all the annotations and yield a plain 'Scope'.-locScopeForget :: Functor f => LocScope l n f a -> Scope n f a-locScopeForget = blankHoistAnno (\(Located _ a) -> Identity a)+-- * Interface++locScopeFree :: Functor f => a -> Colocated l (LocScope l n f a)+locScopeFree = scopeWFree+{-# INLINE locScopeFree #-}++locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a)+locScopeEmbed = scopeWEmbed+{-# INLINE locScopeEmbed #-}++locScopeFromInnerBinder :: Functor f => BinderScope n (LocScope l n f a) -> Colocated l (LocScope l n f a)+locScopeFromInnerBinder = scopeWFromInnerBinder+{-# INLINE locScopeFromInnerBinder #-}++locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b+locScopeBind = scopeWBind+{-# INLINE locScopeBind #-}++locScopeBindOpt :: Functor f => (a -> Maybe (Colocated l (LocScope l n f a))) -> LocScope l n f a -> LocScope l n f a+locScopeBindOpt = scopeWBindOpt+{-# INLINE locScopeBindOpt #-}++locScopeLift :: Traversable f => f a -> Colocated l (LocScope l n f a)+locScopeLift = scopeWLift+{-# INLINE locScopeLift #-}++locScopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> BinderScope n (LocScope l n f a)+locScopeInnerBinder = scopeWInnerBinder+{-# INLINE locScopeInnerBinder #-}++locScopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> BinderScope n (LocScope l n f a)+locScopeInnerBinder1 = scopeWInnerBinder1+{-# INLINE locScopeInnerBinder1 #-}++locScopeAbstract :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> Colocated l (LocScope l n f a)+locScopeAbstract = scopeWAbstract+{-# INLINE locScopeAbstract #-}++locScopeAbstract1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> Colocated l (LocScope l n f a)+locScopeAbstract1 = scopeWAbstract1+{-# INLINE locScopeAbstract1 #-}++locScopeUnAbstract :: Functor f => Seq a -> LocScope l n f a -> LocScope l n f a+locScopeUnAbstract = scopeWUnAbstract+{-# INLINE locScopeUnAbstract #-}++locScopeUnAbstract1 :: Functor f => a -> LocScope l n f a -> LocScope l n f a+locScopeUnAbstract1 = scopeWUnAbstract1+{-# INLINE locScopeUnAbstract1 #-}++locScopeInstantiate :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> LocScope l n f a+locScopeInstantiate = scopeWInstantiate+{-# INLINE locScopeInstantiate #-}++locScopeInstantiate1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> LocScope l n f a+locScopeInstantiate1 = scopeWInstantiate1+{-# INLINE locScopeInstantiate1 #-}++locScopeApply :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> Either SubError (LocScope l n f a)+locScopeApply = scopeWApply+{-# INLINE locScopeApply #-}++locScopeApply1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> Either SubError (LocScope l n f a)+locScopeApply1 = scopeWApply1+{-# INLINE locScopeApply1 #-}++locScopeLiftAnno :: Located l a -> LocScope l n f a+locScopeLiftAnno = scopeWLiftAnno+{-# INLINE locScopeLiftAnno #-}++-- Need an explicit type sig and forall to use this in the hoist below+mapLocatedForall :: (l -> x) -> (forall z. Located l z -> Located x z)+mapLocatedForall f (Located l z) = Located (f l) z++locScopeHoistAnno :: Functor f => (l -> x) -> LocScope l n f a -> LocScope x n f a+locScopeHoistAnno f = scopeWHoistAnno (mapLocatedForall f)+{-# INLINE locScopeHoistAnno #-}++locScopeMapAnno :: Functor f => (Located l a -> Located l b) -> LocScope l n f a -> LocScope l n f b+locScopeMapAnno = scopeWMapAnno+{-# INLINE locScopeMapAnno #-}

@@ -22,8 +22,8 @@ -- It's also basically the 'Writer' monad in certain contexts. -- We define a new, non-transforming datatype so we can pattern-match. data Located l a = Located-  { _locatedLoc :: !l-  , _locatedVal :: a+  { locatedLoc :: !l+  , locatedVal :: a   } deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)     deriving anyclass (NFData) 

@@ -14,8 +14,8 @@ -- terms structurally ('Eq') equivalent. data Name n a =   Name-    { _nameKey :: !n-    , _nameValue :: !a+    { nameKey :: !n+    , nameValue :: !a     }   deriving stock (Show, Functor, Foldable, Traversable, Generic)   deriving anyclass (NFData)

@@ -6,30 +6,41 @@   , pattern ScopeFree   , pattern ScopeBinder   , pattern ScopeEmbed+  , scopeWFromInnerBinder+  , scopeBind+  , scopeBindOpt+  , scopeLift+  , scopeInnerBinder+  , scopeInnerBinder1+  , scopeAbstract+  , scopeAbstract1+  , scopeUnAbstract+  , scopeUnAbstract1+  , scopeInstantiate+  , scopeInstantiate1+  , scopeApply+  , scopeApply1   ) where -import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankFree)+import Blanks.Core (BinderScope) import Blanks.NatNewtype (NatNewtype)-import Blanks.ScopeW (ScopeW (..))-import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,-                          pattern UnderScopeFree)+import Blanks.ScopeW (ScopeW (ScopeW), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind,+                      scopeWBindOpt, scopeWFromInnerBinder, scopeWInnerBinder, scopeWInnerBinder1, scopeWInstantiate,+                      scopeWInstantiate1, scopeWLift, scopeWUnAbstract, scopeWUnAbstract1)+import Blanks.Sub (SubError)+import Blanks.Under (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, pattern UnderScopeFree) import Control.DeepSeq (NFData (..)) import Control.Monad (ap) import Control.Monad.Identity (Identity (..))+import Data.Sequence (Seq)  -- | A simple wrapper for your expression functor that knows how to name-bind.--- See 'Blank' for usage, and see the patterns in this module for easy manipulation--- and inspection.+-- Create free variables is 'pure', bind them with '>>=', and list free variables with folds.+-- See 'LocScope' for a version with additional annotations between layers. newtype Scope n f a = Scope   { unScope :: ScopeW Identity n f (Scope n f) a   } deriving stock (Functor, Foldable, Traversable) -type instance BlankLeft (Scope n f) = Identity-type instance BlankRight (Scope n f) = Identity-type instance BlankInfo (Scope n f) = n-type instance BlankFunctor (Scope n f) = f--instance Functor f => Blank (Scope n f) instance NatNewtype (ScopeW Identity n f (Scope n f)) (Scope n f)  instance (NFData n, NFData a, NFData (f (Scope n f a))) => NFData (Scope n f a) where@@ -50,15 +61,116 @@ {-# COMPLETE ScopeBound, ScopeFree, ScopeBinder, ScopeEmbed #-}  instance Functor f => Applicative (Scope n f) where-  pure = runIdentity . blankFree+  pure = ScopeFree   (<*>) = ap  instance Functor f => Monad (Scope n f) where   return = pure-  s >>= f = blankBind (Identity . f) s+  s >>= f = scopeBind f s  instance (Eq (f (Scope n f a)), Eq n, Eq a) => Eq (Scope n f a) where   Scope su == Scope sv = su == sv  instance (Show (f (Scope n f a)), Show n, Show a) => Show (Scope n f a) where   showsPrec d (Scope (ScopeW tu)) = showString "Scope " . showsPrec (d+1) tu++-- * Interface++scopeFromInnerBinder :: Functor f => BinderScope n (Scope n f a) -> Scope n f a+scopeFromInnerBinder = runIdentity . scopeWFromInnerBinder+{-# INLINE scopeFromInnerBinder #-}++-- | Substitution as a kind of monadic bind.+scopeBind :: Functor f => (a -> Scope n f b) -> Scope n f a -> Scope n f b+scopeBind f = scopeWBind (Identity . f)+{-# INLINE scopeBind #-}++-- | Optional substitution as another kind of monadic bind.+scopeBindOpt :: Functor f => (a -> Maybe (Scope n f a)) -> Scope n f a -> Scope n f a+scopeBindOpt f = scopeWBindOpt (fmap Identity . f)+{-# INLINE scopeBindOpt #-}++-- | Lift an expression functor into the scope functor.+scopeLift :: Traversable f => f a -> Scope n f a+scopeLift = runIdentity . scopeWLift+{-# INLINE scopeLift #-}++scopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> Scope n f a -> BinderScope n (Scope n f a)+scopeInnerBinder = scopeWInnerBinder+{-# INLINE scopeInnerBinder #-}++scopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> BinderScope n (Scope n f a)+scopeInnerBinder1 = scopeWInnerBinder1+{-# INLINE scopeInnerBinder1 #-}++-- | Binds free variables in an expression and returns a binder.+scopeAbstract+  :: (Functor f, Eq a)+  => n+  -- ^ Annotation specific to your expression functor.+  -- Might contain original variable names and types, or might+  -- mark this as a "let" vs a "lambda"+  -> Seq a+  -- ^ Free variables to bind, like the names of function parameters+  -> Scope n f a+  -- ^ The expression to bind in, like the body of a function+  -> Scope n f a+scopeAbstract n ks = runIdentity . scopeWAbstract n ks+{-# INLINE scopeAbstract #-}++-- | 'scopeAbstract' for a single argument.+scopeAbstract1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> Scope n f a+scopeAbstract1 n k = runIdentity . scopeWAbstract1 n k+{-# INLINE scopeAbstract1 #-}++-- | Un-bind free variables in an expression. Basically the inverse of+-- 'scopeAbstract'. Take care to match the arity of the binder! ('scopeApply' is safer.)+scopeUnAbstract+  :: Functor f+  => Seq a+  -- ^ The names of the variables you're freeing+  -> Scope n f a+   -- ^ The expression to substitute in (typically a binder)+  -> Scope n f a+scopeUnAbstract = scopeWUnAbstract+{-# INLINE scopeUnAbstract #-}++-- 'scopeUnAbstract' for a single argument.+scopeUnAbstract1 :: Functor f => a -> Scope n f a -> Scope n f a+scopeUnAbstract1 = scopeWUnAbstract1+{-# INLINE scopeUnAbstract1 #-}++-- | Instantiate the bound variables in an expression with other expressions.+-- Take care to match the arity of the binder! ('scopeApply' is safer.)+scopeInstantiate+  :: Functor f+  => Seq (Scope n f a)+  -- ^ Expressions to substitute in place of bound vars+  -> Scope n f a+  -- ^ The expression to substitute in (typically a binder)+  -> Scope n f a+scopeInstantiate vs = scopeWInstantiate (fmap Identity vs)+{-# INLINE scopeInstantiate #-}++-- | 'scopeInstantiate' for a single argument.+scopeInstantiate1 :: Functor f => Scope n f a -> Scope n f a -> Scope n f a+scopeInstantiate1 v = scopeWInstantiate1 (Identity v)+{-# INLINE scopeInstantiate1 #-}++-- | Instantiates the bound variables in an expression with other expressions.+-- Throws errors on mismatched arity, non binder expression, unbound vars, etc.+-- A version of 'scopeInstantiate' that fails loudly instead of silently!+scopeApply+  :: Functor f+  => Seq (Scope n f a)+  -- ^ Expressions to substitute in place of bound vars+  -> Scope n f a+  -- ^ The binder expression to substitute in+  -> Either SubError (Scope n f a)+scopeApply vs = scopeWApply (fmap Identity vs)+{-# INLINE scopeApply #-}++-- | 'scopeApply' for a single argument.+scopeApply1 :: Functor f => Scope n f a -> Scope n f a -> Either SubError (Scope n f a)+scopeApply1 v = scopeWApply1 (Identity v)+{-# INLINE scopeApply1 #-}

@@ -1,31 +1,35 @@ {-# LANGUAGE UndecidableInstances #-} --- | Internals. You'd need to newtype 'ScopeW' to implement your own 'Blank'.+-- | Internals. module Blanks.ScopeW-  ( ScopeC+  ( ScopeWC   , ScopeW (..)-  , ScopeWRawFold-  , ScopeWFold   , scopeWFree   , scopeWEmbed+  , scopeWFromInnerBinder+  , scopeWInnerBinder+  , scopeWInnerBinder1   , scopeWAbstract+  , scopeWAbstract1   , scopeWUnAbstract+  , scopeWUnAbstract1   , scopeWInstantiate+  , scopeWInstantiate1   , scopeWApply+  , scopeWApply1   , scopeWBind   , scopeWBindOpt   , scopeWLift-  , scopeWRawFold-  , scopeWFold   , scopeWLiftAnno   , scopeWHoistAnno   , scopeWMapAnno   ) where +import Blanks.Core (BinderScope (..)) import Blanks.NatNewtype (NatNewtype, natNewtypeFrom, natNewtypeTo) import Blanks.Sub (SubError (..))-import Blanks.UnderScope (UnderScope, pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,-                          UnderScopeFold, pattern UnderScopeFree, underScopeFold, underScopeShift)+import Blanks.Under (UnderScope (..), pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,+                     pattern UnderScopeFree, underScopeShift) import Control.DeepSeq (NFData (..)) import Data.Bifoldable (bifoldr) import Data.Bifunctor (bimap, first)@@ -37,11 +41,16 @@  -- * ScopeW, patterns, and instances +-- | The core internal scope type. (The "w" comes from "wrapper".)+-- We wrap up an 'UnderScope' in some functor and demand that we+-- unwrap it in an adjoint context. In the first case, these functors will be+-- 'Identity', yielding the 'Scope' newtype. In the second case, these+-- functors will be 'Located' and 'Colocated', yielding the 'LocScope' newtype. newtype ScopeW t n f g a = ScopeW   { unScopeW :: t (UnderScope n f (g a) a)   } -instance NFData (t (UnderScope n f (g a) a) )=> NFData (ScopeW t n f g a) where+instance NFData (t (UnderScope n f (g a) a)) => NFData (ScopeW t n f g a) where   rnf (ScopeW tu) = seq (rnf tu) ()  instance Eq (t (UnderScope n f (g a) a)) => Eq (ScopeW t n f g a) where@@ -59,43 +68,51 @@ instance (Traversable t, Traversable f, Traversable g) => Traversable (ScopeW t n f g) where   traverse f (ScopeW tu) = fmap ScopeW (traverse (bitraverse (traverse f) f) tu) -type ScopeC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g)+type ScopeWC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g)  -- * Smart constructors, shift, and bind -scopeWMod :: ScopeC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x+scopeWMod :: ScopeWC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x scopeWMod f = rightAdjunct f . unScopeW . natNewtypeFrom+{-# INLINE scopeWMod #-} -scopeWModOpt :: ScopeC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a+scopeWModOpt :: ScopeWC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a scopeWModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeW (natNewtypeFrom s))+{-# INLINE scopeWModOpt #-} -scopeWModM :: (ScopeC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x+scopeWModM :: (ScopeWC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x scopeWModM f = rightAdjunct (sequenceA . f) . unScopeW . natNewtypeFrom+{-# INLINE scopeWModM #-} -scopeWBound :: ScopeC t u n f g => Int -> u (g a)+scopeWBound :: ScopeWC t u n f g => Int -> u (g a) scopeWBound b = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBound b)) -scopeWFree :: ScopeC t u n f g => a -> u (g a)+scopeWFree :: ScopeWC t u n f g => a -> u (g a) scopeWFree a = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeFree a)) -scopeWShift :: ScopeC t u n f g => Int -> g a -> g a+scopeWShift :: ScopeWC t u n f g => Int -> g a -> g a scopeWShift = scopeWShiftN 0+{-# INLINE scopeWShift #-} -scopeWShiftN :: ScopeC t u n f g => Int -> Int -> g a -> g a+scopeWShiftN :: ScopeWC t u n f g => Int -> Int -> g a -> g a scopeWShiftN c d e =   let ScopeW tu = natNewtypeFrom e   in natNewtypeTo (ScopeW (fmap (underScopeShift scopeWShiftN c d) tu)) -scopeWBinder :: ScopeC t u n f g => Int -> n -> g a -> u (g a)+scopeWBinder :: ScopeWC t u n f g => Int -> n -> g a -> u (g a) scopeWBinder r n e = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBinder r n e)) -scopeWEmbed :: ScopeC t u n f g => f (g a) -> u (g a)+scopeWFromInnerBinder :: ScopeWC t u n f g => BinderScope n (g a) -> u (g a)+scopeWFromInnerBinder b = fmap (natNewtypeTo . ScopeW) (unit (UnderBinderScope b))++scopeWEmbed :: ScopeWC t u n f g => f (g a) -> u (g a) scopeWEmbed fe = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeEmbed fe)) -scopeWBind :: ScopeC t u n f g => (a -> u (g b)) -> g a -> g b+scopeWBind :: ScopeWC t u n f g => (a -> u (g b)) -> g a -> g b scopeWBind f = scopeWBindN f 0+{-# INLINE scopeWBind #-} -scopeWBindN :: ScopeC t u n f g => (a -> u (g b)) -> Int -> g a -> g b+scopeWBindN :: ScopeWC t u n f g => (a -> u (g b)) -> Int -> g a -> g b scopeWBindN f = scopeWMod . go where   go i us =     case us of@@ -104,10 +121,11 @@       UnderScopeBinder r x e -> scopeWBinder r x (scopeWBindN f (i + r) e)       UnderScopeEmbed fe -> scopeWEmbed (fmap (scopeWBindN f i) fe) -scopeWBindOpt :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a+scopeWBindOpt :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a scopeWBindOpt f = scopeWBindOptN f 0+{-# INLINE scopeWBindOpt #-} -scopeWBindOptN :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a+scopeWBindOptN :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a scopeWBindOptN f = scopeWModOpt . go where   go i us =     case us of@@ -116,29 +134,48 @@       UnderScopeBinder r x e -> Just (scopeWBinder r x (scopeWBindOptN f (i + r) e))       UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWBindOptN f i) fe)) -scopeWLift :: (ScopeC t u n f g, Monad u, Traversable f) => f a -> u (g a)+scopeWLift :: (ScopeWC t u n f g, Monad u, Traversable f) => f a -> u (g a) scopeWLift fa = traverse scopeWFree fa >>= scopeWEmbed  -- * Abstraction -subScopeWAbstract :: (ScopeC t u n f g, Eq a) => Int -> n -> Seq a -> g a -> u (g a)-subScopeWAbstract r n ks e =-  let f = fmap scopeWBound . flip Seq.elemIndexL ks-      e' = scopeWBindOpt f e-  in scopeWBinder r n e'--scopeWAbstract :: (ScopeC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a)-scopeWAbstract n ks =+scopeWInnerBinder :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> BinderScope n (g a)+scopeWInnerBinder n ks e =   let r = Seq.length ks-  in subScopeWAbstract r n ks . scopeWShift r+      e' = scopeWShift r e+      f = fmap scopeWBound . flip Seq.elemIndexL ks+      e'' = scopeWBindOpt f e'+  in BinderScope r n e'' -scopeWUnAbstract :: ScopeC t u n f g => Seq a -> g a -> g a+scopeWInnerBinder1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> BinderScope n (g a)+scopeWInnerBinder1 n = scopeWInnerBinder n . Seq.singleton+{-# INLINE scopeWInnerBinder1 #-}++scopeWAbstract :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a)+scopeWAbstract n ks e = scopeWFromInnerBinder (scopeWInnerBinder n ks e)+{-# INLINE scopeWAbstract #-}++scopeWAbstract1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> u (g a)+scopeWAbstract1 n = scopeWAbstract n . Seq.singleton+{-# INLINE scopeWAbstract1 #-}++scopeWUnAbstract :: ScopeWC t u n f g => Seq a -> g a -> g a scopeWUnAbstract ks = scopeWInstantiate (fmap scopeWFree ks)+{-# INLINE scopeWUnAbstract #-} -scopeWInstantiate :: ScopeC t u n f g => Seq (u (g a)) -> g a -> g a+scopeWUnAbstract1 :: ScopeWC t u n f g => a -> g a -> g a+scopeWUnAbstract1 = scopeWUnAbstract . Seq.singleton+{-# INLINE scopeWUnAbstract1 #-}++scopeWInstantiate :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> g a scopeWInstantiate = scopeWInstantiateN 0+{-# INLINE scopeWInstantiate #-} -scopeWInstantiateN :: ScopeC t u n f g => Int -> Seq (u (g a)) -> g a -> g a+scopeWInstantiate1 :: ScopeWC t u n f g => u (g a) -> g a -> g a+scopeWInstantiate1 = scopeWInstantiate . Seq.singleton+{-# INLINE scopeWInstantiate1 #-}++scopeWInstantiateN :: ScopeWC t u n f g => Int -> Seq (u (g a)) -> g a -> g a scopeWInstantiateN h vs = scopeWModOpt (go h) where   go i us =     case us of@@ -150,7 +187,7 @@         in Just (scopeWBinder r n e')       UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWInstantiateN i vs) fe)) -scopeWApply :: ScopeC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a)+scopeWApply :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a) scopeWApply vs = scopeWModM go where   go us =     case us of@@ -161,16 +198,9 @@               else Left (ApplyError len r)       _ -> Left NonBinderError --- * Folds--type ScopeWRawFold n f g a r = UnderScopeFold n f (g a) a r-type ScopeWFold u n f g a r = ScopeWRawFold n f g a (u r)--scopeWRawFold :: (NatNewtype (ScopeW t n f g) g, Functor t) => ScopeWRawFold n f g a r -> g a -> t r-scopeWRawFold usf = fmap (underScopeFold usf) . unScopeW . natNewtypeFrom--scopeWFold :: (NatNewtype (ScopeW t n f g) g, Adjunction t u) => ScopeWFold u n f g a r -> g a -> r-scopeWFold usf = counit . scopeWRawFold usf+scopeWApply1 :: ScopeWC t u n f g => u (g a) -> g a -> Either SubError (g a)+scopeWApply1 = scopeWApply . Seq.singleton+{-# INLINE scopeWApply1 #-}  -- * Annotation functions @@ -183,7 +213,7 @@       s = ScopeW (nat (fmap (first (scopeWHoistAnno nat)) tu))   in natNewtypeTo s -scopeWMapAnno :: ScopeC t u n f g => (t a -> t b) -> g a -> g b+scopeWMapAnno :: ScopeWC t u n f g => (t a -> t b) -> g a -> g b scopeWMapAnno f = scopeWMod go where   go us = case us of     UnderScopeBound b -> scopeWBound b

@@ -0,0 +1,107 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE UndecidableInstances #-}++module Blanks.Split+  ( BinderId (..)+  , SplitFunctor (..)+  , SplitBinder (..)+  , SplitResult (..)+  , splitLocScope+  ) where++import Blanks.Core (BinderScope (..))+import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed,+                        pattern LocScopeFree)+import Blanks.Tracked (Tracked (..), WithTracked (..), mkTrackedBound, mkTrackedFree)+import Control.DeepSeq (NFData (..))+import Control.Monad.State (State, gets, modify', runState)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import Data.Set (Set)+import qualified Data.Set as Set+import GHC.Generics (Generic)++data Stream x = Stream !x (Stream x)++enumStreamFrom :: Enum e => e -> Stream e+enumStreamFrom e = Stream e (enumStreamFrom (succ e))++enumStream :: Enum e => Stream e+enumStream = enumStreamFrom (toEnum 0)++newtype BinderId = BinderId { unBinderId :: Int }+  deriving stock (Eq, Show, Ord)+  deriving newtype (Enum, NFData, Num)++data SplitFunctor f a =+    SplitFunctorBase !(f a)+  | SplitFunctorClosure !BinderId !(Seq Int)+  deriving stock (Eq, Show, Generic, Functor, Foldable, Traversable)+  deriving anyclass (NFData)++data SplitBinder l n f a = SplitBinder+  { splitBinderClosureArity :: !Int+  , splitBinderFree :: !(Set a)+  , splitBinderScope :: !(BinderScope n (LocScope l n (SplitFunctor f) a))+  } deriving stock (Generic)++instance (Eq l, Eq n, Eq a, Eq (f (LocScope l n (SplitFunctor f) a))) => Eq (SplitBinder l n f a) where+  SplitBinder a1 f1 s1 == SplitBinder a2 f2 s2 = a1 == a2 && f1 == f2 && s1 == s2++instance (Show l, Show n, Show a, Show (f (LocScope l n (SplitFunctor f) a))) => Show (SplitBinder l n f a) where+  showsPrec d (SplitBinder a f s) = showString "SplitBinder " . showsPrec (d+1) a . showChar ' ' . showsPrec (d+1) f . showChar ' ' . showsPrec (d+1) s++instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n (SplitFunctor f) a))) => NFData (SplitBinder l n f a) where+  rnf (SplitBinder a f s) = seq (rnf a) (seq (rnf f) (rnf s))++data SplitState l n f a = SplitState+  { splitStateStream :: !(Stream BinderId)+  , splitStateBinders :: !(Map BinderId (SplitBinder l n f a))+  }++initSplitState :: SplitState l n f a+initSplitState = SplitState enumStream Map.empty++getNextBinderId :: State (SplitState l n f a) BinderId+getNextBinderId = do+  st <- gets splitStateStream+  let Stream hd tl = st+  modify' (\ss -> ss { splitStateStream = tl })+  pure hd++insertBinder :: BinderId -> SplitBinder l n f a -> State (SplitState l n f a) ()+insertBinder bid lb = modify' (\ss -> ss { splitStateBinders = Map.insert bid lb (splitStateBinders ss) })++remapBound :: Int -> Set Int -> Int -> Int+remapBound r bs b = maybe b (+ r) (Set.lookupIndex b bs)++splitLocScopeInner :: (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a)+splitLocScopeInner r bs ls =+  case ls of+    LocScopeBound (WithTracked _ l) b ->+      let !b' = remapBound r bs b+      in pure (mkTrackedBound b', LocScopeBound l b')+    LocScopeFree (WithTracked _ l) a ->+      pure (mkTrackedFree a, LocScopeFree l a)+    LocScopeEmbed (WithTracked _ l) fe -> fmap (\fx -> let (!t, !fe') = sequence fx in (t, LocScopeEmbed l (SplitFunctorBase fe'))) (traverse (splitLocScopeInner r bs) fe)+    LocScopeBinder (WithTracked (Tracked fv bv) l) x n e -> do+      bid <- getNextBinderId+      let bs' = Set.mapMonotonic (+ r) bv+      (_, e') <- splitLocScopeInner x bs' e+      let lb = SplitBinder (Set.size bs') fv (BinderScope x n e')+      insertBinder bid lb+      let ss = Seq.fromList (Set.toList bv)+      pure (Tracked Set.empty bv, LocScopeEmbed l (SplitFunctorClosure bid ss))++data SplitResult l n f a = SplitResult+  { splitResultTracked :: !(Tracked a)+  , splitResultScope :: !(LocScope l n (SplitFunctor f) a)+  , splitResultBinders :: !(Map BinderId (SplitBinder l n f a))+  }++splitLocScope :: (Traversable f, Ord a) => LocScope (WithTracked a l) n f a -> SplitResult l n f a+splitLocScope s =+  let ((!t, !s'), !ss) = runState (splitLocScopeInner 0 Set.empty s) initSplitState+  in SplitResult t s' (splitStateBinders ss)

@@ -0,0 +1,85 @@+{-# LANGUAGE DeriveAnyClass #-}++-- | Utilities for gathering and caching sets of free variables.+module Blanks.Tracked+  ( Tracked (..)+  , mkTrackedFree+  , mkTrackedBound+  , shiftTracked+  , WithTracked (..)+  , forgetTrackedScope+  , trackScope+  , trackScopeSimple+  ) where++import Blanks.Conversion (scopeAnno)+import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed,+                        pattern LocScopeFree, locScopeHoistAnno)+import Blanks.Scope (Scope)+import Control.DeepSeq (NFData)+import Data.Set (Set)+import qualified Data.Set as Set+import GHC.Generics (Generic)++data Tracked a = Tracked+  { trackedFree :: !(Set a)+  , trackedBound :: !(Set Int)+  } deriving stock (Eq, Show, Generic)+    deriving anyclass (NFData)++mkTrackedFree :: a -> Tracked a+mkTrackedFree a = Tracked (Set.singleton a) Set.empty++mkTrackedBound :: Int -> Tracked a+mkTrackedBound b = Tracked Set.empty (Set.singleton b)++shiftTracked :: Int -> Tracked a -> Tracked a+shiftTracked i t@(Tracked f b) =+  if Set.null b+    then t+    else+      let !b' = if Set.findMax b < i then Set.empty else Set.dropWhileAntitone (< 0) (Set.mapMonotonic (\x -> x - i) b)+      in Tracked f b'++instance Ord a => Semigroup (Tracked a) where+  Tracked f1 b1 <> Tracked f2 b2 = Tracked (Set.union f1 f2) (Set.union b1 b2)++instance Ord a => Monoid (Tracked a) where+  mempty = Tracked Set.empty Set.empty+  mappend = (<>)++data WithTracked a l = WithTracked+  { withTrackedState :: !(Tracked a)+  , withTrackedEnv :: !l+  } deriving stock (Eq, Show, Generic, Functor, Foldable, Traversable)+    deriving anyclass (NFData)++forgetTrackedScope :: Functor f => LocScope (WithTracked a l) n f z -> LocScope l n f z+forgetTrackedScope = locScopeHoistAnno withTrackedEnv++trackScopeInner :: (Traversable f, Ord a) => LocScope l n f a -> (Tracked a, LocScope (WithTracked a l) n f a)+trackScopeInner s =+  case s of+    LocScopeBound l b ->+      let !t = Tracked Set.empty (Set.singleton b)+          !m = WithTracked t l+      in (t, LocScopeBound m b)+    LocScopeFree l a ->+      let !t = Tracked (Set.singleton a) Set.empty+          !m = WithTracked t l+      in (t, LocScopeFree m a)+    LocScopeBinder l n i e ->+      let !(t0, y) = trackScopeInner e+          !t = shiftTracked n t0+          !m = WithTracked t l+      in (t, LocScopeBinder m n i y)+    LocScopeEmbed l fe ->+      let (!t, !fy) = traverse trackScopeInner fe+          !m = WithTracked t l+      in (t, LocScopeEmbed m fy)++trackScope :: (Traversable f, Ord a) => LocScope l n f a -> LocScope (WithTracked a l) n f a+trackScope = snd . trackScopeInner++trackScopeSimple :: (Traversable f, Ord a) => Scope n f a -> LocScope (Tracked a) n f a+trackScopeSimple = locScopeHoistAnno withTrackedState . trackScope . scopeAnno ()

@@ -0,0 +1,69 @@+{-# LANGUAGE DeriveAnyClass #-}++-- | Internals.+module Blanks.Under+  ( UnderScope (..)+  , pattern UnderScopeBound+  , pattern UnderScopeFree+  , pattern UnderScopeBinder+  , pattern UnderScopeEmbed+  , underScopeShift+  ) where++import Blanks.Core (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..))+import Control.DeepSeq (NFData)+import Data.Bifoldable (Bifoldable (..))+import Data.Bifunctor (Bifunctor (..))+import Data.Bitraversable (Bitraversable (..))+import GHC.Generics (Generic)++data UnderScope n f e a+  = UnderBoundScope !BoundScope+  | UnderFreeScope !(FreeScope a)+  | UnderBinderScope !(BinderScope n e)+  | UnderEmbedScope !(EmbedScope f e)+  deriving stock (Eq, Show, Functor, Generic)+  deriving anyclass (NFData)++pattern UnderScopeBound :: Int -> UnderScope n f e a+pattern UnderScopeBound i = UnderBoundScope (BoundScope i)++pattern UnderScopeFree :: a -> UnderScope n f e a+pattern UnderScopeFree a = UnderFreeScope (FreeScope a)++pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a+pattern UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e)++pattern UnderScopeEmbed :: f e -> UnderScope n f e a+pattern UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe)++{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-}++instance Functor f => Bifunctor (UnderScope n f) where+  bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b)+  bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a))+  bimap f _ (UnderBinderScope (BinderScope i x e)) = UnderBinderScope (BinderScope i x (f e))+  bimap f _ (UnderEmbedScope (EmbedScope fe)) = UnderEmbedScope (EmbedScope (fmap f fe))++instance Foldable f => Bifoldable (UnderScope n f) where+  bifoldr _ _ z (UnderBoundScope _) = z+  bifoldr _ g z (UnderFreeScope (FreeScope a)) = g a z+  bifoldr f _ z (UnderBinderScope (BinderScope _ _ e)) = f e z+  bifoldr f _ z (UnderEmbedScope (EmbedScope fe)) = foldr f z fe++instance Traversable f => Bitraversable (UnderScope n f) where+  bitraverse _ _ (UnderBoundScope (BoundScope b)) = pure (UnderBoundScope (BoundScope b))+  bitraverse _ g (UnderFreeScope (FreeScope a)) = fmap (UnderFreeScope . FreeScope) (g a)+  bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e)+  bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe)++underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a+underScopeShift recShift c d us =+  case us of+    UnderBoundScope (BoundScope b) ->+      if b < c+        then us+        else UnderBoundScope (BoundScope (b + d))+    UnderFreeScope _ -> us+    UnderBinderScope (BinderScope i x e) -> UnderBinderScope (BinderScope i x (recShift (c + i) d e))+    UnderEmbedScope (EmbedScope fe) -> UnderEmbedScope (EmbedScope (fmap (recShift c d) fe))

@@ -1,119 +0,0 @@-{-# LANGUAGE DeriveAnyClass #-}---- | Internals. You will probably never need these.-module Blanks.UnderScope-  ( BinderScope (..)-  , BoundScope (..)-  , EmbedScope (..)-  , FreeScope (..)-  , UnderScope (..)-  , UnderScopeFold (..)-  , pattern UnderScopeBound-  , pattern UnderScopeFree-  , pattern UnderScopeBinder-  , pattern UnderScopeEmbed-  , underScopeFold-  , underScopeShift-  ) where--import Control.DeepSeq (NFData)-import Data.Bifoldable (Bifoldable (..))-import Data.Bifunctor (Bifunctor (..))-import Data.Bitraversable (Bitraversable (..))-import GHC.Generics (Generic)--newtype BoundScope =-  BoundScope-    { unBoundScope :: Int-    }-  deriving newtype (Eq, Show, NFData)--newtype FreeScope a =-  FreeScope-    { unFreeScope :: a-    }-  deriving stock (Eq, Show, Functor, Foldable, Traversable)-  deriving newtype (NFData)--data BinderScope n e =-  BinderScope-    { binderScopeArity :: !Int-    , binderScopeInfo :: !n-    , binderScopeBody :: e-    }-  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)-  deriving anyclass (NFData)--newtype EmbedScope f e =-  EmbedScope-    { unEmbedScope :: f e-    }-  deriving newtype (Eq, Show, Functor, NFData)--data UnderScope n f e a-  = UnderBoundScope !BoundScope-  | UnderFreeScope !(FreeScope a)-  | UnderBinderScope !(BinderScope n e)-  | UnderEmbedScope !(EmbedScope f e)-  deriving stock (Eq, Show, Functor, Generic)-  deriving anyclass (NFData)--pattern UnderScopeBound :: Int -> UnderScope n f e a-pattern UnderScopeBound i = UnderBoundScope (BoundScope i)--pattern UnderScopeFree :: a -> UnderScope n f e a-pattern UnderScopeFree a = UnderFreeScope (FreeScope a)--pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a-pattern UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e)--pattern UnderScopeEmbed :: f e -> UnderScope n f e a-pattern UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe)--{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-}--instance Functor f => Bifunctor (UnderScope n f) where-  bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b)-  bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a))-  bimap f _ (UnderBinderScope (BinderScope i x e)) = UnderBinderScope (BinderScope i x (f e))-  bimap f _ (UnderEmbedScope (EmbedScope fe)) = UnderEmbedScope (EmbedScope (fmap f fe))--instance Foldable f => Bifoldable (UnderScope n f) where-  bifoldr _ _ z (UnderBoundScope _) = z-  bifoldr _ g z (UnderFreeScope (FreeScope a)) = g a z-  bifoldr f _ z (UnderBinderScope (BinderScope _ _ e)) = f e z-  bifoldr f _ z (UnderEmbedScope (EmbedScope fe)) = foldr f z fe--instance Traversable f => Bitraversable (UnderScope n f) where-  bitraverse _ _ (UnderBoundScope (BoundScope b)) = pure (UnderBoundScope (BoundScope b))-  bitraverse _ g (UnderFreeScope (FreeScope a)) = fmap (UnderFreeScope . FreeScope) (g a)-  bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e)-  bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe)--underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a-underScopeShift recShift c d us =-  case us of-    UnderBoundScope (BoundScope b) ->-      if b < c-        then us-        else UnderBoundScope (BoundScope (b + d))-    UnderFreeScope _ -> us-    UnderBinderScope (BinderScope i x e) -> UnderBinderScope (BinderScope i x (recShift (c + i) d e))-    UnderEmbedScope (EmbedScope fe) -> UnderEmbedScope (EmbedScope (fmap (recShift c d) fe))--data UnderScopeFold n f e a r =-  UnderScopeFold-    { usfBound :: BoundScope -> r-    , usfFree :: FreeScope a -> r-    , usfBinder :: BinderScope n e -> r-    , usfEmbed :: EmbedScope f e -> r-    }-  deriving (Functor)--underScopeFold :: UnderScopeFold n f e a r -> UnderScope n f e a -> r-underScopeFold (UnderScopeFold bound free binder embed) us =-  case us of-    UnderBoundScope x -> bound x-    UnderFreeScope x -> free x-    UnderBinderScope x -> binder x-    UnderEmbedScope x -> embed x

@@ -2,9 +2,11 @@   ( main   ) where -import Test.Blanks.LocScopeTest (testLocScope)+import Test.Blanks.ExpTest (testExp) import Test.Blanks.ScopeTest (testScope)+import Test.Blanks.SplitTest (testSplit)+import Test.Blanks.TrackedTest (testTracked) import Test.Tasty (defaultMain, testGroup)  main :: IO ()-main = defaultMain (testGroup "Blanks" [testScope, testLocScope])+main = defaultMain (testGroup "Blanks" [testScope, testTracked, testExp, testSplit])

@@ -0,0 +1,254 @@+{-# LANGUAGE DeriveAnyClass #-}++module Test.Blanks.Exp+  ( Ident (..)+  , CExp (..)+  , cexpLoc+  , CDecl (..)+  , declKeywords+  , expKeywords+  , cexpParser+  , runCExpParser+  , cdeclParser+  , runCDeclParser+  , Exp (..)+  , ExpScope+  , DeclScope+  , ExpLocScope+  , DeclLocScope+  , declLocScopeForget+  , declScopeAnno+  , expToNameless+  , expToNamed+  , declToNameless+  , declToNamed+  ) where++import Blanks (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, pattern LocScopeFree,+               Located (..), NameOnly, pattern NameOnly, Scope, locScopeAbstract1, locScopeForget, locScopeUnAbstract1,+               runColocated, scopeAnno)+import Control.DeepSeq (NFData)+import Control.Monad (when)+import Data.Set (Set)+import qualified Data.Set as Set+import GHC.Generics (Generic)+import Test.Blanks.Parsing++-- A newtype indicating an identifier in our language+newtype Ident = Ident { unIdent :: String } deriving newtype (Eq, Show, Ord, NFData)++-- The type of concrete expressions, labeled with source location+data CExp l =+    CExpBool !l !Bool+  | CExpInt !l !Int+  | CExpApp !l !(CExp l) !(CExp l)+  | CExpAdd !l !(CExp l) !(CExp l)+  | CExpIf !l !(CExp l) !(CExp l) !(CExp l)+  | CExpIsZero !l !(CExp l)+  | CExpVar !l !Ident+  | CExpAbs !l !Ident !(CExp l)+  | CExpAsc !l !(CExp l) !(CExp l)+  | CExpTyInt !l+  | CExpTyBool !l+  | CExpTyFun !l !(CExp l) !(CExp l)+  deriving stock (Eq, Show, Generic)+  deriving anyclass (NFData)++-- Extracts the location from a concrete expression+cexpLoc :: CExp l -> l+cexpLoc ce =+  case ce of+    CExpBool l _ -> l+    CExpInt l _ -> l+    CExpApp l _ _ -> l+    CExpAdd l _ _ -> l+    CExpIf l _ _ _ -> l+    CExpIsZero l _ -> l+    CExpVar l _ -> l+    CExpAbs l _ _ -> l+    CExpAsc l _ _ -> l+    CExpTyInt l -> l+    CExpTyBool l -> l+    CExpTyFun l _ _ -> l++expKeywords :: Set Ident+expKeywords = Set.fromList $ fmap Ident+  [ "#t"+  , "#f"+  , "+"+  , "if"+  , "zero?"+  , ":"+  , "lambda"+  , "int"+  , "bool"+  , "->"+  ]++declKeywords :: Set Ident+declKeywords = Set.fromList $ fmap Ident+  [ "declare"+  , "define"+  ]++nonKeywordParser :: Parser Ident+nonKeywordParser = do+  rawIdent <- identifier+  let ident = Ident rawIdent+  when (Set.member ident expKeywords) (fail ("Parsed exp keyword: " <> rawIdent))+  when (Set.member ident declKeywords) (fail ("Parsed decl keyword: " <> rawIdent))+  pure ident++-- Parses a concrete expression from a string+cexpParser :: Parser (CExp SourceSpan)+cexpParser = result where+  result = branch+    [ trueParser+    , falseParser+    , intParser+    , addParser+    , ifParser+    , isZeroParser+    , absParser+    , appParser+    , ascParser+    , tyBoolParser+    , tyIntParser+    , tyFunParser+    , varParser+    ]++  trueParser = around (const . flip CExpBool True) (symbol "#t")++  falseParser = around (const . flip CExpBool False) (symbol "#f")++  intParser = around CExpInt signed++  addParser = around2 CExpAdd (parens (symbol "+" *> double cexpParser))++  ifParser = around3 CExpIf (parens (symbol "if" *> triple cexpParser))++  isZeroParser = around CExpIsZero (parens (symbol "zero?" *> cexpParser))++  absParser = around2 CExpAbs $ parens $ do+    _ <- symbol "lambda"+    n <- parens nonKeywordParser+    b <- cexpParser+    pure (n, b)++  appParser = around2 CExpApp (parens (double cexpParser))++  ascParser = around2 CExpAsc (parens (symbol ":" *> double cexpParser))++  tyBoolParser = around (const . CExpTyBool) (symbol "bool")++  tyIntParser = around (const . CExpTyInt) (symbol "int")++  tyFunParser = around2 (CExpTyFun) (parens (symbol "->" *> double cexpParser))++  varParser = around CExpVar nonKeywordParser++runCExpParser :: String -> IO (CExp SourceSpan)+runCExpParser = runParserIO cexpParser++data Level =+    LevelTerm+  | LevelType+  deriving stock (Eq, Show, Generic)+  deriving anyclass (NFData)++data CDecl l = CDecl !l !Level !Ident !(CExp l)+  deriving stock (Eq, Show, Generic)+  deriving anyclass (NFData)++-- Parses a concrete declaration from a string+cdeclParser :: Parser (CDecl SourceSpan)+cdeclParser = result where+  result = branch+    [ parser "declare" LevelType+    , parser "define" LevelTerm+    ]++  parser name lvl = around2 (flip CDecl lvl) (parens (symbol name *> ((,) <$> nonKeywordParser <*> cexpParser)))++runCDeclParser :: String -> IO (CExp SourceSpan)+runCDeclParser = runParserIO cexpParser++-- Just the expressions of our language that have nothing to do with naming+data Exp a =+    ExpBool !Bool+  | ExpInt !Int+  | ExpApp a a+  | ExpAdd a a+  | ExpIf a a a+  | ExpIsZero a+  | ExpAsc a a+  | ExpTyBool+  | ExpTyInt+  | ExpTyFun a a+  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)+  deriving anyclass (NFData)++data Decl a = Decl !Level !Ident a+  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)+  deriving anyclass (NFData)++-- An ExpScope without locations+type ExpScope a = Scope (NameOnly Ident) Exp a++type DeclScope a = Decl (ExpScope a)++-- A nameless equivalent to 'CExp'+type ExpLocScope l a = LocScope l (NameOnly Ident) Exp a++type DeclLocScope l a = Located l (Decl (ExpLocScope l a))++declLocScopeForget :: DeclLocScope l a -> DeclScope a+declLocScopeForget = fmap locScopeForget . locatedVal++declScopeAnno :: l -> DeclScope a -> DeclLocScope l a+declScopeAnno l = Located l . fmap (scopeAnno l)++-- Convert to nameless representation+expToNameless :: CExp l -> ExpLocScope l Ident+expToNameless ce =+  case ce of+    CExpBool l b -> LocScopeEmbed l (ExpBool b)+    CExpInt l i -> LocScopeEmbed l (ExpInt i)+    CExpApp l a b -> LocScopeEmbed l (ExpApp (expToNameless a) (expToNameless b))+    CExpAdd l a b -> LocScopeEmbed l (ExpAdd (expToNameless a) (expToNameless b))+    CExpIf l a b c -> LocScopeEmbed l (ExpIf (expToNameless a) (expToNameless b) (expToNameless c))+    CExpIsZero l a -> LocScopeEmbed l (ExpIsZero (expToNameless a))+    CExpVar l x -> LocScopeFree l x+    CExpAbs l x a -> runColocated (locScopeAbstract1 (NameOnly x) x (expToNameless a)) l+    CExpAsc l a b -> LocScopeEmbed l (ExpAsc (expToNameless a) (expToNameless b))+    CExpTyInt l -> LocScopeEmbed l ExpTyInt+    CExpTyBool l -> LocScopeEmbed l ExpTyBool+    CExpTyFun l a b -> LocScopeEmbed l (ExpTyFun (expToNameless a) (expToNameless b))++-- Convert back to named representation. Usually this isn't a necessary operation,+-- but we want to do round-trip testing+expToNamed :: ExpLocScope l Ident -> Maybe (CExp l)+expToNamed e =+  case e of+    LocScopeBound _ _ -> Nothing+    LocScopeFree l a -> pure (CExpVar l a)+    LocScopeBinder l _ (NameOnly x) b -> CExpAbs l x <$> expToNamed (locScopeUnAbstract1 x b)+    LocScopeEmbed l fe ->+      case fe of+        ExpBool b -> pure (CExpBool l b)+        ExpInt i -> pure (CExpInt l i)+        ExpApp a b -> CExpApp l <$> expToNamed a <*> expToNamed b+        ExpAdd a b -> CExpAdd l <$> expToNamed a <*> expToNamed b+        ExpIf a b c -> CExpIf l <$> expToNamed a <*> expToNamed b <*> expToNamed c+        ExpIsZero a -> CExpIsZero l <$> expToNamed a+        ExpAsc a b -> CExpAsc l <$> expToNamed a <*> expToNamed b+        ExpTyInt -> pure (CExpTyInt l)+        ExpTyBool -> pure (CExpTyBool l)+        ExpTyFun a b -> CExpTyFun l <$> expToNamed a <*> expToNamed b++declToNameless :: CDecl l -> DeclLocScope l Ident+declToNameless (CDecl l lvl i e) = Located l (Decl lvl i (expToNameless e))++declToNamed :: DeclLocScope l Ident -> Maybe (CDecl l)+declToNamed (Located l (Decl lvl i e)) = fmap (CDecl l lvl i) (expToNamed e)

@@ -0,0 +1,51 @@+module Test.Blanks.ExpTest where++import Blanks (pattern NameOnly, pattern ScopeBinder, pattern ScopeBound, pattern ScopeEmbed, pattern ScopeFree,+               locScopeForget, locScopeLocation)+import Control.DeepSeq (force)+import Test.Blanks.Exp (Exp (..), ExpScope, Ident (..), cexpLoc, expToNamed, expToNameless, runCExpParser)+import Test.Tasty (TestName, TestTree, testGroup)+import Test.Tasty.HUnit (testCase, (@?=))++testSingle :: TestName -> String -> ExpScope Ident -> TestTree+testSingle name input expected = testCase name $ do+  namedExp <- runCExpParser input+  -- Force here just to test that we can+  let namelessExp = force (expToNameless namedExp)+  cexpLoc namedExp @?= locScopeLocation namelessExp+  let actual = locScopeForget namelessExp+  expected @?= actual+  let renamedExp = expToNamed namelessExp+  Just namedExp @?= renamedExp++testExp :: TestTree+testExp = testGroup "Exp" cases where+  xIdent = Ident "x"+  yIdent = Ident "y"+  xExp = ScopeFree xIdent+  yExp = ScopeFree yIdent+  trueExp = ScopeEmbed (ExpBool True)+  intExp = ScopeEmbed (ExpInt 42)+  negIntExp = ScopeEmbed (ExpInt (-42))+  boolTyExp = ScopeEmbed ExpTyBool+  intTyExp = ScopeEmbed ExpTyInt+  cases =+    [ testSingle "var" "x" xExp+    , testSingle "true" "#t" trueExp+    , testSingle "false" "#f" (ScopeEmbed (ExpBool False))+    , testSingle "int" "42" intExp+    , testSingle "neg int" "-42" negIntExp+    , testSingle "add" "(+ 42 -42)" (ScopeEmbed (ExpAdd intExp negIntExp))+    , testSingle "if" "(if #t 42 -42)" (ScopeEmbed (ExpIf trueExp intExp negIntExp))+    , testSingle "add var" "(+ 42 x)" (ScopeEmbed (ExpAdd intExp xExp))+    , testSingle "iszero" "(zero? 42)" (ScopeEmbed (ExpIsZero intExp))+    , testSingle "app" "(x y)" (ScopeEmbed (ExpApp xExp yExp))+    , testSingle "abs yy" "(lambda (y) y)" (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0))+    , testSingle "abs xyy" "(lambda (x) (lambda (y) y))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0)))+    , testSingle "abs xyx" "(lambda (x) (lambda (y) x))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 1)))+    , testSingle "app abs" "((lambda (x) x) 42)" (ScopeEmbed (ExpApp (ScopeBinder 1 (NameOnly xIdent) (ScopeBound 0)) intExp))+    , testSingle "ty bool" "bool" boolTyExp+    , testSingle "ty int" "int" intTyExp+    , testSingle "ty fun" "(-> int bool)" (ScopeEmbed (ExpTyFun intTyExp boolTyExp))+    , testSingle "asc" "(: 42 int)" (ScopeEmbed (ExpAsc intExp intTyExp))+    ]

@@ -1,164 +0,0 @@-{-# LANGUAGE DeriveAnyClass #-}--module Test.Blanks.LocScopeTest where--import Blanks-import Control.DeepSeq (NFData, force)-import GHC.Generics (Generic)-import Test.Blanks.Parsing-import Test.Tasty-import Test.Tasty.HUnit---- A newtype indicating an identifier in our language-newtype Ident = Ident { unIdent :: String } deriving newtype (Eq, Show, Ord, NFData)---- The type of concrete expressions, labeled with source location-data CExp l =-    CExpTrue !l-  | CExpFalse !l-  | CExpInt !l !Int-  | CExpApp !l (CExp l) (CExp l)-  | CExpAdd !l (CExp l) (CExp l)-  | CExpIf !l (CExp l) (CExp l) (CExp l)-  | CExpIsZero !l (CExp l)-  | CExpVar !l !Ident-  | CExpAbs !l !Ident (CExp l)-  deriving (Eq, Show)---- Extracts the location from a concrete expression-cexpLoc :: CExp l -> l-cexpLoc ce =-  case ce of-    CExpTrue l -> l-    CExpFalse l -> l-    CExpInt l _ -> l-    CExpApp l _ _ -> l-    CExpAdd l _ _ -> l-    CExpIf l _ _ _ -> l-    CExpIsZero l _ -> l-    CExpVar l _ -> l-    CExpAbs l _ _ -> l---- Just the expressions of our language that have nothing to do with naming-data Exp a =-    ExpTrue-  | ExpFalse-  | ExpInt !Int-  | ExpApp a a-  | ExpAdd a a-  | ExpIf a a a-  | ExpIsZero a-  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic)-  deriving anyclass (NFData)---- A nameless equivalent to 'CExp'-type ExpScope l = LocScope l (NameOnly Ident) Exp Ident---- Parsers a concrete expression from a string-cexpParser :: Parser (CExp SourceSpan)-cexpParser = result where-  result = branch-    [ trueParser-    , falseParser-    , intParser-    , addParser-    , ifParser-    , isZeroParser-    , absParser-    , appParser-    , varParser-    ]--  trueParser = around (const . CExpTrue) (symbol "#t")--  falseParser = around (const . CExpFalse) (symbol "#f")--  intParser = around CExpInt signed--  addParser = around2 CExpAdd (parens (symbol "+" >> double cexpParser))--  ifParser = around3 CExpIf (parens (symbol "if" >> triple cexpParser))--  isZeroParser = around CExpIsZero (parens (symbol "zero?" >> cexpParser))--  absParser = around2 CExpAbs $ parens $ do-    _ <- symbol "lambda"-    n <- parens (fmap Ident identifier)-    b <- cexpParser-    pure (n, b)--  appParser = around2 CExpApp (parens (double cexpParser))--  varParser = around CExpVar (fmap Ident identifier)---- Convert to nameless representation-nameless :: CExp l -> ExpScope l-nameless ce =-  case ce of-    CExpTrue l -> LocScopeEmbed l ExpTrue-    CExpFalse l -> LocScopeEmbed l ExpFalse-    CExpInt l i -> LocScopeEmbed l (ExpInt i)-    CExpApp l a b -> LocScopeEmbed l (ExpApp (nameless a) (nameless b))-    CExpAdd l a b -> LocScopeEmbed l (ExpAdd (nameless a) (nameless b))-    CExpIf l a b c -> LocScopeEmbed l (ExpIf (nameless a) (nameless b) (nameless c))-    CExpIsZero l a -> LocScopeEmbed l (ExpIsZero (nameless a))-    CExpVar l x -> LocScopeFree l x-    CExpAbs l x a -> runColocated (blankAbstract1 (NameOnly x) x (nameless a)) l---- Convert back to named representation. Usually this isn't a necessary operation,--- but we want to do round-trip testing-named :: ExpScope l -> Maybe (CExp l)-named e =-  case e of-    LocScopeBound _ _ -> Nothing-    LocScopeFree l a -> pure (CExpVar l a)-    LocScopeBinder l _ (NameOnly x) b -> CExpAbs l x <$> named (blankUnAbstract1 x b)-    LocScopeEmbed l fe ->-      case fe of-        ExpTrue -> pure (CExpTrue l)-        ExpFalse -> pure (CExpFalse l)-        ExpInt i -> pure (CExpInt l i)-        ExpApp a b -> CExpApp l <$> named a <*> named b-        ExpAdd a b -> CExpAdd l <$> named a <*> named b-        ExpIf a b c -> CExpIf l <$> named a <*> named b <*> named c-        ExpIsZero a -> CExpIsZero l <$> named a---- An ExpScope without locations-type ExpSimpleScope = Scope (NameOnly Ident) Exp Ident--testSingle :: TestName -> String -> ExpSimpleScope -> TestTree-testSingle name input expected = testCase name $ do-  namedExp <- runParserIO cexpParser input-  -- Force here just to test that we can-  let namelessExp = force (nameless namedExp)-  cexpLoc namedExp @?= locScopeLocation namelessExp-  let actual = locScopeForget namelessExp-  expected @?= actual-  let renamedExp = named namelessExp-  Just namedExp @?= renamedExp--testLocScope :: TestTree-testLocScope = testGroup "LocScope" cases where-  xIdent = Ident "x"-  yIdent = Ident "y"-  xExp = ScopeFree xIdent-  yExp = ScopeFree yIdent-  trueExp = ScopeEmbed ExpTrue-  intExp = ScopeEmbed (ExpInt 42)-  negIntExp = ScopeEmbed (ExpInt (-42))-  cases =-    [ testSingle "var" "x" xExp-    , testSingle "true" "#t" trueExp-    , testSingle "false" "#f" (ScopeEmbed ExpFalse)-    , testSingle "int" "42" intExp-    , testSingle "neg int" "-42" negIntExp-    , testSingle "add" "(+ 42 -42)" (ScopeEmbed (ExpAdd intExp negIntExp))-    , testSingle "if" "(if #t 42 -42)" (ScopeEmbed (ExpIf trueExp intExp negIntExp))-    , testSingle "add var" "(+ 42 x)" (ScopeEmbed (ExpAdd intExp xExp))-    , testSingle "iszero" "(zero? 42)" (ScopeEmbed (ExpIsZero intExp))-    , testSingle "app" "(x y)" (ScopeEmbed (ExpApp xExp yExp))-    , testSingle "abs yy" "(lambda (y) y)" (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0))-    , testSingle "abs xyy" "(lambda (x) (lambda (y) y))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0)))-    , testSingle "abs xyx" "(lambda (x) (lambda (y) x))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 1)))-    , testSingle "app abs" "((lambda (x) x) 42)" (ScopeEmbed (ExpApp (ScopeBinder 1 (NameOnly xIdent) (ScopeBound 0)) intExp))-    ]

@@ -22,11 +22,11 @@     Right a -> pure a  data SourceSpan = SourceSpan-  { _ssName :: !FilePath-  , _ssStartLine :: !MP.Pos-  , _ssStartColumn :: !MP.Pos-  , _ssEndLine :: !MP.Pos-  , _ssEndColumn :: !MP.Pos+  { ssName :: !FilePath+  , ssStartLine :: !MP.Pos+  , ssStartColumn :: !MP.Pos+  , ssEndLine :: !MP.Pos+  , ssEndColumn :: !MP.Pos   } deriving stock (Eq, Show, Ord, Generic)     deriving anyclass (NFData) 

@@ -2,42 +2,17 @@   ( testScope   ) where -import Blanks-import Control.Monad.Identity (Identity (..))-import Data.Set (Set)+import Blanks (SubError (..), scopeApply1, scopeInstantiate1) import qualified Data.Set as Set import Test.Blanks.Assertions ((@/=))-import Test.Tasty-import Test.Tasty.HUnit--type BareScope = Scope (NameOnly Char) Identity Char--abst :: Char -> BareScope -> BareScope-abst a = runIdentity . blankAbstract1 (Name a ()) a--bound :: Int -> BareScope-bound = ScopeBound--var :: Char -> BareScope-var = pure--freeVars :: BareScope -> Set Char-freeVars = foldMap Set.singleton+import Test.Blanks.SimpleScope (abst, embed, freeVars, sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, svar2,+                                swonky, swonky2, var)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase, (@?=))  testScope :: TestTree testScope =-  let svar = var 'x'-      sbound = bound 0-      sfree = abst 'y' (var 'x')-      sfree2 = abst 'z' (abst 'y' (var 'x'))-      sid = abst 'x' (var 'x')-      swonky = abst 'x' (bound 0)-      sconst = abst 'x' (abst 'y' (var 'x'))-      sflip = abst 'x' (abst 'y' (var 'y'))-      svar2 = var 'e'-      swonky2 = abst 'x' svar2--      testEq =+  let testEq =         testCase "eq" $ do           svar @?= svar           svar @/= svar2@@ -57,33 +32,38 @@           freeVars swonky @?= Set.empty           freeVars sconst @?= Set.empty           freeVars sflip @?= Set.empty-          freeVars svar2 @=? Set.singleton 'e'+          freeVars svar2 @?= Set.singleton 'e'           freeVars swonky2 @?= Set.singleton 'e'+          freeVars spair @?= Set.singleton 'x'        testInstantiate =         testCase "instantiate" $ do-          blankInstantiate1 (pure svar2) svar @?= svar-          blankInstantiate1 (pure svar2) sbound @?= svar2-          blankInstantiate1 (pure svar2) sid @?= sid-          blankInstantiate1 (pure svar2) swonky @?= swonky2+          scopeInstantiate1 svar2 svar @?= svar+          scopeInstantiate1 svar2 sbound @?= svar2+          scopeInstantiate1 svar2 sid @?= sid+          scopeInstantiate1 svar2 swonky @?= swonky2+          scopeInstantiate1 svar2 spair @?= embed svar svar2        testApply =         testCase "apply" $ do-          blankApply1 (pure svar2) sid @?= Right svar2-          blankApply1 (pure svar2) swonky @?= Right sbound-          blankApply1 (pure svar2) sconst @?= Right swonky2-          blankApply1 (pure svar2) sflip @?= Right sid+          scopeApply1 svar2 sid @?= Right svar2+          scopeApply1 svar2 swonky @?= Right sbound+          scopeApply1 svar2 sconst @?= Right swonky2+          scopeApply1 svar2 sflip @?= Right sid+          scopeApply1 svar2 svar @?= Left NonBinderError        testVarSub =         testCase "var sub" $ do           (svar >>= const svar2) @?= svar2           (sfree >>= const svar2) @?= abst 'y' svar2           (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)+          (spair >>= const svar2) @?= embed svar2 sbound        testIdSub =         testCase "id sub" $ do           (svar >>= const sid) @?= sid           (sfree >>= const sid) @?= abst 'y' sid           (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)+          (spair >>= const sid) @?= embed sid sbound     in testGroup "Scope" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]

@@ -0,0 +1,43 @@+module Test.Blanks.SimpleScope where++import Blanks (NameOnly, pattern NameOnly, Scope, pattern ScopeBound, pattern ScopeEmbed, Tracked, locScopeLocation,+               scopeAbstract1, trackScopeSimple)+import Data.Set (Set)+import qualified Data.Set as Set++data SimpleFunctor a = SimpleFunctor !a !a+  deriving stock (Eq, Show, Functor, Foldable, Traversable)++type SimpleScope = Scope (NameOnly Char) SimpleFunctor Char++abst :: Char -> SimpleScope -> SimpleScope+abst a = scopeAbstract1 (NameOnly a) a++bound :: Int -> SimpleScope+bound = ScopeBound++var :: Char -> SimpleScope+var = pure++freeVars :: SimpleScope -> Set Char+freeVars = foldMap Set.singleton++tracked :: SimpleScope -> Tracked Char+tracked = locScopeLocation . trackScopeSimple++embed :: SimpleScope -> SimpleScope -> SimpleScope+embed x y = ScopeEmbed (SimpleFunctor x y)++svar, sbound, sfree, sfree2, sid, swonky, sconst, sflip, svar2, swonky2, spair, swonky3 :: SimpleScope+svar = var 'x'+sbound = bound 0+sfree = abst 'y' (var 'x')+sfree2 = abst 'z' (abst 'y' (var 'x'))+sid = abst 'x' (var 'x')+swonky = abst 'x' (bound 0)+sconst = abst 'x' (abst 'y' (var 'x'))+sflip = abst 'x' (abst 'y' (var 'y'))+svar2 = var 'e'+swonky2 = abst 'x' svar2+spair = embed svar sbound+swonky3 = abst 'x' (bound 3)

@@ -0,0 +1,45 @@+module Test.Blanks.SplitScope where++import Blanks (BinderId, BinderScope, LocScope, pattern LocScopeBound, pattern LocScopeEmbed, NameOnly,+               pattern NameOnly, SplitBinder (..), SplitFunctor (..), SplitResult, Tracked,+               WithTracked (withTrackedState), locScopeAbstract1, locScopeInnerBinder1, locScopeLocation, runColocated,+               scopeAnno, splitLocScope, trackScope)+import qualified Data.Sequence as Seq+import Data.Set (Set)+import qualified Data.Set as Set+import Test.Blanks.SimpleScope (SimpleFunctor (..), SimpleScope)++type SplitScope = LocScope () (NameOnly Char) (SplitFunctor SimpleFunctor) Char+type SplitInnerBinder = BinderScope (NameOnly Char) SplitScope+type SplitOuterBinder = SplitBinder () (NameOnly Char) SimpleFunctor Char+type SplitScopeResult = SplitResult () (NameOnly Char) SimpleFunctor Char++abstSplit :: Char -> SplitScope -> SplitScope+abstSplit a = flip runColocated () . locScopeAbstract1 (NameOnly a) a++innerBinderSplit :: Char -> SplitScope -> SplitInnerBinder+innerBinderSplit a = locScopeInnerBinder1 (NameOnly a) a++boundSplit :: Int -> SplitScope+boundSplit = LocScopeBound ()++varSplit :: Char -> SplitScope+varSplit = pure++freeVarsSplit :: SplitScope -> Set Char+freeVarsSplit = foldMap Set.singleton++trackedSplit :: SplitScope -> Tracked Char+trackedSplit = withTrackedState . locScopeLocation . trackScope++embedSplit :: SplitScope -> SplitScope -> SplitScope+embedSplit x y = LocScopeEmbed () (SplitFunctorBase (SimpleFunctor x y))++closureSplit :: BinderId -> [Int] -> SplitScope+closureSplit bid vars = LocScopeEmbed () (SplitFunctorClosure bid (Seq.fromList vars))++outerBinderSplit :: Int -> [Char] -> SplitInnerBinder -> SplitOuterBinder+outerBinderSplit a = SplitBinder a . Set.fromList++simpleSplit :: SimpleScope -> SplitScopeResult+simpleSplit s = splitLocScope (trackScope (scopeAnno () s))

@@ -0,0 +1,70 @@+module Test.Blanks.SplitTest+  ( testSplit+  ) where++import Blanks (BinderId, SplitResult (..), Tracked, mkTrackedBound, mkTrackedFree)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Test.Blanks.SimpleScope (SimpleScope, sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, swonky, swonky3)+import Test.Blanks.SplitScope (SplitOuterBinder, SplitScope, boundSplit, closureSplit, embedSplit, innerBinderSplit,+                               outerBinderSplit, simpleSplit, varSplit)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase, (@?=))++data SplitCase = SplitCase+  { splitCaseName :: !String+  , splitCaseScopeIn :: !SimpleScope+  , splitCaseTrackedOut :: !(Tracked Char)+  , splitCaseScopeOut :: !SplitScope+  , splitCaseBinders :: !(Map BinderId SplitOuterBinder)+  } deriving stock (Eq, Show)++splitCases :: [SplitCase]+splitCases =+  let xvar = varSplit 'x'+      xbound = boundSplit 0+      xpair = embedSplit xvar xbound+  in [ SplitCase "var" svar (mkTrackedFree 'x') xvar Map.empty+    , SplitCase "bound" sbound (mkTrackedBound 0) xbound Map.empty+    , SplitCase "pair" spair (mkTrackedFree 'x' <> mkTrackedBound 0) xpair Map.empty+    , let ib = innerBinderSplit 'y' (varSplit 'x')+          ob = outerBinderSplit 0 ['x'] ib+      in SplitCase "free" sfree mempty (closureSplit 0 []) (Map.singleton 0 ob)+    , let ibY = innerBinderSplit 'y' (varSplit 'x')+          obY = outerBinderSplit 0 ['x'] ibY+          ibZ = innerBinderSplit 'z' (closureSplit 1 [])+          obZ = outerBinderSplit 0 ['x'] ibZ+      in SplitCase "free2" sfree2 mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)])+    , let ib = innerBinderSplit 'x' (varSplit 'x')+          ob = outerBinderSplit 0 [] ib+      in SplitCase "id" sid mempty (closureSplit 0 []) (Map.singleton 0 ob)+    , let ib = innerBinderSplit 'x' (boundSplit 0)+          ob = outerBinderSplit 1 [] ib+      in SplitCase "wonky" swonky (mkTrackedBound 0) (closureSplit 0 [0]) (Map.singleton 0 ob)+    , let ibY = innerBinderSplit 'y' (boundSplit 0)+          obY = outerBinderSplit 1 [] ibY+          ibZ = innerBinderSplit 'x' (closureSplit 1 [0])+          obZ = outerBinderSplit 0 [] ibZ+      in SplitCase "const" sconst mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)])+    , let ibY = innerBinderSplit 'y' (varSplit 'y')+          obY = outerBinderSplit 0 [] ibY+          ibZ = innerBinderSplit 'x' (closureSplit 1 [])+          obZ = outerBinderSplit 0 [] ibZ+      in SplitCase "flip" sflip mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)])+    , let ib = innerBinderSplit 'x' (boundSplit 3)+          ob = outerBinderSplit 1 [] ib+      in SplitCase "wonky3" swonky3 (mkTrackedBound 3) (closureSplit 0 [3]) (Map.singleton 0 ob)+    ]++runSplitCase :: SplitCase -> IO ()+runSplitCase (SplitCase _ scopeIn trackedOut scopeOut binders) = do+  let SplitResult actualTrackedOut actualScopeOut actualBinders = simpleSplit scopeIn+  actualTrackedOut @?= trackedOut+  actualScopeOut @?= scopeOut+  actualBinders @?= binders++testSplitCase :: SplitCase -> TestTree+testSplitCase c = testCase (splitCaseName c) (runSplitCase c)++testSplit :: TestTree+testSplit = testGroup "Split" (fmap testSplitCase splitCases)

@@ -0,0 +1,24 @@+module Test.Blanks.TrackedTest+  ( testTracked+  ) where++import Blanks (mkTrackedBound, mkTrackedFree)+import Test.Blanks.SimpleScope (sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, svar2, swonky, swonky2, swonky3,+                                tracked)+import Test.Tasty (TestTree)+import Test.Tasty.HUnit (testCase, (@?=))++testTracked :: TestTree+testTracked = testCase "tracked" $ do+  tracked svar @?= mkTrackedFree 'x'+  tracked sbound @?= mkTrackedBound 0+  tracked sfree @?= mkTrackedFree 'x'+  tracked sfree2 @?= mkTrackedFree 'x'+  tracked sid @?= mempty+  tracked swonky @?= mkTrackedBound 0+  tracked sconst @?= mempty+  tracked sflip @?= mempty+  tracked svar2 @?= mkTrackedFree 'e'+  tracked swonky2 @?= mkTrackedFree 'e'+  tracked spair @?= mkTrackedFree 'x' <> mkTrackedBound 0+  tracked swonky3 @?= mkTrackedBound 3