{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}

module PlutusCore.Core.Instance.Scoping () where

import PlutusCore.Check.Scoping
import PlutusCore.Core.Type
import PlutusCore.Name
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

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

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

-- Kinds have no names, hence the simple instance.
instance EstablishScoping Kind where
    establishScoping :: Kind ann -> Quote (Kind NameAnn)
establishScoping Kind ann
kind = Kind NameAnn -> Quote (Kind NameAnn)
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 (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 :: 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
name Kind ann
kind Type tyname uni ann
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
name Kind ann
kind Type tyname uni ann
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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (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
name
    establishScoping (TyBuiltin ann
_ SomeTypeIn uni
fun) = Type tyname uni NameAnn -> Quote (Type tyname uni NameAnn)
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
fun

instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where
    establishScoping :: 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 Type tyname uni ann
ty Term tyname name uni fun ann
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
name Kind ann
kind Term tyname name uni fun ann
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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (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 (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 (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 (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 (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 (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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 (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
    establishScoping (Constant ann
_ Some (ValueOf uni)
con) = Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
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 (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

instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where
    establishScoping :: Program tyname name uni fun ann
-> Quote (Program tyname name uni fun NameAnn)
establishScoping (Program ann
_ Version ann
ver Term tyname name uni fun ann
term) =
        NameAnn
-> Version NameAnn
-> Term tyname name uni fun NameAnn
-> Program tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version ann
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program NameAnn
NotAName (NameAnn
NotAName NameAnn -> Version ann -> Version NameAnn
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Version ann
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 (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

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

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Program tyname name uni fun) where
    collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Program NameAnn
_ Version 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