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.Dexter2 Require Import Dexter2CPMM.
From ConCert.Examples.Dexter2 Require Import Dexter2FA12.

Local Open Scope string_scope.

Module NullAddressLocalBlockcain <: NullAddress.
  Definition BaseTypes : ChainBase := LocalChainBase.
  Definition null_address := creator.
  Definition set_delegate_call := (fun _ : @baker_address BaseTypes => @nil (@ActionBody BaseTypes)).
  Lemma delegate_call : forall addr, List.Forall (fun action =>
      match action with
      | act_transfer _ _ => False
      | act_call _ _ _ => False
      | act_deploy _ _ _ => False
      end) (set_delegate_call addr).
  Proof.
    now unfold set_delegate_call.
  Qed.
End NullAddressLocalBlockcain.
Module DEX2 := Dexter2 DSInstances NullAddressLocalBlockcain.

#[export]
Instance showAddLiqduidityParam : Show add_liquidity_param :=
{|
  show p := "params{" ++
    "owner: " ++ show p.(owner) ++ sep ++
    "min lqt minted: " ++ show p.(minLqtMinted) ++ sep ++
    "max tokens deposited: " ++ show p.(maxTokensDeposited) ++ sep ++
    "deadline: " ++ show p.(add_deadline) ++ "}"
|}.

#[export]
Instance showRemoveLiqduidityParam : Show remove_liquidity_param :=
{|
  show p := "params{" ++
    "to: " ++ show p.(liquidity_to) ++ sep ++
    "lqt burned: " ++ show p.(lqtBurned) ++ sep ++
    "min xtz withdrawn: " ++ show p.(minXtzWithdrawn) ++ sep ++
    "min tokens withdrawn: " ++ show p.(minTokensWithdrawn) ++ sep ++
    "deadline: " ++ show p.(remove_deadline) ++ "}"
|}.

#[export]
Instance showXtzToTokenParam : Show xtz_to_token_param :=
{|
  show p := "params{" ++
    "to: " ++ show p.(tokens_to) ++ sep ++
    "min tokens bought: " ++ show p.(minTokensBought) ++ sep ++
    "deadline: " ++ show p.(xtt_deadline) ++ "}"
|}.

#[export]
Instance showTokenToXtzParam : Show token_to_xtz_param :=
{|
  show p := "params{" ++
    "to: " ++ show p.(xtz_to) ++ sep ++
    "tokens sold: " ++ show p.(tokensSold) ++ sep ++
    "min xtz bought: " ++ show p.(minXtzBought) ++ sep ++
    "deadline: " ++ show p.(ttx_deadline) ++ "}"
|}.

#[export]
Instance showSetBakerParam : Show set_baker_param :=
{|
  show p := "params{" ++
    "baker: " ++ show p.(baker) ++ sep ++
    "freeze: " ++ show p.(freezeBaker_) ++ "}"
|}.

#[export]
Instance showTokenToTokenParam : Show token_to_token_param :=
{|
  show p := "params{" ++
    "exchange address: " ++ show p.(outputDexterContract) ++ sep ++
    "to: " ++ show p.(to_) ++ sep ++
    "min tokens bought: " ++ show p.(minTokensBought_) ++ sep ++
    "tokens sold: " ++ show p.(tokensSold_) ++ sep ++
    "deadline: " ++ show p.(ttt_deadline) ++ "}"
|}.

#[export]
Instance showCPMMDexterMsg : Show DexterMsg :=
{|
  show m :=
    match m with
    | AddLiquidity param => "add_liquidity " ++ show param
    | RemoveLiquidity param => "remove_liquidity " ++ show param
    | XtzToToken param => "xtz_to_token " ++ show param
    | TokenToXtz param => "token_to_xtz " ++ show param
    | SetBaker param => "set_baker " ++ show param
    | SetManager addr => "set_manager " ++ show addr
    | SetLqtAddress addr => "set_lqt_address " ++ show addr
    | UpdateTokenPool => "update_token_pool"
    | TokenToToken param => "token_to_token " ++ show param
    end
|}.

#[export]
Instance showCPMMMsg : Show Dexter2CPMM.Msg :=
{|
  show m := show m
|}.

#[export]
Instance showCPMMSetup : Show Dexter2CPMM.Setup :=
{|
  show p := "Setup{" ++
    "lqt total: " ++ show p.(lqtTotal_) ++ sep ++
    "manager: " ++ show p.(manager_) ++ sep ++
    "token address: " ++ show p.(tokenAddress_) ++ sep ++
    "token Id: " ++ show p.(tokenId_) ++ "}"
|}.

#[export]
Instance showCPMMState : Show Dexter2CPMM.State :=
{|
  show p := "State{" ++
    "token pool: " ++ show p.(tokenPool) ++ sep ++
    "xtz pool: " ++ show p.(xtzPool) ++ sep ++
    "lqt pool: " ++ show p.(lqtTotal) ++ sep ++
    "is updating token pool: " ++ show p.(selfIsUpdatingTokenPool) ++ sep ++
    "baker frozen: " ++ show p.(freezeBaker) ++ sep ++
    "manager: " ++ show p.(manager) ++ sep ++
    "token address: " ++ show p.(tokenAddress) ++ sep ++
    "lqt address: " ++ show p.(lqtAddress) ++ sep ++
    "token Id: " ++ show p.(tokenId) ++ "}"
|}.

#[export]
Instance showLqtSetup : Show Dexter2FA12.Setup :=
{|
  show p := "Setup{" ++
    "admin: " ++ show p.(admin_) ++ sep ++
    "lqt provider: " ++ show p.(lqt_provider) ++ sep ++
    "initial pool: " ++ show p.(initial_pool) ++ "}"
|}.

#[export]
Instance showLqtState : Show Dexter2FA12.State :=
{|
  show p := "State{" ++
    "tokens: " ++ show p.(tokens) ++ sep ++
    "allowances: " ++ show p.(allowances) ++ sep ++
    "total supply: " ++ show p.(total_supply) ++ sep ++
    "admin: " ++ show p.(admin) ++ "}"
|}.

#[export]
Instance showTransferParam : Show transfer_param :=
{|
  show p := "params{" ++
    "from: " ++ show p.(from) ++ sep ++
    "to: " ++ show p.(to) ++ sep ++
    "value: " ++ show p.(value) ++ "}"
|}.

#[export]
Instance showApproveParam : Show approve_param :=
{|
  show p := "params{" ++
    "spender: " ++ show p.(spender) ++ sep ++
    "value: " ++ show p.(value_) ++ "}"
|}.

#[export]
Instance showMintOrBurnParam : Show mintOrBurn_param :=
{|
  show p := "params{" ++
    "quantity: " ++ show p.(quantity) ++ sep ++
    "target: " ++ show p.(target) ++ "}"
|}.

#[export]
Instance showGetAllowanceParam : Show getAllowance_param :=
{|
  show p := "params{" ++
    "request: " ++ show p.(request) ++ sep ++
    "callback addr: " ++ show p.(allowance_callback).(return_addr) ++ "}"
|}.

#[export]
Instance showGetBalanceParam : Show getBalance_param :=
{|
  show p := "params{" ++
    "owner: " ++ show p.(owner_) ++ sep ++
    "callback addr: " ++ show p.(balance_callback).(return_addr) ++ "}"
|}.

#[export]
Instance showGetTotalSupplyParam : Show getTotalSupply_param :=
{|
  show p := "params{" ++
    "callback addr: " ++ show p.(supply_callback).(return_addr) ++ "}"
|}.

#[export]
Instance showLqtMsg : Show Dexter2FA12.Msg :=
{|
  show m :=
    match m with
    | msg_transfer param => "transfer " ++ show param
    | msg_approve param => "approve " ++ show param
    | msg_mint_or_burn param => "mint_or_burn " ++ show param
    | msg_get_allowance param => "get_allowance " ++ show param
    | msg_get_balance param => "get_balance " ++ show param
    | msg_get_total_supply param => "get_total_supply " ++ show param
    end
|}.

#[export]
Instance showSerializedMsg : Show SerializedValue :=
  Derive Show Msg <
    FA2Token.Msg,
    Dexter2CPMM.Msg,
    Dexter2FA12.Msg,
    FA2Token.Setup,
    Dexter2CPMM.Setup,
    Dexter2FA12.Setup >.