{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

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

  -- * Environments
  Env,
  emptyEnv,
  envTypes,
  envReqs,
  envVals,
  envTydefs,
  lookupValue,
  addBinding,
  addValueBinding,
  addTydef,
) where

import Control.Lens hiding (Const)
import Data.Bool (bool)
import Data.Foldable (Foldable (..))
import Data.Function (on)
import Data.Hashable (Hashable, hash)
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 (Ctx)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Key (KeyCombo, prettyKeyCombo)
import Swarm.Language.Requirements.Type (ReqCtx, Requirements)
import Swarm.Language.Syntax
import Swarm.Language.Syntax.Direction
import Swarm.Language.Typed
import Swarm.Language.Types (Polytype, TCtx, TDCtx, TydefInfo, Type, addBindingTD, emptyTDCtx)
import Swarm.Pretty (prettyText)
import Prelude hiding (Foldable (..))

-- | 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
  -- | 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 -> Maybe Polytype -> Maybe Requirements -> 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
  -- | An indirection to a value stored in a memory cell.  The
  --   difference between VRef and VIndir is that VRef is a "real"
  --   value (of Ref type), whereas VIndir is just a placeholder.  If
  --   a VRef is encountered during evaluation, it is the final
  --   result; if VIndir is encountered during evaluation, the value
  --   it points to should be looked up.
  VIndir :: 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
  -- | A 'suspend' command awaiting execution.
  VSuspend :: Term -> Env -> Value
  -- | A special value representing a program that terminated with
  --   an exception.
  VExc :: Value
  -- | A special value used temporarily as the value for a variable
  --   bound by a recursive let, while its definition is being
  --   evaluated.  If the variable is ever referenced again while its
  --   value is still 'VBlackhole', that means it depends on itself in
  --   a way that would trigger an infinite loop, and we can signal an
  --   error.  (Of course, we
  --   <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot detect
  --   /all/ infinite loops this way>.)
  VBlackhole :: Value
  -- | A special value used to represent runtime type information
  --   passed to ad-hoc polymorphic functions.
  VType :: Type -> Value
  deriving (Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
/= :: Value -> Value -> Bool
Eq, (forall x. Value -> Rep Value x)
-> (forall x. Rep Value x -> Value) -> Generic Value
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
$cfrom :: forall x. Value -> Rep Value x
from :: forall x. Value -> Rep Value x
$cto :: forall x. Rep Value x -> Value
to :: forall x. Rep Value x -> Value
Generic, Eq Value
Eq Value =>
(Int -> Value -> Int) -> (Value -> Int) -> Hashable Value
Int -> Value -> Int
Value -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Value -> Int
hashWithSalt :: Int -> Value -> Int
$chash :: Value -> Int
hash :: Value -> Int
Hashable)

-- For the lack of Show and Eq instances, see Note [Env Show and Eq
-- instances]

-- | A value context is a mapping from variable names to their runtime
--   values.
type VCtx = Ctx Var Value

--------------------------------------------------
-- Environments
--------------------------------------------------

-- | An environment is a record that stores relevant information for
--   all the variables currently in scope.
data Env = Env
  { Env -> TCtx
_envTypes :: TCtx
  -- ^ Map variables to their types.
  , Env -> ReqCtx
_envReqs :: ReqCtx
  -- ^ Map variables to the capabilities required to evaluate/execute
  --   them.
  , Env -> Ctx Var Value
_envVals :: VCtx
  -- ^ Map variables to their values.
  , Env -> TDCtx
_envTydefs :: TDCtx
  -- ^ Type synonym definitions.
  }
  deriving (Eq Env
Eq Env => (Int -> Env -> Int) -> (Env -> Int) -> Hashable Env
Int -> Env -> Int
Env -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Env -> Int
hashWithSalt :: Int -> Env -> Int
$chash :: Env -> Int
hash :: Env -> Int
Hashable, (forall x. Env -> Rep Env x)
-> (forall x. Rep Env x -> Env) -> Generic Env
forall x. Rep Env x -> Env
forall x. Env -> Rep Env x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Env -> Rep Env x
from :: forall x. Env -> Rep Env x
$cto :: forall x. Rep Env x -> Env
to :: forall x. Rep Env x -> Env
Generic)

-- A derived `Eq` instance for `Env` can cause exponential blowup (see
-- Note [Env Show and Eq instances]), but we need an `Eq` instance in
-- order to have a `Hashable` instance.  So we just implement equality
-- testing by comparing hashes.
instance Eq Env where
  == :: Env -> Env -> Bool
(==) = Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool) -> (Env -> Int) -> Env -> Env -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Env -> Int
forall a. Hashable a => a -> Int
hash

-- ~~~~ Note [Env Show and Eq instances]
-- Env contains values, which can be e.g. closures, which
-- contain more Envs.  Normally, in memory, there is a lot of sharing,
-- but when naively printing it out all the sharing is lost and it can
-- generate tons of output.  This is why we intentionally do NOT have
-- a Show instance for Env (hence neither for Value).  Similarly, we
-- do not have a derived Eq instance since it would be incredibly
-- inefficient and there is no good reason to use it.  See #2197.

makeLenses ''Env

emptyEnv :: Env
emptyEnv :: Env
emptyEnv = TCtx -> ReqCtx -> Ctx Var Value -> TDCtx -> Env
Env TCtx
forall v t. Ctx v t
Ctx.empty ReqCtx
forall v t. Ctx v t
Ctx.empty Ctx Var Value
forall v t. Ctx v t
Ctx.empty TDCtx
emptyTDCtx

lookupValue :: Var -> Env -> Maybe Value
lookupValue :: Var -> Env -> Maybe Value
lookupValue Var
x Env
e = Var -> Ctx Var Value -> Maybe Value
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup Var
x (Env
e Env -> Getting (Ctx Var Value) Env (Ctx Var Value) -> Ctx Var Value
forall s a. s -> Getting a s a -> a
^. Getting (Ctx Var Value) Env (Ctx Var Value)
Lens' Env (Ctx Var Value)
envVals)

addBinding :: Var -> Typed Value -> Env -> Env
addBinding :: Var -> Typed Value -> Env -> Env
addBinding Var
x Typed Value
v = Index Env -> Lens' Env (Maybe (IxValue Env))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index Env
x ((Maybe (Typed Value) -> Identity (Maybe (Typed Value)))
 -> Env -> Identity Env)
-> Typed Value -> Env -> Env
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Typed Value
v

-- | Add a binding of a variable to a value *only* (no type and
--   requirements).  NOTE that if we then try to look up the variable
--   name using the `At` instance for `Env`, it will report `Nothing`!
--   `lookupValue` will work though.
addValueBinding :: Var -> Value -> Env -> Env
addValueBinding :: Var -> Value -> Env -> Env
addValueBinding Var
x Value
v = (Ctx Var Value -> Identity (Ctx Var Value)) -> Env -> Identity Env
Lens' Env (Ctx Var Value)
envVals ((Ctx Var Value -> Identity (Ctx Var Value))
 -> Env -> Identity Env)
-> (Ctx Var Value -> Ctx Var Value) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> Value -> Ctx Var Value -> Ctx Var Value
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding Var
x Value
v

addTydef :: Text -> TydefInfo -> Env -> Env
addTydef :: Var -> TydefInfo -> Env -> Env
addTydef Var
x TydefInfo
pty = (TDCtx -> Identity TDCtx) -> Env -> Identity Env
Lens' Env TDCtx
envTydefs ((TDCtx -> Identity TDCtx) -> Env -> Identity Env)
-> (TDCtx -> TDCtx) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> TydefInfo -> TDCtx -> TDCtx
addBindingTD Var
x TydefInfo
pty

type instance Index Env = Var
type instance IxValue Env = Typed Value

instance Ixed Env
instance At Env where
  at :: Index Env -> Lens' Env (Maybe (IxValue Env))
at Index Env
name = (Env -> Maybe (Typed Value))
-> (Env -> Maybe (Typed Value) -> Env)
-> Lens Env Env (Maybe (Typed Value)) (Maybe (Typed Value))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Env -> Maybe (Typed Value)
getter Env -> Maybe (Typed Value) -> Env
setter
   where
    getter :: Env -> Maybe (Typed Value)
getter Env
ctx =
      do
        Polytype
typ <- Var -> TCtx -> Maybe Polytype
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup Var
Index Env
name (Env
ctx Env -> Getting TCtx Env TCtx -> TCtx
forall s a. s -> Getting a s a -> a
^. Getting TCtx Env TCtx
Lens' Env TCtx
envTypes)
        Value
val <- Var -> Ctx Var Value -> Maybe Value
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup Var
Index Env
name (Env
ctx Env -> Getting (Ctx Var Value) Env (Ctx Var Value) -> Ctx Var Value
forall s a. s -> Getting a s a -> a
^. Getting (Ctx Var Value) Env (Ctx Var Value)
Lens' Env (Ctx Var Value)
envVals)
        Requirements
req <- Var -> ReqCtx -> Maybe Requirements
forall v t. Ord v => v -> Ctx v t -> Maybe t
Ctx.lookup Var
Index Env
name (Env
ctx Env -> Getting ReqCtx Env ReqCtx -> ReqCtx
forall s a. s -> Getting a s a -> a
^. Getting ReqCtx Env ReqCtx
Lens' Env ReqCtx
envReqs)
        Typed Value -> Maybe (Typed Value)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Typed Value -> Maybe (Typed Value))
-> Typed Value -> Maybe (Typed Value)
forall a b. (a -> b) -> a -> b
$ Value -> Polytype -> Requirements -> Typed Value
forall v. v -> Polytype -> Requirements -> Typed v
Typed Value
val Polytype
typ Requirements
req
    setter :: Env -> Maybe (Typed Value) -> Env
setter Env
ctx Maybe (Typed Value)
Nothing =
      Env
ctx
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (TCtx -> Identity TCtx) -> Env -> Identity Env
Lens' Env TCtx
envTypes
          ((TCtx -> Identity TCtx) -> Env -> Identity Env)
-> (TCtx -> TCtx) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> TCtx -> TCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Var
Index Env
name
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (Ctx Var Value -> Identity (Ctx Var Value)) -> Env -> Identity Env
Lens' Env (Ctx Var Value)
envVals
          ((Ctx Var Value -> Identity (Ctx Var Value))
 -> Env -> Identity Env)
-> (Ctx Var Value -> Ctx Var Value) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> Ctx Var Value -> Ctx Var Value
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Var
Index Env
name
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (ReqCtx -> Identity ReqCtx) -> Env -> Identity Env
Lens' Env ReqCtx
envReqs
          ((ReqCtx -> Identity ReqCtx) -> Env -> Identity Env)
-> (ReqCtx -> ReqCtx) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> Ctx v t -> Ctx v t
Ctx.delete Var
Index Env
name
    setter Env
ctx (Just (Typed Value
val Polytype
typ Requirements
req)) =
      Env
ctx
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (TCtx -> Identity TCtx) -> Env -> Identity Env
Lens' Env TCtx
envTypes
          ((TCtx -> Identity TCtx) -> Env -> Identity Env)
-> (TCtx -> TCtx) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> Polytype -> TCtx -> TCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding Var
Index Env
name Polytype
typ
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (Ctx Var Value -> Identity (Ctx Var Value)) -> Env -> Identity Env
Lens' Env (Ctx Var Value)
envVals
          ((Ctx Var Value -> Identity (Ctx Var Value))
 -> Env -> Identity Env)
-> (Ctx Var Value -> Ctx Var Value) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> Value -> Ctx Var Value -> Ctx Var Value
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding Var
Index Env
name Value
val
        Env -> (Env -> Env) -> Env
forall a b. a -> (a -> b) -> b
& (ReqCtx -> Identity ReqCtx) -> Env -> Identity Env
Lens' Env ReqCtx
envReqs
          ((ReqCtx -> Identity ReqCtx) -> Env -> Identity Env)
-> (ReqCtx -> ReqCtx) -> Env -> Env
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Var -> Requirements -> ReqCtx -> ReqCtx
forall v t.
(Ord v, Hashable v, Hashable t) =>
v -> t -> Ctx v t -> Ctx v t
Ctx.addBinding Var
Index Env
name Requirements
req

------------------------------------------------------------
-- Pretty-printing for values
------------------------------------------------------------

-- | Pretty-print a value.
prettyValue :: Value -> Text
prettyValue :: Value -> Var
prettyValue = Term -> Var
forall a. PrettyPrec a => a -> Var
prettyText (Term -> Var) -> (Value -> Term) -> Value -> Var
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 = \case
  Value
VUnit -> Term
forall ty. Term' ty
TUnit
  VInt Integer
n -> Integer -> Term
forall ty. Integer -> Term' ty
TInt Integer
n
  VText Var
s -> Var -> Term
forall ty. Var -> Term' ty
TText Var
s
  VDir Direction
d -> Direction -> Term
forall ty. Direction -> Term' ty
TDir Direction
d
  VBool Bool
b -> Bool -> Term
forall ty. Bool -> Term' ty
TBool Bool
b
  VRobot Int
r -> Int -> Term
forall ty. Int -> Term' ty
TRobot Int
r
  VInj Bool
s Value
v -> Term -> Term -> Term
TApp (Const -> Term
forall ty. Const -> Term' ty
TConst (Const -> Const -> Bool -> Const
forall a. a -> a -> Bool -> a
bool Const
Inl Const
Inr Bool
s)) (Value -> Term
valueToTerm Value
v)
  VPair Value
v1 Value
v2 -> Term -> Term -> Term
TPair (Value -> Term
valueToTerm Value
v1) (Value -> Term
valueToTerm Value
v2)
  VClo Var
x Term
t Env
e ->
    (Var -> Value -> Term -> Term) -> Term -> Map Var Value -> Term
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey
      ( \Var
y Value
v -> case Value
v of
          VIndir {} -> Term -> Term
forall a. a -> a
id
          Value
_ -> LetSyntax
-> Bool
-> Var
-> Maybe RawPolytype
-> Maybe Polytype
-> Maybe Requirements
-> Term
-> Term
-> Term
TLet LetSyntax
LSLet Bool
False Var
y Maybe RawPolytype
forall a. Maybe a
Nothing Maybe Polytype
forall a. Maybe a
Nothing Maybe Requirements
forall a. Maybe a
Nothing (Value -> Term
valueToTerm Value
v)
      )
      (Var -> Maybe Type -> Term -> Term
TLam Var
x Maybe Type
forall a. Maybe a
Nothing Term
t)
      (Map Var Value -> Set Var -> Map Var Value
forall k a. Ord k => Map k a -> Set k -> Map k a
M.restrictKeys (Ctx Var Value -> Map Var Value
forall v t. Ctx v t -> Map v t
Ctx.unCtx (Env
e Env -> Getting (Ctx Var Value) Env (Ctx Var Value) -> Ctx Var Value
forall s a. s -> Getting a s a -> a
^. Getting (Ctx Var Value) Env (Ctx Var Value)
Lens' Env (Ctx Var Value)
envVals)) (Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
S.delete Var
x (Getting (Set Var) (Syntax' ()) Var -> Syntax' () -> Set Var
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set Var) (Syntax' ()) Var
forall ty (f :: * -> *).
Applicative f =>
(Var -> f Var) -> Syntax' ty -> f (Syntax' ty)
freeVarsV (SrcLoc -> Term -> Comments -> () -> Syntax' ()
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
NoLoc Term
t Comments
forall s. AsEmpty s => s
Empty ()))))
  VCApp Const
c [Value]
vs -> (Term -> Term -> Term) -> Term -> [Term] -> Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Term -> Term -> Term
TApp (Const -> Term
forall ty. Const -> Term' ty
TConst Const
c) ([Term] -> [Term]
forall a. [a] -> [a]
reverse ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
valueToTerm [Value]
vs))
  VBind Maybe Var
mx Maybe Polytype
mty Maybe Requirements
mreq Term
c1 Term
c2 Env
_ -> Maybe Var
-> Maybe Polytype -> Maybe Requirements -> Term -> Term -> Term
TBind Maybe Var
mx Maybe Polytype
mty Maybe Requirements
mreq Term
c1 Term
c2
  VDelay Term
t Env
_ -> Term -> Term
TDelay Term
t
  VRef Int
n -> Int -> Term
forall ty. Int -> Term' ty
TRef Int
n
  VIndir Int
n -> Int -> Term
forall ty. Int -> Term' ty
TRef Int
n
  VRcd Map Var Value
m -> Map Var (Maybe Term) -> Term
TRcd (Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> (Value -> Term) -> Value -> Maybe Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
valueToTerm (Value -> Maybe Term) -> Map Var Value -> Map Var (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var Value
m)
  VKey KeyCombo
kc -> Term -> Term -> Term
TApp (Const -> Term
forall ty. Const -> Term' ty
TConst Const
Key) (Var -> Term
forall ty. Var -> Term' ty
TText (KeyCombo -> Var
prettyKeyCombo KeyCombo
kc))
  VRequirements Var
x Term
t Env
_ -> Var -> Term -> Term
TRequirements Var
x Term
t
  VSuspend Term
t Env
_ -> Term -> Term
TSuspend Term
t
  Value
VExc -> Const -> Term
forall ty. Const -> Term' ty
TConst Const
Undefined
  Value
VBlackhole -> Const -> Term
forall ty. Const -> Term' ty
TConst Const
Undefined
  VType Type
ty -> Type -> Term
forall ty. Type -> Term' ty
TType Type
ty