-- |
-- 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.Carrier.Throw.Either (runThrow)
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.TDVar (tdVarName)
import Swarm.Language.Types
import Swarm.Util (applyWhen)

-- | 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 Var
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TText Var
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TAntiText Var
_ -> () -> 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 ()
    TType {} -> () -> 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 Var
_ 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.
    TRequire Var
d -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Var -> Requirements
singletonDev Var
d)
    TStock Int
n Var
e -> Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Int -> Var -> Requirements
singletonInv Int
n Var
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 Var
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_ (Var -> ReqCtx -> Maybe Requirements
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup Var
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 Var
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 (Var -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Var
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
    -- Special case for 'use' with a device literal.
    TApp t1 :: Term
t1@(TConst Const
Use) t2 :: Term
t2@(TText Var
device) ->
      Requirements -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Accum w) sig m =>
w -> m ()
add (Var -> Requirements
singletonDev Var
device) 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
    -- In general, 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 Var
x Maybe RawPolytype
mty Maybe Polytype
_ 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)
      (RawPolytype -> m ()) -> Maybe RawPolytype -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ RawPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *)
       (q :: ImplicitQuantification).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Poly q Type -> m ()
polytypeRequirements Maybe RawPolytype
mty
      forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local @ReqCtx (Var -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Var
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 Var
x Maybe RawPolytype
mty Maybe Polytype
_ 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)
      (RawPolytype -> m ()) -> Maybe RawPolytype -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ RawPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *)
       (q :: ImplicitQuantification).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Poly q Type -> m ()
polytypeRequirements Maybe RawPolytype
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 =
            Bool
-> (Requirements -> Requirements) -> Requirements -> Requirements
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
r (Capability -> Requirements
singletonCap Capability
CRecursion Requirements -> Requirements -> Requirements
forall a. Semigroup a => a -> a -> a
<>) (Requirements -> Requirements) -> Requirements -> Requirements
forall a b. (a -> b) -> a -> b
$
              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 (Var -> Requirements -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding Var
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 TDVar
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 :: * -> *)
       (q :: ImplicitQuantification).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Poly q Type -> 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 (Var -> TydefInfo -> TDCtx -> TDCtx
addBindingTD (TDVar -> Var
tdVarName TDVar
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
. [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Var] -> Int) -> (Polytype -> [Var]) -> Polytype -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polytype -> [Var]
forall t. Poly 'Quantified t -> [Var]
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 Var
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)
-> (Var -> ReqCtx -> ReqCtx) -> Maybe Var -> ReqCtx -> ReqCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReqCtx -> ReqCtx
forall a. a -> a
id Var -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Maybe Var
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 Var (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
*> [(Var, Maybe Term)] -> ((Var, Maybe Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Var (Maybe Term) -> [(Var, Maybe Term)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Var (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 ())
-> ((Var, Maybe Term) -> Term) -> (Var, Maybe Term) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Maybe Term) -> Term
forall {ty}. (Var, Maybe (Term' ty)) -> Term' ty
expandEq)
     where
      expandEq :: (Var, Maybe (Term' ty)) -> Term' ty
expandEq (Var
x, Maybe (Term' ty)
Nothing) = Var -> Term' ty
forall ty. Var -> Term' ty
TVar Var
x
      expandEq (Var
_, Just Term' ty
t) = Term' ty
t
    TProj Term
t Var
_ -> 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 RawPolytype
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
*> RawPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *)
       (q :: ImplicitQuantification).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Poly q Type -> m ()
polytypeRequirements RawPolytype
ty
    TParens 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

polytypeRequirements ::
  (Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
  Poly q Type ->
  m ()
polytypeRequirements :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *)
       (q :: ImplicitQuantification).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Poly q Type -> m ()
polytypeRequirements = Type -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
Type -> m ()
typeRequirements (Type -> m ()) -> (Poly q Type -> Type) -> Poly q Type -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly q Type -> Type
forall (q :: ImplicitQuantification) t. Poly q t -> t
ptBody

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 Var
_ Var
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    TyConF (TCUser TDVar
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
      Either ExpandTydefErr Type
res <- forall e (m :: * -> *) a. ThrowC e m a -> m (Either e a)
runThrow @ExpandTydefErr (TDVar -> [Type] -> ThrowC ExpandTydefErr m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [Type]
tys)
      case Either ExpandTydefErr Type
res of
        -- If the user tycon is undefined, just return 0 requirements.
        -- This is not really correct---it should be some kind of
        -- error---but in theory it should be impossible for a user
        -- tycon to be undefined, and adding error propagation here
        -- would be annoying.  The undefined tycon can be caught
        -- somewhere else.
        Left ExpandTydefErr
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Right Type
ty' -> 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 Var Type
m -> (Type -> m ()) -> Map Var Type -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> m ()
go Map Var Type
m
    TyRecF Var
_ 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 ()