{-# LANGUAGE LambdaCase #-}
-- | Definition analysis for Plutus Core.
module PlutusCore.Analysis.Definitions
    ( UniqueInfos
    , ScopeType(..)
    , termDefs
    , typeDefs
    , runTermDefs
    , runTypeDefs
    , addDef
    , addUsage
    ) where

import PlutusCore.Core
import PlutusCore.Error
import PlutusCore.Name

import Data.Functor.Foldable

import Control.Lens hiding (use, uses)
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer

import Data.Foldable
import Data.Set qualified as Set

{- Note [Unique usage errors]
The definitions analysis can find a number of problems with usage of uniques, however
clients may not always want to throw an error on all of them, hence we simply return
them all and allow the client to chose if they want to throw some of them.
-}

-- | Information about a unique, a pair of a definition if we have one and a set of uses.
type UniqueInfo ann = (Maybe (ScopedLoc ann), Set.Set (ScopedLoc ann))
type UniqueInfos ann = UniqueMap Unique (UniqueInfo ann)

data ScopedLoc ann = ScopedLoc ScopeType ann deriving stock (ScopedLoc ann -> ScopedLoc ann -> Bool
(ScopedLoc ann -> ScopedLoc ann -> Bool)
-> (ScopedLoc ann -> ScopedLoc ann -> Bool) -> Eq (ScopedLoc ann)
forall ann. Eq ann => ScopedLoc ann -> ScopedLoc ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c/= :: forall ann. Eq ann => ScopedLoc ann -> ScopedLoc ann -> Bool
== :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c== :: forall ann. Eq ann => ScopedLoc ann -> ScopedLoc ann -> Bool
Eq, Eq (ScopedLoc ann)
Eq (ScopedLoc ann)
-> (ScopedLoc ann -> ScopedLoc ann -> Ordering)
-> (ScopedLoc ann -> ScopedLoc ann -> Bool)
-> (ScopedLoc ann -> ScopedLoc ann -> Bool)
-> (ScopedLoc ann -> ScopedLoc ann -> Bool)
-> (ScopedLoc ann -> ScopedLoc ann -> Bool)
-> (ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann)
-> (ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann)
-> Ord (ScopedLoc ann)
ScopedLoc ann -> ScopedLoc ann -> Bool
ScopedLoc ann -> ScopedLoc ann -> Ordering
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall ann. Ord ann => Eq (ScopedLoc ann)
forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Bool
forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Ordering
forall ann.
Ord ann =>
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
min :: ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
$cmin :: forall ann.
Ord ann =>
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
max :: ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
$cmax :: forall ann.
Ord ann =>
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
>= :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c>= :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Bool
> :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c> :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Bool
<= :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c<= :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Bool
< :: ScopedLoc ann -> ScopedLoc ann -> Bool
$c< :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Bool
compare :: ScopedLoc ann -> ScopedLoc ann -> Ordering
$ccompare :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Ordering
$cp1Ord :: forall ann. Ord ann => Eq (ScopedLoc ann)
Ord)

-- | Tag for distinguishing between whether we are talking about the term scope
-- for variables or the type scope for variables.
data ScopeType = TermScope | TypeScope deriving stock (ScopeType -> ScopeType -> Bool
(ScopeType -> ScopeType -> Bool)
-> (ScopeType -> ScopeType -> Bool) -> Eq ScopeType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopeType -> ScopeType -> Bool
$c/= :: ScopeType -> ScopeType -> Bool
== :: ScopeType -> ScopeType -> Bool
$c== :: ScopeType -> ScopeType -> Bool
Eq, Eq ScopeType
Eq ScopeType
-> (ScopeType -> ScopeType -> Ordering)
-> (ScopeType -> ScopeType -> Bool)
-> (ScopeType -> ScopeType -> Bool)
-> (ScopeType -> ScopeType -> Bool)
-> (ScopeType -> ScopeType -> Bool)
-> (ScopeType -> ScopeType -> ScopeType)
-> (ScopeType -> ScopeType -> ScopeType)
-> Ord ScopeType
ScopeType -> ScopeType -> Bool
ScopeType -> ScopeType -> Ordering
ScopeType -> ScopeType -> ScopeType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScopeType -> ScopeType -> ScopeType
$cmin :: ScopeType -> ScopeType -> ScopeType
max :: ScopeType -> ScopeType -> ScopeType
$cmax :: ScopeType -> ScopeType -> ScopeType
>= :: ScopeType -> ScopeType -> Bool
$c>= :: ScopeType -> ScopeType -> Bool
> :: ScopeType -> ScopeType -> Bool
$c> :: ScopeType -> ScopeType -> Bool
<= :: ScopeType -> ScopeType -> Bool
$c<= :: ScopeType -> ScopeType -> Bool
< :: ScopeType -> ScopeType -> Bool
$c< :: ScopeType -> ScopeType -> Bool
compare :: ScopeType -> ScopeType -> Ordering
$ccompare :: ScopeType -> ScopeType -> Ordering
$cp1Ord :: Eq ScopeType
Ord)

lookupDef
    :: (Ord ann,
        HasUnique name unique,
        MonadState (UniqueInfos ann) m)
    => name
    -> m (UniqueInfo ann)
lookupDef :: name -> m (UniqueInfo ann)
lookupDef name
n = do
    Maybe (UniqueInfo ann)
previousDef <- (UniqueMap Unique (UniqueInfo ann) -> Maybe (UniqueInfo ann))
-> m (Maybe (UniqueInfo ann))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((UniqueMap Unique (UniqueInfo ann) -> Maybe (UniqueInfo ann))
 -> m (Maybe (UniqueInfo ann)))
-> (UniqueMap Unique (UniqueInfo ann) -> Maybe (UniqueInfo ann))
-> m (Maybe (UniqueInfo ann))
forall a b. (a -> b) -> a -> b
$ name -> UniqueMap Unique (UniqueInfo ann) -> Maybe (UniqueInfo ann)
forall name unique1 unique2 a.
(HasUnique name unique1, Coercible unique2 Unique) =>
name -> UniqueMap unique2 a -> Maybe a
lookupNameIndex name
n
    case Maybe (UniqueInfo ann)
previousDef of
        Just UniqueInfo ann
d -> UniqueInfo ann -> m (UniqueInfo ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UniqueInfo ann
d
        Maybe (UniqueInfo ann)
Nothing -> do
            let empty :: (Maybe a, Set (ScopedLoc ann))
empty = (Maybe a
forall a. Maybe a
Nothing, Set (ScopedLoc ann)
forall a. Monoid a => a
mempty)
            (UniqueMap Unique (UniqueInfo ann)
 -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueMap Unique (UniqueInfo ann)
  -> UniqueMap Unique (UniqueInfo ann))
 -> m ())
-> (UniqueMap Unique (UniqueInfo ann)
    -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall a b. (a -> b) -> a -> b
$ name
-> UniqueInfo ann
-> UniqueMap Unique (UniqueInfo ann)
-> UniqueMap Unique (UniqueInfo ann)
forall name unique1 unique2 a.
(HasUnique name unique1, Coercible unique2 Unique) =>
name -> a -> UniqueMap unique2 a -> UniqueMap unique2 a
insertByNameIndex name
n UniqueInfo ann
forall a. (Maybe a, Set (ScopedLoc ann))
empty
            UniqueInfo ann -> m (UniqueInfo ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UniqueInfo ann
forall a. (Maybe a, Set (ScopedLoc ann))
empty

addDef
    :: (Ord ann,
        HasUnique n unique,
        MonadState (UniqueInfos ann) m,
        MonadWriter [UniqueError ann] m)
    => n -- ^ The variable
    -> ann -- ^ The annotation of the variable
    -> ScopeType -- ^ The scope type
    -> m ()
addDef :: n -> ann -> ScopeType -> m ()
addDef n
n ann
newDef ScopeType
tpe = do
    let def :: ScopedLoc ann
def = ScopeType -> ann -> ScopedLoc ann
forall ann. ScopeType -> ann -> ScopedLoc ann
ScopedLoc ScopeType
tpe ann
newDef

    d :: UniqueInfo ann
d@(Maybe (ScopedLoc ann)
_, Set (ScopedLoc ann)
uses) <- n -> m (UniqueInfo ann)
forall ann name unique (m :: * -> *).
(Ord ann, HasUnique name unique, MonadState (UniqueInfos ann) m) =>
name -> m (UniqueInfo ann)
lookupDef n
n
    n -> ScopedLoc ann -> UniqueInfo ann -> m ()
forall n u ann (m :: * -> *).
(HasUnique n u, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkUndefined n
n ScopedLoc ann
def UniqueInfo ann
d
    (UniqueMap Unique (UniqueInfo ann)
 -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueMap Unique (UniqueInfo ann)
  -> UniqueMap Unique (UniqueInfo ann))
 -> m ())
-> (UniqueMap Unique (UniqueInfo ann)
    -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall a b. (a -> b) -> a -> b
$ n
-> UniqueInfo ann
-> UniqueMap Unique (UniqueInfo ann)
-> UniqueMap Unique (UniqueInfo ann)
forall name unique1 unique2 a.
(HasUnique name unique1, Coercible unique2 Unique) =>
name -> a -> UniqueMap unique2 a -> UniqueMap unique2 a
insertByNameIndex n
n (ScopedLoc ann -> Maybe (ScopedLoc ann)
forall a. a -> Maybe a
Just ScopedLoc ann
def, Set (ScopedLoc ann)
uses)

-- | Check that a variable is currently undefined.
checkUndefined
    :: (HasUnique n u,
        MonadState (UniqueInfos ann) m,
        MonadWriter [UniqueError ann] m)
    => n -- ^ The variable
    -> ScopedLoc ann -- ^ The new definition
    -> UniqueInfo ann -- ^ The existing info
    -> m ()
checkUndefined :: n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkUndefined n
n (ScopedLoc ScopeType
_ ann
newDef) UniqueInfo ann
info = case UniqueInfo ann
info of
    (Just (ScopedLoc ScopeType
_ ann
prevDef), Set (ScopedLoc ann)
_) -> [UniqueError ann] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Unique -> ann -> ann -> UniqueError ann
forall ann. Unique -> ann -> ann -> UniqueError ann
MultiplyDefined (n
n n -> Getting Unique n Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique n Unique
forall name unique. HasUnique name unique => Lens' name Unique
theUnique) ann
prevDef ann
newDef]
    UniqueInfo ann
_                               -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

addUsage
    :: (Ord ann,
        HasUnique n unique,
        MonadState (UniqueInfos ann) m,
        MonadWriter [UniqueError ann] m)
    => n -- ^ The variable
    -> ann -- ^ The annotation of the variable
    -> ScopeType -- ^ The scope type
    -> m ()
addUsage :: n -> ann -> ScopeType -> m ()
addUsage n
n ann
newUse ScopeType
tpe = do
    let use :: ScopedLoc ann
use = ScopeType -> ann -> ScopedLoc ann
forall ann. ScopeType -> ann -> ScopedLoc ann
ScopedLoc ScopeType
tpe ann
newUse

    d :: UniqueInfo ann
d@(Maybe (ScopedLoc ann)
def, Set (ScopedLoc ann)
uses) <- n -> m (UniqueInfo ann)
forall ann name unique (m :: * -> *).
(Ord ann, HasUnique name unique, MonadState (UniqueInfos ann) m) =>
name -> m (UniqueInfo ann)
lookupDef n
n
    n -> ScopedLoc ann -> UniqueInfo ann -> m ()
forall n u ann (m :: * -> *).
(HasUnique n u, MonadWriter [UniqueError ann] m) =>
n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkCoherency n
n ScopedLoc ann
use UniqueInfo ann
d
    n -> ScopedLoc ann -> UniqueInfo ann -> m ()
forall n u ann (m :: * -> *).
(HasUnique n u, MonadWriter [UniqueError ann] m) =>
n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkDefined n
n ScopedLoc ann
use UniqueInfo ann
d
    (UniqueMap Unique (UniqueInfo ann)
 -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueMap Unique (UniqueInfo ann)
  -> UniqueMap Unique (UniqueInfo ann))
 -> m ())
-> (UniqueMap Unique (UniqueInfo ann)
    -> UniqueMap Unique (UniqueInfo ann))
-> m ()
forall a b. (a -> b) -> a -> b
$ n
-> UniqueInfo ann
-> UniqueMap Unique (UniqueInfo ann)
-> UniqueMap Unique (UniqueInfo ann)
forall name unique1 unique2 a.
(HasUnique name unique1, Coercible unique2 Unique) =>
name -> a -> UniqueMap unique2 a -> UniqueMap unique2 a
insertByNameIndex n
n (Maybe (ScopedLoc ann)
def, ScopedLoc ann -> Set (ScopedLoc ann) -> Set (ScopedLoc ann)
forall a. Ord a => a -> Set a -> Set a
Set.insert ScopedLoc ann
use Set (ScopedLoc ann)
uses)

checkDefined
    :: (HasUnique n u,
        MonadWriter [UniqueError ann] m)
    => n -- ^ The variable
    -> ScopedLoc ann -- ^ The new definition
    -> UniqueInfo ann -- ^ The existing info
    -> m ()
checkDefined :: n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkDefined n
n (ScopedLoc ScopeType
_ ann
loc) (Maybe (ScopedLoc ann)
def, Set (ScopedLoc ann)
_) = case Maybe (ScopedLoc ann)
def of
    Maybe (ScopedLoc ann)
Nothing -> [UniqueError ann] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Unique -> ann -> UniqueError ann
forall ann. Unique -> ann -> UniqueError ann
FreeVariable (n
n n -> Getting Unique n Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique n Unique
forall name unique. HasUnique name unique => Lens' name Unique
theUnique) ann
loc]
    Just ScopedLoc ann
_  -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

checkCoherency
    :: (HasUnique n u,
        MonadWriter [UniqueError ann] m)
    => n -- ^ The variable
    -> ScopedLoc ann -- ^ The new definition
    -> UniqueInfo ann -- ^ The existing info
    -> m ()
checkCoherency :: n -> ScopedLoc ann -> UniqueInfo ann -> m ()
checkCoherency n
n (ScopedLoc ScopeType
tpe ann
loc) (Maybe (ScopedLoc ann)
def, Set (ScopedLoc ann)
uses) = do
    Maybe (ScopedLoc ann) -> (ScopedLoc ann -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe (ScopedLoc ann)
def ScopedLoc ann -> m ()
forall (f :: * -> *).
MonadWriter [UniqueError ann] f =>
ScopedLoc ann -> f ()
checkLoc
    [ScopedLoc ann] -> (ScopedLoc ann -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Set (ScopedLoc ann) -> [ScopedLoc ann]
forall a. Set a -> [a]
Set.toList Set (ScopedLoc ann)
uses) ScopedLoc ann -> m ()
forall (f :: * -> *).
MonadWriter [UniqueError ann] f =>
ScopedLoc ann -> f ()
checkLoc

    where
        checkLoc :: ScopedLoc ann -> f ()
checkLoc (ScopedLoc ScopeType
tpe' ann
loc') = Bool -> f () -> f ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ScopeType
tpe' ScopeType -> ScopeType -> Bool
forall a. Eq a => a -> a -> Bool
/= ScopeType
tpe) (f () -> f ()) -> f () -> f ()
forall a b. (a -> b) -> a -> b
$
            [UniqueError ann] -> f ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Unique -> ann -> ann -> UniqueError ann
forall ann. Unique -> ann -> ann -> UniqueError ann
IncoherentUsage (n
n n -> Getting Unique n Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique n Unique
forall name unique. HasUnique name unique => Lens' name Unique
theUnique) ann
loc' ann
loc]

termDefs
    :: (Ord ann,
        HasUnique name TermUnique,
        HasUnique tyname TypeUnique,
        MonadState (UniqueInfos ann) m,
        MonadWriter [UniqueError ann] m)
    => Term tyname name uni fun ann
    -> m ()
termDefs :: Term tyname name uni fun ann -> m ()
termDefs = (Base (Term tyname name uni fun ann) (m ()) -> m ())
-> Term tyname name uni fun ann -> m ()
forall t a. Recursive t => (Base t a -> a) -> t -> a
cata ((Base (Term tyname name uni fun ann) (m ()) -> m ())
 -> Term tyname name uni fun ann -> m ())
-> (Base (Term tyname name uni fun ann) (m ()) -> m ())
-> Term tyname name uni fun ann
-> m ()
forall a b. (a -> b) -> a -> b
$ \case
    VarF ann n         -> name -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addUsage name
n ann
ann ScopeType
TermScope
    LamAbsF ann n ty t -> name -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addDef name
n ann
ann ScopeType
TermScope m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann -> m ()
forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
typeDefs Type tyname uni ann
ty m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
t
    IWrapF _ pat arg t -> Type tyname uni ann -> m ()
forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
typeDefs Type tyname uni ann
pat m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann -> m ()
forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
typeDefs Type tyname uni ann
arg m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
t
    TyAbsF ann tn _ t  -> tyname -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addDef tyname
tn ann
ann ScopeType
TypeScope m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
t
    TyInstF _ t ty     -> m ()
t m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type tyname uni ann -> m ()
forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
typeDefs Type tyname uni ann
ty
    Base (Term tyname name uni fun ann) (m ())
x                  -> TermF tyname name uni fun ann (m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ Base (Term tyname name uni fun ann) (m ())
TermF tyname name uni fun ann (m ())
x

typeDefs
    :: (Ord ann,
        HasUnique tyname TypeUnique,
        MonadState (UniqueInfos ann) m,
        MonadWriter [UniqueError ann] m)
    => Type tyname uni ann
    -> m ()
typeDefs :: Type tyname uni ann -> m ()
typeDefs = (Base (Type tyname uni ann) (m ()) -> m ())
-> Type tyname uni ann -> m ()
forall t a. Recursive t => (Base t a -> a) -> t -> a
cata ((Base (Type tyname uni ann) (m ()) -> m ())
 -> Type tyname uni ann -> m ())
-> (Base (Type tyname uni ann) (m ()) -> m ())
-> Type tyname uni ann
-> m ()
forall a b. (a -> b) -> a -> b
$ \case
    TyVarF ann n         -> tyname -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addUsage tyname
n ann
ann ScopeType
TypeScope
    TyForallF ann tn _ t -> tyname -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addDef tyname
tn ann
ann ScopeType
TypeScope m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
t
    TyLamF ann tn _ t    -> tyname -> ann -> ScopeType -> m ()
forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
n -> ann -> ScopeType -> m ()
addDef tyname
tn ann
ann ScopeType
TypeScope m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
t
    Base (Type tyname uni ann) (m ())
x                    -> TypeF tyname uni ann (m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ Base (Type tyname uni ann) (m ())
TypeF tyname uni ann (m ())
x

runTermDefs
    :: (Ord ann,
        HasUnique name TermUnique,
        HasUnique tyname TypeUnique,
        Monad m)
    => Term tyname name uni fun ann
    -> m (UniqueInfos ann, [UniqueError ann])
runTermDefs :: Term tyname name uni fun ann
-> m (UniqueInfos ann, [UniqueError ann])
runTermDefs = WriterT [UniqueError ann] m (UniqueInfos ann)
-> m (UniqueInfos ann, [UniqueError ann])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [UniqueError ann] m (UniqueInfos ann)
 -> m (UniqueInfos ann, [UniqueError ann]))
-> (Term tyname name uni fun ann
    -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> Term tyname name uni fun ann
-> m (UniqueInfos ann, [UniqueError ann])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
 -> UniqueInfos ann
 -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> UniqueInfos ann
-> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
-> WriterT [UniqueError ann] m (UniqueInfos ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
-> UniqueInfos ann -> WriterT [UniqueError ann] m (UniqueInfos ann)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT UniqueInfos ann
forall a. Monoid a => a
mempty (StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
 -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> (Term tyname name uni fun ann
    -> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ())
-> Term tyname name uni fun ann
-> WriterT [UniqueError ann] m (UniqueInfos ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
forall ann name tyname (m :: * -> *) (uni :: * -> *) fun.
(Ord ann, HasUnique name TermUnique, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Term tyname name uni fun ann -> m ()
termDefs

runTypeDefs
    :: (Ord ann,
        HasUnique tyname TypeUnique,
        Monad m)
    => Type tyname uni ann
    -> m (UniqueInfos ann, [UniqueError ann])
runTypeDefs :: Type tyname uni ann -> m (UniqueInfos ann, [UniqueError ann])
runTypeDefs = WriterT [UniqueError ann] m (UniqueInfos ann)
-> m (UniqueInfos ann, [UniqueError ann])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [UniqueError ann] m (UniqueInfos ann)
 -> m (UniqueInfos ann, [UniqueError ann]))
-> (Type tyname uni ann
    -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> Type tyname uni ann
-> m (UniqueInfos ann, [UniqueError ann])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
 -> UniqueInfos ann
 -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> UniqueInfos ann
-> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
-> WriterT [UniqueError ann] m (UniqueInfos ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
-> UniqueInfos ann -> WriterT [UniqueError ann] m (UniqueInfos ann)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT UniqueInfos ann
forall a. Monoid a => a
mempty (StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
 -> WriterT [UniqueError ann] m (UniqueInfos ann))
-> (Type tyname uni ann
    -> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ())
-> Type tyname uni ann
-> WriterT [UniqueError ann] m (UniqueInfos ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> StateT (UniqueInfos ann) (WriterT [UniqueError ann] m) ()
forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
typeDefs