{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.Core.Instance.Scoping () where
import PlutusCore.Check.Scoping
import PlutusCore.Core.Type
import PlutusCore.Name.Unique
import PlutusCore.Quote
instance tyname ~ TyName => Reference TyName (Type tyname uni) where
referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Type tyname uni NameAnn
ty = NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp NameAnn
NotAName Type tyname uni NameAnn
ty (Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Type tyname uni NameAnn -> Type tyname uni NameAnn
forall a b. (a -> b) -> a -> b
$ NameAnn -> tyname -> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname) tyname
TyName
tyname
instance tyname ~ TyName => Reference TyName (Term tyname name uni fun) where
referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Term tyname name uni fun NameAnn
term = NameAnn
-> Term tyname name uni fun NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst NameAnn
NotAName Term tyname name uni fun NameAnn
term (Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
-> Type tyname uni NameAnn -> Term tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ NameAnn -> tyname -> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname) tyname
TyName
tyname
instance name ~ Name => Reference Name (Term tyname name uni fun) where
referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> Name
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg Name
name Term tyname name uni fun NameAnn
term = NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply NameAnn
NotAName Term tyname name uni fun NameAnn
term (Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ NameAnn -> name -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg Name
name) name
Name
name
instance EstablishScoping Kind where
establishScoping :: forall ann. Kind ann -> Quote (Kind NameAnn)
establishScoping Kind ann
kind = Kind NameAnn -> Quote (Kind NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind NameAnn -> Quote (Kind NameAnn))
-> Kind NameAnn -> Quote (Kind NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn
NotAName NameAnn -> Kind ann -> Kind NameAnn
forall a b. a -> Kind b -> Kind a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Kind ann
kind
instance CollectScopeInfo Kind where
collectScopeInfo :: Kind NameAnn -> ScopeErrorOrInfo
collectScopeInfo Kind NameAnn
_ = ScopeErrorOrInfo
forall a. Monoid a => a
mempty
instance tyname ~ TyName => EstablishScoping (Type tyname uni) where
establishScoping :: forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
establishScoping (TyLam ann
_ tyname
nameDup Kind ann
kind Type tyname uni ann
ty) = do
TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
(NameAnn
-> tyname
-> Kind NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn)
-> tyname
-> Kind ann
-> Type tyname uni ann
-> Quote (Type tyname uni NameAnn)
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
-> tyname
-> Kind NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam tyname
TyName
name Kind ann
kind Type tyname uni ann
ty
establishScoping (TyForall ann
_ tyname
nameDup Kind ann
kind Type tyname uni ann
ty) = do
TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
(NameAnn
-> tyname
-> Kind NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn)
-> tyname
-> Kind ann
-> Type tyname uni ann
-> Quote (Type tyname uni NameAnn)
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
-> tyname
-> Kind NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall tyname
TyName
name Kind ann
kind Type tyname uni ann
ty
establishScoping (TyIFix ann
_ Type tyname uni ann
pat Type tyname uni ann
arg) =
NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix NameAnn
NotAName (Type tyname uni NameAnn
-> Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
pat QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
arg
establishScoping (TyApp ann
_ Type tyname uni ann
fun Type tyname uni ann
arg) =
NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp NameAnn
NotAName (Type tyname uni NameAnn
-> Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
fun QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
arg
establishScoping (TyFun ann
_ Type tyname uni ann
dom Type tyname uni ann
cod) =
NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun NameAnn
NotAName (Type tyname uni NameAnn
-> Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
dom QuoteT
Identity (Type tyname uni NameAnn -> Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
-> Quote (Type tyname uni NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
cod
establishScoping (TyVar ann
_ tyname
nameDup) = do
TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn))
-> Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> tyname -> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerFree TyName
name) tyname
TyName
name
establishScoping (TyBuiltin ann
_ SomeTypeIn uni
someUni) = Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn))
-> Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> SomeTypeIn uni -> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin NameAnn
NotAName SomeTypeIn uni
someUni
establishScoping (TySOP ann
_ [[Type tyname uni ann]]
tyls) =
NameAnn -> [[Type tyname uni NameAnn]] -> Type tyname uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP NameAnn
NotAName ([[Type tyname uni NameAnn]] -> Type tyname uni NameAnn)
-> QuoteT Identity [[Type tyname uni NameAnn]]
-> Quote (Type tyname uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Type tyname uni ann]
-> QuoteT Identity [Type tyname uni NameAnn])
-> [[Type tyname uni ann]]
-> QuoteT Identity [[Type tyname uni NameAnn]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (([Type tyname uni ann]
-> QuoteT Identity [Type tyname uni NameAnn])
-> [[Type tyname uni ann]]
-> QuoteT Identity [[Type tyname uni NameAnn]])
-> ((Type tyname uni ann -> Quote (Type tyname uni NameAnn))
-> [Type tyname uni ann]
-> QuoteT Identity [Type tyname uni NameAnn])
-> (Type tyname uni ann -> Quote (Type tyname uni NameAnn))
-> [[Type tyname uni ann]]
-> QuoteT Identity [[Type tyname uni NameAnn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> Quote (Type tyname uni NameAnn))
-> [Type tyname uni ann]
-> QuoteT Identity [Type tyname uni NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall ann. Type tyname uni ann -> Quote (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping [[Type tyname uni ann]]
tyls
instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where
establishScoping :: forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
establishScoping (LamAbs ann
_ name
nameDup Type tyname uni ann
ty Term tyname name uni fun ann
body) = do
Name
name <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName name
Name
nameDup
(NameAnn
-> name
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
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
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs name
Name
name Type tyname uni ann
ty Term tyname name uni fun ann
body
establishScoping (TyAbs ann
_ tyname
nameDup Kind ann
kind Term tyname name uni fun ann
body) = do
TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
(NameAnn
-> tyname
-> Kind NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
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
-> tyname
-> Kind NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs tyname
TyName
name Kind ann
kind Term tyname name uni fun ann
body
establishScoping (IWrap ann
_ Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term) =
NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap NameAnn
NotAName (Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
Identity
(Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
pat QuoteT
Identity
(Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
Identity
(Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
arg QuoteT
Identity
(Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term
establishScoping (Apply ann
_ Term tyname name uni fun ann
fun Term tyname name uni fun ann
arg) =
NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply NameAnn
NotAName (Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> QuoteT
Identity
(Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
fun QuoteT
Identity
(Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
arg
establishScoping (Unwrap ann
_ Term tyname name uni fun ann
term) = NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap NameAnn
NotAName (Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term
establishScoping (Error ann
_ Type tyname uni ann
ty) = NameAnn
-> Type tyname uni NameAnn -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error NameAnn
NotAName (Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty
establishScoping (TyInst ann
_ Term tyname name uni fun ann
term Type tyname uni ann
ty) =
NameAnn
-> Term tyname name uni fun NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst NameAnn
NotAName (Term tyname name uni fun NameAnn
-> Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> QuoteT
Identity
(Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term QuoteT
Identity
(Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty
establishScoping (Var ann
_ name
nameDup) = do
Name
name <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName name
Name
nameDup
Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> name -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerFree Name
name) name
Name
name
establishScoping (Constant ann
_ Some (ValueOf uni)
con) = Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> Some (ValueOf uni) -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant NameAnn
NotAName Some (ValueOf uni)
con
establishScoping (Builtin ann
_ fun
bi) = Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> fun -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin NameAnn
NotAName fun
bi
establishScoping (Constr ann
_ Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es) =
NameAnn
-> Type tyname uni NameAnn
-> Word64
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr NameAnn
NotAName (Type tyname uni NameAnn
-> Word64
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
Identity
(Word64
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty QuoteT
Identity
(Word64
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity Word64
-> QuoteT
Identity
([Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> QuoteT Identity Word64
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i QuoteT
Identity
([Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity [Term tyname name uni fun NameAnn]
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn))
-> [Term tyname name uni fun ann]
-> QuoteT Identity [Term tyname name uni fun NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping [Term tyname name uni fun ann]
es
establishScoping (Case ann
_ Type tyname uni ann
ty Term tyname name uni fun ann
a [Term tyname name uni fun ann]
es) =
NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case NameAnn
NotAName (Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
Identity
(Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty QuoteT
Identity
(Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> QuoteT
Identity
([Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
a QuoteT
Identity
([Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity [Term tyname name uni fun NameAnn]
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn))
-> [Term tyname name uni fun ann]
-> QuoteT Identity [Term tyname name uni fun NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping [Term tyname name uni fun ann]
es
instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where
establishScoping :: forall ann.
Program tyname name uni fun ann
-> Quote (Program tyname name uni fun NameAnn)
establishScoping (Program ann
_ Version
ver Term tyname name uni fun ann
term) =
NameAnn
-> Version
-> Term tyname name uni fun NameAnn
-> Program tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program NameAnn
NotAName Version
ver (Term tyname name uni fun NameAnn
-> Program tyname name uni fun NameAnn)
-> QuoteT Identity (Term tyname name uni fun NameAnn)
-> Quote (Program tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> QuoteT Identity (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> QuoteT Identity (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term
instance tyname ~ TyName => CollectScopeInfo (Type tyname uni) where
collectScopeInfo :: Type tyname uni NameAnn -> ScopeErrorOrInfo
collectScopeInfo (TyLam NameAnn
ann tyname
name Kind NameAnn
kind Type tyname uni NameAnn
ty) =
NameAnn -> tyname -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann tyname
name ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Kind NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Kind NameAnn
kind ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty
collectScopeInfo (TyForall NameAnn
ann tyname
name Kind NameAnn
kind Type tyname uni NameAnn
ty) =
NameAnn -> tyname -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann tyname
name ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Kind NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Kind NameAnn
kind ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty
collectScopeInfo (TyIFix NameAnn
_ Type tyname uni NameAnn
pat Type tyname uni NameAnn
arg) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
pat ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
arg
collectScopeInfo (TyApp NameAnn
_ Type tyname uni NameAnn
fun Type tyname uni NameAnn
arg) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
fun ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
arg
collectScopeInfo (TyFun NameAnn
_ Type tyname uni NameAnn
dom Type tyname uni NameAnn
cod) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
dom ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
cod
collectScopeInfo (TyVar NameAnn
ann tyname
name) = NameAnn -> tyname -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann tyname
name
collectScopeInfo (TyBuiltin NameAnn
_ SomeTypeIn uni
_) = ScopeErrorOrInfo
forall a. Monoid a => a
mempty
collectScopeInfo (TySOP NameAnn
_ [[Type tyname uni NameAnn]]
tyls) = (([Type tyname uni NameAnn] -> ScopeErrorOrInfo)
-> [[Type tyname uni NameAnn]] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (([Type tyname uni NameAnn] -> ScopeErrorOrInfo)
-> [[Type tyname uni NameAnn]] -> ScopeErrorOrInfo)
-> ((Type tyname uni NameAnn -> ScopeErrorOrInfo)
-> [Type tyname uni NameAnn] -> ScopeErrorOrInfo)
-> (Type tyname uni NameAnn -> ScopeErrorOrInfo)
-> [[Type tyname uni NameAnn]]
-> ScopeErrorOrInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni NameAnn -> ScopeErrorOrInfo)
-> [Type tyname uni NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap) Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [[Type tyname uni NameAnn]]
tyls
instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Term tyname name uni fun) where
collectScopeInfo :: Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (LamAbs NameAnn
ann name
name Type tyname uni NameAnn
ty Term tyname name uni fun NameAnn
body) =
NameAnn -> name -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann name
name ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
body
collectScopeInfo (TyAbs NameAnn
ann tyname
name Kind NameAnn
kind Term tyname name uni fun NameAnn
body) =
NameAnn -> tyname -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann tyname
name ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Kind NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Kind NameAnn
kind ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
body
collectScopeInfo (IWrap NameAnn
_ Type tyname uni NameAnn
pat Type tyname uni NameAnn
arg Term tyname name uni fun NameAnn
term) =
Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
pat ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
arg ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
term
collectScopeInfo (Apply NameAnn
_ Term tyname name uni fun NameAnn
fun Term tyname name uni fun NameAnn
arg) = Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
fun ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
arg
collectScopeInfo (Unwrap NameAnn
_ Term tyname name uni fun NameAnn
term) = Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
term
collectScopeInfo (Error NameAnn
_ Type tyname uni NameAnn
ty) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty
collectScopeInfo (TyInst NameAnn
_ Term tyname name uni fun NameAnn
term Type tyname uni NameAnn
ty) = Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
term ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty
collectScopeInfo (Var NameAnn
ann name
name) = NameAnn -> name -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann name
name
collectScopeInfo (Constant NameAnn
_ Some (ValueOf uni)
_) = ScopeErrorOrInfo
forall a. Monoid a => a
mempty
collectScopeInfo (Builtin NameAnn
_ fun
_) = ScopeErrorOrInfo
forall a. Monoid a => a
mempty
collectScopeInfo (Constr NameAnn
_ Type tyname uni NameAnn
ty Word64
_ [Term tyname name uni fun NameAnn]
es) =
Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> [Term tyname name uni fun NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [Term tyname name uni fun NameAnn]
es
collectScopeInfo (Case NameAnn
_ Type tyname uni NameAnn
ty Term tyname name uni fun NameAnn
arg [Term tyname name uni fun NameAnn]
cs) =
Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
arg ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> [Term tyname name uni fun NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [Term tyname name uni fun NameAnn]
cs
instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Program tyname name uni fun) where
collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Program NameAnn
_ Version
_ Term tyname name uni fun NameAnn
term) = Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
term