module GUI.GUIFeaturesPart3 where

open import Size
open import Function

open import Data.Unit
open import Data.Sum
open import Data.Product

open import NativeIO
open import SizedIO.Base renaming (IO to IO∞; IO' to IO) hiding (_>>=_ ; _>>_ ; return)
open import SizedIO.Console using (consoleI)
open import StateSizedIO.GUI.BaseStateDependent


--
-- This is the main code about the Feature Machines:
--
open import GUI.GUIFeatures hiding (base)
open import GUI.GUIFeaturesPart2

open import GUI.GUIDefinitions

open import GUI.GUICompilationFeatures using (compileFeatureVM)




lift⊎3  : {A B C : Set} → A ⊎ B → A ⊎ B ⊎ C
lift⊎3 (inj₁ x) = inj₁ x
lift⊎3 (inj₂ y) = inj₂ (inj₁ y)


mapStateMachineHandl : {S S' : Set}(f : S → S')
                       (p : IO consoleI ∞ S)
                       → IO consoleI ∞ S'
mapStateMachineHandl f p = mapIO' f p


mapSMachineState : {S S' : Set}(f : S → S')(sm : SMachineState S)
                    → SMachineState S'
mapSMachineState f sm .fSM = sm .fSM
mapSMachineState f sm .handlSM m = mapStateMachineHandl f (sm .handlSM m)



mapFMachineHandle : {A B C : Set}
                          (a : A ⊎ B)(sm : SMachineState (A ⊎ B))
                          → SMachineState (A ⊎ B ⊎ C) {-(lift⊎3 a)-}
mapFMachineHandle a sm = mapSMachineState lift⊎3 {-a-} sm

mapIOFeatureM : {A B C : Set}
            → IO consoleI ∞ (A ⊎ B)
            → IO consoleI ∞ (A ⊎ B ⊎ C)
mapIOFeatureM p = mapIO' lift⊎3 p


Cancel : FMachine StateV → FMachine StateV
Cancel vm .Features = vm .Features × FeatureCancel
Cancel vm .AddStateF  = vm .AddStateF ⊎ ⊤
Cancel vm .GUIF (f , yesCancel) (inj₁ s1) =
      addBtn2StateMachine (mapFMachineHandle (inj₁ s1) (vm .GUIF f (inj₁ s1)))
                          "Cancel" ((inj₂ (inj₂ _)))
Cancel vm .GUIF (f , _) (inj₁ s) = mapFMachineHandle (inj₁ s) (vm .GUIF f (inj₁ s))
Cancel vm .GUIF (f , _) (inj₂ (inj₁ x)) = mapFMachineHandle (inj₂ x) (vm .GUIF f (inj₂ x))

-- neuer Zustand
-- nachfolge Zustand s0
Cancel vm .GUIF (f , _) (inj₂ (inj₂ _)) = simpleSMState "Intermediate" (inj₁ s0)



Tea : FMachine StateV → FMachine StateV
Tea vm .Features = vm .Features × FeatureTea
Tea vm .AddStateF  = vm .AddStateF ⊎ ⊤
Tea vm .GUIF (f , yeTea) (inj₁ s2) =
      addBtn2StateMachine (mapFMachineHandle (inj₁ s2) (vm .GUIF f (inj₁ s2)))
                          "Tea" (inj₂ (inj₂ _))
Tea vm .GUIF (f , _) (inj₁ s) = mapFMachineHandle (inj₁ s) (vm .GUIF f (inj₁ s))
Tea vm .GUIF (f , _) (inj₂ (inj₁ x)) = mapFMachineHandle (inj₂ x) (vm .GUIF f (inj₂ x))
Tea vm .GUIF (f , _) (inj₂ (inj₂ _)) = simpleSMState "Get Your Tea" (inj₁ s0)


cancelBase : FMachine StateV
cancelBase = Cancel base

teaCancelBase : FMachine StateV
teaCancelBase = Tea cancelBase


--
--  NOTE: strange behaviour is correct!
--        there is no 'serve soda' state in GUIFeaturesPart2.
--        Therefore the after 'soda' is chosen, we jump back to 'payP
--

main1 : NativeIO Unit
main1 =
   nativePutStrLn "Note: strange behaviour, there is no 'serve soda' state, but only 'serve tea'." native>>= λ _ →
   compileFeatureVM cancelBase (_ , yesCancel) {-((_ , noCancel) , yesTea)-} (inj₁ s0) --

main2 : NativeIO Unit
main2 =
  nativePutStrLn "\n\n ====\n Note: strange behaviour, there is no 'serve soda' state, but only 'serve tea'." native>>= λ _ →
  compileFeatureVM teaCancelBase ((_ , noCancel) , yesTea) (inj₁ s0) --


main = main2