Library ConCert.Examples.Escrow.extraction.EscrowRust

From ConCert.Extraction Require Import Common.
From ConCert.Extraction Require Import ConcordiumExtract.
From ConCert.Examples.Escrow Require Import Escrow.
From Stdlib Require Import Bool.
From Stdlib Require Import String.
From MetaRocq.Template Require Import All.

Definition ESCROW_MODULE : ConcordiumMod _ _ :=
  {| concmd_contract_name := "escrow"%bs;
     concmd_init := @Escrow.init;
     concmd_receive := @Escrow.receive;
     concmd_extra := []; |}.

Definition should_inline kn :=
  eq_kername kn <%% @Monad.bind %%>
  || eq_kername kn <%% OptionMonad.Monad_option %%>
  || eq_kername kn <%% @ConCert.Execution.ResultMonad.Monad_result %%>
  || if String.index 0 "setter_from_getter" (string_of_kername kn) then true else false.

(* NOTE: it is important to declare a printing config, otherwise MetaRocq evaluation tries to normalize a term with an unresolved instance and runs out of memory. *)
#[local]
Existing Instance DefaultPrintConfig.RustConfig.

Redirect "concordium-extract/escrow.rs"
MetaRocq Run (concordium_extraction
               ESCROW_MODULE
               (ConcordiumRemap.build_remaps
                  (ConcordiumRemap.remap_Z_arith
                     ++ ConcordiumRemap.remap_nat_arith
                     ++ ConcordiumRemap.remap_blockchain_consts)
                  ConcordiumRemap.remap_inline_bool_ops
                  (ConcordiumRemap.remap_std_types
                     ++ ConcordiumRemap.remap_blockchain_inductives))
               should_inline).