{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Values and environments used for interpreting the Swarm language.
module Swarm.Language.Value (
  -- * Values
  Value (..),
  stripVResult,
  prettyValue,
  valueToTerm,

  -- * Environments
  Env,
) where

import Data.Aeson (FromJSON, ToJSON)
import Data.Bool (bool)
import Data.List (foldl')
import Data.Map (Map)
import Data.Map qualified as M
import Data.Set qualified as S
import Data.Set.Lens (setOf)
import Data.Text (Text)
import GHC.Generics (Generic)
import Swarm.Language.Context
import Swarm.Language.Key (KeyCombo, prettyKeyCombo)
import Swarm.Language.Pretty (prettyText)
import Swarm.Language.Syntax

-- | A /value/ is a term that cannot (or does not) take any more
--   evaluation steps on its own.
data Value where
  -- | The unit value.
  VUnit :: Value
  -- | An integer.
  VInt :: Integer -> Value
  -- | Literal text.
  VText :: Text -> Value
  -- | A direction.
  VDir :: Direction -> Value
  -- | A boolean.
  VBool :: Bool -> Value
  -- | A reference to a robot.
  VRobot :: Int -> Value
  -- | An injection into a sum type.  False = left, True = right.
  VInj :: Bool -> Value -> Value
  -- | A pair.
  VPair :: Value -> Value -> Value
  -- | A /closure/, representing a lambda term along with an
  --   environment containing bindings for any free variables in the
  --   body of the lambda.
  VClo :: Var -> Term -> Env -> Value
  -- | An application of a constant to some value arguments,
  --   potentially waiting for more arguments.  If a constant
  --   application is fully saturated (as defined by its 'arity'),
  --   whether it is a value or not depends on whether or not it
  --   represents a command (as defined by 'isCmd').  If a command
  --   (e.g. 'Build'), it is a value, and awaits an 'Swarm.Game.CESK.FExec' frame
  --   which will cause it to execute.  Otherwise (e.g. 'If'), it is
  --   not a value, and will immediately reduce.
  VCApp :: Const -> [Value] -> Value
  -- | A definition, which does not take effect until executed.
  --   The @Bool@ indicates whether the definition is recursive.
  VDef :: Bool -> Var -> Term -> Env -> Value
  -- | The result of a command, consisting of the result of the
  --   command as well as an environment of bindings from 'TDef'
  --   commands.
  VResult :: Value -> Env -> Value
  -- | An unevaluated bind expression, waiting to be executed, of the
  --   form /i.e./ @c1 ; c2@ or @x <- c1; c2@.  We also store an 'Env'
  --   in which to interpret the commands.
  VBind :: Maybe Var -> Term -> Term -> Env -> Value
  -- | A (non-recursive) delayed term, along with its environment. If
  --   a term would otherwise be evaluated but we don't want it to be
  --   (/e.g./ as in the case of arguments to an 'if', or a recursive
  --   binding), we can stick a 'TDelay' on it, which turns it into a
  --   value.  Delayed terms won't be evaluated until 'Force' is
  --   applied to them.
  VDelay :: Term -> Env -> Value
  -- | A reference to a memory cell in the store.
  VRef :: Int -> Value
  -- | A record value.
  VRcd :: Map Var Value -> Value
  -- | A keyboard input.
  VKey :: KeyCombo -> Value
  -- | A 'requirements' command awaiting execution.
  VRequirements :: Text -> Term -> Env -> Value
  deriving (Value -> Value -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq, Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show, forall x. Rep Value x -> Value
forall x. Value -> Rep Value x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Value x -> Value
$cfrom :: forall x. Value -> Rep Value x
Generic, Value -> Parser [Value]
Value -> Parser Value
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Value]
$cparseJSONList :: Value -> Parser [Value]
parseJSON :: Value -> Parser Value
$cparseJSON :: Value -> Parser Value
FromJSON, [Value] -> Encoding
[Value] -> Value
Value -> Encoding
Value -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Value] -> Encoding
$ctoEncodingList :: [Value] -> Encoding
toJSONList :: [Value] -> Value
$ctoJSONList :: [Value] -> Value
toEncoding :: Value -> Encoding
$ctoEncoding :: Value -> Encoding
toJSON :: Value -> Value
$ctoJSON :: Value -> Value
ToJSON)

-- | Ensure that a value is not wrapped in 'VResult'.
stripVResult :: Value -> Value
stripVResult :: Value -> Value
stripVResult (VResult Value
v Env
_) = Value -> Value
stripVResult Value
v
stripVResult Value
v = Value
v

-- | Pretty-print a value.
prettyValue :: Value -> Text
prettyValue :: Value -> Text
prettyValue = forall a. PrettyPrec a => a -> Text
prettyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valueToTerm

-- | Inject a value back into a term.
valueToTerm :: Value -> Term
valueToTerm :: Value -> Term
valueToTerm Value
VUnit = forall ty. Term' ty
TUnit
valueToTerm (VInt Integer
n) = forall ty. Integer -> Term' ty
TInt Integer
n
valueToTerm (VText Text
s) = forall ty. Text -> Term' ty
TText Text
s
valueToTerm (VDir Direction
d) = forall ty. Direction -> Term' ty
TDir Direction
d
valueToTerm (VBool Bool
b) = forall ty. Bool -> Term' ty
TBool Bool
b
valueToTerm (VRobot Int
r) = forall ty. Int -> Term' ty
TRobot Int
r
valueToTerm (VInj Bool
s Value
v) = Term -> Term -> Term
TApp (forall ty. Const -> Term' ty
TConst (forall a. a -> a -> Bool -> a
bool Const
Inl Const
Inr Bool
s)) (Value -> Term
valueToTerm Value
v)
valueToTerm (VPair Value
v1 Value
v2) = Term -> Term -> Term
TPair (Value -> Term
valueToTerm Value
v1) (Value -> Term
valueToTerm Value
v2)
valueToTerm (VClo Text
x Term
t Env
e) =
  forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey
    (\Text
y Value
v -> Bool -> Text -> Maybe Polytype -> Term -> Term -> Term
TLet Bool
False Text
y forall a. Maybe a
Nothing (Value -> Term
valueToTerm Value
v))
    (Text -> Maybe Type -> Term -> Term
TLam Text
x forall a. Maybe a
Nothing Term
t)
    (forall k a. Ord k => Map k a -> Set k -> Map k a
M.restrictKeys (forall t. Ctx t -> Map Text t
unCtx Env
e) (forall a. Ord a => a -> Set a -> Set a
S.delete Text
x (forall a s. Getting (Set a) s a -> s -> Set a
setOf forall ty. Traversal' (Syntax' ty) Text
freeVarsV (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
NoLoc Term
t ()))))
valueToTerm (VCApp Const
c [Value]
vs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Term -> Term -> Term
TApp (forall ty. Const -> Term' ty
TConst Const
c) (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
valueToTerm [Value]
vs))
valueToTerm (VDef Bool
r Text
x Term
t Env
_) = Bool -> Text -> Maybe Polytype -> Term -> Term
TDef Bool
r Text
x forall a. Maybe a
Nothing Term
t
valueToTerm (VResult Value
v Env
_) = Value -> Term
valueToTerm Value
v
valueToTerm (VBind Maybe Text
mx Term
c1 Term
c2 Env
_) = Maybe Text -> Term -> Term -> Term
TBind Maybe Text
mx Term
c1 Term
c2
valueToTerm (VDelay Term
t Env
_) = DelayType -> Term -> Term
TDelay DelayType
SimpleDelay Term
t
valueToTerm (VRef Int
n) = forall ty. Int -> Term' ty
TRef Int
n
valueToTerm (VRcd Map Text Value
m) = Map Text (Maybe Term) -> Term
TRcd (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valueToTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text Value
m)
valueToTerm (VKey KeyCombo
kc) = Term -> Term -> Term
TApp (forall ty. Const -> Term' ty
TConst Const
Key) (forall ty. Text -> Term' ty
TText (KeyCombo -> Text
prettyKeyCombo KeyCombo
kc))
valueToTerm (VRequirements Text
x Term
t Env
_) = Text -> Term -> Term
TRequirements Text
x Term
t

-- | An environment is a mapping from variable names to values.
type Env = Ctx Value