{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# OPTIONS_GHC -Wno-orphans       #-}
module PlutusIR.Core.Instance.Scoping where

import PlutusIR.Core.Type

import PlutusCore.Check.Scoping
import PlutusCore.MkPlc
import PlutusCore.Quote

import Data.Foldable
import Data.List.NonEmpty (NonEmpty (..), (<|))
import Data.List.NonEmpty qualified as NonEmpty
import Data.Traversable

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 a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
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 a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a.
a -> name -> Term tyname name uni fun a
Var (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg Name
name) Name
name

instance tyname ~ TyName => Reference TyName (VarDecl tyname name uni fun) where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> VarDecl tyname name uni fun NameAnn
-> VarDecl tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname (VarDecl NameAnn
ann name
varName Type tyname uni NameAnn
ty) =
        NameAnn
-> name
-> Type tyname uni NameAnn
-> VarDecl tyname name uni fun NameAnn
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl NameAnn
ann name
varName (Type tyname uni NameAnn -> VarDecl tyname name uni fun NameAnn)
-> Type tyname uni NameAnn -> VarDecl tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Type tyname uni NameAnn
ty

-- | Scoping for data types is hard, so we employ some extra paranoia and reference the provided
-- 'TyName' in the type of every single constructor, and also apply the final head to that 'TyName'.
instance tyname ~ TyName => Reference TyName (Datatype tyname name uni fun) where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Datatype tyname name uni fun NameAnn
-> Datatype tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname (Datatype NameAnn
dataAnn TyVarDecl tyname NameAnn
dataDecl [TyVarDecl tyname NameAnn]
params name
matchName [VarDecl tyname name uni fun NameAnn]
constrs) =
        NameAnn
-> TyVarDecl tyname NameAnn
-> [TyVarDecl tyname NameAnn]
-> name
-> [VarDecl tyname name uni fun NameAnn]
-> Datatype tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype NameAnn
dataAnn TyVarDecl tyname NameAnn
dataDecl [TyVarDecl tyname NameAnn]
params name
matchName ([VarDecl tyname name uni fun NameAnn]
 -> Datatype tyname name uni fun NameAnn)
-> [VarDecl tyname name uni fun NameAnn]
-> Datatype tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (VarDecl TyName name uni fun NameAnn
 -> VarDecl TyName name uni fun NameAnn)
-> [VarDecl TyName name uni fun NameAnn]
-> [VarDecl TyName name uni fun NameAnn]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl TyName name uni fun NameAnn
-> VarDecl TyName name uni fun NameAnn
goConstr [VarDecl tyname name uni fun NameAnn]
[VarDecl TyName name uni fun NameAnn]
constrs where
            tyVar :: Type TyName uni NameAnn
tyVar = 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

            goConstr :: VarDecl TyName name uni fun NameAnn
-> VarDecl TyName name uni fun NameAnn
goConstr (VarDecl NameAnn
ann name
constrName Type TyName uni NameAnn
constrTy) = NameAnn
-> name
-> Type TyName uni NameAnn
-> VarDecl TyName name uni fun NameAnn
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl NameAnn
ann name
constrName (Type TyName uni NameAnn -> VarDecl TyName name uni fun NameAnn)
-> Type TyName uni NameAnn -> VarDecl TyName name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ Type TyName uni NameAnn -> Type TyName uni NameAnn
goSpine Type TyName uni NameAnn
constrTy

            goSpine :: Type TyName uni NameAnn -> Type TyName uni NameAnn
goSpine (TyForall NameAnn
ann TyName
name Kind NameAnn
kind Type TyName uni NameAnn
ty) = 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 NameAnn
ann TyName
name Kind NameAnn
kind (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn -> Type TyName uni NameAnn
forall a b. (a -> b) -> a -> b
$ Type TyName uni NameAnn -> Type TyName uni NameAnn
goSpine Type TyName uni NameAnn
ty
            goSpine (TyFun NameAnn
ann Type TyName uni NameAnn
dom Type TyName uni NameAnn
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
ann Type TyName uni NameAnn
dom (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn -> Type TyName uni NameAnn
forall a b. (a -> b) -> a -> b
$ Type TyName uni NameAnn -> Type TyName uni NameAnn
goSpine Type TyName uni NameAnn
cod
            goSpine 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
TyFun NameAnn
NotAName Type TyName uni NameAnn
tyVar (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn -> Type TyName uni NameAnn
forall a b. (a -> b) -> a -> b
$ Type TyName uni NameAnn -> Type TyName uni NameAnn
goResult Type TyName uni NameAnn
ty

            goResult :: Type TyName uni NameAnn -> Type TyName uni NameAnn
goResult (TyApp NameAnn
ann Type TyName uni NameAnn
fun Type TyName uni NameAnn
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
ann (Type TyName uni NameAnn -> Type TyName uni NameAnn
goResult Type TyName uni NameAnn
fun) Type TyName uni NameAnn
arg
            goResult 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
tyVar

instance tyname ~ TyName => Reference TyName (Binding tyname name uni fun) where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Binding tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname (TermBind NameAnn
ann Strictness
strictness VarDecl tyname name uni fun NameAnn
varDecl Term tyname name uni fun NameAnn
term) =
        NameAnn
-> Strictness
-> VarDecl tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind NameAnn
ann Strictness
strictness ((forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> VarDecl tyname name uni fun NameAnn
-> VarDecl tyname name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname VarDecl tyname name uni fun NameAnn
varDecl) (Term tyname name uni fun NameAnn
 -> Binding tyname name uni fun NameAnn)
-> Term tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Term tyname name uni fun NameAnn
term
    referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname (TypeBind NameAnn
ann TyVarDecl tyname NameAnn
tyVarDecl Type tyname uni NameAnn
ty) =
        NameAnn
-> TyVarDecl tyname NameAnn
-> Type tyname uni NameAnn
-> Binding tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind NameAnn
ann TyVarDecl tyname NameAnn
tyVarDecl (Type tyname uni NameAnn -> Binding tyname name uni fun NameAnn)
-> Type tyname uni NameAnn -> Binding tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Type tyname uni NameAnn
ty
    referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname (DatatypeBind NameAnn
ann Datatype tyname name uni fun NameAnn
datatype) =
        NameAnn
-> Datatype tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind NameAnn
ann (Datatype tyname name uni fun NameAnn
 -> Binding tyname name uni fun NameAnn)
-> Datatype tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Datatype tyname name uni fun NameAnn
-> Datatype tyname name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Datatype tyname name uni fun NameAnn
datatype

-- | Unlike other 'Reference' instances this one does not guarantee that the name will actually be
-- referenced, but it's too convenient to have this instance to give up on it, without it would be
-- awkward to express \"reference this binding in this thing\".
instance name ~ Name => Reference Name (Binding tyname name uni fun) where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> Name
-> Binding tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg Name
name (TermBind NameAnn
ann Strictness
strictness VarDecl tyname name uni fun NameAnn
varDecl Term tyname name uni fun NameAnn
term) =
        NameAnn
-> Strictness
-> VarDecl tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind NameAnn
ann Strictness
strictness VarDecl tyname name uni fun NameAnn
varDecl (Term tyname name uni fun NameAnn
 -> Binding tyname name uni fun NameAnn)
-> Term tyname name uni fun NameAnn
-> Binding tyname name uni fun NameAnn
forall a b. (a -> b) -> a -> b
$ (forall name. ToScopedName name => name -> NameAnn)
-> Name
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg Name
name Term tyname name uni fun NameAnn
term
    referenceVia forall name. ToScopedName name => name -> NameAnn
_ Name
_ typeBind :: Binding tyname name uni fun NameAnn
typeBind@TypeBind{} = Binding tyname name uni fun NameAnn
typeBind
    referenceVia forall name. ToScopedName name => name -> NameAnn
_ Name
_ datatypeBind :: Binding tyname name uni fun NameAnn
datatypeBind@DatatypeBind{} = Binding tyname name uni fun NameAnn
datatypeBind

instance Reference tyname t => Reference (TyVarDecl tyname ann) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyVarDecl tyname ann -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (forall name. ToScopedName name => name -> NameAnn)
-> tyname -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg (tyname -> t NameAnn -> t NameAnn)
-> (TyVarDecl tyname ann -> tyname)
-> TyVarDecl tyname ann
-> t NameAnn
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl tyname ann -> tyname
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName

instance Reference name t => Reference (VarDecl tyname name uni fun ann) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> VarDecl tyname name uni fun ann -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg = (forall name. ToScopedName name => name -> NameAnn)
-> name -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg (name -> t NameAnn -> t NameAnn)
-> (VarDecl tyname name uni fun ann -> name)
-> VarDecl tyname name uni fun ann
-> t NameAnn
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni fun ann -> name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName

instance (Reference TyName t, Reference Name t) => Reference (Datatype TyName Name uni fun ann) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> Datatype TyName Name uni fun ann -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg (Datatype ann
_ TyVarDecl TyName ann
dataDecl [TyVarDecl TyName ann]
params Name
matchName [VarDecl TyName Name uni fun ann]
constrs)
        = (forall name. ToScopedName name => name -> NameAnn)
-> TyVarDecl TyName ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyVarDecl TyName ann
dataDecl
        -- Parameters of a data type are not visible outside of the data type no matter what.
        (t NameAnn -> t NameAnn)
-> (t NameAnn -> t NameAnn) -> t NameAnn -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyVarDecl TyName ann] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope [TyVarDecl TyName ann]
params
        (t NameAnn -> t NameAnn)
-> (t NameAnn -> t NameAnn) -> t NameAnn -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> Name -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg Name
matchName
        (t NameAnn -> t NameAnn)
-> (t NameAnn -> t NameAnn) -> t NameAnn -> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> [VarDecl TyName Name uni fun ann] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg [VarDecl TyName Name uni fun ann]
constrs

instance (Reference TyName t, Reference Name t) => Reference (Binding TyName Name uni fun ann) t where
    referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> Binding TyName Name uni fun ann -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg (TermBind ann
_ Strictness
_ VarDecl TyName Name uni fun ann
varDecl Term TyName Name uni fun ann
_)  = (forall name. ToScopedName name => name -> NameAnn)
-> VarDecl TyName Name uni fun ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg VarDecl TyName Name uni fun ann
varDecl
    referenceVia forall name. ToScopedName name => name -> NameAnn
reg (TypeBind ann
_ TyVarDecl TyName ann
tyVarDecl Type TyName uni ann
_)  = (forall name. ToScopedName name => name -> NameAnn)
-> TyVarDecl TyName ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg TyVarDecl TyName ann
tyVarDecl
    referenceVia forall name. ToScopedName name => name -> NameAnn
reg (DatatypeBind ann
_ Datatype TyName Name uni fun ann
datatype) = (forall name. ToScopedName name => name -> NameAnn)
-> Datatype TyName Name uni fun ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg Datatype TyName Name uni fun ann
datatype

-- | Establish scoping for each of the parameters of a datatype by only annotating every parameter
-- with 'introduceBound'.
establishScopingParams :: [TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn]
establishScopingParams :: [TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn]
establishScopingParams =
    (TyVarDecl TyName ann
 -> QuoteT Identity (TyVarDecl TyName NameAnn))
-> [TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((TyVarDecl TyName ann
  -> QuoteT Identity (TyVarDecl TyName NameAnn))
 -> [TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn])
-> (TyVarDecl TyName ann
    -> QuoteT Identity (TyVarDecl TyName NameAnn))
-> [TyVarDecl TyName ann]
-> Quote [TyVarDecl TyName NameAnn]
forall a b. (a -> b) -> a -> b
$ \(TyVarDecl ann
_ TyName
paramNameDup Kind ann
paramKind) -> do
        TyName
paramName <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName TyName
paramNameDup
        NameAnn -> TyName -> Kind NameAnn -> TyVarDecl TyName NameAnn
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound TyName
paramName) TyName
paramName (Kind NameAnn -> TyVarDecl TyName NameAnn)
-> QuoteT Identity (Kind NameAnn)
-> QuoteT Identity (TyVarDecl TyName NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind ann -> QuoteT Identity (Kind NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Kind ann
paramKind

-- See Note [Weird IR data types].
{- | Establish scoping for the type of a constructor. The updated constructor expects an argument
of the \"the data type applied to all its parameters\" type (that argument is the last one) and
always returns that exact type as a result. For example, this functions turns the following
generated type of constructor

    integer -> a -> <a_non_->_type>

into

    integer -> a -> D a b -> D a b

assuming the constructor is supposed to construct a data type @D@ parameterized by two parameters
@a@ and @b@. Note that @<a_non_->_type>@ can be anything as the generator is allowed to generate
mess such as a constructor not actually constructing a value of the data type.

Whether the name of the data type is referenced as in-scope or out-of-scope one in the types of
arguments of constructors is controlled by the first argument, which ultimately depends on the
recursivity of the data type.
-}
establishScopingConstrTy
    :: (TyName -> NameAnn)
    -> TyName
    -> [TyVarDecl TyName NameAnn]
    -> Type TyName uni ann
    -> Quote (Type TyName uni NameAnn)
establishScopingConstrTy :: (TyName -> NameAnn)
-> TyName
-> [TyVarDecl TyName NameAnn]
-> Type TyName uni ann
-> Quote (Type TyName uni NameAnn)
establishScopingConstrTy TyName -> NameAnn
regSelf TyName
dataName [TyVarDecl TyName NameAnn]
params = Type TyName uni ann -> Quote (Type TyName uni NameAnn)
goSpine where
    toDataAppliedToParams :: (TyName -> NameAnn) -> Type TyName uni NameAnn
toDataAppliedToParams TyName -> NameAnn
reg
        = NameAnn
-> Type TyName uni NameAnn
-> [Type TyName uni NameAnn]
-> Type TyName uni NameAnn
forall ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
mkIterTyApp NameAnn
NotAName (NameAnn -> TyName -> Type TyName uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (TyName -> NameAnn
reg TyName
dataName) TyName
dataName)
        ([Type TyName uni NameAnn] -> Type TyName uni NameAnn)
-> [Type TyName uni NameAnn] -> Type TyName uni NameAnn
forall a b. (a -> b) -> a -> b
$ (TyVarDecl TyName NameAnn -> Type TyName uni NameAnn)
-> [TyVarDecl TyName NameAnn] -> [Type TyName uni NameAnn]
forall a b. (a -> b) -> [a] -> [b]
map (\(TyVarDecl NameAnn
_ TyName
name Kind NameAnn
_) -> 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
registerBound TyName
name) TyName
name) [TyVarDecl TyName NameAnn]
params

    goSpine :: Type TyName uni ann -> Quote (Type TyName uni NameAnn)
goSpine (TyForall ann
_ TyName
nameDup Kind ann
kindDup Type TyName uni ann
ty) = do
        -- Similar to 'establishScopingBinder', but uses 'TyFun' rather than whatever 'registerVia'
        -- uses in order not to break the invariants described in Note [Weird IR data types].
        -- Also calls 'goSpine' recursively rather than 'establishScoping'.
        TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName TyName
nameDup
        Kind NameAnn
kind <- Kind ann -> QuoteT Identity (Kind NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Kind ann
kindDup
        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 (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
registerOutOfScope TyName
name) TyName
name) (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn
-> Type TyName uni NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            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 -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound TyName
name) TyName
name Kind NameAnn
kind (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn
-> Type TyName uni NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                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 (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
registerBound TyName
name) TyName
name) (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Quote (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 -> Quote (Type TyName uni NameAnn)
goSpine Type TyName uni ann
ty
    goSpine (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)
goSpine Type TyName uni ann
cod
    goSpine Type TyName uni ann
_                 =
        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 -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn
-> Quote (Type TyName uni NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ((TyName -> NameAnn) -> Type TyName uni NameAnn
toDataAppliedToParams TyName -> NameAnn
regSelf) (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
$ (TyName -> NameAnn) -> Type TyName uni NameAnn
toDataAppliedToParams TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerBound

-- | Establish scoping for all constructors of a data type by establishing scoping for each of them
-- individually. If there are no constructors, then a dummy one is added, because we need to
-- maintain the invariant that every binding is referenced as an in-scope one somewhere and the only
-- place where parameters of a data type can be referenced this way is a constructor of that data
-- type.
establishScopingConstrs
    :: (TyName -> NameAnn)
    -> ann
    -> TyName
    -> [TyVarDecl TyName NameAnn]
    -> [VarDecl TyName Name uni fun ann]
    -> Quote [VarDecl TyName Name uni fun NameAnn]
establishScopingConstrs :: (TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni fun ann]
-> Quote [VarDecl TyName Name uni fun NameAnn]
establishScopingConstrs TyName -> NameAnn
regSelf ann
dataAnn TyName
dataName [TyVarDecl TyName NameAnn]
params [VarDecl TyName Name uni fun ann]
constrsPossiblyEmpty = do
    Name
cons0Name <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"cons0"
    let cons0 :: VarDecl TyName Name uni fun ann
cons0 = ann
-> Name -> Type TyName uni ann -> VarDecl TyName Name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
dataAnn Name
cons0Name (Type TyName uni ann -> VarDecl TyName Name uni fun ann)
-> Type TyName uni ann -> VarDecl TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
dataAnn TyName
dataName
        constrs :: [VarDecl TyName Name uni fun ann]
constrs = if [VarDecl TyName Name uni fun ann] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarDecl TyName Name uni fun ann]
constrsPossiblyEmpty then [VarDecl TyName Name uni fun ann
cons0] else [VarDecl TyName Name uni fun ann]
constrsPossiblyEmpty
    [VarDecl TyName Name uni fun ann]
-> (VarDecl TyName Name uni fun ann
    -> QuoteT Identity (VarDecl TyName Name uni fun NameAnn))
-> Quote [VarDecl TyName Name uni fun NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl TyName Name uni fun ann]
constrs ((VarDecl TyName Name uni fun ann
  -> QuoteT Identity (VarDecl TyName Name uni fun NameAnn))
 -> Quote [VarDecl TyName Name uni fun NameAnn])
-> (VarDecl TyName Name uni fun ann
    -> QuoteT Identity (VarDecl TyName Name uni fun NameAnn))
-> Quote [VarDecl TyName Name uni fun NameAnn]
forall a b. (a -> b) -> a -> b
$ \(VarDecl ann
_ Name
constrNameDup Type TyName uni ann
constrTyDup) -> do
        Name
constrName <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName Name
constrNameDup
        Type TyName uni NameAnn
constrTy <- (TyName -> NameAnn)
-> TyName
-> [TyVarDecl TyName NameAnn]
-> Type TyName uni ann
-> Quote (Type TyName uni NameAnn)
forall (uni :: * -> *) ann.
(TyName -> NameAnn)
-> TyName
-> [TyVarDecl TyName NameAnn]
-> Type TyName uni ann
-> Quote (Type TyName uni NameAnn)
establishScopingConstrTy TyName -> NameAnn
regSelf TyName
dataName [TyVarDecl TyName NameAnn]
params Type TyName uni ann
constrTyDup
        VarDecl TyName Name uni fun NameAnn
-> QuoteT Identity (VarDecl TyName Name uni fun NameAnn)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun NameAnn
 -> QuoteT Identity (VarDecl TyName Name uni fun NameAnn))
-> VarDecl TyName Name uni fun NameAnn
-> QuoteT Identity (VarDecl TyName Name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn
-> Name
-> Type TyName uni NameAnn
-> VarDecl TyName Name uni fun NameAnn
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound Name
constrName) Name
constrName Type TyName uni NameAnn
constrTy

-- | Establish scoping of a binding. Each bindings gets referenced in its own body either as an
-- in-scope or out-of-scope one, which is controlled by the first argument and ultimately depends on
-- the recursivity of the binding.
establishScopingBinding
    :: (forall name. ToScopedName name => name -> NameAnn)
    -> Binding TyName Name uni fun ann
    -> Quote (Binding TyName Name uni fun NameAnn)
establishScopingBinding :: (forall name. ToScopedName name => name -> NameAnn)
-> Binding TyName Name uni fun ann
-> Quote (Binding TyName Name uni fun NameAnn)
establishScopingBinding forall name. ToScopedName name => name -> NameAnn
regSelf (TermBind ann
_ Strictness
strictness (VarDecl ann
_ Name
nameDup Type TyName uni ann
ty) Term TyName Name uni fun ann
term) = do
    Name
name <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName Name
nameDup
    VarDecl TyName Name uni fun NameAnn
varDecl <- NameAnn
-> Name
-> Type TyName uni NameAnn
-> VarDecl TyName Name uni fun NameAnn
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound Name
name) Name
name (Type TyName uni NameAnn -> VarDecl TyName Name uni fun NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
-> QuoteT Identity (VarDecl 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
    NameAnn
-> Strictness
-> VarDecl TyName Name uni fun NameAnn
-> Term TyName Name uni fun NameAnn
-> Binding TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind NameAnn
NotAName Strictness
strictness VarDecl TyName Name uni fun NameAnn
varDecl (Term TyName Name uni fun NameAnn
 -> Binding TyName Name uni fun NameAnn)
-> (Term TyName Name uni fun NameAnn
    -> Term TyName Name uni fun NameAnn)
-> Term TyName Name uni fun NameAnn
-> Binding TyName Name uni fun NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> Name
-> Term TyName Name uni fun NameAnn
-> Term TyName Name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
regSelf Name
name (Term TyName Name uni fun NameAnn
 -> Binding TyName Name uni fun NameAnn)
-> QuoteT Identity (Term TyName Name uni fun NameAnn)
-> Quote (Binding 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
establishScopingBinding forall name. ToScopedName name => name -> NameAnn
regSelf (TypeBind ann
_ (TyVarDecl 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
nameDup
    TyVarDecl TyName NameAnn
tyVarDecl <- NameAnn -> TyName -> Kind NameAnn -> TyVarDecl TyName NameAnn
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound TyName
name) TyName
name (Kind NameAnn -> TyVarDecl TyName NameAnn)
-> QuoteT Identity (Kind NameAnn)
-> QuoteT Identity (TyVarDecl TyName NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind ann -> QuoteT Identity (Kind NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Kind ann
kind
    NameAnn
-> TyVarDecl TyName NameAnn
-> Type TyName uni NameAnn
-> Binding TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind NameAnn
NotAName TyVarDecl TyName NameAnn
tyVarDecl (Type TyName uni NameAnn -> Binding TyName Name uni fun NameAnn)
-> (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn
-> Binding TyName Name uni fun NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> TyName -> Type TyName uni NameAnn -> Type TyName uni NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
regSelf TyName
name (Type TyName uni NameAnn -> Binding TyName Name uni fun NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
-> Quote (Binding 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
establishScopingBinding forall name. ToScopedName name => name -> NameAnn
regSelf (DatatypeBind ann
dataAnn Datatype TyName Name uni fun ann
datatypeDup) = do
    let Datatype ann
_ TyVarDecl TyName ann
dataDeclDup [TyVarDecl TyName ann]
paramsDup Name
matchNameDup [VarDecl TyName Name uni fun ann]
constrsDup = Datatype TyName Name uni fun ann
datatypeDup
        TyVarDecl ann
_ TyName
dataNameDup Kind ann
dataKind = TyVarDecl TyName ann
dataDeclDup
    TyName
dataName <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName TyName
dataNameDup
    TyVarDecl TyName NameAnn
dataDecl <- NameAnn -> TyName -> Kind NameAnn -> TyVarDecl TyName NameAnn
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl (TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound TyName
dataName) TyName
dataName (Kind NameAnn -> TyVarDecl TyName NameAnn)
-> QuoteT Identity (Kind NameAnn)
-> QuoteT Identity (TyVarDecl TyName NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind ann -> QuoteT Identity (Kind NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Kind ann
dataKind
    [TyVarDecl TyName NameAnn]
params <- [TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn]
forall ann.
[TyVarDecl TyName ann] -> Quote [TyVarDecl TyName NameAnn]
establishScopingParams [TyVarDecl TyName ann]
paramsDup
    Name
matchName <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName Name
matchNameDup
    [VarDecl TyName Name uni fun NameAnn]
constrs <- (TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni fun ann]
-> Quote [VarDecl TyName Name uni fun NameAnn]
forall ann (uni :: * -> *) fun.
(TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni fun ann]
-> Quote [VarDecl TyName Name uni fun NameAnn]
establishScopingConstrs TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
regSelf ann
dataAnn TyName
dataName [TyVarDecl TyName NameAnn]
params [VarDecl TyName Name uni fun ann]
constrsDup
    let datatype :: Datatype TyName Name uni fun NameAnn
datatype = NameAnn
-> TyVarDecl TyName NameAnn
-> [TyVarDecl TyName NameAnn]
-> Name
-> [VarDecl TyName Name uni fun NameAnn]
-> Datatype TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound Name
matchName) TyVarDecl TyName NameAnn
dataDecl [TyVarDecl TyName NameAnn]
params Name
matchName [VarDecl TyName Name uni fun NameAnn]
constrs
    Binding TyName Name uni fun NameAnn
-> Quote (Binding TyName Name uni fun NameAnn)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding TyName Name uni fun NameAnn
 -> Quote (Binding TyName Name uni fun NameAnn))
-> Binding TyName Name uni fun NameAnn
-> Quote (Binding TyName Name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn
-> Datatype TyName Name uni fun NameAnn
-> Binding TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind NameAnn
NotAName Datatype TyName Name uni fun NameAnn
datatype

-- | Reference each binding in the last one apart from itself.
referenceViaBindings
    :: (forall name. ToScopedName name => name -> NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceViaBindings :: (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceViaBindings forall name. ToScopedName name => name -> NameAnn
_   (Binding TyName Name uni fun NameAnn
b0 :| [])  = Binding TyName Name uni fun NameAnn
b0 Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall a. a -> [a] -> NonEmpty a
:| []
referenceViaBindings forall name. ToScopedName name => name -> NameAnn
reg (Binding TyName Name uni fun NameAnn
b0 :| [Binding TyName Name uni fun NameAnn]
bs0) = [Binding TyName Name uni fun NameAnn]
-> Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> NonEmpty (Binding TyName Name uni fun NameAnn)
go [] Binding TyName Name uni fun NameAnn
b0 [Binding TyName Name uni fun NameAnn]
bs0 where
    go :: [Binding TyName Name uni fun NameAnn]
-> Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> NonEmpty (Binding TyName Name uni fun NameAnn)
go [Binding TyName Name uni fun NameAnn]
prevs Binding TyName Name uni fun NameAnn
b []       = (forall name. ToScopedName name => name -> NameAnn)
-> [Binding TyName Name uni fun NameAnn]
-> Binding TyName Name uni fun NameAnn
-> Binding TyName Name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia forall name. ToScopedName name => name -> NameAnn
reg [Binding TyName Name uni fun NameAnn]
prevs Binding TyName Name uni fun NameAnn
b Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall a. a -> [a] -> NonEmpty a
:| []
    go [Binding TyName Name uni fun NameAnn]
prevs Binding TyName Name uni fun NameAnn
b (Binding TyName Name uni fun NameAnn
c : [Binding TyName Name uni fun NameAnn]
bs) = Binding TyName Name uni fun NameAnn
b Binding TyName Name uni fun NameAnn
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall a. a -> NonEmpty a -> NonEmpty a
<| [Binding TyName Name uni fun NameAnn]
-> Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> NonEmpty (Binding TyName Name uni fun NameAnn)
go (Binding TyName Name uni fun NameAnn
b Binding TyName Name uni fun NameAnn
-> [Binding TyName Name uni fun NameAnn]
-> [Binding TyName Name uni fun NameAnn]
forall a. a -> [a] -> [a]
: [Binding TyName Name uni fun NameAnn]
prevs) Binding TyName Name uni fun NameAnn
c [Binding TyName Name uni fun NameAnn]
bs

-- | Reference each binding in the first one apart from itself and in the last one also apart from
-- itself. Former bindings are always visible in latter ones and whether latter bindings are visible
-- in former ones is controlled by the first argument and ultimately depends on the recursivity
-- of the family of bindings.
referenceBindingsBothWays
    :: (forall name. ToScopedName name => name -> NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceBindingsBothWays :: (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceBindingsBothWays forall name. ToScopedName name => name -> NameAnn
regRec          -- Whether latter bindings are visible in former ones
    = NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall a. NonEmpty a -> NonEmpty a
NonEmpty.reverse                    -- or not depends on the recursivity and so we have
    (NonEmpty (Binding TyName Name uni fun NameAnn)
 -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> (NonEmpty (Binding TyName Name uni fun NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall (uni :: * -> *) fun.
(forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceViaBindings forall name. ToScopedName name => name -> NameAnn
regRec         -- the registering function as an argument.
    (NonEmpty (Binding TyName Name uni fun NameAnn)
 -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> (NonEmpty (Binding TyName Name uni fun NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall a. NonEmpty a -> NonEmpty a
NonEmpty.reverse
    (NonEmpty (Binding TyName Name uni fun NameAnn)
 -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> (NonEmpty (Binding TyName Name uni fun NameAnn)
    -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall (uni :: * -> *) fun.
(forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceViaBindings forall name. ToScopedName name => name -> NameAnn
registerBound  -- Former bindings are always visible in latter ones.

-- | Establish scoping for a family of bindings.
establishScopingBindings
    :: (forall name. ToScopedName name => name -> NameAnn)
    -> NonEmpty (Binding TyName Name uni fun ann)
    -> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
establishScopingBindings :: (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun ann)
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
establishScopingBindings forall name. ToScopedName name => name -> NameAnn
regRec =
    -- Note that mutual recursion and self-recursion are handled separately.
    (NonEmpty (Binding TyName Name uni fun NameAnn)
 -> NonEmpty (Binding TyName Name uni fun NameAnn))
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
forall (uni :: * -> *) fun.
(forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> NonEmpty (Binding TyName Name uni fun NameAnn)
referenceBindingsBothWays forall name. ToScopedName name => name -> NameAnn
regRec) (Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
 -> Quote (NonEmpty (Binding TyName Name uni fun NameAnn)))
-> (NonEmpty (Binding TyName Name uni fun ann)
    -> Quote (NonEmpty (Binding TyName Name uni fun NameAnn)))
-> NonEmpty (Binding TyName Name uni fun ann)
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Binding TyName Name uni fun ann
 -> QuoteT Identity (Binding TyName Name uni fun NameAnn))
-> NonEmpty (Binding TyName Name uni fun ann)
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((forall name. ToScopedName name => name -> NameAnn)
-> Binding TyName Name uni fun ann
-> QuoteT Identity (Binding TyName Name uni fun NameAnn)
forall (uni :: * -> *) fun ann.
(forall name. ToScopedName name => name -> NameAnn)
-> Binding TyName Name uni fun ann
-> Quote (Binding TyName Name uni fun NameAnn)
establishScopingBinding forall name. ToScopedName name => name -> NameAnn
regRec)

-- | Return a registering function depending on the recursivity.
registerByRecursivity :: ToScopedName name => Recursivity -> name -> NameAnn
registerByRecursivity :: Recursivity -> name -> NameAnn
registerByRecursivity Recursivity
Rec    = name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerBound
registerByRecursivity Recursivity
NonRec = name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerOutOfScope

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 (Let ann
_ Recursivity
recy NonEmpty (Binding tyname name uni fun ann)
bindingsDup Term tyname name uni fun ann
body) = do
        NonEmpty (Binding TyName Name uni fun NameAnn)
bindings <- (forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun ann)
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
forall (uni :: * -> *) fun ann.
(forall name. ToScopedName name => name -> NameAnn)
-> NonEmpty (Binding TyName Name uni fun ann)
-> Quote (NonEmpty (Binding TyName Name uni fun NameAnn))
establishScopingBindings (Recursivity -> name -> NameAnn
forall name. ToScopedName name => Recursivity -> name -> NameAnn
registerByRecursivity Recursivity
recy) NonEmpty (Binding tyname name uni fun ann)
NonEmpty (Binding TyName Name uni fun ann)
bindingsDup
        -- Follows the shape of 'establishScopingBinder', but subtly differs (for example,
        -- does not bind a single name, does not have a @sort@ etc), hence we write things out
        -- manually.
        NonEmpty (Binding TyName Name uni fun NameAnn)
-> Term TyName Name uni fun NameAnn
-> Term TyName Name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope NonEmpty (Binding TyName Name uni fun NameAnn)
bindings (Term TyName Name uni fun NameAnn
 -> Term TyName Name uni fun NameAnn)
-> (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 b c a. (b -> c) -> (a -> b) -> a -> c
.
            NameAnn
-> Recursivity
-> NonEmpty (Binding TyName Name uni fun NameAnn)
-> Term TyName Name uni fun NameAnn
-> Term TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let NameAnn
NotAName Recursivity
recy NonEmpty (Binding TyName Name uni fun NameAnn)
bindings (Term TyName Name uni fun NameAnn
 -> Term TyName Name uni fun NameAnn)
-> (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 b c a. (b -> c) -> (a -> b) -> a -> c
.
                NonEmpty (Binding TyName Name uni fun NameAnn)
-> Term TyName Name uni fun NameAnn
-> Term TyName Name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceBound NonEmpty (Binding TyName Name uni fun NameAnn)
bindings (Term TyName Name uni fun NameAnn
 -> Term TyName Name uni fun NameAnn)
-> QuoteT Identity (Term TyName Name uni fun NameAnn)
-> QuoteT Identity (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
body
    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 a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
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 a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
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 a.
a -> Type tyname uni a -> Term tyname name uni fun a
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 a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
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 a.
a -> name -> Term tyname name uni fun a
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 a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
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 a.
a -> fun -> Term tyname name uni fun a
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
_ Term tyname name uni fun ann
term) = NameAnn
-> Term tyname name uni fun NameAnn
-> Program tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
Program NameAnn
NotAName (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 (TyVarDecl tyname) where
    collectScopeInfo :: TyVarDecl tyname NameAnn -> ScopeErrorOrInfo
collectScopeInfo (TyVarDecl NameAnn
ann tyname
tyname Kind NameAnn
kind) = NameAnn -> tyname -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
ann tyname
tyname ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Kind NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Kind NameAnn
kind

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (VarDecl tyname name uni fun) where
    collectScopeInfo :: VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (VarDecl NameAnn
ann name
name Type tyname uni NameAnn
ty) = 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

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Datatype tyname name uni fun) where
    collectScopeInfo :: Datatype tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Datatype NameAnn
matchAnn TyVarDecl tyname NameAnn
dataDecl [TyVarDecl tyname NameAnn]
params name
matchName [VarDecl tyname name uni fun NameAnn]
constrs) = [ScopeErrorOrInfo] -> ScopeErrorOrInfo
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
        [ TyVarDecl tyname NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo TyVarDecl tyname NameAnn
dataDecl
        , (TyVarDecl tyname NameAnn -> ScopeErrorOrInfo)
-> [TyVarDecl tyname NameAnn] -> ScopeErrorOrInfo
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TyVarDecl tyname NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [TyVarDecl tyname NameAnn]
params
        , NameAnn -> name -> ScopeErrorOrInfo
forall name.
ToScopedName name =>
NameAnn -> name -> ScopeErrorOrInfo
handleSname NameAnn
matchAnn name
matchName
        , (VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> [VarDecl tyname name uni fun NameAnn] -> ScopeErrorOrInfo
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [VarDecl tyname name uni fun NameAnn]
constrs
        ]

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Binding tyname name uni fun) where
    collectScopeInfo :: Binding tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (TermBind NameAnn
_ Strictness
_ VarDecl tyname name uni fun NameAnn
varDecl Term tyname name uni fun NameAnn
term) = VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo VarDecl tyname name uni fun NameAnn
varDecl 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 (TypeBind NameAnn
_ TyVarDecl tyname NameAnn
tyVarDecl Type tyname uni NameAnn
ty)   = TyVarDecl tyname NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo TyVarDecl tyname NameAnn
tyVarDecl 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 (DatatypeBind NameAnn
_ Datatype tyname name uni fun NameAnn
datatype)   = Datatype tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Datatype tyname name uni fun NameAnn
datatype

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Term tyname name uni fun) where
    collectScopeInfo :: Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Let NameAnn
_ Recursivity
_ NonEmpty (Binding tyname name uni fun NameAnn)
bindings Term tyname name uni fun NameAnn
body) =
        (Binding tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> NonEmpty (Binding tyname name uni fun NameAnn)
-> ScopeErrorOrInfo
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo NonEmpty (Binding tyname name uni fun NameAnn)
bindings 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 (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
_ 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