{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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
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
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
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
(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
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
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
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
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
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
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
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
= 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
regRec
(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
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 =
(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)
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
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
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, 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
name Type tyname uni ann
ty Term tyname name uni fun ann
body
establishScoping (TyAbs ann
_ tyname
nameDup Kind ann
kind Term tyname name uni fun ann
body) = do
TyName
name <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName tyname
TyName
nameDup
(NameAnn
-> tyname
-> Kind NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn)
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall name (value :: * -> *) (sort :: * -> *) ann.
(Reference name value, ToScopedName name, Scoping sort,
Scoping value) =>
(NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn)
-> name -> sort ann -> value ann -> Quote (value NameAnn)
establishScopingBinder NameAnn
-> tyname
-> Kind NameAnn
-> Term tyname name uni fun NameAnn
-> Term tyname name uni fun NameAnn
forall tyname name (uni :: * -> *) fun 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
arg [Term tyname name uni fun ann]
cs) = 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
-> Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> QuoteT Identity (Type tyname uni NameAnn)
-> QuoteT
Identity
(Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall ann.
Type tyname uni ann -> QuoteT Identity (Type tyname uni NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Type tyname uni ann
ty QuoteT
Identity
(Term tyname name uni fun NameAnn
-> [Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
-> Quote (Term tyname name uni fun NameAnn)
-> QuoteT
Identity
([Term tyname name uni fun NameAnn]
-> Term tyname name uni fun NameAnn)
forall a b.
QuoteT Identity (a -> b) -> QuoteT Identity a -> QuoteT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall ann.
Term tyname name uni fun ann
-> Quote (Term tyname name uni fun NameAnn)
forall (t :: * -> *) ann.
EstablishScoping t =>
t ann -> Quote (t NameAnn)
establishScoping Term tyname name uni fun ann
arg 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]
cs
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