{-# LANGUAGE LambdaCase #-}

-- | Definition analysis for Plutus Core.
module PlutusCore.Analysis.Definitions
  ( UniqueInfos
  , ScopeType (..)
  , termDefs
  , handleType
  , runTermDefs
  , addDef
  , addUsage
  ) where

import PlutusCore.Core.Plated (termSubtermsDeep, termSubtypesDeep)
import PlutusCore.Core.Type (Term (LamAbs, TyAbs, Var), Type (TyForall, TyLam, TyVar))
import PlutusCore.Error (UniqueError (..))
import PlutusCore.Name.Unique
  ( HasUnique
  , TermUnique (TermUnique)
  , TypeUnique (TypeUnique)
  , Unique (Unique)
  , theUnique
  )
import PlutusCore.Name.UniqueMap (UniqueMap, insertByNameIndex, lookupNameIndex)

import Control.Lens (forMOf_, (^.))
import Control.Monad (when)
import Control.Monad.State (MonadState, execStateT, gets, modify)
import Control.Monad.Writer (MonadWriter, runWriterT, tell)

import Data.Foldable (for_)
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
$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
/= :: 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
$ccompare :: forall ann. Ord ann => ScopedLoc ann -> ScopedLoc ann -> Ordering
compare :: ScopedLoc ann -> ScopedLoc ann -> Ordering
$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
>= :: ScopedLoc ann -> ScopedLoc ann -> Bool
$cmax :: forall ann.
Ord ann =>
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
max :: ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
$cmin :: forall ann.
Ord ann =>
ScopedLoc ann -> ScopedLoc ann -> ScopedLoc ann
min :: ScopedLoc ann -> ScopedLoc ann -> 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
$c== :: ScopeType -> ScopeType -> Bool
== :: ScopeType -> ScopeType -> Bool
$c/= :: ScopeType -> ScopeType -> Bool
/= :: 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
$ccompare :: ScopeType -> ScopeType -> Ordering
compare :: ScopeType -> ScopeType -> Ordering
$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
>= :: ScopeType -> ScopeType -> Bool
$cmax :: ScopeType -> ScopeType -> ScopeType
max :: ScopeType -> ScopeType -> ScopeType
$cmin :: ScopeType -> ScopeType -> ScopeType
min :: ScopeType -> ScopeType -> ScopeType
Ord)

lookupDef
  :: ( Ord ann
     , HasUnique name unique
     , MonadState (UniqueInfos ann) m
     )
  => name
  -> m (UniqueInfo ann)
lookupDef :: forall ann name unique (m :: * -> *).
(Ord ann, HasUnique name unique, MonadState (UniqueInfos ann) m) =>
name -> m (UniqueInfo ann)
lookupDef name
n = do
  Maybe (UniqueInfo ann)
previousDef <- (UniqueInfos ann -> Maybe (UniqueInfo ann))
-> m (Maybe (UniqueInfo ann))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((UniqueInfos ann -> Maybe (UniqueInfo ann))
 -> m (Maybe (UniqueInfo ann)))
-> (UniqueInfos ann -> Maybe (UniqueInfo ann))
-> m (Maybe (UniqueInfo ann))
forall a b. (a -> b) -> a -> b
$ name -> UniqueInfos 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 a. a -> m a
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)
      (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueInfos ann -> UniqueInfos ann) -> m ())
-> (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall a b. (a -> b) -> a -> b
$ name -> UniqueInfo ann -> UniqueInfos ann -> UniqueInfos 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 a. a -> m a
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 :: forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
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
  (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueInfos ann -> UniqueInfos ann) -> m ())
-> (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall a b. (a -> b) -> a -> b
$ n -> UniqueInfo ann -> UniqueInfos ann -> UniqueInfos 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 :: 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 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
Lens' n Unique
theUnique) ann
prevDef ann
newDef]
  UniqueInfo ann
_ -> () -> m ()
forall a. a -> m a
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 :: forall ann n unique (m :: * -> *).
(Ord ann, HasUnique n unique, MonadState (UniqueInfos ann) m,
 MonadWriter [UniqueError ann] m) =>
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
  (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UniqueInfos ann -> UniqueInfos ann) -> m ())
-> (UniqueInfos ann -> UniqueInfos ann) -> m ()
forall a b. (a -> b) -> a -> b
$ n -> UniqueInfo ann -> UniqueInfos ann -> UniqueInfos 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 :: forall n u ann (m :: * -> *).
(HasUnique n u, MonadWriter [UniqueError ann] m) =>
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
Lens' n Unique
theUnique) ann
loc]
  Just ScopedLoc ann
_ -> () -> m ()
forall a. a -> m a
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 :: forall n u ann (m :: * -> *).
(HasUnique n u, MonadWriter [UniqueError ann] m) =>
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
Lens' n Unique
theUnique) ann
loc' ann
loc]

{-| Given a PLC term, add all of its term and type definitions and usages, including its subterms
and subtypes, to a global map. -}
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 :: 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 Term tyname name uni fun ann
tm = do
  Getting
  (Sequenced () m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> Term tyname name uni fun ann
-> (Term tyname name uni fun ann -> m ())
-> m ()
forall (m :: * -> *) r s a.
Monad m =>
Getting (Sequenced r m) s a -> s -> (a -> m r) -> m ()
forMOf_ Getting
  (Sequenced () m)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtermsDeep Term tyname name uni fun ann
tm Term tyname name uni fun 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 ()
handleTerm
  Getting
  (Sequenced () m)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
-> Term tyname name uni fun ann
-> (Type tyname uni ann -> m ())
-> m ()
forall (m :: * -> *) r s a.
Monad m =>
Getting (Sequenced r m) s a -> s -> (a -> m r) -> m ()
forMOf_ Getting
  (Sequenced () m)
  (Term tyname name uni fun ann)
  (Type tyname uni ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypesDeep Term tyname name uni fun ann
tm 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 ()
handleType

handleTerm
  :: ( Ord ann
     , HasUnique name TermUnique
     , HasUnique tyname TypeUnique
     , MonadState (UniqueInfos ann) m
     , MonadWriter [UniqueError ann] m
     )
  => Term tyname name uni fun ann
  -> m ()
handleTerm :: 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 ()
handleTerm = \case
  Var ann
ann name
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
  LamAbs ann
ann name
n Type tyname uni ann
_ Term tyname name uni fun ann
_ -> do
    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
  TyAbs ann
ann tyname
tn Kind ann
_ Term tyname name uni fun ann
_ -> do
    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
  Term tyname name uni fun ann
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Given a type, add its type definition/usage, including its subtypes, to a global map.
handleType
  :: ( Ord ann
     , HasUnique tyname TypeUnique
     , MonadState (UniqueInfos ann) m
     , MonadWriter [UniqueError ann] m
     )
  => Type tyname uni ann
  -> m ()
handleType :: forall ann tyname (m :: * -> *) (uni :: * -> *).
(Ord ann, HasUnique tyname TypeUnique,
 MonadState (UniqueInfos ann) m, MonadWriter [UniqueError ann] m) =>
Type tyname uni ann -> m ()
handleType = \case
  TyVar ann
ann tyname
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
  TyForall ann
ann tyname
tn Kind ann
_ Type tyname uni ann
_ ->
    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
  TyLam ann
ann tyname
tn Kind ann
_ Type tyname uni ann
_ ->
    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
  Type tyname uni ann
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

runTermDefs
  :: ( Ord ann
     , HasUnique name TermUnique
     , HasUnique tyname TypeUnique
     , Monad m
     )
  => Term tyname name uni fun ann
  -> m (UniqueInfos ann, [UniqueError ann])
runTermDefs :: forall ann name tyname (m :: * -> *) (uni :: * -> *) fun.
(Ord ann, HasUnique name TermUnique, HasUnique tyname TypeUnique,
 Monad m) =>
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