-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module PlutusIR.Core.Instance.Scoping where

import PlutusPrelude

import PlutusIR.Core.Type

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

import Data.List.NonEmpty ((<|))
import Data.List.NonEmpty qualified as NonEmpty

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
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
name

instance tyname ~ TyName => Reference TyName (VarDecl tyname name uni) where
  referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> VarDecl tyname name uni NameAnn
-> VarDecl tyname name uni 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 NameAnn
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl NameAnn
ann name
varName (Type tyname uni NameAnn -> VarDecl tyname name uni NameAnn)
-> Type tyname uni NameAnn -> VarDecl tyname name uni 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 name -> NameAnn
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) where
  referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> TyName
-> Datatype tyname name uni NameAnn
-> Datatype tyname name uni 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 NameAnn]
constrs) =
    NameAnn
-> TyVarDecl tyname NameAnn
-> [TyVarDecl tyname NameAnn]
-> name
-> [VarDecl tyname name uni NameAnn]
-> Datatype tyname name uni NameAnn
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype NameAnn
dataAnn TyVarDecl tyname NameAnn
dataDecl [TyVarDecl tyname NameAnn]
params name
matchName ([VarDecl tyname name uni NameAnn]
 -> Datatype tyname name uni NameAnn)
-> [VarDecl tyname name uni NameAnn]
-> Datatype tyname name uni NameAnn
forall a b. (a -> b) -> a -> b
$ (VarDecl TyName name uni NameAnn
 -> VarDecl tyname name uni NameAnn)
-> [VarDecl TyName name uni NameAnn]
-> [VarDecl tyname name uni NameAnn]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl TyName name uni NameAnn -> VarDecl tyname name uni NameAnn
VarDecl TyName name uni NameAnn -> VarDecl TyName name uni NameAnn
goConstr [VarDecl tyname name uni NameAnn]
[VarDecl TyName name uni 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 NameAnn -> VarDecl TyName name uni NameAnn
goConstr (VarDecl NameAnn
ann name
constrName Type TyName uni NameAnn
constrTy) = NameAnn
-> name
-> Type TyName uni NameAnn
-> VarDecl TyName name uni NameAnn
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl NameAnn
ann name
constrName (Type TyName uni NameAnn -> VarDecl TyName name uni NameAnn)
-> Type TyName uni NameAnn -> VarDecl TyName name uni 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 NameAnn
varDecl Term tyname name uni fun NameAnn
term) =
    NameAnn
-> Strictness
-> VarDecl tyname name uni 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 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 NameAnn
-> VarDecl tyname name uni NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname VarDecl tyname name uni 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 name -> NameAnn
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 name -> NameAnn
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 NameAnn
datatype) =
    NameAnn
-> Datatype tyname name uni NameAnn
-> Binding tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind NameAnn
ann (Datatype tyname name uni NameAnn
 -> Binding tyname name uni fun NameAnn)
-> Datatype tyname name uni 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 NameAnn
-> Datatype tyname name uni NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg TyName
tyname Datatype tyname name uni 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 NameAnn
varDecl Term tyname name uni fun NameAnn
term) =
    NameAnn
-> Strictness
-> VarDecl tyname name uni 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 a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind NameAnn
ann Strictness
strictness VarDecl tyname name uni 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 name -> NameAnn
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 name -> NameAnn
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 ann) t where
  referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> VarDecl tyname name uni 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 name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg (name -> t NameAnn -> t NameAnn)
-> (VarDecl tyname name uni ann -> name)
-> VarDecl tyname name uni ann
-> t NameAnn
-> t NameAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni ann -> name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName

instance (Reference TyName t, Reference Name t) => Reference (Datatype TyName Name uni ann) t where
  referenceVia :: (forall name. ToScopedName name => name -> NameAnn)
-> Datatype TyName Name uni 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 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 name -> NameAnn
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 name -> NameAnn
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 ann] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg [VarDecl TyName Name uni 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 ann
varDecl Term TyName Name uni fun ann
_) = (forall name. ToScopedName name => name -> NameAnn)
-> VarDecl TyName Name uni ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg VarDecl TyName Name uni 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 name -> NameAnn
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 ann
datatype) = (forall name. ToScopedName name => name -> NameAnn)
-> Datatype TyName Name uni ann -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
(forall name. ToScopedName name => name -> NameAnn)
-> n -> t NameAnn -> t NameAnn
referenceVia name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
reg Datatype TyName Name uni 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 :: forall ann.
[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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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 ann. 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 :: 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 -> QuoteT Identity (Type TyName uni NameAnn)
goSpine
  where
    toDataAppliedToParams :: (TyName -> NameAnn) -> Type TyName uni NameAnn
toDataAppliedToParams TyName -> NameAnn
reg =
      Type TyName uni NameAnn
-> [(NameAnn, Type TyName uni NameAnn)] -> Type TyName uni NameAnn
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyApp (NameAnn -> TyName -> Type TyName uni NameAnn
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar (TyName -> NameAnn
reg TyName
dataName) TyName
dataName) ([(NameAnn, Type TyName uni NameAnn)] -> Type TyName uni NameAnn)
-> [(NameAnn, Type TyName uni NameAnn)] -> Type TyName uni NameAnn
forall a b. (a -> b) -> a -> b
$
        (TyVarDecl TyName NameAnn -> (NameAnn, Type TyName uni NameAnn))
-> [TyVarDecl TyName NameAnn]
-> [(NameAnn, Type TyName uni NameAnn)]
forall a b. (a -> b) -> [a] -> [b]
map (\(TyVarDecl NameAnn
_ TyName
name Kind NameAnn
_) -> (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)) [TyVarDecl TyName NameAnn]
params

    goSpine :: Type TyName uni ann -> QuoteT Identity (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 ann. 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)
-> QuoteT Identity (Type TyName uni NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
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)
-> QuoteT Identity (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 -> QuoteT Identity (Type TyName uni NameAnn)
forall ann.
Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type TyName uni ann
dom QuoteT
  Identity (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
goSpine Type TyName uni ann
cod
    goSpine Type TyName uni ann
_ =
      Type TyName uni NameAnn
-> QuoteT Identity (Type TyName uni NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni NameAnn
 -> QuoteT Identity (Type TyName uni NameAnn))
-> (Type TyName uni NameAnn -> Type TyName uni NameAnn)
-> Type TyName uni NameAnn
-> QuoteT Identity (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
 -> QuoteT Identity (Type TyName uni NameAnn))
-> Type TyName uni NameAnn
-> QuoteT Identity (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 ann]
  -> Quote [VarDecl TyName Name uni NameAnn]
establishScopingConstrs :: forall ann (uni :: * -> *).
(TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni ann]
-> Quote [VarDecl TyName Name uni NameAnn]
establishScopingConstrs TyName -> NameAnn
regSelf ann
dataAnn TyName
dataName [TyVarDecl TyName NameAnn]
params [VarDecl TyName Name uni 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 ann
cons0 = ann -> Name -> Type TyName uni ann -> VarDecl TyName Name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
dataAnn Name
cons0Name (Type TyName uni ann -> VarDecl TyName Name uni ann)
-> Type TyName uni ann -> VarDecl TyName Name uni 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 ann]
constrs = if [VarDecl TyName Name uni ann] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VarDecl TyName Name uni ann]
constrsPossiblyEmpty then [VarDecl TyName Name uni ann
cons0] else [VarDecl TyName Name uni ann]
constrsPossiblyEmpty
  [VarDecl TyName Name uni ann]
-> (VarDecl TyName Name uni ann
    -> QuoteT Identity (VarDecl TyName Name uni NameAnn))
-> Quote [VarDecl TyName Name uni NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl TyName Name uni ann]
constrs ((VarDecl TyName Name uni ann
  -> QuoteT Identity (VarDecl TyName Name uni NameAnn))
 -> Quote [VarDecl TyName Name uni NameAnn])
-> (VarDecl TyName Name uni ann
    -> QuoteT Identity (VarDecl TyName Name uni NameAnn))
-> Quote [VarDecl TyName Name uni 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 NameAnn
-> QuoteT Identity (VarDecl TyName Name uni NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni NameAnn
 -> QuoteT Identity (VarDecl TyName Name uni NameAnn))
-> VarDecl TyName Name uni NameAnn
-> QuoteT Identity (VarDecl TyName Name uni NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn
-> Name
-> Type TyName uni NameAnn
-> VarDecl TyName Name uni NameAnn
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni 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 (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
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 NameAnn
varDecl <- NameAnn
-> Name
-> Type TyName uni NameAnn
-> VarDecl TyName Name uni NameAnn
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
introduceBound Name
name) Name
name (Type TyName uni NameAnn -> VarDecl TyName Name uni NameAnn)
-> QuoteT Identity (Type TyName uni NameAnn)
-> QuoteT Identity (VarDecl TyName Name uni NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
forall ann.
Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type TyName uni ann
ty
  NameAnn
-> Strictness
-> VarDecl TyName Name uni 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 a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind NameAnn
NotAName Strictness
strictness VarDecl TyName Name uni 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 name -> NameAnn
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 ann.
Term TyName Name uni fun ann
-> QuoteT Identity (Term TyName Name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term TyName Name uni fun ann
term
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 ann. 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 name -> NameAnn
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 ann.
Type TyName uni ann -> QuoteT Identity (Type TyName uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type TyName uni ann
ty
establishScopingBinding forall name. ToScopedName name => name -> NameAnn
regSelf (DatatypeBind ann
dataAnn Datatype TyName Name uni ann
datatypeDup) = do
  let Datatype ann
_ TyVarDecl TyName ann
dataDeclDup [TyVarDecl TyName ann]
paramsDup Name
matchNameDup [VarDecl TyName Name uni ann]
constrsDup = Datatype TyName Name uni 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 ann. 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 NameAnn]
constrs <- (TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni ann]
-> Quote [VarDecl TyName Name uni NameAnn]
forall ann (uni :: * -> *).
(TyName -> NameAnn)
-> ann
-> TyName
-> [TyVarDecl TyName NameAnn]
-> [VarDecl TyName Name uni ann]
-> Quote [VarDecl TyName Name uni NameAnn]
establishScopingConstrs TyName -> NameAnn
forall name. ToScopedName name => name -> NameAnn
regSelf ann
dataAnn TyName
dataName [TyVarDecl TyName NameAnn]
params [VarDecl TyName Name uni ann]
constrsDup
  let datatype :: Datatype TyName Name uni NameAnn
datatype = NameAnn
-> TyVarDecl TyName NameAnn
-> [TyVarDecl TyName NameAnn]
-> Name
-> [VarDecl TyName Name uni NameAnn]
-> Datatype TyName Name uni NameAnn
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni 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 NameAnn]
constrs
  Binding TyName Name uni fun NameAnn
-> Quote (Binding TyName Name uni fun NameAnn)
forall a. a -> QuoteT Identity a
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 NameAnn
-> Binding TyName Name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind NameAnn
NotAName Datatype TyName Name uni 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 (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
_ (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 name -> NameAnn
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 (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 -- 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 name -> NameAnn
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 name -> NameAnn
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 (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 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))
-> QuoteT Identity (NonEmpty (Binding TyName Name uni fun NameAnn))
-> QuoteT Identity (NonEmpty (Binding TyName Name uni fun NameAnn))
forall a b. (a -> b) -> QuoteT Identity a -> QuoteT Identity b
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 name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
regRec) (QuoteT Identity (NonEmpty (Binding TyName Name uni fun NameAnn))
 -> QuoteT
      Identity (NonEmpty (Binding TyName Name uni fun NameAnn)))
-> (NonEmpty (Binding TyName Name uni fun ann)
    -> QuoteT
         Identity (NonEmpty (Binding TyName Name uni fun NameAnn)))
-> NonEmpty (Binding TyName Name uni fun ann)
-> QuoteT Identity (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)
-> QuoteT Identity (NonEmpty (Binding TyName Name uni fun NameAnn))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty 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 name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
regRec)

-- | Return a registering function depending on the recursivity.
registerByRecursivity :: ToScopedName name => Recursivity -> name -> NameAnn
registerByRecursivity :: forall name. ToScopedName name => 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

firstBound :: Term tyname name uni fun ann -> [name]
firstBound :: forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> [name]
firstBound (Apply ann
_ (LamAbs ann
_ name
name Type tyname uni ann
_ Term tyname name uni fun ann
body) Term tyname name uni fun ann
_) = name
name name -> [name] -> [name]
forall a. a -> [a] -> [a]
: Term tyname name uni fun ann -> [name]
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> [name]
firstBound Term tyname name uni fun ann
body
firstBound Term tyname name uni fun ann
_ = []

instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) where
  establishScoping :: forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
establishScoping (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)
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)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
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, EstablishScoping sort,
 EstablishScoping 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
name Type tyname uni ann
ty Term tyname name uni fun ann
body
  establishScoping (TyAbs ann
_ tyname
nameDup Kind ann
kind Term tyname name uni fun ann
body) = do
    TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
    (NameAnn
 -> tyname
 -> Kind NameAnn
 -> Term tyname name uni fun NameAnn
 -> Term tyname name uni fun NameAnn)
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall name (value :: * -> *) (sort :: * -> *) ann.
(Reference name value, ToScopedName name, EstablishScoping sort,
 EstablishScoping 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
TyName
name Kind ann
kind Term tyname name uni fun ann
body
  establishScoping (IWrap ann
_ Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term) =
    NameAnn
-> Type tyname uni NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
pat QuoteT
  Identity
  (Type tyname uni NameAnn
   -> Term tyname name uni fun NameAnn
   -> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
     Identity
     (Term tyname name uni fun NameAnn
      -> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
arg QuoteT
  Identity
  (Term tyname name uni fun NameAnn
   -> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term
  establishScoping (Apply ann
_ Term tyname name uni fun ann
fun Term tyname name uni fun ann
arg) =
    NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
fun QuoteT
  Identity
  (Term tyname name uni fun NameAnn
   -> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
arg
  establishScoping (Unwrap ann
_ Term tyname name uni fun ann
term) = NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term
  establishScoping (Error ann
_ Type tyname uni ann
ty) = NameAnn
-> Type tyname uni NameAnn -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty
  establishScoping (TyInst ann
_ Term tyname name uni fun ann
term Type tyname uni ann
ty) =
    NameAnn
-> Term tyname name uni fun NameAnn
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term QuoteT
  Identity
  (Type tyname uni NameAnn -> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty
  establishScoping (Var ann
_ name
nameDup) = do
    Name
name <- Name -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName name
Name
nameDup
    Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
 -> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> name -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var (Name -> NameAnn
forall name. ToScopedName name => name -> NameAnn
registerFree Name
name) name
Name
name
  establishScoping (Constant ann
_ Some (ValueOf uni)
con) = Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
 -> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> Some (ValueOf uni) -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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 a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
 -> Quote (Term tyname name uni fun NameAnn))
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a b. (a -> b) -> a -> b
$ NameAnn -> fun -> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin NameAnn
NotAName fun
bi
  establishScoping (Constr ann
_ Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es) = NameAnn
-> Type tyname uni NameAnn
-> Word64
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr NameAnn
NotAName (Type tyname uni NameAnn
 -> Word64
 -> [Term tyname name uni fun NameAnn]
 -> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
     Identity
     (Word64
      -> [Term tyname name uni fun NameAnn]
      -> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty QuoteT
  Identity
  (Word64
   -> [Term tyname name uni fun NameAnn]
   -> Term tyname name uni fun NameAnn)
-> QuoteT Identity Word64
-> QuoteT
     Identity
     ([Term tyname name uni fun NameAnn]
      -> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> QuoteT Identity Word64
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i QuoteT
  Identity
  ([Term tyname name uni fun NameAnn]
   -> Term tyname name uni fun NameAnn)
-> QuoteT Identity [Term tyname name uni fun NameAnn]
-> Quote (Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term tyname name uni fun ann
 -> Quote (Term tyname name uni fun NameAnn))
-> [Term tyname name uni fun ann]
-> QuoteT Identity [Term tyname name uni fun NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping [Term tyname name uni fun ann]
es
  establishScoping (Case ann
_ Type tyname uni ann
ty Term tyname name uni fun ann
a [Term tyname name uni fun ann]
es) = do
    [Term tyname name uni fun NameAnn]
esScoped <- (Term tyname name uni fun ann
 -> Quote (Term tyname name uni fun NameAnn))
-> [Term tyname name uni fun ann]
-> QuoteT Identity [Term tyname name uni fun NameAnn]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping [Term tyname name uni fun ann]
es
    let esScopedPoked :: [((Term tyname name uni fun NameAnn, [name]),
  [(Term tyname name uni fun NameAnn, [name])])]
esScopedPoked = [(Term tyname name uni fun NameAnn, [name])]
-> [((Term tyname name uni fun NameAnn, [name]),
     [(Term tyname name uni fun NameAnn, [name])])]
forall a. [a] -> [(a, [a])]
addTheRest ([(Term tyname name uni fun NameAnn, [name])]
 -> [((Term tyname name uni fun NameAnn, [name]),
      [(Term tyname name uni fun NameAnn, [name])])])
-> [(Term tyname name uni fun NameAnn, [name])]
-> [((Term tyname name uni fun NameAnn, [name]),
     [(Term tyname name uni fun NameAnn, [name])])]
forall a b. (a -> b) -> a -> b
$ (Term tyname name uni fun NameAnn
 -> (Term tyname name uni fun NameAnn, [name]))
-> [Term tyname name uni fun NameAnn]
-> [(Term tyname name uni fun NameAnn, [name])]
forall a b. (a -> b) -> [a] -> [b]
map (\Term tyname name uni fun NameAnn
e -> (Term tyname name uni fun NameAnn
e, Term tyname name uni fun NameAnn -> [name]
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> [name]
firstBound Term tyname name uni fun NameAnn
e)) [Term tyname name uni fun NameAnn]
esScoped
        branchBounds :: [[name]]
branchBounds = (((Term tyname name uni fun NameAnn, [name]),
  [(Term tyname name uni fun NameAnn, [name])])
 -> [name])
-> [((Term tyname name uni fun NameAnn, [name]),
     [(Term tyname name uni fun NameAnn, [name])])]
-> [[name]]
forall a b. (a -> b) -> [a] -> [b]
map ((Term tyname name uni fun NameAnn, [name]) -> [name]
forall a b. (a, b) -> b
snd ((Term tyname name uni fun NameAnn, [name]) -> [name])
-> (((Term tyname name uni fun NameAnn, [name]),
     [(Term tyname name uni fun NameAnn, [name])])
    -> (Term tyname name uni fun NameAnn, [name]))
-> ((Term tyname name uni fun NameAnn, [name]),
    [(Term tyname name uni fun NameAnn, [name])])
-> [name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Term tyname name uni fun NameAnn, [name]),
 [(Term tyname name uni fun NameAnn, [name])])
-> (Term tyname name uni fun NameAnn, [name])
forall a b. (a, b) -> a
fst) [((Term tyname name uni fun NameAnn, [name]),
  [(Term tyname name uni fun NameAnn, [name])])]
esScopedPoked
        referenceInBranch :: ((t NameAnn, b), [(a, b)]) -> t NameAnn
referenceInBranch ((t NameAnn
branch, b
_), [(a, b)]
others) = [b] -> t NameAnn -> t NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope (((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
others) t NameAnn
branch
    Type tyname uni NameAnn
tyScoped <- Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty
    Term tyname name uni fun NameAnn
aScoped <- Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
a
    -- For each of the branches reference (as out-of-scope) the variables bound in that branch
    -- in all the other ones, as well as outside of the whole case-expression. This is to check
    -- that none of the transformations leak variables outside of the branch they're bound in.
    Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun NameAnn
 -> Quote (Term tyname name uni fun NameAnn))
-> (Term tyname name uni fun NameAnn
    -> Term tyname name uni fun NameAnn)
-> Term tyname name uni fun NameAnn
-> Quote (Term tyname name uni fun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[name]]
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall n (t :: * -> *).
Reference n t =>
n -> t NameAnn -> t NameAnn
referenceOutOfScope [[name]]
branchBounds (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
-> Type tyname uni NameAnn
-> Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case NameAnn
NotAName Type tyname uni NameAnn
tyScoped Term tyname name uni fun NameAnn
aScoped ([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
$
        (((Term tyname name uni fun NameAnn, [name]),
  [(Term tyname name uni fun NameAnn, [name])])
 -> Term tyname name uni fun NameAnn)
-> [((Term tyname name uni fun NameAnn, [name]),
     [(Term tyname name uni fun NameAnn, [name])])]
-> [Term tyname name uni fun NameAnn]
forall a b. (a -> b) -> [a] -> [b]
map ((Term tyname name uni fun NameAnn, [name]),
 [(Term tyname name uni fun NameAnn, [name])])
-> Term tyname name uni fun NameAnn
forall {b} {t :: * -> *} {b} {a}.
Reference b t =>
((t NameAnn, b), [(a, b)]) -> t NameAnn
referenceInBranch [((Term tyname name uni fun NameAnn, [name]),
  [(Term tyname name uni fun NameAnn, [name])])]
esScopedPoked

instance (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) where
  establishScoping :: forall ann.
Program tyname name uni fun ann
-> Quote (Program tyname name uni fun NameAnn)
establishScoping (Program ann
_ Version
v Term tyname name uni fun ann
term) = NameAnn
-> Version
-> Term tyname name uni fun NameAnn
-> Program tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program NameAnn
NotAName Version
v (Term tyname name uni fun NameAnn
 -> Program tyname name uni fun NameAnn)
-> QuoteT Identity (Term tyname name uni fun NameAnn)
-> Quote (Program tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> QuoteT Identity (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> QuoteT Identity (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
term

instance tyname ~ TyName => CollectScopeInfo (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) where
  collectScopeInfo :: VarDecl tyname name uni 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) where
  collectScopeInfo :: Datatype tyname name uni NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Datatype NameAnn
matchAnn TyVarDecl tyname NameAnn
dataDecl [TyVarDecl tyname NameAnn]
params name
matchName [VarDecl tyname name uni NameAnn]
constrs) =
    [ScopeErrorOrInfo] -> ScopeErrorOrInfo
forall m. Monoid m => [m] -> m
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 m a. Monoid m => (a -> m) -> [a] -> m
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 NameAnn -> ScopeErrorOrInfo)
-> [VarDecl tyname name uni NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap VarDecl tyname name uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [VarDecl tyname name uni 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 NameAnn
varDecl Term tyname name uni fun NameAnn
term) = VarDecl tyname name uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo VarDecl tyname name uni 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 NameAnn
datatype) = Datatype tyname name uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Datatype tyname name uni 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 m a. Monoid m => (a -> m) -> NonEmpty a -> m
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
  collectScopeInfo (Constr NameAnn
_ Type tyname uni NameAnn
ty Word64
_ [Term tyname name uni fun NameAnn]
es) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> [Term tyname name uni fun NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [Term tyname name uni fun NameAnn]
es
  collectScopeInfo (Case NameAnn
_ Type tyname uni NameAnn
ty Term tyname name uni fun NameAnn
arg [Term tyname name uni fun NameAnn]
cs) = Type tyname uni NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Type tyname uni NameAnn
ty ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
arg ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo
forall a. Semigroup a => a -> a -> a
<> (Term tyname name uni fun NameAnn -> ScopeErrorOrInfo)
-> [Term tyname name uni fun NameAnn] -> ScopeErrorOrInfo
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo [Term tyname name uni fun NameAnn]
cs

instance (tyname ~ TyName, name ~ Name) => CollectScopeInfo (Program tyname name uni fun) where
  collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo
collectScopeInfo (Program NameAnn
_ Version
_ Term tyname name uni fun NameAnn
term) = Term tyname name uni fun NameAnn -> ScopeErrorOrInfo
forall (t :: * -> *).
CollectScopeInfo t =>
t NameAnn -> ScopeErrorOrInfo
collectScopeInfo Term tyname name uni fun NameAnn
term