-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE EmptyDataDeriving #-}

-- | Re-exports typed Value, CValue, some core types, some helpers and
-- defines aliases for constructors of typed values.
--
module Lorentz.Value
  ( M.Value
  , M.IsoValue (..)
  , M.WellTypedIsoValue

    -- * Primitive types
  , Integer
  , Natural
  , MText
  , Bool (..)
  , ByteString
  , Address
  , EpAddress (..)
  , Mutez
  , Never
  , Timestamp
  , ChainId
  , KeyHash
  , PublicKey
  , Signature
  , Bls12381Fr
  , Bls12381G1
  , Bls12381G2
  , Set
  , Map
  , M.BigMapId (..)
  , M.BigMap
  , M.mkBigMap
  , M.Operation
  , Maybe (..)
  , List
  , ReadTicket (..)
  , ContractRef (..)
  , TAddress (..)
  , FutureContract (..)
  , M.Ticket (..)

  , M.EpName
  , pattern M.DefEpName
  , M.EntrypointCall
  , M.SomeEntrypointCall

    -- * Custom datatypes
  , Fixed (..)
  , NFixed (..)
  , DecBase (..)
  , BinBase (..)

    -- * Constructors
  , toMutez
  , zeroMutez
  , oneMutez
  , mt
  , timestampFromSeconds
  , timestampFromUTCTime
  , timestampQuote

    -- * Conversions
  , M.coerceContractRef
  , callingAddress
  , callingDefAddress
  , callingTAddress
  , callingDefTAddress
  , ToAddress (..)
  , ToTAddress (..)
  , ToContractRef (..)
  , FromContractRef (..)
  , convertContractRef

    -- * Misc
  , Show
  , Default (..)
  , Label (..)
  , PrintAsValue (..)

  -- * Re-exports
  , module ReExports
  ) where

import Data.Constraint ((\\))
import Data.Default (Default(..))
import Data.Fixed (Fixed(..), HasResolution(..))
import GHC.Num
import Prelude hiding (fromInteger)
import qualified Text.Show

import Fmt (Buildable(..))

import Lorentz.Address
import Lorentz.Constraints.Scopes
import Lorentz.Wrappable
import Morley.Michelson.Text
import qualified Morley.Michelson.Typed as M
import Morley.Michelson.Typed.Haskell.Compatibility as ReExports
import Morley.Tezos.Core
  (ChainId, Mutez, Timestamp, oneMutez, timestampFromSeconds, timestampFromUTCTime, timestampQuote,
  toMutez, zeroMutez)
import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)
import Morley.Util.CustomGeneric as ReExports
import Morley.Util.Label (Label(..))

import Lorentz.Annotation

type List = []

data Never
  deriving stock ((forall x. Never -> Rep Never x)
-> (forall x. Rep Never x -> Never) -> Generic Never
forall x. Rep Never x -> Never
forall x. Never -> Rep Never x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Never x -> Never
$cfrom :: forall x. Never -> Rep Never x
Generic, Int -> Never -> ShowS
[Never] -> ShowS
Never -> String
(Int -> Never -> ShowS)
-> (Never -> String) -> ([Never] -> ShowS) -> Show Never
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Never] -> ShowS
$cshowList :: [Never] -> ShowS
show :: Never -> String
$cshow :: Never -> String
showsPrec :: Int -> Never -> ShowS
$cshowsPrec :: Int -> Never -> ShowS
Show, Never -> Never -> Bool
(Never -> Never -> Bool) -> (Never -> Never -> Bool) -> Eq Never
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Never -> Never -> Bool
$c/= :: Never -> Never -> Bool
== :: Never -> Never -> Bool
$c== :: Never -> Never -> Bool
Eq, Eq Never
Eq Never
-> (Never -> Never -> Ordering)
-> (Never -> Never -> Bool)
-> (Never -> Never -> Bool)
-> (Never -> Never -> Bool)
-> (Never -> Never -> Bool)
-> (Never -> Never -> Never)
-> (Never -> Never -> Never)
-> Ord Never
Never -> Never -> Bool
Never -> Never -> Ordering
Never -> Never -> Never
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
min :: Never -> Never -> Never
$cmin :: Never -> Never -> Never
max :: Never -> Never -> Never
$cmax :: Never -> Never -> Never
>= :: Never -> Never -> Bool
$c>= :: Never -> Never -> Bool
> :: Never -> Never -> Bool
$c> :: Never -> Never -> Bool
<= :: Never -> Never -> Bool
$c<= :: Never -> Never -> Bool
< :: Never -> Never -> Bool
$c< :: Never -> Never -> Bool
compare :: Never -> Never -> Ordering
$ccompare :: Never -> Never -> Ordering
$cp1Ord :: Eq Never
Ord)
  deriving anyclass (WellTypedToT Never
WellTypedToT Never
-> (Never -> Value (ToT Never))
-> (Value (ToT Never) -> Never)
-> IsoValue Never
Value (ToT Never) -> Never
Never -> Value (ToT Never)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT Never) -> Never
$cfromVal :: Value (ToT Never) -> Never
toVal :: Never -> Value (ToT Never)
$ctoVal :: Never -> Value (ToT Never)
$cp1IsoValue :: WellTypedToT Never
M.IsoValue, Never -> ()
(Never -> ()) -> NFData Never
forall a. (a -> ()) -> NFData a
rnf :: Never -> ()
$crnf :: Never -> ()
NFData)

instance Buildable Never where
  build :: Never -> Builder
build = Never -> Builder
\case

instance HasAnnotation Never where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT Never)
getAnnotation FollowEntrypointFlag
_ = Notes (ToT Never)
forall (t :: T). SingI t => Notes t
M.starNotes

instance M.TypeHasDoc Never where
  typeDocMdDescription :: Builder
typeDocMdDescription = Builder
"An uninhabited type."

-- | Value returned by @READ_TICKET@ instruction.
data ReadTicket a = ReadTicket
  { ReadTicket a -> Address
rtTicketer :: Address
  , ReadTicket a -> a
rtData :: a
  , ReadTicket a -> Natural
rtAmount :: Natural
  } deriving stock (Int -> ReadTicket a -> ShowS
[ReadTicket a] -> ShowS
ReadTicket a -> String
(Int -> ReadTicket a -> ShowS)
-> (ReadTicket a -> String)
-> ([ReadTicket a] -> ShowS)
-> Show (ReadTicket a)
forall a. Show a => Int -> ReadTicket a -> ShowS
forall a. Show a => [ReadTicket a] -> ShowS
forall a. Show a => ReadTicket a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReadTicket a] -> ShowS
$cshowList :: forall a. Show a => [ReadTicket a] -> ShowS
show :: ReadTicket a -> String
$cshow :: forall a. Show a => ReadTicket a -> String
showsPrec :: Int -> ReadTicket a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ReadTicket a -> ShowS
Show, ReadTicket a -> ReadTicket a -> Bool
(ReadTicket a -> ReadTicket a -> Bool)
-> (ReadTicket a -> ReadTicket a -> Bool) -> Eq (ReadTicket a)
forall a. Eq a => ReadTicket a -> ReadTicket a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReadTicket a -> ReadTicket a -> Bool
$c/= :: forall a. Eq a => ReadTicket a -> ReadTicket a -> Bool
== :: ReadTicket a -> ReadTicket a -> Bool
$c== :: forall a. Eq a => ReadTicket a -> ReadTicket a -> Bool
Eq, Eq (ReadTicket a)
Eq (ReadTicket a)
-> (ReadTicket a -> ReadTicket a -> Ordering)
-> (ReadTicket a -> ReadTicket a -> Bool)
-> (ReadTicket a -> ReadTicket a -> Bool)
-> (ReadTicket a -> ReadTicket a -> Bool)
-> (ReadTicket a -> ReadTicket a -> Bool)
-> (ReadTicket a -> ReadTicket a -> ReadTicket a)
-> (ReadTicket a -> ReadTicket a -> ReadTicket a)
-> Ord (ReadTicket a)
ReadTicket a -> ReadTicket a -> Bool
ReadTicket a -> ReadTicket a -> Ordering
ReadTicket a -> ReadTicket a -> ReadTicket a
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 a. Ord a => Eq (ReadTicket a)
forall a. Ord a => ReadTicket a -> ReadTicket a -> Bool
forall a. Ord a => ReadTicket a -> ReadTicket a -> Ordering
forall a. Ord a => ReadTicket a -> ReadTicket a -> ReadTicket a
min :: ReadTicket a -> ReadTicket a -> ReadTicket a
$cmin :: forall a. Ord a => ReadTicket a -> ReadTicket a -> ReadTicket a
max :: ReadTicket a -> ReadTicket a -> ReadTicket a
$cmax :: forall a. Ord a => ReadTicket a -> ReadTicket a -> ReadTicket a
>= :: ReadTicket a -> ReadTicket a -> Bool
$c>= :: forall a. Ord a => ReadTicket a -> ReadTicket a -> Bool
> :: ReadTicket a -> ReadTicket a -> Bool
$c> :: forall a. Ord a => ReadTicket a -> ReadTicket a -> Bool
<= :: ReadTicket a -> ReadTicket a -> Bool
$c<= :: forall a. Ord a => ReadTicket a -> ReadTicket a -> Bool
< :: ReadTicket a -> ReadTicket a -> Bool
$c< :: forall a. Ord a => ReadTicket a -> ReadTicket a -> Bool
compare :: ReadTicket a -> ReadTicket a -> Ordering
$ccompare :: forall a. Ord a => ReadTicket a -> ReadTicket a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ReadTicket a)
Ord)

customGeneric "ReadTicket" rightComb

deriving anyclass instance M.IsoValue a => M.IsoValue (ReadTicket a)

-- | Provides 'Buildable' instance that prints Lorentz value via Michelson's
-- 'M.Value'.
--
-- Result won't be very pretty, but this avoids requiring 'Show' or
-- 'Buildable' instances.
newtype PrintAsValue a = PrintAsValue a

instance NiceUntypedValue a => Buildable (PrintAsValue a) where
  build :: PrintAsValue a -> Builder
build (PrintAsValue a
a) = Value (ToT a) -> Builder
forall p. Buildable p => p -> Builder
build (a -> Value (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
M.toVal a
a) ((SingI (ToT a), HasNoOp (ToT a)) => Builder)
-> (NiceUntypedValue a :- (SingI (ToT a), HasNoOp (ToT a)))
-> Builder
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ NiceUntypedValue a :- (SingI (ToT a), HasNoOp (ToT a))
forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
niceUntypedValueEvi @a

-- | Datatypes, representing base of the fixed-point values
data DecBase p where
  DecBase :: KnownNat p => DecBase p
data BinBase p where
  BinBase :: KnownNat p => BinBase p

instance KnownNat p => HasResolution (DecBase p) where
  resolution :: p (DecBase p) -> Integer
resolution p (DecBase p)
_ = Integer
10 Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy p -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy p
forall k (t :: k). Proxy t
Proxy @p))

instance KnownNat p => HasResolution (BinBase p) where
  resolution :: p (BinBase p) -> Integer
resolution p (BinBase p)
_ = Integer
2 Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy p -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy p
forall k (t :: k). Proxy t
Proxy @p))

-- | Like @Fixed@ but with a @Natural@ value inside constructor
newtype NFixed p = MkNFixed Natural deriving stock (NFixed p -> NFixed p -> Bool
(NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool) -> Eq (NFixed p)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (p :: k). NFixed p -> NFixed p -> Bool
/= :: NFixed p -> NFixed p -> Bool
$c/= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
== :: NFixed p -> NFixed p -> Bool
$c== :: forall k (p :: k). NFixed p -> NFixed p -> Bool
Eq, Eq (NFixed p)
Eq (NFixed p)
-> (NFixed p -> NFixed p -> Ordering)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> Bool)
-> (NFixed p -> NFixed p -> NFixed p)
-> (NFixed p -> NFixed p -> NFixed p)
-> Ord (NFixed p)
NFixed p -> NFixed p -> Bool
NFixed p -> NFixed p -> Ordering
NFixed p -> NFixed p -> NFixed p
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 k (p :: k). Eq (NFixed p)
forall k (p :: k). NFixed p -> NFixed p -> Bool
forall k (p :: k). NFixed p -> NFixed p -> Ordering
forall k (p :: k). NFixed p -> NFixed p -> NFixed p
min :: NFixed p -> NFixed p -> NFixed p
$cmin :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
max :: NFixed p -> NFixed p -> NFixed p
$cmax :: forall k (p :: k). NFixed p -> NFixed p -> NFixed p
>= :: NFixed p -> NFixed p -> Bool
$c>= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
> :: NFixed p -> NFixed p -> Bool
$c> :: forall k (p :: k). NFixed p -> NFixed p -> Bool
<= :: NFixed p -> NFixed p -> Bool
$c<= :: forall k (p :: k). NFixed p -> NFixed p -> Bool
< :: NFixed p -> NFixed p -> Bool
$c< :: forall k (p :: k). NFixed p -> NFixed p -> Bool
compare :: NFixed p -> NFixed p -> Ordering
$ccompare :: forall k (p :: k). NFixed p -> NFixed p -> Ordering
$cp1Ord :: forall k (p :: k). Eq (NFixed p)
Ord)

convertNFixedToFixed :: NFixed a -> Fixed a
convertNFixedToFixed :: NFixed a -> Fixed a
convertNFixedToFixed (MkNFixed Natural
a) = Integer -> Fixed a
forall k (a :: k). Integer -> Fixed a
MkFixed (Natural -> Integer
forall a b.
(Integral a, Integral b, IsIntSubType a b ~ 'True) =>
a -> b
fromIntegral Natural
a)

instance (HasResolution a) => Show (NFixed a) where
  show :: NFixed a -> String
show = Fixed a -> String
forall b a. (Show a, IsString b) => a -> b
show (Fixed a -> String) -> (NFixed a -> Fixed a) -> NFixed a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NFixed a -> Fixed a
forall k (a :: k). NFixed a -> Fixed a
convertNFixedToFixed

-- Note: This instances are copies of those in Data.Fixed for Fixed datatype
instance (HasResolution a) => Num (NFixed a) where
  (MkNFixed Natural
a) + :: NFixed a -> NFixed a -> NFixed a
+ (MkNFixed Natural
b) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b)
  (MkNFixed Natural
a) - :: NFixed a -> NFixed a -> NFixed a
- (MkNFixed Natural
b) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
b)
  fa :: NFixed a
fa@(MkNFixed Natural
a) * :: NFixed a -> NFixed a -> NFixed a
* (MkNFixed Natural
b) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
div (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b) (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa)))
  negate :: NFixed a -> NFixed a
negate (MkNFixed Natural
a) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural
forall a. Num a => a -> a
negate Natural
a)
  abs :: NFixed a -> NFixed a
abs = NFixed a -> NFixed a
forall a. a -> a
id
  signum :: NFixed a -> NFixed a
signum (MkNFixed Natural
a) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural
forall a. Num a => a -> a
signum Natural
a)
  fromInteger :: Integer -> NFixed a
fromInteger Integer
i = (Natural -> NFixed a) -> NFixed a
forall k (a :: k) (f :: k -> *).
HasResolution a =>
(Natural -> f a) -> f a
withResolution (\Natural
res -> Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed ((Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
res))

instance (HasResolution a) => Fractional (NFixed a) where
  fa :: NFixed a
fa@(MkNFixed Natural
a) / :: NFixed a -> NFixed a -> NFixed a
/ (MkNFixed Natural
b) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
div (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa))) Natural
b)
  recip :: NFixed a -> NFixed a
recip fa :: NFixed a
fa@(MkNFixed Natural
a) = Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
div (Natural
res Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
res) Natural
a) where
      res :: Natural
res = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ NFixed a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution NFixed a
fa
  fromRational :: Rational -> NFixed a
fromRational Rational
r = (Natural -> NFixed a) -> NFixed a
forall k (a :: k) (f :: k -> *).
HasResolution a =>
(Natural -> f a) -> f a
withResolution (\Natural
res -> Natural -> NFixed a
forall k (p :: k). Natural -> NFixed p
MkNFixed (Rational -> Natural
forall a b. (RealFrac a, Integral b) => a -> b
floor (Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* (Natural -> Rational
forall a. Real a => a -> Rational
toRational Natural
res))))

instance M.IsoValue (NFixed p) where
  type ToT (NFixed p) = 'M.TNat
  toVal :: NFixed p -> Value (ToT (NFixed p))
toVal (MkNFixed Natural
x) = Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
M.VNat Natural
x
  fromVal :: Value (ToT (NFixed p)) -> NFixed p
fromVal (M.VNat Natural
x) = Natural -> NFixed p
forall k (p :: k). Natural -> NFixed p
MkNFixed Natural
x

instance Unwrappable (NFixed a) where
  type Unwrappabled (NFixed a) = Natural

-- Helpers copied from Data.Fixed, because they are not exported from there
withResolution :: forall a f. (HasResolution a) => (Natural -> f a) -> f a
withResolution :: (Natural -> f a) -> f a
withResolution Natural -> f a
foo = Natural -> f a
foo (Natural -> f a) -> (Proxy a -> Natural) -> Proxy a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> (Proxy a -> Integer) -> Proxy a -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Integer
forall k (a :: k) (p :: k -> *). HasResolution a => p a -> Integer
resolution (Proxy a -> f a) -> Proxy a -> f a
forall a b. (a -> b) -> a -> b
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a