-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Analyze a term to discover the requirements for
-- evaluating/executing it.
--
-- Note, eventually, requirements will be part of types and
-- requirements analysis will just be part of typechecking
-- (https://github.com/swarm-game/swarm/issues/231).
module Swarm.Language.Requirements.Analysis (
  requirements,
) where

import Control.Algebra (Has, run)
import Control.Carrier.Accum.Strict (execAccum)
import Control.Carrier.Reader (runReader)
import Control.Effect.Accum (Accum, add)
import Control.Effect.Reader (Reader, ask, local)
import Control.Monad (when)
import Data.Fix (Fix (..))
import Data.Foldable (forM_)
import Data.Map qualified as M
import Swarm.Language.Capability (Capability (..), constCaps)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Requirements.Type
import Swarm.Language.Syntax
import Swarm.Language.Syntax.Direction (isCardinal)
import Swarm.Language.Types

-- | Infer the requirements to execute/evaluate a term in a given
--   context.
--
--   For function application and let-expressions, we assume that the
--   argument (respectively let-bound expression) is used at least
--   once in the body.  Doing otherwise would require a much more
--   fine-grained analysis where we differentiate between the
--   capabilities needed to *evaluate* versus *execute* any expression
--   (since e.g. an unused let-binding would still incur the
--   capabilities to *evaluate* it), which does not seem worth it at
--   all.
--
--   This is all a bit of a hack at the moment, to be honest; see #231
--   for a description of a more correct approach.
requirements :: TDCtx -> ReqCtx -> Term -> Requirements
requirements :: TDCtx -> ReqCtx -> Term -> Requirements
requirements TDCtx
tdCtx ReqCtx
ctx =
  Identity Requirements -> Requirements
forall a. Identity a -> a
run (Identity Requirements -> Requirements)
-> (Term -> Identity Requirements) -> Term -> Requirements
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Requirements
-> AccumC Requirements Identity () -> Identity Requirements
forall (m :: * -> *) w a. Functor m => w -> AccumC w m a -> m w
execAccum Requirements
forall a. Monoid a => a
mempty (AccumC Requirements Identity () -> Identity Requirements)
-> (Term -> AccumC Requirements Identity ())
-> Term
-> Identity Requirements
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TDCtx
-> ReaderC TDCtx (AccumC Requirements Identity) ()
-> AccumC Requirements Identity ()
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader TDCtx
tdCtx (ReaderC TDCtx (AccumC Requirements Identity) ()
 -> AccumC Requirements Identity ())
-> (Term -> ReaderC TDCtx (AccumC Requirements Identity) ())
-> Term
-> AccumC Requirements Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReqCtx
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
-> ReaderC TDCtx (AccumC Requirements Identity) ()
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader ReqCtx
ctx (ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
 -> ReaderC TDCtx (AccumC Requirements Identity) ())
-> (Term
    -> ReaderC
         ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ())
-> Term
-> ReaderC TDCtx (AccumC Requirements Identity) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Requirements
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CPower) ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
forall a b.
ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) a
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) b
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>) (ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
 -> ReaderC
      ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ())
-> (Term
    -> ReaderC
         ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ())
-> Term
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term
-> ReaderC ReqCtx (ReaderC TDCtx (AccumC Requirements Identity)) ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go
 where
  go ::
    ( Has (Accum Requirements) sig m
    , Has (Reader ReqCtx) sig m
    , Has (Reader TDCtx) sig m
    ) =>
    Term ->
    m ()
  go :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go = \case
    -- Some primitive literals that don't require any special
    -- capability.
    Term
TUnit -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TDir Direction
d -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Direction -> Bool
isCardinal Direction
d) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
COrient)
    TInt Integer
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TAntiInt Text
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TText Text
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TAntiText Text
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TBool Bool
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TSuspend {} -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- It doesn't require any special capability to *inquire* about
    -- the requirements of a term.
    TRequirements Text
_ Term
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- Look up the capabilities required by a function/command
    -- constants using 'constCaps'.
    TConst Const
c -> Maybe Capability -> (Capability -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Const -> Maybe Capability
constCaps Const
c) (Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Requirements -> m ())
-> (Capability -> Requirements) -> Capability -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Capability -> Requirements
singletonCap)
    -- Simply record device or inventory requirements.
    TRequireDevice Text
d -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Text -> Requirements
singletonDev Text
d)
    TRequire Int
n Text
e -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Int -> Text -> Requirements
singletonInv Int
n Text
e)
    -- Note that a variable might not show up in the context, and
    -- that's OK; if not, it just means using the variable requires
    -- no special capabilities.
    TVar Text
x -> do
      ReqCtx
reqs <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @ReqCtx
      Maybe Requirements -> (Requirements -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Text -> ReqCtx -> Maybe Requirements
forall t. Text -> Ctx t -> Maybe t
Ctx.lookup Text
x ReqCtx
reqs) Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add
    -- A lambda expression requires the 'CLambda' capability, and
    -- also all the capabilities of the body.  We assume that the
    -- lambda will eventually get applied, at which point it will
    -- indeed require the body's capabilities (this is unnecessarily
    -- conservative if the lambda is never applied, but such a
    -- program could easily be rewritten without the unused
    -- lambda). We also don't do anything with the argument: we
    -- assume that it is used at least once within the body, and the
    -- capabilities required by any argument will be picked up at
    -- the application site.  Again, this is overly conservative in
    -- the case that the argument is unused, but in that case the
    -- unused argument could be removed.
    --
    -- Note, however, that we do need to *delete* the argument from
    -- the context, in case the context already contains a definition
    -- with the same name: inside the lambda that definition will be
    -- shadowed, so we do not want the name to be associated to any
    -- capabilities.
    TLam Text
x Maybe Type
mty Term
t -> do
      Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CLambda)
      (Type -> m ()) -> Maybe Type -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Type -> m ()
typeRequirements Maybe Type
mty
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @ReqCtx (Text -> ReqCtx -> ReqCtx
forall t. Text -> Ctx t -> Ctx t
Ctx.delete Text
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t
    -- An application simply requires the union of the capabilities
    -- from the left- and right-hand sides.  This assumes that the
    -- argument will be used at least once by the function.
    TApp Term
t1 Term
t2 -> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2
    -- Similarly, for a let, we assume that the let-bound expression
    -- will be used at least once in the body. We delete the let-bound
    -- name from the context when recursing for the same reason as
    -- lambda.
    TLet LetSyntax
LSLet Bool
r Text
x Maybe Polytype
mty Maybe Requirements
_ Term
t1 Term
t2 -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
r (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CRecursion)
      Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CEnv)
      (Polytype -> m ()) -> Maybe Polytype -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Polytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Polytype -> m ()
polytypeRequirements Maybe Polytype
mty
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @ReqCtx (Text -> ReqCtx -> ReqCtx
forall t. Text -> Ctx t -> Ctx t
Ctx.delete Text
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2
    -- However, for def, we do NOT assume that the defined expression
    -- will be used at least once in the body; it may not be executed
    -- until later on, when the base robot has more capabilities.
    TLet LetSyntax
LSDef Bool
r Text
x Maybe Polytype
mty Maybe Requirements
_ Term
t1 Term
t2 -> do
      Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CEnv)
      (Polytype -> m ()) -> Maybe Polytype -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Polytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Polytype -> m ()
polytypeRequirements Maybe Polytype
mty
      ReqCtx
localReqCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @ReqCtx
      TDCtx
localTDCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TDCtx
      let bodyReqs :: Requirements
bodyReqs =
            (if Bool
r then (Capability -> Requirements
singletonCap Capability
CRecursion Requirements -> Requirements -> Requirements
forall a. Semigroup a => a -> a -> a
<>) else Requirements -> Requirements
forall a. a -> a
id)
              (TDCtx -> ReqCtx -> Term -> Requirements
requirements TDCtx
localTDCtx ReqCtx
localReqCtx Term
t1)
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @ReqCtx (Text -> Requirements -> ReqCtx -> ReqCtx
forall t. Text -> t -> Ctx t -> Ctx t
Ctx.addBinding Text
x Requirements
bodyReqs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2
    -- Using tydef requires CEnv, plus whatever the requirements are
    -- for the type itself.
    TTydef Text
x Polytype
ty Maybe TydefInfo
_ Term
t2 -> do
      Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CEnv)
      Polytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Polytype -> m ()
polytypeRequirements Polytype
ty
      -- Now check the nested term with the new type definition added
      -- to the context.
      --
      -- Note, it's not ideal to be creating a TydefInfo from scratch
      -- here; ideally we should get it from the kind checker.
      -- Eventually we will put that into the third field of TTydef,
      -- but it's not there yet at this point.  This is really just a
      -- symptom of the fact that typechecking, kind checking, and
      -- requirements checking really all need to be done at the same
      -- time during a single traversal of the term (see #231).
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @TDCtx (Text -> TydefInfo -> TDCtx -> TDCtx
forall t. Text -> t -> Ctx t -> Ctx t
Ctx.addBinding Text
x (Polytype -> Arity -> TydefInfo
TydefInfo Polytype
ty (Int -> Arity
Arity (Int -> Arity) -> (Polytype -> Int) -> Polytype -> Arity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Text] -> Int) -> (Polytype -> [Text]) -> Polytype -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polytype -> [Text]
forall t. Poly t -> [Text]
ptVars (Polytype -> Arity) -> Polytype -> Arity
forall a b. (a -> b) -> a -> b
$ Polytype
ty))) (Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2)
    -- We also delete the name in a TBind, if any, while recursing on
    -- the RHS.
    TBind Maybe Text
mx Maybe Polytype
_ Maybe Requirements
_ Term
t1 Term
t2 -> do
      Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t1
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @ReqCtx ((ReqCtx -> ReqCtx)
-> (Text -> ReqCtx -> ReqCtx) -> Maybe Text -> ReqCtx -> ReqCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReqCtx -> ReqCtx
forall a. a -> a
id Text -> ReqCtx -> ReqCtx
forall t. Text -> Ctx t -> Ctx t
Ctx.delete Maybe Text
mx) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2
    -- Everything else is straightforward.
    TPair Term
t1 Term
t2 -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CProd) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t1 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t2
    TDelay Term
t -> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t
    TRcd Map Text (Maybe Term)
m -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CRecord) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [(Text, Maybe Term)] -> ((Text, Maybe Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Text (Maybe Term) -> [(Text, Maybe Term)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Text (Maybe Term)
m) (Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go (Term -> m ())
-> ((Text, Maybe Term) -> Term) -> (Text, Maybe Term) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Maybe Term) -> Term
forall {ty}. (Text, Maybe (Term' ty)) -> Term' ty
expandEq)
     where
      expandEq :: (Text, Maybe (Term' ty)) -> Term' ty
expandEq (Text
x, Maybe (Term' ty)
Nothing) = Text -> Term' ty
forall ty. Text -> Term' ty
TVar Text
x
      expandEq (Text
_, Just Term' ty
t) = Term' ty
t
    TProj Term
t Text
_ -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CRecord) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t
    -- A type ascription doesn't change requirements
    TAnnotate Term
t Polytype
ty -> Term -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader ReqCtx) sig m,
 Has (Reader TDCtx) sig m) =>
Term -> m ()
go Term
t m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Polytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Polytype -> m ()
polytypeRequirements Polytype
ty

polytypeRequirements ::
  (Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
  Polytype ->
  m ()
polytypeRequirements :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Polytype -> m ()
polytypeRequirements (Forall [Text]
_ Type
ty) = Type -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Type -> m ()
typeRequirements Type
ty

typeRequirements ::
  (Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
  Type ->
  m ()
typeRequirements :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Type -> m ()
typeRequirements = Type -> m ()
go
 where
  go :: Type -> m ()
go (Fix TypeF Type
tyF) = TypeF Type -> m ()
goF TypeF Type
tyF

  goF :: TypeF Type -> m ()
goF = \case
    TyVarF Text
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TyConF (TCUser Text
u) [Type]
tys -> do
      (Type -> m ()) -> [Type] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> m ()
go [Type]
tys
      Type
ty' <- Text -> [Type] -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Typical t) =>
Text -> [t] -> m t
expandTydef Text
u [Type]
tys
      Type -> m ()
go Type
ty'
    TyConF TyCon
c [Type]
tys -> do
      case TyCon
c of
        TyCon
TCSum -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CSum)
        TyCon
TCProd -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CProd)
        TyCon
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      (Type -> m ()) -> [Type] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> m ()
go [Type]
tys
    TyRcdF Map Text Type
m -> (Type -> m ()) -> Map Text Type -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> m ()
go Map Text Type
m
    TyRecF Text
_ Type
ty' -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Capability -> Requirements
singletonCap Capability
CRectype) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type -> m ()
go Type
ty'
    TyRecVarF Nat
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()