Library ConCert.Examples.ExchangeBuggy.ExchangeBuggyPrinters

From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Serializable.
#[warnings="-notation-incompatible-prefix"]
From ConCert.Execution.Test Require Import QCTest.
From ConCert.Examples.FA2 Require Import FA2Token.
From ConCert.Examples.FA2 Require Export FA2Printers.
From ConCert.Examples.ExchangeBuggy Require Import ExchangeBuggy.

Local Open Scope string_scope.

#[export]
Instance showExchangeExchangeParam : Show ExchangeBuggy.exchange_param :=
{|
  show t := "exchange{"
          ++ "exchange_owner: " ++ show t.(exchange_owner) ++ sep
          ++ "exchange_token_id: " ++ show t.(exchange_token_id) ++ sep
          ++ "tokens_sold: " ++ show t.(tokens_sold)
          ++ "}"
|}.

#[export]
Instance showExchangeMsgMsg : Show ExchangeBuggy.ExchangeMsg :=
{|
  show m :=
    match m with
    | tokens_to_asset param =>
        "token_to_asset " ++ show param
    | add_to_tokens_reserve tokenid =>
        "add_to_tokens_reserve (token_id=" ++ show tokenid ++ ")"
    end
|}.

#[export]
Instance showExchangeMsg : Show ExchangeBuggy.Msg :=
{|
  show m := show m
|}.

#[export]
Instance showExchangeState : Show ExchangeBuggy.State :=
{|
  show t := "ExchangeState{"
          ++ "fa2_caddr: " ++ show t.(fa2_caddr) ++ sep
          ++ "ongoing_exchanges: " ++ show t.(ongoing_exchanges)
          ++ "}"
|}.

#[export]
Instance showExchangeSetup : Show ExchangeBuggy.Setup :=
{|
  show t := "ExchangeSetup{"
          ++ "fa2_caddr_: " ++ show t.(fa2_caddr_)
          ++ "}"
|}.

#[export]
Instance showSerializedMsg : Show SerializedValue :=
  Derive Show Msg <
    FA2Token.Msg,
    ExchangeBuggy.Msg,
    FA2LegacyInterface.fa2_token_sender,
    FA2Token.Setup,
    ExchangeBuggy.Setup,
    unit >.