-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- A requirement is something that is needed in order to successfully
-- build a robot running a certain program.
module Swarm.Language.Requirement (
  -- * Requirements

  -- ** The 'Requirement' type
  Requirement (..),

  -- ** The 'Requirements' type and utility functions
  Requirements (..),
  singleton,
  singletonCap,
  singletonDev,
  singletonInv,
  insert,
  ReqCtx,

  -- * Requirements analysis
  requirements,
) where

import Data.Aeson (FromJSON, ToJSON)
import Data.Bifunctor (first)
import Data.Data (Data)
import Data.Hashable (Hashable)
import Data.Map (Map)
import Data.Map qualified as M
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import Data.Set qualified as S
import Data.Text (Text)
import GHC.Generics (Generic)
import Swarm.Language.Capability (Capability (..), constCaps)
import Swarm.Language.Context (Ctx)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Syntax

-- | A /requirement/ is something a robot must have when it is
--   built. There are three types:
--   - A robot can require a certain 'Capability', which should be fulfilled
--     by equipping an appropriate device.
--   - A robot can require a specific /device/, which should be equipped.
--   - A robot can require some number of a specific entity in its inventory.
data Requirement
  = -- | Require a specific capability.  This must be fulfilled by
    --   equipping an appropriate device.  Requiring the same
    --   capability multiple times is the same as requiring it once.
    ReqCap Capability
  | -- | Require a specific device to be equipped.  Note that at this
    --   point it is only a name, and has not been resolved to an actual
    --   'Swarm.Game.Entity.Entity'.  That's because programs have to be type- and
    --   capability-checked independent of an 'Swarm.Game.Entity.EntityMap'.  The name
    --   will be looked up at runtime, when actually executing a 'Swarm.Language.Syntax.Build'
    --   or 'Swarm.Language.Syntax.Reprogram' command, and an appropriate exception thrown if
    --   a device with the given name does not exist.
    --
    --   Requiring the same device multiple times is the same as
    --   requiring it once.
    ReqDev Text
  | -- | Require a certain number of a specific entity to be available
    --   in the inventory.  The same comments apply re: resolving the
    --   entity name to an actual 'Swarm.Game.Entity.Entity'.
    --
    --   Inventory requirements are additive, that is, say, requiring 5
    --   of entity @"e"@ and later requiring 7 is the same as requiring
    --   12.
    ReqInv Int Text
  deriving (Requirement -> Requirement -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Requirement -> Requirement -> Bool
$c/= :: Requirement -> Requirement -> Bool
== :: Requirement -> Requirement -> Bool
$c== :: Requirement -> Requirement -> Bool
Eq, Eq Requirement
Requirement -> Requirement -> Bool
Requirement -> Requirement -> Ordering
Requirement -> Requirement -> Requirement
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Requirement -> Requirement -> Requirement
$cmin :: Requirement -> Requirement -> Requirement
max :: Requirement -> Requirement -> Requirement
$cmax :: Requirement -> Requirement -> Requirement
>= :: Requirement -> Requirement -> Bool
$c>= :: Requirement -> Requirement -> Bool
> :: Requirement -> Requirement -> Bool
$c> :: Requirement -> Requirement -> Bool
<= :: Requirement -> Requirement -> Bool
$c<= :: Requirement -> Requirement -> Bool
< :: Requirement -> Requirement -> Bool
$c< :: Requirement -> Requirement -> Bool
compare :: Requirement -> Requirement -> Ordering
$ccompare :: Requirement -> Requirement -> Ordering
Ord, Int -> Requirement -> ShowS
[Requirement] -> ShowS
Requirement -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Requirement] -> ShowS
$cshowList :: [Requirement] -> ShowS
show :: Requirement -> String
$cshow :: Requirement -> String
showsPrec :: Int -> Requirement -> ShowS
$cshowsPrec :: Int -> Requirement -> ShowS
Show, ReadPrec [Requirement]
ReadPrec Requirement
Int -> ReadS Requirement
ReadS [Requirement]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Requirement]
$creadListPrec :: ReadPrec [Requirement]
readPrec :: ReadPrec Requirement
$creadPrec :: ReadPrec Requirement
readList :: ReadS [Requirement]
$creadList :: ReadS [Requirement]
readsPrec :: Int -> ReadS Requirement
$creadsPrec :: Int -> ReadS Requirement
Read, forall x. Rep Requirement x -> Requirement
forall x. Requirement -> Rep Requirement x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Requirement x -> Requirement
$cfrom :: forall x. Requirement -> Rep Requirement x
Generic, Eq Requirement
Int -> Requirement -> Int
Requirement -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Requirement -> Int
$chash :: Requirement -> Int
hashWithSalt :: Int -> Requirement -> Int
$chashWithSalt :: Int -> Requirement -> Int
Hashable, Typeable Requirement
Requirement -> DataType
Requirement -> Constr
(forall b. Data b => b -> b) -> Requirement -> Requirement
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Requirement -> u
forall u. (forall d. Data d => d -> u) -> Requirement -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirement
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirement -> c Requirement
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirement)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirement)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirement -> m Requirement
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Requirement -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Requirement -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Requirement -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Requirement -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirement -> r
gmapT :: (forall b. Data b => b -> b) -> Requirement -> Requirement
$cgmapT :: (forall b. Data b => b -> b) -> Requirement -> Requirement
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirement)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirement)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirement)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirement)
dataTypeOf :: Requirement -> DataType
$cdataTypeOf :: Requirement -> DataType
toConstr :: Requirement -> Constr
$ctoConstr :: Requirement -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirement
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirement
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirement -> c Requirement
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirement -> c Requirement
Data, Value -> Parser [Requirement]
Value -> Parser Requirement
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Requirement]
$cparseJSONList :: Value -> Parser [Requirement]
parseJSON :: Value -> Parser Requirement
$cparseJSON :: Value -> Parser Requirement
FromJSON, [Requirement] -> Encoding
[Requirement] -> Value
Requirement -> Encoding
Requirement -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Requirement] -> Encoding
$ctoEncodingList :: [Requirement] -> Encoding
toJSONList :: [Requirement] -> Value
$ctoJSONList :: [Requirement] -> Value
toEncoding :: Requirement -> Encoding
$ctoEncoding :: Requirement -> Encoding
toJSON :: Requirement -> Value
$ctoJSON :: Requirement -> Value
ToJSON)

-- | It is tempting to define @Requirements = Set Requirement@, but
--   that would be wrong, since two identical 'ReqInv' should have
--   their counts added rather than simply being deduplicated.
--
--   Since we will eventually need to deal with the different types of
--   requirements separately, it makes sense to store them separately
--   anyway.
data Requirements = Requirements
  { Requirements -> Set Capability
capReqs :: Set Capability
  , Requirements -> Set Text
devReqs :: Set Text
  , Requirements -> Map Text Int
invReqs :: Map Text Int
  }
  deriving (Requirements -> Requirements -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Requirements -> Requirements -> Bool
$c/= :: Requirements -> Requirements -> Bool
== :: Requirements -> Requirements -> Bool
$c== :: Requirements -> Requirements -> Bool
Eq, Eq Requirements
Requirements -> Requirements -> Bool
Requirements -> Requirements -> Ordering
Requirements -> Requirements -> Requirements
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Requirements -> Requirements -> Requirements
$cmin :: Requirements -> Requirements -> Requirements
max :: Requirements -> Requirements -> Requirements
$cmax :: Requirements -> Requirements -> Requirements
>= :: Requirements -> Requirements -> Bool
$c>= :: Requirements -> Requirements -> Bool
> :: Requirements -> Requirements -> Bool
$c> :: Requirements -> Requirements -> Bool
<= :: Requirements -> Requirements -> Bool
$c<= :: Requirements -> Requirements -> Bool
< :: Requirements -> Requirements -> Bool
$c< :: Requirements -> Requirements -> Bool
compare :: Requirements -> Requirements -> Ordering
$ccompare :: Requirements -> Requirements -> Ordering
Ord, Int -> Requirements -> ShowS
[Requirements] -> ShowS
Requirements -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Requirements] -> ShowS
$cshowList :: [Requirements] -> ShowS
show :: Requirements -> String
$cshow :: Requirements -> String
showsPrec :: Int -> Requirements -> ShowS
$cshowsPrec :: Int -> Requirements -> ShowS
Show, Typeable Requirements
Requirements -> DataType
Requirements -> Constr
(forall b. Data b => b -> b) -> Requirements -> Requirements
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Requirements -> u
forall u. (forall d. Data d => d -> u) -> Requirements -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirements
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirements -> c Requirements
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirements)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirements)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Requirements -> m Requirements
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Requirements -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Requirements -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Requirements -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Requirements -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Requirements -> r
gmapT :: (forall b. Data b => b -> b) -> Requirements -> Requirements
$cgmapT :: (forall b. Data b => b -> b) -> Requirements -> Requirements
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirements)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Requirements)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirements)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Requirements)
dataTypeOf :: Requirements -> DataType
$cdataTypeOf :: Requirements -> DataType
toConstr :: Requirements -> Constr
$ctoConstr :: Requirements -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirements
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Requirements
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirements -> c Requirements
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Requirements -> c Requirements
Data, forall x. Rep Requirements x -> Requirements
forall x. Requirements -> Rep Requirements x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Requirements x -> Requirements
$cfrom :: forall x. Requirements -> Rep Requirements x
Generic, Value -> Parser [Requirements]
Value -> Parser Requirements
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Requirements]
$cparseJSONList :: Value -> Parser [Requirements]
parseJSON :: Value -> Parser Requirements
$cparseJSON :: Value -> Parser Requirements
FromJSON, [Requirements] -> Encoding
[Requirements] -> Value
Requirements -> Encoding
Requirements -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Requirements] -> Encoding
$ctoEncodingList :: [Requirements] -> Encoding
toJSONList :: [Requirements] -> Value
$ctoJSONList :: [Requirements] -> Value
toEncoding :: Requirements -> Encoding
$ctoEncoding :: Requirements -> Encoding
toJSON :: Requirements -> Value
$ctoJSON :: Requirements -> Value
ToJSON)

instance Semigroup Requirements where
  Requirements Set Capability
c1 Set Text
d1 Map Text Int
i1 <> :: Requirements -> Requirements -> Requirements
<> Requirements Set Capability
c2 Set Text
d2 Map Text Int
i2 =
    Set Capability -> Set Text -> Map Text Int -> Requirements
Requirements (Set Capability
c1 forall a. Semigroup a => a -> a -> a
<> Set Capability
c2) (Set Text
d1 forall a. Semigroup a => a -> a -> a
<> Set Text
d2) (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Num a => a -> a -> a
(+) Map Text Int
i1 Map Text Int
i2)

instance Monoid Requirements where
  mempty :: Requirements
mempty = Set Capability -> Set Text -> Map Text Int -> Requirements
Requirements forall a. Set a
S.empty forall a. Set a
S.empty forall k a. Map k a
M.empty

-- | Create a 'Requirements' set with a single 'Requirement'.
singleton :: Requirement -> Requirements
singleton :: Requirement -> Requirements
singleton (ReqCap Capability
c) = Set Capability -> Set Text -> Map Text Int -> Requirements
Requirements (forall a. a -> Set a
S.singleton Capability
c) forall a. Set a
S.empty forall k a. Map k a
M.empty
singleton (ReqDev Text
d) = Set Capability -> Set Text -> Map Text Int -> Requirements
Requirements forall a. Set a
S.empty (forall a. a -> Set a
S.singleton Text
d) forall k a. Map k a
M.empty
singleton (ReqInv Int
n Text
e) = Set Capability -> Set Text -> Map Text Int -> Requirements
Requirements forall a. Set a
S.empty forall a. Set a
S.empty (forall k a. k -> a -> Map k a
M.singleton Text
e Int
n)

-- | For convenience, create a 'Requirements' set with a single
--   'Capability' requirement.
singletonCap :: Capability -> Requirements
singletonCap :: Capability -> Requirements
singletonCap = Requirement -> Requirements
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. Capability -> Requirement
ReqCap

-- | For convenience, create a 'Requirements' set with a single
--   device requirement.
singletonDev :: Text -> Requirements
singletonDev :: Text -> Requirements
singletonDev = Requirement -> Requirements
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Requirement
ReqDev

-- | For convenience, create a 'Requirements' set with a single
--   inventory requirement.
singletonInv :: Int -> Text -> Requirements
singletonInv :: Int -> Text -> Requirements
singletonInv Int
n Text
e = Requirement -> Requirements
singleton (Int -> Text -> Requirement
ReqInv Int
n Text
e)

insert :: Requirement -> Requirements -> Requirements
insert :: Requirement -> Requirements -> Requirements
insert = forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Requirement -> Requirements
singleton

-- | A requirement context records the requirements for the
--   definitions bound to variables.
type ReqCtx = Ctx Requirements

-- | Analyze a program to see what capabilities may be needed to
--   execute it. Also return a capability context mapping from any
--   variables declared via 'TDef' to the capabilities needed by
--   their definitions.
--
--   Note that this is necessarily a conservative analysis, especially
--   if the program contains conditional expressions.  Some
--   capabilities may end up not being actually needed if certain
--   commands end up not being executed.  However, the analysis should
--   be safe in the sense that a robot with the indicated capabilities
--   will always be able to run the given program.
requirements :: ReqCtx -> Term -> (Requirements, ReqCtx)
requirements :: ReqCtx -> Term -> (Requirements, ReqCtx)
requirements ReqCtx
ctx Term
tm = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CPower)) forall a b. (a -> b) -> a -> b
$ case Term
tm of
  -- First, at the top level, we have to keep track of the
  -- requirements for variables bound with the 'TDef' command.

  -- To make a definition requires the env capability.  Note that the
  -- act of MAKING the definition does not require the capabilities of
  -- the body of the definition (including the possibility of the
  -- recursion capability, if the definition is recursive).  However,
  -- we also return a map which associates the defined name to the
  -- capabilities it requires.
  TDef Bool
r Text
x Maybe Polytype
_ Term
t ->
    let bodyReqs :: Requirements
bodyReqs = (if Bool
r then Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CRecursion) else forall a. a -> a
id) (ReqCtx -> Term -> Requirements
requirements' ReqCtx
ctx Term
t)
     in (Capability -> Requirements
singletonCap Capability
CEnv, forall t. Text -> t -> Ctx t
Ctx.singleton Text
x Requirements
bodyReqs)
  TBind Maybe Text
_ Term
t1 Term
t2 ->
    -- First, see what the requirements are to execute the
    -- first command.  It may also define some names, so we get a
    -- map of those names to their required capabilities.
    let (Requirements
reqs1, ReqCtx
ctx1) = ReqCtx -> Term -> (Requirements, ReqCtx)
requirements ReqCtx
ctx Term
t1

        -- Now see what capabilities are required for the second
        -- command; use an extended context since it may refer to
        -- things defined in the first command.
        ctx' :: ReqCtx
ctx' = ReqCtx
ctx forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` ReqCtx
ctx1
        (Requirements
reqs2, ReqCtx
ctx2) = ReqCtx -> Term -> (Requirements, ReqCtx)
requirements ReqCtx
ctx' Term
t2
     in -- Finally return the union of everything.
        (Requirements
reqs1 forall a. Semigroup a => a -> a -> a
<> Requirements
reqs2, ReqCtx
ctx' forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` ReqCtx
ctx2)
  -- Any other term can't bind variables with 'TDef', so we no longer
  -- need to worry about tracking a returned context.
  Term
_ -> (ReqCtx -> Term -> Requirements
requirements' ReqCtx
ctx Term
tm, forall t. Ctx t
Ctx.empty)

-- | Infer the requirements to execute/evaluate a term in a
--   given context, where the term is guaranteed not to contain any
--   'TDef'.
--
--   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.
requirements' :: ReqCtx -> Term -> Requirements
requirements' :: ReqCtx -> Term -> Requirements
requirements' = ReqCtx -> Term -> Requirements
go
 where
  go :: ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
tm = case Term
tm of
    -- Some primitive literals that don't require any special
    -- capability.
    Term
TUnit -> forall a. Monoid a => a
mempty
    TDir Direction
d -> if Direction -> Bool
isCardinal Direction
d then Capability -> Requirements
singletonCap Capability
COrient else forall a. Monoid a => a
mempty
    TInt Integer
_ -> forall a. Monoid a => a
mempty
    TAntiInt Text
_ -> forall a. Monoid a => a
mempty
    TText Text
_ -> forall a. Monoid a => a
mempty
    TAntiText Text
_ -> forall a. Monoid a => a
mempty
    TBool Bool
_ -> forall a. Monoid a => a
mempty
    -- It doesn't require any special capability to *inquire* about
    -- the requirements of a term.
    TRequirements Text
_ Term
_ -> forall a. Monoid a => a
mempty
    -- Look up the capabilities required by a function/command
    -- constants using 'constCaps'.
    TConst Const
c -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty Capability -> Requirements
singletonCap (Const -> Maybe Capability
constCaps Const
c)
    -- Simply record device or inventory requirements.
    TRequireDevice Text
d -> Text -> Requirements
singletonDev Text
d
    TRequire Int
n Text
e -> Int -> Text -> Requirements
singletonInv Int
n Text
e
    -- Note that a variable might not show up in the context, and
    -- that's OK.  In particular, only variables bound by 'TDef' go
    -- in the context; variables bound by a lambda or let will not
    -- be there.
    TVar Text
x -> forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty (forall t. Text -> Ctx t -> Maybe t
Ctx.lookup Text
x ReqCtx
ctx)
    -- 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
_ Term
t -> Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CLambda) forall a b. (a -> b) -> a -> b
$ ReqCtx -> Term -> Requirements
go (forall t. Text -> Ctx t -> Ctx t
Ctx.delete Text
x ReqCtx
ctx) 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 -> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t1 forall a. Semigroup a => a -> a -> a
<> ReqCtx -> Term -> Requirements
go ReqCtx
ctx 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 Bool
r Text
x Maybe Polytype
_ Term
t1 Term
t2 ->
      (if Bool
r then Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CRecursion) else forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$
        Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CEnv) forall a b. (a -> b) -> a -> b
$
          ReqCtx -> Term -> Requirements
go (forall t. Text -> Ctx t -> Ctx t
Ctx.delete Text
x ReqCtx
ctx) Term
t1 forall a. Semigroup a => a -> a -> a
<> ReqCtx -> Term -> Requirements
go (forall t. Text -> Ctx t -> Ctx t
Ctx.delete Text
x ReqCtx
ctx) Term
t2
    -- We also delete the name in a TBind, if any, while recursing on
    -- the RHS.
    TBind Maybe Text
mx Term
t1 Term
t2 -> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t1 forall a. Semigroup a => a -> a -> a
<> ReqCtx -> Term -> Requirements
go (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall t. Text -> Ctx t -> Ctx t
Ctx.delete Maybe Text
mx ReqCtx
ctx) Term
t2
    -- Everything else is straightforward.
    TPair Term
t1 Term
t2 -> Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CProd) forall a b. (a -> b) -> a -> b
$ ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t1 forall a. Semigroup a => a -> a -> a
<> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t2
    TDelay DelayType
_ Term
t -> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t
    -- This case should never happen if the term has been
    -- typechecked; Def commands are only allowed at the top level,
    -- so simply returning mempty is safe.
    TDef {} -> forall a. Monoid a => a
mempty
    TRcd Map Text (Maybe Term)
m -> Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CRecord) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (ReqCtx -> Term -> Requirements
go ReqCtx
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {ty}. (Text, Maybe (Term' ty)) -> Term' ty
expandEq) (forall k a. Map k a -> [(k, a)]
M.assocs Map Text (Maybe Term)
m)
     where
      expandEq :: (Text, Maybe (Term' ty)) -> Term' ty
expandEq (Text
x, Maybe (Term' ty)
Nothing) = forall ty. Text -> Term' ty
TVar Text
x
      expandEq (Text
_, Just Term' ty
t) = Term' ty
t
    TProj Term
t Text
_ -> Requirement -> Requirements -> Requirements
insert (Capability -> Requirement
ReqCap Capability
CRecord) forall a b. (a -> b) -> a -> b
$ ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t
    -- A type ascription doesn't change requirements
    TAnnotate Term
t Polytype
_ -> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t