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

module GUI.GUICompilationFeatures where

open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Function

open import Size

open import SizedIO.Base renaming (IO to IO∞; IO' to IO) --hiding (_>>=_ ; _>>_ ; return)
open import SizedIO.Console using (consoleI; translateIOConsole; translateIOConsoleTODO)

open import heap.libraryVec using (Tuple)

open import GUI.Debug using (showNat)

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

--
-- This is the main code about the Feature Machines:
--
open import GUI.GUIFeaturesPart2

open import GUI.GUIDefinitions
open import GUI.RasterificFFI using (SDLWindow; getEventsFFI; renderFrameToScreenFFI; createWindowFFI)

import GUI.GUICompilation renaming (compile to compileRegularGUI)
mutual
  stateMachine2Method : ∀{i} (S : Set)(sm : SMachine S)(s : S) → GUIObj {i} (sm s .fSM)
  stateMachine2Method S sm s m = sm s .handlSM m >>=' λ sNEW →
                               return (compileToGUI S sm sNEW)

  compileToGUI : ∀{i} (S : Set)(sm : SMachine S)(s : S) → GUI {i}
  compileToGUI S sm s .gui    = sm s .fSM
  compileToGUI S sm s .method = stateMachine2Method S sm s

compileToGUI' : ∀{i} {S : Set}(sm : SMachine S)(s : S) → GUI {i}
compileToGUI' {i} {S} sm s = compileToGUI {i} S sm s



--
-- Compiling state machines to GUIs, then to IO program
--
compileGUI : (S : Set)(sm : SMachine S)(s : S) → NativeIO Unit
compileGUI S sm s =
  createWindowFFI native>>= λ win →
  GUI.GUICompilation.compileRegularGUI win (compileToGUI S sm s)


compileRegularGUI : (g : GUI) → NativeIO Unit
compileRegularGUI g =
  createWindowFFI native>>= λ win →
  GUI.GUICompilation.compileRegularGUI win g




--
-- Compiling FeatureMachines to GUIs, then to IO programs
--

-- (this function is a bit redundant)
--
compileSMachine :  {S : Set} (sm : SMachine S) (s : S)
                   → NativeIO Unit
compileSMachine {S} sm s =
         compileGUI S sm s


compileFeatureVM : {BaseSt : Set}
                   (vm : FMachine BaseSt)
                   (f : vm .Features)
                   (s : State vm)
                    → NativeIO Unit
compileFeatureVM {BaseSt} vm f s = compileGUI (BaseSt ⊎ vm .AddStateF) (λ s → (vm .GUIF f) s) s

compileFeatureVMToGUI : {BaseSt : Set}
                   (vm : FMachine BaseSt)
                   (f : vm .Features)
                   (s : State vm)
                    → GUI
compileFeatureVMToGUI {BaseSt} vm f s = compileToGUI (BaseSt ⊎ vm .AddStateF) (λ s → (vm .GUIF f) s) s