blanks 0.3.0 → 0.4.0

raw patch · 23 files changed

+1050/−540 lines, 23 filesdep +megaparsecdep +textdep −tasty-discoverdep ~adjunctionsdep ~containersdep ~distributivePVP ok

version bump matches the API change (PVP)

Dependencies added: megaparsec, text

Dependencies removed: tasty-discover

Dependency ranges changed: adjunctions, containers, distributive, mtl

API changes (from Hackage documentation)

Files

• README.md +20/−1
• app/Main.hs +0/−5
• blanks.cabal +24/−37
• src/Blanks.hs +23/−5
• src/Blanks/Class.hs +0/−53
• src/Blanks/Interface.hs +209/−0
• src/Blanks/LocScope.hs +61/−74
• src/Blanks/Located.hs +59/−0
• src/Blanks/Name.hs +12/−2
• src/Blanks/NatNewtype.hs +29/−0
• src/Blanks/PureScope.hs +0/−55
• src/Blanks/RightAdjunct.hs +0/−20
• src/Blanks/Scope.hs +60/−0
• src/Blanks/ScopeT.hs +0/−171
• src/Blanks/ScopeW.hs +188/−0
• src/Blanks/Sub.hs +12/−17
• src/Blanks/UnderScope.hs +20/−12
• test/Main.hs +10/−0
• test/Tasty.hs +0/−1
• test/Test/Blanks/BlanksTest.hs +0/−87
• test/Test/Blanks/LocScopeTest.hs +159/−0
• test/Test/Blanks/Parsing.hs +75/−0
• test/Test/Blanks/ScopeTest.hs +89/−0

@@ -2,4 +2,23 @@  [![CircleCI](https://circleci.com/gh/ejconlon/blanks/tree/master.svg?style=svg)](https://circleci.com/gh/ejconlon/blanks/tree/master) -Fill-in-the-blanks - A library factoring out substitution from ASTs. (Not production ready!)+Fill-in-the-blanks - A library factoring out substitution from ASTs.++It's a pain to track de Bruijn indices yourself to implement capture-avoiding subsititution,+so this library provides some wrappers that help. One of the best libraries for this is+[bound](https://hackage.haskell.org/package/bound), which uses a clever representation to make+these operations safe and fast. The tradeoff is that you have to define a `Monad` instance+for your expression functor, which in practice can be tricky. (It's even trickier to derive+`Eq` and `Show`!)++This library takes the simpler, slower, and rather "succ-y" free-monad-ish approach,+but with a twist. It expects you to rewrite all name-binding constructors in your expression+as annotations on a single "binder" constructor. This allows you to use the provided `Scope`+type (or a variant) as a wrapper around your expression functor, which is only required to+implement `Functor`. This representation is less safe (since you can inspect and manipulate+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.

@@ -1,5 +0,0 @@-module Main where---- TODO(ejconlon) Create demo app-main :: IO ()-main = pure ()

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: 6dd5dac29a7eb8991e9d2728daa61f8651bf8e283305aa1063f1daf4dce65fd8+-- hash: dce6fa2995f08e5b1615eab81bbbbb7339ba49c1db0902125b8495fc24c84bd1  name:           blanks-version:        0.3.0+version:        0.4.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,64 +29,51 @@ library   exposed-modules:       Blanks-      Blanks.Class+      Blanks.Interface+      Blanks.Located       Blanks.LocScope       Blanks.Name-      Blanks.PureScope-      Blanks.RightAdjunct-      Blanks.ScopeT+      Blanks.NatNewtype+      Blanks.Scope+      Blanks.ScopeW       Blanks.Sub       Blanks.UnderScope   other-modules:       Paths_blanks   hs-source-dirs:       src-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable 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-    , base >=4.12 && <5-    , containers >=0.6-    , distributive >=0.6-    , mtl >=2.2-  default-language: Haskell2010--executable blanks-exe-  main-is: Main.hs-  other-modules:-      Paths_blanks-  hs-source-dirs:-      app-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses 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+      adjunctions >=4.4 && <5     , base >=4.12 && <5-    , blanks-    , containers >=0.6-    , distributive >=0.6-    , mtl >=2.2+    , containers >=0.6 && <1+    , distributive >=0.6 && <1+    , mtl >=2.2 && <3   default-language: Haskell2010  test-suite blanks-test   type: exitcode-stdio-1.0-  main-is: Tasty.hs+  main-is: Main.hs   other-modules:       Test.Blanks.Assertions-      Test.Blanks.BlanksTest+      Test.Blanks.LocScopeTest+      Test.Blanks.Parsing+      Test.Blanks.ScopeTest       Paths_blanks   hs-source-dirs:       test-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable 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+      adjunctions >=4.4 && <5     , base >=4.12 && <5     , blanks-    , containers >=0.6-    , distributive >=0.6-    , mtl >=2.2+    , containers >=0.6 && <1+    , distributive >=0.6 && <1+    , megaparsec+    , mtl >=2.2 && <3     , tasty-    , tasty-discover     , tasty-hunit+    , text   default-language: Haskell2010

@@ -1,12 +1,30 @@+-- | Fill-in-the-blanks - A library factoring out substitution from ASTs.+--+-- It's a pain to track de Bruijn indices yourself to implement capture-avoiding subsititution,+-- so this library provides some wrappers that help. One of the best libraries for this is+-- <https://hackage.haskell.org/package/bound bound>, which uses a clever representation to make+-- these operations safe and fast. The tradeoff is that you have to define a 'Monad' instance+-- for your expression functor, which in practice can be tricky. (It's even trickier to derive+-- 'Eq' and 'Show'!)+--+-- This library takes the simpler, slower, and rather "succ-y" free-monad-ish approach,+-- but with a twist. It expects you to rewrite all name-binding constructors in your expression+-- as annotations on a single "binder" constructor. This allows you to use the provided 'Scope'+-- type (or a variant) as a wrapper around your expression functor, which is only required to+-- implement 'Functor'. This representation is less safe (since you can inspect and manipulate+-- 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. module Blanks   ( module Blanks   ) where -import Blanks.Class as Blanks+import Blanks.Interface as Blanks+import Blanks.Located as Blanks import Blanks.LocScope as Blanks import Blanks.Name as Blanks-import Blanks.PureScope as Blanks-import Blanks.RightAdjunct as Blanks-import Blanks.ScopeT as Blanks+import Blanks.Scope as Blanks import Blanks.Sub as Blanks-import Blanks.UnderScope as Blanks

@@ -1,53 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}--module Blanks.Class-  ( BlankAbstract (..)-  , BlankCodomain-  , BlankEmbed (..)-  , BlankFunctor-  , BlankInfo-  ) where--import Blanks.Sub (SubError)-import Data.Sequence (Seq)-import qualified Data.Sequence as Seq--type family BlankInfo (m :: * -> *) :: *-type family BlankFunctor (m :: * -> *) :: * -> *-type family BlankCodomain (m :: * -> *) :: * -> *--class BlankEmbed (m :: * -> *) where-  -- | "embed functor"-  blankEmbed :: BlankFunctor m (m a) -> BlankCodomain m (m a)--class BlankAbstract (m :: * -> *) where-  -- | "free name"-  blankFree :: a -> BlankCodomain m (m a)--  -- | "abstract info names body"-  blankAbstract :: Eq a => BlankInfo m -> Seq a -> m a -> BlankCodomain m (m a)--  -- | 'blankAbstract' for a single argument-  blankAbstract1 :: Eq a => BlankInfo m -> a -> m a -> BlankCodomain m (m a)-  blankAbstract1 n k = blankAbstract n (Seq.singleton k)--  -- | "unAbstract names body"-  blankUnAbstract :: Seq a -> m a -> m a--  -- 'blankUnAbstract' for a single argument-  blankUnAbstract1 :: a -> m a -> m a-  blankUnAbstract1 = blankUnAbstract . Seq.singleton--  -- | "instantiate args body"-  blankInstantiate :: Seq (BlankCodomain m (m a)) -> m a -> m a--  -- | 'blankInstantiate' for a single argument-  blankInstantiate1 :: BlankCodomain m (m a) -> m a -> m a-  blankInstantiate1 = blankInstantiate . Seq.singleton--  -- | "apply args abstraction"-  blankApply :: Seq (BlankCodomain m (m a)) -> m a -> Either SubError (m a)--  -- | 'blankApply' for a single argument-  blankApply1 :: BlankCodomain m (m a) -> m a -> Either SubError (m a)-  blankApply1 = blankApply . Seq.singleton

@@ -0,0 +1,209 @@+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 #-}

@@ -1,98 +1,85 @@ {-# LANGUAGE UndecidableInstances #-}  module Blanks.LocScope-  ( Colocated (..)-  , Located (..)-  , LocScope (..)-  , LocScopeRawFold-  , LocScopeFold-  , askColocated-  , colocated-  , locScopeBind-  , locScopeEmbed-  , locScopeRawFold-  , locScopeFold-  , locScopeFree-  , runColocated+  ( LocScope (..)+  , pattern LocScopeBound+  , pattern LocScopeFree+  , pattern LocScopeBinder+  , pattern LocScopeEmbed+  , locScopeLocation+  , locScopeForget   ) where -import Blanks.Class-import Blanks.RightAdjunct (RightAdjunct)-import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFold, scopeTFree, scopeTRawFold)-import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)+import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankHoistAnno, blankMapAnno)+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 Control.Monad (ap) import Control.Monad.Identity (Identity (..))-import Control.Monad.Reader (MonadReader, Reader, ReaderT (..), ask, runReader)-import Data.Distributive (Distributive (..))-import Data.Functor.Adjunction (Adjunction (..))-import Data.Functor.Rep (Representable)+import Control.Monad.Writer (MonadWriter (..)) -data Located l a = Located-  { _locatedLoc :: !l-  , _locatedVal :: !a-  } deriving (Eq, Show, Functor, Foldable, Traversable)+-- | 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 (Functor, Foldable, Traversable) -newtype Colocated l a = Colocated-  { unColocated :: Reader l a-  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)+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 -type instance RightAdjunct (Located l) = Colocated l+instance Functor f => Blank (LocScope l n f)+instance NatNewtype (ScopeW (Located l) n f (LocScope l n f)) (LocScope l n f) -colocated :: (l -> a) -> Colocated l a-colocated f = Colocated (ReaderT (Identity . f))+pattern LocScopeBound :: l -> Int -> LocScope l n f a+pattern LocScopeBound l b = LocScope (ScopeW (Located l (UnderScopeBound b))) -askColocated :: Colocated l l-askColocated = Colocated ask+pattern LocScopeFree :: l -> a -> LocScope l n f a+pattern LocScopeFree l a = LocScope (ScopeW (Located l (UnderScopeFree a))) -runColocated :: Colocated l a -> l -> a-runColocated = runReader . unColocated+pattern LocScopeBinder :: l -> Int -> n -> LocScope l n f a -> LocScope l n f a+pattern LocScopeBinder l i n e = LocScope (ScopeW (Located l (UnderScopeBinder i n e))) -instance Distributive (Colocated l) where-  distribute = Colocated . distribute . fmap unColocated+pattern LocScopeEmbed :: l -> f (LocScope l n f a) -> LocScope l n f a+pattern LocScopeEmbed l fe = LocScope (ScopeW (Located l (UnderScopeEmbed fe))) -instance Adjunction (Located l) (Colocated l) where-  leftAdjunct v a = colocated (v . flip Located a)-  rightAdjunct h (Located l a) = runColocated (h a) l+{-# COMPLETE LocScopeBound, LocScopeFree, LocScopeBinder, LocScopeEmbed #-} -instance Monoid l => Applicative (Located l) where-  pure = Located mempty+-- | Extract the location (annotation) from this scope.+locScopeLocation :: LocScope l n f a -> l+locScopeLocation s =+  case s of+    LocScopeBound l _ -> l+    LocScopeFree l _ -> l+    LocScopeBinder l _ _ _ -> l+    LocScopeEmbed l _ -> l++instance (Monoid l, Functor f) => Applicative (LocScope l n f) where+  pure = LocScopeFree mempty   (<*>) = ap -instance Monoid l => Monad (Located l) where+instance (Monoid l, Functor f) => Monad (LocScope l n f) where   return = pure-  Located l a >>= f = let Located p b = f a in Located (l <> p) b--newtype LocScope l n f a = LocScope-  { unLocScope :: ScopeT (Located l) n f a-  } deriving (Functor, Foldable, Traversable, BlankAbstract)--type instance BlankInfo (LocScope l n f) = n-type instance BlankFunctor (LocScope l n f) = f-type instance BlankCodomain (LocScope l n f) = Colocated l+  s >>= f = blankBind go s where+    go a = fmap (\l1 -> let LocScope (ScopeW (Located l2 b)) = f a in LocScope (ScopeW (Located (l1 <> l2) b))) askColocated -instance Functor f => BlankEmbed (LocScope l n f) where-  blankEmbed = locScopeEmbed+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) -instance (Eq (f (ScopeT (Located l) n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where+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 -instance (Show (f (ScopeT (Located l) n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where-  showsPrec d (LocScope (ScopeT tu)) = showString "LocScope " . showsPrec (d+1) tu--locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a)-locScopeEmbed fe = colocated (\l -> LocScope (ScopeT (Located l (UnderEmbedScope (EmbedScope (fmap unLocScope fe))))))--locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b-locScopeBind f = LocScope . scopeTBind (fmap unLocScope . f) . unLocScope--locScopeFree :: a -> Colocated l (LocScope l n f a)-locScopeFree = fmap LocScope . scopeTFree--type LocScopeRawFold l n f a r = UnderScopeFold n f (LocScope l n f a) a r-type LocScopeFold l n f a r = LocScopeRawFold l n f a (Colocated l r)--locScopeRawFold :: Functor f => LocScopeRawFold l n f a r -> LocScope l n f a -> Located l r-locScopeRawFold usf = scopeTRawFold (underScopeFoldContraMap LocScope usf) . unLocScope+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 -locScopeFold :: Functor f => LocScopeFold l n f a r -> LocScope l n f a -> r-locScopeFold usf = scopeTFold (underScopeFoldContraMap LocScope usf) . unLocScope+-- | 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)

@@ -0,0 +1,59 @@+{-# LANGUAGE UndecidableInstances #-}++module Blanks.Located+  ( Colocated (..)+  , Located (..)+  , askColocated+  , colocated+  , runColocated+  ) where++import Control.Monad (ap)+import Control.Monad.Reader (MonadReader, Reader, ReaderT (..), ask, reader, runReader)+import Control.Monad.Writer (MonadWriter (..))+import Data.Distributive (Distributive (..))+import Data.Functor.Adjunction (Adjunction (..))+import Data.Functor.Rep (Representable)++-- | This is basically the 'Env' comonad, but with the env strict.+-- 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+  } deriving (Eq, Show, Functor, Foldable, Traversable)++-- | Because we defined a unique left adjoint, we have to define the unique right.+newtype Colocated l a = Colocated+  { unColocated :: Reader l a+  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)++colocated :: (l -> a) -> Colocated l a+colocated f = Colocated (reader f)++askColocated :: Colocated l l+askColocated = Colocated ask++runColocated :: Colocated l a -> l -> a+runColocated = runReader . unColocated++instance Distributive (Colocated l) where+  distribute = Colocated . distribute . fmap unColocated++instance Adjunction (Located l) (Colocated l) where+  leftAdjunct v a = colocated (v . flip Located a)+  rightAdjunct h (Located l a) = runColocated (h a) l++instance Monoid l => Applicative (Located l) where+  pure = Located mempty+  (<*>) = ap++instance Monoid l => Monad (Located l) where+  return = pure+  Located l a >>= f = let Located p b = f a in Located (l <> p) b++instance Monoid l => MonadWriter l (Located l) where+  writer (a, l) = Located l a+  tell l = Located l ()+  listen (Located l a) = Located l (a, l)+  pass (Located l (a, f)) = Located (f l) a

@@ -1,16 +1,26 @@ module Blanks.Name   ( Name (..)   , NameOnly+  , pattern NameOnly   ) where +-- | 'Name' is compared on value only, allowing you to define and use+-- things like 'NameOnly' in your 'BlankInfo' values to make alpha-equivalent+-- terms structurally ('Eq') equivalent. data Name n a =   Name-    { nameKey :: n-    , nameValue :: a+    { _nameKey :: n+    , _nameValue :: a     }   deriving (Show, Functor, Foldable, Traversable)  instance Eq a => Eq (Name n a) where   Name _ x == Name _ y = x == y +-- An erased 'Name'. type NameOnly n = Name n ()++pattern NameOnly :: n -> NameOnly n+pattern NameOnly n = Name n ()++{-# COMPLETE NameOnly #-}

@@ -0,0 +1,29 @@+{-# LANGUAGE QuantifiedConstraints #-}++module Blanks.NatNewtype+  ( NatNewtype+  , natNewtypeFrom+  , natNewtypeTo+  ) where++import Data.Coerce (Coercible, coerce)+import Data.Kind (Type)++-- | A "natural isomorphism" between two functors, like exists+-- derivably between newtyped functors and their wrapped types.+-- The functional dependency requires that 'g' be the newtype+-- and 'm' the wrapped type.+class+  ( forall a. Coercible (m a) (g a)+  , forall a. Coercible (g a) (m a)+  )=> NatNewtype (m :: Type -> Type) (g :: Type -> Type) | g -> m++-- | Coerce from the wrapped type to the newtype.+natNewtypeTo :: NatNewtype m g => m a -> g a+natNewtypeTo = coerce+{-# INLINE natNewtypeTo #-}++-- | Coerce from the newtype to the wrapped type.+natNewtypeFrom :: NatNewtype m g => g a -> m a+natNewtypeFrom = coerce+{-# INLINE natNewtypeFrom #-}

@@ -1,55 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Blanks.PureScope-  ( PureScope (..)-  , PureScopeFold-  , pureScopeBind-  , pureScopeEmbed-  , pureScopeFold-  , pureScopeFree-  ) where--import Blanks.Class-import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFree, scopeTRawFold)-import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)-import Control.Monad (ap)-import Control.Monad.Identity (Identity (..))--newtype PureScope n f a = PureScope-  { unPureScope :: ScopeT Identity n f a-  } deriving (Functor, Foldable, Traversable, BlankAbstract)--type instance BlankInfo (PureScope n f) = n-type instance BlankFunctor (PureScope n f) = f-type instance BlankCodomain (PureScope n f) = Identity--instance Functor f => Applicative (PureScope n f) where-  pure = pureScopeFree-  (<*>) = ap--instance Functor f => Monad (PureScope n f) where-  return = pureScopeFree-  s >>= f = pureScopeBind f s--instance Functor f => BlankEmbed (PureScope n f) where-  blankEmbed = Identity . pureScopeEmbed--instance (Eq (f (ScopeT Identity n f a)), Eq n, Eq a) => Eq (PureScope n f a) where-  PureScope su == PureScope sv = su == sv--instance (Show (f (ScopeT Identity n f a)), Show n, Show a) => Show (PureScope n f a) where-  showsPrec d (PureScope (ScopeT tu)) = showString "PureScope " . showsPrec (d+1) tu--pureScopeFree :: a -> PureScope n f a-pureScopeFree = PureScope . runIdentity . scopeTFree--pureScopeBind :: Functor f => (a -> PureScope n f b) -> PureScope n f a -> PureScope n f b-pureScopeBind f = PureScope . scopeTBind (Identity . unPureScope . f) . unPureScope--pureScopeEmbed :: Functor f => f (PureScope n f a) -> PureScope n f a-pureScopeEmbed fe = PureScope (ScopeT (Identity (UnderEmbedScope (EmbedScope (fmap unPureScope fe)))))--type PureScopeFold n f a r = UnderScopeFold n f (PureScope n f a) a r--pureScopeFold :: Traversable f => PureScopeFold n f a r -> PureScope n f a -> r-pureScopeFold usf = runIdentity . scopeTRawFold (underScopeFoldContraMap PureScope usf) . unPureScope

@@ -1,20 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE UndecidableInstances #-}--module Blanks.RightAdjunct-  ( RightAdjunct-  , RightAdjunction-  , RightAdjunctionApplicative-  ) where--import Control.Monad.Identity (Identity)-import Data.Functor.Adjunction (Adjunction (..))--type family RightAdjunct (t :: * -> *) :: * -> *--type instance RightAdjunct Identity = Identity--type RightAdjunction (t :: * -> *) = Adjunction t (RightAdjunct t)--type RightAdjunctionApplicative t = (RightAdjunction t, Applicative (RightAdjunct t))

@@ -0,0 +1,60 @@+{-# LANGUAGE UndecidableInstances #-}++module Blanks.Scope+  ( Scope (..)+  , pattern ScopeBound+  , pattern ScopeFree+  , pattern ScopeBinder+  , pattern ScopeEmbed+  ) where++import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankFree)+import Blanks.NatNewtype (NatNewtype)+import Blanks.ScopeW (ScopeW (..))+import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,+                          pattern UnderScopeFree)+import Control.Monad (ap)+import Control.Monad.Identity (Identity (..))++-- | 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.+newtype Scope n f a = Scope+  { unScope :: ScopeW Identity n f (Scope n f) a+  } deriving (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)++pattern ScopeBound :: Int -> Scope n f a+pattern ScopeBound b = Scope (ScopeW (Identity (UnderScopeBound b)))++pattern ScopeFree :: a -> Scope n f a+pattern ScopeFree a = Scope (ScopeW (Identity (UnderScopeFree a)))++pattern ScopeBinder :: Int -> n -> Scope n f a -> Scope n f a+pattern ScopeBinder i n e = Scope (ScopeW (Identity (UnderScopeBinder i n e)))++pattern ScopeEmbed :: f (Scope n f a) -> Scope n f a+pattern ScopeEmbed fe = Scope (ScopeW (Identity (UnderScopeEmbed fe)))++{-# COMPLETE ScopeBound, ScopeFree, ScopeBinder, ScopeEmbed #-}++instance Functor f => Applicative (Scope n f) where+  pure = runIdentity . blankFree+  (<*>) = ap++instance Functor f => Monad (Scope n f) where+  return = pure+  s >>= f = blankBind (Identity . 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

@@ -1,171 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}--module Blanks.ScopeT-  ( ScopeT (..)-  , ScopeTFold-  , ScopeTRawFold-  , scopeTBind-  , scopeTEmbed-  , scopeTFold-  , scopeTFree-  , scopeTHoistAnno-  , scopeTLiftAnno-  , scopeTRawFold-  ) where--import Blanks.Class-import Blanks.RightAdjunct-import Blanks.Sub (SubError (..))-import Blanks.UnderScope (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..), UnderScope (..),-                          UnderScopeFold (..), underScopeFold, underScopePure, underScopeShift)-import Data.Bifoldable (bifoldr)-import Data.Bifunctor (bimap, first)-import Data.Bitraversable (bitraverse)-import Data.Functor.Adjunction (Adjunction (..))-import Data.Maybe (fromMaybe)-import Data.Sequence (Seq)-import qualified Data.Sequence as Seq--newtype ScopeT t n f a = ScopeT-  { unScopeT :: t (UnderScope n f (ScopeT t n f a) a)-  }--instance Eq (t (UnderScope n f (ScopeT t n f a) a)) => Eq (ScopeT t n f a) where-  ScopeT tu == ScopeT tv = tu == tv--instance Show (t (UnderScope n f (ScopeT t n f a) a)) => Show (ScopeT t n f a) where-  showsPrec d (ScopeT tu) = showString "ScopeT " . showsPrec (d+1) tu--instance (Functor t, Functor f) => Functor (ScopeT t n f) where-  fmap f (ScopeT tu) = ScopeT (fmap (bimap (fmap f) f) tu)--instance (Foldable t, Foldable f) => Foldable (ScopeT t n f) where-  foldr f z (ScopeT tu) = foldr (flip (bifoldr (flip (foldr f)) f)) z tu--instance (Traversable t, Traversable f) => Traversable (ScopeT t n f) where-  traverse f (ScopeT tu) = fmap ScopeT (traverse (bitraverse (traverse f) f) tu)--type instance BlankFunctor (ScopeT t n f) = f-type instance BlankInfo (ScopeT t n f) = n-type instance BlankCodomain (ScopeT t n f) = RightAdjunct t--instance RightAdjunction t => BlankEmbed (ScopeT t n f) where-  blankEmbed = scopeTEmbed--instance (RightAdjunctionApplicative t, Functor f) => BlankAbstract (ScopeT t n f) where-  blankFree = scopeTFree-  blankAbstract = scopeTAbstract-  blankUnAbstract = scopeTUnAbstract-  blankInstantiate = scopeTInstantiate-  blankApply = scopeTApply--scopeTWrap :: RightAdjunction t => UnderScope n f (ScopeT t n f a) a -> RightAdjunct t (ScopeT t n f a)-scopeTWrap = fmap ScopeT . unit--scopeTBound :: RightAdjunction t => Int -> RightAdjunct t (ScopeT t n f a)-scopeTBound = scopeTWrap . UnderBoundScope . BoundScope--scopeTFree :: RightAdjunction t => a -> RightAdjunct t (ScopeT t n f a)-scopeTFree = scopeTWrap . UnderFreeScope . FreeScope--scopeTBinder :: RightAdjunction t => Int -> n -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)-scopeTBinder r n e = scopeTWrap (UnderBinderScope (BinderScope r n e))--scopeTEmbed :: RightAdjunction t => f (ScopeT t n f a) -> RightAdjunct t (ScopeT t n f a)-scopeTEmbed fe = fmap ScopeT (unit (UnderEmbedScope (EmbedScope fe)))--scopeTShiftN :: (Functor t, Functor f) => Int -> Int -> ScopeT t n f a -> ScopeT t n f a-scopeTShiftN c d (ScopeT tu) = ScopeT (fmap (underScopeShift scopeTShiftN c d) tu)--scopeTShift :: (Functor t, Functor f) => Int -> ScopeT t n f a -> ScopeT t n f a-scopeTShift = scopeTShiftN 0--scopeTBindOptN :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> Int -> ScopeT t n f a -> ScopeT t n f a-scopeTBindOptN f = scopeTModOpt . go where-  go i us =-    case us of-      UnderBoundScope _ -> Nothing-      UnderFreeScope (FreeScope a) -> fmap (fmap (scopeTShift i)) (f a)-      UnderBinderScope (BinderScope r x e) -> Just (scopeTBinder r x (scopeTBindOptN f (i + r) e))-      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTBindOptN f i) fe))--scopeTBindOpt :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a-scopeTBindOpt f = scopeTBindOptN f 0--scopeTBindN :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> Int -> ScopeT t n f a -> ScopeT t n f b-scopeTBindN f = scopeTMod . go where-  go i us =-    case us of-      UnderBoundScope (BoundScope b) -> scopeTBound b-      UnderFreeScope (FreeScope a) -> fmap (scopeTShift i) (f a)-      UnderBinderScope (BinderScope r x e) -> scopeTBinder r x (scopeTBindN f (i + r) e)-      UnderEmbedScope (EmbedScope fe) -> scopeTEmbed (fmap (scopeTBindN f i) fe)--scopeTBind :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> ScopeT t n f a -> ScopeT t n f b-scopeTBind f = scopeTBindN f 0--subScopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => Int -> n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)-subScopeTAbstract r n ks e =-  let f = fmap scopeTBound . flip Seq.elemIndexL ks-      e' = scopeTBindOpt f e-  in scopeTBinder r n e'--scopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)-scopeTAbstract n ks =-  let r = Seq.length ks-  in subScopeTAbstract r n ks . scopeTShift r--scopeTUnAbstract :: (RightAdjunctionApplicative t, Functor f) => Seq a -> ScopeT t n f a -> ScopeT t n f a-scopeTUnAbstract ks = scopeTInstantiate (fmap scopeTFree ks)--scopeTModOpt :: RightAdjunctionApplicative t => (UnderScope n f (ScopeT t n f a) a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a-scopeTModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeT s)--scopeTModM :: (RightAdjunctionApplicative t, Traversable m) => (UnderScope n f (ScopeT t n f a) a -> m (RightAdjunct t x)) -> ScopeT t n f a -> m x-scopeTModM f = rightAdjunct (sequenceA . f) . unScopeT--scopeTMod :: RightAdjunction t => (UnderScope n f (ScopeT t n f a) a -> RightAdjunct t x) -> ScopeT t n f a -> x-scopeTMod f = rightAdjunct f . unScopeT--scopeTInstantiateN :: (RightAdjunctionApplicative t, Functor f) => Int -> Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a-scopeTInstantiateN h vs = scopeTModOpt (go h vs) where-  go i ws us =-    case us of-      UnderBoundScope (BoundScope b) -> vs Seq.!? (b - i)-      UnderFreeScope _ -> Nothing-      UnderBinderScope (BinderScope r n e) ->-        let ws' = fmap (fmap (scopeTShift r)) ws-            e' = scopeTInstantiateN (r + i) ws' e-        in Just (scopeTBinder r n e')-      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTInstantiateN i ws) fe))--scopeTInstantiate :: (RightAdjunctionApplicative t,  Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a-scopeTInstantiate = scopeTInstantiateN 0--scopeTApply :: (RightAdjunctionApplicative t, Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> Either SubError (ScopeT t n f a)-scopeTApply vs = scopeTModM go where-  go us =-    case us of-      UnderBinderScope (BinderScope r _ e) ->-        let len = Seq.length vs-        in if len == r-              then Right (pure (scopeTShift (-1) (scopeTInstantiate vs e)))-              else Left (ApplyError len r)-      _ -> Left NonBinderError--type ScopeTRawFold t n f a r = UnderScopeFold n f (ScopeT t n f a) a r-type ScopeTFold t n f a r = ScopeTRawFold t n f a (RightAdjunct t r)--scopeTRawFold :: Functor t => ScopeTRawFold t n f a r -> ScopeT t n f a -> t r-scopeTRawFold usf = fmap (underScopeFold usf) . unScopeT--scopeTFold :: RightAdjunction t => ScopeTFold t n f a r -> ScopeT t n f a -> r-scopeTFold usf = counit . scopeTRawFold usf--scopeTLiftAnno :: Functor t => t a -> ScopeT t n f a-scopeTLiftAnno ta = ScopeT (fmap underScopePure ta)--scopeTHoistAnno :: (Functor t, Functor f) => (forall x. t x -> w x) -> ScopeT t n f a -> ScopeT w n f a-scopeTHoistAnno nat (ScopeT tu) = ScopeT (nat (fmap (first (scopeTHoistAnno nat)) tu))

@@ -0,0 +1,188 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Internals. You'd need to newtype 'ScopeW' to implement your own 'Blank'.+module Blanks.ScopeW+  ( ScopeC+  , ScopeW (..)+  , ScopeWRawFold+  , ScopeWFold+  , scopeWFree+  , scopeWEmbed+  , scopeWAbstract+  , scopeWUnAbstract+  , scopeWInstantiate+  , scopeWApply+  , scopeWBind+  , scopeWBindOpt+  , scopeWLift+  , scopeWRawFold+  , scopeWFold+  , scopeWLiftAnno+  , scopeWHoistAnno+  , scopeWMapAnno+  ) where++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 Data.Bifoldable (bifoldr)+import Data.Bifunctor (bimap, first)+import Data.Bitraversable (bitraverse)+import Data.Functor.Adjunction (Adjunction (..))+import Data.Maybe (fromMaybe)+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq++-- * ScopeW, patterns, and instances++newtype ScopeW t n f g a = ScopeW+  { unScopeW :: t (UnderScope n f (g a) a)+  }++instance Eq (t (UnderScope n f (g a) a)) => Eq (ScopeW t n f g a) where+  ScopeW tu == ScopeW tv = tu == tv++instance Show (t (UnderScope n f (g a) a)) => Show (ScopeW t n f g a) where+  showsPrec d (ScopeW tu) = showString "ScopeW " . showsPrec (d+1) tu++instance (Functor t, Functor f, Functor g) => Functor (ScopeW t n f g) where+  fmap f (ScopeW tu) = ScopeW (fmap (bimap (fmap f) f) tu)++instance (Foldable t, Foldable f, Foldable g) => Foldable (ScopeW t n f g) where+  foldr f z (ScopeW tu) = foldr (flip (bifoldr (flip (foldr f)) f)) z tu++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)++-- * Smart constructors, shift, and bind++scopeWMod :: ScopeC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x+scopeWMod f = rightAdjunct f . unScopeW . natNewtypeFrom++scopeWModOpt :: ScopeC 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))++scopeWModM :: (ScopeC 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++scopeWBound :: ScopeC 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 a = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeFree a))++scopeWShift :: ScopeC t u n f g => Int -> g a -> g a+scopeWShift = scopeWShiftN 0++scopeWShiftN :: ScopeC 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 r n e = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBinder r n e))++scopeWEmbed :: ScopeC 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 f = scopeWBindN f 0++scopeWBindN :: ScopeC 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+      UnderScopeBound b -> scopeWBound b+      UnderScopeFree a -> fmap (scopeWShift i) (f a)+      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 f = scopeWBindOptN f 0++scopeWBindOptN :: ScopeC 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+      UnderScopeBound _ -> Nothing+      UnderScopeFree a -> fmap (fmap (scopeWShift i)) (f a)+      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 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 =+  let r = Seq.length ks+  in subScopeWAbstract r n ks . scopeWShift r++scopeWUnAbstract :: ScopeC t u n f g => Seq a -> g a -> g a+scopeWUnAbstract ks = scopeWInstantiate (fmap scopeWFree ks)++scopeWInstantiate :: ScopeC t u n f g => Seq (u (g a)) -> g a -> g a+scopeWInstantiate = scopeWInstantiateN 0++scopeWInstantiateN :: ScopeC 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+      UnderScopeBound b -> vs Seq.!? (b - i)+      UnderScopeFree _ -> Nothing+      UnderScopeBinder r n e ->+        let vs' = fmap (fmap (scopeWShift r)) vs+            e' = scopeWInstantiateN (r + i) vs' e+        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 vs = scopeWModM go where+  go us =+    case us of+      UnderScopeBinder r _ e ->+        let len = Seq.length vs+        in if len == r+              then Right (pure (scopeWShift (-1) (scopeWInstantiate vs e)))+              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++-- * Annotation functions++scopeWLiftAnno :: (NatNewtype (ScopeW t n f g) g, Functor t) => t a -> g a+scopeWLiftAnno = natNewtypeTo . ScopeW . fmap UnderScopeFree++scopeWHoistAnno :: (NatNewtype (ScopeW t n f g) g, NatNewtype (ScopeW w n f h) h, Functor t, Functor w, Functor f) => (forall x. t x -> w x) -> g a -> h a+scopeWHoistAnno nat ga =+  let ScopeW tu = natNewtypeFrom ga+      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 f = scopeWMod go where+  go us = case us of+    UnderScopeBound b -> scopeWBound b+    UnderScopeFree a -> fmap (natNewtypeTo . ScopeW . fmap UnderScopeFree . f) (unit a)+    UnderScopeBinder r x e -> scopeWBinder r x (scopeWMapAnno f e)+    UnderScopeEmbed fe -> scopeWEmbed (fmap (scopeWMapAnno f) fe)

@@ -1,37 +1,32 @@ module Blanks.Sub-  ( Sub (..)-  , SubError (..)+  ( SubError (..)   , ThrowSub (..)   , rethrowSub-  , runSub   ) where -import Control.Exception (Exception)-import Control.Monad.Except (Except, MonadError (..), runExcept)-import Data.Typeable (Typeable)+import Control.Exception (Exception, throwIO) +-- | Errors that happen in the course of instantiation, thrown by 'blankApply'+-- and related functions. data SubError   = ApplyError !Int !Int   | UnboundError !Int   | NonBinderError-  deriving (Eq, Show, Typeable)+  deriving (Eq, Show)  instance Exception SubError +-- | Some monadic context that lets you throw a 'SubError'.+-- Exists to let you rethrow to a more convenient context rather than+-- pattern maching. class ThrowSub m where   throwSub :: SubError -> m a  rethrowSub :: (Applicative m, ThrowSub m) => Either SubError a -> m a rethrowSub = either throwSub pure -newtype Sub a =-  Sub-    { unSub :: Except SubError a-    }-  deriving (Functor, Applicative, Monad, Foldable, Traversable)--instance ThrowSub Sub where-  throwSub = Sub . throwError+instance ThrowSub (Either SubError) where+  throwSub = Left -runSub :: Sub a -> Either SubError a-runSub = runExcept . unSub+instance ThrowSub IO where+  throwSub = throwIO

@@ -1,3 +1,4 @@+-- | Internals. You will probably never need these. module Blanks.UnderScope   ( BinderScope (..)   , BoundScope (..)@@ -5,9 +6,11 @@   , FreeScope (..)   , UnderScope (..)   , UnderScopeFold (..)+  , pattern UnderScopeBound+  , pattern UnderScopeFree+  , pattern UnderScopeBinder+  , pattern UnderScopeEmbed   , underScopeFold-  , underScopeFoldContraMap-  , underScopePure   , underScopeShift   ) where @@ -31,7 +34,7 @@   BinderScope     { binderScopeArity :: !Int     , binderScopeInfo :: !n-    , binderScopeBody :: !e+    , binderScopeBody :: e     }   deriving (Eq, Show, Functor, Foldable, Traversable) @@ -48,6 +51,20 @@   | UnderEmbedScope !(EmbedScope f e)   deriving (Eq, Show, Functor) +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))@@ -66,9 +83,6 @@   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) -underScopePure :: a -> UnderScope n f e a-underScopePure = UnderFreeScope . FreeScope- 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@@ -96,9 +110,3 @@     UnderFreeScope x -> free x     UnderBinderScope x -> binder x     UnderEmbedScope x -> embed x--underScopeFoldContraMap :: Functor f => (x -> e) -> UnderScopeFold n f e a r -> UnderScopeFold n f x a r-underScopeFoldContraMap f (UnderScopeFold bound free binder embed) = UnderScopeFold bound free binder' embed' where-  binder' (BinderScope r n x) = binder (BinderScope r n (f x))-  embed' (EmbedScope fx) = embed (EmbedScope (fmap f fx))-

@@ -0,0 +1,10 @@+module Main+  ( main+  ) where++import Test.Blanks.LocScopeTest (testLocScope)+import Test.Blanks.ScopeTest (testScope)+import Test.Tasty (defaultMain, testGroup)++main :: IO ()+main = defaultMain (testGroup "Blanks" [testScope, testLocScope])

@@ -1,1 +0,0 @@-{-# OPTIONS_GHC -F -pgmF tasty-discover #-}

@@ -1,87 +0,0 @@-module Test.Blanks.BlanksTest where--import Blanks-import Control.Monad.Identity (Identity (..))-import Data.Set (Set)-import qualified Data.Set as Set-import Test.Blanks.Assertions ((@/=))-import Test.Tasty-import Test.Tasty.HUnit--type BareScope = PureScope (NameOnly Char) Identity Char--abst :: Char -> BareScope -> BareScope-abst a = runIdentity . blankAbstract1 (Name a ()) a--bound :: Int -> BareScope-bound = PureScope . ScopeT . pure . UnderBoundScope . BoundScope--var :: Char -> BareScope-var = pure--freeVars :: BareScope -> Set Char-freeVars = foldMap Set.singleton--test_sub :: TestTree-test_sub =-  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 =-        testCase "eq" $ do-          svar @?= svar-          svar @/= svar2-          sid @?= abst 'x' (var 'x')-          sid @?= abst 'y' (var 'y')-          sid @/= abst 'x' (var 'y')-          sid @/= abst 'y' (var 'x')-          sid @/= svar--      testFreeVars =-        testCase "free vars" $ do-          freeVars svar @?= Set.singleton 'x'-          freeVars sbound @?= Set.empty-          freeVars sfree @?= Set.singleton 'x'-          freeVars sfree2 @?= Set.singleton 'x'-          freeVars sid @?= Set.empty-          freeVars swonky @?= Set.empty-          freeVars sconst @?= Set.empty-          freeVars sflip @?= Set.empty-          freeVars svar2 @=? Set.singleton 'e'-          freeVars swonky2 @?= Set.singleton 'e'--      testInstantiate =-        testCase "instantiate" $ do-          blankInstantiate1 (pure svar2) svar @?= svar-          blankInstantiate1 (pure svar2) sbound @?= svar2-          blankInstantiate1 (pure svar2) sid @?= sid-          blankInstantiate1 (pure svar2) swonky @?= swonky2--      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--      testVarSub =-        testCase "var sub" $ do-          (svar >>= const svar2) @?= svar2-          (sfree >>= const svar2) @?= abst 'y' svar2-          (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)--      testIdSub =-        testCase "id sub" $ do-          (svar >>= const sid) @?= sid-          (sfree >>= const sid) @?= abst 'y' sid-          (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)--   in testGroup "sub" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]

@@ -0,0 +1,159 @@+module Test.Blanks.LocScopeTest where++import Blanks+import Data.String (IsString)+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 (Eq, Show, Ord, IsString)++-- 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 (Eq, Show, Functor, Foldable, Traversable)++-- 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+  let namelessExp = 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))+    ]

@@ -0,0 +1,75 @@+module Test.Blanks.Parsing where++import Control.Applicative (Alternative (..))+import Control.Exception (throwIO)+import Data.Void (Void)+import qualified Text.Megaparsec as MP+import qualified Text.Megaparsec.Char as MPC+import qualified Text.Megaparsec.Char.Lexer as MPCL++type Parser = MP.Parsec Void String++-- The parser is not the SUT here, so if it fails,+-- so does the test. We ensure valid input.+runParserIO :: Parser a -> String -> IO a+runParserIO p s =+  case MP.runParser p "<test>" s of+    Left e -> throwIO e+    Right a -> pure a++data SourceSpan = SourceSpan+  { _ssName :: !FilePath+  , _ssStartLine :: !MP.Pos+  , _ssStartColumn :: !MP.Pos+  , _ssEndLine :: !MP.Pos+  , _ssEndColumn :: !MP.Pos+  } deriving (Eq, Show, Ord)++mkSourceSpan :: MP.SourcePos -> MP.SourcePos -> SourceSpan+mkSourceSpan (MP.SourcePos n sl sc) (MP.SourcePos _ el ec) = SourceSpan n sl sc el ec++around :: (SourceSpan -> a -> b) -> Parser a -> Parser b+around f pa = (\s a e -> f (mkSourceSpan s e) a) <$> MP.getSourcePos <*> pa <*> MP.getSourcePos++around2 :: (SourceSpan -> a -> b -> c) -> Parser (a, b) -> Parser c+around2 f pab = (\s (a, b) e -> f (mkSourceSpan s e) a b) <$> MP.getSourcePos <*> pab <*> MP.getSourcePos++around3 :: (SourceSpan -> a -> b -> c -> d) -> Parser (a, b, c) -> Parser d+around3 f pabc = (\s (a, b, c) e -> f (mkSourceSpan s e) a b c) <$> MP.getSourcePos <*> pabc <*> MP.getSourcePos++double :: Parser a -> Parser (a, a)+double p = (,) <$> p <*> p++triple :: Parser a -> Parser (a, a, a)+triple p = (,,) <$> p <*> p <*> p++spaceConsumer :: Parser ()+spaceConsumer = MPCL.space MPC.space1 lineCmnt blockCmnt+  where+    lineCmnt = MPCL.skipLineComment ";"+    blockCmnt = MPCL.skipBlockComment "#|" "|#"++lexeme :: Parser a -> Parser a+lexeme = MPCL.lexeme spaceConsumer++symbol :: String -> Parser String+symbol = MPCL.symbol spaceConsumer++parens :: Parser a -> Parser a+parens = MP.between (symbol "(") (symbol ")")++nonDelimPred :: Char -> Bool+nonDelimPred c = c /= '(' && c /= ')' && c /= ' ' && c /= '\t' && c /= '\n'++identifier :: Parser String+identifier = lexeme (MP.takeWhile1P Nothing nonDelimPred)++-- Take the first successful result, backtracking on failure.+branch :: [Parser a] -> Parser a+branch xs =+  case xs of+    [] -> empty+    x:xs' -> MP.try x <|> branch xs'++signed :: Parser Int+signed = MPCL.signed spaceConsumer (lexeme MPCL.decimal)

@@ -0,0 +1,89 @@+module Test.Blanks.ScopeTest+  ( testScope+  ) where++import Blanks+import Control.Monad.Identity (Identity (..))+import Data.Set (Set)+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++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 =+        testCase "eq" $ do+          svar @?= svar+          svar @/= svar2+          sid @?= abst 'x' (var 'x')+          sid @?= abst 'y' (var 'y')+          sid @/= abst 'x' (var 'y')+          sid @/= abst 'y' (var 'x')+          sid @/= svar++      testFreeVars =+        testCase "free vars" $ do+          freeVars svar @?= Set.singleton 'x'+          freeVars sbound @?= Set.empty+          freeVars sfree @?= Set.singleton 'x'+          freeVars sfree2 @?= Set.singleton 'x'+          freeVars sid @?= Set.empty+          freeVars swonky @?= Set.empty+          freeVars sconst @?= Set.empty+          freeVars sflip @?= Set.empty+          freeVars svar2 @=? Set.singleton 'e'+          freeVars swonky2 @?= Set.singleton 'e'++      testInstantiate =+        testCase "instantiate" $ do+          blankInstantiate1 (pure svar2) svar @?= svar+          blankInstantiate1 (pure svar2) sbound @?= svar2+          blankInstantiate1 (pure svar2) sid @?= sid+          blankInstantiate1 (pure svar2) swonky @?= swonky2++      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++      testVarSub =+        testCase "var sub" $ do+          (svar >>= const svar2) @?= svar2+          (sfree >>= const svar2) @?= abst 'y' svar2+          (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)++      testIdSub =+        testCase "id sub" $ do+          (svar >>= const sid) @?= sid+          (sfree >>= const sid) @?= abst 'y' sid+          (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)++   in testGroup "Scope" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]