From MetaRocq.Template Require Import All.
From ConCert.Embedding.Extraction Require Import PreludeExt.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Extraction Require Import Common.
From ConCert.Extraction Require CameLIGOPretty.
From ConCert.Extraction Require CameLIGOExtract.
From ConCert.Examples.StackInterpreter Require Import StackInterpreterExtract.
From Stdlib Require Import ZArith.
Local Open Scope string_scope.
Import MonadNotation.
Import Interpreter.

Module CameLIGOInterp.

  Import CameLIGOExtract CameLIGOPretty.
  #[local]
  Existing Instance PrintConfShortNames.PrintWithShortNames.

  Definition init (setup : unit)
                  : result storage Error :=
    (* prevents optimizations from removing unused setup. TODO: override masks instead *)
    let setup0 := setup in
    Ok [].

  Definition receive_ (c : Chain)
                      (ctx : ContractCallContext)
                      (s : storage)
                      (msg : option params)
                      : result (list action * storage) Error :=
    (* prevent optimizations from deleting these arguments from receive_'s type signature *)
    let c_ := c in
    let ctx_ := ctx in
    match msg with
    | Some msg => receive msg s
    | None => Err default_error
    end.

  Definition TT_remap_ligo : list (kername * string) :=
    [ (* remapping types *)
        remap <%% Z %%> "int"
      ; remap <%% bool %%> "bool"
      ; remap <%% unit %%> "unit"
      ; remap <%% option %%> "option"
      ; remap <%% Amount %%> "tez"
      ; remap <%% address_rocq %%> "address"
      ; remap <%% time_rocq %%> "timestamp"
      ; remap <%% list %%> "list"
      ; remap <%% String.string %%> "string"
      ; remap <%% ext_map %%> (print_finmap_type "string * int" "value")
      ; remap <%% action %%> "operation"
      (* remapping operations *)
      ; remap <%% Z.add %%> "addInt"
      ; remap <%% Z.mul %%> "multInt"
      ; remap <%% Z.sub %%> "subInt"
      ; remap <%% Z.eqb %%> "eqInt"
      ; remap <%% Z.leb %%> "leInt"
      ; remap <%% Z.ltb %%> "ltInt"
      ; remap <%% @lookup %%> "Map.find_opt"
      ; remap <%% @fst %%> "fst"
      ; remap <%% @snd %%> "snd"
      ; remap <%% andb %%> "andb"
      ; remap <%% one %%> "1"
    ].

  Definition LIGO_INTERP_MODULE : CameLIGOMod params ContractCallContext unit storage action Error :=
    {| (* a name for the definition with the extracted code *)
       lmd_module_name := "cameligo_interp" ;

       (* definitions of operations on ints, bools, pairs, ect. *)
       lmd_prelude := CameLIGOPrelude;

       lmd_init := init ;

       lmd_init_prelude := "";
       lmd_receive_prelude := "";

       lmd_receive := receive_ ;

       (* code for the entry point *)
       lmd_entry_point :=
         CameLIGOPretty.printMain "receive_" "params" "value list"
    |}.

End CameLIGOInterp.