Token.etiml

pragma etiml ^0.1

structure Pervasive = struct
  fun addBy b a = a + b
  fun subBy b a = a - b
  fun orBy b a = a || b
(* fun waste_time () = 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 *)
                                                                                              
(* fun for_ ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {i : Nat | start <= i /\ i < eend} using (m1, m1'), nat {i} * 'a -- m2, m2' --> 'a) return 'a using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52*32)*(eend-start)+50*32 = *)
(*   lets *)
(*     fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(*       ifi i #>= eend then (* waste_time (); *) acc *)
(*       else *)
(*         %loop (i #+ #1, %f (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(*       end *)
(*   in *)
(*     %loop (start, init) *)
(*   end *)
  
  fun require b = if b then (* waste_time ();  *)() else (throw using _) end
end

interface tokenRecipient = sig
  public fun receiveApproval (_from : address, _value : uint256, _token : address, _extraData : bytes)
end

contract TokenERC20 = struct

  (* Public variables of the token *)
  public state name : vector uint256
  public state symbol : vector uint256
         
  (* public val decimals = #18 *)
  public val decimals = #0
  (* 18 decimals is the strongly suggested default, avoid changing it *)
  public state totalSupply : cell uint256

  (* This creates an array with all balances *)
  public state balanceOf : map address uint256
  public state allowance : map address (map address uint256)

  (* This generates a public event on the blockchain that will notify clients *)
  event Transfer(indexed from : address, indexed to : address, value : uint256)

  (* This notifies clients about the amount burnt *)
  event Burn(indexed from : address, value : uint256)

(* (* PW: here is a limitation of TiML: it can't parametrize on states. MicroTiML actually supports it (for continuations), so TiML should support it too.  *)                               *)
(* fun for_name ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {j : Nat | start <= j /\ j < eend} using (m1, m1'), funtype pre {name : j} post {name : j+1} nat {j} * 'a -- m2, m2' --> 'a) pre {name : start} post {name : eend} return 'a (* using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52)*(eend-start)+50 *) = *)
(*   lets *)
(*     fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) pre {name : i} post {name : eend} (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(*       ifi i #>= eend then (* waste_time ();  *)acc asc_state {name : eend} *)
(*       else *)
(*         @loop {i+1} (i #+ #1, @f {i} (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(*       end *)
(*   in *)
(*     %loop (start, init) *)
(*   end *)
  
(*   fun copy_name {old len : Nat} (s : array uint256 {len}) pre {name : old} post {name : len} = *)
(*     vector_clear name; *)
(*     %for_name (#0, array_len s, (), fn {i | 0 <= i /\ i < len} (i : nat {i}, ()) pre {name : i} post {name : i+1} => *)
(*       push_back (name, array_get(s, i)) *)
(*     ) *)

(* fun for_symbol ['a] {m1 m2: Time} {m1' m2' start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {j : Nat | start <= j /\ j < eend} using (m1, m1'), funtype pre {symbol : j} post {symbol : j+1} nat {j} * 'a -- m2, m2' --> 'a) pre {symbol : start} post {symbol : eend} return 'a using (m1+m2+3281.0)*$(eend-start)+3970.0, (m1'+m2'+52*32)*(eend-start)+50*32 = *)
(*   lets *)
(*     fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) pre {symbol : i} post {symbol : eend} (* using (m1+m2) * $(eend-i), (m1'+m2') * (eend-i) *) = *)
(*       ifi i #>= eend then (* waste_time ();  *)acc asc_state {symbol : eend} *)
(*       else *)
(*         @loop {i+1} (i #+ #1, @f {i} (i, acc)) using (m1+m2+3281.0) * $(eend-i)+1651.0, (m1'+m2'+52*32) * (eend-i)+16*32 *)
(*       end *)
(*   in *)
(*     %loop (start, init) *)
(*   end *)
  
(*   fun copy_symbol {old len : Nat} (s : array uint256 {len}) pre {symbol : old} post {symbol : len} = *)
(*     vector_clear symbol; *)
(*     %for_symbol (#0, array_len s, (), fn {i | 0 <= i /\ i < len} (i : nat {i}, ()) pre {symbol : i} post {symbol : i+1} => *)
(*       push_back (symbol, array_get(s, i)) *)
(*     ) *)

  (**
   * Constructor function
   *
   * Initializes contract with initial supply tokens to the creator of the contract
   *)
  public fun constructor {old1 old2 len1 len2 : Nat} (
        initialSupply : uint256,
        tokenName : array uint256 {len1},
        tokenSymbol : array uint256 {len2}
    ) (* pre {name : old1, symbol : old2} post {name : len1, symbol : len2} *) = 
           totalSupply ::= initialSupply * ((10 #** decimals) using _);  (* Update total supply with the decimal amount *)
    set balanceOf[msg.sender] !!totalSupply                (* Give the creator all initial tokens *)
    (* %copy_name tokenName;                                   (* Set the name for display purposes *) *)
    (* %copy_symbol tokenSymbol                               (* Set the symbol for display purposes *) *)

  (** *)
  (*  * Internal transfer, only can be called by this contract *)
  (*  *)
  internal fun _transfer (_from : address, _to : address, _value : uint) using _ =
    (* Prevent transfer to 0x0 address. Use burn() instead *)
    require(1=1);
    require(_to <> 0x0);
    (* Check if the sender has enough *)
    require(balanceOf[_from] >= _value);
    (* Check for overflows *)
    require(balanceOf[_to] + _value > balanceOf[_to]);
    (* Save this for an assertion in the future *)
    let previousBalances = balanceOf[_from] + balanceOf[_to];
    (* Subtract from the sender *)
    modify balanceOf[_from] -= _value;
    (* Add the same to the recipient *)
    modify balanceOf[_to] += _value;
    (* emit Transfer(_from, _to, _value); *)
    (* Asserts are used to use static analysis to find bugs in your code. They should never fail *)
    require(balanceOf[_from] + balanceOf[_to] = previousBalances)
    
    (* (* (* assert2(balanceOf[_from] + balanceOf[_to] = previousBalances) *) *) *)
    (* assert2(1=1) *)

  (*  * Transfer tokens *)
  (*  * *)
  (*  * Send `_value` tokens to `_to` from your account *)
  (*  * *)
  (*  * @param _to The address of the recipient *)
  (*  * @param _value the amount to send *)
  public fun transfer (_to : address, _value : uint256) =
           _transfer(msg.sender, _to, _value)
    (* ; (_to, _value, msg.sender, balanceOf[msg.sender], balanceOf[_to]) *)

  (*  * Transfer tokens from other address *)
  (*  * *)
  (*  * Send `_value` tokens to `_to` on behalf of `_from` *)
  (*  * *)
  (*  * @param _from The address of the sender *)
  (*  * @param _to The address of the recipient *)
  (*  * @param _value the amount to send *)
  public fun transferFrom (_from : address, _to : address, _value : uint256) =
    require(_value <= allowance[_from][msg.sender]);     (* Check allowance *)
    modify allowance[_from][msg.sender] -= _value;
    _transfer(_from, _to, _value);
    true
    (* (_from, _to, _value, msg.sender, allowance[_from][msg.sender], balanceOf[_from], balanceOf[_to]) *)
      
  (*  * Set allowance for other address *)
  (*  * *)
  (*  * Allows `_spender` to spend no more than `_value` tokens on your behalf *)
  (*  * *)
  (*  * @param _spender The address authorized to spend *)
  (*  * @param _value the max amount they can spend *)
  public fun approve (_spender : address, _value : uint256) =
    set allowance[msg.sender][_spender] _value;
    true
    (* (msg.sender, _spender, _value, allowance[msg.sender][_spender]) *)
             
  (** *)
  (*  * Set allowance for other address and notify *)
  (*  * *)
  (*  * Allows `_spender` to spend no more than `_value` tokens on your behalf, and then ping the contract about it *)
  (*  * *)
  (*  * @param _spender The address authorized to spend *)
  (*  * @param _value the max amount they can spend *)
  (*  * @param _extraData some extra information to send to the approved contract *)
  (*  *)
  public fun approveAndCall (_spender : address, _value : uint256(* , _extraData : bytes *)) =
    let spender = attach _spender tokenRecipient;
    if approve(_spender, _value) then
      call spender receiveApproval(msg.sender, _value, this, _extraData);
      true
    else false end
    (* ; (msg.sender, _spender, _value, allowance[msg.sender][_spender]) *)

  (** *)
  (*  * Destroy tokens *)
  (*  * *)
  (*  * Remove `_value` tokens from the system irreversibly *)
  (*  * *)
  (*  * @param _value the amount of money to burn *)
  (*  *)
  public fun burn (_value : uint256) =
    require(balanceOf[msg.sender] >= _value);   (* Check if the sender has enough *)
    modify balanceOf[msg.sender] -= _value;            (* Subtract from the sender *)
    modify totalSupply -= _value;                      (* Updates totalSupply *)
    (* emit Burn(msg.sender, _value); *)
    true
    (* (msg.sender, _value, balanceOf[msg.sender], !!totalSupply) *)

  (** *)
  (*  * Destroy tokens from other account *)
  (*  * *)
  (*  * Remove `_value` tokens from the system irreversibly on behalf of `_from`. *)
  (*  * *)
  (*  * @param _from the address of the sender *)
  (*  * @param _value the amount of money to burn *)
  (*  *)
  public fun burnFrom (_from : address, _value : uint256) =
    require(balanceOf[_from] >= _value);                (* Check if the targeted balance is enough *)
    require(_value <= allowance[_from][msg.sender]);    (* Check allowance *)
    modify balanceOf[_from] -= _value;                         (* Subtract from the targeted balance *)
    modify allowance[_from][msg.sender] -= _value;             (* Subtract from the sender's allowance *)
    modify totalSupply -= _value;                              (* Update totalSupply *)
    (* emit Burn(_from, _value); *)
    true
    (* (msg.sender, _from, _value, balanceOf[_from], !!totalSupply, allowance[_from][msg.sender]) *)

  val () = %constructor (0xa0, {}, {})
  (* val _ = transfer (0x246, 0x80) *)
  (* val () = set allowance[0x246][0x8888] 0x50 *)
  (* val _ = transferFrom (0x246, 0x123, 0x20) *)
  (* val _ = burnFrom (0x246, 0x20) *)
  (* val _ = approve (0x123, 0x80) *)
  (* val _ = burn 0x20 *)
  (* val _ = approveAndCall (0x123, 0x80) *)
            
  (* val () = dispatch {transfer = transfer, *)
  (*                    transferFrom = transferFrom, *)
  (*                    approve = approve, *)
  (*                    approveAndCall = approveAndCall, *)
  (*                    burn = burn, *)
  (*                    burnFrom = burnFrom, *)
  (*                   } *)
                    
end