diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -19,6 +19,5 @@ bound variables), but if you stick to the provided combinators, things will work out fine. You'll get most of what you want by just importing this module unqualified. -See the `Blanks` class definition and related methods to manipulate variables and abstractions. See `Scope` for the basic wrapper and `LocScope` for a wrapper with annotations you can use for source locations and the like. See the test suite for examples. diff --git a/blanks.cabal b/blanks.cabal --- a/blanks.cabal +++ b/blanks.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: bce7c1157ad17dfb08bdd82fd1d9cef7f5aead112c1349019b6dbfed38de7959 +-- hash: 3e66404b6e808993a99490ba1327e8e872e5dee4cfb34980b7cd5f84ce47aba6 name: blanks -version: 0.4.2 +version: 0.5.0 synopsis: Fill-in-the-blanks - A library factoring out substitution from ASTs description: Please see the README on GitHub at category: Language @@ -29,20 +29,23 @@ library exposed-modules: Blanks - Blanks.Interface + Blanks.Conversion + Blanks.Core Blanks.Located Blanks.LocScope Blanks.Name Blanks.NatNewtype Blanks.Scope Blanks.ScopeW + Blanks.Split Blanks.Sub - Blanks.UnderScope + Blanks.Tracked + Blanks.Under other-modules: Paths_blanks hs-source-dirs: src - default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies + default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds build-depends: adjunctions >=4.4 && <5 @@ -58,13 +61,18 @@ main-is: Main.hs other-modules: Test.Blanks.Assertions - Test.Blanks.LocScopeTest + Test.Blanks.Exp + Test.Blanks.ExpTest Test.Blanks.Parsing Test.Blanks.ScopeTest + Test.Blanks.SimpleScope + Test.Blanks.SplitScope + Test.Blanks.SplitTest + Test.Blanks.TrackedTest Paths_blanks hs-source-dirs: test - default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies + default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N build-depends: adjunctions >=4.4 && <5 diff --git a/src/Blanks.hs b/src/Blanks.hs --- a/src/Blanks.hs +++ b/src/Blanks.hs @@ -1,14 +1,17 @@ -- | You'll get most of what you want by just importing this module unqualified. --- See the 'Blanks' class definition and related methods to manipulate variables and abstractions. -- See 'Scope' for the basic wrapper and 'LocScope' for a wrapper with annotations you can use -- for source locations and the like. See the test suite for examples. module Blanks ( module Blanks + , BinderScope (..) ) where -import Blanks.Interface as Blanks +import Blanks.Conversion as Blanks +import Blanks.Core (BinderScope (..)) import Blanks.Located as Blanks import Blanks.LocScope as Blanks import Blanks.Name as Blanks import Blanks.Scope as Blanks +import Blanks.Split as Blanks import Blanks.Sub as Blanks +import Blanks.Tracked as Blanks diff --git a/src/Blanks/Conversion.hs b/src/Blanks/Conversion.hs new file mode 100644 --- /dev/null +++ b/src/Blanks/Conversion.hs @@ -0,0 +1,27 @@ +module Blanks.Conversion + ( locScopeForget + , scopeAnno + ) where + +import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, + pattern LocScopeFree) +import Blanks.Scope (Scope, pattern ScopeBinder, pattern ScopeBound, pattern ScopeEmbed, pattern ScopeFree) + +-- | Forget all the annotations and yield a plain 'Scope'. +locScopeForget :: Functor f => LocScope l n f a -> Scope n f a +locScopeForget ls = + case ls of + LocScopeBound _ b -> ScopeBound b + LocScopeFree _ a -> ScopeFree a + LocScopeBinder _ r x e -> ScopeBinder r x (locScopeForget e) + LocScopeEmbed _ fe -> ScopeEmbed (fmap locScopeForget fe) + +-- | Annotate every location in the 'Scope' with a given value as a 'LocScope'. +scopeAnno :: Functor f => l -> Scope n f a -> LocScope l n f a +scopeAnno l = go where + go s = + case s of + ScopeBound b -> LocScopeBound l b + ScopeFree a -> LocScopeFree l a + ScopeBinder r x e -> LocScopeBinder l r x (go e) + ScopeEmbed fe -> LocScopeEmbed l (fmap go fe) diff --git a/src/Blanks/Core.hs b/src/Blanks/Core.hs new file mode 100644 --- /dev/null +++ b/src/Blanks/Core.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE DeriveAnyClass #-} + +-- | Internals. +module Blanks.Core + ( BoundScope (..) + , FreeScope (..) + , BinderScope (..) + , EmbedScope (..) + ) where + +import Control.DeepSeq (NFData) +import GHC.Generics (Generic) + +newtype BoundScope = + BoundScope + { unBoundScope :: Int + } + deriving newtype (Eq, Show, NFData) + +newtype FreeScope a = + FreeScope + { unFreeScope :: a + } + deriving stock (Eq, Show, Functor, Foldable, Traversable) + deriving newtype (NFData) + +data BinderScope n e = + BinderScope + { binderScopeArity :: !Int + , binderScopeInfo :: !n + , binderScopeBody :: e + } + deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) + deriving anyclass (NFData) + +newtype EmbedScope f e = + EmbedScope + { unEmbedScope :: f e + } + deriving newtype (Eq, Show, Functor, NFData) diff --git a/src/Blanks/Interface.hs b/src/Blanks/Interface.hs deleted file mode 100644 --- a/src/Blanks/Interface.hs +++ /dev/null @@ -1,209 +0,0 @@ -module Blanks.Interface - ( Blank - , BlankLeft - , BlankRight - , BlankInfo - , BlankFunctor - , BlankRawFold - , BlankFold - , BlankPair - , blankFree - , blankEmbed - , blankAbstract - , blankAbstract1 - , blankUnAbstract - , blankUnAbstract1 - , blankInstantiate - , blankInstantiate1 - , blankApply - , blankApply1 - , blankApplyThrow - , blankApply1Throw - , blankBind - , blankBindOpt - , blankLift - , blankRawFold - , blankFold - , blankLiftAnno - , blankHoistAnno - , blankMapAnno - ) where - -import Blanks.NatNewtype (NatNewtype) -import Blanks.ScopeW -import Blanks.Sub (SubError, ThrowSub, rethrowSub) -import Blanks.UnderScope (UnderScopeFold) -import Data.Functor.Adjunction (Adjunction) -import Data.Kind (Type) -import Data.Sequence (Seq) -import qualified Data.Sequence as Seq - --- | The left adjoint functor used by 'g'. -type family BlankLeft (g :: Type -> Type) :: Type -> Type - --- | The right adjoint functor used by 'g' -type family BlankRight (g :: Type -> Type) :: Type -> Type - --- | The binder info used by 'g'. -type family BlankInfo (g :: Type -> Type) :: Type - --- | The expression functor used by 'g'. -type family BlankFunctor (g :: Type -> Type) :: Type -> Type - -type BlankRawFold (g :: Type -> Type) (a :: Type) (r :: Type) = UnderScopeFold (BlankInfo g) (BlankFunctor g) (g a) a r -type BlankFold (g :: Type -> Type) (a :: Type) (r :: Type) = BlankRawFold g a (BlankRight g r) - --- | Indicates that 'g' is a "scope" functor we can use for name-binding. (Behind-the-scenes, 'g' must --- be a newtype wrapper over the 'ScopeW' datatype.) Most of the time you will use 'Scope' or 'LocScope' --- directly, which are instances of this class. --- --- We use the pair of adjoint functors indexed by 'g' to shift the burden of operating in context --- where it is more convenient. For example, 'LocScope' uses a pair of functors that are --- essentially 'Env' and 'Reader'. The left adjoint 'Env' lets us annotate every level of our --- expression tree with a location, and the right adjoint 'Reader' informs us of that location --- so we don't have to make one up out of thin air! --- --- 'Scope' uses the pair of functors 'Identity' and 'Identity', which means there is --- no ability to store any additional information in the tree, but there's also no additional --- burden to provide that information. -class - ( Adjunction (BlankLeft g) (BlankRight g) - , Applicative (BlankRight g) - , Functor (BlankFunctor g) - , NatNewtype (ScopeW (BlankLeft g) (BlankInfo g) (BlankFunctor g) g) g - ) => Blank (g :: Type -> Type) - --- | A pair of 'Blank' functors that index the same info and embedded functors. Used to change adjoint functors. -type BlankPair g h = (Blank g, Blank h, BlankInfo g ~ BlankInfo h, BlankFunctor g ~ BlankFunctor h) - --- | Creates a free variable in context. -blankFree :: - Blank g - => a -- ^ The name of the free variable - -> BlankRight g (g a) -blankFree = scopeWFree -{-# INLINE blankFree #-} - --- | Embeds an expression functor in context. -blankEmbed :: - Blank g - => BlankFunctor g (g a) -- ^ An expression - -> BlankRight g (g a) -blankEmbed = scopeWEmbed -{-# INLINE blankEmbed #-} - --- | Binds free variables in an expression and returns a binder. -blankAbstract :: - (Blank g, Eq a) - => BlankInfo g -- ^ Annotation specific to your expression functor. - -- Might contain original variable names and types, or might - -- mark this as a "let" vs a "lambda". - -> Seq a -- ^ Free variables to bind, like the names of function parameters - -> g a -- ^ The expression to bind in, like the body of a function - -> BlankRight g (g a) -blankAbstract = scopeWAbstract -{-# INLINE blankAbstract #-} - --- | 'blankAbstract' for a single argument. -blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a) -blankAbstract1 n k = scopeWAbstract n (Seq.singleton k) -{-# INLINE blankAbstract1 #-} - --- | Un-bind free variables in an expression. Basically the inverse of --- 'blankAbstract'. Take care to match the arity of the binder! ('blankApply' is safer.) -blankUnAbstract :: - Blank g - => Seq a -- ^ The names of the variables you're freeing - -> g a -- ^ The expression to substitutue in (typically a binder) - -> g a -blankUnAbstract = scopeWUnAbstract -{-# INLINE blankUnAbstract #-} - --- 'blankUnAbstract' for a single argument. -blankUnAbstract1 :: Blank g => a -> g a -> g a -blankUnAbstract1 = scopeWUnAbstract . Seq.singleton -{-# INLINE blankUnAbstract1 #-} - --- | Instantiate the bound variables in an expression with other expressions. --- Take care to match the arity of the binder! ('blankApply' is safer.) -blankInstantiate :: - Blank g - => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars - -> g a -- ^ The expression to substitute in (typically a binder) - -> g a -blankInstantiate = scopeWInstantiate -{-# INLINE blankInstantiate #-} - --- | 'blankInstantiate' for a single argument. -blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a -blankInstantiate1 = scopeWInstantiate . Seq.singleton -{-# INLINE blankInstantiate1 #-} - --- | Instantiates the bound variables in an expression with other expressions. --- Throws errors on mismatched arity, non binder expression, unbound vars, etc. --- A version of 'blankInstantiate' that fails loudly instead of silently! -blankApply :: - Blank g - => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars - -> g a -- ^ The binder expression to substitute in - -> Either SubError (g a) -blankApply = scopeWApply -{-# INLINE blankApply #-} - --- | 'blankApply' for a single argument. -blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a) -blankApply1 = scopeWApply . Seq.singleton -{-# INLINE blankApply1 #-} - --- | A 'ThrowSub' version of 'blankApply'. -blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a) -blankApplyThrow ks = rethrowSub . scopeWApply ks -{-# INLINE blankApplyThrow #-} - --- | A 'ThrowSub' version of 'blankApply1'. -blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a) -blankApply1Throw k = rethrowSub . scopeWApply (Seq.singleton k) -{-# INLINE blankApply1Throw #-} - --- | Substitution as a kind of monadic bind. -blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b -blankBind = scopeWBind -{-# INLINE blankBind #-} - --- | Optional substitution as another kind of monadic bind. -blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a -blankBindOpt = scopeWBindOpt -{-# INLINE blankBindOpt #-} - --- | Lift an expression functor into the scope functor. -blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a) -blankLift = scopeWLift -{-# INLINE blankLift #-} - --- | Pattern match all cases of the scope functor. -blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r -blankRawFold = scopeWRawFold -{-# INLINE blankRawFold #-} - --- | Pattern match all cases of the scope functor, and eliminate the adjoints. -blankFold :: Blank g => BlankFold g a r -> g a -> r -blankFold = scopeWFold -{-# INLINE blankFold #-} - --- | Lift a value of your left adjoint functor (annotating the tree) into your --- scope functor. -blankLiftAnno :: Blank g => BlankLeft g a -> g a -blankLiftAnno = scopeWLiftAnno -{-# INLINE blankLiftAnno #-} - --- | Apply a natural transformation to your left adjoint functor (annotating the tree) to --- change scope functors. -blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a -blankHoistAnno = scopeWHoistAnno -{-# INLINE blankHoistAnno #-} - --- | Apply a function to the free variables in scope in the context of the left adjoint functor. --- (Allows you to read annotations when fmapping.) -blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b -blankMapAnno = scopeWMapAnno -{-# INLINE blankMapAnno #-} diff --git a/src/Blanks/LocScope.hs b/src/Blanks/LocScope.hs --- a/src/Blanks/LocScope.hs +++ b/src/Blanks/LocScope.hs @@ -7,34 +7,46 @@ , pattern LocScopeBinder , pattern LocScopeEmbed , locScopeLocation - , locScopeForget + , locScopeFree + , locScopeEmbed + , locScopeFromInnerBinder + , locScopeBind + , locScopeBindOpt + , locScopeLift + , locScopeInnerBinder + , locScopeInnerBinder1 + , locScopeAbstract + , locScopeAbstract1 + , locScopeUnAbstract + , locScopeUnAbstract1 + , locScopeInstantiate + , locScopeInstantiate1 + , locScopeApply + , locScopeApply1 + , locScopeLiftAnno + , locScopeHoistAnno + , locScopeMapAnno ) where -import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankHoistAnno, blankMapAnno) +import Blanks.Core (BinderScope) import Blanks.Located (Colocated, Located (..), askColocated) import Blanks.NatNewtype (NatNewtype) -import Blanks.Scope (Scope (..)) -import Blanks.ScopeW (ScopeW (..)) -import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, - pattern UnderScopeFree) +import Blanks.ScopeW (ScopeW (..), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind, + scopeWBindOpt, scopeWEmbed, scopeWFree, scopeWFromInnerBinder, scopeWHoistAnno, scopeWInnerBinder, + scopeWInnerBinder1, scopeWInstantiate, scopeWInstantiate1, scopeWLift, scopeWLiftAnno, + scopeWMapAnno, scopeWUnAbstract, scopeWUnAbstract1) +import Blanks.Sub (SubError) +import Blanks.Under (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, pattern UnderScopeFree) import Control.DeepSeq (NFData (..)) import Control.Monad (ap) -import Control.Monad.Identity (Identity (..)) import Control.Monad.Writer (MonadWriter (..)) +import Data.Sequence (Seq) -- | A 'Scope' annotated with some information between constructors. --- See 'Blank' for usage, and see the patterns in this module for easy manipulation --- and inspection. newtype LocScope l n f a = LocScope { unLocScope :: ScopeW (Located l) n f (LocScope l n f) a } deriving stock (Functor, Foldable, Traversable) -type instance BlankLeft (LocScope l n f) = Located l -type instance BlankRight (LocScope l n f) = Colocated l -type instance BlankInfo (LocScope l n f) = n -type instance BlankFunctor (LocScope l n f) = f - -instance Functor f => Blank (LocScope l n f) instance NatNewtype (ScopeW (Located l) n f (LocScope l n f)) (LocScope l n f) instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n f a))) => NFData (LocScope l n f a) where @@ -69,14 +81,14 @@ instance (Monoid l, Functor f) => Monad (LocScope l n f) where return = pure - s >>= f = blankBind go s where + s >>= f = locScopeBind go s where go a = fmap (\l1 -> let LocScope (ScopeW (Located l2 b)) = f a in LocScope (ScopeW (Located (l1 <> l2) b))) askColocated instance (Monoid l, Functor f) => MonadWriter l (LocScope l n f) where writer (a, l) = LocScopeFree l a tell l = LocScopeFree l () - listen = blankMapAnno (\(Located l a) -> Located l (a, l)) - pass = blankMapAnno (\(Located l (a, f)) -> Located (f l) a) + listen = locScopeMapAnno (\(Located l a) -> Located l (a, l)) + pass = locScopeMapAnno (\(Located l (a, f)) -> Located (f l) a) instance (Eq (f (LocScope l n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where LocScope su == LocScope sv = su == sv @@ -84,6 +96,84 @@ instance (Show (f (LocScope l n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where showsPrec d (LocScope (ScopeW tu)) = showString "LocScope " . showsPrec (d+1) tu --- | Forget all the annotations and yield a plain 'Scope'. -locScopeForget :: Functor f => LocScope l n f a -> Scope n f a -locScopeForget = blankHoistAnno (\(Located _ a) -> Identity a) +-- * Interface + +locScopeFree :: Functor f => a -> Colocated l (LocScope l n f a) +locScopeFree = scopeWFree +{-# INLINE locScopeFree #-} + +locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a) +locScopeEmbed = scopeWEmbed +{-# INLINE locScopeEmbed #-} + +locScopeFromInnerBinder :: Functor f => BinderScope n (LocScope l n f a) -> Colocated l (LocScope l n f a) +locScopeFromInnerBinder = scopeWFromInnerBinder +{-# INLINE locScopeFromInnerBinder #-} + +locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b +locScopeBind = scopeWBind +{-# INLINE locScopeBind #-} + +locScopeBindOpt :: Functor f => (a -> Maybe (Colocated l (LocScope l n f a))) -> LocScope l n f a -> LocScope l n f a +locScopeBindOpt = scopeWBindOpt +{-# INLINE locScopeBindOpt #-} + +locScopeLift :: Traversable f => f a -> Colocated l (LocScope l n f a) +locScopeLift = scopeWLift +{-# INLINE locScopeLift #-} + +locScopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> BinderScope n (LocScope l n f a) +locScopeInnerBinder = scopeWInnerBinder +{-# INLINE locScopeInnerBinder #-} + +locScopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> BinderScope n (LocScope l n f a) +locScopeInnerBinder1 = scopeWInnerBinder1 +{-# INLINE locScopeInnerBinder1 #-} + +locScopeAbstract :: (Functor f, Eq a) => n -> Seq a -> LocScope l n f a -> Colocated l (LocScope l n f a) +locScopeAbstract = scopeWAbstract +{-# INLINE locScopeAbstract #-} + +locScopeAbstract1 :: (Functor f, Eq a) => n -> a -> LocScope l n f a -> Colocated l (LocScope l n f a) +locScopeAbstract1 = scopeWAbstract1 +{-# INLINE locScopeAbstract1 #-} + +locScopeUnAbstract :: Functor f => Seq a -> LocScope l n f a -> LocScope l n f a +locScopeUnAbstract = scopeWUnAbstract +{-# INLINE locScopeUnAbstract #-} + +locScopeUnAbstract1 :: Functor f => a -> LocScope l n f a -> LocScope l n f a +locScopeUnAbstract1 = scopeWUnAbstract1 +{-# INLINE locScopeUnAbstract1 #-} + +locScopeInstantiate :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> LocScope l n f a +locScopeInstantiate = scopeWInstantiate +{-# INLINE locScopeInstantiate #-} + +locScopeInstantiate1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> LocScope l n f a +locScopeInstantiate1 = scopeWInstantiate1 +{-# INLINE locScopeInstantiate1 #-} + +locScopeApply :: Functor f => Seq (Colocated l (LocScope l n f a)) -> LocScope l n f a -> Either SubError (LocScope l n f a) +locScopeApply = scopeWApply +{-# INLINE locScopeApply #-} + +locScopeApply1 :: Functor f => Colocated l (LocScope l n f a) -> LocScope l n f a -> Either SubError (LocScope l n f a) +locScopeApply1 = scopeWApply1 +{-# INLINE locScopeApply1 #-} + +locScopeLiftAnno :: Located l a -> LocScope l n f a +locScopeLiftAnno = scopeWLiftAnno +{-# INLINE locScopeLiftAnno #-} + +-- Need an explicit type sig and forall to use this in the hoist below +mapLocatedForall :: (l -> x) -> (forall z. Located l z -> Located x z) +mapLocatedForall f (Located l z) = Located (f l) z + +locScopeHoistAnno :: Functor f => (l -> x) -> LocScope l n f a -> LocScope x n f a +locScopeHoistAnno f = scopeWHoistAnno (mapLocatedForall f) +{-# INLINE locScopeHoistAnno #-} + +locScopeMapAnno :: Functor f => (Located l a -> Located l b) -> LocScope l n f a -> LocScope l n f b +locScopeMapAnno = scopeWMapAnno +{-# INLINE locScopeMapAnno #-} diff --git a/src/Blanks/Located.hs b/src/Blanks/Located.hs --- a/src/Blanks/Located.hs +++ b/src/Blanks/Located.hs @@ -22,8 +22,8 @@ -- It's also basically the 'Writer' monad in certain contexts. -- We define a new, non-transforming datatype so we can pattern-match. data Located l a = Located - { _locatedLoc :: !l - , _locatedVal :: a + { locatedLoc :: !l + , locatedVal :: a } deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) deriving anyclass (NFData) diff --git a/src/Blanks/Name.hs b/src/Blanks/Name.hs --- a/src/Blanks/Name.hs +++ b/src/Blanks/Name.hs @@ -14,8 +14,8 @@ -- terms structurally ('Eq') equivalent. data Name n a = Name - { _nameKey :: !n - , _nameValue :: !a + { nameKey :: !n + , nameValue :: !a } deriving stock (Show, Functor, Foldable, Traversable, Generic) deriving anyclass (NFData) diff --git a/src/Blanks/Scope.hs b/src/Blanks/Scope.hs --- a/src/Blanks/Scope.hs +++ b/src/Blanks/Scope.hs @@ -6,30 +6,41 @@ , pattern ScopeFree , pattern ScopeBinder , pattern ScopeEmbed + , scopeWFromInnerBinder + , scopeBind + , scopeBindOpt + , scopeLift + , scopeInnerBinder + , scopeInnerBinder1 + , scopeAbstract + , scopeAbstract1 + , scopeUnAbstract + , scopeUnAbstract1 + , scopeInstantiate + , scopeInstantiate1 + , scopeApply + , scopeApply1 ) where -import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankFree) +import Blanks.Core (BinderScope) import Blanks.NatNewtype (NatNewtype) -import Blanks.ScopeW (ScopeW (..)) -import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, - pattern UnderScopeFree) +import Blanks.ScopeW (ScopeW (ScopeW), scopeWAbstract, scopeWAbstract1, scopeWApply, scopeWApply1, scopeWBind, + scopeWBindOpt, scopeWFromInnerBinder, scopeWInnerBinder, scopeWInnerBinder1, scopeWInstantiate, + scopeWInstantiate1, scopeWLift, scopeWUnAbstract, scopeWUnAbstract1) +import Blanks.Sub (SubError) +import Blanks.Under (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, pattern UnderScopeFree) import Control.DeepSeq (NFData (..)) import Control.Monad (ap) import Control.Monad.Identity (Identity (..)) +import Data.Sequence (Seq) -- | A simple wrapper for your expression functor that knows how to name-bind. --- See 'Blank' for usage, and see the patterns in this module for easy manipulation --- and inspection. +-- Create free variables is 'pure', bind them with '>>=', and list free variables with folds. +-- See 'LocScope' for a version with additional annotations between layers. newtype Scope n f a = Scope { unScope :: ScopeW Identity n f (Scope n f) a } deriving stock (Functor, Foldable, Traversable) -type instance BlankLeft (Scope n f) = Identity -type instance BlankRight (Scope n f) = Identity -type instance BlankInfo (Scope n f) = n -type instance BlankFunctor (Scope n f) = f - -instance Functor f => Blank (Scope n f) instance NatNewtype (ScopeW Identity n f (Scope n f)) (Scope n f) instance (NFData n, NFData a, NFData (f (Scope n f a))) => NFData (Scope n f a) where @@ -50,15 +61,116 @@ {-# COMPLETE ScopeBound, ScopeFree, ScopeBinder, ScopeEmbed #-} instance Functor f => Applicative (Scope n f) where - pure = runIdentity . blankFree + pure = ScopeFree (<*>) = ap instance Functor f => Monad (Scope n f) where return = pure - s >>= f = blankBind (Identity . f) s + s >>= f = scopeBind f s instance (Eq (f (Scope n f a)), Eq n, Eq a) => Eq (Scope n f a) where Scope su == Scope sv = su == sv instance (Show (f (Scope n f a)), Show n, Show a) => Show (Scope n f a) where showsPrec d (Scope (ScopeW tu)) = showString "Scope " . showsPrec (d+1) tu + +-- * Interface + +scopeFromInnerBinder :: Functor f => BinderScope n (Scope n f a) -> Scope n f a +scopeFromInnerBinder = runIdentity . scopeWFromInnerBinder +{-# INLINE scopeFromInnerBinder #-} + +-- | Substitution as a kind of monadic bind. +scopeBind :: Functor f => (a -> Scope n f b) -> Scope n f a -> Scope n f b +scopeBind f = scopeWBind (Identity . f) +{-# INLINE scopeBind #-} + +-- | Optional substitution as another kind of monadic bind. +scopeBindOpt :: Functor f => (a -> Maybe (Scope n f a)) -> Scope n f a -> Scope n f a +scopeBindOpt f = scopeWBindOpt (fmap Identity . f) +{-# INLINE scopeBindOpt #-} + +-- | Lift an expression functor into the scope functor. +scopeLift :: Traversable f => f a -> Scope n f a +scopeLift = runIdentity . scopeWLift +{-# INLINE scopeLift #-} + +scopeInnerBinder :: (Functor f, Eq a) => n -> Seq a -> Scope n f a -> BinderScope n (Scope n f a) +scopeInnerBinder = scopeWInnerBinder +{-# INLINE scopeInnerBinder #-} + +scopeInnerBinder1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> BinderScope n (Scope n f a) +scopeInnerBinder1 = scopeWInnerBinder1 +{-# INLINE scopeInnerBinder1 #-} + +-- | Binds free variables in an expression and returns a binder. +scopeAbstract + :: (Functor f, Eq a) + => n + -- ^ Annotation specific to your expression functor. + -- Might contain original variable names and types, or might + -- mark this as a "let" vs a "lambda" + -> Seq a + -- ^ Free variables to bind, like the names of function parameters + -> Scope n f a + -- ^ The expression to bind in, like the body of a function + -> Scope n f a +scopeAbstract n ks = runIdentity . scopeWAbstract n ks +{-# INLINE scopeAbstract #-} + +-- | 'scopeAbstract' for a single argument. +scopeAbstract1 :: (Functor f, Eq a) => n -> a -> Scope n f a -> Scope n f a +scopeAbstract1 n k = runIdentity . scopeWAbstract1 n k +{-# INLINE scopeAbstract1 #-} + +-- | Un-bind free variables in an expression. Basically the inverse of +-- 'scopeAbstract'. Take care to match the arity of the binder! ('scopeApply' is safer.) +scopeUnAbstract + :: Functor f + => Seq a + -- ^ The names of the variables you're freeing + -> Scope n f a + -- ^ The expression to substitute in (typically a binder) + -> Scope n f a +scopeUnAbstract = scopeWUnAbstract +{-# INLINE scopeUnAbstract #-} + +-- 'scopeUnAbstract' for a single argument. +scopeUnAbstract1 :: Functor f => a -> Scope n f a -> Scope n f a +scopeUnAbstract1 = scopeWUnAbstract1 +{-# INLINE scopeUnAbstract1 #-} + +-- | Instantiate the bound variables in an expression with other expressions. +-- Take care to match the arity of the binder! ('scopeApply' is safer.) +scopeInstantiate + :: Functor f + => Seq (Scope n f a) + -- ^ Expressions to substitute in place of bound vars + -> Scope n f a + -- ^ The expression to substitute in (typically a binder) + -> Scope n f a +scopeInstantiate vs = scopeWInstantiate (fmap Identity vs) +{-# INLINE scopeInstantiate #-} + +-- | 'scopeInstantiate' for a single argument. +scopeInstantiate1 :: Functor f => Scope n f a -> Scope n f a -> Scope n f a +scopeInstantiate1 v = scopeWInstantiate1 (Identity v) +{-# INLINE scopeInstantiate1 #-} + +-- | Instantiates the bound variables in an expression with other expressions. +-- Throws errors on mismatched arity, non binder expression, unbound vars, etc. +-- A version of 'scopeInstantiate' that fails loudly instead of silently! +scopeApply + :: Functor f + => Seq (Scope n f a) + -- ^ Expressions to substitute in place of bound vars + -> Scope n f a + -- ^ The binder expression to substitute in + -> Either SubError (Scope n f a) +scopeApply vs = scopeWApply (fmap Identity vs) +{-# INLINE scopeApply #-} + +-- | 'scopeApply' for a single argument. +scopeApply1 :: Functor f => Scope n f a -> Scope n f a -> Either SubError (Scope n f a) +scopeApply1 v = scopeWApply1 (Identity v) +{-# INLINE scopeApply1 #-} diff --git a/src/Blanks/ScopeW.hs b/src/Blanks/ScopeW.hs --- a/src/Blanks/ScopeW.hs +++ b/src/Blanks/ScopeW.hs @@ -1,31 +1,35 @@ {-# LANGUAGE UndecidableInstances #-} --- | Internals. You'd need to newtype 'ScopeW' to implement your own 'Blank'. +-- | Internals. module Blanks.ScopeW - ( ScopeC + ( ScopeWC , ScopeW (..) - , ScopeWRawFold - , ScopeWFold , scopeWFree , scopeWEmbed + , scopeWFromInnerBinder + , scopeWInnerBinder + , scopeWInnerBinder1 , scopeWAbstract + , scopeWAbstract1 , scopeWUnAbstract + , scopeWUnAbstract1 , scopeWInstantiate + , scopeWInstantiate1 , scopeWApply + , scopeWApply1 , scopeWBind , scopeWBindOpt , scopeWLift - , scopeWRawFold - , scopeWFold , scopeWLiftAnno , scopeWHoistAnno , scopeWMapAnno ) where +import Blanks.Core (BinderScope (..)) import Blanks.NatNewtype (NatNewtype, natNewtypeFrom, natNewtypeTo) import Blanks.Sub (SubError (..)) -import Blanks.UnderScope (UnderScope, pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, - UnderScopeFold, pattern UnderScopeFree, underScopeFold, underScopeShift) +import Blanks.Under (UnderScope (..), pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed, + pattern UnderScopeFree, underScopeShift) import Control.DeepSeq (NFData (..)) import Data.Bifoldable (bifoldr) import Data.Bifunctor (bimap, first) @@ -37,11 +41,16 @@ -- * ScopeW, patterns, and instances +-- | The core internal scope type. (The "w" comes from "wrapper".) +-- We wrap up an 'UnderScope' in some functor and demand that we +-- unwrap it in an adjoint context. In the first case, these functors will be +-- 'Identity', yielding the 'Scope' newtype. In the second case, these +-- functors will be 'Located' and 'Colocated', yielding the 'LocScope' newtype. newtype ScopeW t n f g a = ScopeW { unScopeW :: t (UnderScope n f (g a) a) } -instance NFData (t (UnderScope n f (g a) a) )=> NFData (ScopeW t n f g a) where +instance NFData (t (UnderScope n f (g a) a)) => NFData (ScopeW t n f g a) where rnf (ScopeW tu) = seq (rnf tu) () instance Eq (t (UnderScope n f (g a) a)) => Eq (ScopeW t n f g a) where @@ -59,43 +68,51 @@ instance (Traversable t, Traversable f, Traversable g) => Traversable (ScopeW t n f g) where traverse f (ScopeW tu) = fmap ScopeW (traverse (bitraverse (traverse f) f) tu) -type ScopeC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g) +type ScopeWC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g) -- * Smart constructors, shift, and bind -scopeWMod :: ScopeC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x +scopeWMod :: ScopeWC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x scopeWMod f = rightAdjunct f . unScopeW . natNewtypeFrom +{-# INLINE scopeWMod #-} -scopeWModOpt :: ScopeC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a +scopeWModOpt :: ScopeWC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a scopeWModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeW (natNewtypeFrom s)) +{-# INLINE scopeWModOpt #-} -scopeWModM :: (ScopeC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x +scopeWModM :: (ScopeWC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x scopeWModM f = rightAdjunct (sequenceA . f) . unScopeW . natNewtypeFrom +{-# INLINE scopeWModM #-} -scopeWBound :: ScopeC t u n f g => Int -> u (g a) +scopeWBound :: ScopeWC t u n f g => Int -> u (g a) scopeWBound b = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBound b)) -scopeWFree :: ScopeC t u n f g => a -> u (g a) +scopeWFree :: ScopeWC t u n f g => a -> u (g a) scopeWFree a = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeFree a)) -scopeWShift :: ScopeC t u n f g => Int -> g a -> g a +scopeWShift :: ScopeWC t u n f g => Int -> g a -> g a scopeWShift = scopeWShiftN 0 +{-# INLINE scopeWShift #-} -scopeWShiftN :: ScopeC t u n f g => Int -> Int -> g a -> g a +scopeWShiftN :: ScopeWC t u n f g => Int -> Int -> g a -> g a scopeWShiftN c d e = let ScopeW tu = natNewtypeFrom e in natNewtypeTo (ScopeW (fmap (underScopeShift scopeWShiftN c d) tu)) -scopeWBinder :: ScopeC t u n f g => Int -> n -> g a -> u (g a) +scopeWBinder :: ScopeWC t u n f g => Int -> n -> g a -> u (g a) scopeWBinder r n e = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBinder r n e)) -scopeWEmbed :: ScopeC t u n f g => f (g a) -> u (g a) +scopeWFromInnerBinder :: ScopeWC t u n f g => BinderScope n (g a) -> u (g a) +scopeWFromInnerBinder b = fmap (natNewtypeTo . ScopeW) (unit (UnderBinderScope b)) + +scopeWEmbed :: ScopeWC t u n f g => f (g a) -> u (g a) scopeWEmbed fe = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeEmbed fe)) -scopeWBind :: ScopeC t u n f g => (a -> u (g b)) -> g a -> g b +scopeWBind :: ScopeWC t u n f g => (a -> u (g b)) -> g a -> g b scopeWBind f = scopeWBindN f 0 +{-# INLINE scopeWBind #-} -scopeWBindN :: ScopeC t u n f g => (a -> u (g b)) -> Int -> g a -> g b +scopeWBindN :: ScopeWC t u n f g => (a -> u (g b)) -> Int -> g a -> g b scopeWBindN f = scopeWMod . go where go i us = case us of @@ -104,10 +121,11 @@ UnderScopeBinder r x e -> scopeWBinder r x (scopeWBindN f (i + r) e) UnderScopeEmbed fe -> scopeWEmbed (fmap (scopeWBindN f i) fe) -scopeWBindOpt :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a +scopeWBindOpt :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a scopeWBindOpt f = scopeWBindOptN f 0 +{-# INLINE scopeWBindOpt #-} -scopeWBindOptN :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a +scopeWBindOptN :: ScopeWC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a scopeWBindOptN f = scopeWModOpt . go where go i us = case us of @@ -116,29 +134,48 @@ UnderScopeBinder r x e -> Just (scopeWBinder r x (scopeWBindOptN f (i + r) e)) UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWBindOptN f i) fe)) -scopeWLift :: (ScopeC t u n f g, Monad u, Traversable f) => f a -> u (g a) +scopeWLift :: (ScopeWC t u n f g, Monad u, Traversable f) => f a -> u (g a) scopeWLift fa = traverse scopeWFree fa >>= scopeWEmbed -- * Abstraction -subScopeWAbstract :: (ScopeC t u n f g, Eq a) => Int -> n -> Seq a -> g a -> u (g a) -subScopeWAbstract r n ks e = - let f = fmap scopeWBound . flip Seq.elemIndexL ks - e' = scopeWBindOpt f e - in scopeWBinder r n e' - -scopeWAbstract :: (ScopeC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a) -scopeWAbstract n ks = +scopeWInnerBinder :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> BinderScope n (g a) +scopeWInnerBinder n ks e = let r = Seq.length ks - in subScopeWAbstract r n ks . scopeWShift r + e' = scopeWShift r e + f = fmap scopeWBound . flip Seq.elemIndexL ks + e'' = scopeWBindOpt f e' + in BinderScope r n e'' -scopeWUnAbstract :: ScopeC t u n f g => Seq a -> g a -> g a +scopeWInnerBinder1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> BinderScope n (g a) +scopeWInnerBinder1 n = scopeWInnerBinder n . Seq.singleton +{-# INLINE scopeWInnerBinder1 #-} + +scopeWAbstract :: (ScopeWC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a) +scopeWAbstract n ks e = scopeWFromInnerBinder (scopeWInnerBinder n ks e) +{-# INLINE scopeWAbstract #-} + +scopeWAbstract1 :: (ScopeWC t u n f g, Eq a) => n -> a -> g a -> u (g a) +scopeWAbstract1 n = scopeWAbstract n . Seq.singleton +{-# INLINE scopeWAbstract1 #-} + +scopeWUnAbstract :: ScopeWC t u n f g => Seq a -> g a -> g a scopeWUnAbstract ks = scopeWInstantiate (fmap scopeWFree ks) +{-# INLINE scopeWUnAbstract #-} -scopeWInstantiate :: ScopeC t u n f g => Seq (u (g a)) -> g a -> g a +scopeWUnAbstract1 :: ScopeWC t u n f g => a -> g a -> g a +scopeWUnAbstract1 = scopeWUnAbstract . Seq.singleton +{-# INLINE scopeWUnAbstract1 #-} + +scopeWInstantiate :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> g a scopeWInstantiate = scopeWInstantiateN 0 +{-# INLINE scopeWInstantiate #-} -scopeWInstantiateN :: ScopeC t u n f g => Int -> Seq (u (g a)) -> g a -> g a +scopeWInstantiate1 :: ScopeWC t u n f g => u (g a) -> g a -> g a +scopeWInstantiate1 = scopeWInstantiate . Seq.singleton +{-# INLINE scopeWInstantiate1 #-} + +scopeWInstantiateN :: ScopeWC t u n f g => Int -> Seq (u (g a)) -> g a -> g a scopeWInstantiateN h vs = scopeWModOpt (go h) where go i us = case us of @@ -150,7 +187,7 @@ in Just (scopeWBinder r n e') UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWInstantiateN i vs) fe)) -scopeWApply :: ScopeC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a) +scopeWApply :: ScopeWC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a) scopeWApply vs = scopeWModM go where go us = case us of @@ -161,16 +198,9 @@ else Left (ApplyError len r) _ -> Left NonBinderError --- * Folds - -type ScopeWRawFold n f g a r = UnderScopeFold n f (g a) a r -type ScopeWFold u n f g a r = ScopeWRawFold n f g a (u r) - -scopeWRawFold :: (NatNewtype (ScopeW t n f g) g, Functor t) => ScopeWRawFold n f g a r -> g a -> t r -scopeWRawFold usf = fmap (underScopeFold usf) . unScopeW . natNewtypeFrom - -scopeWFold :: (NatNewtype (ScopeW t n f g) g, Adjunction t u) => ScopeWFold u n f g a r -> g a -> r -scopeWFold usf = counit . scopeWRawFold usf +scopeWApply1 :: ScopeWC t u n f g => u (g a) -> g a -> Either SubError (g a) +scopeWApply1 = scopeWApply . Seq.singleton +{-# INLINE scopeWApply1 #-} -- * Annotation functions @@ -183,7 +213,7 @@ s = ScopeW (nat (fmap (first (scopeWHoistAnno nat)) tu)) in natNewtypeTo s -scopeWMapAnno :: ScopeC t u n f g => (t a -> t b) -> g a -> g b +scopeWMapAnno :: ScopeWC t u n f g => (t a -> t b) -> g a -> g b scopeWMapAnno f = scopeWMod go where go us = case us of UnderScopeBound b -> scopeWBound b diff --git a/src/Blanks/Split.hs b/src/Blanks/Split.hs new file mode 100644 --- /dev/null +++ b/src/Blanks/Split.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE UndecidableInstances #-} + +module Blanks.Split + ( BinderId (..) + , SplitFunctor (..) + , SplitBinder (..) + , SplitResult (..) + , splitLocScope + ) where + +import Blanks.Core (BinderScope (..)) +import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, + pattern LocScopeFree) +import Blanks.Tracked (Tracked (..), WithTracked (..), mkTrackedBound, mkTrackedFree) +import Control.DeepSeq (NFData (..)) +import Control.Monad.State (State, gets, modify', runState) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.Generics (Generic) + +data Stream x = Stream !x (Stream x) + +enumStreamFrom :: Enum e => e -> Stream e +enumStreamFrom e = Stream e (enumStreamFrom (succ e)) + +enumStream :: Enum e => Stream e +enumStream = enumStreamFrom (toEnum 0) + +newtype BinderId = BinderId { unBinderId :: Int } + deriving stock (Eq, Show, Ord) + deriving newtype (Enum, NFData, Num) + +data SplitFunctor f a = + SplitFunctorBase !(f a) + | SplitFunctorClosure !BinderId !(Seq Int) + deriving stock (Eq, Show, Generic, Functor, Foldable, Traversable) + deriving anyclass (NFData) + +data SplitBinder l n f a = SplitBinder + { splitBinderClosureArity :: !Int + , splitBinderFree :: !(Set a) + , splitBinderScope :: !(BinderScope n (LocScope l n (SplitFunctor f) a)) + } deriving stock (Generic) + +instance (Eq l, Eq n, Eq a, Eq (f (LocScope l n (SplitFunctor f) a))) => Eq (SplitBinder l n f a) where + SplitBinder a1 f1 s1 == SplitBinder a2 f2 s2 = a1 == a2 && f1 == f2 && s1 == s2 + +instance (Show l, Show n, Show a, Show (f (LocScope l n (SplitFunctor f) a))) => Show (SplitBinder l n f a) where + showsPrec d (SplitBinder a f s) = showString "SplitBinder " . showsPrec (d+1) a . showChar ' ' . showsPrec (d+1) f . showChar ' ' . showsPrec (d+1) s + +instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n (SplitFunctor f) a))) => NFData (SplitBinder l n f a) where + rnf (SplitBinder a f s) = seq (rnf a) (seq (rnf f) (rnf s)) + +data SplitState l n f a = SplitState + { splitStateStream :: !(Stream BinderId) + , splitStateBinders :: !(Map BinderId (SplitBinder l n f a)) + } + +initSplitState :: SplitState l n f a +initSplitState = SplitState enumStream Map.empty + +getNextBinderId :: State (SplitState l n f a) BinderId +getNextBinderId = do + st <- gets splitStateStream + let Stream hd tl = st + modify' (\ss -> ss { splitStateStream = tl }) + pure hd + +insertBinder :: BinderId -> SplitBinder l n f a -> State (SplitState l n f a) () +insertBinder bid lb = modify' (\ss -> ss { splitStateBinders = Map.insert bid lb (splitStateBinders ss) }) + +remapBound :: Int -> Set Int -> Int -> Int +remapBound r bs b = maybe b (+ r) (Set.lookupIndex b bs) + +splitLocScopeInner :: (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) +splitLocScopeInner r bs ls = + case ls of + LocScopeBound (WithTracked _ l) b -> + let !b' = remapBound r bs b + in pure (mkTrackedBound b', LocScopeBound l b') + LocScopeFree (WithTracked _ l) a -> + pure (mkTrackedFree a, LocScopeFree l a) + LocScopeEmbed (WithTracked _ l) fe -> fmap (\fx -> let (!t, !fe') = sequence fx in (t, LocScopeEmbed l (SplitFunctorBase fe'))) (traverse (splitLocScopeInner r bs) fe) + LocScopeBinder (WithTracked (Tracked fv bv) l) x n e -> do + bid <- getNextBinderId + let bs' = Set.mapMonotonic (+ r) bv + (_, e') <- splitLocScopeInner x bs' e + let lb = SplitBinder (Set.size bs') fv (BinderScope x n e') + insertBinder bid lb + let ss = Seq.fromList (Set.toList bv) + pure (Tracked Set.empty bv, LocScopeEmbed l (SplitFunctorClosure bid ss)) + +data SplitResult l n f a = SplitResult + { splitResultTracked :: !(Tracked a) + , splitResultScope :: !(LocScope l n (SplitFunctor f) a) + , splitResultBinders :: !(Map BinderId (SplitBinder l n f a)) + } + +splitLocScope :: (Traversable f, Ord a) => LocScope (WithTracked a l) n f a -> SplitResult l n f a +splitLocScope s = + let ((!t, !s'), !ss) = runState (splitLocScopeInner 0 Set.empty s) initSplitState + in SplitResult t s' (splitStateBinders ss) diff --git a/src/Blanks/Tracked.hs b/src/Blanks/Tracked.hs new file mode 100644 --- /dev/null +++ b/src/Blanks/Tracked.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DeriveAnyClass #-} + +-- | Utilities for gathering and caching sets of free variables. +module Blanks.Tracked + ( Tracked (..) + , mkTrackedFree + , mkTrackedBound + , shiftTracked + , WithTracked (..) + , forgetTrackedScope + , trackScope + , trackScopeSimple + ) where + +import Blanks.Conversion (scopeAnno) +import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, + pattern LocScopeFree, locScopeHoistAnno) +import Blanks.Scope (Scope) +import Control.DeepSeq (NFData) +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.Generics (Generic) + +data Tracked a = Tracked + { trackedFree :: !(Set a) + , trackedBound :: !(Set Int) + } deriving stock (Eq, Show, Generic) + deriving anyclass (NFData) + +mkTrackedFree :: a -> Tracked a +mkTrackedFree a = Tracked (Set.singleton a) Set.empty + +mkTrackedBound :: Int -> Tracked a +mkTrackedBound b = Tracked Set.empty (Set.singleton b) + +shiftTracked :: Int -> Tracked a -> Tracked a +shiftTracked i t@(Tracked f b) = + if Set.null b + then t + else + let !b' = if Set.findMax b < i then Set.empty else Set.dropWhileAntitone (< 0) (Set.mapMonotonic (\x -> x - i) b) + in Tracked f b' + +instance Ord a => Semigroup (Tracked a) where + Tracked f1 b1 <> Tracked f2 b2 = Tracked (Set.union f1 f2) (Set.union b1 b2) + +instance Ord a => Monoid (Tracked a) where + mempty = Tracked Set.empty Set.empty + mappend = (<>) + +data WithTracked a l = WithTracked + { withTrackedState :: !(Tracked a) + , withTrackedEnv :: !l + } deriving stock (Eq, Show, Generic, Functor, Foldable, Traversable) + deriving anyclass (NFData) + +forgetTrackedScope :: Functor f => LocScope (WithTracked a l) n f z -> LocScope l n f z +forgetTrackedScope = locScopeHoistAnno withTrackedEnv + +trackScopeInner :: (Traversable f, Ord a) => LocScope l n f a -> (Tracked a, LocScope (WithTracked a l) n f a) +trackScopeInner s = + case s of + LocScopeBound l b -> + let !t = Tracked Set.empty (Set.singleton b) + !m = WithTracked t l + in (t, LocScopeBound m b) + LocScopeFree l a -> + let !t = Tracked (Set.singleton a) Set.empty + !m = WithTracked t l + in (t, LocScopeFree m a) + LocScopeBinder l n i e -> + let !(t0, y) = trackScopeInner e + !t = shiftTracked n t0 + !m = WithTracked t l + in (t, LocScopeBinder m n i y) + LocScopeEmbed l fe -> + let (!t, !fy) = traverse trackScopeInner fe + !m = WithTracked t l + in (t, LocScopeEmbed m fy) + +trackScope :: (Traversable f, Ord a) => LocScope l n f a -> LocScope (WithTracked a l) n f a +trackScope = snd . trackScopeInner + +trackScopeSimple :: (Traversable f, Ord a) => Scope n f a -> LocScope (Tracked a) n f a +trackScopeSimple = locScopeHoistAnno withTrackedState . trackScope . scopeAnno () diff --git a/src/Blanks/Under.hs b/src/Blanks/Under.hs new file mode 100644 --- /dev/null +++ b/src/Blanks/Under.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE DeriveAnyClass #-} + +-- | Internals. +module Blanks.Under + ( UnderScope (..) + , pattern UnderScopeBound + , pattern UnderScopeFree + , pattern UnderScopeBinder + , pattern UnderScopeEmbed + , underScopeShift + ) where + +import Blanks.Core (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..)) +import Control.DeepSeq (NFData) +import Data.Bifoldable (Bifoldable (..)) +import Data.Bifunctor (Bifunctor (..)) +import Data.Bitraversable (Bitraversable (..)) +import GHC.Generics (Generic) + +data UnderScope n f e a + = UnderBoundScope !BoundScope + | UnderFreeScope !(FreeScope a) + | UnderBinderScope !(BinderScope n e) + | UnderEmbedScope !(EmbedScope f e) + deriving stock (Eq, Show, Functor, Generic) + deriving anyclass (NFData) + +pattern UnderScopeBound :: Int -> UnderScope n f e a +pattern UnderScopeBound i = UnderBoundScope (BoundScope i) + +pattern UnderScopeFree :: a -> UnderScope n f e a +pattern UnderScopeFree a = UnderFreeScope (FreeScope a) + +pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a +pattern UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e) + +pattern UnderScopeEmbed :: f e -> UnderScope n f e a +pattern UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe) + +{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-} + +instance Functor f => Bifunctor (UnderScope n f) where + bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b) + bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a)) + bimap f _ (UnderBinderScope (BinderScope i x e)) = UnderBinderScope (BinderScope i x (f e)) + bimap f _ (UnderEmbedScope (EmbedScope fe)) = UnderEmbedScope (EmbedScope (fmap f fe)) + +instance Foldable f => Bifoldable (UnderScope n f) where + bifoldr _ _ z (UnderBoundScope _) = z + bifoldr _ g z (UnderFreeScope (FreeScope a)) = g a z + bifoldr f _ z (UnderBinderScope (BinderScope _ _ e)) = f e z + bifoldr f _ z (UnderEmbedScope (EmbedScope fe)) = foldr f z fe + +instance Traversable f => Bitraversable (UnderScope n f) where + bitraverse _ _ (UnderBoundScope (BoundScope b)) = pure (UnderBoundScope (BoundScope b)) + bitraverse _ g (UnderFreeScope (FreeScope a)) = fmap (UnderFreeScope . FreeScope) (g a) + bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e) + bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe) + +underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a +underScopeShift recShift c d us = + case us of + UnderBoundScope (BoundScope b) -> + if b < c + then us + else UnderBoundScope (BoundScope (b + d)) + UnderFreeScope _ -> us + UnderBinderScope (BinderScope i x e) -> UnderBinderScope (BinderScope i x (recShift (c + i) d e)) + UnderEmbedScope (EmbedScope fe) -> UnderEmbedScope (EmbedScope (fmap (recShift c d) fe)) diff --git a/src/Blanks/UnderScope.hs b/src/Blanks/UnderScope.hs deleted file mode 100644 --- a/src/Blanks/UnderScope.hs +++ /dev/null @@ -1,119 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} - --- | Internals. You will probably never need these. -module Blanks.UnderScope - ( BinderScope (..) - , BoundScope (..) - , EmbedScope (..) - , FreeScope (..) - , UnderScope (..) - , UnderScopeFold (..) - , pattern UnderScopeBound - , pattern UnderScopeFree - , pattern UnderScopeBinder - , pattern UnderScopeEmbed - , underScopeFold - , underScopeShift - ) where - -import Control.DeepSeq (NFData) -import Data.Bifoldable (Bifoldable (..)) -import Data.Bifunctor (Bifunctor (..)) -import Data.Bitraversable (Bitraversable (..)) -import GHC.Generics (Generic) - -newtype BoundScope = - BoundScope - { unBoundScope :: Int - } - deriving newtype (Eq, Show, NFData) - -newtype FreeScope a = - FreeScope - { unFreeScope :: a - } - deriving stock (Eq, Show, Functor, Foldable, Traversable) - deriving newtype (NFData) - -data BinderScope n e = - BinderScope - { binderScopeArity :: !Int - , binderScopeInfo :: !n - , binderScopeBody :: e - } - deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) - deriving anyclass (NFData) - -newtype EmbedScope f e = - EmbedScope - { unEmbedScope :: f e - } - deriving newtype (Eq, Show, Functor, NFData) - -data UnderScope n f e a - = UnderBoundScope !BoundScope - | UnderFreeScope !(FreeScope a) - | UnderBinderScope !(BinderScope n e) - | UnderEmbedScope !(EmbedScope f e) - deriving stock (Eq, Show, Functor, Generic) - deriving anyclass (NFData) - -pattern UnderScopeBound :: Int -> UnderScope n f e a -pattern UnderScopeBound i = UnderBoundScope (BoundScope i) - -pattern UnderScopeFree :: a -> UnderScope n f e a -pattern UnderScopeFree a = UnderFreeScope (FreeScope a) - -pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a -pattern UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e) - -pattern UnderScopeEmbed :: f e -> UnderScope n f e a -pattern UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe) - -{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-} - -instance Functor f => Bifunctor (UnderScope n f) where - bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b) - bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a)) - bimap f _ (UnderBinderScope (BinderScope i x e)) = UnderBinderScope (BinderScope i x (f e)) - bimap f _ (UnderEmbedScope (EmbedScope fe)) = UnderEmbedScope (EmbedScope (fmap f fe)) - -instance Foldable f => Bifoldable (UnderScope n f) where - bifoldr _ _ z (UnderBoundScope _) = z - bifoldr _ g z (UnderFreeScope (FreeScope a)) = g a z - bifoldr f _ z (UnderBinderScope (BinderScope _ _ e)) = f e z - bifoldr f _ z (UnderEmbedScope (EmbedScope fe)) = foldr f z fe - -instance Traversable f => Bitraversable (UnderScope n f) where - bitraverse _ _ (UnderBoundScope (BoundScope b)) = pure (UnderBoundScope (BoundScope b)) - bitraverse _ g (UnderFreeScope (FreeScope a)) = fmap (UnderFreeScope . FreeScope) (g a) - bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e) - bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe) - -underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a -underScopeShift recShift c d us = - case us of - UnderBoundScope (BoundScope b) -> - if b < c - then us - else UnderBoundScope (BoundScope (b + d)) - UnderFreeScope _ -> us - UnderBinderScope (BinderScope i x e) -> UnderBinderScope (BinderScope i x (recShift (c + i) d e)) - UnderEmbedScope (EmbedScope fe) -> UnderEmbedScope (EmbedScope (fmap (recShift c d) fe)) - -data UnderScopeFold n f e a r = - UnderScopeFold - { usfBound :: BoundScope -> r - , usfFree :: FreeScope a -> r - , usfBinder :: BinderScope n e -> r - , usfEmbed :: EmbedScope f e -> r - } - deriving (Functor) - -underScopeFold :: UnderScopeFold n f e a r -> UnderScope n f e a -> r -underScopeFold (UnderScopeFold bound free binder embed) us = - case us of - UnderBoundScope x -> bound x - UnderFreeScope x -> free x - UnderBinderScope x -> binder x - UnderEmbedScope x -> embed x diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -2,9 +2,11 @@ ( main ) where -import Test.Blanks.LocScopeTest (testLocScope) +import Test.Blanks.ExpTest (testExp) import Test.Blanks.ScopeTest (testScope) +import Test.Blanks.SplitTest (testSplit) +import Test.Blanks.TrackedTest (testTracked) import Test.Tasty (defaultMain, testGroup) main :: IO () -main = defaultMain (testGroup "Blanks" [testScope, testLocScope]) +main = defaultMain (testGroup "Blanks" [testScope, testTracked, testExp, testSplit]) diff --git a/test/Test/Blanks/Exp.hs b/test/Test/Blanks/Exp.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/Exp.hs @@ -0,0 +1,254 @@ +{-# LANGUAGE DeriveAnyClass #-} + +module Test.Blanks.Exp + ( Ident (..) + , CExp (..) + , cexpLoc + , CDecl (..) + , declKeywords + , expKeywords + , cexpParser + , runCExpParser + , cdeclParser + , runCDeclParser + , Exp (..) + , ExpScope + , DeclScope + , ExpLocScope + , DeclLocScope + , declLocScopeForget + , declScopeAnno + , expToNameless + , expToNamed + , declToNameless + , declToNamed + ) where + +import Blanks (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, pattern LocScopeFree, + Located (..), NameOnly, pattern NameOnly, Scope, locScopeAbstract1, locScopeForget, locScopeUnAbstract1, + runColocated, scopeAnno) +import Control.DeepSeq (NFData) +import Control.Monad (when) +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.Generics (Generic) +import Test.Blanks.Parsing + +-- A newtype indicating an identifier in our language +newtype Ident = Ident { unIdent :: String } deriving newtype (Eq, Show, Ord, NFData) + +-- The type of concrete expressions, labeled with source location +data CExp l = + CExpBool !l !Bool + | CExpInt !l !Int + | CExpApp !l !(CExp l) !(CExp l) + | CExpAdd !l !(CExp l) !(CExp l) + | CExpIf !l !(CExp l) !(CExp l) !(CExp l) + | CExpIsZero !l !(CExp l) + | CExpVar !l !Ident + | CExpAbs !l !Ident !(CExp l) + | CExpAsc !l !(CExp l) !(CExp l) + | CExpTyInt !l + | CExpTyBool !l + | CExpTyFun !l !(CExp l) !(CExp l) + deriving stock (Eq, Show, Generic) + deriving anyclass (NFData) + +-- Extracts the location from a concrete expression +cexpLoc :: CExp l -> l +cexpLoc ce = + case ce of + CExpBool l _ -> l + CExpInt l _ -> l + CExpApp l _ _ -> l + CExpAdd l _ _ -> l + CExpIf l _ _ _ -> l + CExpIsZero l _ -> l + CExpVar l _ -> l + CExpAbs l _ _ -> l + CExpAsc l _ _ -> l + CExpTyInt l -> l + CExpTyBool l -> l + CExpTyFun l _ _ -> l + +expKeywords :: Set Ident +expKeywords = Set.fromList $ fmap Ident + [ "#t" + , "#f" + , "+" + , "if" + , "zero?" + , ":" + , "lambda" + , "int" + , "bool" + , "->" + ] + +declKeywords :: Set Ident +declKeywords = Set.fromList $ fmap Ident + [ "declare" + , "define" + ] + +nonKeywordParser :: Parser Ident +nonKeywordParser = do + rawIdent <- identifier + let ident = Ident rawIdent + when (Set.member ident expKeywords) (fail ("Parsed exp keyword: " <> rawIdent)) + when (Set.member ident declKeywords) (fail ("Parsed decl keyword: " <> rawIdent)) + pure ident + +-- Parses a concrete expression from a string +cexpParser :: Parser (CExp SourceSpan) +cexpParser = result where + result = branch + [ trueParser + , falseParser + , intParser + , addParser + , ifParser + , isZeroParser + , absParser + , appParser + , ascParser + , tyBoolParser + , tyIntParser + , tyFunParser + , varParser + ] + + trueParser = around (const . flip CExpBool True) (symbol "#t") + + falseParser = around (const . flip CExpBool False) (symbol "#f") + + intParser = around CExpInt signed + + addParser = around2 CExpAdd (parens (symbol "+" *> double cexpParser)) + + ifParser = around3 CExpIf (parens (symbol "if" *> triple cexpParser)) + + isZeroParser = around CExpIsZero (parens (symbol "zero?" *> cexpParser)) + + absParser = around2 CExpAbs $ parens $ do + _ <- symbol "lambda" + n <- parens nonKeywordParser + b <- cexpParser + pure (n, b) + + appParser = around2 CExpApp (parens (double cexpParser)) + + ascParser = around2 CExpAsc (parens (symbol ":" *> double cexpParser)) + + tyBoolParser = around (const . CExpTyBool) (symbol "bool") + + tyIntParser = around (const . CExpTyInt) (symbol "int") + + tyFunParser = around2 (CExpTyFun) (parens (symbol "->" *> double cexpParser)) + + varParser = around CExpVar nonKeywordParser + +runCExpParser :: String -> IO (CExp SourceSpan) +runCExpParser = runParserIO cexpParser + +data Level = + LevelTerm + | LevelType + deriving stock (Eq, Show, Generic) + deriving anyclass (NFData) + +data CDecl l = CDecl !l !Level !Ident !(CExp l) + deriving stock (Eq, Show, Generic) + deriving anyclass (NFData) + +-- Parses a concrete declaration from a string +cdeclParser :: Parser (CDecl SourceSpan) +cdeclParser = result where + result = branch + [ parser "declare" LevelType + , parser "define" LevelTerm + ] + + parser name lvl = around2 (flip CDecl lvl) (parens (symbol name *> ((,) <$> nonKeywordParser <*> cexpParser))) + +runCDeclParser :: String -> IO (CExp SourceSpan) +runCDeclParser = runParserIO cexpParser + +-- Just the expressions of our language that have nothing to do with naming +data Exp a = + ExpBool !Bool + | ExpInt !Int + | ExpApp a a + | ExpAdd a a + | ExpIf a a a + | ExpIsZero a + | ExpAsc a a + | ExpTyBool + | ExpTyInt + | ExpTyFun a a + deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) + deriving anyclass (NFData) + +data Decl a = Decl !Level !Ident a + deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) + deriving anyclass (NFData) + +-- An ExpScope without locations +type ExpScope a = Scope (NameOnly Ident) Exp a + +type DeclScope a = Decl (ExpScope a) + +-- A nameless equivalent to 'CExp' +type ExpLocScope l a = LocScope l (NameOnly Ident) Exp a + +type DeclLocScope l a = Located l (Decl (ExpLocScope l a)) + +declLocScopeForget :: DeclLocScope l a -> DeclScope a +declLocScopeForget = fmap locScopeForget . locatedVal + +declScopeAnno :: l -> DeclScope a -> DeclLocScope l a +declScopeAnno l = Located l . fmap (scopeAnno l) + +-- Convert to nameless representation +expToNameless :: CExp l -> ExpLocScope l Ident +expToNameless ce = + case ce of + CExpBool l b -> LocScopeEmbed l (ExpBool b) + CExpInt l i -> LocScopeEmbed l (ExpInt i) + CExpApp l a b -> LocScopeEmbed l (ExpApp (expToNameless a) (expToNameless b)) + CExpAdd l a b -> LocScopeEmbed l (ExpAdd (expToNameless a) (expToNameless b)) + CExpIf l a b c -> LocScopeEmbed l (ExpIf (expToNameless a) (expToNameless b) (expToNameless c)) + CExpIsZero l a -> LocScopeEmbed l (ExpIsZero (expToNameless a)) + CExpVar l x -> LocScopeFree l x + CExpAbs l x a -> runColocated (locScopeAbstract1 (NameOnly x) x (expToNameless a)) l + CExpAsc l a b -> LocScopeEmbed l (ExpAsc (expToNameless a) (expToNameless b)) + CExpTyInt l -> LocScopeEmbed l ExpTyInt + CExpTyBool l -> LocScopeEmbed l ExpTyBool + CExpTyFun l a b -> LocScopeEmbed l (ExpTyFun (expToNameless a) (expToNameless b)) + +-- Convert back to named representation. Usually this isn't a necessary operation, +-- but we want to do round-trip testing +expToNamed :: ExpLocScope l Ident -> Maybe (CExp l) +expToNamed e = + case e of + LocScopeBound _ _ -> Nothing + LocScopeFree l a -> pure (CExpVar l a) + LocScopeBinder l _ (NameOnly x) b -> CExpAbs l x <$> expToNamed (locScopeUnAbstract1 x b) + LocScopeEmbed l fe -> + case fe of + ExpBool b -> pure (CExpBool l b) + ExpInt i -> pure (CExpInt l i) + ExpApp a b -> CExpApp l <$> expToNamed a <*> expToNamed b + ExpAdd a b -> CExpAdd l <$> expToNamed a <*> expToNamed b + ExpIf a b c -> CExpIf l <$> expToNamed a <*> expToNamed b <*> expToNamed c + ExpIsZero a -> CExpIsZero l <$> expToNamed a + ExpAsc a b -> CExpAsc l <$> expToNamed a <*> expToNamed b + ExpTyInt -> pure (CExpTyInt l) + ExpTyBool -> pure (CExpTyBool l) + ExpTyFun a b -> CExpTyFun l <$> expToNamed a <*> expToNamed b + +declToNameless :: CDecl l -> DeclLocScope l Ident +declToNameless (CDecl l lvl i e) = Located l (Decl lvl i (expToNameless e)) + +declToNamed :: DeclLocScope l Ident -> Maybe (CDecl l) +declToNamed (Located l (Decl lvl i e)) = fmap (CDecl l lvl i) (expToNamed e) diff --git a/test/Test/Blanks/ExpTest.hs b/test/Test/Blanks/ExpTest.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/ExpTest.hs @@ -0,0 +1,51 @@ +module Test.Blanks.ExpTest where + +import Blanks (pattern NameOnly, pattern ScopeBinder, pattern ScopeBound, pattern ScopeEmbed, pattern ScopeFree, + locScopeForget, locScopeLocation) +import Control.DeepSeq (force) +import Test.Blanks.Exp (Exp (..), ExpScope, Ident (..), cexpLoc, expToNamed, expToNameless, runCExpParser) +import Test.Tasty (TestName, TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) + +testSingle :: TestName -> String -> ExpScope Ident -> TestTree +testSingle name input expected = testCase name $ do + namedExp <- runCExpParser input + -- Force here just to test that we can + let namelessExp = force (expToNameless namedExp) + cexpLoc namedExp @?= locScopeLocation namelessExp + let actual = locScopeForget namelessExp + expected @?= actual + let renamedExp = expToNamed namelessExp + Just namedExp @?= renamedExp + +testExp :: TestTree +testExp = testGroup "Exp" cases where + xIdent = Ident "x" + yIdent = Ident "y" + xExp = ScopeFree xIdent + yExp = ScopeFree yIdent + trueExp = ScopeEmbed (ExpBool True) + intExp = ScopeEmbed (ExpInt 42) + negIntExp = ScopeEmbed (ExpInt (-42)) + boolTyExp = ScopeEmbed ExpTyBool + intTyExp = ScopeEmbed ExpTyInt + cases = + [ testSingle "var" "x" xExp + , testSingle "true" "#t" trueExp + , testSingle "false" "#f" (ScopeEmbed (ExpBool False)) + , testSingle "int" "42" intExp + , testSingle "neg int" "-42" negIntExp + , testSingle "add" "(+ 42 -42)" (ScopeEmbed (ExpAdd intExp negIntExp)) + , testSingle "if" "(if #t 42 -42)" (ScopeEmbed (ExpIf trueExp intExp negIntExp)) + , testSingle "add var" "(+ 42 x)" (ScopeEmbed (ExpAdd intExp xExp)) + , testSingle "iszero" "(zero? 42)" (ScopeEmbed (ExpIsZero intExp)) + , testSingle "app" "(x y)" (ScopeEmbed (ExpApp xExp yExp)) + , testSingle "abs yy" "(lambda (y) y)" (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0)) + , testSingle "abs xyy" "(lambda (x) (lambda (y) y))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0))) + , testSingle "abs xyx" "(lambda (x) (lambda (y) x))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 1))) + , testSingle "app abs" "((lambda (x) x) 42)" (ScopeEmbed (ExpApp (ScopeBinder 1 (NameOnly xIdent) (ScopeBound 0)) intExp)) + , testSingle "ty bool" "bool" boolTyExp + , testSingle "ty int" "int" intTyExp + , testSingle "ty fun" "(-> int bool)" (ScopeEmbed (ExpTyFun intTyExp boolTyExp)) + , testSingle "asc" "(: 42 int)" (ScopeEmbed (ExpAsc intExp intTyExp)) + ] diff --git a/test/Test/Blanks/LocScopeTest.hs b/test/Test/Blanks/LocScopeTest.hs deleted file mode 100644 --- a/test/Test/Blanks/LocScopeTest.hs +++ /dev/null @@ -1,164 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} - -module Test.Blanks.LocScopeTest where - -import Blanks -import Control.DeepSeq (NFData, force) -import GHC.Generics (Generic) -import Test.Blanks.Parsing -import Test.Tasty -import Test.Tasty.HUnit - --- A newtype indicating an identifier in our language -newtype Ident = Ident { unIdent :: String } deriving newtype (Eq, Show, Ord, NFData) - --- The type of concrete expressions, labeled with source location -data CExp l = - CExpTrue !l - | CExpFalse !l - | CExpInt !l !Int - | CExpApp !l (CExp l) (CExp l) - | CExpAdd !l (CExp l) (CExp l) - | CExpIf !l (CExp l) (CExp l) (CExp l) - | CExpIsZero !l (CExp l) - | CExpVar !l !Ident - | CExpAbs !l !Ident (CExp l) - deriving (Eq, Show) - --- Extracts the location from a concrete expression -cexpLoc :: CExp l -> l -cexpLoc ce = - case ce of - CExpTrue l -> l - CExpFalse l -> l - CExpInt l _ -> l - CExpApp l _ _ -> l - CExpAdd l _ _ -> l - CExpIf l _ _ _ -> l - CExpIsZero l _ -> l - CExpVar l _ -> l - CExpAbs l _ _ -> l - --- Just the expressions of our language that have nothing to do with naming -data Exp a = - ExpTrue - | ExpFalse - | ExpInt !Int - | ExpApp a a - | ExpAdd a a - | ExpIf a a a - | ExpIsZero a - deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic) - deriving anyclass (NFData) - --- A nameless equivalent to 'CExp' -type ExpScope l = LocScope l (NameOnly Ident) Exp Ident - --- Parsers a concrete expression from a string -cexpParser :: Parser (CExp SourceSpan) -cexpParser = result where - result = branch - [ trueParser - , falseParser - , intParser - , addParser - , ifParser - , isZeroParser - , absParser - , appParser - , varParser - ] - - trueParser = around (const . CExpTrue) (symbol "#t") - - falseParser = around (const . CExpFalse) (symbol "#f") - - intParser = around CExpInt signed - - addParser = around2 CExpAdd (parens (symbol "+" >> double cexpParser)) - - ifParser = around3 CExpIf (parens (symbol "if" >> triple cexpParser)) - - isZeroParser = around CExpIsZero (parens (symbol "zero?" >> cexpParser)) - - absParser = around2 CExpAbs $ parens $ do - _ <- symbol "lambda" - n <- parens (fmap Ident identifier) - b <- cexpParser - pure (n, b) - - appParser = around2 CExpApp (parens (double cexpParser)) - - varParser = around CExpVar (fmap Ident identifier) - --- Convert to nameless representation -nameless :: CExp l -> ExpScope l -nameless ce = - case ce of - CExpTrue l -> LocScopeEmbed l ExpTrue - CExpFalse l -> LocScopeEmbed l ExpFalse - CExpInt l i -> LocScopeEmbed l (ExpInt i) - CExpApp l a b -> LocScopeEmbed l (ExpApp (nameless a) (nameless b)) - CExpAdd l a b -> LocScopeEmbed l (ExpAdd (nameless a) (nameless b)) - CExpIf l a b c -> LocScopeEmbed l (ExpIf (nameless a) (nameless b) (nameless c)) - CExpIsZero l a -> LocScopeEmbed l (ExpIsZero (nameless a)) - CExpVar l x -> LocScopeFree l x - CExpAbs l x a -> runColocated (blankAbstract1 (NameOnly x) x (nameless a)) l - --- Convert back to named representation. Usually this isn't a necessary operation, --- but we want to do round-trip testing -named :: ExpScope l -> Maybe (CExp l) -named e = - case e of - LocScopeBound _ _ -> Nothing - LocScopeFree l a -> pure (CExpVar l a) - LocScopeBinder l _ (NameOnly x) b -> CExpAbs l x <$> named (blankUnAbstract1 x b) - LocScopeEmbed l fe -> - case fe of - ExpTrue -> pure (CExpTrue l) - ExpFalse -> pure (CExpFalse l) - ExpInt i -> pure (CExpInt l i) - ExpApp a b -> CExpApp l <$> named a <*> named b - ExpAdd a b -> CExpAdd l <$> named a <*> named b - ExpIf a b c -> CExpIf l <$> named a <*> named b <*> named c - ExpIsZero a -> CExpIsZero l <$> named a - --- An ExpScope without locations -type ExpSimpleScope = Scope (NameOnly Ident) Exp Ident - -testSingle :: TestName -> String -> ExpSimpleScope -> TestTree -testSingle name input expected = testCase name $ do - namedExp <- runParserIO cexpParser input - -- Force here just to test that we can - let namelessExp = force (nameless namedExp) - cexpLoc namedExp @?= locScopeLocation namelessExp - let actual = locScopeForget namelessExp - expected @?= actual - let renamedExp = named namelessExp - Just namedExp @?= renamedExp - -testLocScope :: TestTree -testLocScope = testGroup "LocScope" cases where - xIdent = Ident "x" - yIdent = Ident "y" - xExp = ScopeFree xIdent - yExp = ScopeFree yIdent - trueExp = ScopeEmbed ExpTrue - intExp = ScopeEmbed (ExpInt 42) - negIntExp = ScopeEmbed (ExpInt (-42)) - cases = - [ testSingle "var" "x" xExp - , testSingle "true" "#t" trueExp - , testSingle "false" "#f" (ScopeEmbed ExpFalse) - , testSingle "int" "42" intExp - , testSingle "neg int" "-42" negIntExp - , testSingle "add" "(+ 42 -42)" (ScopeEmbed (ExpAdd intExp negIntExp)) - , testSingle "if" "(if #t 42 -42)" (ScopeEmbed (ExpIf trueExp intExp negIntExp)) - , testSingle "add var" "(+ 42 x)" (ScopeEmbed (ExpAdd intExp xExp)) - , testSingle "iszero" "(zero? 42)" (ScopeEmbed (ExpIsZero intExp)) - , testSingle "app" "(x y)" (ScopeEmbed (ExpApp xExp yExp)) - , testSingle "abs yy" "(lambda (y) y)" (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0)) - , testSingle "abs xyy" "(lambda (x) (lambda (y) y))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0))) - , testSingle "abs xyx" "(lambda (x) (lambda (y) x))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 1))) - , testSingle "app abs" "((lambda (x) x) 42)" (ScopeEmbed (ExpApp (ScopeBinder 1 (NameOnly xIdent) (ScopeBound 0)) intExp)) - ] diff --git a/test/Test/Blanks/Parsing.hs b/test/Test/Blanks/Parsing.hs --- a/test/Test/Blanks/Parsing.hs +++ b/test/Test/Blanks/Parsing.hs @@ -22,11 +22,11 @@ Right a -> pure a data SourceSpan = SourceSpan - { _ssName :: !FilePath - , _ssStartLine :: !MP.Pos - , _ssStartColumn :: !MP.Pos - , _ssEndLine :: !MP.Pos - , _ssEndColumn :: !MP.Pos + { ssName :: !FilePath + , ssStartLine :: !MP.Pos + , ssStartColumn :: !MP.Pos + , ssEndLine :: !MP.Pos + , ssEndColumn :: !MP.Pos } deriving stock (Eq, Show, Ord, Generic) deriving anyclass (NFData) diff --git a/test/Test/Blanks/ScopeTest.hs b/test/Test/Blanks/ScopeTest.hs --- a/test/Test/Blanks/ScopeTest.hs +++ b/test/Test/Blanks/ScopeTest.hs @@ -2,42 +2,17 @@ ( testScope ) where -import Blanks -import Control.Monad.Identity (Identity (..)) -import Data.Set (Set) +import Blanks (SubError (..), scopeApply1, scopeInstantiate1) import qualified Data.Set as Set import Test.Blanks.Assertions ((@/=)) -import Test.Tasty -import Test.Tasty.HUnit - -type BareScope = Scope (NameOnly Char) Identity Char - -abst :: Char -> BareScope -> BareScope -abst a = runIdentity . blankAbstract1 (Name a ()) a - -bound :: Int -> BareScope -bound = ScopeBound - -var :: Char -> BareScope -var = pure - -freeVars :: BareScope -> Set Char -freeVars = foldMap Set.singleton +import Test.Blanks.SimpleScope (abst, embed, freeVars, sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, svar2, + swonky, swonky2, var) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) testScope :: TestTree testScope = - let svar = var 'x' - sbound = bound 0 - sfree = abst 'y' (var 'x') - sfree2 = abst 'z' (abst 'y' (var 'x')) - sid = abst 'x' (var 'x') - swonky = abst 'x' (bound 0) - sconst = abst 'x' (abst 'y' (var 'x')) - sflip = abst 'x' (abst 'y' (var 'y')) - svar2 = var 'e' - swonky2 = abst 'x' svar2 - - testEq = + let testEq = testCase "eq" $ do svar @?= svar svar @/= svar2 @@ -57,33 +32,38 @@ freeVars swonky @?= Set.empty freeVars sconst @?= Set.empty freeVars sflip @?= Set.empty - freeVars svar2 @=? Set.singleton 'e' + freeVars svar2 @?= Set.singleton 'e' freeVars swonky2 @?= Set.singleton 'e' + freeVars spair @?= Set.singleton 'x' testInstantiate = testCase "instantiate" $ do - blankInstantiate1 (pure svar2) svar @?= svar - blankInstantiate1 (pure svar2) sbound @?= svar2 - blankInstantiate1 (pure svar2) sid @?= sid - blankInstantiate1 (pure svar2) swonky @?= swonky2 + scopeInstantiate1 svar2 svar @?= svar + scopeInstantiate1 svar2 sbound @?= svar2 + scopeInstantiate1 svar2 sid @?= sid + scopeInstantiate1 svar2 swonky @?= swonky2 + scopeInstantiate1 svar2 spair @?= embed svar svar2 testApply = testCase "apply" $ do - blankApply1 (pure svar2) sid @?= Right svar2 - blankApply1 (pure svar2) swonky @?= Right sbound - blankApply1 (pure svar2) sconst @?= Right swonky2 - blankApply1 (pure svar2) sflip @?= Right sid + scopeApply1 svar2 sid @?= Right svar2 + scopeApply1 svar2 swonky @?= Right sbound + scopeApply1 svar2 sconst @?= Right swonky2 + scopeApply1 svar2 sflip @?= Right sid + scopeApply1 svar2 svar @?= Left NonBinderError testVarSub = testCase "var sub" $ do (svar >>= const svar2) @?= svar2 (sfree >>= const svar2) @?= abst 'y' svar2 (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2) + (spair >>= const svar2) @?= embed svar2 sbound testIdSub = testCase "id sub" $ do (svar >>= const sid) @?= sid (sfree >>= const sid) @?= abst 'y' sid (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid) + (spair >>= const sid) @?= embed sid sbound in testGroup "Scope" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub] diff --git a/test/Test/Blanks/SimpleScope.hs b/test/Test/Blanks/SimpleScope.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/SimpleScope.hs @@ -0,0 +1,43 @@ +module Test.Blanks.SimpleScope where + +import Blanks (NameOnly, pattern NameOnly, Scope, pattern ScopeBound, pattern ScopeEmbed, Tracked, locScopeLocation, + scopeAbstract1, trackScopeSimple) +import Data.Set (Set) +import qualified Data.Set as Set + +data SimpleFunctor a = SimpleFunctor !a !a + deriving stock (Eq, Show, Functor, Foldable, Traversable) + +type SimpleScope = Scope (NameOnly Char) SimpleFunctor Char + +abst :: Char -> SimpleScope -> SimpleScope +abst a = scopeAbstract1 (NameOnly a) a + +bound :: Int -> SimpleScope +bound = ScopeBound + +var :: Char -> SimpleScope +var = pure + +freeVars :: SimpleScope -> Set Char +freeVars = foldMap Set.singleton + +tracked :: SimpleScope -> Tracked Char +tracked = locScopeLocation . trackScopeSimple + +embed :: SimpleScope -> SimpleScope -> SimpleScope +embed x y = ScopeEmbed (SimpleFunctor x y) + +svar, sbound, sfree, sfree2, sid, swonky, sconst, sflip, svar2, swonky2, spair, swonky3 :: SimpleScope +svar = var 'x' +sbound = bound 0 +sfree = abst 'y' (var 'x') +sfree2 = abst 'z' (abst 'y' (var 'x')) +sid = abst 'x' (var 'x') +swonky = abst 'x' (bound 0) +sconst = abst 'x' (abst 'y' (var 'x')) +sflip = abst 'x' (abst 'y' (var 'y')) +svar2 = var 'e' +swonky2 = abst 'x' svar2 +spair = embed svar sbound +swonky3 = abst 'x' (bound 3) diff --git a/test/Test/Blanks/SplitScope.hs b/test/Test/Blanks/SplitScope.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/SplitScope.hs @@ -0,0 +1,45 @@ +module Test.Blanks.SplitScope where + +import Blanks (BinderId, BinderScope, LocScope, pattern LocScopeBound, pattern LocScopeEmbed, NameOnly, + pattern NameOnly, SplitBinder (..), SplitFunctor (..), SplitResult, Tracked, + WithTracked (withTrackedState), locScopeAbstract1, locScopeInnerBinder1, locScopeLocation, runColocated, + scopeAnno, splitLocScope, trackScope) +import qualified Data.Sequence as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import Test.Blanks.SimpleScope (SimpleFunctor (..), SimpleScope) + +type SplitScope = LocScope () (NameOnly Char) (SplitFunctor SimpleFunctor) Char +type SplitInnerBinder = BinderScope (NameOnly Char) SplitScope +type SplitOuterBinder = SplitBinder () (NameOnly Char) SimpleFunctor Char +type SplitScopeResult = SplitResult () (NameOnly Char) SimpleFunctor Char + +abstSplit :: Char -> SplitScope -> SplitScope +abstSplit a = flip runColocated () . locScopeAbstract1 (NameOnly a) a + +innerBinderSplit :: Char -> SplitScope -> SplitInnerBinder +innerBinderSplit a = locScopeInnerBinder1 (NameOnly a) a + +boundSplit :: Int -> SplitScope +boundSplit = LocScopeBound () + +varSplit :: Char -> SplitScope +varSplit = pure + +freeVarsSplit :: SplitScope -> Set Char +freeVarsSplit = foldMap Set.singleton + +trackedSplit :: SplitScope -> Tracked Char +trackedSplit = withTrackedState . locScopeLocation . trackScope + +embedSplit :: SplitScope -> SplitScope -> SplitScope +embedSplit x y = LocScopeEmbed () (SplitFunctorBase (SimpleFunctor x y)) + +closureSplit :: BinderId -> [Int] -> SplitScope +closureSplit bid vars = LocScopeEmbed () (SplitFunctorClosure bid (Seq.fromList vars)) + +outerBinderSplit :: Int -> [Char] -> SplitInnerBinder -> SplitOuterBinder +outerBinderSplit a = SplitBinder a . Set.fromList + +simpleSplit :: SimpleScope -> SplitScopeResult +simpleSplit s = splitLocScope (trackScope (scopeAnno () s)) diff --git a/test/Test/Blanks/SplitTest.hs b/test/Test/Blanks/SplitTest.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/SplitTest.hs @@ -0,0 +1,70 @@ +module Test.Blanks.SplitTest + ( testSplit + ) where + +import Blanks (BinderId, SplitResult (..), Tracked, mkTrackedBound, mkTrackedFree) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Test.Blanks.SimpleScope (SimpleScope, sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, swonky, swonky3) +import Test.Blanks.SplitScope (SplitOuterBinder, SplitScope, boundSplit, closureSplit, embedSplit, innerBinderSplit, + outerBinderSplit, simpleSplit, varSplit) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) + +data SplitCase = SplitCase + { splitCaseName :: !String + , splitCaseScopeIn :: !SimpleScope + , splitCaseTrackedOut :: !(Tracked Char) + , splitCaseScopeOut :: !SplitScope + , splitCaseBinders :: !(Map BinderId SplitOuterBinder) + } deriving stock (Eq, Show) + +splitCases :: [SplitCase] +splitCases = + let xvar = varSplit 'x' + xbound = boundSplit 0 + xpair = embedSplit xvar xbound + in [ SplitCase "var" svar (mkTrackedFree 'x') xvar Map.empty + , SplitCase "bound" sbound (mkTrackedBound 0) xbound Map.empty + , SplitCase "pair" spair (mkTrackedFree 'x' <> mkTrackedBound 0) xpair Map.empty + , let ib = innerBinderSplit 'y' (varSplit 'x') + ob = outerBinderSplit 0 ['x'] ib + in SplitCase "free" sfree mempty (closureSplit 0 []) (Map.singleton 0 ob) + , let ibY = innerBinderSplit 'y' (varSplit 'x') + obY = outerBinderSplit 0 ['x'] ibY + ibZ = innerBinderSplit 'z' (closureSplit 1 []) + obZ = outerBinderSplit 0 ['x'] ibZ + in SplitCase "free2" sfree2 mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)]) + , let ib = innerBinderSplit 'x' (varSplit 'x') + ob = outerBinderSplit 0 [] ib + in SplitCase "id" sid mempty (closureSplit 0 []) (Map.singleton 0 ob) + , let ib = innerBinderSplit 'x' (boundSplit 0) + ob = outerBinderSplit 1 [] ib + in SplitCase "wonky" swonky (mkTrackedBound 0) (closureSplit 0 [0]) (Map.singleton 0 ob) + , let ibY = innerBinderSplit 'y' (boundSplit 0) + obY = outerBinderSplit 1 [] ibY + ibZ = innerBinderSplit 'x' (closureSplit 1 [0]) + obZ = outerBinderSplit 0 [] ibZ + in SplitCase "const" sconst mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)]) + , let ibY = innerBinderSplit 'y' (varSplit 'y') + obY = outerBinderSplit 0 [] ibY + ibZ = innerBinderSplit 'x' (closureSplit 1 []) + obZ = outerBinderSplit 0 [] ibZ + in SplitCase "flip" sflip mempty (closureSplit 0 []) (Map.fromList [(0, obZ), (1, obY)]) + , let ib = innerBinderSplit 'x' (boundSplit 3) + ob = outerBinderSplit 1 [] ib + in SplitCase "wonky3" swonky3 (mkTrackedBound 3) (closureSplit 0 [3]) (Map.singleton 0 ob) + ] + +runSplitCase :: SplitCase -> IO () +runSplitCase (SplitCase _ scopeIn trackedOut scopeOut binders) = do + let SplitResult actualTrackedOut actualScopeOut actualBinders = simpleSplit scopeIn + actualTrackedOut @?= trackedOut + actualScopeOut @?= scopeOut + actualBinders @?= binders + +testSplitCase :: SplitCase -> TestTree +testSplitCase c = testCase (splitCaseName c) (runSplitCase c) + +testSplit :: TestTree +testSplit = testGroup "Split" (fmap testSplitCase splitCases) diff --git a/test/Test/Blanks/TrackedTest.hs b/test/Test/Blanks/TrackedTest.hs new file mode 100644 --- /dev/null +++ b/test/Test/Blanks/TrackedTest.hs @@ -0,0 +1,24 @@ +module Test.Blanks.TrackedTest + ( testTracked + ) where + +import Blanks (mkTrackedBound, mkTrackedFree) +import Test.Blanks.SimpleScope (sbound, sconst, sflip, sfree, sfree2, sid, spair, svar, svar2, swonky, swonky2, swonky3, + tracked) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (testCase, (@?=)) + +testTracked :: TestTree +testTracked = testCase "tracked" $ do + tracked svar @?= mkTrackedFree 'x' + tracked sbound @?= mkTrackedBound 0 + tracked sfree @?= mkTrackedFree 'x' + tracked sfree2 @?= mkTrackedFree 'x' + tracked sid @?= mempty + tracked swonky @?= mkTrackedBound 0 + tracked sconst @?= mempty + tracked sflip @?= mempty + tracked svar2 @?= mkTrackedFree 'e' + tracked swonky2 @?= mkTrackedFree 'e' + tracked spair @?= mkTrackedFree 'x' <> mkTrackedBound 0 + tracked swonky3 @?= mkTrackedBound 3