packages feed

blanks (empty) → 0.3.0

raw patch · 17 files changed

+813/−0 lines, 17 filesdep +adjunctionsdep +basedep +blankssetup-changed

Dependencies added: adjunctions, base, blanks, containers, distributive, mtl, tasty, tasty-discover, tasty-hunit

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Eric Conlon (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Eric Conlon nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,5 @@+# blanks++[![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!)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,5 @@+module Main where++-- TODO(ejconlon) Create demo app+main :: IO ()+main = pure ()
+ blanks.cabal view
@@ -0,0 +1,92 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 6dd5dac29a7eb8991e9d2728daa61f8651bf8e283305aa1063f1daf4dce65fd8++name:           blanks+version:        0.3.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+homepage:       https://github.com/ejconlon/blanks#readme+bug-reports:    https://github.com/ejconlon/blanks/issues+author:         Eric Conlon+maintainer:     ejconlon@gmail.com+copyright:      (c) 2019 Eric Conlon+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md++source-repository head+  type: git+  location: https://github.com/ejconlon/blanks++library+  exposed-modules:+      Blanks+      Blanks.Class+      Blanks.LocScope+      Blanks.Name+      Blanks.PureScope+      Blanks.RightAdjunct+      Blanks.ScopeT+      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+  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+    , base >=4.12 && <5+    , blanks+    , containers >=0.6+    , distributive >=0.6+    , mtl >=2.2+  default-language: Haskell2010++test-suite blanks-test+  type: exitcode-stdio-1.0+  main-is: Tasty.hs+  other-modules:+      Test.Blanks.Assertions+      Test.Blanks.BlanksTest+      Paths_blanks+  hs-source-dirs:+      test+  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+    , base >=4.12 && <5+    , blanks+    , containers >=0.6+    , distributive >=0.6+    , mtl >=2.2+    , tasty+    , tasty-discover+    , tasty-hunit+  default-language: Haskell2010
+ src/Blanks.hs view
@@ -0,0 +1,12 @@+module Blanks+  ( module Blanks+  ) where++import Blanks.Class 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.Sub as Blanks+import Blanks.UnderScope as Blanks
+ src/Blanks/Class.hs view
@@ -0,0 +1,53 @@+{-# 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
+ src/Blanks/LocScope.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE UndecidableInstances #-}++module Blanks.LocScope+  ( Colocated (..)+  , Located (..)+  , LocScope (..)+  , LocScopeRawFold+  , LocScopeFold+  , askColocated+  , colocated+  , locScopeBind+  , locScopeEmbed+  , locScopeRawFold+  , locScopeFold+  , locScopeFree+  , runColocated+  ) where++import Blanks.Class+import Blanks.RightAdjunct (RightAdjunct)+import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFold, scopeTFree, scopeTRawFold)+import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)+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)++data Located l a = Located+  { _locatedLoc :: !l+  , _locatedVal :: !a+  } deriving (Eq, Show, Functor, Foldable, Traversable)++newtype Colocated l a = Colocated+  { unColocated :: Reader l a+  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)++type instance RightAdjunct (Located l) = Colocated l++colocated :: (l -> a) -> Colocated l a+colocated f = Colocated (ReaderT (Identity . 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++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++instance Functor f => BlankEmbed (LocScope l n f) where+  blankEmbed = locScopeEmbed++instance (Eq (f (ScopeT (Located 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++locScopeFold :: Functor f => LocScopeFold l n f a r -> LocScope l n f a -> r+locScopeFold usf = scopeTFold (underScopeFoldContraMap LocScope usf) . unLocScope
+ src/Blanks/Name.hs view
@@ -0,0 +1,16 @@+module Blanks.Name+  ( Name (..)+  , NameOnly+  ) where++data Name n a =+  Name+    { nameKey :: n+    , nameValue :: a+    }+  deriving (Show, Functor, Foldable, Traversable)++instance Eq a => Eq (Name n a) where+  Name _ x == Name _ y = x == y++type NameOnly n = Name n ()
+ src/Blanks/PureScope.hs view
@@ -0,0 +1,55 @@+{-# 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
+ src/Blanks/RightAdjunct.hs view
@@ -0,0 +1,20 @@+{-# 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))
+ src/Blanks/ScopeT.hs view
@@ -0,0 +1,171 @@+{-# 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))
+ src/Blanks/Sub.hs view
@@ -0,0 +1,37 @@+module Blanks.Sub+  ( Sub (..)+  , SubError (..)+  , ThrowSub (..)+  , rethrowSub+  , runSub+  ) where++import Control.Exception (Exception)+import Control.Monad.Except (Except, MonadError (..), runExcept)+import Data.Typeable (Typeable)++data SubError+  = ApplyError !Int !Int+  | UnboundError !Int+  | NonBinderError+  deriving (Eq, Show, Typeable)++instance Exception SubError++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++runSub :: Sub a -> Either SubError a+runSub = runExcept . unSub
+ src/Blanks/UnderScope.hs view
@@ -0,0 +1,104 @@+module Blanks.UnderScope+  ( BinderScope (..)+  , BoundScope (..)+  , EmbedScope (..)+  , FreeScope (..)+  , UnderScope (..)+  , UnderScopeFold (..)+  , underScopeFold+  , underScopeFoldContraMap+  , underScopePure+  , underScopeShift+  ) where++import Data.Bifoldable (Bifoldable (..))+import Data.Bifunctor (Bifunctor (..))+import Data.Bitraversable (Bitraversable (..))++newtype BoundScope =+  BoundScope+    { unBoundScope :: Int+    }+  deriving (Eq, Show)++newtype FreeScope a =+  FreeScope+    { unFreeScope :: a+    }+  deriving (Eq, Show, Functor, Foldable, Traversable)++data BinderScope n e =+  BinderScope+    { binderScopeArity :: !Int+    , binderScopeInfo :: !n+    , binderScopeBody :: !e+    }+  deriving (Eq, Show, Functor, Foldable, Traversable)++newtype EmbedScope f e =+  EmbedScope+    { unEmbedScope :: f e+    }+  deriving (Eq, Show, Functor)++data UnderScope n f e a+  = UnderBoundScope !BoundScope+  | UnderFreeScope !(FreeScope a)+  | UnderBinderScope !(BinderScope n e)+  | UnderEmbedScope !(EmbedScope f e)+  deriving (Eq, Show, Functor)++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)++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+    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++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))+
+ test/Tasty.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}
+ test/Test/Blanks/Assertions.hs view
@@ -0,0 +1,25 @@+module Test.Blanks.Assertions where++import Control.Monad (unless)+import Test.Tasty.HUnit (Assertion, HasCallStack, assertFailure)++assertPredicate :: (Show a, HasCallStack) => (a -> a -> Bool) -> String -> a -> a -> Assertion+assertPredicate predicate preface left right = unless (predicate left right) (assertFailure msg)+  where+    msg =+      (if null preface+         then ""+         else preface ++ "\n") +++      "left: " ++ show left ++ "\n right: " ++ show right++assertNotEqual :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion+assertNotEqual = assertPredicate (/=) "Expected not equal"++assertTrue :: HasCallStack => Bool -> Assertion+assertTrue a = assertPredicate (==) "Expected True" a True++assertFalse :: HasCallStack => Bool -> Assertion+assertFalse a = assertPredicate (==) "Expected False" a False++(@/=) :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion+(@/=) = assertNotEqual
+ test/Test/Blanks/BlanksTest.hs view
@@ -0,0 +1,87 @@+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]