{-# 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