{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE UndecidableInstances  #-}
-- TODO: add @NoFieldSelectors@ once we are past antiquity, so that 'ScopeError' doesn't generate
-- partial field selectors.

module PlutusCore.Check.Scoping where

import PlutusCore.Name.Unique
import PlutusCore.Quote

import Control.Monad (join, unless)
import Data.Bifunctor
import Data.Coerce
import Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict as Map
import Data.Maybe
import Data.Set as Set
import Text.Pretty
import Text.PrettyBy

{- Note [Example of a scoping check]
Consider the following type:

    \(x_42 :: *) -> x_42

This Note describes how we can use this type to check that a renamer handles scoping correctly.
Any other type could be used as well (and in property tests we generate random ones), but the type
above is the simplest example, so we're going to use it.

First, we traverse the type and freshen every single name in it, which gives us

    \(x_0 :: *) -> x_1

After this procedure all names in the new type are distinct, not just globally unique -- completely
distinct: all variables are free variables with different uniques and all bindings are distinct and
never referenced.

Now for each binder we insert one in-scope variable and one out-of-scope one by referencing them
in an added constructor (we could use 'TyFun', but we use 'TyApp', 'cause it has an analogue at the
term level -- 'Apply' and we can also reference a type variable in a 'Term' via a similar
constructor -- 'TyInst'). That gives us

    (\(x_0 :: *) -> x_1 x_0) x_0

(currently we just decorate the binder with those constructors. In future we could employ a fancier
strategy and go under to the leaves of the term being processed etc).

The next step is to annotate each name with what is supposed to happen to it once the renaming is
performed.

1. the @x_0@ binding is supposed to be renamed and hence will disappear
2. the @x_1@ variable is free, so it's supposed to stay free
3. the inner @x_0@ variable is in scope and so is supposed to be renamed
4. the outer @x_0@ is out of scope and so is free and is supposed to stay

In the actual implementation everything that we did above happens in a single definition.

After this initial scoping setup is performed, we run the provided renamer (which is not supposed
to touch any annotations) and collect all the available information: which names disappeared,
which didn't, which appeared etc, simultaneously checking that the names that were supposed to
disappear indeed disappeared and the names that were supposed to stay indeed stayed.

Once all this scoping information is collected, we run 'checkScopeInfo' to check that the
information is coherent. See its docs for the details on what exactly the checked invariants are.

The advantage of this approach is that we can pinpoint exactly where what is visible and, just
as importantly, what is not.
-}

data ScopedName
    = TypeName TyName
    | TermName Name
    deriving stock (Int -> ScopedName -> ShowS
[ScopedName] -> ShowS
ScopedName -> String
(Int -> ScopedName -> ShowS)
-> (ScopedName -> String)
-> ([ScopedName] -> ShowS)
-> Show ScopedName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopedName -> ShowS
showsPrec :: Int -> ScopedName -> ShowS
$cshow :: ScopedName -> String
show :: ScopedName -> String
$cshowList :: [ScopedName] -> ShowS
showList :: [ScopedName] -> ShowS
Show, ScopedName -> ScopedName -> Bool
(ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool) -> Eq ScopedName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopedName -> ScopedName -> Bool
== :: ScopedName -> ScopedName -> Bool
$c/= :: ScopedName -> ScopedName -> Bool
/= :: ScopedName -> ScopedName -> Bool
Eq, Eq ScopedName
Eq ScopedName =>
(ScopedName -> ScopedName -> Ordering)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> Bool)
-> (ScopedName -> ScopedName -> ScopedName)
-> (ScopedName -> ScopedName -> ScopedName)
-> Ord ScopedName
ScopedName -> ScopedName -> Bool
ScopedName -> ScopedName -> Ordering
ScopedName -> ScopedName -> ScopedName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ScopedName -> ScopedName -> Ordering
compare :: ScopedName -> ScopedName -> Ordering
$c< :: ScopedName -> ScopedName -> Bool
< :: ScopedName -> ScopedName -> Bool
$c<= :: ScopedName -> ScopedName -> Bool
<= :: ScopedName -> ScopedName -> Bool
$c> :: ScopedName -> ScopedName -> Bool
> :: ScopedName -> ScopedName -> Bool
$c>= :: ScopedName -> ScopedName -> Bool
>= :: ScopedName -> ScopedName -> Bool
$cmax :: ScopedName -> ScopedName -> ScopedName
max :: ScopedName -> ScopedName -> ScopedName
$cmin :: ScopedName -> ScopedName -> ScopedName
min :: ScopedName -> ScopedName -> ScopedName
Ord)

isSameScope :: ScopedName -> ScopedName -> Bool
isSameScope :: ScopedName -> ScopedName -> Bool
isSameScope TypeName{} TypeName{} = Bool
True
isSameScope TermName{} TermName{} = Bool
True
isSameScope TypeName{} TermName{} = Bool
False
isSameScope TermName{} TypeName{} = Bool
False

-- | Staying names.
data Stays
    = StaysOutOfScopeVariable  -- ^ An out-of-scope variable does not get renamed and hence stays.
    | StaysFreeVariable        -- ^ A free variable does not get renamed and hence stays.
    deriving stock (Int -> Stays -> ShowS
[Stays] -> ShowS
Stays -> String
(Int -> Stays -> ShowS)
-> (Stays -> String) -> ([Stays] -> ShowS) -> Show Stays
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Stays -> ShowS
showsPrec :: Int -> Stays -> ShowS
$cshow :: Stays -> String
show :: Stays -> String
$cshowList :: [Stays] -> ShowS
showList :: [Stays] -> ShowS
Show)

-- | Changing names.
data Disappears
    = DisappearsBinding   -- ^ A binding gets renamed and hence the name that it binds disappears.
    | DisappearsVariable  -- ^ A bound variable gets renamed and hence its name disappears.
    deriving stock (Int -> Disappears -> ShowS
[Disappears] -> ShowS
Disappears -> String
(Int -> Disappears -> ShowS)
-> (Disappears -> String)
-> ([Disappears] -> ShowS)
-> Show Disappears
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Disappears -> ShowS
showsPrec :: Int -> Disappears -> ShowS
$cshow :: Disappears -> String
show :: Disappears -> String
$cshowList :: [Disappears] -> ShowS
showList :: [Disappears] -> ShowS
Show)

-- | A name either stays or disappears.
data NameAction
    = Stays Stays
    | Disappears Disappears
    deriving stock (Int -> NameAction -> ShowS
[NameAction] -> ShowS
NameAction -> String
(Int -> NameAction -> ShowS)
-> (NameAction -> String)
-> ([NameAction] -> ShowS)
-> Show NameAction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NameAction -> ShowS
showsPrec :: Int -> NameAction -> ShowS
$cshow :: NameAction -> String
show :: NameAction -> String
$cshowList :: [NameAction] -> ShowS
showList :: [NameAction] -> ShowS
Show)

data NameAnn
    = NameAction NameAction ScopedName
    | NotAName
    deriving stock (Int -> NameAnn -> ShowS
[NameAnn] -> ShowS
NameAnn -> String
(Int -> NameAnn -> ShowS)
-> (NameAnn -> String) -> ([NameAnn] -> ShowS) -> Show NameAnn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NameAnn -> ShowS
showsPrec :: Int -> NameAnn -> ShowS
$cshow :: NameAnn -> String
show :: NameAnn -> String
$cshowList :: [NameAnn] -> ShowS
showList :: [NameAnn] -> ShowS
Show)

instance Pretty NameAnn where
    pretty :: forall ann. NameAnn -> Doc ann
pretty = NameAnn -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

class ToScopedName name where
    toScopedName :: name -> ScopedName

instance ToScopedName TyName where
    toScopedName :: TyName -> ScopedName
toScopedName = TyName -> ScopedName
TypeName

instance ToScopedName Name where
    toScopedName :: Name -> ScopedName
toScopedName = Name -> ScopedName
TermName

-- Naming: @introduce*@ for bindings and @register*@ for variables.

-- | Annotation for a binding saying \"supposed to disappear\".
introduceBound :: ToScopedName name => name -> NameAnn
introduceBound :: forall name. ToScopedName name => name -> NameAnn
introduceBound = NameAction -> ScopedName -> NameAnn
NameAction (Disappears -> NameAction
Disappears Disappears
DisappearsBinding) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for a bound variable saying \"supposed to disappear\".
registerBound :: ToScopedName name => name -> NameAnn
registerBound :: forall name. ToScopedName name => name -> NameAnn
registerBound = NameAction -> ScopedName -> NameAnn
NameAction (Disappears -> NameAction
Disappears Disappears
DisappearsVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for an out-of-scope variable saying \"supposed to stay out of scope\".
registerOutOfScope :: ToScopedName name => name -> NameAnn
registerOutOfScope :: forall name. ToScopedName name => name -> NameAnn
registerOutOfScope = NameAction -> ScopedName -> NameAnn
NameAction (Stays -> NameAction
Stays Stays
StaysOutOfScopeVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

-- | Annotation for a free variable saying \"supposed to stay free\".
registerFree :: ToScopedName name => name -> NameAnn
registerFree :: forall name. ToScopedName name => name -> NameAnn
registerFree = NameAction -> ScopedName -> NameAnn
NameAction (Stays -> NameAction
Stays Stays
StaysFreeVariable) (ScopedName -> NameAnn) -> (name -> ScopedName) -> name -> NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName

class Reference n t where
    -- | Take a registering function, apply it to the provided name, create a type\/term variable
    -- out of the resulting annotation and the original name and reference that variable in the
    -- provided type\/term by prepending a constructor to it mentioning the variable.
    referenceVia
        :: (forall name. ToScopedName name => name -> NameAnn)
        -> n
        -> t NameAnn
        -> t NameAnn

-- | Reference the provided variable in the provided type\/term as an in-scope one.
referenceBound :: Reference n t => n -> t NameAnn -> t NameAnn
referenceBound :: forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceBound = (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerBound

-- | Reference the provided variable in the provided type\/term as an out-of-scope one.
referenceOutOfScope :: Reference n t => n -> t NameAnn -> t NameAnn
referenceOutOfScope :: forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope = (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerOutOfScope

-- #####################################################
-- ## Information about scopes and relevant functions ##
-- #####################################################

-- | Each kind of old and new names.
data ScopeEntry
    = DisappearedBindings
    | DisappearedVariables
    | AppearedBindings
    | AppearedVariables
    | StayedOutOfScopeVariables
    | StayedFreeVariables
    deriving stock (Int -> ScopeEntry -> ShowS
[ScopeEntry] -> ShowS
ScopeEntry -> String
(Int -> ScopeEntry -> ShowS)
-> (ScopeEntry -> String)
-> ([ScopeEntry] -> ShowS)
-> Show ScopeEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeEntry -> ShowS
showsPrec :: Int -> ScopeEntry -> ShowS
$cshow :: ScopeEntry -> String
show :: ScopeEntry -> String
$cshowList :: [ScopeEntry] -> ShowS
showList :: [ScopeEntry] -> ShowS
Show, ScopeEntry -> ScopeEntry -> Bool
(ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool) -> Eq ScopeEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopeEntry -> ScopeEntry -> Bool
== :: ScopeEntry -> ScopeEntry -> Bool
$c/= :: ScopeEntry -> ScopeEntry -> Bool
/= :: ScopeEntry -> ScopeEntry -> Bool
Eq, Eq ScopeEntry
Eq ScopeEntry =>
(ScopeEntry -> ScopeEntry -> Ordering)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> Bool)
-> (ScopeEntry -> ScopeEntry -> ScopeEntry)
-> (ScopeEntry -> ScopeEntry -> ScopeEntry)
-> Ord ScopeEntry
ScopeEntry -> ScopeEntry -> Bool
ScopeEntry -> ScopeEntry -> Ordering
ScopeEntry -> ScopeEntry -> ScopeEntry
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ScopeEntry -> ScopeEntry -> Ordering
compare :: ScopeEntry -> ScopeEntry -> Ordering
$c< :: ScopeEntry -> ScopeEntry -> Bool
< :: ScopeEntry -> ScopeEntry -> Bool
$c<= :: ScopeEntry -> ScopeEntry -> Bool
<= :: ScopeEntry -> ScopeEntry -> Bool
$c> :: ScopeEntry -> ScopeEntry -> Bool
> :: ScopeEntry -> ScopeEntry -> Bool
$c>= :: ScopeEntry -> ScopeEntry -> Bool
>= :: ScopeEntry -> ScopeEntry -> Bool
$cmax :: ScopeEntry -> ScopeEntry -> ScopeEntry
max :: ScopeEntry -> ScopeEntry -> ScopeEntry
$cmin :: ScopeEntry -> ScopeEntry -> ScopeEntry
min :: ScopeEntry -> ScopeEntry -> ScopeEntry
Ord)

-- | A 'ScopeInfo' is a set of 'ScopedName's for each of the 'ScopeEntry'.
-- If a 'ScopeEntry' is not present in the map, the corresponding set of 'ScopeName's is considered
-- to be empty.
newtype ScopeInfo = ScopeInfo (Map ScopeEntry (Set ScopedName))
    deriving stock (Int -> ScopeInfo -> ShowS
[ScopeInfo] -> ShowS
ScopeInfo -> String
(Int -> ScopeInfo -> ShowS)
-> (ScopeInfo -> String)
-> ([ScopeInfo] -> ShowS)
-> Show ScopeInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeInfo -> ShowS
showsPrec :: Int -> ScopeInfo -> ShowS
$cshow :: ScopeInfo -> String
show :: ScopeInfo -> String
$cshowList :: [ScopeInfo] -> ShowS
showList :: [ScopeInfo] -> ShowS
Show)

-- Defining manually because of plan to move to @NoFieldSelectors@.
unScopeInfo :: ScopeInfo -> Map ScopeEntry (Set ScopedName)
unScopeInfo :: ScopeInfo -> Map ScopeEntry (Set ScopedName)
unScopeInfo = ScopeInfo -> Map ScopeEntry (Set ScopedName)
forall a b. Coercible a b => a -> b
coerce

-- | Extract the set stored in the provided 'ScopeInfo' at the provided 'ScopeEntry'.
to :: ScopeEntry -> ScopeInfo -> Set ScopedName
to :: ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
entry = Set ScopedName -> Maybe (Set ScopedName) -> Set ScopedName
forall a. a -> Maybe a -> a
fromMaybe Set ScopedName
forall a. Set a
Set.empty (Maybe (Set ScopedName) -> Set ScopedName)
-> (ScopeInfo -> Maybe (Set ScopedName))
-> ScopeInfo
-> Set ScopedName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeEntry
-> Map ScopeEntry (Set ScopedName) -> Maybe (Set ScopedName)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ScopeEntry
entry (Map ScopeEntry (Set ScopedName) -> Maybe (Set ScopedName))
-> (ScopeInfo -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo
-> Maybe (Set ScopedName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Map ScopeEntry (Set ScopedName)
unScopeInfo

emptyScopeInfo :: ScopeInfo
emptyScopeInfo :: ScopeInfo
emptyScopeInfo = Map ScopeEntry (Set ScopedName) -> ScopeInfo
ScopeInfo Map ScopeEntry (Set ScopedName)
forall k a. Map k a
Map.empty

-- | Check if a set is empty and report an error with the set embedded in it otherwise.
checkEmptyOn
    :: (Set ScopedName -> Set ScopedName -> Set ScopedName)
    -> (Set ScopedName -> Set ScopedName -> ScopeError)
    -> Set ScopedName
    -> Set ScopedName
    -> Either ScopeError ()
checkEmptyOn :: (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn Set ScopedName -> Set ScopedName -> Set ScopedName
f Set ScopedName -> Set ScopedName -> ScopeError
err Set ScopedName
s1 Set ScopedName
s2 = Bool -> Either ScopeError () -> Either ScopeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set ScopedName -> Bool
forall a. Set a -> Bool
Set.null (Set ScopedName -> Bool) -> Set ScopedName -> Bool
forall a b. (a -> b) -> a -> b
$ Set ScopedName -> Set ScopedName -> Set ScopedName
f Set ScopedName
s1 Set ScopedName
s2) (Either ScopeError () -> Either ScopeError ())
-> (ScopeError -> Either ScopeError ())
-> ScopeError
-> Either ScopeError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeError -> Either ScopeError ()
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ())
-> ScopeError -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$ Set ScopedName -> Set ScopedName -> ScopeError
err Set ScopedName
s1 Set ScopedName
s2

-- | Merge two 'ScopeInfo's checking that binders in them do not intersect along the way.
mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo ScopeInfo
si1 ScopeInfo
si2 = do
    let disappearedBindings1 :: Set ScopedName
disappearedBindings1 = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings ScopeInfo
si1
        disappearedBindings2 :: Set ScopedName
disappearedBindings2 = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings ScopeInfo
si2
        appearedBindings1 :: Set ScopedName
appearedBindings1    = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings    ScopeInfo
si1
        appearedBindings2 :: Set ScopedName
appearedBindings2    = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings    ScopeInfo
si2
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
        Set ScopedName -> Set ScopedName -> ScopeError
DuplicateBindersInTheInput
        Set ScopedName
disappearedBindings1
        Set ScopedName
disappearedBindings2
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
        Set ScopedName -> Set ScopedName -> ScopeError
DuplicateBindersInTheOutput
        Set ScopedName
appearedBindings1
        Set ScopedName
appearedBindings2
    ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ (Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo -> ScopeInfo -> ScopeInfo
forall a b. Coercible a b => a -> b
coerce ((Set ScopedName -> Set ScopedName -> Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.union) ScopeInfo
si1 ScopeInfo
si2

-- We might want to use @Validation@ or something instead of 'Either'.
-- @newtype@-ing it for the sake of providing very convenient 'Semigroup' and 'Monoid' instances.
newtype ScopeErrorOrInfo = ScopeErrorOrInfo (Either ScopeError ScopeInfo)

-- Defining manually because of plan to move to @NoFieldSelectors@.
unScopeErrorOrInfo :: ScopeErrorOrInfo -> Either ScopeError ScopeInfo
unScopeErrorOrInfo :: ScopeErrorOrInfo -> Either ScopeError ScopeInfo
unScopeErrorOrInfo = ScopeErrorOrInfo -> Either ScopeError ScopeInfo
forall a b. Coercible a b => a -> b
coerce

instance Semigroup ScopeErrorOrInfo where
    ScopeErrorOrInfo Either ScopeError ScopeInfo
errOrInfo1 <> :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
<> ScopeErrorOrInfo Either ScopeError ScopeInfo
errOrInfo2 =
        Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> (Either ScopeError (Either ScopeError ScopeInfo)
    -> Either ScopeError ScopeInfo)
-> Either ScopeError (Either ScopeError ScopeInfo)
-> ScopeErrorOrInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either ScopeError (Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either ScopeError (Either ScopeError ScopeInfo)
 -> ScopeErrorOrInfo)
-> Either ScopeError (Either ScopeError ScopeInfo)
-> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
mergeScopeInfo (ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
-> Either ScopeError (ScopeInfo -> Either ScopeError ScopeInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either ScopeError ScopeInfo
errOrInfo1 Either ScopeError (ScopeInfo -> Either ScopeError ScopeInfo)
-> Either ScopeError ScopeInfo
-> Either ScopeError (Either ScopeError ScopeInfo)
forall a b.
Either ScopeError (a -> b)
-> Either ScopeError a -> Either ScopeError b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either ScopeError ScopeInfo
errOrInfo2

instance Monoid ScopeErrorOrInfo where
    mempty :: ScopeErrorOrInfo
mempty = Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> Either ScopeError ScopeInfo -> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right ScopeInfo
emptyScopeInfo

-- | Whether it's OK if the pass removes bindings. A renamer isn't supposed to do that, but for
-- example an inliner may do it, since it's basically the entire point of an inliner.
data BindingRemoval
    = BindingRemovalOk
    | BindingRemovalNotOk
    deriving stock (Int -> BindingRemoval -> ShowS
[BindingRemoval] -> ShowS
BindingRemoval -> String
(Int -> BindingRemoval -> ShowS)
-> (BindingRemoval -> String)
-> ([BindingRemoval] -> ShowS)
-> Show BindingRemoval
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BindingRemoval -> ShowS
showsPrec :: Int -> BindingRemoval -> ShowS
$cshow :: BindingRemoval -> String
show :: BindingRemoval -> String
$cshowList :: [BindingRemoval] -> ShowS
showList :: [BindingRemoval] -> ShowS
Show, BindingRemoval -> BindingRemoval -> Bool
(BindingRemoval -> BindingRemoval -> Bool)
-> (BindingRemoval -> BindingRemoval -> Bool) -> Eq BindingRemoval
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BindingRemoval -> BindingRemoval -> Bool
== :: BindingRemoval -> BindingRemoval -> Bool
$c/= :: BindingRemoval -> BindingRemoval -> Bool
/= :: BindingRemoval -> BindingRemoval -> Bool
Eq)

-- ########################################################################
-- ## Main class for collecting scope information and relevant functions ##
-- ########################################################################

class EstablishScoping t where
    {-| Traverse a 't' freshening every name (both at the binding and the use sites)
    and annotating the freshened names with either 'DisappearsBinding' or 'StaysFreeVariable'
    depending on whether the name occurs at the binding or the use site.

    In addition to that every binder should be decorated with one out-of-scope variable (annotated
    with 'StaysOutOfScopeVariable') and one in-scope one (annotated with 'DisappearsVariable').

    Note that no original name occurring in 't' should survive this procedure (and hence we don't
    care if any of the freshened names clashes with an original one as all original ones are
    supposed to be gone).

    How to provide an implementation:

    1. handle bindings with 'freshen*Name' + 'establishScopingBinder' (or similar)
    2. handle variables with 'freshen*Name' + 'registerFree'
    3. everything else is direct recursion + 'Applicative' stuff
    -}
    establishScoping :: t ann -> Quote (t NameAnn)

-- That will retraverse the same type multiple times. Should we have @referenceListVia@ as a
-- primitive instead and derive 'referenceVia' in terms of it for better performance?
-- Should we only pick an arbitrary sublist of the provided list instead of using the whole list
-- for better performance? That requires enhancing 'Reference' with @Hedgehog.Gen@ or something.
instance Reference n t => Reference [n] t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> [n] -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (t NameAnn -> [n] -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((t NameAnn -> [n] -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn)
-> ((n -> t NameAnn -> t NameAnn) -> t NameAnn -> [n] -> t NameAnn)
-> (n -> t NameAnn -> t NameAnn)
-> [n]
-> t NameAnn
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> t NameAnn -> t NameAnn) -> t NameAnn -> [n] -> t NameAnn
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr ((n -> t NameAnn -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn)
-> (n -> t NameAnn -> t NameAnn) -> [n] -> t NameAnn -> t NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg

instance Reference n t => Reference (NonEmpty n) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (forall name. ToScopedName name => name -> NameAnn)
-> [n] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg ([n] -> t NameAnn -> t NameAnn)
-> (NonEmpty n -> [n]) -> NonEmpty n -> t NameAnn -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NonEmpty.toList

-- Given that it's straightforward to provide an implementation for the method,
-- it would be nice to somehow do that generically by default.
class CollectScopeInfo t where
    {-| Collect scoping information after scoping was established and renaming was performed.

    How to provide an implementation:

    1. handle names (both bindings and variables) with 'handleSname'
    2. everything else is direct recursion + 'Monoid' stuff
    -}
    collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo

-- See Note [Example of a scoping check].
type Scoping t = (EstablishScoping t, CollectScopeInfo t)

-- | Take a constructor for a binder, a name bound by it, a sort (kind\/type), a value of that sort
-- (type\/term) and call 'establishScoping' on both the sort and its value and reassemble the
-- original binder with the annotated sort and its value, but also decorate the reassembled binder
-- with one out-of-scope variable and one in-scope one.
establishScopingBinder
    :: (Reference name value, ToScopedName name, Scoping sort, Scoping value)
    => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
    -> name
    -> sort ann
    -> value ann
    -> Quote (value NameAnn)
establishScopingBinder :: forall name (value :: * -> *) (sort :: * -> *) ann.
(Reference name value, ToScopedName name, Scoping sort,
 Scoping value) =>
(NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
-> name -> sort ann -> value ann -> Quote (value NameAnn)
establishScopingBinder NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn
binder name
name sort ann
sort value ann
value = do
    sort NameAnn
sortS <- sort ann -> Quote (sort NameAnn)
forall ann. sort ann -> Quote (sort NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping sort ann
sort
    name -> value NameAnn -> value NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope name
name (value NameAnn -> value NameAnn)
-> (value NameAnn -> value NameAnn)
-> value NameAnn
-> value NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn
binder (name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound name
name) name
name sort NameAnn
sortS (value NameAnn -> value NameAnn)
-> (value NameAnn -> value NameAnn)
-> value NameAnn
-> value NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            name -> value NameAnn -> value NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceBound name
name (value NameAnn -> value NameAnn)
-> Quote (value NameAnn) -> Quote (value NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                value ann -> Quote (value NameAnn)
forall ann. value ann -> Quote (value NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping value ann
value

-- #############################################
-- ## Checking coherence of scope information ##
-- #############################################

-- | Every kind of error thrown by the scope checking machinery at different stages.
data ScopeError
    = UnannotatedName !ScopedName
    | NameChangedItsScope
        { ScopeError -> ScopedName
_oldName :: !ScopedName
        , ScopeError -> ScopedName
_newName :: !ScopedName
        }
    | NameUnexpectedlyDisappeared
        { _oldName :: !ScopedName
        , _newName :: !ScopedName
        }
    | NameUnexpectedlyStayed !ScopedName
    | DuplicateBindersInTheInput
        { ScopeError -> Set ScopedName
_duplicateBindersLeft  :: !(Set ScopedName)
        , ScopeError -> Set ScopedName
_duplicateBindersRight :: !(Set ScopedName)
        }
    | DuplicateBindersInTheOutput !(Set ScopedName) !(Set ScopedName)
    | DisappearedBindingsDiscordWithBoundVariables
        { ScopeError -> Set ScopedName
_disappearedBindings :: !(Set ScopedName)
        , ScopeError -> Set ScopedName
_boundVariables      :: !(Set ScopedName)
        }
    | DisappearedBindingsDiscordWithOutOfScopeVariables
        { _disappearedBindings :: !(Set ScopedName)
        , ScopeError -> Set ScopedName
_outOfScopeVariables :: !(Set ScopedName)
        }
    | AppearedBindingsDiscordWithBoundVariables
        { ScopeError -> Set ScopedName
_appearedBindings :: !(Set ScopedName)
        , _boundVariables   :: !(Set ScopedName)
        }
    | DisappearedBindingsClashWithFreeVariables
        { _disappearedBindings :: !(Set ScopedName)
        , ScopeError -> Set ScopedName
_freeVariables       :: !(Set ScopedName)
        }
    | DisappearedBindingsClashWithAppearedBindings
        { ScopeError -> Set ScopedName
_disppearedBindings :: !(Set ScopedName)
        , _appearedBindings   :: !(Set ScopedName)
        }
    | AppearedBindingsClashWithFreeVariabes
        { _appearedBindings :: !(Set ScopedName)
        , _freeVariables    :: !(Set ScopedName)
        }
    deriving stock (Int -> ScopeError -> ShowS
[ScopeError] -> ShowS
ScopeError -> String
(Int -> ScopeError -> ShowS)
-> (ScopeError -> String)
-> ([ScopeError] -> ShowS)
-> Show ScopeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeError -> ShowS
showsPrec :: Int -> ScopeError -> ShowS
$cshow :: ScopeError -> String
show :: ScopeError -> String
$cshowList :: [ScopeError] -> ShowS
showList :: [ScopeError] -> ShowS
Show)

instance Pretty ScopeError where
    pretty :: forall ann. ScopeError -> Doc ann
pretty = ScopeError -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

-- | Override the set at the provided 'ScopeEntry' to contain only the provided 'ScopedName'.
overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
key = (Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> ScopeInfo -> ScopeInfo
forall a b. Coercible a b => a -> b
coerce ((Map ScopeEntry (Set ScopedName)
  -> Map ScopeEntry (Set ScopedName))
 -> ScopeInfo -> ScopeInfo)
-> (ScopedName
    -> Map ScopeEntry (Set ScopedName)
    -> Map ScopeEntry (Set ScopedName))
-> ScopedName
-> ScopeInfo
-> ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeEntry
-> Set ScopedName
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ScopeEntry
key (Set ScopedName
 -> Map ScopeEntry (Set ScopedName)
 -> Map ScopeEntry (Set ScopedName))
-> (ScopedName -> Set ScopedName)
-> ScopedName
-> Map ScopeEntry (Set ScopedName)
-> Map ScopeEntry (Set ScopedName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopedName -> Set ScopedName
forall a. a -> Set a
Set.singleton

-- | Use a 'Stays' to handle an unchanged old name.
applyStays :: Stays -> ScopedName -> ScopeInfo
applyStays :: Stays -> ScopedName -> ScopeInfo
applyStays Stays
stays ScopedName
sname = ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
key ScopedName
sname ScopeInfo
emptyScopeInfo where
    key :: ScopeEntry
key = case Stays
stays of
        Stays
StaysOutOfScopeVariable -> ScopeEntry
StayedOutOfScopeVariables
        Stays
StaysFreeVariable       -> ScopeEntry
StayedFreeVariables

-- | Use a 'Disappears' to handle differing old and new names.
applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears Disappears
disappears ScopedName
snameOld ScopedName
snameNew =
    ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
keyNew ScopedName
snameNew (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
overrideSname ScopeEntry
keyOld ScopedName
snameOld ScopeInfo
emptyScopeInfo where
        (ScopeEntry
keyOld, ScopeEntry
keyNew) = case Disappears
disappears of
            Disappears
DisappearsBinding  -> (ScopeEntry
DisappearedBindings, ScopeEntry
AppearedBindings)
            Disappears
DisappearsVariable -> (ScopeEntry
DisappearedVariables, ScopeEntry
AppearedVariables)

-- | Use a 'NameAction' to handle an old and a new name.
applyNameAction
    :: NameAction -> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction :: NameAction
-> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction (Stays Stays
stays) ScopedName
snameOld ScopedName
snameNew
    | ScopedName
snameOld ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedName
snameNew = ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ Stays -> ScopedName -> ScopeInfo
applyStays Stays
stays ScopedName
snameOld
    | Bool
otherwise            = ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopedName -> ScopeError
NameUnexpectedlyDisappeared ScopedName
snameOld ScopedName
snameNew
applyNameAction (Disappears Disappears
disappears) ScopedName
snameOld ScopedName
snameNew
    | ScopedName
snameOld ScopedName -> ScopedName -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedName
snameNew = ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopeError
NameUnexpectedlyStayed ScopedName
snameOld
    | Bool
otherwise            = ScopeInfo -> Either ScopeError ScopeInfo
forall a b. b -> Either a b
Right (ScopeInfo -> Either ScopeError ScopeInfo)
-> ScopeInfo -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ Disappears -> ScopedName -> ScopedName -> ScopeInfo
applyDisappears Disappears
disappears ScopedName
snameOld ScopedName
snameNew

-- | Use a 'NameAnn' to handle a new name.
handleSname :: ToScopedName name => NameAnn -> name -> ScopeErrorOrInfo
handleSname :: forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann name
nameNew = Either ScopeError ScopeInfo -> ScopeErrorOrInfo
ScopeErrorOrInfo (Either ScopeError ScopeInfo -> ScopeErrorOrInfo)
-> Either ScopeError ScopeInfo -> ScopeErrorOrInfo
forall a b. (a -> b) -> a -> b
$ do
    let snameNew :: ScopedName
snameNew = name -> ScopedName
forall name. ToScopedName name => name -> ScopedName
toScopedName name
nameNew
    case NameAnn
ann of
        NameAnn
NotAName -> ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopeError
UnannotatedName ScopedName
snameNew
        NameAction NameAction
action ScopedName
snameOld ->
            if ScopedName
snameOld ScopedName -> ScopedName -> Bool
`isSameScope` ScopedName
snameNew
                then NameAction
-> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
applyNameAction NameAction
action ScopedName
snameOld ScopedName
snameNew
                else ScopeError -> Either ScopeError ScopeInfo
forall a b. a -> Either a b
Left (ScopeError -> Either ScopeError ScopeInfo)
-> ScopeError -> Either ScopeError ScopeInfo
forall a b. (a -> b) -> a -> b
$ ScopedName -> ScopedName -> ScopeError
NameChangedItsScope ScopedName
snameOld ScopedName
snameNew

symmetricDifference :: Ord a => Set a -> Set a -> Set a
symmetricDifference :: forall a. Ord a => Set a -> Set a -> Set a
symmetricDifference Set a
s Set a
t = (Set a
s Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set a
t) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` (Set a
s Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set a
t)

{-| Check that each kind of 'Set' from 'ScopeInfo' relates to all other ones in a certain way.
We start with these three relations that are based on the assumption that for each binder we add
at least one out-of-scope variable and at least one in-scope one:

1. disappeared bindings should be the same as stayed out of scope variables
     (ensures that old bindings disappear via renaming and not via removal)
2. disappeared bindings should be the same as disappeared variables
     (ensures that old names consistently disappear at the binding and use sites)
3. appeared bindings should be the same as appeared variables
     (ensures that new names consistently appear at the binding and use sites)

Once we've ensured all of that, we're left with only three sets and 3C2 equals 3,
so we only need to consider three more relations:

1. disappeared bindings should not intersect with free variables
     (an internal sanity check)
2. appeared bindings should not intersect with disappeared bindings
3. appeared bindings should not intersect with free variables

The last two ensure that no new name has an old name's unique.
-}
checkScopeInfo :: BindingRemoval -> ScopeInfo -> Either ScopeError ()
checkScopeInfo :: BindingRemoval -> ScopeInfo -> Either ScopeError ()
checkScopeInfo BindingRemoval
bindRem ScopeInfo
scopeInfo = do
    let disappearedBindings :: Set ScopedName
disappearedBindings       = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedBindings       ScopeInfo
scopeInfo
        disappearedVariables :: Set ScopedName
disappearedVariables      = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
DisappearedVariables      ScopeInfo
scopeInfo
        appearedBindings :: Set ScopedName
appearedBindings          = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedBindings          ScopeInfo
scopeInfo
        appearedVariables :: Set ScopedName
appearedVariables         = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
AppearedVariables         ScopeInfo
scopeInfo
        stayedOutOfScopeVariables :: Set ScopedName
stayedOutOfScopeVariables = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
StayedOutOfScopeVariables ScopeInfo
scopeInfo
        stayedFreeVariables :: Set ScopedName
stayedFreeVariables       = ScopeEntry -> ScopeInfo -> Set ScopedName
to ScopeEntry
StayedFreeVariables       ScopeInfo
scopeInfo
    Bool -> Either ScopeError () -> Either ScopeError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BindingRemoval
bindRem BindingRemoval -> BindingRemoval -> Bool
forall a. Eq a => a -> a -> Bool
== BindingRemoval
BindingRemovalOk) (Either ScopeError () -> Either ScopeError ())
-> Either ScopeError () -> Either ScopeError ()
forall a b. (a -> b) -> a -> b
$ do
        (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
            Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
symmetricDifference
            Set ScopedName -> Set ScopedName -> ScopeError
DisappearedBindingsDiscordWithOutOfScopeVariables
            Set ScopedName
disappearedBindings
            Set ScopedName
stayedOutOfScopeVariables
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
symmetricDifference
        Set ScopedName -> Set ScopedName -> ScopeError
DisappearedBindingsDiscordWithBoundVariables
        Set ScopedName
disappearedBindings
        Set ScopedName
disappearedVariables
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
symmetricDifference
        Set ScopedName -> Set ScopedName -> ScopeError
AppearedBindingsDiscordWithBoundVariables
        Set ScopedName
appearedBindings
        Set ScopedName
appearedVariables
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
        Set ScopedName -> Set ScopedName -> ScopeError
DisappearedBindingsClashWithFreeVariables
        Set ScopedName
disappearedBindings
        Set ScopedName
stayedFreeVariables
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
        Set ScopedName -> Set ScopedName -> ScopeError
DisappearedBindingsClashWithAppearedBindings
        Set ScopedName
appearedBindings
        Set ScopedName
disappearedBindings
    (Set ScopedName -> Set ScopedName -> Set ScopedName)
-> (Set ScopedName -> Set ScopedName -> ScopeError)
-> Set ScopedName
-> Set ScopedName
-> Either ScopeError ()
checkEmptyOn
        Set ScopedName -> Set ScopedName -> Set ScopedName
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
        Set ScopedName -> Set ScopedName -> ScopeError
AppearedBindingsClashWithFreeVariabes
        Set ScopedName
appearedBindings
        Set ScopedName
stayedFreeVariables

-- | The type of errors that the scope checking machinery returns.
data ScopeCheckError t = ScopeCheckError
    { forall (t :: * -> *). ScopeCheckError t -> t NameAnn
_input  :: !(t NameAnn)  -- ^ What got fed to the scoping check pass.
    , forall (t :: * -> *). ScopeCheckError t -> t NameAnn
_output :: !(t NameAnn)  -- ^ What got out of it.
    , forall (t :: * -> *). ScopeCheckError t -> ScopeError
_error  :: !ScopeError   -- ^ The error returned by the scoping check pass.
    }

deriving stock instance Show (t NameAnn) => Show (ScopeCheckError t)

instance PrettyBy config (t NameAnn) => PrettyBy config (ScopeCheckError t) where
    prettyBy :: forall ann. config -> ScopeCheckError t -> Doc ann
prettyBy config
config (ScopeCheckError t NameAnn
input t NameAnn
output ScopeError
err) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
        [ ScopeError -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ScopeError -> Doc ann
pretty ScopeError
err
        , Doc ann
"when checking that transformation of" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ config -> t NameAnn -> Doc ann
forall ann. config -> t NameAnn -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config t NameAnn
input Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
        , Doc ann
"to" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ config -> t NameAnn -> Doc ann
forall ann. config -> t NameAnn -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config t NameAnn
output Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
        , Doc ann
"is correct"
        ]

-- See Note [Example of a scoping check].
-- | Check if a pass respects scoping.
--
-- Returns the thing that the scoping tests run on, the result of the pass and the scope checking
-- outcome, respectively.
checkRespectsScoping
    :: Scoping t
    => BindingRemoval
    -> (t NameAnn -> t NameAnn)  -- ^ For preparation before running the scoping tests.
                                 --   Commonly, either @runQuote . rename@ or @id@.
    -> (t NameAnn -> t NameAnn)  -- ^ The runner of the pass.
    -> t ann
    -> Either (ScopeCheckError t) ()
checkRespectsScoping :: forall (t :: * -> *) ann.
Scoping t =>
BindingRemoval
-> (t NameAnn -> t NameAnn)
-> (t NameAnn -> t NameAnn)
-> t ann
-> Either (ScopeCheckError t) ()
checkRespectsScoping BindingRemoval
bindRem t NameAnn -> t NameAnn
prep t NameAnn -> t NameAnn
run t ann
thing =
    (ScopeError -> ScopeCheckError t)
-> Either ScopeError () -> Either (ScopeCheckError t) ()
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (t NameAnn -> t NameAnn -> ScopeError -> ScopeCheckError t
forall (t :: * -> *).
t NameAnn -> t NameAnn -> ScopeError -> ScopeCheckError t
ScopeCheckError t NameAnn
input t NameAnn
output) (Either ScopeError () -> Either (ScopeCheckError t) ())
-> Either ScopeError () -> Either (ScopeCheckError t) ()
forall a b. (a -> b) -> a -> b
$
        ScopeErrorOrInfo -> Either ScopeError ScopeInfo
unScopeErrorOrInfo (t NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo t NameAnn
output) Either ScopeError ScopeInfo
-> (ScopeInfo -> Either ScopeError ()) -> Either ScopeError ()
forall a b.
Either ScopeError a
-> (a -> Either ScopeError b) -> Either ScopeError b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingRemoval -> ScopeInfo -> Either ScopeError ()
checkScopeInfo BindingRemoval
bindRem
  where
    input :: t NameAnn
input  = t NameAnn -> t NameAnn
prep (t NameAnn -> t NameAnn)
-> (Quote (t NameAnn) -> t NameAnn)
-> Quote (t NameAnn)
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quote (t NameAnn) -> t NameAnn
forall a. Quote a -> a
runQuote (Quote (t NameAnn) -> t NameAnn) -> Quote (t NameAnn) -> t NameAnn
forall a b. (a -> b) -> a -> b
$ t ann -> Quote (t NameAnn)
forall ann. t ann -> Quote (t NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping t ann
thing
    output :: t NameAnn
output = t NameAnn -> t NameAnn
run t NameAnn
input