{-# 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   #-}

-- 9.6 notices that a constraint generated by the deriving machinery is redundant:
-- https://gitlab.haskell.org/ghc/ghc/-/issues/23143
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
-- | Support for generating PIR with global definitions with dependencies between them.
module PlutusIR.Compiler.Definitions (
  DefT,
  MonadDefs (..),
  TermDefWithStrictness,
  runDefT,
  defineTerm,
  modifyTermDef,
  defineType,
  modifyTypeDef,
  defineDatatype,
  modifyDatatypeDef,
  modifyDeps,
  recordAlias,
  lookupTerm,
  lookupOrDefineTerm,
  lookupType,
  lookupOrDefineType,
  lookupConstructors,
  lookupDestructor,
) where

import PlutusIR 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

{- Note [Annotations on Bindings]

When constructing Bindings (including TermBind, TypeBind and DatatypeBind) from definitions
in `runDefT`, we use the annotation on the VarDecl and TyVarDecl as the annotation of the
Binding itself. The reason is that the simplifier looks at the annotation of a Binding as
one of the factors to determine whether to inline the Binding. When we define a term that
should be inlined, we put the corresponding annotation in the VarDecl or TyVarDecl (note
that there's no need to annotate the term itself), and that annotation needs to be copied
to the Binding when creating the Binding.
-}

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

mapDefs :: (a -> b) -> DefMap key a -> DefMap key b
mapDefs :: 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
    )

-- Need to write this by hand, deriving wants to derive the one for DefState
instance (MonadState s m) => MonadState s (DefT key uni fun ann m) where
  get :: DefT key uni fun ann m s
get = m s -> DefT key uni fun ann m s
forall (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
        -- See Note [Annotations on Bindings]
        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

{- | Given the definitions in the program, create a topologically ordered list of the
SCCs using the dependency information
-}
defSccs :: (Ord key) => DefMap key def -> [NAM.AdjacencyMap key]
defSccs :: 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
    -- the graph made by 'scc' is guaranteed to be acyclic
    case AdjacencyMap (AdjacencyMap key)
-> Either (Cycle (AdjacencyMap key)) [AdjacencyMap key]
forall a. Ord a => AdjacencyMap a -> Either (Cycle a) [a]
AM.topSort AdjacencyMap (AdjacencyMap key)
keySccs of
      Right [AdjacencyMap key]
sorted -> [AdjacencyMap key]
sorted
      -- TODO: report cycle
      Left Cycle (AdjacencyMap key)
_       -> [Char] -> [AdjacencyMap key]
forall a. HasCallStack => [Char] -> a
error [Char]
"No topological sort of SCC graph"

wrapWithDefs ::
  (Ord key) =>
  ann ->
  DefMap key (Binding tyname name uni fun ann) ->
  Term tyname name uni fun ann ->
  Term tyname name uni fun ann
wrapWithDefs :: 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 -- process from the inside out
      (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

-- | Modifies the dependency set of a key.
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
  -- This is a little crude: we expect most keys will appear in only one map, so we just modify the
  -- dependencies in all of them! That lets us just have one function.
  (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DefState key uni fun ann -> DefState key uni fun ann)
 -> StateT (DefState key uni fun ann) Identity ())
-> (DefState key uni fun ann -> DefState key uni fun ann)
-> StateT (DefState key uni fun ann) Identity ()
forall a b. (a -> b) -> a -> b
$ ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
-> (DefMap key (TermDefWithStrictness uni fun ann)
    -> DefMap key (TermDefWithStrictness uni fun ann))
-> DefState key uni fun ann
-> DefState key uni fun ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (DefState key uni fun ann)
  (DefState key uni fun ann)
  (DefMap key (TermDefWithStrictness uni fun ann))
  (DefMap key (TermDefWithStrictness uni fun ann))
forall key (uni :: * -> *) fun ann 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