{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TemplateHaskell        #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE UndecidableInstances   #-}
-- | Support for generating PIR with global definitions with dependencies between them.
module PlutusIR.Compiler.Definitions (DefT
                                              , MonadDefs (..)
                                              , TermDefWithStrictness
                                              , runDefT
                                              , defineTerm
                                              , modifyTermDef
                                              , defineType
                                              , modifyTypeDef
                                              , defineDatatype
                                              , modifyDatatypeDef
                                              , modifyDeps
                                              , recordAlias
                                              , lookupTerm
                                              , lookupOrDefineTerm
                                              , lookupType
                                              , lookupOrDefineType
                                              , lookupConstructors
                                              , lookupDestructor) where

import PlutusIR
import PlutusIR.MkPir hiding (error)

import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote

import Control.Lens
import Control.Monad.Except
import Control.Monad.Morph qualified as MM
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

import Algebra.Graph.AdjacencyMap qualified as AM
import Algebra.Graph.AdjacencyMap.Algorithm qualified as AM
import Algebra.Graph.NonEmpty.AdjacencyMap qualified as NAM
import Algebra.Graph.ToGraph qualified as Graph

import Data.Bifunctor (first, second)
import Data.Foldable
import Data.Map qualified as Map
import Data.Maybe
import Data.Set qualified as Set

-- | A map from keys to pairs of bindings and their dependencies (as a list of keys).
type DefMap key def = Map.Map key (def, Set.Set key)

mapDefs :: (a -> b) -> DefMap key a -> DefMap key b
mapDefs :: (a -> b) -> DefMap key a -> DefMap key b
mapDefs a -> b
f = ((a, Set key) -> (b, Set key)) -> DefMap key a -> DefMap key b
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((a -> b) -> (a, Set key) -> (b, Set key)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f)

type TermDefWithStrictness uni fun ann =
    PLC.Def (VarDecl TyName Name uni fun ann) (Term TyName Name uni fun ann, Strictness)

data DefState key uni fun ann = DefState {
    DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
_termDefs     :: DefMap key (TermDefWithStrictness uni fun ann),
    DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
_typeDefs     :: DefMap key (TypeDef TyName uni ann),
    DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni fun ann)
_datatypeDefs :: DefMap key (DatatypeDef TyName Name uni fun ann),
    DefState key uni fun ann -> Set key
_aliases      :: Set.Set key
    }
makeLenses ''DefState

newtype DefT key uni fun ann m a = DefT { DefT key uni fun ann m a -> StateT (DefState key uni fun ann) m a
unDefT :: StateT (DefState key uni fun ann) m a }
    deriving (a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
(a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b
(forall a b.
 (a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b)
-> (forall a b.
    a -> DefT key uni fun ann m b -> DefT key uni fun ann m a)
-> Functor (DefT key uni fun ann m)
forall a b.
a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
forall a b.
(a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Functor m =>
a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Functor m =>
(a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
$c<$ :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Functor m =>
a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
fmap :: (a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b
$cfmap :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Functor m =>
(a -> b) -> DefT key uni fun ann m a -> DefT key uni fun ann m b
Functor, Functor (DefT key uni fun ann m)
a -> DefT key uni fun ann m a
Functor (DefT key uni fun ann m)
-> (forall a. a -> DefT key uni fun ann m a)
-> (forall a b.
    DefT key uni fun ann m (a -> b)
    -> DefT key uni fun ann m a -> DefT key uni fun ann m b)
-> (forall a b c.
    (a -> b -> c)
    -> DefT key uni fun ann m a
    -> DefT key uni fun ann m b
    -> DefT key uni fun ann m c)
-> (forall a b.
    DefT key uni fun ann m a
    -> DefT key uni fun ann m b -> DefT key uni fun ann m b)
-> (forall a b.
    DefT key uni fun ann m a
    -> DefT key uni fun ann m b -> DefT key uni fun ann m a)
-> Applicative (DefT key uni fun ann m)
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m a
DefT key uni fun ann m (a -> b)
-> DefT key uni fun ann m a -> DefT key uni fun ann m b
(a -> b -> c)
-> DefT key uni fun ann m a
-> DefT key uni fun ann m b
-> DefT key uni fun ann m c
forall a. a -> DefT key uni fun ann m a
forall a b.
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m a
forall a b.
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
forall a b.
DefT key uni fun ann m (a -> b)
-> DefT key uni fun ann m a -> DefT key uni fun ann m b
forall a b c.
(a -> b -> c)
-> DefT key uni fun ann m a
-> DefT key uni fun ann m b
-> DefT key uni fun ann m c
forall key (uni :: * -> *) fun ann (m :: * -> *).
Monad m =>
Functor (DefT key uni fun ann m)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m a
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m (a -> b)
-> DefT key uni fun ann m a -> DefT key uni fun ann m b
forall key (uni :: * -> *) fun ann (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> DefT key uni fun ann m a
-> DefT key uni fun ann m b
-> DefT key uni fun ann m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m a
$c<* :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m a
*> :: DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
$c*> :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
liftA2 :: (a -> b -> c)
-> DefT key uni fun ann m a
-> DefT key uni fun ann m b
-> DefT key uni fun ann m c
$cliftA2 :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> DefT key uni fun ann m a
-> DefT key uni fun ann m b
-> DefT key uni fun ann m c
<*> :: DefT key uni fun ann m (a -> b)
-> DefT key uni fun ann m a -> DefT key uni fun ann m b
$c<*> :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m (a -> b)
-> DefT key uni fun ann m a -> DefT key uni fun ann m b
pure :: a -> DefT key uni fun ann m a
$cpure :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
$cp1Applicative :: forall key (uni :: * -> *) fun ann (m :: * -> *).
Monad m =>
Functor (DefT key uni fun ann m)
Applicative, Applicative (DefT key uni fun ann m)
a -> DefT key uni fun ann m a
Applicative (DefT key uni fun ann m)
-> (forall a b.
    DefT key uni fun ann m a
    -> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b)
-> (forall a b.
    DefT key uni fun ann m a
    -> DefT key uni fun ann m b -> DefT key uni fun ann m b)
-> (forall a. a -> DefT key uni fun ann m a)
-> Monad (DefT key uni fun ann m)
DefT key uni fun ann m a
-> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
forall a. a -> DefT key uni fun ann m a
forall a b.
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
forall a b.
DefT key uni fun ann m a
-> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b
forall key (uni :: * -> *) fun ann (m :: * -> *).
Monad m =>
Applicative (DefT key uni fun ann m)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> DefT key uni fun ann m a
$creturn :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
>> :: DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
$c>> :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
>>= :: DefT key uni fun ann m a
-> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b
$c>>= :: forall key (uni :: * -> *) fun ann (m :: * -> *) a b.
Monad m =>
DefT key uni fun ann m a
-> (a -> DefT key uni fun ann m b) -> DefT key uni fun ann m b
$cp1Monad :: forall key (uni :: * -> *) fun ann (m :: * -> *).
Monad m =>
Applicative (DefT key uni fun ann m)
Monad, m a -> DefT key uni fun ann m a
(forall (m :: * -> *) a.
 Monad m =>
 m a -> DefT key uni fun ann m a)
-> MonadTrans (DefT key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
m a -> DefT key uni fun ann m a
forall (m :: * -> *) a. Monad m => m a -> DefT key uni fun ann m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: m a -> DefT key uni fun ann m a
$clift :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
m a -> DefT key uni fun ann m a
MonadTrans, (forall a. m a -> n a)
-> DefT key uni fun ann m b -> DefT key uni fun ann n b
(forall (m :: * -> *) (n :: * -> *) b.
 Monad m =>
 (forall a. m a -> n a)
 -> DefT key uni fun ann m b -> DefT key uni fun ann n b)
-> MFunctor (DefT key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a)
-> DefT key uni fun ann m b -> DefT key uni fun ann n b
forall k (t :: (* -> *) -> k -> *).
(forall (m :: * -> *) (n :: * -> *) (b :: k).
 Monad m =>
 (forall a. m a -> n a) -> t m b -> t n b)
-> MFunctor t
forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a)
-> DefT key uni fun ann m b -> DefT key uni fun ann n b
hoist :: (forall a. m a -> n a)
-> DefT key uni fun ann m b -> DefT key uni fun ann n b
$choist :: forall key (uni :: * -> *) fun ann (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a)
-> DefT key uni fun ann m b -> DefT key uni fun ann n b
MM.MFunctor, MonadError e, MonadReader r, Monad (DefT key uni fun ann m)
Monad (DefT key uni fun ann m)
-> (forall a. Quote a -> DefT key uni fun ann m a)
-> MonadQuote (DefT key uni fun ann m)
Quote a -> DefT key uni fun ann m a
forall a. Quote a -> DefT key uni fun ann m a
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadQuote m =>
Monad (DefT key uni fun ann m)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadQuote m =>
Quote a -> DefT key uni fun ann m a
forall (m :: * -> *).
Monad m -> (forall a. Quote a -> m a) -> MonadQuote m
liftQuote :: Quote a -> DefT key uni fun ann m a
$cliftQuote :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadQuote m =>
Quote a -> DefT key uni fun ann m a
$cp1MonadQuote :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadQuote m =>
Monad (DefT key uni fun ann m)
MonadQuote, MonadWriter w)

-- Need to write this by hand, deriving wants to derive the one for DefState
instance MonadState s m => MonadState s (DefT key uni fun ann m) where
    get :: DefT key uni fun ann m s
get = m s -> DefT key uni fun ann m s
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: * -> *). MonadState s m => m s
get
    put :: s -> DefT key uni fun ann m ()
put = m () -> DefT key uni fun ann m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> DefT key uni fun ann m ())
-> (s -> m ()) -> s -> DefT key uni fun ann m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
    state :: (s -> (a, s)) -> DefT key uni fun ann m a
state = m a -> DefT key uni fun ann m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> DefT key uni fun ann m a)
-> ((s -> (a, s)) -> m a)
-> (s -> (a, s))
-> DefT key uni fun ann m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state

-- TODO: provenances
runDefT :: (Monad m, Ord key) => ann -> DefT key uni fun ann m (Term TyName Name uni fun ann) -> m (Term TyName Name uni fun ann)
runDefT :: ann
-> DefT key uni fun ann m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
runDefT ann
x DefT key uni fun ann m (Term TyName Name uni fun ann)
act = do
    (Term TyName Name uni fun ann
term, DefState key uni fun ann
s) <- StateT (DefState key uni fun ann) m (Term TyName Name uni fun ann)
-> DefState key uni fun ann
-> m (Term TyName Name uni fun ann, DefState key uni fun ann)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (DefT key uni fun ann m (Term TyName Name uni fun ann)
-> StateT
     (DefState key uni fun ann) m (Term TyName Name uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
DefT key uni fun ann m a -> StateT (DefState key uni fun ann) m a
unDefT DefT key uni fun ann m (Term TyName Name uni fun ann)
act) (DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> Set key
-> DefState key uni fun ann
forall key (uni :: * -> *) fun ann.
DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> Set key
-> DefState key uni fun ann
DefState DefMap key (TermDefWithStrictness uni fun ann)
forall a. Monoid a => a
mempty DefMap key (TypeDef TyName uni ann)
forall a. Monoid a => a
mempty DefMap key (DatatypeDef TyName Name uni fun ann)
forall a. Monoid a => a
mempty Set key
forall a. Monoid a => a
mempty)
    Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> DefMap key (Binding TyName Name uni fun ann)
-> Term TyName Name uni fun ann
-> Term TyName Name uni fun ann
forall key ann tyname name (uni :: * -> *) fun.
Ord key =>
ann
-> DefMap key (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
wrapWithDefs ann
x (DefState key uni fun ann
-> DefMap key (Binding TyName Name uni fun ann)
bindingDefs DefState key uni fun ann
s) Term TyName Name uni fun ann
term
        where
            bindingDefs :: DefState key uni fun ann
-> DefMap key (Binding TyName Name uni fun ann)
bindingDefs DefState key uni fun ann
defs =
                let
                    terms :: DefMap key (Binding TyName Name uni fun ann)
terms = (TermDefWithStrictness uni fun ann
 -> Binding TyName Name uni fun ann)
-> DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs (\TermDefWithStrictness uni fun ann
d -> ann
-> Strictness
-> VarDecl TyName Name uni fun ann
-> Term TyName Name uni fun ann
-> Binding TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x ((Term TyName Name uni fun ann, Strictness) -> Strictness
forall a b. (a, b) -> b
snd ((Term TyName Name uni fun ann, Strictness) -> Strictness)
-> (Term TyName Name uni fun ann, Strictness) -> Strictness
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann
-> (Term TyName Name uni fun ann, Strictness)
forall var val. Def var val -> val
PLC.defVal TermDefWithStrictness uni fun ann
d) (TermDefWithStrictness uni fun ann
-> VarDecl TyName Name uni fun ann
forall var val. Def var val -> var
PLC.defVar TermDefWithStrictness uni fun ann
d) ((Term TyName Name uni fun ann, Strictness)
-> Term TyName Name uni fun ann
forall a b. (a, b) -> a
fst ((Term TyName Name uni fun ann, Strictness)
 -> Term TyName Name uni fun ann)
-> (Term TyName Name uni fun ann, Strictness)
-> Term TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann
-> (Term TyName Name uni fun ann, Strictness)
forall var val. Def var val -> val
PLC.defVal TermDefWithStrictness uni fun ann
d)) (DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
_termDefs DefState key uni fun ann
defs)
                    types :: DefMap key (Binding TyName Name uni fun ann)
types = (TypeDef TyName uni ann -> Binding TyName Name uni fun ann)
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (Binding TyName Name uni fun ann)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs (\TypeDef TyName uni ann
d -> ann
-> TyVarDecl TyName ann
-> Type TyName uni ann
-> Binding TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x (TypeDef TyName uni ann -> TyVarDecl TyName ann
forall var val. Def var val -> var
PLC.defVar TypeDef TyName uni ann
d) (TypeDef TyName uni ann -> Type TyName uni ann
forall var val. Def var val -> val
PLC.defVal TypeDef TyName uni ann
d)) (DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
_typeDefs DefState key uni fun ann
defs)
                    datatypes :: DefMap key (Binding TyName Name uni fun ann)
datatypes = (DatatypeDef TyName Name uni fun ann
 -> Binding TyName Name uni fun ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs (\DatatypeDef TyName Name uni fun ann
d -> ann
-> Datatype TyName Name uni fun ann
-> Binding TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind ann
x (DatatypeDef TyName Name uni fun ann
-> Datatype TyName Name uni fun ann
forall var val. Def var val -> val
PLC.defVal DatatypeDef TyName Name uni fun ann
d)) (DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni fun ann)
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni fun ann)
_datatypeDefs DefState key uni fun ann
defs)
                in DefMap key (Binding TyName Name uni fun ann)
terms DefMap key (Binding TyName Name uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` DefMap key (Binding TyName Name uni fun ann)
types DefMap key (Binding TyName Name uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
-> DefMap key (Binding TyName Name uni fun ann)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` DefMap key (Binding TyName Name uni fun ann)
datatypes

-- | Given the definitions in the program, create a topologically ordered list of the
-- SCCs using the dependency information
defSccs :: Ord key => DefMap key def -> [ NAM.AdjacencyMap key ]
defSccs :: DefMap key def -> [AdjacencyMap key]
defSccs DefMap key def
tds =
    let
        perKeyDeps :: [(key, Set key)]
perKeyDeps = ((key, (def, Set key)) -> (key, Set key))
-> [(key, (def, Set key))] -> [(key, Set key)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(key
key, (def
_, Set key
deps)) -> (key
key, Set key
deps)) (DefMap key def -> [(key, (def, Set key))]
forall k a. Map k a -> [(k, a)]
Map.assocs DefMap key def
tds)
        keySccs :: AdjacencyMap (AdjacencyMap key)
keySccs = AdjacencyMap key -> AdjacencyMap (AdjacencyMap key)
forall a. Ord a => AdjacencyMap a -> AdjacencyMap (AdjacencyMap a)
AM.scc ([(key, Set key)] -> AdjacencyMap key
forall a. Ord a => [(a, Set a)] -> AdjacencyMap a
AM.fromAdjacencySets [(key, Set key)]
perKeyDeps)
    -- the graph made by 'scc' is guaranteed to be acyclic
    in case AdjacencyMap (AdjacencyMap key)
-> Either (Cycle (AdjacencyMap key)) [AdjacencyMap key]
forall a. Ord a => AdjacencyMap a -> Either (Cycle a) [a]
AM.topSort AdjacencyMap (AdjacencyMap key)
keySccs of
        Right [AdjacencyMap key]
sorted -> [AdjacencyMap key]
sorted
        -- TODO: report cycle
        Left Cycle (AdjacencyMap key)
_       -> [Char] -> [AdjacencyMap key]
forall a. HasCallStack => [Char] -> a
error [Char]
"No topological sort of SCC graph"

wrapWithDefs
    :: Ord key
    => ann
    -> DefMap key (Binding tyname name uni fun ann)
    -> Term tyname name uni fun ann
    -> Term tyname name uni fun ann
wrapWithDefs :: ann
-> DefMap key (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
wrapWithDefs ann
x DefMap key (Binding tyname name uni fun ann)
tds Term tyname name uni fun ann
body =
    let toValue :: key -> Maybe (Binding tyname name uni fun ann)
toValue key
k = (Binding tyname name uni fun ann, Set key)
-> Binding tyname name uni fun ann
forall a b. (a, b) -> a
fst ((Binding tyname name uni fun ann, Set key)
 -> Binding tyname name uni fun ann)
-> Maybe (Binding tyname name uni fun ann, Set key)
-> Maybe (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> key
-> DefMap key (Binding tyname name uni fun ann)
-> Maybe (Binding tyname name uni fun ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
k DefMap key (Binding tyname name uni fun ann)
tds
        wrapDefScc :: Term tyname name uni fun ann
-> AdjacencyMap key -> Term tyname name uni fun ann
wrapDefScc Term tyname name uni fun ann
acc AdjacencyMap key
scc =
            let bs :: [Binding tyname name uni fun ann]
bs = [Maybe (Binding tyname name uni fun ann)]
-> [Binding tyname name uni fun ann]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Binding tyname name uni fun ann)]
 -> [Binding tyname name uni fun ann])
-> [Maybe (Binding tyname name uni fun ann)]
-> [Binding tyname name uni fun ann]
forall a b. (a -> b) -> a -> b
$ key -> Maybe (Binding tyname name uni fun ann)
toValue (key -> Maybe (Binding tyname name uni fun ann))
-> [key] -> [Maybe (Binding tyname name uni fun ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AdjacencyMap key -> [ToVertex (AdjacencyMap key)]
forall t. (ToGraph t, Ord (ToVertex t)) => t -> [ToVertex t]
Graph.vertexList AdjacencyMap key
scc
            in ann
-> Recursivity
-> [Binding tyname name uni fun ann]
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall a tyname name (uni :: * -> *) fun.
a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
mkLet ann
x (if AdjacencyMap key -> Bool
forall t. (ToGraph t, Ord (ToVertex t)) => t -> Bool
Graph.isAcyclic AdjacencyMap key
scc then Recursivity
NonRec else Recursivity
Rec) [Binding tyname name uni fun ann]
bs Term tyname name uni fun ann
acc
    -- process from the inside out
    in (Term tyname name uni fun ann
 -> AdjacencyMap key -> Term tyname name uni fun ann)
-> Term tyname name uni fun ann
-> [AdjacencyMap key]
-> Term tyname name uni fun ann
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Term tyname name uni fun ann
-> AdjacencyMap key -> Term tyname name uni fun ann
wrapDefScc Term tyname name uni fun ann
body (DefMap key (Binding tyname name uni fun ann) -> [AdjacencyMap key]
forall key def. Ord key => DefMap key def -> [AdjacencyMap key]
defSccs DefMap key (Binding tyname name uni fun ann)
tds)

class (Monad m, Ord key) => MonadDefs key uni fun ann m | m -> key uni fun ann where
    liftDef :: DefT key uni fun ann Identity a -> m a
    default liftDef :: (MonadDefs key uni fun ann n, MonadTrans t, t n ~ m) => DefT key uni fun ann Identity a -> m a
    liftDef = n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n a -> t n a)
-> (DefT key uni fun ann Identity a -> n a)
-> DefT key uni fun ann Identity a
-> t n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefT key uni fun ann Identity a -> n a
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef

instance (Ord key, Monad m) => MonadDefs key uni fun ann (DefT key uni fun ann m) where
    liftDef :: DefT key uni fun ann Identity a -> DefT key uni fun ann m a
liftDef = (forall a. Identity a -> m a)
-> DefT key uni fun ann Identity a -> DefT key uni fun ann m a
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
MM.hoist (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Identity a -> a) -> Identity a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity)

instance MonadDefs key uni fun ann m => MonadDefs key uni fun ann (StateT s m)
instance MonadDefs key uni fun ann m => MonadDefs key uni fun ann (ExceptT e m)
instance MonadDefs key uni fun ann m => MonadDefs key uni fun ann (ReaderT r m)

defineTerm :: MonadDefs key uni fun ann m => key -> TermDefWithStrictness uni fun ann -> Set.Set key -> m ()
defineTerm :: key -> TermDefWithStrictness uni fun ann -> Set key -> m ()
defineTerm key
name TermDefWithStrictness uni fun ann
def Set key
deps = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
termDefs ((DefMap key (TermDefWithStrictness uni fun ann)
  -> DefMap key (TermDefWithStrictness uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ key
-> (TermDefWithStrictness uni fun ann, Set key)
-> DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (TermDefWithStrictness uni fun ann)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert key
name (TermDefWithStrictness uni fun ann
def, Set key
deps)

modifyTermDef :: MonadDefs key uni fun ann m => key -> (TermDefWithStrictness uni fun ann -> TermDefWithStrictness uni fun ann)-> m ()
modifyTermDef :: key
-> (TermDefWithStrictness uni fun ann
    -> TermDefWithStrictness uni fun ann)
-> m ()
modifyTermDef key
name TermDefWithStrictness uni fun ann
-> TermDefWithStrictness uni fun ann
f = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
termDefs ((DefMap key (TermDefWithStrictness uni fun ann)
  -> DefMap key (TermDefWithStrictness uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((TermDefWithStrictness uni fun ann, Set key)
 -> (TermDefWithStrictness uni fun ann, Set key))
-> key
-> DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (TermDefWithStrictness uni fun ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((TermDefWithStrictness uni fun ann
 -> TermDefWithStrictness uni fun ann)
-> (TermDefWithStrictness uni fun ann, Set key)
-> (TermDefWithStrictness uni fun ann, Set key)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TermDefWithStrictness uni fun ann
-> TermDefWithStrictness uni fun ann
f) key
name

defineType :: MonadDefs key uni fun ann m => key -> TypeDef TyName uni ann -> Set.Set key -> m ()
defineType :: key -> TypeDef TyName uni ann -> Set key -> m ()
defineType key
name TypeDef TyName uni ann
def Set key
deps = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann) (DefMap key (TypeDef TyName uni ann))
typeDefs ((DefMap key (TypeDef TyName uni ann)
  -> DefMap key (TypeDef TyName uni ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ key
-> (TypeDef TyName uni ann, Set key)
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (TypeDef TyName uni ann)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert key
name (TypeDef TyName uni ann
def, Set key
deps)

modifyTypeDef :: MonadDefs key uni fun ann m => key -> (TypeDef TyName uni ann -> TypeDef TyName uni ann)-> m ()
modifyTypeDef :: key -> (TypeDef TyName uni ann -> TypeDef TyName uni ann) -> m ()
modifyTypeDef key
name TypeDef TyName uni ann -> TypeDef TyName uni ann
f = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann) (DefMap key (TypeDef TyName uni ann))
typeDefs ((DefMap key (TypeDef TyName uni ann)
  -> DefMap key (TypeDef TyName uni ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((TypeDef TyName uni ann, Set key)
 -> (TypeDef TyName uni ann, Set key))
-> key
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (TypeDef TyName uni ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((TypeDef TyName uni ann -> TypeDef TyName uni ann)
-> (TypeDef TyName uni ann, Set key)
-> (TypeDef TyName uni ann, Set key)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TypeDef TyName uni ann -> TypeDef TyName uni ann
f) key
name

defineDatatype
    :: forall key uni fun ann m . MonadDefs key uni fun ann m
    => key -> DatatypeDef TyName Name uni fun ann -> Set.Set key -> m ()
defineDatatype :: key -> DatatypeDef TyName Name uni fun ann -> Set key -> m ()
defineDatatype key
name DatatypeDef TyName Name uni fun ann
def Set key
deps = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni fun ann)
  -> DefMap key (DatatypeDef TyName Name uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ key
-> (DatatypeDef TyName Name uni fun ann, Set key)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert key
name (DatatypeDef TyName Name uni fun ann
def, Set key
deps)

modifyDatatypeDef :: MonadDefs key uni fun ann m => key -> (DatatypeDef TyName Name uni fun ann -> DatatypeDef TyName Name uni fun ann)-> m ()
modifyDatatypeDef :: key
-> (DatatypeDef TyName Name uni fun ann
    -> DatatypeDef TyName Name uni fun ann)
-> m ()
modifyDatatypeDef key
name DatatypeDef TyName Name uni fun ann
-> DatatypeDef TyName Name uni fun ann
f = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni fun ann)
  -> DefMap key (DatatypeDef TyName Name uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((DatatypeDef TyName Name uni fun ann, Set key)
 -> (DatatypeDef TyName Name uni fun ann, Set key))
-> key
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((DatatypeDef TyName Name uni fun ann
 -> DatatypeDef TyName Name uni fun ann)
-> (DatatypeDef TyName Name uni fun ann, Set key)
-> (DatatypeDef TyName Name uni fun ann, Set key)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first DatatypeDef TyName Name uni fun ann
-> DatatypeDef TyName Name uni fun ann
f) key
name

-- | Modifies the dependency set of a key.
modifyDeps :: MonadDefs key uni fun ann m => key -> (Set.Set key -> Set.Set key)-> m ()
modifyDeps :: key -> (Set key -> Set key) -> m ()
modifyDeps key
name Set key -> Set key
f = DefT key uni fun ann Identity () -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ do
    -- This is a little crude: we expect most keys will appear in only one map, so we just modify the
    -- dependencies in all of them! That lets us just have one function.
    (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
termDefs ((DefMap key (TermDefWithStrictness uni fun ann)
  -> DefMap key (TermDefWithStrictness uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((TermDefWithStrictness uni fun ann, Set key)
 -> (TermDefWithStrictness uni fun ann, Set key))
-> key
-> DefMap key (TermDefWithStrictness uni fun ann)
-> DefMap key (TermDefWithStrictness uni fun ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((Set key -> Set key)
-> (TermDefWithStrictness uni fun ann, Set key)
-> (TermDefWithStrictness uni fun ann, Set key)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Set key -> Set key
f) key
name
    (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TypeDef TyName uni ann))
  (DefMap key (TypeDef TyName uni ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann) (DefMap key (TypeDef TyName uni ann))
typeDefs ((DefMap key (TypeDef TyName uni ann)
  -> DefMap key (TypeDef TyName uni ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (TypeDef TyName uni ann)
    -> DefMap key (TypeDef TyName uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((TypeDef TyName uni ann, Set key)
 -> (TypeDef TyName uni ann, Set key))
-> key
-> DefMap key (TypeDef TyName uni ann)
-> DefMap key (TypeDef TyName uni ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((Set key -> Set key)
-> (TypeDef TyName uni ann, Set key)
-> (TypeDef TyName uni ann, Set key)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Set key -> Set key
f) key
name
    (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni fun ann)
  -> DefMap key (DatatypeDef TyName Name uni fun ann))
 -> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni fun ann)
    -> DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((DatatypeDef TyName Name uni fun ann, Set key)
 -> (DatatypeDef TyName Name uni fun ann, Set key))
-> key
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> DefMap key (DatatypeDef TyName Name uni fun ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((Set key -> Set key)
-> (DatatypeDef TyName Name uni fun ann, Set key)
-> (DatatypeDef TyName Name uni fun ann, Set key)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Set key -> Set key
f) key
name

recordAlias :: forall key uni fun ann m . MonadDefs key uni fun ann m => key -> m ()
recordAlias :: key -> m ()
recordAlias key
name = forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
forall (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef @key @uni @fun @ann (DefT key uni fun ann Identity () -> m ())
-> DefT key uni fun ann Identity () -> m ()
forall a b. (a -> b) -> a -> b
$ StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT (DefState key uni fun ann) Identity ()
 -> DefT key uni fun ann Identity ())
-> StateT (DefState key uni fun ann) Identity ()
-> DefT key uni fun ann Identity ()
forall a b. (a -> b) -> a -> b
$ (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (Set key)
  (Set key)
-> (Set key -> Set key)
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (Set key)
  (Set key)
forall key (uni :: * -> *) fun ann.
Lens' (DefState key uni fun ann) (Set key)
aliases (key -> Set key -> Set key
forall a. Ord a => a -> Set a -> Set a
Set.insert key
name)

lookupTerm :: (MonadDefs key uni fun ann m) => ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupTerm :: ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupTerm ann
x key
name = do
    DefState{_termDefs :: forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
_termDefs=DefMap key (TermDefWithStrictness uni fun ann)
ds,_aliases :: forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> Set key
_aliases=Set key
as} <- DefT key uni fun ann Identity (DefState key uni fun ann)
-> m (DefState key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity (DefState key uni fun ann)
 -> m (DefState key uni fun ann))
-> DefT key uni fun ann Identity (DefState key uni fun ann)
-> m (DefState key uni fun ann)
forall a b. (a -> b) -> a -> b
$ StateT
  (DefState key uni fun ann) Identity (DefState key uni fun ann)
-> DefT key uni fun ann Identity (DefState key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT StateT
  (DefState key uni fun ann) Identity (DefState key uni fun ann)
forall s (m :: * -> *). MonadState s m => m s
get
    Maybe (Term TyName Name uni fun ann)
-> m (Maybe (Term TyName Name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term TyName Name uni fun ann)
 -> m (Maybe (Term TyName Name uni fun ann)))
-> Maybe (Term TyName Name uni fun ann)
-> m (Maybe (Term TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ case key
-> DefMap key (TermDefWithStrictness uni fun ann)
-> Maybe (TermDefWithStrictness uni fun ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (TermDefWithStrictness uni fun ann)
ds of
        Just (TermDefWithStrictness uni fun ann
def, Set key
_) | Bool -> Bool
not (key -> Set key -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member key
name Set key
as) -> Term TyName Name uni fun ann
-> Maybe (Term TyName Name uni fun ann)
forall a. a -> Maybe a
Just (Term TyName Name uni fun ann
 -> Maybe (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann
-> Maybe (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ann
x (VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann
-> VarDecl TyName Name uni fun ann
forall var val. Def var val -> var
PLC.defVar TermDefWithStrictness uni fun ann
def
        Maybe (TermDefWithStrictness uni fun ann, Set key)
_                                        -> Maybe (Term TyName Name uni fun ann)
forall a. Maybe a
Nothing

lookupOrDefineTerm :: (MonadDefs key uni fun ann m) => ann -> key -> m (TermDefWithStrictness uni fun ann, Set.Set key) -> m (Term TyName Name uni fun ann)
lookupOrDefineTerm :: ann
-> key
-> m (TermDefWithStrictness uni fun ann, Set key)
-> m (Term TyName Name uni fun ann)
lookupOrDefineTerm ann
x key
name m (TermDefWithStrictness uni fun ann, Set key)
mdef = do
    Maybe (Term TyName Name uni fun ann)
mTerm <- ann -> key -> m (Maybe (Term TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupTerm ann
x key
name
    case Maybe (Term TyName Name uni fun ann)
mTerm of
        Just Term TyName Name uni fun ann
t -> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName Name uni fun ann
t
        Maybe (Term TyName Name uni fun ann)
Nothing -> do
            (TermDefWithStrictness uni fun ann
def, Set key
deps) <- m (TermDefWithStrictness uni fun ann, Set key)
mdef
            key -> TermDefWithStrictness uni fun ann -> Set key -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> TermDefWithStrictness uni fun ann -> Set key -> m ()
defineTerm key
name TermDefWithStrictness uni fun ann
def Set key
deps
            Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann -> m (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ann
x (VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann
-> VarDecl TyName Name uni fun ann
forall var val. Def var val -> var
PLC.defVar TermDefWithStrictness uni fun ann
def

lookupType :: (MonadDefs key uni fun ann m) => ann -> key -> m (Maybe (Type TyName uni ann))
lookupType :: ann -> key -> m (Maybe (Type TyName uni ann))
lookupType ann
x key
name = do
    DefState{_typeDefs :: forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
_typeDefs=DefMap key (TypeDef TyName uni ann)
tys, _datatypeDefs :: forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni fun ann)
_datatypeDefs=DefMap key (DatatypeDef TyName Name uni fun ann)
dtys, _aliases :: forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> Set key
_aliases=Set key
as} <- DefT key uni fun ann Identity (DefState key uni fun ann)
-> m (DefState key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT key uni fun ann Identity (DefState key uni fun ann)
 -> m (DefState key uni fun ann))
-> DefT key uni fun ann Identity (DefState key uni fun ann)
-> m (DefState key uni fun ann)
forall a b. (a -> b) -> a -> b
$ StateT
  (DefState key uni fun ann) Identity (DefState key uni fun ann)
-> DefT key uni fun ann Identity (DefState key uni fun ann)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT StateT
  (DefState key uni fun ann) Identity (DefState key uni fun ann)
forall s (m :: * -> *). MonadState s m => m s
get
    Maybe (Type TyName uni ann) -> m (Maybe (Type TyName uni ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Type TyName uni ann) -> m (Maybe (Type TyName uni ann)))
-> Maybe (Type TyName uni ann) -> m (Maybe (Type TyName uni ann))
forall a b. (a -> b) -> a -> b
$ case key
-> DefMap key (TypeDef TyName uni ann)
-> Maybe (TypeDef TyName uni ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (TypeDef TyName uni ann)
tys of
        Just (TypeDef TyName uni ann
def, Set key
_) -> Type TyName uni ann -> Maybe (Type TyName uni ann)
forall a. a -> Maybe a
Just (Type TyName uni ann -> Maybe (Type TyName uni ann))
-> Type TyName uni ann -> Maybe (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ if key -> Set key -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member key
name Set key
as then TypeDef TyName uni ann -> Type TyName uni ann
forall var val. Def var val -> val
PLC.defVal TypeDef TyName uni ann
def else ann -> TyVarDecl TyName ann -> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ann
x (TyVarDecl TyName ann -> Type TyName uni ann)
-> TyVarDecl TyName ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ TypeDef TyName uni ann -> TyVarDecl TyName ann
forall var val. Def var val -> var
PLC.defVar TypeDef TyName uni ann
def
        Maybe (TypeDef TyName uni ann, Set key)
Nothing -> case key
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> Maybe (DatatypeDef TyName Name uni fun ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni fun ann)
dtys of
            Just (DatatypeDef TyName Name uni fun ann
def, Set key
_) -> Type TyName uni ann -> Maybe (Type TyName uni ann)
forall a. a -> Maybe a
Just (Type TyName uni ann -> Maybe (Type TyName uni ann))
-> Type TyName uni ann -> Maybe (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> TyVarDecl TyName ann -> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ann
x (TyVarDecl TyName ann -> Type TyName uni ann)
-> TyVarDecl TyName ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ DatatypeDef TyName Name uni fun ann -> TyVarDecl TyName ann
forall var val. Def var val -> var
PLC.defVar DatatypeDef TyName Name uni fun ann
def
            Maybe (DatatypeDef TyName Name uni fun ann, Set key)
Nothing       -> Maybe (Type TyName uni ann)
forall a. Maybe a
Nothing

lookupOrDefineType :: (MonadDefs key uni fun ann m) => ann -> key -> m (TypeDef TyName uni ann, Set.Set key) -> m (Type TyName uni ann)
lookupOrDefineType :: ann
-> key
-> m (TypeDef TyName uni ann, Set key)
-> m (Type TyName uni ann)
lookupOrDefineType ann
x key
name m (TypeDef TyName uni ann, Set key)
mdef = do
    Maybe (Type TyName uni ann)
mTy <- ann -> key -> m (Maybe (Type TyName uni ann))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Type TyName uni ann))
lookupType ann
x key
name
    case Maybe (Type TyName uni ann)
mTy of
        Just Type TyName uni ann
ty -> Type TyName uni ann -> m (Type TyName uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ann
ty
        Maybe (Type TyName uni ann)
Nothing -> do
            (TypeDef TyName uni ann
def, Set key
deps) <- m (TypeDef TyName uni ann, Set key)
mdef
            key -> TypeDef TyName uni ann -> Set key -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> TypeDef TyName uni ann -> Set key -> m ()
defineType key
name TypeDef TyName uni ann
def Set key
deps
            Type TyName uni ann -> m (Type TyName uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> m (Type TyName uni ann))
-> Type TyName uni ann -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> TyVarDecl TyName ann -> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ann
x (TyVarDecl TyName ann -> Type TyName uni ann)
-> TyVarDecl TyName ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ TypeDef TyName uni ann -> TyVarDecl TyName ann
forall var val. Def var val -> var
PLC.defVar TypeDef TyName uni ann
def

lookupConstructors :: (MonadDefs key uni fun ann m) => ann -> key -> m (Maybe [Term TyName Name uni fun ann])
lookupConstructors :: ann -> key -> m (Maybe [Term TyName Name uni fun ann])
lookupConstructors ann
x key
name = do
    DefMap key (DatatypeDef TyName Name uni fun ann)
ds <- DefT
  key
  uni
  fun
  ann
  Identity
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> m (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef (DefT
   key
   uni
   fun
   ann
   Identity
   (DefMap key (DatatypeDef TyName Name uni fun ann))
 -> m (DefMap key (DatatypeDef TyName Name uni fun ann)))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
-> m (DefMap key (DatatypeDef TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ StateT
  (DefState key uni fun ann)
  Identity
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT
   (DefState key uni fun ann)
   Identity
   (DefMap key (DatatypeDef TyName Name uni fun ann))
 -> DefT
      key
      uni
      fun
      ann
      Identity
      (DefMap key (DatatypeDef TyName Name uni fun ann)))
-> StateT
     (DefState key uni fun ann)
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Getting
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> StateT
     (DefState key uni fun ann)
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
datatypeDefs
    Maybe [Term TyName Name uni fun ann]
-> m (Maybe [Term TyName Name uni fun ann])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe [Term TyName Name uni fun ann]
 -> m (Maybe [Term TyName Name uni fun ann]))
-> Maybe [Term TyName Name uni fun ann]
-> m (Maybe [Term TyName Name uni fun ann])
forall a b. (a -> b) -> a -> b
$ case key
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> Maybe (DatatypeDef TyName Name uni fun ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni fun ann)
ds of
        Just (PLC.Def{defVal :: forall var val. Def var val -> val
PLC.defVal=(Datatype ann
_ TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
_ Name
_ [VarDecl TyName Name uni fun ann]
constrs)}, Set key
_) -> [Term TyName Name uni fun ann]
-> Maybe [Term TyName Name uni fun ann]
forall a. a -> Maybe a
Just ([Term TyName Name uni fun ann]
 -> Maybe [Term TyName Name uni fun ann])
-> [Term TyName Name uni fun ann]
-> Maybe [Term TyName Name uni fun ann]
forall a b. (a -> b) -> a -> b
$ (VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann)
-> [VarDecl TyName Name uni fun ann]
-> [Term TyName Name uni fun ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ann
-> VarDecl TyName Name uni fun ann -> Term TyName Name uni fun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ann
x) [VarDecl TyName Name uni fun ann]
constrs
        Maybe (DatatypeDef TyName Name uni fun ann, Set key)
Nothing                                                  -> Maybe [Term TyName Name uni fun ann]
forall a. Maybe a
Nothing

lookupDestructor
    :: forall key uni fun ann m . (MonadDefs key uni fun ann m)
    => ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupDestructor :: ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupDestructor ann
x key
name = do
    DefMap key (DatatypeDef TyName Name uni fun ann)
ds <- forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
forall (m :: * -> *) a.
MonadDefs key uni fun ann m =>
DefT key uni fun ann Identity a -> m a
liftDef @key @uni @fun @ann (DefT
   key
   uni
   fun
   ann
   Identity
   (DefMap key (DatatypeDef TyName Name uni fun ann))
 -> m (DefMap key (DatatypeDef TyName Name uni fun ann)))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
-> m (DefMap key (DatatypeDef TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ StateT
  (DefState key uni fun ann)
  Identity
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
StateT (DefState key uni fun ann) m a -> DefT key uni fun ann m a
DefT (StateT
   (DefState key uni fun ann)
   Identity
   (DefMap key (DatatypeDef TyName Name uni fun ann))
 -> DefT
      key
      uni
      fun
      ann
      Identity
      (DefMap key (DatatypeDef TyName Name uni fun ann)))
-> StateT
     (DefState key uni fun ann)
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
-> DefT
     key
     uni
     fun
     ann
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Getting
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
-> StateT
     (DefState key uni fun ann)
     Identity
     (DefMap key (DatatypeDef TyName Name uni fun ann))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (DefMap key (DatatypeDef TyName Name uni fun ann))
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
forall key (uni :: * -> *) fun ann.
Lens'
  (DefState key uni fun ann)
  (DefMap key (DatatypeDef TyName Name uni fun ann))
datatypeDefs
    Maybe (Term TyName Name uni fun ann)
-> m (Maybe (Term TyName Name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term TyName Name uni fun ann)
 -> m (Maybe (Term TyName Name uni fun ann)))
-> Maybe (Term TyName Name uni fun ann)
-> m (Maybe (Term TyName Name uni fun ann))
forall a b. (a -> b) -> a -> b
$ case key
-> DefMap key (DatatypeDef TyName Name uni fun ann)
-> Maybe (DatatypeDef TyName Name uni fun ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni fun ann)
ds of
        Just (PLC.Def{defVal :: forall var val. Def var val -> val
PLC.defVal=(Datatype ann
_ TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
_ Name
destr [VarDecl TyName Name uni fun ann]
_)}, Set key
_) -> Term TyName Name uni fun ann
-> Maybe (Term TyName Name uni fun ann)
forall a. a -> Maybe a
Just (Term TyName Name uni fun ann
 -> Maybe (Term TyName Name uni fun ann))
-> Term TyName Name uni fun ann
-> Maybe (Term TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Name -> Term TyName Name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var ann
x Name
destr
        Maybe (DatatypeDef TyName Name uni fun ann, Set key)
Nothing                                                -> Maybe (Term TyName Name uni fun ann)
forall a. Maybe a
Nothing