Library ConCert.Examples.FA2.FA2Printers

From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution.Test Require Import QCTest.
From ConCert.Examples.FA2 Require Import FA2LegacyInterface.
From ConCert.Examples.FA2 Require Import FA2Token.
From ConCert.Examples.FA2 Require Import TestContracts.
Local Open Scope string_scope.

Arguments return_addr {_ _}.

#[export]
Instance showCallback {A : Type}: Show (FA2LegacyInterface.callback A) :=
{|
  show v := "return address: " ++ show v.(return_addr)
|}.

#[export]
Instance showFA2InterfaceTransferDestination : Show FA2LegacyInterface.transfer_destination :=
{|
  show t := "{"
            ++ "to_: " ++ show t.(to_) ++ sep
            ++ "dst_token_id: " ++ show t.(dst_token_id) ++ sep
            ++ "amount: " ++ show t.(amount) ++ sep
            ++ "}"
|}.

#[export]
Instance showFA2InterfaceTransfer : Show FA2LegacyInterface.transfer :=
{|
  show t := "{"
            ++ "from_: " ++ show t.(from_) ++ sep
            ++ "txs:" ++ show t.(txs) ++ sep
            ++ "callback: " ++ show t.(sender_callback_addr)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacebalance_of_request : Show FA2LegacyInterface.balance_of_request :=
{|
  show t := "balance_of_request{"
            ++ "owner: " ++ show t.(owner) ++ sep
            ++ "bal_req_token_id: " ++ show t.(bal_req_token_id)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacebalance_of_response : Show FA2LegacyInterface.balance_of_response :=
{|
  show t := "balance_of_response{"
            ++ "request: " ++ show t.(request) ++ sep
            ++ "balance: " ++ show t.(balance)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacebalance_of_param : Show FA2LegacyInterface.balance_of_param :=
{|
  show t := "balance_of_param{"
            ++ "bal_requests: " ++ show t.(bal_requests) ++ sep
            ++ "bal_callback: " ++ show t.(bal_callback)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetotal_supply_response : Show FA2LegacyInterface.total_supply_response :=
{|
  show t := "total_supply_response{"
            ++ "supply_resp_token_id: " ++ show t.(supply_resp_token_id) ++ sep
            ++ "total_supply: " ++ show t.(total_supply)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetotal_supply_param : Show FA2LegacyInterface.total_supply_param :=
{|
  show t := "total_supply_param{"
            ++ "supply_param_token_ids: " ++ show t.(supply_param_token_ids) ++ sep
            ++ "supply_param_callback: " ++ show t.(supply_param_callback)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetoken_metadata : Show FA2LegacyInterface.token_metadata :=
{|
  show t := "token_metadata{"
            ++ "metadata_token_id: " ++ show t.(metadata_token_id) ++ sep
            ++ "metadata_decimals: " ++ show t.(metadata_decimals)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetoken_metadata_param : Show FA2LegacyInterface.token_metadata_param :=
{|
  show t := "token_metadata_param{"
            ++ "metadata_token_ids: " ++ show t.(metadata_token_ids) ++ sep
            ++ "metadata_callback: " ++ show t.(metadata_callback)
            ++ "}"
|}.

#[export]
Instance showoperator_tokens : Show operator_tokens :=
{|
  show m := match m with
            | all_tokens => "all_tokens"
            | some_tokens token_ids => "some_tokens " ++ show token_ids
            end
|}.

#[export]
Instance showFA2Interfaceoperator_param : Show FA2LegacyInterface.operator_param :=
{|
  show t := "operator_param{"
            ++ "op_param_owner: " ++ show t.(op_param_owner) ++ sep
            ++ "op_param_operator: " ++ show t.(op_param_operator) ++ sep
            ++ "op_param_tokens: " ++ show t.(op_param_tokens) ++ sep
            ++ "}"
|}.

#[export]
Instance showupdate_operator : Show update_operator :=
{|
  show m := match m with
            | add_operator param => "add_operator " ++ show param
            | remove_operator param => "remove_operator " ++ show param
            end
|}.

#[export]
Instance showFA2Interfaceis_operator_response : Show FA2LegacyInterface.is_operator_response :=
{|
  show t := "is_operator_response{"
            ++ "operator: " ++ show t.(operator) ++ sep
            ++ "is_operator: " ++ show t.(is_operator)
            ++ "}"
|}.

#[export]
Instance showFA2Interfaceis_operator_param : Show FA2LegacyInterface.is_operator_param :=
{|
  show t := "is_operator_param{"
            ++ "is_operator_operator: " ++ show t.(is_operator_operator) ++ sep
            ++ "is_operator_callback: " ++ show t.(is_operator_callback)
            ++ "}"
|}.

#[export]
Instance showself_transfer_policy : Show self_transfer_policy :=
{|
  show m := match m with
            | self_transfer_permitted => "self_transfer_permitted "
            | self_transfer_denied => "self_transfer_denied "
            end
|}.

#[export]
Instance showoperator_transfer_policy : Show operator_transfer_policy :=
{|
  show m := match m with
            | operator_transfer_permitted => "operator_transfer_permitted "
            | operator_transfer_denied => "operator_transfer_denied "
            end
|}.

#[export]
Instance showowner_transfer_policy : Show owner_transfer_policy :=
{|
  show m := match m with
            | owner_no_op => "owner_no_op "
            | optional_owner_hook => "optional_owner_hook "
            | required_owner_hook => "required_owner_hook "
            end
|}.

#[export]
Instance showFA2Interfacepermissions_descriptor : Show FA2LegacyInterface.permissions_descriptor :=
{|
  show t := "permissions_descriptor{"
            ++ "descr_self: " ++ show t.(descr_self) ++ sep
            ++ "descr_operator: " ++ show t.(descr_operator) ++ sep
            ++ "descr_receiver: " ++ show t.(descr_receiver) ++ sep
            ++ "descr_sender: " ++ show t.(descr_sender) ++ sep
            ++ "descr_custom: " ++ show t.(descr_custom)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetransfer_destination_descriptor : Show FA2LegacyInterface.transfer_destination_descriptor :=
{|
  show t := "transfer_destination_descriptor{"
            ++ "transfer_dst_descr_to_: " ++ show t.(transfer_dst_descr_to_) ++ sep
            ++ "transfer_dst_descr_token_id: " ++ show t.(transfer_dst_descr_token_id) ++ sep
            ++ "transfer_dst_descr_amount: " ++ show t.(transfer_dst_descr_amount)
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetransfer_descriptor : Show FA2LegacyInterface.transfer_descriptor :=
{|
  show t := "transfer_descriptor{"
            ++ "transfer_descr_from_: " ++ show t.(transfer_descr_from_) ++ sep
            ++ "transfer_descr_txs: " ++ show t.(transfer_descr_txs) ++ sep
            ++ "}"
|}.

#[export]
Instance showFA2Interfacetransfer_descriptor_param : Show FA2LegacyInterface.transfer_descriptor_param :=
{|
  show t := "transfer_descriptor_param{"
            ++ "transfer_descr_fa2: " ++ show t.(transfer_descr_fa2) ++ sep
            ++ "transfer_descr_batch: " ++ show t.(transfer_descr_batch) ++ sep
            ++ "transfer_descr_operator: " ++ show t.(transfer_descr_operator)
            ++ "}"
|}.

#[export]
Instance showfa2_token_receiver : Show fa2_token_receiver :=
{|
  show m := match m with
            | tokens_received param => "tokens_received " ++ show param
            end
|}.

#[export]
Instance showfa2_token_sender : Show fa2_token_sender :=
{|
  show m := match m with
            | tokens_sent param => "tokens_sent " ++ show param
            end
|}.

#[export]
Instance showFA2Interfaceset_hook_param : Show FA2LegacyInterface.set_hook_param :=
{|
  show t := "set_hook_param{"
            ++ "hook_addr: " ++ show t.(hook_addr) ++ sep
            ++ "hook_permissions_descriptor: " ++ show t.(hook_permissions_descriptor)
            ++ "}"
|}.

#[export]
Instance showFA2ReceiverMsg {Msg : Type}
                           `{serMsg : Serializable Msg}
                           `{Show Msg}
                           : Show (@FA2ReceiverMsg _ Msg) :=
{|
  show m := match m with
            | receive_balance_of_param param => "receive_balance_of_param " ++ show param
            | receive_total_supply_param param => "receive_total_supply_param " ++ show param
            | receive_metadata_callback param => "receive_metadata_callback " ++ show param
            | receive_is_operator param => "receive_is_operator " ++ show param
            | receive_permissions_descriptor param => "receive_permissions_descriptor " ++ show param
            | other_msg msg => show msg
            end
|}.

#[export]
Instance showFA2TransferHook {Msg : Type}
                            `{serMsg : Serializable Msg}
                            `{Show Msg}
                             : Show (@FA2TransferHook _ Msg) :=
{|
  show m := match m with
            | transfer_hook param => "transferhook " ++ show param
            | hook_other_msg msg => show msg
            end
|}.

#[export]
Instance showFA2TokenMsg : Show FA2Token.Msg :=
{|
  show m := match m with
            | msg_transfer param => "transfer " ++ show param
            | msg_set_transfer_hook param => "set_transfer_hook " ++ show param
            | msg_balance_of param => "balance_of " ++ show param
            | msg_total_supply param => "total_supply " ++ show param
            | msg_token_metadata param => "token_metadata " ++ show param
            | msg_permissions_descriptor param => "permissions_descriptor " ++ show param
            | msg_update_operators param => "update_operators " ++ show param
            | msg_is_operator param => "is_operator " ++ show param
            | msg_receive_hook_transfer param => "receive_hook_transfer " ++ show param
            | msg_create_tokens tokenid => "create_tokens " ++ show tokenid
            end
|}.

#[export]
Instance showFA2TokenLedger : Show FA2Token.TokenLedger :=
{|
  show t := "Token_Ledger{"
            ++ "fungible: " ++ show t.(fungible) ++ sep
            ++ "balances: " ++ show t.(balances)
            ++ "}"
|}.

#[export]
Instance showFA2State : Show FA2Token.State :=
{|
  show t := "FA2TokenState{"
            ++ "fa2_owner: " ++ show t.(fa2_owner) ++ sep
            ++ "assets: " ++ show t.(assets) ++ sep
            ++ "operators: " ++ show t.(operators) ++ sep
            ++ "tokens_metadata: " ++ show t.(tokens) ++ sep
            ++ "transfer_hook: " ++ show t.(transfer_hook_addr) ++ sep
            ++ "permission_policy: " ++ show t.(permission_policy)
            ++ "}"
|}.

#[export]
Instance showFA2Setup : Show FA2Token.Setup :=
{|
  show t := "FA2TokenSetup{"
            ++ "setup_total_supply: " ++ show t.(setup_total_supply) ++ sep
            ++ "tokens_metadata: " ++ show t.(setup_tokens) ++ sep
            ++ "permission_policy: " ++ show t.(initial_permission_policy)
            ++ "}"
|}.

(* Printers for Test Contracts *)
#[export]
Instance showFA2ClientMsg : Show FA2ClientMsg :=
{|
  show m := match m with
            | Call_fa2_is_operator param => "Call_fa2_is_operator " ++ show param
            | Call_fa2_balance_of_param param => "Call_fa2_balance_of_param " ++ show param
            | Call_fa2_total_supply_param param => "Call_fa2_total_supply_param param " ++ show param
            | Call_fa2_metadata_callback param => "Call_fa2_metadata_callback param " ++ show param
            | Call_fa2_permissions_descriptor param => "Call_fa2_permissions_descriptor param " ++ show param
            end
|}.

#[export]
Instance showFA2ClientContractMsg : Show ClientMsg :=
{|
  show m := show m
|}.

#[export]
Instance showFA2ClientState : Show ClientState :=
{|
  show t := "FA2ClientState{"
            ++ "fa2_caddr: " ++ show t.(fa2_caddr) ++ sep
            ++ "bit: " ++ show t.(bit)
            ++ "}"
|}.

#[export]
Instance showFA2ClientSetup : Show ClientSetup :=
{|
  show t := "FA2ClientSetup{"
            ++ "fa2_caddr_: " ++ show t.(fa2_caddr_)
            ++ "}"
|}.

#[export]
Instance showFA2TransferHookMsg : Show FA2TransferHookMsg :=
{|
  show m := match m with
            | set_permission_policy param => "set_permission_policy " ++ show param
            end
|}.

#[export]
Instance showTransferHookMsg : Show TransferHookMsg :=
{|
  show m := show m
|}.

#[export]
Instance showFA2TransferHookContractState : Show HookState :=
{|
  show t := "FA2TransferHookState{"
            ++ "fa2_caddr: " ++ show t.(hook_fa2_caddr) ++ sep
            ++ "policy: " ++ show t.(hook_policy) ++ sep
            ++ "owner: " ++ show t.(hook_owner)
            ++ "}"
|}.

#[export]
Instance showFA2TransferHookContractSetup : Show HookSetup :=
{|
  show t := "FA2TransferHookSetup{"
            ++ "fa2_caddr_: " ++ show t.(hook_fa2_caddr_) ++ sep
            ++ "policy_: " ++ show t.(hook_policy_) ++ sep
            ++ "}"
|}.

#[export]
Instance showSerializedMsg : Show SerializedValue :=
  Derive Show Msg <
    FA2Token.Msg,
    TestContracts.ClientMsg,
    TestContracts.TransferHookMsg,
    FA2Token.Setup,
    TestContracts.ClientSetup,
    TestContracts.HookSetup >.