module GUI.Vers1.GUIExampleLib where

open import Data.String
open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Bool
open import Data.Nat

open import Data.Product
open import Function

open import NativeIO
open import Size
open import SizedIO.Base using (IOInterface; Command; Response; IO; return)
open import SizedIO.Console using (consoleI; translateIOConsole)
open import StateSizedIO.GUI.BaseStateDependent
open import GUI.Vers1.GUIDefinitionsBase
open import GUI.Vers1.GUIDefinitions
open import GUI.Vers1.RasterificFFI
open import heap.libraryVec

open import SizedIO.Base
open import SizedIO.Console using (putStrLn)

Button : Set
Button = GUIel frameCmpStruc button

Label : Set
Label = GUIel frameCmpStruc label

Textbox : Set
Textbox = GUIel frameCmpStruc textbox
--

createButton : String  Button
createButton str = createCmp {_}{button} str

createLabel : String  Label
createLabel str = createCmp {_}{label} str

-- should be a text box which a pre filled in value
createTextboxStr : String  Textbox
createTextboxStr str = createCmp {_}{textbox} str

-- should be a text box which has empty input initially (the default)
createTextbox : Textbox
createTextbox = createCmp {_}{textbox} ""


addButtonCmp : Button  Frame  Frame
addButtonCmp bt fr = addCmp fr buttonIdx bt

-- \GUIExampleLib
emptyFrame  :  Frame
addButton   :  String  Frame  Frame
addLabel    :  String  Frame  Frame
addTextbox  :  Frame  Frame


addButton str fr = addCmp fr buttonIdx (createButton str)


addLabel str fr = addCmp fr labelIdx (createLabel str)

addTextbox fr = addCmp fr textboxIdx createTextbox


--
emptyFrame = createCmp tt

buttonStr : String  Frame
buttonStr str = addButton str emptyFrame

onebuttonStrGUI : {i : Size}  String  GUI {i}  GUI { i}
onebuttonStrGUI str f .gui = buttonStr str
onebuttonStrGUI str f .obj .method m = returnGUI f






endEventGUI : String  GUI {}
endEventGUI str .gui = addLabel str emptyFrame
endEventGUI str .obj .method ()

xorGUI : List (String × GUI {})  GUI {}
xorGUI [] .gui = emptyFrame
xorGUI [] .obj .method ()
xorGUI ((str , g)  l) .gui = addButton str (xorGUI l .gui)
xorGUI ((str , g)  l) .obj .method (zero , _) = returnGUI g
xorGUI ((str , g)  l) .obj .method (suc m , x) = xorGUI l .obj .method (m , x)


multiTextboxFrame : (n : )  Tuple String n  Frame
multiTextboxFrame 0 v = emptyFrame
multiTextboxFrame 1 str = addLabel str (addTextbox (addButton "Continue" emptyFrame))
multiTextboxFrame (suc (suc n)) (str , v) =
                  addLabel str
                  (addTextbox
                  (multiTextboxFrame (suc n) v  ))


{-
multiTextboxFrame : (n : ℕ) → Tuple String n → Frame
multiTextboxFrame 0 v = emptyFrame
multiTextboxFrame 1 str = addTextbox (addLabel str (addButton "Continue" emptyFrame))
multiTextboxFrame (suc (suc n)) (str , v) =
                  addTextbox
                  (addLabel str
                  (multiTextboxFrame (suc n) v  ))
-}
{-
test : IO {!!} {!!} {!!}
test = {!!}
-}

multiTextboxHandler : {i : Size}(n k : ) (v : Tuple String n)
                      (f : Tuple String n  Tuple String k  GUI {i})
                       Tuple String k
                       FrameObj { i} (multiTextboxFrame n v)
multiTextboxHandler 0 k v f v' .method (() , _)
multiTextboxHandler 1 k v f v' .method ( _ ,  str ) .force =
   exec' (putStrLn "Handler is activated >>") λ _  returnGUI (f  str v' )
   --returnGUI (f  str v' )
multiTextboxHandler (suc (suc n)) k (str , v) f v' .method ( l  , m) =
            multiTextboxHandler (suc n) (suc k) v
              v''  λ v'''  f (headTuple m , v'')
                                 (tailTuple {String} v''') )
             (consVec {String} (headTuple m)  v')
             .method (l , tailTuple {String}  m)


multiTextboxGUI : ∀{i}  (n : )  (v : Tuple String n)  (f : Tuple String n  GUI {i}) 
  GUI { i}
multiTextboxGUI n v f .gui = multiTextboxFrame n v
multiTextboxGUI n v f .obj = multiTextboxHandler n 0 v  v _  f v) _