Replace Core.Scope with Syntax.Scope.

semantic-core/semantic-core.cabal

@@ -54,7 +54,6 @@ library
     Core.File
     Core.Loc
     Core.Name
-    Core.Scope
   build-depends:
       algebraic-graphs            ^>= 0.3
     , base                         >= 4.12 && < 5

semantic-core/src/Analysis/Eval.hs

@@ -20,12 +20,12 @@ import Core.Core as Core
 import Core.File
 import Core.Loc
 import Core.Name
-import Core.Scope
 import Data.Functor
 import Data.Maybe (fromJust, fromMaybe)
 import Data.Text (Text)
 import GHC.Stack
 import Prelude hiding (fail)
+import Syntax.Scope
 import Source.Span
 import Syntax.Term
 

semantic-core/src/Analysis/Typecheck.hs

@@ -19,7 +19,6 @@ import           Control.Monad ((>=>), unless)
 import           Core.File
 import           Core.Loc
 import           Core.Name as Name
-import           Core.Scope
 import           Data.Foldable (for_)
 import           Data.Function (fix)
 import           Data.Functor (($>))
@@ -37,7 +36,9 @@ import           GHC.Generics (Generic1)
 import           Prelude hiding (fail)
 import           Source.Span
 import           Syntax.Module
+import           Syntax.Scope
 import           Syntax.Term
+import           Syntax.Var (closed)
 
 data Monotype f a
   = Bool

semantic-core/src/Core/Core.hs

@@ -39,7 +39,6 @@ import Control.Applicative (Alternative (..))
 import Control.Effect.Carrier
 import Core.Loc
 import Core.Name
-import Core.Scope
 import Data.Bifunctor (Bifunctor (..))
 import Data.Foldable (foldl')
 import Data.List.NonEmpty (NonEmpty (..))
@@ -48,6 +47,7 @@ import Data.Text (Text)
 import GHC.Generics (Generic1)
 import GHC.Stack
 import Source.Span
+import Syntax.Scope
 import Syntax.Stack
 import Syntax.Module
 import Syntax.Term

semantic-core/src/Core/Core/Pretty.hs

@@ -11,12 +11,12 @@ module Core.Core.Pretty
 import           Core.Core
 import           Core.File
 import           Core.Name
-import           Core.Scope
 import           Data.Foldable (toList)
 import           Data.Text.Prettyprint.Doc
 import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
 import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
 import           Syntax.Pretty
+import           Syntax.Scope
 import           Syntax.Stack
 import           Syntax.Term
 

semantic-core/src/Core/Scope.hs

@@ -1,107 +0,0 @@
-{-# LANGUAGE DeriveTraversable, LambdaCase, RankNTypes, QuantifiedConstraints, StandaloneDeriving #-}
-module Core.Scope
-( Incr(..)
-, incr
-, closed
-, Scope(..)
-, fromScope
-, toScope
-, abstract1
-, abstract
-, abstractEither
-, instantiate1
-, instantiate
-, instantiateEither
-) where
-
-import Control.Applicative (liftA2)
-import Control.Effect.Carrier
-import Control.Monad ((>=>), guard)
-import Control.Monad.Trans.Class
-import Data.Function (on)
-import Syntax.Module
-
-data Incr a b
-  = Z a
-  | S b
-  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
-
-instance Applicative (Incr a) where
-  pure = S
-  Z a <*> _ = Z a
-  S f <*> a = f <$> a
-
-instance Monad (Incr a) where
-  Z a >>= _ = Z a
-  S a >>= f = f a
-
-match :: Applicative f => (b -> Either a c) -> b -> Incr a (f c)
-match f x = either Z (S . pure) (f x)
-
-matchMaybe :: (b -> Maybe a) -> (b -> Either a b)
-matchMaybe f a = maybe (Right a) Left (f a)
-
-incr :: (a -> c) -> (b -> c) -> Incr a b -> c
-incr z s = \case { Z a -> z a ; S b -> s b }
-
-
-closed :: Traversable f => f a -> Maybe (f b)
-closed = traverse (const Nothing)
-
-
-newtype Scope a f b = Scope { unScope :: f (Incr a (f b)) }
-  deriving (Foldable, Functor, Traversable)
-
-instance HFunctor (Scope a) where
-  hmap f = Scope . f . fmap (fmap f) . unScope
-
-instance (Eq   a, Eq   b, forall a . Eq   a => Eq   (f a), Monad f) => Eq   (Scope a f b) where
-  (==) = (==) `on` fromScope
-
-instance (Ord  a, Ord  b, forall a . Eq   a => Eq   (f a)
-                        , forall a . Ord  a => Ord  (f a), Monad f) => Ord  (Scope a f b) where
-  compare = compare `on` fromScope
-
-deriving instance (Show a, Show b, forall a . Show a => Show (f a)) => Show (Scope a f b)
-
-instance Applicative f => Applicative (Scope a f) where
-  pure = Scope . pure . S . pure
-  Scope f <*> Scope a = Scope (liftA2 (liftA2 (<*>)) f a)
-
-instance Monad f => Monad (Scope a f) where
-  Scope e >>= f = Scope (e >>= incr (pure . Z) (>>= unScope . f))
-
-instance MonadTrans (Scope a) where
-  lift = Scope . pure . S
-
-instance RightModule (Scope a) where
-  Scope m >>=* f = Scope (fmap (>>= f) <$> m)
-
-
-fromScope :: Monad f => Scope a f b -> f (Incr a b)
-fromScope = unScope >=> sequenceA
-
-toScope :: Applicative f => f (Incr a b) -> Scope a f b
-toScope = Scope . fmap (fmap pure)
-
-
--- | Bind occurrences of a variable in a term, producing a term in which the variable is bound.
-abstract1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
-abstract1 n = abstract (guard . (== n))
-
-abstract :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
-abstract f = abstractEither (matchMaybe f)
-
-abstractEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
-abstractEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
-
-
--- | Substitute a term for the free variable in a given term, producing a closed term.
-instantiate1 :: Monad f => f b -> Scope a f b -> f b
-instantiate1 t = instantiate (const t)
-
-instantiate :: Monad f => (a -> f b) -> Scope a f b -> f b
-instantiate f = instantiateEither (either f pure)
-
-instantiateEither :: Monad f => (Either a b -> f c) -> Scope a f b -> f c
-instantiateEither f = unScope >=> incr (f . Left) (>>= f . Right)