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

module GUI.GUICompilationFeaturesPaper 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.GUIFeaturesPart2Paper

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 : StateMachine S)(s : S) → GUIObj {i} (sm s .view)
  stateMachine2Method S sm s m = sm s .handleUserInput m >>=' λ sNEW →
                               return (compileToGUI S sm sNEW)

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

compileToGUI' : ∀{i} {S : Set}(sm : StateMachine 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 : StateMachine S)(s : S) → NativeIO Unit
compileGUI S sm s =
  createWindowFFI native>>= λ win →
  GUI.GUICompilation.compileRegularGUI win (compileToGUI S sm s)

compileGUI' : {S : Set}(sm : StateMachine S)(s : S) → NativeIO Unit
compileGUI' {S} =  compileGUI 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)
--
compileStateMachine :  {S : Set} (sm : StateMachine S) (s : S)
                   → NativeIO Unit
compileStateMachine {S} sm s =
         compileGUI S sm s

{-

compileFeatureVM : {BaseSt : Set}
                   (vm : FeatureMachine 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 : FeatureMachine BaseSt)
                   (f : vm .Features)
                   (s : State vm)
                    → GUI
compileFeatureVMToGUI {BaseSt} vm f s = compileToGUI (BaseSt ⊎ vm .AddStateF) (λ s → (vm .GUIF f) s) s
-}