{-# LANGUAGE DeriveDataTypeable #-}

-- |
-- 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.Algebra (Has)
import Control.Effect.Reader (Reader, ask, local)
import Control.Lens.Empty (AsEmpty (..))
import Control.Lens.Prism (prism)
import Data.Aeson (FromJSON (..), ToJSON (..), genericParseJSON, genericToJSON)
import Data.Data (Data)
import Data.Map (Map)
import Data.Map qualified as M
import Data.Text (Text)
import GHC.Generics (Generic)
import Swarm.Util.JSON (optionsUnwrapUnary)
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
(Ctx t -> Ctx t -> Bool) -> (Ctx t -> Ctx t -> Bool) -> Eq (Ctx t)
forall t. Eq t => Ctx t -> Ctx t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Ctx t -> Ctx t -> Bool
Eq, Int -> Ctx t -> ShowS
[Ctx t] -> ShowS
Ctx t -> String
(Int -> Ctx t -> ShowS)
-> (Ctx t -> String) -> ([Ctx t] -> ShowS) -> Show (Ctx t)
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
$cshowsPrec :: forall t. Show t => Int -> Ctx t -> ShowS
showsPrec :: Int -> Ctx t -> ShowS
$cshow :: forall t. Show t => Ctx t -> String
show :: Ctx t -> String
$cshowList :: forall t. Show t => [Ctx t] -> ShowS
showList :: [Ctx t] -> ShowS
Show, (forall a b. (a -> b) -> Ctx a -> Ctx b)
-> (forall a b. a -> Ctx b -> Ctx a) -> Functor Ctx
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
$cfmap :: forall a b. (a -> b) -> Ctx a -> Ctx b
fmap :: forall a b. (a -> b) -> Ctx a -> Ctx b
$c<$ :: forall a b. a -> Ctx b -> Ctx a
<$ :: forall a b. a -> Ctx b -> Ctx a
Functor, (forall m. Monoid m => Ctx m -> m)
-> (forall m a. Monoid m => (a -> m) -> Ctx a -> m)
-> (forall m a. Monoid m => (a -> m) -> Ctx a -> m)
-> (forall a b. (a -> b -> b) -> b -> Ctx a -> b)
-> (forall a b. (a -> b -> b) -> b -> Ctx a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ctx a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ctx a -> b)
-> (forall a. (a -> a -> a) -> Ctx a -> a)
-> (forall a. (a -> a -> a) -> Ctx a -> a)
-> (forall a. Ctx a -> [a])
-> (forall a. Ctx a -> Bool)
-> (forall a. Ctx a -> Int)
-> (forall a. Eq a => a -> Ctx a -> Bool)
-> (forall a. Ord a => Ctx a -> a)
-> (forall a. Ord a => Ctx a -> a)
-> (forall a. Num a => Ctx a -> a)
-> (forall a. Num a => Ctx a -> a)
-> Foldable Ctx
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
$cfold :: forall m. Monoid m => Ctx m -> m
fold :: forall m. Monoid m => Ctx m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Ctx a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Ctx a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Ctx a -> a
foldr1 :: forall a. (a -> a -> a) -> Ctx a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ctx a -> a
foldl1 :: forall a. (a -> a -> a) -> Ctx a -> a
$ctoList :: forall a. Ctx a -> [a]
toList :: forall a. Ctx a -> [a]
$cnull :: forall a. Ctx a -> Bool
null :: forall a. Ctx a -> Bool
$clength :: forall a. Ctx a -> Int
length :: forall a. Ctx a -> Int
$celem :: forall a. Eq a => a -> Ctx a -> Bool
elem :: forall a. Eq a => a -> Ctx a -> Bool
$cmaximum :: forall a. Ord a => Ctx a -> a
maximum :: forall a. Ord a => Ctx a -> a
$cminimum :: forall a. Ord a => Ctx a -> a
minimum :: forall a. Ord a => Ctx a -> a
$csum :: forall a. Num a => Ctx a -> a
sum :: forall a. Num a => Ctx a -> a
$cproduct :: forall a. Num a => Ctx a -> a
product :: forall a. Num a => Ctx a -> a
Foldable, Functor Ctx
Foldable Ctx
(Functor Ctx, Foldable Ctx) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Ctx a -> f (Ctx b))
-> (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 (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx a -> f (Ctx b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx a -> f (Ctx b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Ctx (f a) -> f (Ctx a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Ctx (f a) -> f (Ctx a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
$csequence :: forall (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a)
sequence :: forall (m :: * -> *) a. Monad m => Ctx (m a) -> m (Ctx a)
Traversable, Typeable (Ctx t)
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Ctx t))
-> (Ctx t -> Constr)
-> (Ctx t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Ctx t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ctx t)))
-> ((forall b. Data b => b -> b) -> Ctx t -> Ctx t)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ctx t -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ctx t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t))
-> Data (Ctx t)
Ctx t -> Constr
Ctx t -> DataType
(forall b. Data b => b -> b) -> Ctx t -> Ctx t
forall t. Data t => Typeable (Ctx t)
forall t. Data t => Ctx t -> Constr
forall t. Data t => Ctx t -> DataType
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 u. Int -> (forall d. Data d => d -> u) -> Ctx t -> u
forall u. (forall d. Data d => d -> u) -> Ctx t -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctx t -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ctx t)
$ctoConstr :: forall t. Data t => Ctx t -> Constr
toConstr :: Ctx t -> Constr
$cdataTypeOf :: forall t. Data t => Ctx t -> DataType
dataTypeOf :: Ctx t -> DataType
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ctx t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ctx t))
$cgmapT :: forall t. Data t => (forall b. Data b => b -> b) -> Ctx t -> Ctx t
gmapT :: (forall b. Data b => b -> b) -> Ctx t -> Ctx t
$cgmapQl :: 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
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctx t -> r
$cgmapQ :: forall t u. Data t => (forall d. Data d => d -> u) -> Ctx t -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ctx t -> u
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctx t -> m (Ctx t)
Data, (forall x. Ctx t -> Rep (Ctx t) x)
-> (forall x. Rep (Ctx t) x -> Ctx t) -> Generic (Ctx t)
forall x. Rep (Ctx t) x -> Ctx t
forall x. Ctx t -> Rep (Ctx t) x
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
$cfrom :: forall t x. Ctx t -> Rep (Ctx t) x
from :: forall x. Ctx t -> Rep (Ctx t) x
$cto :: forall t x. Rep (Ctx t) x -> Ctx t
to :: forall x. Rep (Ctx t) x -> Ctx t
Generic)

instance ToJSON t => ToJSON (Ctx t) where
  toJSON :: Ctx t -> Value
toJSON = Options -> Ctx t -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsUnwrapUnary

instance FromJSON t => FromJSON (Ctx t) where
  parseJSON :: Value -> Parser (Ctx t)
parseJSON = Options -> Value -> Parser (Ctx t)
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
optionsUnwrapUnary

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

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

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

-- | The empty context.
empty :: Ctx t
empty :: forall t. Ctx t
empty = Map Var t -> Ctx t
forall t. Map Var t -> Ctx t
Ctx Map Var t
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 = Map Var t -> Ctx t
forall t. Map Var t -> Ctx t
Ctx (Var -> t -> Map Var t
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) = Var -> Map Var t -> Maybe t
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var t
c

-- | Look up a variable in a context in an ambient Reader effect.
lookupR :: Has (Reader (Ctx t)) sig m => Var -> m (Maybe t)
lookupR :: forall t (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Ctx t)) sig m =>
Var -> m (Maybe t)
lookupR Var
x = Var -> Ctx t -> Maybe t
forall t. Var -> Ctx t -> Maybe t
lookup Var
x (Ctx t -> Maybe t) -> m (Ctx t) -> m (Maybe t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Ctx t)
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask

-- | 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) = Map Var t -> Ctx t
forall t. Map Var t -> Ctx t
Ctx (Var -> Map Var t -> Map Var t
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 = Map Var t -> [(Var, t)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map Var t -> [(Var, t)])
-> (Ctx t -> Map Var t) -> Ctx t -> [(Var, t)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx t -> Map Var t
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) = Map Var t -> Ctx t
forall t. Map Var t -> Ctx t
Ctx (Var -> t -> Map Var t -> Map Var t
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) = Map Var t -> Ctx t
forall t. Map Var t -> Ctx t
Ctx (Map Var t
c2 Map Var t -> Map Var t -> Map Var t
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 :: Has (Reader (Ctx t)) sig m => Var -> t -> m a -> m a
withBinding :: forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding Var
x t
ty = (Ctx t -> Ctx t) -> m a -> m a
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local (Var -> t -> Ctx t -> Ctx t
forall t. Var -> t -> Ctx t -> Ctx t
addBinding Var
x t
ty)

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