module GUI.GUIExampleBankAccount   where


open import SizedIO.Base hiding (_>>=_)
open import SizedIO.Console hiding (main)
open import Size
open import Data.String hiding (show)
open import Data.Nat renaming (_∸_ to _-_)
open import Data.Fin hiding (_-_)
open import Data.Bool
open import Data.Product
open import GUI.GUIDefinitions
open import GUI.GUIExampleLib
open import GUI.GUIExample
open import NativeIO renaming (nativeReturn to return;
                               _native>>=_ to _>>=_;
                               _native>>_ to _>>_)
open import GUI.GUICompilation hiding (main)
open import GUI.RasterificFFI

open import Data.Nat.Show
open import heap.libraryNat renaming (_≧ℕb_ to _≧_)




{-
guifullToReturnType : ∀ {i} {g} → GUI {i} → returnType g
guifullToReturnType f = changedGUI (f .defFrame) (f .property)

guifullToReturnType' : ∀ {i} {g} → GUI {i} →
                       Σ[ r ∈ returnType g ]
                       (IOObjectˢ GuiInterface handlerInterface i
                           (nextStateFrame g r))
guifullToReturnType' {i} {g} f = guifullToReturnType f , f .obj
-}

{-
changeGUI : ∀ {i} {g} → GUI {i} →
                       IO GuiInterface ∞ (Σ[ r ∈ returnType g ]
                       (IOObjectˢ GuiInterface handlerInterface i
                           (nextStateFrame g r)))
changeGUI  f = return (guifullToReturnType' f)
-}

threeBtnFrame : (s s' s'' : String) → Frame
threeBtnFrame s s'  s'' = addButton s  (addButton s'
                             (addButton s'' emptyFrame))

test = _-_

mutual
 atm :  ∀{i} → ℕ → GUI {i}
 atm n .gui  = addButton  "Withdraw 10"
               (addButton  "Withdraw 1"
               (addButton  "Refresh"
               (addLabel(show n) emptyFrame)))
 atm n .method (zero , str) = if n ≧ 10  then  return' (atm (n - 10))
                              else  return' (invalid n)
 atm n .method (suc zero , str) = if n ≧ 1  then  return' (atm (n - 1))
                              else  return' (invalid n)
 atm n .method (suc (suc zero) , str) = return' (atm 55)
 atm n .method (suc (suc (suc ())) , str)

 invalid : ∀{i} → ℕ → GUI {i}
 invalid n .gui =
     addButton "Not enough money" emptyFrame
 invalid n .method m  =  return' (atm n)




main : NativeIO Unit
main = do
  win <- createWindowFFI
  compile win (atm 55)