module Swarm.Language.Requirement (
Requirement (..),
Requirements (..),
singleton,
singletonCap,
singletonDev,
singletonInv,
insert,
ReqCtx,
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
data Requirement
=
ReqCap Capability
|
ReqDev Text
|
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)
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
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)
singletonCap :: Capability -> Requirements
singletonCap :: Capability -> Requirements
singletonCap = Requirement -> Requirements
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. Capability -> Requirement
ReqCap
singletonDev :: Text -> Requirements
singletonDev :: Text -> Requirements
singletonDev = Requirement -> Requirements
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Requirement
ReqDev
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
type ReqCtx = Ctx Requirements
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
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 ->
let (Requirements
reqs1, ReqCtx
ctx1) = ReqCtx -> Term -> (Requirements, ReqCtx)
requirements ReqCtx
ctx Term
t1
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
(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)
Term
_ -> (ReqCtx -> Term -> Requirements
requirements' ReqCtx
ctx Term
tm, forall t. Ctx t
Ctx.empty)
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
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
TRequirements Text
_ Term
_ -> forall a. Monoid a => a
mempty
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)
TRequireDevice Text
d -> Text -> Requirements
singletonDev Text
d
TRequire Int
n Text
e -> Int -> Text -> Requirements
singletonInv Int
n Text
e
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)
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
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
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
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
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
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
TAnnotate Term
t Polytype
_ -> ReqCtx -> Term -> Requirements
go ReqCtx
ctx Term
t