{-# OPTIONS --allow-unsolved-metas #-}

module GUI.Vers1.GUICompilation where

open import Data.String renaming (_++_ to _++Str_)
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.Nat.Show renaming (show to showNat)
open import Data.Maybe.Base

open import Data.Product
open import Function

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.GUIExampleLib

open import GUI.Vers1.RasterificFFI -- hiding (main)

open import NativeIO renaming (nativeReturn to return;
                               _native>>=_ to _>>=_;
                               _native>>_ to _>>_)

open import GUI.Vers1.GUIExampleTest
open import heap.libraryVec

open import GUI.Debug

maxFin : (n : )  Fin (suc n)
maxFin zero = zero
maxFin (suc n) = suc (maxFin n)

embed : {n : }  Fin n  Fin (suc n)
embed {zero} ()
embed {suc n} zero = zero
embed {suc n} (suc m) = suc (embed m)

-- not needed here but useful to add to library
predFin : {n : }  Fin n  Fin n
predFin {zero} ()
predFin {suc n} zero = zero
predFin {suc n} (suc m) = embed m

invertFin : {n : }(k :  Fin n)  Fin n
invertFin {zero} ()
invertFin {suc n} zero = maxFin n
invertFin {suc n} (suc k) = embed (invertFin k)

liftFinN : {A : Set}  (n : )  (Fin n  A)  A  (  A)
liftFinN zero f a m    = a
liftFinN (suc n) f a zero = f zero
liftFinN (suc n) f a (suc m) = liftFinN n (f  suc) a m

liftStringList : {A : Set}  (n : )  (Tuple String n  A)  A  (List String  A)
liftStringList zero f a l = f _
liftStringList (suc n) f a [] = a
liftStringList (suc zero) f a (x  l) = f x
liftStringList (suc (suc n)) f a (x  l) = liftStringList (suc n)  y  f (x , y)) a l
{- liftStringList n (λ x → f (a , x)) a l -}

liftFinNStringList : {A : Set}  (n m : )  (Fin n  Tuple String m  A)  A  (  List String  A)
liftFinNStringList {A} n m f a = liftFinN n  k  liftStringList m (f k) a)  v  a)

  triggerHsLoop : SDLWindow  GUI  (  List String  NativeIO GUI)  NativeIO Unit
  triggerHsLoop win (guic gui obj) f =
    nativePutStrLn "beginning of triggerHsLoop function" >>= λ _ 

    getEventsFFI win gui >>=  λ {
    (n , listStr)  f n listStr >>= λ gui    
       nativePutStrLn (showNat "triggerHsLoop" n) >> compile win gui 

-- \GUICompilation
  compile : SDLWindow  GUI  NativeIO Unit
  compile win (guic gui obj) =
         nativePutStrLn "beginning of compile function" >>= λ _ 
         renderFrameToScreenFFI win gui >>= λ _ 
         triggerHsLoop win (guic gui obj)  n s 
         (debug ((translateIOConsole (liftFinNStringList
                             (guiEl2NrButtons frameCmpStruc frame gui)
                             (guiEl2NrTextboxes frameCmpStruc frame gui)

                             -- If buttons are wrongly displayed, then check here and wether invertFin n' is needed or not
                             -- (λ n' s → obj .method ((invertFin n') , s))
                              n' s  obj .method (debug (invertFin n') (showNat "n' object method call" (toℕ  n')) , s))
                             (SizedIO.Base.return (gui , obj)) n s))
         >>= λ {
                  (gui' , obj')  return (guic gui' obj') }) "debug translateIOConsole"))

-- Main

main : NativeIO Unit
main = do
  win <- createWindowFFI
  compile win (guic threeBtnGUI obj3Btn)
  nativePutStrLn "hello Agda"