{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
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
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 newtype (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)
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
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
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)
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 :: 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 (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
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
(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