{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall #-}

-- TODO: Variables for user-defined data types

{-|

Defines a strongly-typed representation of Fortran variables.

-}
module Language.Fortran.Model.Vars
  (
    -- * Variables
    FortranVar(..)
    -- * Names
  , NamePair(..)
  , npSource
  , npUnique
  , SourceName(..)
  , UniqueName(..)
  ) where

import           Data.Typeable                      ((:~:) (..))

import           Control.Lens                       hiding (Index, op)

import           Data.SBV.Dynamic
import           Data.SBV                           (MonadSymbolic(..))

import           Control.Monad.Trans.Class          (lift)

import           Data.Vinyl                         (rtraverse)

import qualified Language.Fortran.AST               as F

import           Language.Expression.Pretty
import           Language.Verification

import           Language.Fortran.Model.Repr
import           Language.Fortran.Model.Repr.Prim
import           Language.Fortran.Model.Types
import           Language.Fortran.Model.Types.Match

--------------------------------------------------------------------------------
--  Names
--------------------------------------------------------------------------------

-- | Newtype wrapper for source-level variable names.
newtype SourceName = SourceName { SourceName -> Name
getSourceName :: F.Name }
  deriving (SourceName -> SourceName -> Bool
(SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool) -> Eq SourceName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SourceName -> SourceName -> Bool
== :: SourceName -> SourceName -> Bool
$c/= :: SourceName -> SourceName -> Bool
/= :: SourceName -> SourceName -> Bool
Eq, Eq SourceName
Eq SourceName
-> (SourceName -> SourceName -> Ordering)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> SourceName)
-> (SourceName -> SourceName -> SourceName)
-> Ord SourceName
SourceName -> SourceName -> Bool
SourceName -> SourceName -> Ordering
SourceName -> SourceName -> SourceName
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 :: SourceName -> SourceName -> Ordering
compare :: SourceName -> SourceName -> Ordering
$c< :: SourceName -> SourceName -> Bool
< :: SourceName -> SourceName -> Bool
$c<= :: SourceName -> SourceName -> Bool
<= :: SourceName -> SourceName -> Bool
$c> :: SourceName -> SourceName -> Bool
> :: SourceName -> SourceName -> Bool
$c>= :: SourceName -> SourceName -> Bool
>= :: SourceName -> SourceName -> Bool
$cmax :: SourceName -> SourceName -> SourceName
max :: SourceName -> SourceName -> SourceName
$cmin :: SourceName -> SourceName -> SourceName
min :: SourceName -> SourceName -> SourceName
Ord)

instance Show SourceName where show :: SourceName -> Name
show = Name -> Name
forall a. Show a => a -> Name
show (Name -> Name) -> (SourceName -> Name) -> SourceName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> Name
getSourceName

-- | Newtype wrapper for unique variable names.
newtype UniqueName = UniqueName { UniqueName -> Name
getUniqueName :: F.Name }
  deriving (UniqueName -> UniqueName -> Bool
(UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool) -> Eq UniqueName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UniqueName -> UniqueName -> Bool
== :: UniqueName -> UniqueName -> Bool
$c/= :: UniqueName -> UniqueName -> Bool
/= :: UniqueName -> UniqueName -> Bool
Eq, Eq UniqueName
Eq UniqueName
-> (UniqueName -> UniqueName -> Ordering)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> UniqueName)
-> (UniqueName -> UniqueName -> UniqueName)
-> Ord UniqueName
UniqueName -> UniqueName -> Bool
UniqueName -> UniqueName -> Ordering
UniqueName -> UniqueName -> UniqueName
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 :: UniqueName -> UniqueName -> Ordering
compare :: UniqueName -> UniqueName -> Ordering
$c< :: UniqueName -> UniqueName -> Bool
< :: UniqueName -> UniqueName -> Bool
$c<= :: UniqueName -> UniqueName -> Bool
<= :: UniqueName -> UniqueName -> Bool
$c> :: UniqueName -> UniqueName -> Bool
> :: UniqueName -> UniqueName -> Bool
$c>= :: UniqueName -> UniqueName -> Bool
>= :: UniqueName -> UniqueName -> Bool
$cmax :: UniqueName -> UniqueName -> UniqueName
max :: UniqueName -> UniqueName -> UniqueName
$cmin :: UniqueName -> UniqueName -> UniqueName
min :: UniqueName -> UniqueName -> UniqueName
Ord)

instance Show UniqueName where show :: UniqueName -> Name
show = Name -> Name
forall a. Show a => a -> Name
show (Name -> Name) -> (UniqueName -> Name) -> UniqueName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueName -> Name
getUniqueName

makeWrapped ''SourceName
makeWrapped ''UniqueName

-- | A 'NamePair' represents the name of some part of a Fortran program,
-- including the human-readable source name and the unique name.
data NamePair =
  NamePair
  { NamePair -> UniqueName
_npUnique :: UniqueName
  , NamePair -> SourceName
_npSource :: SourceName
  }
  deriving (NamePair -> NamePair -> Bool
(NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool) -> Eq NamePair
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NamePair -> NamePair -> Bool
== :: NamePair -> NamePair -> Bool
$c/= :: NamePair -> NamePair -> Bool
/= :: NamePair -> NamePair -> Bool
Eq, Eq NamePair
Eq NamePair
-> (NamePair -> NamePair -> Ordering)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> NamePair)
-> (NamePair -> NamePair -> NamePair)
-> Ord NamePair
NamePair -> NamePair -> Bool
NamePair -> NamePair -> Ordering
NamePair -> NamePair -> NamePair
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 :: NamePair -> NamePair -> Ordering
compare :: NamePair -> NamePair -> Ordering
$c< :: NamePair -> NamePair -> Bool
< :: NamePair -> NamePair -> Bool
$c<= :: NamePair -> NamePair -> Bool
<= :: NamePair -> NamePair -> Bool
$c> :: NamePair -> NamePair -> Bool
> :: NamePair -> NamePair -> Bool
$c>= :: NamePair -> NamePair -> Bool
>= :: NamePair -> NamePair -> Bool
$cmax :: NamePair -> NamePair -> NamePair
max :: NamePair -> NamePair -> NamePair
$cmin :: NamePair -> NamePair -> NamePair
min :: NamePair -> NamePair -> NamePair
Ord, Int -> NamePair -> Name -> Name
[NamePair] -> Name -> Name
NamePair -> Name
(Int -> NamePair -> Name -> Name)
-> (NamePair -> Name)
-> ([NamePair] -> Name -> Name)
-> Show NamePair
forall a.
(Int -> a -> Name -> Name)
-> (a -> Name) -> ([a] -> Name -> Name) -> Show a
$cshowsPrec :: Int -> NamePair -> Name -> Name
showsPrec :: Int -> NamePair -> Name -> Name
$cshow :: NamePair -> Name
show :: NamePair -> Name
$cshowList :: [NamePair] -> Name -> Name
showList :: [NamePair] -> Name -> Name
Show)

makeLenses ''NamePair

instance Pretty SourceName where
  pretty :: SourceName -> Name
pretty = Getting Name SourceName Name -> SourceName -> Name
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Name SourceName Name
(Unwrapped SourceName -> Const Name (Unwrapped SourceName))
-> SourceName -> Const Name SourceName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso' SourceName (Unwrapped SourceName)
_Wrapped

-- | The pretty version of a 'NamePair' is its source name.
instance Pretty NamePair where
  pretty :: NamePair -> Name
pretty = SourceName -> Name
forall a. Pretty a => a -> Name
pretty (SourceName -> Name)
-> (NamePair -> SourceName) -> NamePair -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SourceName NamePair SourceName -> NamePair -> SourceName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SourceName NamePair SourceName
Lens' NamePair SourceName
npSource

--------------------------------------------------------------------------------
--  Fortran Variables
--------------------------------------------------------------------------------

-- | A variable representing a value of type @a@. Contains a @'D' a@ as proof
-- that the type has a corresponding Fortran type, and the variable name.
data FortranVar a where
  FortranVar :: D a -> NamePair -> FortranVar a

instance VerifiableVar FortranVar where
  type VarKey FortranVar = UniqueName
  type VarSym FortranVar = CoreRepr
  type VarEnv FortranVar = PrimReprHandlers

  symForVar :: forall a.
FortranVar a -> VarEnv FortranVar -> Symbolic (VarSym FortranVar a)
symForVar (FortranVar D a
d NamePair
np) VarEnv FortranVar
env =
    case D a
d of
      DPrim Prim p k a1
prim -> D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
forall a1. D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
CRPrim D a
D (PrimS a1)
d (SVal -> CoreRepr (PrimS a1))
-> SymbolicT IO SVal -> SymbolicT IO (CoreRepr (PrimS a1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p k a1 -> Name -> PrimReprHandlers -> SymbolicT IO SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> Name -> m (SymbolicT IO SVal)
primSymbolic Prim p k a1
prim Name
Unwrapped UniqueName
uniqueName VarEnv FortranVar
PrimReprHandlers
env
      DArray Index i
i ArrValue a1
val -> D (Array i a1) -> ArrRepr i a1 -> CoreRepr (Array i a1)
forall {k} (i :: k) a1.
D (Array i a1) -> ArrRepr i a1 -> CoreRepr (Array i a1)
CRArray D a
D (Array i a1)
d (ArrRepr i a1 -> CoreRepr (Array i a1))
-> SymbolicT IO (ArrRepr i a1)
-> SymbolicT IO (CoreRepr (Array i a1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index i
-> ArrValue a1
-> Name
-> PrimReprHandlers
-> SymbolicT IO (ArrRepr i a1)
forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic Index i
i ArrValue a1
val Name
Unwrapped UniqueName
uniqueName VarEnv FortranVar
PrimReprHandlers
env
      DData SSymbol name
_ Rec (Field D) fs
_ -> Name -> SymbolicT IO (CoreRepr (Record name fs))
forall a. Name -> SymbolicT IO a
forall (m :: * -> *) a. MonadFail m => Name -> m a
fail Name
"User-defined data type variables are not supported yet"
    where
      uniqueName :: Unwrapped UniqueName
uniqueName = NamePair
np NamePair
-> Getting (Unwrapped UniqueName) NamePair (Unwrapped UniqueName)
-> Unwrapped UniqueName
forall s a. s -> Getting a s a -> a
^. (UniqueName -> Const (Unwrapped UniqueName) UniqueName)
-> NamePair -> Const (Unwrapped UniqueName) NamePair
Lens' NamePair UniqueName
npUnique ((UniqueName -> Const (Unwrapped UniqueName) UniqueName)
 -> NamePair -> Const (Unwrapped UniqueName) NamePair)
-> ((Unwrapped UniqueName
     -> Const (Unwrapped UniqueName) (Unwrapped UniqueName))
    -> UniqueName -> Const (Unwrapped UniqueName) UniqueName)
-> Getting (Unwrapped UniqueName) NamePair (Unwrapped UniqueName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unwrapped UniqueName
 -> Const (Unwrapped UniqueName) (Unwrapped UniqueName))
-> UniqueName -> Const (Unwrapped UniqueName) UniqueName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso' UniqueName (Unwrapped UniqueName)
_Wrapped

  varKey :: forall a. FortranVar a -> VarKey FortranVar
varKey (FortranVar D a
_ NamePair
np) = NamePair
np NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique

  eqVarTypes :: forall a b. FortranVar a -> FortranVar b -> Maybe (a :~: b)
eqVarTypes (FortranVar D a
d1 NamePair
_) (FortranVar D b
d2 NamePair
_) = D a -> D b -> Maybe (a :~: b)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D b
d2

  castVarSym :: forall a b.
FortranVar a -> VarSym FortranVar b -> Maybe (VarSym FortranVar a)
castVarSym (FortranVar D a
d1 NamePair
_) VarSym FortranVar b
s = case VarSym FortranVar b
s of
    CRPrim D (PrimS a1)
d2 SVal
_  | Just a :~: PrimS a1
Refl <- D a -> D (PrimS a1) -> Maybe (a :~: PrimS a1)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (PrimS a1)
d2 -> CoreRepr (PrimS a1) -> Maybe (CoreRepr (PrimS a1))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (PrimS a1)
s
    CRArray D (Array i a1)
d2 ArrRepr i a1
_ | Just a :~: Array i a1
Refl <- D a -> D (Array i a1) -> Maybe (a :~: Array i a1)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (Array i a1)
d2 -> CoreRepr (Array i a1) -> Maybe (CoreRepr (Array i a1))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (Array i a1)
s
    CRData D (Record name fs)
d2 Rec (Field CoreRepr) fs
_  | Just a :~: Record name fs
Refl <- D a -> D (Record name fs) -> Maybe (a :~: Record name fs)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (Record name fs)
d2 -> CoreRepr (Record name fs) -> Maybe (CoreRepr (Record name fs))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (Record name fs)
s

    -- Variables can't have the 'Bool' type so 'CRProp' can't be casted.
    VarSym FortranVar b
_            -> Maybe (VarSym FortranVar a)
Maybe (CoreRepr a)
forall a. Maybe a
Nothing

instance Pretty1 FortranVar where
  pretty1 :: forall a. FortranVar a -> Name
pretty1 (FortranVar D a
_ NamePair
np) = NamePair -> Name
forall a. Pretty a => a -> Name
pretty NamePair
np

--------------------------------------------------------------------------------
--  Internals
--------------------------------------------------------------------------------

arraySymbolic :: (HasPrimReprHandlers r) => Index i -> ArrValue a -> String -> r -> Symbolic (ArrRepr i a)
arraySymbolic :: forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic ixIndex :: Index i
ixIndex@(Index Prim p 'BTInt a1
ixPrim) ArrValue a
valAV Name
nm r
env =
  case ArrValue a
valAV of
    ArrPrim Prim p k a1
valPrim -> SArr -> ArrRepr i a
SArr -> ArrRepr i (PrimS a1)
forall {k} (i :: k) a1. SArr -> ArrRepr i (PrimS a1)
ARPrim (SArr -> ArrRepr i a)
-> SymbolicT IO SArr -> Symbolic (ArrRepr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p 'BTInt a1 -> Prim p k a1 -> Name -> r -> SymbolicT IO SArr
forall r (p1 :: Precision) (k1 :: BasicType) i (p2 :: Precision)
       (k2 :: BasicType) a.
HasPrimReprHandlers r =>
Prim p1 k1 i -> Prim p2 k2 a -> Name -> r -> SymbolicT IO SArr
arraySymbolicPrim Prim p 'BTInt a1
ixPrim Prim p k a1
valPrim Name
nm r
env
    ArrData SSymbol name
_ Rec (Field ArrValue) fs
valData -> do
      Rec (Field (ArrRepr i)) fs
valReprs <- (forall (x :: (Symbol, *)).
 Field ArrValue x -> SymbolicT IO (Field (ArrRepr i) x))
-> Rec (Field ArrValue) fs
-> SymbolicT IO (Rec (Field (ArrRepr i)) fs)
forall {u} (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse ((forall a. ArrValue a -> SymbolicT IO (ArrRepr (PrimS a1) a))
-> Field ArrValue x -> SymbolicT IO (Field (ArrRepr (PrimS a1)) x)
forall {k} (t :: * -> *) (f :: k -> *) (g :: k -> *)
       (nv :: (Symbol, k)).
Functor t =>
(forall (a :: k). f a -> t (g a)) -> Field f nv -> t (Field g nv)
traverseField' (\ArrValue a
av -> Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic Index i
ixIndex ArrValue a
av Name
nm r
env)) Rec (Field ArrValue) fs
valData
      ArrRepr i a -> Symbolic (ArrRepr i a)
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrRepr i a -> Symbolic (ArrRepr i a))
-> ArrRepr i a -> Symbolic (ArrRepr i a)
forall a b. (a -> b) -> a -> b
$ Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
forall {k} (i :: k) (fs :: [(Symbol, *)]) (name :: Symbol).
Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
ARData Rec (Field (ArrRepr i)) fs
valReprs

arraySymbolicPrim :: (HasPrimReprHandlers r) => Prim p1 k1 i -> Prim p2 k2 a -> String -> r -> Symbolic SArr
arraySymbolicPrim :: forall r (p1 :: Precision) (k1 :: BasicType) i (p2 :: Precision)
       (k2 :: BasicType) a.
HasPrimReprHandlers r =>
Prim p1 k1 i -> Prim p2 k2 a -> Name -> r -> SymbolicT IO SArr
arraySymbolicPrim Prim p1 k1 i
ixPrim Prim p2 k2 a
valPrim Name
nm r
env = do
  Kind
k1 <- IO Kind -> SymbolicT IO Kind
forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Kind -> SymbolicT IO Kind)
-> (Kind -> IO Kind) -> Kind -> SymbolicT IO Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> IO Kind
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> SymbolicT IO Kind) -> Kind -> SymbolicT IO Kind
forall a b. (a -> b) -> a -> b
$ Prim p1 k1 i -> r -> Kind
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> m Kind
primSBVKind Prim p1 k1 i
ixPrim r
env
  Kind
k2 <- IO Kind -> SymbolicT IO Kind
forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Kind -> SymbolicT IO Kind)
-> (Kind -> IO Kind) -> Kind -> SymbolicT IO Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> IO Kind
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> SymbolicT IO Kind) -> Kind -> SymbolicT IO Kind
forall a b. (a -> b) -> a -> b
$ Prim p2 k2 a -> r -> Kind
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> m Kind
primSBVKind Prim p2 k2 a
valPrim r
env
  State
state <- SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
  IO SArr -> SymbolicT IO SArr
forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO SArr -> SymbolicT IO SArr) -> IO SArr -> SymbolicT IO SArr
forall a b. (a -> b) -> a -> b
$ State -> (Kind, Kind) -> (Int -> Name) -> Maybe SVal -> IO SArr
newSArr State
state (Kind
k1, Kind
k2) (\Int
i -> Name
nm Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"_" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Int -> Name
forall a. Show a => a -> Name
show Int
i) Maybe SVal
forall a. Maybe a
Nothing