{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE DerivingStrategies        #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE MagicHash                 #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE UndecidableInstances      #-}

{- |
Copyright: (c) 2018-2020 Kowainik
SPDX-License-Identifier: MPL-2.0
Maintainer: Kowainik <xrom.xkov@gmail.com>

This module contains 'Memory' data type and various utility functions:

1. Create values of type 'Memory'.
2. Unwrap values of type 'Memory' to integral types.
3. Pretty-displaying functions.
4. Parsing.
5. Numeric functions.
-}

module Membrain.Memory
       ( -- * Data type
         Memory (..)
       , memory
       , toMemory
       , showMemory
       , readMemory

         -- * Conversion functions
       , toBits
       , toRat
       , floor

         -- * Numeric operations
       , memoryMul
       , memoryDiff
       , memoryPlus
       , memoryDiv

         -- * Any memory data type
         -- $any
       , AnyMemory (..)
       ) where

import Prelude hiding (floor)

import Data.Char (isDigit, isSpace)
import Data.Coerce (coerce)
import Data.Foldable (foldl')
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Ratio (Ratio, (%))
import Data.Semigroup (Semigroup (..))
import GHC.Exts (Proxy#, proxy#)
import GHC.Generics (Generic)
import GHC.TypeNats (KnownNat, Nat, natVal')
import Numeric.Natural (Natural)

import Membrain.Units (KnownUnitSymbol, unitSymbol)

import qualified Prelude


{- $setup
>>> import Membrain
-}

{- | Main memory units type. It has phantom type parameter @mem@ of kind 'Nat'
which is type level representation of the unit. Stores internally memory as
bits. To construct values of type 'Memory', use functions from the
"Membrain.Constructors" module.
-}
newtype Memory (mem :: Nat) = Memory
    { Memory mem -> Natural
unMemory :: Natural
    } deriving stock   (Int -> Memory mem -> ShowS
[Memory mem] -> ShowS
Memory mem -> String
(Int -> Memory mem -> ShowS)
-> (Memory mem -> String)
-> ([Memory mem] -> ShowS)
-> Show (Memory mem)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (mem :: Nat). Int -> Memory mem -> ShowS
forall (mem :: Nat). [Memory mem] -> ShowS
forall (mem :: Nat). Memory mem -> String
showList :: [Memory mem] -> ShowS
$cshowList :: forall (mem :: Nat). [Memory mem] -> ShowS
show :: Memory mem -> String
$cshow :: forall (mem :: Nat). Memory mem -> String
showsPrec :: Int -> Memory mem -> ShowS
$cshowsPrec :: forall (mem :: Nat). Int -> Memory mem -> ShowS
Show, ReadPrec [Memory mem]
ReadPrec (Memory mem)
Int -> ReadS (Memory mem)
ReadS [Memory mem]
(Int -> ReadS (Memory mem))
-> ReadS [Memory mem]
-> ReadPrec (Memory mem)
-> ReadPrec [Memory mem]
-> Read (Memory mem)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (mem :: Nat). ReadPrec [Memory mem]
forall (mem :: Nat). ReadPrec (Memory mem)
forall (mem :: Nat). Int -> ReadS (Memory mem)
forall (mem :: Nat). ReadS [Memory mem]
readListPrec :: ReadPrec [Memory mem]
$creadListPrec :: forall (mem :: Nat). ReadPrec [Memory mem]
readPrec :: ReadPrec (Memory mem)
$creadPrec :: forall (mem :: Nat). ReadPrec (Memory mem)
readList :: ReadS [Memory mem]
$creadList :: forall (mem :: Nat). ReadS [Memory mem]
readsPrec :: Int -> ReadS (Memory mem)
$creadsPrec :: forall (mem :: Nat). Int -> ReadS (Memory mem)
Read, (forall x. Memory mem -> Rep (Memory mem) x)
-> (forall x. Rep (Memory mem) x -> Memory mem)
-> Generic (Memory mem)
forall x. Rep (Memory mem) x -> Memory mem
forall x. Memory mem -> Rep (Memory mem) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (mem :: Nat) x. Rep (Memory mem) x -> Memory mem
forall (mem :: Nat) x. Memory mem -> Rep (Memory mem) x
$cto :: forall (mem :: Nat) x. Rep (Memory mem) x -> Memory mem
$cfrom :: forall (mem :: Nat) x. Memory mem -> Rep (Memory mem) x
Generic)
      deriving newtype (Memory mem -> Memory mem -> Bool
(Memory mem -> Memory mem -> Bool)
-> (Memory mem -> Memory mem -> Bool) -> Eq (Memory mem)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (mem :: Nat). Memory mem -> Memory mem -> Bool
/= :: Memory mem -> Memory mem -> Bool
$c/= :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
== :: Memory mem -> Memory mem -> Bool
$c== :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
Eq, Eq (Memory mem)
Eq (Memory mem) =>
(Memory mem -> Memory mem -> Ordering)
-> (Memory mem -> Memory mem -> Bool)
-> (Memory mem -> Memory mem -> Bool)
-> (Memory mem -> Memory mem -> Bool)
-> (Memory mem -> Memory mem -> Bool)
-> (Memory mem -> Memory mem -> Memory mem)
-> (Memory mem -> Memory mem -> Memory mem)
-> Ord (Memory mem)
Memory mem -> Memory mem -> Bool
Memory mem -> Memory mem -> Ordering
Memory mem -> Memory mem -> Memory mem
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
forall (mem :: Nat). Eq (Memory mem)
forall (mem :: Nat). Memory mem -> Memory mem -> Bool
forall (mem :: Nat). Memory mem -> Memory mem -> Ordering
forall (mem :: Nat). Memory mem -> Memory mem -> Memory mem
min :: Memory mem -> Memory mem -> Memory mem
$cmin :: forall (mem :: Nat). Memory mem -> Memory mem -> Memory mem
max :: Memory mem -> Memory mem -> Memory mem
$cmax :: forall (mem :: Nat). Memory mem -> Memory mem -> Memory mem
>= :: Memory mem -> Memory mem -> Bool
$c>= :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
> :: Memory mem -> Memory mem -> Bool
$c> :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
<= :: Memory mem -> Memory mem -> Bool
$c<= :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
< :: Memory mem -> Memory mem -> Bool
$c< :: forall (mem :: Nat). Memory mem -> Memory mem -> Bool
compare :: Memory mem -> Memory mem -> Ordering
$ccompare :: forall (mem :: Nat). Memory mem -> Memory mem -> Ordering
$cp1Ord :: forall (mem :: Nat). Eq (Memory mem)
Ord)

{- | Semigroup over addition.

>>> byte 2 <> byte 5
Memory {unMemory = 56}
-}
instance Semigroup (Memory (mem :: Nat)) where
    (<>) :: Memory mem -> Memory mem -> Memory mem
    <> :: Memory mem -> Memory mem -> Memory mem
(<>) = (Natural -> Natural -> Natural)
-> Memory mem -> Memory mem -> Memory mem
forall a b. Coercible a b => a -> b
coerce (Num Natural => Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(+) @Natural)
    {-# INLINE (<>) #-}

    sconcat :: NonEmpty (Memory mem) -> Memory mem
    sconcat :: NonEmpty (Memory mem) -> Memory mem
sconcat = (Memory mem -> Memory mem -> Memory mem)
-> Memory mem -> NonEmpty (Memory mem) -> Memory mem
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Memory mem -> Memory mem -> Memory mem
forall a. Semigroup a => a -> a -> a
(<>) Memory mem
forall a. Monoid a => a
mempty
    {-# INLINE sconcat #-}

    stimes :: Integral b => b -> Memory mem -> Memory mem
    stimes :: b -> Memory mem -> Memory mem
stimes n :: b
n (Memory m :: Natural
m) = Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory (b -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
m)
    {-# INLINE stimes #-}

instance Monoid (Memory (mem :: Nat)) where
    mempty :: Memory mem
    mempty :: Memory mem
mempty = Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory 0
    {-# INLINE mempty #-}

    mappend :: Memory mem -> Memory mem -> Memory mem
    mappend :: Memory mem -> Memory mem -> Memory mem
mappend = Memory mem -> Memory mem -> Memory mem
forall a. Semigroup a => a -> a -> a
(<>)
    {-# INLINE mappend #-}

    mconcat :: [Memory mem] -> Memory mem
    mconcat :: [Memory mem] -> Memory mem
mconcat = (Memory mem -> Memory mem -> Memory mem)
-> Memory mem -> [Memory mem] -> Memory mem
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Memory mem -> Memory mem -> Memory mem
forall a. Semigroup a => a -> a -> a
(<>) Memory mem
forall a. Monoid a => a
mempty
    {-# INLINE mconcat #-}

{- |
This 'showMemory' function shows a 'Memory' value as 'Double' along with the
measure unit suffix. It shows 'Memory' losslessly while used with standardized
units of measurements. The following mathematical law is used to display
'Memory':

A decimal representation written with a repeating final @0@ is supposed to
terminate before these zeros. Instead of @1.585000...@ one simply writes
@1.585@. The decimal is also called a terminating decimal. Terminating decimals
represent rational numbers of the form \( \cfrac{k}{2^n 5^m} \). If you use
different forms of units then the 'show' function for 'Memory' hangs.

>>> showMemory (Memory 22 :: Memory Byte)
"2.75B"
-}
showMemory :: forall mem . (KnownNat mem, KnownUnitSymbol mem) => Memory mem -> String
showMemory :: Memory mem -> String
showMemory (Memory m :: Natural
m) = Natural -> Natural -> String
showFrac Natural
m (KnownNat mem => Natural
forall (mem :: Nat). KnownNat mem => Natural
nat @mem) String -> ShowS
forall a. [a] -> [a] -> [a]
++ KnownUnitSymbol mem => String
forall (mem :: Nat). KnownUnitSymbol mem => String
unitSymbol @mem
  where
    showFrac :: Natural -> Natural -> String
    showFrac :: Natural -> Natural -> String
showFrac number :: Natural
number d :: Natural
d = Natural -> String
goIntegral Natural
number
      where
        -- take integral part of fraction
        goIntegral :: Natural -> String
        goIntegral :: Natural -> String
goIntegral n :: Natural
n =
            let (q :: Natural
q, r :: Natural
r) = Natural
n Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
d
                integral :: String
integral = Natural -> String
forall a. Show a => a -> String
show Natural
q
            in if Natural
r Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 0
               then String
integral
               else String
integral String -> ShowS
forall a. [a] -> [a] -> [a]
++ '.' Char -> ShowS
forall a. a -> [a] -> [a]
: Natural -> String
goFractional Natural
r

        -- convert reminder to fractional part
        goFractional :: Natural -> String
        goFractional :: Natural -> String
goFractional 0 = ""
        goFractional n :: Natural
n =
            let (q :: Natural
q, r :: Natural
r) = (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* 10) Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
d
            in Natural -> String
forall a. Show a => a -> String
show Natural
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
goFractional Natural
r


{- | Inverse of 'showMemory'.

>>> readMemory @Byte "2.75B"
Just (Memory {unMemory = 22})
>>> readMemory @Bit "2.75B"
Nothing
-}
readMemory
    :: forall (mem :: Nat)
     . (KnownUnitSymbol mem, KnownNat mem)
    => String
    -> Maybe (Memory mem)
readMemory :: String -> Maybe (Memory mem)
readMemory ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace -> String
str) = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit String
str of
    ([], _) -> Maybe (Memory mem)
forall a. Maybe a
Nothing
    (_, []) -> Maybe (Memory mem)
forall a. Maybe a
Nothing
    (ds :: String
ds, '.': rest :: String
rest) -> case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit String
rest of
        ([], _)           -> Maybe (Memory mem)
forall a. Maybe a
Nothing
        (numerator :: String
numerator, unit :: String
unit) -> String -> String -> String -> Maybe (Memory mem)
makeMemory String
ds String
numerator String
unit
    (ds :: String
ds, unit :: String
unit) -> String -> String -> String -> Maybe (Memory mem)
makeMemory String
ds "0" String
unit
  where
    makeMemory :: String -> String -> String -> Maybe (Memory mem)
    makeMemory :: String -> String -> String -> Maybe (Memory mem)
makeMemory (Read Natural => String -> Natural
forall a. Read a => String -> a
read @Natural -> Natural
whole) numStr :: String
numStr u :: String
u =
        if KnownUnitSymbol mem => String
forall (mem :: Nat). KnownUnitSymbol mem => String
unitSymbol @mem String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
u
        then case ((Natural
whole Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
numPow Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
num) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
unit) Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
numPow of
            (b :: Natural
b, 0) -> Memory mem -> Maybe (Memory mem)
forall a. a -> Maybe a
Just (Memory mem -> Maybe (Memory mem))
-> Memory mem -> Maybe (Memory mem)
forall a b. (a -> b) -> a -> b
$ Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory Natural
b
            _      -> Maybe (Memory mem)
forall a. Maybe a
Nothing
        else Maybe (Memory mem)
forall a. Maybe a
Nothing
      where
          unit :: Natural
          unit :: Natural
unit = KnownNat mem => Natural
forall (mem :: Nat). KnownNat mem => Natural
nat @mem

          num :: Natural
          num :: Natural
num = String -> Natural
forall a. Read a => String -> a
read @Natural String
numStr

          numPow :: Natural
          numPow :: Natural
numPow = 10 Natural -> Int -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
numStr

{- | Creates 'Memory' of unit @mem@ by the given 'Natural' number. 'Memory's
smart constructor.

>>> memory @Byte 3
Memory {unMemory = 24}
-}
memory :: forall (mem :: Nat) . KnownNat mem => Natural -> Memory mem
memory :: Natural -> Memory mem
memory = Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory (Natural -> Memory mem)
-> (Natural -> Natural) -> Natural -> Memory mem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* KnownNat mem => Natural
forall (mem :: Nat). KnownNat mem => Natural
nat @mem)
{-# INLINE memory #-}

{- | Convert memory from one unit to another.

__Note:__ this changes only view, not model.
So this operation has zero runtime cost.

>>> showMemory $ toMemory @Kilobyte $ byte 100
"0.1kB"
>>> showMemory $ toMemory @Kibibyte $ byte 100
"0.09765625KiB"
-}
toMemory :: forall (to :: Nat) (from :: Nat) . Memory from -> Memory to
toMemory :: Memory from -> Memory to
toMemory = Memory from -> Memory to
forall a b. Coercible a b => a -> b
coerce
{-# INLINE toMemory #-}

{- | Lossless 'Memory' conversion to bits. Alias to 'unMemory'.

>>> toBits $ byte 1
8
>>> toBits $ kilobyte 1
8000
-}
toBits :: Memory mem -> Natural
toBits :: Memory mem -> Natural
toBits = Memory mem -> Natural
forall a b. Coercible a b => a -> b
coerce
{-# INLINE toBits #-}

{- | Lossless 'Memory' conversion to rational number.

>>> toRat $ byte 4
4 % 1
>>> toRat $ toMemory @Byte $ bit 22
11 % 4
-}
toRat :: forall (mem :: Nat) . KnownNat mem => Memory mem -> Ratio Natural
toRat :: Memory mem -> Ratio Natural
toRat (Memory m :: Natural
m) = Natural
m Natural -> Natural -> Ratio Natural
forall a. Integral a => a -> a -> Ratio a
% KnownNat mem => Natural
forall (mem :: Nat). KnownNat mem => Natural
nat @mem
{-# INLINE toRat #-}

{- | Floor 'Memory' unit to integral number. This function may lose some
information, so use only when:

1. You don't care about losing information.
2. You are sure that there will be no loss.

>>> floor $ byte 4
4
>>> floor $ toMemory @Byte $ bit 22
2
-}
floor
    :: forall (n :: Type) (mem :: Nat) .
       (Integral n, KnownNat mem)
    => Memory mem
    -> n
floor :: Memory mem -> n
floor = Ratio Natural -> n
forall a b. (RealFrac a, Integral b) => a -> b
Prelude.floor (Ratio Natural -> n)
-> (Memory mem -> Ratio Natural) -> Memory mem -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Memory mem -> Ratio Natural
forall (mem :: Nat). KnownNat mem => Memory mem -> Ratio Natural
toRat
{-# INLINE floor #-}
{-# SPECIALIZE floor :: KnownNat mem => Memory mem -> Int     #-}
{-# SPECIALIZE floor :: KnownNat mem => Memory mem -> Word    #-}
{-# SPECIALIZE floor :: KnownNat mem => Memory mem -> Integer #-}
{-# SPECIALIZE floor :: KnownNat mem => Memory mem -> Natural #-}

----------------------------------------------------------------------------
-- Numeric functions
----------------------------------------------------------------------------

{- | Returns the result of multiplication 'Natural' with the given 'Memory' value

>>> memoryMul 2 (byte 4)
Memory {unMemory = 64}
-}
memoryMul  :: Natural -> Memory mem -> Memory mem
memoryMul :: Natural -> Memory mem -> Memory mem
memoryMul = Natural -> Memory mem -> Memory mem
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes
{-# INLINE memoryMul #-}

{- | Returns the result of comparison of two 'Memory' values
and the difference between them as another 'Memory' of the same unit.

>>> memoryDiff (bit 4) (bit 8)
(LT,Memory {unMemory = 4})
>>> memoryDiff (byte 8) (byte 4)
(GT,Memory {unMemory = 32})
>>> memoryDiff (kilobyte 2) (kilobyte 2)
(EQ,Memory {unMemory = 0})
-}
memoryDiff :: Memory mem -> Memory mem -> (Ordering, Memory mem)
memoryDiff :: Memory mem -> Memory mem -> (Ordering, Memory mem)
memoryDiff (Memory m1 :: Natural
m1) (Memory m2 :: Natural
m2) = case Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Natural
m1 Natural
m2 of
    LT -> (Ordering
LT, Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory (Natural -> Memory mem) -> Natural -> Memory mem
forall a b. (a -> b) -> a -> b
$ Natural
m2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
m1)
    GT -> (Ordering
GT, Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory (Natural -> Memory mem) -> Natural -> Memory mem
forall a b. (a -> b) -> a -> b
$ Natural
m1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
m2)
    EQ -> (Ordering
EQ, Natural -> Memory mem
forall (mem :: Nat). Natural -> Memory mem
Memory 0)
{-# INLINE memoryDiff #-}

{- | Returns the result of addition of two 'Memory' values casted
to the second memory unit.

>>> memoryPlus (bit 8) (megabyte 2)
Memory {unMemory = 16000008}
-}
memoryPlus :: Memory mem1 -> Memory mem2 -> Memory mem2
memoryPlus :: Memory mem1 -> Memory mem2 -> Memory mem2
memoryPlus m1 :: Memory mem1
m1 = Memory mem2 -> Memory mem2 -> Memory mem2
forall a. Semigroup a => a -> a -> a
(<>) (Memory mem1 -> Memory mem2
forall (to :: Nat) (from :: Nat). Memory from -> Memory to
toMemory Memory mem1
m1)
{-# INLINE memoryPlus #-}

{- | Retuns the result of division of two 'Memory' values of any units.

>>> memoryDiv (kilobyte 3) (byte 2)
1500 % 1
-}
memoryDiv :: Memory mem1 -> Memory mem2 -> Ratio Natural
memoryDiv :: Memory mem1 -> Memory mem2 -> Ratio Natural
memoryDiv (Memory m1 :: Natural
m1) (Memory m2 :: Natural
m2) = Natural
m1 Natural -> Natural -> Ratio Natural
forall a. Integral a => a -> a -> Ratio a
% Natural
m2
{-# INLINE memoryDiv #-}

----------------------------------------------------------------------------
-- AnyMemory
----------------------------------------------------------------------------

{- $any
This data type is useful for working with 'Memory' of different units in
collections, or when 'Memory' of non-specified unit can be returned.
-}

-- | Existential data type for 'Memory's.
data AnyMemory
    = forall (mem :: Nat) . (KnownNat mem, KnownUnitSymbol mem)
    => MkAnyMemory (Memory mem)

instance Show AnyMemory where
    show :: AnyMemory -> String
show (MkAnyMemory t :: Memory mem
t) = Memory mem -> String
forall (mem :: Nat).
(KnownNat mem, KnownUnitSymbol mem) =>
Memory mem -> String
showMemory Memory mem
t

----------------------------------------------------------------------------
-- Internal
----------------------------------------------------------------------------

nat :: forall (mem :: Nat) . KnownNat mem => Natural
nat :: Natural
nat = Proxy# mem -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' (Proxy# mem
forall k (a :: k). Proxy# a
proxy# :: Proxy# mem)
{-# INLINE nat #-}