{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} module PlutusCore.Check.Scoping where import PlutusCore.Name import PlutusCore.Quote import Control.Monad.Except 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 {- 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 (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 showList :: [ScopedName] -> ShowS $cshowList :: [ScopedName] -> ShowS show :: ScopedName -> String $cshow :: ScopedName -> String showsPrec :: Int -> ScopedName -> ShowS $cshowsPrec :: Int -> ScopedName -> ShowS Show, ScopedName -> ScopedName -> Bool (ScopedName -> ScopedName -> Bool) -> (ScopedName -> ScopedName -> Bool) -> Eq ScopedName forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ScopedName -> ScopedName -> Bool $c/= :: ScopedName -> ScopedName -> Bool == :: ScopedName -> ScopedName -> Bool $c== :: 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 min :: ScopedName -> ScopedName -> ScopedName $cmin :: ScopedName -> ScopedName -> ScopedName max :: ScopedName -> ScopedName -> ScopedName $cmax :: ScopedName -> ScopedName -> ScopedName >= :: ScopedName -> ScopedName -> Bool $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 compare :: ScopedName -> ScopedName -> Ordering $ccompare :: ScopedName -> ScopedName -> Ordering $cp1Ord :: Eq 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 (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 showList :: [Stays] -> ShowS $cshowList :: [Stays] -> ShowS show :: Stays -> String $cshow :: Stays -> String showsPrec :: Int -> Stays -> ShowS $cshowsPrec :: Int -> 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 (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 showList :: [Disappears] -> ShowS $cshowList :: [Disappears] -> ShowS show :: Disappears -> String $cshow :: Disappears -> String showsPrec :: Int -> Disappears -> ShowS $cshowsPrec :: Int -> Disappears -> ShowS Show) -- | A name either stays or disappears. data NameAction = Stays Stays | Disappears Disappears deriving (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 showList :: [NameAction] -> ShowS $cshowList :: [NameAction] -> ShowS show :: NameAction -> String $cshow :: NameAction -> String showsPrec :: Int -> NameAction -> ShowS $cshowsPrec :: Int -> NameAction -> ShowS Show) data NameAnn = NameAction NameAction ScopedName | NotAName deriving (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 showList :: [NameAnn] -> ShowS $cshowList :: [NameAnn] -> ShowS show :: NameAnn -> String $cshow :: NameAnn -> String showsPrec :: Int -> NameAnn -> ShowS $cshowsPrec :: Int -> NameAnn -> ShowS Show) 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 :: 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 :: 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 :: 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 :: 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 :: 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 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 :: 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 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 (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 showList :: [ScopeEntry] -> ShowS $cshowList :: [ScopeEntry] -> ShowS show :: ScopeEntry -> String $cshow :: ScopeEntry -> String showsPrec :: Int -> ScopeEntry -> ShowS $cshowsPrec :: Int -> ScopeEntry -> ShowS Show, ScopeEntry -> ScopeEntry -> Bool (ScopeEntry -> ScopeEntry -> Bool) -> (ScopeEntry -> ScopeEntry -> Bool) -> Eq ScopeEntry forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ScopeEntry -> ScopeEntry -> Bool $c/= :: ScopeEntry -> ScopeEntry -> Bool == :: ScopeEntry -> ScopeEntry -> Bool $c== :: 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 min :: ScopeEntry -> ScopeEntry -> ScopeEntry $cmin :: ScopeEntry -> ScopeEntry -> ScopeEntry max :: ScopeEntry -> ScopeEntry -> ScopeEntry $cmax :: ScopeEntry -> ScopeEntry -> ScopeEntry >= :: ScopeEntry -> ScopeEntry -> Bool $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 compare :: ScopeEntry -> ScopeEntry -> Ordering $ccompare :: ScopeEntry -> ScopeEntry -> Ordering $cp1Ord :: Eq 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 { ScopeInfo -> Map ScopeEntry (Set ScopedName) unScopeInfo :: Map ScopeEntry (Set ScopedName) } deriving (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 showList :: [ScopeInfo] -> ShowS $cshowList :: [ScopeInfo] -> ShowS show :: ScopeInfo -> String $cshow :: ScopeInfo -> String showsPrec :: Int -> ScopeInfo -> ShowS $cshowsPrec :: Int -> ScopeInfo -> ShowS Show) -- | 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. checkEmpty :: (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty :: (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError err Set ScopedName s = 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 s) (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 -> ScopeError err Set ScopedName s -- | Merge two 'ScopeInfo's checking that they 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 duplicateDisappearedBindings :: Set ScopedName duplicateDisappearedBindings = Set ScopedName disappearedBindings1 Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `Set.intersection` Set ScopedName disappearedBindings2 duplicateAppearedBindings :: Set ScopedName duplicateAppearedBindings = Set ScopedName appearedBindings1 Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `Set.intersection` Set ScopedName appearedBindings2 (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError DuplicateBindersInTheInput Set ScopedName duplicateDisappearedBindings (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError DuplicateBindersInTheOutput Set ScopedName duplicateAppearedBindings 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 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 -- @newtype@-ing it for the sake of providing very convenient 'Semigroup' and 'Monoid' instances. newtype ScopeErrorOrInfo = ScopeErrorOrInfo -- We might want to use @Validation@ or something instead of 'Either'. { ScopeErrorOrInfo -> Either ScopeError ScopeInfo unScopeErrorOrInfo :: Either ScopeError ScopeInfo } 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 (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 -- ######################################################################## -- ## 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 (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 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 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 :: (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 (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 (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 ScopedName ScopedName | NameUnexpectedlyDisappeared ScopedName ScopedName | NameUnexpectedlyStayed ScopedName | DuplicateBindersInTheInput (Set ScopedName) | DuplicateBindersInTheOutput (Set ScopedName) | OldBindingsDiscordWithBoundVariables (Set ScopedName) | OldBindingsDiscordWithOutOfScopeVariables (Set ScopedName) | NewBindingsDiscordWithBoundVariables (Set ScopedName) | OldBindingsClashWithFreeVariables (Set ScopedName) | OldBindingsClashWithNewBindings (Set ScopedName) | NewBindingsClashWithFreeVariabes (Set ScopedName) deriving (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 showList :: [ScopeError] -> ShowS $cshowList :: [ScopeError] -> ShowS show :: ScopeError -> String $cshow :: ScopeError -> String showsPrec :: Int -> ScopeError -> ShowS $cshowsPrec :: Int -> ScopeError -> ShowS Show) -- | 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 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 :: 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 :: 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 (an internal sanity check) 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 :: ScopeInfo -> Either ScopeError () checkScopeInfo :: ScopeInfo -> Either ScopeError () checkScopeInfo 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 (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError OldBindingsDiscordWithOutOfScopeVariables (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `symmetricDifference` Set ScopedName stayedOutOfScopeVariables (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError OldBindingsDiscordWithBoundVariables (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `symmetricDifference` Set ScopedName disappearedVariables (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError NewBindingsDiscordWithBoundVariables (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName appearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `symmetricDifference` Set ScopedName appearedVariables (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError OldBindingsClashWithFreeVariables (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName disappearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `Set.intersection` Set ScopedName stayedFreeVariables (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError OldBindingsClashWithNewBindings (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName appearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `Set.intersection` Set ScopedName disappearedBindings (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () checkEmpty Set ScopedName -> ScopeError NewBindingsClashWithFreeVariabes (Set ScopedName -> Either ScopeError ()) -> Set ScopedName -> Either ScopeError () forall a b. (a -> b) -> a -> b $ Set ScopedName appearedBindings Set ScopedName -> Set ScopedName -> Set ScopedName forall a. Ord a => Set a -> Set a -> Set a `Set.intersection` Set ScopedName stayedFreeVariables -- See Note [Example of a scoping check]. -- | Check if a renamer respects scoping. checkRespectsScoping :: Scoping t => (t NameAnn -> t NameAnn) -> t ann -> Either ScopeError () checkRespectsScoping :: (t NameAnn -> t NameAnn) -> t ann -> Either ScopeError () checkRespectsScoping t NameAnn -> t NameAnn ren = ScopeInfo -> Either ScopeError () checkScopeInfo (ScopeInfo -> Either ScopeError ()) -> (t ann -> Either ScopeError ScopeInfo) -> t ann -> Either ScopeError () forall (m :: * -> *) b c a. Monad m => (b -> m c) -> (a -> m b) -> a -> m c <=< ScopeErrorOrInfo -> Either ScopeError ScopeInfo unScopeErrorOrInfo (ScopeErrorOrInfo -> Either ScopeError ScopeInfo) -> (t ann -> ScopeErrorOrInfo) -> t ann -> Either ScopeError ScopeInfo forall b c a. (b -> c) -> (a -> b) -> a -> c . t NameAnn -> ScopeErrorOrInfo forall (t :: * -> *). CollectScopeInfo t => t NameAnn -> ScopeErrorOrInfo collectScopeInfo (t NameAnn -> ScopeErrorOrInfo) -> (t ann -> t NameAnn) -> t ann -> ScopeErrorOrInfo forall b c a. (b -> c) -> (a -> b) -> a -> c . t NameAnn -> t NameAnn ren (t NameAnn -> t NameAnn) -> (t ann -> t NameAnn) -> t ann -> 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) -> (t ann -> Quote (t NameAnn)) -> t ann -> t NameAnn forall b c a. (b -> c) -> (a -> b) -> a -> c . t ann -> Quote (t NameAnn) forall (t :: * -> *) ann. EstablishScoping t => t ann -> Quote (t NameAnn) establishScoping