{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
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 as PIR
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 qualified as Foldable
import Data.Map qualified as Map
import Data.Maybe
import Data.Set qualified as Set
type DefMap key def = Map.Map key (def, Set.Set key)
mapDefs :: (a -> b) -> DefMap key a -> DefMap key b
mapDefs :: forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs a -> b
f = ((a, Set key) -> (b, Set key))
-> Map key (a, Set key) -> Map key (b, Set key)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((a -> b) -> (a, Set key) -> (b, Set key)
forall a b c. (a -> b) -> (a, c) -> (b, c)
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 ann) (Term TyName Name uni fun ann, Strictness)
data DefState key uni fun ann = DefState
{ forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
_termDefs :: DefMap key (TermDefWithStrictness uni fun ann)
, forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
_typeDefs :: DefMap key (TypeDef TyName uni ann)
, forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni ann)
_datatypeDefs :: DefMap key (DatatypeDef TyName Name uni ann)
, forall key (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 {forall key (uni :: * -> *) fun ann (m :: * -> *) a.
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 newtype
( (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
$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
fmap :: forall a b.
(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.
Functor m =>
a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
<$ :: forall a b.
a -> DefT key uni fun ann m b -> DefT key uni fun ann m a
Functor
, Functor (DefT key uni fun ann m)
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)
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
$cpure :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
pure :: forall a. a -> 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 -> b)
-> DefT key uni fun ann m a -> 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
$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
liftA2 :: 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
$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
*> :: forall a b.
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 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
Applicative
, Applicative (DefT key uni fun ann m)
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)
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
$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
>>= :: 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
$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
>> :: forall a b.
DefT key uni fun ann m a
-> DefT key uni fun ann m b -> DefT key uni fun ann m b
$creturn :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
a -> DefT key uni fun ann m a
return :: forall a. a -> DefT key uni fun ann m a
Monad
, (forall (m :: * -> *).
Monad m =>
Monad (DefT key uni fun ann m)) =>
(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 :: * -> *).
Monad m =>
Monad (DefT key uni fun ann m)
forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
m a -> DefT key uni fun ann m a
forall (m :: * -> *). Monad m => Monad (DefT key uni fun ann m)
forall (m :: * -> *) a. Monad m => m a -> DefT key uni fun ann m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
Monad m =>
m a -> DefT key uni fun ann m a
lift :: forall (m :: * -> *) a. Monad m => m a -> DefT key uni fun ann m a
MonadTrans
, (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
$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
hoist :: 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
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)
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
$cliftQuote :: forall key (uni :: * -> *) fun ann (m :: * -> *) a.
MonadQuote m =>
Quote a -> DefT key uni fun ann m a
liftQuote :: forall a. Quote a -> DefT key uni fun ann m a
MonadQuote
, MonadWriter w
)
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 (m :: * -> *) a. Monad m => m a -> DefT key uni fun ann m a
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 (m :: * -> *) a. Monad m => m a -> DefT key uni fun ann m a
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 :: forall a. (s -> (a, s)) -> DefT key uni fun ann m a
state = 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 :: (* -> *) -> * -> *) (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 a. (s -> (a, s)) -> m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state
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 :: forall (m :: * -> *) key ann (uni :: * -> *) fun.
(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
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 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 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 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 a. a -> m a
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)
forall {k} {uni :: * -> *} {fun} {a}.
Ord k =>
DefState k uni fun a
-> Map k (Binding TyName Name uni fun a, Set k)
bindingDefs DefState key uni fun ann
s) Term TyName Name uni fun ann
term
where
bindingDefs :: DefState k uni fun a
-> Map k (Binding TyName Name uni fun a, Set k)
bindingDefs DefState k uni fun a
defs =
let
terms :: Map k (Binding TyName Name uni fun a, Set k)
terms =
(Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
-> Binding TyName Name uni fun a)
-> DefMap
k
(Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness))
-> Map k (Binding TyName Name uni fun a, Set k)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs
( \Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
d ->
a
-> Strictness
-> VarDecl TyName Name uni a
-> Term TyName Name uni fun a
-> Binding TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind
(VarDecl TyName Name uni a -> a
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> ann
_varDeclAnn (Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
-> VarDecl TyName Name uni a
forall var val. Def var val -> var
defVar Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
d))
((Term TyName Name uni fun a, Strictness) -> Strictness
forall a b. (a, b) -> b
snd ((Term TyName Name uni fun a, Strictness) -> Strictness)
-> (Term TyName Name uni fun a, Strictness) -> Strictness
forall a b. (a -> b) -> a -> b
$ Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
-> (Term TyName Name uni fun a, Strictness)
forall var val. Def var val -> val
PLC.defVal Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
d)
(Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
-> VarDecl TyName Name uni a
forall var val. Def var val -> var
PLC.defVar Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
d)
((Term TyName Name uni fun a, Strictness)
-> Term TyName Name uni fun a
forall a b. (a, b) -> a
fst ((Term TyName Name uni fun a, Strictness)
-> Term TyName Name uni fun a)
-> (Term TyName Name uni fun a, Strictness)
-> Term TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$ Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
-> (Term TyName Name uni fun a, Strictness)
forall var val. Def var val -> val
PLC.defVal Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness)
d)
)
(DefState k uni fun a
-> DefMap
k
(Def
(VarDecl TyName Name uni a)
(Term TyName Name uni fun a, Strictness))
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (TermDefWithStrictness uni fun ann)
_termDefs DefState k uni fun a
defs)
types :: Map k (Binding TyName Name uni fun a, Set k)
types =
(Def (TyVarDecl TyName a) (Type TyName uni a)
-> Binding TyName Name uni fun a)
-> DefMap k (Def (TyVarDecl TyName a) (Type TyName uni a))
-> Map k (Binding TyName Name uni fun a, Set k)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs
( \Def (TyVarDecl TyName a) (Type TyName uni a)
d ->
a
-> TyVarDecl TyName a
-> Type TyName uni a
-> Binding TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind (TyVarDecl TyName a -> a
forall tyname ann. TyVarDecl tyname ann -> ann
_tyVarDeclAnn (Def (TyVarDecl TyName a) (Type TyName uni a) -> TyVarDecl TyName a
forall var val. Def var val -> var
defVar Def (TyVarDecl TyName a) (Type TyName uni a)
d)) (Def (TyVarDecl TyName a) (Type TyName uni a) -> TyVarDecl TyName a
forall var val. Def var val -> var
PLC.defVar Def (TyVarDecl TyName a) (Type TyName uni a)
d) (Def (TyVarDecl TyName a) (Type TyName uni a) -> Type TyName uni a
forall var val. Def var val -> val
PLC.defVal Def (TyVarDecl TyName a) (Type TyName uni a)
d)
)
(DefState k uni fun a
-> DefMap k (Def (TyVarDecl TyName a) (Type TyName uni a))
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann -> DefMap key (TypeDef TyName uni ann)
_typeDefs DefState k uni fun a
defs)
datatypes :: Map k (Binding TyName Name uni fun a, Set k)
datatypes =
(Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
-> Binding TyName Name uni fun a)
-> DefMap k (Def (TyVarDecl TyName a) (Datatype TyName Name uni a))
-> Map k (Binding TyName Name uni fun a, Set k)
forall a b key. (a -> b) -> DefMap key a -> DefMap key b
mapDefs
(\Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
d -> a -> Datatype TyName Name uni a -> Binding TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind (TyVarDecl TyName a -> a
forall tyname ann. TyVarDecl tyname ann -> ann
_tyVarDeclAnn (Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
-> TyVarDecl TyName a
forall var val. Def var val -> var
defVar Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
d)) (Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
-> Datatype TyName Name uni a
forall var val. Def var val -> val
PLC.defVal Def (TyVarDecl TyName a) (Datatype TyName Name uni a)
d))
(DefState k uni fun a
-> DefMap k (Def (TyVarDecl TyName a) (Datatype TyName Name uni a))
forall key (uni :: * -> *) fun ann.
DefState key uni fun ann
-> DefMap key (DatatypeDef TyName Name uni ann)
_datatypeDefs DefState k uni fun a
defs)
in
Map k (Binding TyName Name uni fun a, Set k)
terms Map k (Binding TyName Name uni fun a, Set k)
-> Map k (Binding TyName Name uni fun a, Set k)
-> Map k (Binding TyName Name uni fun a, Set k)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map k (Binding TyName Name uni fun a, Set k)
types Map k (Binding TyName Name uni fun a, Set k)
-> Map k (Binding TyName Name uni fun a, Set k)
-> Map k (Binding TyName Name uni fun a, Set k)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map k (Binding TyName Name uni fun a, Set k)
datatypes
defSccs :: (Ord key) => DefMap key def -> [NAM.AdjacencyMap key]
defSccs :: forall key def. Ord key => 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 a b. (a -> b) -> [a] -> [b]
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)
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
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 :: 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 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
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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.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 -> m a
n a -> t n a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n a -> m a)
-> (DefT key uni fun ann Identity a -> n a)
-> DefT key uni fun ann Identity a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefT key uni fun ann Identity a -> n a
forall a. 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 :: forall a.
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
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
MM.hoist (a -> m a
forall a. 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 :: 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 = DefT key uni fun ann Identity () -> m ()
forall a. DefT key uni fun ann Identity a -> m a
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 fun (f :: * -> *).
Functor f =>
(DefMap key (TermDefWithStrictness uni fun ann)
-> f (DefMap key (TermDefWithStrictness uni fun ann)))
-> DefState key uni fun ann -> f (DefState key 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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
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 a. DefT key uni fun ann Identity a -> m a
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 fun (f :: * -> *).
Functor f =>
(DefMap key (TermDefWithStrictness uni fun ann)
-> f (DefMap key (TermDefWithStrictness uni fun ann)))
-> DefState key uni fun ann -> f (DefState key 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 a b c. (a -> b) -> (a, c) -> (b, c)
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 :: 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 = DefT key uni fun ann Identity () -> m ()
forall a. DefT key uni fun ann Identity a -> m a
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 (f :: * -> *).
Functor f =>
(DefMap key (TypeDef TyName uni ann)
-> f (DefMap key (TypeDef TyName uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun 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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
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 a. DefT key uni fun ann Identity a -> m a
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 (f :: * -> *).
Functor f =>
(DefMap key (TypeDef TyName uni ann)
-> f (DefMap key (TypeDef TyName uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun 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 a b c. (a -> b) -> (a, c) -> (b, c)
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 ann ->
Set.Set key ->
m ()
defineDatatype :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> DatatypeDef TyName Name uni ann -> Set key -> m ()
defineDatatype key
name DatatypeDef TyName Name uni ann
def Set key
deps =
DefT key uni fun ann Identity () -> m ()
forall a. DefT key uni fun ann Identity a -> m a
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 ann))
(DefMap key (DatatypeDef TyName Name uni ann))
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name 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 (DatatypeDef TyName Name uni ann))
(DefMap key (DatatypeDef TyName Name uni ann))
forall key (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(DefMap key (DatatypeDef TyName Name uni ann)
-> f (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ key
-> (DatatypeDef TyName Name uni ann, Set key)
-> DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert key
name (DatatypeDef TyName Name uni ann
def, Set key
deps)
modifyDatatypeDef ::
(MonadDefs key uni fun ann m) =>
key ->
(DatatypeDef TyName Name uni ann -> DatatypeDef TyName Name uni ann) ->
m ()
modifyDatatypeDef :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key
-> (DatatypeDef TyName Name uni ann
-> DatatypeDef TyName Name uni ann)
-> m ()
modifyDatatypeDef key
name DatatypeDef TyName Name uni ann -> DatatypeDef TyName Name uni ann
f = DefT key uni fun ann Identity () -> m ()
forall a. DefT key uni fun ann Identity a -> m a
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 ann))
(DefMap key (DatatypeDef TyName Name uni ann))
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name 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 (DatatypeDef TyName Name uni ann))
(DefMap key (DatatypeDef TyName Name uni ann))
forall key (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(DefMap key (DatatypeDef TyName Name uni ann)
-> f (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((DatatypeDef TyName Name uni ann, Set key)
-> (DatatypeDef TyName Name uni ann, Set key))
-> key
-> DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ((DatatypeDef TyName Name uni ann
-> DatatypeDef TyName Name uni ann)
-> (DatatypeDef TyName Name uni ann, Set key)
-> (DatatypeDef TyName Name uni ann, Set key)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first DatatypeDef TyName Name uni ann -> DatatypeDef TyName Name uni ann
f) key
name
modifyDeps :: (MonadDefs key uni fun ann m) => key -> (Set.Set key -> Set.Set key) -> m ()
modifyDeps :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> (Set key -> Set key) -> m ()
modifyDeps key
name Set key -> Set key
f = DefT key uni fun ann Identity () -> m ()
forall a. DefT key uni fun ann Identity a -> m a
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
(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 fun (f :: * -> *).
Functor f =>
(DefMap key (TermDefWithStrictness uni fun ann)
-> f (DefMap key (TermDefWithStrictness uni fun ann)))
-> DefState key uni fun ann -> f (DefState key 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 b c a. (b -> c) -> (a, b) -> (a, c)
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 (f :: * -> *).
Functor f =>
(DefMap key (TypeDef TyName uni ann)
-> f (DefMap key (TypeDef TyName uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun 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 b c a. (b -> c) -> (a, b) -> (a, c)
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 ann))
(DefMap key (DatatypeDef TyName Name uni ann))
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name 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 (DatatypeDef TyName Name uni ann))
(DefMap key (DatatypeDef TyName Name uni ann))
forall key (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(DefMap key (DatatypeDef TyName Name uni ann)
-> f (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
datatypeDefs ((DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann -> DefState key uni fun ann)
-> (DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall a b. (a -> b) -> a -> b
$ ((DatatypeDef TyName Name uni ann, Set key)
-> (DatatypeDef TyName Name uni ann, Set key))
-> key
-> DefMap key (DatatypeDef TyName Name uni ann)
-> DefMap key (DatatypeDef TyName Name uni 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 ann, Set key)
-> (DatatypeDef TyName Name uni ann, Set key)
forall b c a. (b -> c) -> (a, b) -> (a, c)
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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
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
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 (f :: * -> *).
Functor f =>
(Set key -> f (Set key))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
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 :: 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 = 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 a. DefT key uni fun ann Identity a -> m a
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 a. a -> m a
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 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 ann -> term ann
mkVar ann
x (VarDecl TyName Name uni ann -> Term TyName Name uni fun ann)
-> VarDecl TyName Name uni ann -> Term TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann -> VarDecl TyName Name uni 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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
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 a. a -> m a
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 a. a -> m a
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 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 ann -> term ann
mkVar ann
x (VarDecl TyName Name uni ann -> Term TyName Name uni fun ann)
-> VarDecl TyName Name uni ann -> Term TyName Name uni fun ann
forall a b. (a -> b) -> a -> b
$ TermDefWithStrictness uni fun ann -> VarDecl TyName Name uni 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 :: 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 = 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 ann)
_datatypeDefs = DefMap key (DatatypeDef TyName Name uni 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 a. DefT key uni fun ann Identity a -> m a
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 a. a -> m a
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 ann)
-> Maybe (DatatypeDef TyName Name uni ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni ann)
dtys of
Just (DatatypeDef TyName Name 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
$ 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 ann -> TyVarDecl TyName ann
forall var val. Def var val -> var
PLC.defVar DatatypeDef TyName Name uni ann
def
Maybe (DatatypeDef TyName Name uni 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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
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 a. a -> m a
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 a. a -> m a
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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe [Term TyName Name uni fun ann])
lookupConstructors ann
x key
name = do
DefMap key (DatatypeDef TyName Name uni ann)
ds <- DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> m (DefMap key (DatatypeDef TyName Name uni ann))
forall a. DefT key uni fun ann Identity a -> m a
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 ann))
-> m (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> m (DefMap key (DatatypeDef TyName Name uni ann))
forall a b. (a -> b) -> a -> b
$ StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni 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 ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann)))
-> StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
forall a b. (a -> b) -> a -> b
$ Getting
(DefMap key (DatatypeDef TyName Name uni ann))
(DefState key uni fun ann)
(DefMap key (DatatypeDef TyName Name uni ann))
-> StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
(DefMap key (DatatypeDef TyName Name uni ann))
(DefState key uni fun ann)
(DefMap key (DatatypeDef TyName Name uni ann))
forall key (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(DefMap key (DatatypeDef TyName Name uni ann)
-> f (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
datatypeDefs
Maybe [Term TyName Name uni fun ann]
-> m (Maybe [Term TyName Name uni fun ann])
forall a. a -> m a
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 ann)
-> Maybe (DatatypeDef TyName Name uni ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni 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 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 ann -> Term TyName Name uni fun ann)
-> [VarDecl TyName Name uni ann] -> [Term TyName Name uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ann -> VarDecl TyName Name uni 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 ann -> term ann
mkVar ann
x) [VarDecl TyName Name uni ann]
constrs
Maybe (DatatypeDef TyName Name uni 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 :: forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Term TyName Name uni fun ann))
lookupDestructor ann
x key
name = do
DefMap key (DatatypeDef TyName Name uni ann)
ds <- forall key (uni :: * -> *) fun ann (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 ann))
-> m (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> m (DefMap key (DatatypeDef TyName Name uni ann))
forall a b. (a -> b) -> a -> b
$ StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni 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 ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann)))
-> StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
-> DefT
key
uni
fun
ann
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
forall a b. (a -> b) -> a -> b
$ Getting
(DefMap key (DatatypeDef TyName Name uni ann))
(DefState key uni fun ann)
(DefMap key (DatatypeDef TyName Name uni ann))
-> StateT
(DefState key uni fun ann)
Identity
(DefMap key (DatatypeDef TyName Name uni ann))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
(DefMap key (DatatypeDef TyName Name uni ann))
(DefState key uni fun ann)
(DefMap key (DatatypeDef TyName Name uni ann))
forall key (uni :: * -> *) fun ann (f :: * -> *).
Functor f =>
(DefMap key (DatatypeDef TyName Name uni ann)
-> f (DefMap key (DatatypeDef TyName Name uni ann)))
-> DefState key uni fun ann -> f (DefState key uni fun ann)
datatypeDefs
Maybe (Term TyName Name uni fun ann)
-> m (Maybe (Term TyName Name uni fun ann))
forall a. a -> m a
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 ann)
-> Maybe (DatatypeDef TyName Name uni ann, Set key)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup key
name DefMap key (DatatypeDef TyName Name uni 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 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 ann, Set key)
Nothing -> Maybe (Term TyName Name uni fun ann)
forall a. Maybe a
Nothing