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

-- In the three instances below the added variable is always the last field of a constructor.
-- Just to be consistent.

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

-- Kinds have no names, hence the simple instance.
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

-- Kinds have no names, hence the simple instance.
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