Symbolic.hs

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

-- | All the basic 'Expr'essions used in Indigo code.
--
-- Note: infix operators acting on structure follow a naming convention:
--
-- 1. the last character identifies the structure type:
--
--      - @:@ for containers ('Map', 'BigMap', 'Set', 'List')
--      - @\@@ for 'UStore'
--      - @!@ for 'HasField'
--      - @~@ fot 'Util.Named'
--
-- 2. the preceding characters identify the action:
--
--      - @#@ for get, lookup or from
--      - @!@ for set, update or to
--      - @+@ for insert
--      - @++@ for insertNew
--      - @-@ for remove
--      - @?@ for mem or elem
--
-- The only exception to this convention is '(.:)' (for 'cons')

module Indigo.Internal.Expr.Symbolic
  ( -- * Basic
    constExpr, varExpr, cast

  -- * Math
  , add, sub, mul, div, mod, neg, abs
  , (+), (-), (*), (/), (%)

  -- * Comparison
  , eq, neq, lt, gt, le, ge
  , (==), (/=), (<), (>), (<=), (>=)

  -- * Conversion
  , isNat, toInt, nonZero

  -- * Bits and boolean
  , lsl, lsr, and, or, xor, not
  , (<<<), (>>>), (&&), (||), (^)

  -- * Serialization
  , pack, unpack

  -- * Pairs
  , pair, car, cdr, fst, snd

  -- * Maybe
  , some, none

  -- * Either
  , right, left

  -- * Bytes and string
  , slice, concat, (<>)

  -- * List
  , concatAll, nil, cons, (.:)

  -- * Containers
  , get, update, insert, remove, mem, size
  , (#:), (!:), (+:), (-:), (?:)
  , empty, emptyBigMap, emptyMap, emptySet

  -- * UStore
  , uGet, uUpdate, uInsert, uInsertNew, uDelete, uMem
  , (#@), (!@), (+@), (++@), (-@), (?@)

  -- * HasField
  , (!!), (#!)

  -- * Record and Named
  , name, unName, (!~), (#~)
  , construct, constructRec

  -- * Contract
  , contract
  , self
  , contractAddress
  , contractCallingUnsafe
  , contractCallingString
  , runFutureContract
  , implicitAccount
  , convertEpAddressToContract
  , makeView
  , makeVoid

  -- * Auxiliary
  , now
  , amount
  , sender
  , blake2b
  , sha256
  , sha512
  , hashKey
  , chainId
  , balance
  , checkSignature
  ) where

import Data.Vinyl.Core (RMap(..))

import Indigo.Internal.Expr.Types
import Indigo.Internal.Field
import Indigo.Internal.Object (Var)
import Indigo.Lorentz
import Indigo.Prelude
import qualified Michelson.Typed.Arith as M
import Util.TypeTuple
import Michelson.Text (unMText)
import Michelson.Untyped.Entrypoints (unsafeBuildEpName)

----------------------------------------------------------------------------
-- Basic
----------------------------------------------------------------------------

constExpr :: NiceConstant a => a -> Expr a
constExpr = C

-- | Create an expression holding a variable.
varExpr :: KnownValue a => Var a -> Expr a
varExpr = V

cast :: (ex :~> a) => ex -> Expr a
cast = Cast

----------------------------------------------------------------------------
-- Math
----------------------------------------------------------------------------

infixl 6 +
add, (+)
  :: IsArithExpr exN exM M.Add n m
  => exN -> exM
  -> Expr (ArithResHs M.Add n m)
add = Add
(+) = Add

infixl 6 -
sub, (-)
  :: IsArithExpr exN exM M.Sub n m
  => exN -> exM
  -> Expr (ArithResHs M.Sub n m)
sub = Sub
(-) = Sub

infixl 7 *
mul, (*)
  :: IsArithExpr exN exM M.Mul n m
  => exN -> exM
  -> Expr (ArithResHs M.Mul n m)
mul = Mul
(*) = Mul

infixl 7 /
div, (/)
  :: IsDivExpr exN exM n m
  => exN -> exM
  -> Expr (EDivOpResHs n m)
div = Div
(/) = Div

infixl 7 %
mod, (%)
  :: IsModExpr exN exM n m
  => exN -> exM
  -> Expr (EModOpResHs n m)
mod = Mod
(%) = Mod

abs
  :: IsUnaryArithExpr exN M.Abs n
  => exN
  -> Expr (UnaryArithResHs M.Abs n)
abs = Abs

neg
  :: IsUnaryArithExpr exN M.Neg n
  => exN
  -> Expr (UnaryArithResHs M.Neg n)
neg = Neg

----------------------------------------------------------------------------
-- Comparison
----------------------------------------------------------------------------

infix 4 ==
eq, (==)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
eq = Eq'
(==) = Eq'

infix 4 /=
neq, (/=)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
neq = Neq
(/=) = Neq

infix 4 <
lt, (<)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
lt = Lt
(<) = Lt

infix 4 >
gt, (>)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
gt = Gt
(>) = Gt

infix 4 <=
le, (<=)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
le = Le
(<=) = Le

infix 4 >=
ge, (>=)
  :: (NiceComparable n, AreExprs c c1 n n)
  => c -> c1
  -> Expr Bool
ge = Ge
(>=) = Ge

----------------------------------------------------------------------------
-- Conversion
----------------------------------------------------------------------------

isNat :: (ex :~> Integer) => ex -> Expr (Maybe Natural)
isNat = IsNat

toInt :: (ex :~> Natural) => ex -> Expr Integer
toInt = Int'

nonZero :: (ex :~> n, NonZero n, KnownValue (Maybe n)) => ex -> Expr (Maybe n)
nonZero = NonZero

----------------------------------------------------------------------------
-- Bits and boolean
----------------------------------------------------------------------------

infixl 8 <<<
lsl, (<<<)
  :: IsArithExpr exN exM M.Lsl n m
  => exN -> exM
  -> Expr (ArithResHs M.Lsl n m)
lsl = Lsl
(<<<) = Lsl

infixl 8 >>>
lsr, (>>>)
  :: IsArithExpr exN exM M.Lsr n m
  => exN -> exM
  -> Expr (ArithResHs M.Lsr n m)
lsr = Lsr
(>>>) = Lsr

infixr 2 ||
or, (||)
  :: IsArithExpr exN exM M.Or n m
  => exN -> exM
  -> Expr (ArithResHs M.Or n m)
or = Or
(||) = Or

infixr 3 &&
and, (&&)
  :: IsArithExpr exN exM M.And n m
  => exN -> exM
  -> Expr (ArithResHs M.And n m)
and = And
(&&) = And

infixr 2 ^
xor, (^)
  :: IsArithExpr exN exM M.Xor n m
  => exN -> exM
  -> Expr (ArithResHs M.Xor n m)
xor = Xor
(^) = Xor

not
  :: IsUnaryArithExpr exN M.Not n
  => exN
  -> Expr (UnaryArithResHs M.Not n)
not = Not

----------------------------------------------------------------------------
-- Serialization
----------------------------------------------------------------------------

pack :: (IsExpr ex a, NicePackedValue a) => ex -> Expr ByteString
pack = Pack

unpack :: (NiceUnpackedValue a, exb :~> ByteString) => exb -> Expr (Maybe a)
unpack = Unpack

----------------------------------------------------------------------------
-- Pairs
----------------------------------------------------------------------------

pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)
pair = Pair

car, fst :: (op :~> (n, m), KnownValue n) => op -> Expr n
car = Fst
fst = Fst

cdr, snd :: (op :~> (n, m), KnownValue m) => op -> Expr m
cdr = Snd
snd = Snd

----------------------------------------------------------------------------
-- Maybe
----------------------------------------------------------------------------

some :: (ex :~> t, KnownValue (Maybe t)) => ex -> Expr (Maybe t)
some = Some

none :: KnownValue t => Expr (Maybe t)
none = None

----------------------------------------------------------------------------
-- Either
----------------------------------------------------------------------------

right :: (ex :~> x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x)
right = Right'

left :: (ex :~> y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x)
left = Left'

----------------------------------------------------------------------------
-- Bytes and string
----------------------------------------------------------------------------

slice
  :: ( an :~> Natural
     , bn :~> Natural
     , IsSliceExpr ex c
     )
  => (an, bn) -> ex
  -> Expr (Maybe c)
slice (a, b) = Slice a b

infixr 6 <>
concat, (<>)
  :: IsConcatExpr exN1 exN2 n
  => exN1 -> exN2
  -> Expr n
concat = Concat
(<>) = Concat

----------------------------------------------------------------------------
-- List
----------------------------------------------------------------------------

infixr 5 .:
cons, (.:) :: (ex1 :~> a, ex2 :~> List a) => ex1 -> ex2 -> Expr (List a)
cons = Cons
(.:) = Cons

concatAll :: IsConcatListExpr exN n => exN -> Expr n
concatAll = Concat'

nil :: KnownValue a => Expr (List a)
nil = Nil

----------------------------------------------------------------------------
-- Containers
----------------------------------------------------------------------------

class ExprMagma c where
  empty :: (NiceComparable (UpdOpKeyHs c), KnownValue c) => Expr c

instance KnownValue v => ExprMagma (BigMap k v) where
  empty = EmptyBigMap

instance KnownValue v => ExprMagma (Map k v) where
  empty = EmptyMap

instance ExprMagma (Set k) where
  empty = EmptySet

-- | Expression class to insert an element into a data structure.
--
-- Note that while this is based on 'update' and 'UpdOpHs', it is necessary to
-- have different instances to allow for different 'update' parameter types,
-- ('Set' uses a 'Bool' instead of a 'Maybe'), just like 'ExprRemovable'.
--
-- Moreover, this class is parameterized with an @insParam@ as well in order to
-- have both key-value pairs ('Map' and 'BigMap') as well as key only ('Set').
class UpdOpHs c => ExprInsertable c insParam where
  insert :: ex :~> c => insParam -> ex -> Expr c

instance (NiceComparable k, exKey :~> k, exValue :~> v)
    => ExprInsertable (BigMap k v) (exKey, exValue) where
  insert (k, v) c = Update c k (some v)

instance (NiceComparable k, exKey :~> k, exValue :~> v)
    => ExprInsertable (Map k v) (exKey, exValue) where
  insert (k, v) c = Update c k (some v)

instance (NiceComparable a, exKey :~> a) => ExprInsertable (Set a) exKey where
  insert k c = Update c k True

-- | Expression class to remove an element from a data structure.
--
-- Note that while this is based on 'update' and 'UpdOpHs', it is necessary to
-- have different instances to allow for different 'update' parameter types,
-- ('Set' uses a 'Bool' instead of a 'Maybe').
class UpdOpHs c => ExprRemovable c where
  remove
    :: (exStruct :~> c, exKey :~> UpdOpKeyHs c)
    => exKey -> exStruct -> Expr c

instance (NiceComparable k, KnownValue v) => ExprRemovable (BigMap k v) where
  remove k c = Update c k none

instance (NiceComparable k, KnownValue v) => ExprRemovable (Map k v) where
  remove k c = Update c k none

instance NiceComparable a => ExprRemovable (Set a) where
  remove k c = Update c k False

get
  :: IsGetExpr exKey exMap map
  => exKey -> exMap
  -> Expr (Maybe (GetOpValHs map))
get = Get

update
  :: IsUpdExpr exKey exVal exMap map
  => (exKey, exVal) -> exMap
  -> Expr map
update (k, v) s = Update s k v

mem
  :: IsMemExpr exKey exN n
  => exKey -> exN
  -> Expr Bool
mem = Mem

size
  :: IsSizeExpr exN n
  => exN -> Expr Natural
size = Size

infixl 8 #:
(#:)
  :: IsGetExpr exKey exMap map
  => exMap -> exKey
  -> Expr (Maybe (GetOpValHs map))
(#:) = flip get

infixl 8 !:
(!:)
  :: IsUpdExpr exKey exVal exMap map
  => exMap -> (exKey, exVal)
  -> Expr map
(!:) = flip update

infixl 8 +:
(+:)
  :: ( ExprInsertable c exParam
     , exStructure :~> c
     )
     => exStructure -> exParam
     -> Expr c
(+:) = flip insert

infixl 8 -:
(-:)
  :: ( ExprRemovable c
     , exStruct :~> c
     , exKey :~> UpdOpKeyHs c
     )
  => exStruct -> exKey
  -> Expr c
(-:) = flip remove

infixl 8 ?:
(?:)
  :: IsMemExpr exKey exN n
  => exN -> exKey
  -> Expr Bool
(?:) = flip mem

emptyBigMap
  :: (KnownValue value, NiceComparable key, KnownValue (BigMap key value))
  => Expr (BigMap key value)
emptyBigMap = empty

emptyMap
  :: (KnownValue value, NiceComparable key, KnownValue (Map key value))
  => Expr (Map key value)
emptyMap = empty

emptySet
  :: (NiceComparable key, KnownValue (Set key))
  => Expr (Set key)
emptySet = empty

----------------------------------------------------------------------------
-- UStore
----------------------------------------------------------------------------

infixr 8 #@
uGet, (#@)
  :: ( HasUStore name key value store
     , exKey   :~> key
     , exStore :~> (UStore store)
     )
  => exStore -> (Label name, exKey)
  -> Expr (Maybe value)
uGet store (uName, key) = UGet uName key store
(#@) = uGet

infixl 8 !@
uUpdate, (!@)
  :: ( HasUStore name key value store
     , exKey   :~> key
     , exVal   :~> Maybe value
     , exStore :~> UStore store
     )
  => exStore -> (Label name, exKey, exVal)
  -> Expr (UStore store)
uUpdate store (uName, key, val) = UUpdate uName key val store
(!@) = uUpdate

infixr 8 +@
uInsert, (+@)
  :: ( HasUStore name key value store
     , exKey   :~> key
     , exVal   :~> value
     , exStore :~> UStore store
     )
  => exStore -> (Label name, exKey, exVal)
  -> Expr (UStore store)
uInsert store (uName, key, val) = UInsert uName key val store
(+@) = uInsert

infixr 8 ++@
uInsertNew, (++@)
  :: ( HasUStore name key value store
     , IsError err
     , exKey   :~> key
     , exVal   :~> value
     , exStore :~> UStore store
     )
  => exStore
  -> (Label name, err, exKey, exVal)
  -> Expr (UStore store)
uInsertNew store (uName, err, key, val) = UInsertNew uName err key val store
(++@) = uInsertNew

infixl 8 -@
uDelete, (-@)
  :: ( HasUStore name key value store
     , exKey   :~> key
     , exStore :~> (UStore store)
     )
  => exStore -> (Label name, exKey)
  -> Expr (UStore store)
uDelete store (uName, key) = UDelete uName key store
(-@) = uDelete

infixl 8 ?@
uMem, (?@)
  :: ( HasUStore name key value store
     , exKey   :~> key
     , exStore :~> (UStore store)
     )
  => exStore -> (Label name, exKey)
  -> Expr Bool
uMem store (uName, key) = UMem uName key store
(?@) = uMem

----------------------------------------------------------------------------
-- HasField
----------------------------------------------------------------------------

infixl 8 #!
(#!)
  :: (HasField dt name ftype, exDt :~> dt)
  => exDt
  -> Label name
  -> Expr ftype
(#!) (toExpr -> (ObjMan fa)) fName = ObjMan (ToField fa fName)
(#!) exDt fName = ObjMan (ToField (Object $ toExpr exDt) fName)

infixl 8 !!
(!!)
  :: ( HasField dt name ftype
     , exDt :~> dt
     , exFld :~> ftype
     )
  => exDt
  -> (Label name, exFld)
  -> Expr dt
(!!) (toExpr -> (ObjMan fa)) (fName, eFld) = ObjMan (SetField fa fName (toExpr eFld))
dt !! (fName, eFld) = ObjMan (SetField (Object $ toExpr dt) fName (toExpr eFld))

----------------------------------------------------------------------------
-- Record and Named
----------------------------------------------------------------------------

name :: (ex :~> t, KnownValue (name :! t)) => Label name -> ex -> Expr (name :! t)
name = Name

unName :: (ex :~> (name :! t), KnownValue t) => Label name -> ex -> Expr t
unName = UnName

infixl 8 !~
(!~)
  :: (ex :~> t, KnownValue (name :! t))
  => ex -> Label name
  -> Expr (name :! t)
(!~) = flip name

infixl 8 #~
(#~)
  :: (ex :~> (name :! t), KnownValue t)
  => ex -> Label name
  -> Expr t
(#~) = flip unName

construct
  :: ( InstrConstructC dt, KnownValue dt
     , RMap (ConstructorFieldTypes dt)
     , fields ~ Rec Expr (ConstructorFieldTypes dt)
     , RecFromTuple fields
     )
  => IsoRecTuple fields -> Expr dt
construct = Construct . recFromTuple

constructRec
  :: ( InstrConstructC dt
     , RMap (ConstructorFieldTypes dt)
     , KnownValue dt
     )
  => Rec Expr (ConstructorFieldTypes dt)
  -> Expr dt
constructRec = Construct

----------------------------------------------------------------------------
-- Contract
----------------------------------------------------------------------------

contract
  :: ( NiceParameterFull p
     , NoExplicitDefaultEntrypoint p
     , ToTAddress p addr
     , ToT addr ~ ToT Address
     , exAddr :~> addr
     )
  => exAddr -> Expr (Maybe (ContractRef p))
contract = Contract

self
  :: ( NiceParameterFull p
     , NoExplicitDefaultEntrypoint p
     )
  => Expr (ContractRef p)
self = Self

contractAddress :: (exc :~> ContractRef p) => exc -> Expr Address
contractAddress = ContractAddress

contractCallingUnsafe
  :: ( NiceParameter arg
     , exAddr :~> Address
     )
  => EpName -> exAddr -> Expr (Maybe (ContractRef arg))
contractCallingUnsafe = ContractCallingUnsafe

contractCallingString
  :: ( NiceParameter arg
     , exAddr :~> Address
     )
  => MText -> exAddr -> Expr (Maybe (ContractRef arg))
contractCallingString =
    contractCallingUnsafe
  . unsafeBuildEpName
  . unMText

runFutureContract
  :: ( NiceParameter p
     , conExpr :~> FutureContract p
     )
  => conExpr -> Expr (Maybe (ContractRef p))
runFutureContract = RunFutureContract

implicitAccount
  :: (exkh :~> KeyHash)
  => exkh
  -> Expr (ContractRef ())
implicitAccount = ImplicitAccount

convertEpAddressToContract
  :: ( NiceParameter p
     , epExpr :~> EpAddress
     )
  => epExpr -> Expr (Maybe (ContractRef p))
convertEpAddressToContract = ConvertEpAddressToContract

makeView
  :: ( KnownValue (View a r)
     , exa :~> a
     , exCRef :~> ContractRef r
     )
  => exa -> exCRef -> Expr (View a r)
makeView = MakeView

makeVoid
  :: ( KnownValue (Void_ a b)
     , exa :~> a
     , exCRef :~> Lambda b b
     )
  => exa -> exCRef -> Expr (Void_ a b)
makeVoid = MakeVoid

----------------------------------------------------------------------------
-- Auxiliary
----------------------------------------------------------------------------

now :: Expr Timestamp
now = Now

amount :: Expr Mutez
amount = Amount

sender :: Expr Address
sender = Sender

checkSignature
  :: ( pkExpr :~> PublicKey
     , sigExpr :~> Signature
     , hashExpr :~> ByteString
     )
  => pkExpr -> sigExpr -> hashExpr
  -> Expr Bool
checkSignature = CheckSignature

sha256 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
sha256 = Sha256

sha512 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
sha512 = Sha512

blake2b :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
blake2b = Blake2b

hashKey :: (keyExpr :~> PublicKey) => keyExpr -> Expr KeyHash
hashKey = HashKey

chainId :: Expr ChainId
chainId = ChainId

balance :: Expr Mutez
balance = Balance