(* 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 :=
  "{ DUP ;
     CAR ;
     SENDER ;
     COMPARE ;
     EQ ;
     IF { DROP }
        { SWAP ;
          DUP ;
          CAR ;
          SENDER ;
          GET ;
          IF_NONE { EMPTY_MAP address nat ;
                    PUSH nat 0 ;
                    PAIR }
                  {  } ;
          DUP ;
          CDR ;
          DIP 3 { DUP } ;
          DIG 3 ;
          CAR ;
          GET ;
          IF_NONE {  }
                  { INT ;
                    EQ ;
                    IF {  }
                       { DIP 2 { DUP } ;
                         DIG 2 ;
                         CDR ;
                         INT ;
                         EQ ;
                         IF {  }
                            { PUSH string ""UnsafeAllowanceChange"" ;
                              FAILWITH } } } ;
          DUP ;
          CDR ;
          DIG 3 ;
          DUP ;
          CAR ;
          DIP { CDR ;
                SOME } ;
          UPDATE ;
          DIP { DUP ;
                DIP { CAR } ;
                CDR } ;
          SWAP ;
          DROP ;
          SWAP ;
          PAIR ;
          DIP { DUP ;
                CAR } ;
          SOME ;
          SENDER ;
          UPDATE ;
          DIP { DUP ;
                DIP { CDR } ;
                CAR } ;
          SWAP ;
          DROP ;
          PAIR } ;
     NIL operation ;
     PAIR }".

Definition ep_transfer : string :=
  "{ DUP ;
     CAR ;
     DIP { SWAP } ;
     DIP { DUP ;
           CAR } ;
     GET ;
     IF_NONE { PUSH string ""NotEnoughBalance"" ;
               FAILWITH }
             {  } ;
     DIP 2 { DUP } ;
     DIG 2 ;
     CAR ;
     SENDER ;
     COMPARE ;
     EQ ;
     IF {  }
        { DUP ;
          CDR ;
          SENDER ;
          GET ;
          IF_NONE { PUSH string ""NotEnoughAllowance"" ;
                    FAILWITH }
                  {  } ;
          DIP { DIP 2 { DUP } ;
                DIG 2 ;
                CDR ;
                CDR ;
                DUP } ;
          DUP ;
          DIP { COMPARE ;
                GE ;
                IF {  }
                   { PUSH string ""NotEnoughAllowance"" ;
                     FAILWITH } } ;
          SUB ;
          DUP ;
          PUSH int 0 ;
          COMPARE ;
          LE ;
          IF { ABS }
             { PUSH string ""Allowance - value is negative. This should not happen."" ;
               FAILWITH } ;
          DIP { DUP ;
                CDR } ;
          SOME ;
          SENDER ;
          UPDATE ;
          DIP { DUP ;
                DIP { CAR } ;
                CDR } ;
          SWAP ;
          DROP ;
          SWAP ;
          PAIR } ;
     DUP ;
     CAR ;
     DIP 3 { DUP } ;
     DIG 3 ;
     CDR ;
     CDR ;
     COMPARE ;
     LE ;
     IF {  }
        { PUSH string ""NotEnoughBalance"" ;
          FAILWITH } ;
     DIP 2 { DUP } ;
     DIG 2 ;
     CDR ;
     CDR ;
     DIP { DUP ;
           CAR } ;
     SWAP ;
     SUB ;
     DUP ;
     PUSH int 0 ;
     COMPARE ;
     LE ;
     IF { ABS }
        { PUSH string ""Owner's balance - value is negative. This should not happen."" ;
          FAILWITH } ;
     DIP { DUP ;
           DIP { CDR } ;
           CAR } ;
     SWAP ;
     DROP ;
     PAIR ;
     SOME ;
     DIP { DUP ;
           CAR } ;
     DIP 3 { DUP } ;
     DIG 3 ;
     CAR ;
     UPDATE ;
     DIP { DUP ;
           DIP { CDR } ;
           CAR } ;
     SWAP ;
     DROP ;
     PAIR ;
     DUP ;
     CAR ;
     DIP 2 { DUP } ;
     DIG 2 ;
     CDR ;
     CAR ;
     GET ;
     IF_NONE { SWAP ;
               DUP ;
               CDR ;
               CDR ;
               DIP { EMPTY_MAP address nat } ;
               PAIR ;
               SOME ;
               SWAP ;
               CDR ;
               CAR ;
               DIP { DIP { DUP ;
                           CAR } } ;
               UPDATE ;
               DIP { DUP ;
                     DIP { CDR } ;
                     CAR } ;
               SWAP ;
               DROP ;
               PAIR }
             { DUP ;
               CAR ;
               DIP 3 { DUP } ;
               DIG 3 ;
               CDR ;
               CDR ;
               ADD ;
               DIP { DUP ;
                     DIP { CDR } ;
                     CAR } ;
               SWAP ;
               DROP ;
               PAIR ;
               SOME ;
               DIP { DUP ;
                     CAR } ;
               DIG 3 ;
               CDR ;
               CAR ;
               UPDATE ;
               DIP { DUP ;
                     DIP { CDR } ;
                     CAR } ;
               SWAP ;
               DROP ;
               PAIR } ;
     NIL operation ;
     PAIR }".

Definition ep_getTotalSupply : string :=
  "{ CDR ;
     AMOUNT ;
     DIP 2 { DUP } ;
     DIG 2 ;
     CDR ;
     TRANSFER_TOKENS ;
     DIP { NIL operation } ;
     CONS ;
     PAIR }".

Definition ep_getBalance : string :=
  "{ DUP ;
     CAR ;
     DIP { SWAP } ;
     DIP { DUP ;
           CAR } ;
     GET ;
     IF_NONE { PUSH string ""NotEnoughBalance"" ;
               FAILWITH }
             {  } ;
     CAR ;
     DIP { SWAP ;
           CDR ;
           AMOUNT } ;
     TRANSFER_TOKENS ;
     DIP { NIL operation } ;
     CONS ;
     PAIR }".

Definition ep_getAllowance : string :=
  "{ DUP ;
     CAR ;
     CAR ;
     DIP { SWAP } ;
     DIP { DUP ;
           CAR } ;
     GET ;
     IF_NONE { PUSH string ""NotEnoughBalance"" ;
               FAILWITH }
             {  } ;
     CDR ;
     DIP 2 { DUP } ;
     DIG 2 ;
     CAR ;
     CDR ;
     GET ;
     IF_NONE { PUSH string ""spender does not have an approval for this owner."" ;
               FAILWITH }
             {  } ;
     DIP { SWAP ;
           CDR ;
           AMOUNT } ;
     TRANSFER_TOKENS ;
     DIP { NIL operation } ;
     CONS ;
     PAIR }".

Definition contract : string :=
  "parameter (or (or (pair %approve (address :spender) (nat :value))
                     (pair %transfer (address :owner) (pair (address :to) (nat :value))))
                 (or (pair %getAllowance (pair :ownerSpender (address :owner) (address :spender)) (contract :contr nat))
                     (or (pair %getBalance (address :owner) (contract :contr nat))
                         (pair %getTotalSupply (unit :unit) (contract :contr nat))))) ;
   storage (pair (big_map %accounts address (pair (nat :balance) (map :approvals address nat))) (nat %fields)) ;
   code { CAST (pair (or (or (pair address nat) (pair address (pair address nat)))
                         (or (pair (pair address address) (contract nat))
                             (or (pair address (contract nat))
                                 (pair unit (contract nat)))))
               (pair (big_map address (pair nat (map address nat))) nat)) ;
          DUP ;
          CAR ;
          DIP { CDR } ;
          IF_LEFT { IF_LEFT " ++ ep_approve
                              ++ ep_transfer ++ " }
                  { IF_LEFT " ++ ep_getAllowance
                              ++ "{ IF_LEFT " ++ ep_getBalance
                                              ++ ep_getTotalSupply ++ " } } }".