{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Type definition variables.
module Swarm.Language.TDVar where

import Data.Aeson (FromJSON (..), FromJSONKey, ToJSON (..), ToJSONKey)
import Data.Data (Data)
import Data.Hashable
import Data.String (IsString (..))
import Data.Text (Text)
import GHC.Generics (Generic)
import Prettyprinter (Doc, pretty)
import Swarm.Pretty (PrettyPrec (..))
import Swarm.Util (showT)

-- | The name of a user-defined type is represented by a textual name
--   as well as a version number which we can use to differentiate
--   between names which are otherwise the same, when one shadows the
--   other.
--
--   See Note [Shadowing for value-level and type-level variables]
data TDVar = TDVar {TDVar -> Text
tdVarName :: Text, TDVar -> Int
tdVarVersion :: Int}
  deriving (TDVar -> TDVar -> Bool
(TDVar -> TDVar -> Bool) -> (TDVar -> TDVar -> Bool) -> Eq TDVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TDVar -> TDVar -> Bool
== :: TDVar -> TDVar -> Bool
$c/= :: TDVar -> TDVar -> Bool
/= :: TDVar -> TDVar -> Bool
Eq, Eq TDVar
Eq TDVar =>
(TDVar -> TDVar -> Ordering)
-> (TDVar -> TDVar -> Bool)
-> (TDVar -> TDVar -> Bool)
-> (TDVar -> TDVar -> Bool)
-> (TDVar -> TDVar -> Bool)
-> (TDVar -> TDVar -> TDVar)
-> (TDVar -> TDVar -> TDVar)
-> Ord TDVar
TDVar -> TDVar -> Bool
TDVar -> TDVar -> Ordering
TDVar -> TDVar -> TDVar
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
$ccompare :: TDVar -> TDVar -> Ordering
compare :: TDVar -> TDVar -> Ordering
$c< :: TDVar -> TDVar -> Bool
< :: TDVar -> TDVar -> Bool
$c<= :: TDVar -> TDVar -> Bool
<= :: TDVar -> TDVar -> Bool
$c> :: TDVar -> TDVar -> Bool
> :: TDVar -> TDVar -> Bool
$c>= :: TDVar -> TDVar -> Bool
>= :: TDVar -> TDVar -> Bool
$cmax :: TDVar -> TDVar -> TDVar
max :: TDVar -> TDVar -> TDVar
$cmin :: TDVar -> TDVar -> TDVar
min :: TDVar -> TDVar -> TDVar
Ord, Int -> TDVar -> ShowS
[TDVar] -> ShowS
TDVar -> String
(Int -> TDVar -> ShowS)
-> (TDVar -> String) -> ([TDVar] -> ShowS) -> Show TDVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TDVar -> ShowS
showsPrec :: Int -> TDVar -> ShowS
$cshow :: TDVar -> String
show :: TDVar -> String
$cshowList :: [TDVar] -> ShowS
showList :: [TDVar] -> ShowS
Show, Typeable TDVar
Typeable TDVar =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TDVar -> c TDVar)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TDVar)
-> (TDVar -> Constr)
-> (TDVar -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TDVar))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TDVar))
-> ((forall b. Data b => b -> b) -> TDVar -> TDVar)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r)
-> (forall u. (forall d. Data d => d -> u) -> TDVar -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TDVar -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TDVar -> m TDVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TDVar -> m TDVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TDVar -> m TDVar)
-> Data TDVar
TDVar -> Constr
TDVar -> DataType
(forall b. Data b => b -> b) -> TDVar -> TDVar
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) -> TDVar -> u
forall u. (forall d. Data d => d -> u) -> TDVar -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TDVar
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TDVar -> c TDVar
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TDVar)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TDVar)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TDVar -> c TDVar
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TDVar -> c TDVar
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TDVar
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TDVar
$ctoConstr :: TDVar -> Constr
toConstr :: TDVar -> Constr
$cdataTypeOf :: TDVar -> DataType
dataTypeOf :: TDVar -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TDVar)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TDVar)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TDVar)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TDVar)
$cgmapT :: (forall b. Data b => b -> b) -> TDVar -> TDVar
gmapT :: (forall b. Data b => b -> b) -> TDVar -> TDVar
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TDVar -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TDVar -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TDVar -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TDVar -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TDVar -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TDVar -> m TDVar
Data, (forall x. TDVar -> Rep TDVar x)
-> (forall x. Rep TDVar x -> TDVar) -> Generic TDVar
forall x. Rep TDVar x -> TDVar
forall x. TDVar -> Rep TDVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TDVar -> Rep TDVar x
from :: forall x. TDVar -> Rep TDVar x
$cto :: forall x. Rep TDVar x -> TDVar
to :: forall x. Rep TDVar x -> TDVar
Generic, Eq TDVar
Eq TDVar =>
(Int -> TDVar -> Int) -> (TDVar -> Int) -> Hashable TDVar
Int -> TDVar -> Int
TDVar -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> TDVar -> Int
hashWithSalt :: Int -> TDVar -> Int
$chash :: TDVar -> Int
hash :: TDVar -> Int
Hashable, [TDVar] -> Value
[TDVar] -> Encoding
TDVar -> Bool
TDVar -> Value
TDVar -> Encoding
(TDVar -> Value)
-> (TDVar -> Encoding)
-> ([TDVar] -> Value)
-> ([TDVar] -> Encoding)
-> (TDVar -> Bool)
-> ToJSON TDVar
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: TDVar -> Value
toJSON :: TDVar -> Value
$ctoEncoding :: TDVar -> Encoding
toEncoding :: TDVar -> Encoding
$ctoJSONList :: [TDVar] -> Value
toJSONList :: [TDVar] -> Value
$ctoEncodingList :: [TDVar] -> Encoding
toEncodingList :: [TDVar] -> Encoding
$comitField :: TDVar -> Bool
omitField :: TDVar -> Bool
ToJSON, Maybe TDVar
Value -> Parser [TDVar]
Value -> Parser TDVar
(Value -> Parser TDVar)
-> (Value -> Parser [TDVar]) -> Maybe TDVar -> FromJSON TDVar
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser TDVar
parseJSON :: Value -> Parser TDVar
$cparseJSONList :: Value -> Parser [TDVar]
parseJSONList :: Value -> Parser [TDVar]
$comittedField :: Maybe TDVar
omittedField :: Maybe TDVar
FromJSON, ToJSONKeyFunction [TDVar]
ToJSONKeyFunction TDVar
ToJSONKeyFunction TDVar
-> ToJSONKeyFunction [TDVar] -> ToJSONKey TDVar
forall a.
ToJSONKeyFunction a -> ToJSONKeyFunction [a] -> ToJSONKey a
$ctoJSONKey :: ToJSONKeyFunction TDVar
toJSONKey :: ToJSONKeyFunction TDVar
$ctoJSONKeyList :: ToJSONKeyFunction [TDVar]
toJSONKeyList :: ToJSONKeyFunction [TDVar]
ToJSONKey, FromJSONKeyFunction [TDVar]
FromJSONKeyFunction TDVar
FromJSONKeyFunction TDVar
-> FromJSONKeyFunction [TDVar] -> FromJSONKey TDVar
forall a.
FromJSONKeyFunction a -> FromJSONKeyFunction [a] -> FromJSONKey a
$cfromJSONKey :: FromJSONKeyFunction TDVar
fromJSONKey :: FromJSONKeyFunction TDVar
$cfromJSONKeyList :: FromJSONKeyFunction [TDVar]
fromJSONKeyList :: FromJSONKeyFunction [TDVar]
FromJSONKey)

-- ~~~~ Note [Shadowing for value-level and type-level variables]
--
-- The problem we are solving here is: what happens when y is defined
-- in terms of x, but then later x is redefined/shadowed?  We want to
-- make sure that y still refers to the *old*, shadowed version of x,
-- not the new one.  This problem with user-defined type names caused
-- a type soundness bug, https://github.com/swarm-game/swarm/issues/2437 .
--
-- So how do the version numbers help solve this... and why wasn't it
-- already a problem with value-level names (i.e. things defined via
-- `def`)?
--
-- The language is strict at the value level.  Any use of a variable
-- will be immediately evaluated.  The resulting value will either not
-- mention variables any more, OR will be some kind of closure that
-- contains an environment mapping in-scope variables to their values.
-- So if y is defined in terms of x, it will be evaluated and either
-- not refer to x any more (e.g. `def y = x + 2 end`) or contain a
-- closure with the current value of x.  So if x is later shadowed it
-- makes no difference to the value of y.
--
-- On the other hand, user-defined types are evaluated lazily.  This
-- is a feature: otherwise it would be very annoying to use them for
-- purposes of abbreviating long types (see the discussion at
-- https://github.com/swarm-game/swarm/pull/2438).
--
-- One way this could be solved is by making each type a closure that
-- stores a TDCtx along with it.  However, that would be pretty
-- annoying and require large and tedious changes to the codebase.
-- The other solution is to use version numbers: when a user type is
-- defined, it is given a version number which is one greater than the
-- latest version of the same name already in the TDCtx.  Other
-- definitions referring to older versions will continue to refer to
-- them, and the definitions of the older versions will be
-- retained. When a user type name is used, it is parsed initially as
-- version 0, but in a later name resolution phase (see
-- 'Swarm.Language.Kindcheck.resolveTydefs') the version is updated to
-- the latest in-scope version.

-- | Create a type definition variable with the given name and a
--   default version of 0.
mkTDVar :: Text -> TDVar
mkTDVar :: Text -> TDVar
mkTDVar = Int -> Text -> TDVar
mkTDVar' Int
0

-- | Create a type definition variable with a given version number and
--   name.
mkTDVar' :: Int -> Text -> TDVar
mkTDVar' :: Int -> Text -> TDVar
mkTDVar' Int
v Text
x = Text -> Int -> TDVar
TDVar Text
x Int
v

-- | Pretty-print a type definition variable, given an extra argument
--   representing the latest version of any variable with this name.
--   If this variable is the latest version, just print its name.  If
--   it is not the latest version, print @name%version@.
prettyTDVar :: Int -> TDVar -> Doc ann
prettyTDVar :: forall ann. Int -> TDVar -> Doc ann
prettyTDVar Int
latest (TDVar Text
x Int
n)
  | Int
latest Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"%" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showT Int
n)
  | Bool
otherwise = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
x

-- TODO(#2452): overhaul pretty-printing to take extra
-- environment/parameters, such as TDCtx to know when to print a user
-- type name with its version number, to disambiguate when it has been
-- shadowed.

-- | The 'PrettyPrec' instance for 'TDVar' never prints the version
--   number.  If you care about the version number possibly being
--   printed, you must use 'prettyTDVar' instead.
instance PrettyPrec TDVar where
  prettyPrec :: forall ann. Int -> TDVar -> Doc ann
prettyPrec Int
_ (TDVar Text
x Int
_) = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
x

instance IsString TDVar where
  fromString :: String -> TDVar
fromString = Text -> TDVar
mkTDVar (Text -> TDVar) -> (String -> Text) -> String -> TDVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString