{-# LANGUAGE LambdaCase #-}
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
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)
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
-> ann
-> ScopeType
-> 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)
checkUndefined
:: (HasUnique n u,
MonadState (UniqueInfos ann) m,
MonadWriter [UniqueError ann] m)
=> n
-> ScopedLoc ann
-> UniqueInfo ann
-> 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
-> ann
-> ScopeType
-> 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
-> ScopedLoc ann
-> UniqueInfo ann
-> 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
-> ScopedLoc ann
-> UniqueInfo ann
-> 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]
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 ()
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