(* Open Source License *)
(* Copyright (c) 2021 Nomadic Labs. <contact@nomadic-labs.com> *)

(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)

(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)

(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)

Require Import String.

Definition ep_approve : string :=
  "{ SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     CAR ;
     SWAP ;
     DUP ;
     DUG 2 ;
     CAR ;
     SENDER ;
     PAIR ;
     PUSH nat 0 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     CDR ;
     COMPARE ;
     GT ;
     PUSH nat 0 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     COMPARE ;
     GT ;
     AND ;
     IF { PUSH string ""UnsafeAllowanceChange"" ;
          FAILWITH }
        {  } ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     CDR ;
     CDR ;
     DIG 2 ;
     DIG 3 ;
     CDR ;
     PUSH nat 0 ;
     SWAP ;
     DUP ;
     DUG 2 ;
     COMPARE ;
     EQ ;
     IF { DROP ;
          NONE nat }
        { SOME } ;
     DIG 3 ;
     UPDATE ;
     PAIR ;
     SWAP ;
     CAR ;
     PAIR ;
     NIL operation ;
     PAIR }".

Definition ep_transfer : string :=
  "{ SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     CAR ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CAR ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CAR ;
     SENDER ;
     COMPARE ;
     EQ ;
     IF { SWAP }
        { SENDER ;
          DIG 3 ;
          DUP ;
          DUG 4 ;
          CAR ;
          PAIR ;
          DIG 3 ;
          DUP ;
          DUG 4 ;
          CDR ;
          CDR ;
          DIG 3 ;
          DUP ;
          DUG 4 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          GET ;
          IF_NONE { PUSH nat 0 }
                  {  } ;
          SUB ;
          ISNAT ;
          IF_NONE { PUSH string ""NotEnoughAllowance"" ;
                    FAILWITH }
                  {  } ;
          DIG 3 ;
          PUSH nat 0 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          COMPARE ;
          EQ ;
          IF { SWAP ;
               DROP ;
               NONE nat }
             { SWAP ;
               SOME } ;
          DIG 2 ;
          UPDATE } ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CDR ;
     CDR ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     CAR ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     SUB ;
     ISNAT ;
     IF_NONE { PUSH string ""NotEnoughBalance"" ;
               FAILWITH }
             {  } ;
     DIG 2 ;
     PUSH nat 0 ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     COMPARE ;
     EQ ;
     IF { SWAP ;
          DROP ;
          NONE nat }
        { SWAP ;
          SOME } ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     CAR ;
     UPDATE ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CDR ;
     CDR ;
     SWAP ;
     DUP ;
     DUG 2 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     CDR ;
     CAR ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     ADD ;
     SWAP ;
     PUSH nat 0 ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     COMPARE ;
     EQ ;
     IF { SWAP ;
          DROP ;
          NONE nat }
        { SWAP ;
          SOME } ;
     DIG 3 ;
     CDR ;
     CAR ;
     UPDATE ;
     DIG 2 ;
     CDR ;
     SWAP ;
     PAIR ;
     DUP ;
     CDR ;
     CDR ;
     DIG 2 ;
     PAIR ;
     SWAP ;
     CAR ;
     PAIR ;
     NIL operation ;
     PAIR }".

Definition ep_getAllowance : string :=
  "{ SWAP ;
     DUP ;
     DIG 2 ;
     NIL operation ;
     SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     PUSH mutez 0 ;
     DIG 4 ;
     CDR ;
     CAR ;
     DIG 4 ;
     CAR ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     TRANSFER_TOKENS ;
     CONS ;
     PAIR }".

Definition ep_getBalance : string :=
  "{ SWAP ;
     DUP ;
     DIG 2 ;
     NIL operation ;
     SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     PUSH mutez 0 ;
     DIG 4 ;
     CAR ;
     DIG 4 ;
     CAR ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     TRANSFER_TOKENS ;
     CONS ;
     PAIR }".

Definition ep_getTotalSupply : string :=
  "{ SWAP ;
     DUP ;
     DIG 2 ;
     NIL operation ;
     SWAP ;
     CDR ;
     PUSH mutez 0 ;
     DIG 3 ;
     CDR ;
     CDR ;
     CDR ;
     TRANSFER_TOKENS ;
     CONS ;
     PAIR }".

Definition ep_mintOrBurn : string :=
  "{ SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     CDR ;
     CAR ;
     SENDER ;
     COMPARE ;
     NEQ ;
     IF { PUSH string ""OnlyAdmin"" ;
          FAILWITH }
        {  } ;
     DUP ;
     CAR ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CAR ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     CDR ;
     GET ;
     IF_NONE { PUSH nat 0 }
             {  } ;
     ADD ;
     ISNAT ;
     IF_NONE { PUSH string ""Cannot burn more than the target's balance."" ;
               FAILWITH }
             {  } ;
     SWAP ;
     DUP ;
     DUG 2 ;
     CAR ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     CDR ;
     CDR ;
     CDR ;
     ADD ;
     ABS ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     CDR ;
     DIG 4 ;
     CAR ;
     PUSH nat 0 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     COMPARE ;
     EQ ;
     IF { DIG 3 ;
          DROP ;
          NONE nat }
        { DIG 3 ;
          SOME } ;
     DIG 4 ;
     CDR ;
     UPDATE ;
     PAIR ;
     DUP ;
     DUG 2 ;
     CDR ;
     CDR ;
     CAR ;
     PAIR ;
     SWAP ;
     DUP ;
     DUG 2 ;
     CDR ;
     CAR ;
     PAIR ;
     SWAP ;
     CAR ;
     PAIR ;
     NIL operation ;
     PAIR }".

Definition contract : string :=
  "{ parameter (or (or (or (pair %approve (address %spender) (nat %value))
                           (pair %getAllowance (pair %request (address %owner) (address %spender)) (contract %callback nat)))
                       (or (pair %getBalance (address %owner) (contract %callback nat))
                           (pair %getTotalSupply (unit %request) (contract %callback nat))))
                   (or (pair %mintOrBurn (int %quantity) (address %target))
                       (pair %transfer (address %from) (pair (address %to) (nat %value))))) ;
     storage (pair (big_map %tokens address nat)
                   (pair (big_map %allowances (pair (address %owner) (address %spender)) nat)
                         (pair (address %admin) (nat %total_supply)))) ;
     code { DUP ;
            CDR ;
            PUSH mutez 0 ;
            AMOUNT ;
            COMPARE ;
            NEQ ;
            IF { PUSH string ""DontSendTez"" ;
                 FAILWITH } {  } ;
            SWAP ;
            CAR ;
            IF_LEFT { IF_LEFT { IF_LEFT " ++ ep_approve
                                          ++ ep_getAllowance ++ " }
                              { IF_LEFT " ++ ep_getBalance
                                          ++ ep_getTotalSupply ++ " } }
                    { IF_LEFT " ++ ep_mintOrBurn
                                ++ ep_transfer ++ " } } }".