-- 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 storage operations (@MEM@, @GET@, @UPDATE@)
--      - @!@ 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
  , packRaw, unpackRaw

  -- * 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

  -- * Storages
  , stGet, stUpdate, stInsert, stInsertNew, stDelete, stMem
  , (#@), (!@), (+@), (++@), (-@), (?@)

  -- * 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.Constraint ((\\))
import Data.Vinyl.Core (RMap(..), RecordToList (..))
import Fmt (Buildable)

import Indigo.Internal.Expr.Types
import Indigo.Internal.Field
import Indigo.Internal.Var (Var)
import Indigo.Lorentz hiding (forcedCoerce)
import Indigo.Prelude
import Michelson.Text (unMText)
import qualified Michelson.Typed.Arith as M
import Michelson.Typed.Haskell.Instr.Sum (CtorOnlyField, InstrUnwrapC, InstrWrapOneC)
import Michelson.Untyped.Entrypoints (unsafeBuildEpName)
import Util.TypeTuple

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

constExpr :: forall a . NiceConstant a => a -> Expr a
constExpr a = C a \\ niceConstantEvi @a

-- | 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 (Packed a)
pack = Pack . toExpr

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

packRaw :: (ex :~> a, NicePackedValue a) => ex -> Expr ByteString
packRaw = PackRaw . toExpr

unpackRaw :: (NiceUnpackedValue a, exb :~> ByteString) => exb -> Expr (Maybe a)
unpackRaw = UnpackRaw . 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

----------------------------------------------------------------------------
-- Storages
----------------------------------------------------------------------------

infixr 8 #@
stGet, (#@)
  :: ( StoreHasSubmap store name key value
     , KnownValue value
     , exKey   :~> key
     , exStore :~> store
     )
  => exStore -> (Label name, exKey)
  -> Expr (Maybe value)
stGet store (uName, key) = StGet uName (toExpr key) (toExpr store)
(#@) = stGet

infixl 8 !@
stUpdate, (!@)
  :: ( StoreHasSubmap store name key value
     , exKey   :~> key
     , exVal   :~> Maybe value
     , exStore :~> store
     )
  => exStore -> (Label name, exKey, exVal)
  -> Expr store
stUpdate store (uName, key, val) =
  StUpdate uName (toExpr key) (toExpr val) (toExpr store)
(!@) = stUpdate

infixr 8 +@
stInsert, (+@)
  :: ( StoreHasSubmap store name key value
     , exKey   :~> key
     , exVal   :~> value
     , exStore :~> store
     )
  => exStore -> (Label name, exKey, exVal)
  -> Expr store
stInsert store (uName, key, val) =
  StInsert uName (toExpr key) (toExpr val) (toExpr store)
(+@) = stInsert

infixr 8 ++@
stInsertNew, (++@)
  :: ( StoreHasSubmap store name key value
     , IsError err
     , Buildable err
     , exKey   :~> key
     , exVal   :~> value
     , exStore :~> store
     )
  => exStore
  -> (Label name, err, exKey, exVal)
  -> Expr store
stInsertNew store (uName, err, key, val) =
  StInsertNew uName err (toExpr key) (toExpr val) (toExpr store)
(++@) = stInsertNew

infixl 8 -@
stDelete, (-@)
  :: ( StoreHasSubmap store name key value
     , KnownValue value
     , exKey   :~> key
     , exStore :~> store
     )
  => exStore -> (Label name, exKey)
  -> Expr store
stDelete store (uName, key) = StDelete uName (toExpr key) (toExpr store)
(-@) = stDelete

infixl 8 ?@
stMem, (?@)
  :: ( StoreHasSubmap store name key value
     , KnownValue value
     , exKey   :~> key
     , exStore :~> store
     )
  => exStore -> (Label name, exKey)
  -> Expr Bool
stMem store (uName, key) = StMem uName (toExpr key) (toExpr store)
(?@) = stMem

----------------------------------------------------------------------------
-- 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)
     , RecordToList (ConstructorFieldTypes dt)
     , fields ~ Rec Expr (ConstructorFieldTypes dt)
     , RecFromTuple fields
     )
  => IsoRecTuple fields -> Expr dt
construct = Construct Proxy. recFromTuple

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

----------------------------------------------------------------------------
-- 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 :~> TSignature bs
     , hashExpr :~> bs
     , BytesLike bs
     )
  => pkExpr -> sigExpr -> hashExpr
  -> Expr Bool
checkSignature pk sig hash = CheckSignature (toExpr pk) (toExpr sig) (toExpr hash)

sha256 :: (hashExpr :~> bs, BytesLike bs) => hashExpr -> Expr (Hash Sha256 bs)
sha256 = Sha256 . toExpr

sha512 :: (hashExpr :~> bs, BytesLike bs) => hashExpr -> Expr (Hash Sha512 bs)
sha512 = Sha512 . toExpr

blake2b :: (hashExpr :~> bs, BytesLike bs) => hashExpr -> Expr (Hash Blake2b bs)
blake2b = Blake2b . toExpr

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

chainId :: Expr ChainId
chainId = ChainId

balance :: Expr Mutez
balance = Balance