TypePrototype.hs

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import qualified Data.ByteString as B
import qualified Data.Text as T
import Data.Map (Map)
import Data.Set (Set)
import Data.Natural (Natural)
import Data.Int (Int64)
import Data.Time.Clock (UTCTime)
import Data.Proxy (Proxy(..))
import Data.Vinyl (Rec(..))

data T =
    T_c CT
  | T_key
  | T_unit
  | T_signature
  | T_option T
  | T_list T
  | T_set CT
  | T_operation
  | T_contract T
  | T_pair T T
  | T_or T T
  | T_lambda T T
  | T_map CT T
  | T_big_map CT T

data CT =
    T_int
  | T_nat
  | T_string
  | T_bytes
  | T_mutez
  | T_bool
  | T_key_hash
  | T_timestamp
  | T_address
  deriving (Eq, Show)

-- TODO use concrete types
type KeyHash = B.ByteString
type Address = B.ByteString
type Key = B.ByteString
type Signature = B.ByteString

data CVal t where
  CvInt       :: Integer -> CVal 'T_int
  CvNat       :: Natural -> CVal 'T_nat
  CvString    :: T.Text -> CVal 'T_string
  CvBytes     :: B.ByteString -> CVal 'T_bytes
  CvMutez     :: Int64 -> CVal 'T_mutez
  CvBool      :: Bool -> CVal 'T_bool
  CvKeyHash   :: KeyHash -> CVal 'T_key_hash
  CvTimestamp :: UTCTime -> CVal 'T_timestamp
  CvAddress   :: Address -> CVal 'T_address

deriving instance Show (CVal t)

-- | Representation of Michelson value.
--
-- Type parameter @op@ states for intrinsic operations.
-- Type parameter @ref@ states for big map reference (as big map is
-- normally not fully loaded into memory).
-- produced by some instructions, returned within a list by contract
-- and executed by system after the contract.
data Val op t where
  VC :: CVal t -> Val op ('T_c t)
  VKey :: Key -> Val op 'T_key
  VUnit :: Val op 'T_unit
  VSignature :: Signature -> Val op 'T_signature
  VOption :: Maybe (Val op t) -> Val op ('T_option t)
  VList :: [Val op t] -> Val op ('T_list t)
  VSet :: Set (CVal t) -> Val op ('T_set t)
  VOp :: op -> Val op 'T_operation
  VContract :: Address -> Val op ('T_contract p)
  VPair :: (Val op l, Val op r) -> Val op ('T_pair l r)
  VOr :: Either (Val op l) (Val op r) -> Val op ('T_or l r)
  VLam :: Instr op (inp ': '[]) (out ': '[]) -> Val op ('T_lambda inp out)
  VMap :: Map (CVal k) (Val op v) -> Val op ('T_map k v)
--  VBigMap :: BigMap op ref k v -> Val op ('T_big_map k v)

deriving instance Show op => Show (Val op t)

-- data ValueOp v
--     = New v
--     | Upd v
--     | Rem
--     | NotExisted
--
-- data BigMap op ref k v = BigMap { bmRef :: ref k v, bmChanges :: Map (CVal k) (ValueOp (Val op v)) }

-- | @myInstr@ is an equivalent to Michelson code:
--
--    PUSH int 223;
--    SOME;
--    IF_NONE DUP SWAP;
--    ADD
myInstr =
  PUSH (VC $ CvInt 223) #
  SOME #
  IF_NONE DUP SWAP #
  ADD #
  PUSH (VC $ CvNat 12) #
  ADD

-- | @myInstr2@ can not be represented in Michelson
-- syntax as Michelson has no way to directly push value
-- of type "option int"
myInstr2 =
  PUSH (VOption $ Just $ VC $ CvInt 223) #
  IF_NONE DUP Nop

(#) :: Instr op a b -> Instr op b c -> Instr op a c
(#) = Seq

infixl 0 #

class ArithOp op (n :: CT) (m :: CT) where
  type ArithResT op n m :: CT
  evalOp :: proxy op -> CVal n -> CVal m -> CVal (ArithResT op n m)

data Add

instance ArithOp Add 'T_nat 'T_int where
  type ArithResT Add 'T_nat 'T_int = 'T_int
  evalOp _ (CvNat i) (CvInt j) = CvInt (toInteger i + j)
instance ArithOp Add 'T_int 'T_nat where
  type ArithResT Add 'T_int 'T_nat = 'T_int
  evalOp _ (CvInt i) (CvNat j) = CvInt (i + toInteger j)
instance ArithOp Add 'T_nat 'T_nat where
  type ArithResT Add 'T_nat 'T_nat = 'T_nat
  evalOp _ (CvNat i) (CvNat j) = CvNat (i + j)
instance ArithOp Add 'T_int 'T_int where
  type ArithResT Add 'T_int 'T_int = 'T_int
  evalOp _ (CvInt i) (CvInt j) = CvInt (i + j)

-- TODO support add operation for mutez
-- don't forget to throw arith exception (async exception)

data Instr op (inp :: [T]) (out :: [T]) where
  Seq :: Instr op a b -> Instr op b c -> Instr op a c
  Nop :: Instr op s s -- Added to parse construction like  `IF {} { SWAP; }`

  DROP :: Instr op (a ': s) s
  DUP  :: Instr op (a ': s) (a ': a ': s)
  SWAP :: Instr op (a ': b ': s) (b ': a ': s)
  PUSH :: forall t s op. Val op t -> Instr op s (t ': s)
  SOME :: Instr op (a ': s) ('T_option a ': s)
  NONE :: forall a s op. Instr op s ('T_option a ': s)
  UNIT :: Instr op s ('T_unit ': s)
  IF_NONE :: Instr op s (b ': s) -> Instr op (a ': s) (b ': s) -> Instr op ('T_option a ': s) (b ': s)
  PAIR :: Instr op (a ': b ': s) ('T_pair a b ': s)
  -- CAR               VarNote FieldNote
  -- CDR               VarNote FieldNote
  -- LEFT              TypeNote VarNote FieldNote FieldNote Type
  -- RIGHT             TypeNote VarNote FieldNote FieldNote Type
  -- IF_LEFT           [op] [op]
  -- IF_RIGHT          [op] [op]
  -- NIL               TypeNote VarNote Type
  -- CONS              VarNote
  -- IF_CONS           [op] [op]
  -- SIZE              VarNote
  -- EMPTY_SET         TypeNote VarNote Comparable
  -- EMPTY_MAP         TypeNote VarNote Comparable Type
  -- MAP               VarNote [op]
  -- ITER              VarNote [op]
  -- MEM               VarNote
  -- GET               VarNote
  -- UPDATE
  -- IF                [op] [op]
  -- LOOP              [op]
  -- LOOP_LEFT         [op]
  -- LAMBDA            VarNote Type Type [op]
  -- EXEC              VarNote
  -- DIP               [op]
  -- FAILWITH
  -- CAST              TypeNote VarNote
  -- RENAME            VarNote
  -- PACK              VarNote
  -- UNPACK            VarNote Type
  -- CONCAT            VarNote
  -- SLICE             VarNote
  -- ISNAT
  ADD :: ArithOp Add n m => Instr op ('T_c n ': 'T_c m ': s) ('T_c (ArithResT Add n m) ': s)
  -- SUB               VarNote
  -- MUL               VarNote
  -- EDIV              VarNote
  -- ABS               VarNote
  -- NEG
  -- MOD
  -- LSL               VarNote
  -- LSR               VarNote
  -- OR                VarNote
  -- AND               VarNote
  -- XOR               VarNote
  -- NOT               VarNote
  -- COMPARE           VarNote
  -- EQ                VarNote
  -- NEQ               VarNote
  -- LT                VarNote
  -- GT                VarNote
  -- LE                VarNote
  -- GE                VarNote
  -- INT               VarNote
  -- SELF              VarNote
  -- CONTRACT          Type
  TRANSFER_TOKENS :: Instr op (p ': 'T_c 'T_mutez ': 'T_contract p ': s) ('T_operation ': s)
  -- SET_DELEGATE
  -- CREATE_ACCOUNT    VarNote VarNote
  -- CREATE_CONTRACT   VarNote VarNote
  -- CREATE_CONTRACT2  VarNote VarNote (Contract op)
  -- IMPLICIT_ACCOUNT  VarNote
  -- NOW               VarNote
  -- AMOUNT            VarNote
  -- BALANCE           VarNote
  -- CHECK_SIGNATURE   VarNote
  -- SHA256            VarNote
  -- SHA512            VarNote
  -- BLAKE2B           VarNote
  -- HASH_KEY          VarNote
  -- STEPS_TO_QUOTA    VarNot e
  -- SOURCE            VarNote
  -- SENDER            VarNote
  -- ADDRESS           VarNote

deriving instance Show op => Show (Instr op inp out)

data Operation where
  TransferTokens :: Show p => p -> Int64 -> Address -> Operation

deriving instance Show Operation

run :: Instr Operation inp out -> Rec (Val Operation) inp -> Rec (Val Operation) out
run (Seq i1 i2) r = run i2 (run i1 r)
run Nop r = r
run DROP (_ :& r) = r
run DUP (a :& r) = a :& a :& r
run SWAP (a :& b :& r) = b :& a :& r
run (PUSH v) r = v :& r
run SOME (a :& r) = VOption (Just a) :& r
run NONE r = VOption Nothing :& r
run UNIT r = VUnit :& r
run (IF_NONE bNone bJust) (VOption m :& r) = maybe (run bNone r) (run bJust . (:& r)) m
run PAIR (a :& b :& r) = VPair (a, b) :& r
-- More here
run ADD (VC l :& VC r :& rest) = VC (evalOp (Proxy @Add) l r) :& rest
-- More here
run TRANSFER_TOKENS (p :& VC (CvMutez mutez) :& VContract addr :& r) = VOp (TransferTokens p mutez addr) :& r

myInstrEvaluated :: Rec (Val Operation) '[ 'T_c 'T_int ]
myInstrEvaluated = run myInstr (VC (CvInt 90) :& RNil)