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, coerce, forcedCoerce

  -- * 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
  , (#@), (!@), (+@), (++@), (-@), (?@)

  -- * Sum types
  , wrap, unwrap

  -- * 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 hiding (forcedCoerce)
import Indigo.Prelude
import qualified Michelson.Typed.Arith as M
import Util.TypeTuple
import Michelson.Text (unMText)
import Michelson.Typed.Haskell.Instr.Sum (CtorOnlyField, InstrUnwrapC, InstrWrapOneC)
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 . toExpr

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

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

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

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

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

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

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

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

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

infix 4 ==
eq, (==)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
eq a b = Eq' (toExpr a) (toExpr b)
(==) = eq

infix 4 /=
neq, (/=)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
neq a b = Neq (toExpr a) (toExpr b)
(/=) = neq

infix 4 <
lt, (<)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
lt a b = Lt (toExpr a) (toExpr b)
(<) = lt

infix 4 >
gt, (>)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
gt a b = Gt (toExpr a) (toExpr b)
(>) = gt

infix 4 <=
le, (<=)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
le a b = Le (toExpr a) (toExpr b)
(<=) = le

infix 4 >=
ge, (>=)
  :: (NiceComparable n, c :~> n, c1 :~> n)
  => c -> c1
  -> Expr Bool
ge a b = Ge (toExpr a) (toExpr b)
(>=) = ge

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

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

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

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

-- | Convert between types that have the same Michelson representation and an
-- explicit permission for that in the face of 'CanCastTo' constraint.
coerce :: forall b a ex. (Castable_ a b, KnownValue b, ex :~> a) => ex -> Expr b
coerce = Coerce . toExpr

-- | Convert between expressions of types that have the same Michelson
-- representation.
forcedCoerce
  :: forall b a ex. (MichelsonCoercible a b, KnownValue b, ex :~> a)
  => ex -> Expr b
forcedCoerce = ForcedCoerce . toExpr

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

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

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

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

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

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

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

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

pack :: (ex :~> a, NicePackedValue a) => ex -> Expr ByteString
pack = Pack . toExpr

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

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

pair :: (ex1 :~> n, ex2 :~> m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)
pair a b = Pair (toExpr a) (toExpr b)

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

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

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

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

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' . toExpr

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

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

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

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

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

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

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

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 (k, some v) c

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

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

-- | 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 (k, none) c

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

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

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

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

mem
  :: IsMemExpr exKey exN n
  => exKey -> exN
  -> Expr Bool
mem key n = Mem (toExpr key) (toExpr n)

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

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 (toExpr key) (toExpr 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 (toExpr key) (toExpr val) (toExpr 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 (toExpr key) (toExpr val) (toExpr 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 (toExpr key) (toExpr val) (toExpr 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 (toExpr key) (toExpr 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 (toExpr key) (toExpr store)
(?@) = uMem

----------------------------------------------------------------------------
-- Sum types
----------------------------------------------------------------------------

wrap
  :: ( InstrWrapOneC dt name
     , exField :~> CtorOnlyField name dt
     , KnownValue dt
     )
  => Label name
  -> exField
  -> Expr dt
wrap l = Wrap l . toExpr

unwrap
  :: ( InstrUnwrapC dt name
     , exDt :~> dt
     , KnownValue (CtorOnlyField name dt)
     )
  => Label name
  -> exDt
  -> Expr (CtorOnlyField name dt)
unwrap l = Unwrap l . toExpr

----------------------------------------------------------------------------
-- 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 lName = Name lName . toExpr

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

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

-- TODO: we should try to make this have a set of 'IsExpr' as input instead of 'Expr'
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 . toExpr

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

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

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

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 . toExpr

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

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

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

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

----------------------------------------------------------------------------
-- 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 pk sig hash = CheckSignature (toExpr pk) (toExpr sig) (toExpr hash)

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

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

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

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

chainId :: Expr ChainId
chainId = ChainId

balance :: Expr Mutez
balance = Balance