{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}

-- |
-- Module      :  Swarm.Language.Context
-- Copyright   :  Brent Yorgey
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Generic contexts (mappings from variables to other things, such as
-- types, values, or capability sets) used throughout the codebase.
module Swarm.Language.Context where

import Control.Lens.Empty (AsEmpty (..))
import Control.Lens.Prism (prism)
import Control.Monad.Reader (MonadReader, local)
import Data.Aeson (FromJSON, ToJSON)
import Data.Data (Data)
import Data.Map (Map)
import Data.Map qualified as M
import Data.Text (Text)
import GHC.Generics (Generic)
import Prelude hiding (lookup)

-- | We use 'Text' values to represent variables.
type Var = Text

-- | A context is a mapping from variable names to things.
newtype Ctx t = Ctx {forall t. Ctx t -> Map Var t
unCtx :: Map Var t}
  deriving (Ctx t -> Ctx t -> Bool
forall t. Eq t => Ctx t -> Ctx t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ctx t -> Ctx t -> Bool
$c/= :: forall t. Eq t => Ctx t -> Ctx t -> Bool
== :: Ctx t -> Ctx t -> Bool
$c== :: forall t. Eq t => Ctx t -> Ctx t -> Bool
Eq, Int -> Ctx t -> ShowS
forall t. Show t => Int -> Ctx t -> ShowS
forall t. Show t => [Ctx t] -> ShowS
forall t. Show t => Ctx t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ctx t] -> ShowS
$cshowList :: forall t. Show t => [Ctx t] -> ShowS
show :: Ctx t -> String
$cshow :: forall t. Show t => Ctx t -> String
showsPrec :: Int -> Ctx t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Ctx t -> ShowS
Show, forall a b. a -> Ctx b -> Ctx a
forall a b. (a -> b) -> Ctx a -> Ctx b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Ctx b -> Ctx a
$c<$ :: forall a b. a -> Ctx b -> Ctx a
fmap :: forall a b. (a -> b) -> Ctx a -> Ctx b
$cfmap :: forall a b. (a -> b) -> Ctx a -> Ctx b
Functor, forall a. Eq a => a -> Ctx a -> Bool
forall a. Num a => Ctx a -> a
forall a. Ord a => Ctx a -> a
forall m. Monoid m => Ctx m -> m
forall a. Ctx a -> Bool
forall a. Ctx a -> Int
forall a. Ctx a -> [a]
forall a. (a -> a -> a) -> Ctx a -> a
forall m a. Monoid m => (a -> m) -> Ctx a -> m
forall b a. (b -> a -> b) -> b -> Ctx a -> b
forall a b. (a -> b -> b) -> b -> Ctx a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Ctx a -> a
$cproduct :: forall a. Num a => Ctx a -> a
sum :: forall a. Num a => Ctx a -> a
$csum :: forall a. Num a => Ctx a -> a
minimum :: forall a. Ord a => Ctx a -> a
$cminimum :: forall a. Ord a => Ctx a -> a
maximum :: forall a. Ord a => Ctx a -> a
$cmaximum :: forall a. Ord a => Ctx a -> a
elem :: forall a. Eq a => a -> Ctx a -> Bool
$celem :: forall a. Eq a => a -> Ctx a -> Bool
length :: forall a. Ctx a -> Int
$clength :: forall a. Ctx a -> Int
null :: forall a. Ctx a -> Bool
$cnull :: forall a. Ctx a -> Bool
toList :: forall a. Ctx a -> [a]
$ctoList :: forall a. Ctx a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Ctx a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ctx a -> a
foldr1 :: forall a. (a -> a -> a) -> Ctx a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Ctx a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Ctx a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ctx a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Ctx a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ctx a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Ctx a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ctx a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Ctx a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ctx a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Ctx a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ctx a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Ctx a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ctx a -> m
fold :: forall m. Monoid m => Ctx m -> m
$cfold :: forall m. Monoid m => Ctx m -> m
Foldable, Functor Ctx
Foldable Ctx
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a)
forall (f :: * -> *) a. Applicative f => Ctx (f a) -> f (Ctx a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx a -> f (Ctx b)
sequence :: forall (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a)
$csequence :: forall (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Ctx (f a) -> f (Ctx a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Ctx (f a) -> f (Ctx a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx a -> f (Ctx b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx a -> f (Ctx b)
Traversable, Ctx t -> DataType
Ctx t -> Constr
forall {t}. Data t => Typeable (Ctx t)
forall t. Data t => Ctx t -> DataType
forall t. Data t => Ctx t -> Constr
forall t. Data t => (forall b. Data b => b -> b) -> Ctx t -> Ctx t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ctx t -> u
forall t u. Data t => (forall d. Data d => d -> u) -> Ctx t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ctx t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctx t -> c (Ctx t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ctx t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ctx t))
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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ctx t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctx t -> c (Ctx t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ctx t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ctx t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ctx t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ctx t -> [u]
$cgmapQ :: forall t u. Data t => (forall d. Data d => d -> u) -> Ctx t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
gmapT :: (forall b. Data b => b -> b) -> Ctx t -> Ctx t
$cgmapT :: forall t. Data t => (forall b. Data b => b -> b) -> Ctx t -> Ctx t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ctx t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ctx t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ctx t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ctx t))
dataTypeOf :: Ctx t -> DataType
$cdataTypeOf :: forall t. Data t => Ctx t -> DataType
toConstr :: Ctx t -> Constr
$ctoConstr :: forall t. Data t => Ctx t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ctx t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ctx t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctx t -> c (Ctx t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctx t -> c (Ctx t)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Ctx t) x -> Ctx t
forall t x. Ctx t -> Rep (Ctx t) x
$cto :: forall t x. Rep (Ctx t) x -> Ctx t
$cfrom :: forall t x. Ctx t -> Rep (Ctx t) x
Generic, forall t. FromJSON t => Value -> Parser [Ctx t]
forall t. FromJSON t => Value -> Parser (Ctx t)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Ctx t]
$cparseJSONList :: forall t. FromJSON t => Value -> Parser [Ctx t]
parseJSON :: Value -> Parser (Ctx t)
$cparseJSON :: forall t. FromJSON t => Value -> Parser (Ctx t)
FromJSON, forall t. ToJSON t => [Ctx t] -> Encoding
forall t. ToJSON t => [Ctx t] -> Value
forall t. ToJSON t => Ctx t -> Encoding
forall t. ToJSON t => Ctx t -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Ctx t] -> Encoding
$ctoEncodingList :: forall t. ToJSON t => [Ctx t] -> Encoding
toJSONList :: [Ctx t] -> Value
$ctoJSONList :: forall t. ToJSON t => [Ctx t] -> Value
toEncoding :: Ctx t -> Encoding
$ctoEncoding :: forall t. ToJSON t => Ctx t -> Encoding
toJSON :: Ctx t -> Value
$ctoJSON :: forall t. ToJSON t => Ctx t -> Value
ToJSON)

-- | The semigroup operation for contexts is /right/-biased union.
instance Semigroup (Ctx t) where
  <> :: Ctx t -> Ctx t -> Ctx t
(<>) = forall t. Ctx t -> Ctx t -> Ctx t
union

instance Monoid (Ctx t) where
  mempty :: Ctx t
mempty = forall t. Ctx t
empty
  mappend :: Ctx t -> Ctx t -> Ctx t
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance AsEmpty (Ctx t) where
  _Empty :: Prism' (Ctx t) ()
_Empty = forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism (forall a b. a -> b -> a
const forall t. Ctx t
empty) forall {t}. Ctx t -> Either (Ctx t) ()
isEmpty
   where
    isEmpty :: Ctx t -> Either (Ctx t) ()
isEmpty (Ctx Map Var t
c)
      | forall k a. Map k a -> Bool
M.null Map Var t
c = forall a b. b -> Either a b
Right ()
      | Bool
otherwise = forall a b. a -> Either a b
Left (forall t. Map Var t -> Ctx t
Ctx Map Var t
c)

-- | The empty context.
empty :: Ctx t
empty :: forall t. Ctx t
empty = forall t. Map Var t -> Ctx t
Ctx forall k a. Map k a
M.empty

-- | A singleton context.
singleton :: Var -> t -> Ctx t
singleton :: forall t. Var -> t -> Ctx t
singleton Var
x t
t = forall t. Map Var t -> Ctx t
Ctx (forall k a. k -> a -> Map k a
M.singleton Var
x t
t)

-- | Look up a variable in a context.
lookup :: Var -> Ctx t -> Maybe t
lookup :: forall t. Var -> Ctx t -> Maybe t
lookup Var
x (Ctx Map Var t
c) = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var t
c

-- | Delete a variable from a context.
delete :: Var -> Ctx t -> Ctx t
delete :: forall t. Var -> Ctx t -> Ctx t
delete Var
x (Ctx Map Var t
c) = forall t. Map Var t -> Ctx t
Ctx (forall k a. Ord k => k -> Map k a -> Map k a
M.delete Var
x Map Var t
c)

-- | Get the list of key-value associations from a context.
assocs :: Ctx t -> [(Var, t)]
assocs :: forall t. Ctx t -> [(Var, t)]
assocs = forall k a. Map k a -> [(k, a)]
M.assocs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Ctx t -> Map Var t
unCtx

-- | Add a key-value binding to a context (overwriting the old one if
--   the key is already present).
addBinding :: Var -> t -> Ctx t -> Ctx t
addBinding :: forall t. Var -> t -> Ctx t -> Ctx t
addBinding Var
x t
t (Ctx Map Var t
c) = forall t. Map Var t -> Ctx t
Ctx (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
x t
t Map Var t
c)

-- | /Right/-biased union of contexts.
union :: Ctx t -> Ctx t -> Ctx t
union :: forall t. Ctx t -> Ctx t -> Ctx t
union (Ctx Map Var t
c1) (Ctx Map Var t
c2) = forall t. Map Var t -> Ctx t
Ctx (Map Var t
c2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map Var t
c1)

-- | Locally extend the context with an additional binding.
withBinding :: MonadReader (Ctx t) m => Var -> t -> m a -> m a
withBinding :: forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding Var
x t
ty = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall t. Var -> t -> Ctx t -> Ctx t
addBinding Var
x t
ty)

-- | Locally extend the context with an additional context of
--   bindings.
withBindings :: MonadReader (Ctx t) m => Ctx t -> m a -> m a
withBindings :: forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Ctx t -> m a -> m a
withBindings Ctx t
ctx = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall t. Ctx t -> Ctx t -> Ctx t
`union` Ctx t
ctx)