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

module GUI.GUIFeaturesPart2 where



open import Size
open import Data.Product
open import Data.Sum renaming (inj₁ to state; inj₂ to extendedState)
open import Data.Empty
open import Data.Unit
open import Data.Fin
open import Data.Nat.Base


open import heap.libraryVec

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

open import GUI.GUIDefinitions using (Frame; FrameMethod; addButton; emptyFrame)
open import GUI.GUIFeatures hiding (base)


{-   *** STATE MACHINES  **** -}

sMachineHdl : (S : Set)(f  : Frame) → Set
sMachineHdl S f =  (m : FrameMethod f) → IO consoleI ∞ S

record SMachineState (S : Set) : Set where 
  field
    fSM     : Frame
    handlSM : sMachineHdl S fSM

SMachine : Set → Set
SMachine S = (s : S) → SMachineState S

open SMachineState public


{-  **************** FEATURE MACHINE **** -}

-- an example of a feature machine wihout additional states:

record FeatureVMVers1 : Set₁ where 
  field
    Features  : Set
    State     : Set
    GUIF      : (f : Features) → SMachine State


record FMachine (BaseSt : Set) : Set₁ where 
  field  
     Features : Set
     AddStateF : Set
     GUIF      : (f : Features) → SMachine (BaseSt ⊎ AddStateF) 
  State : Set
  State =  BaseSt ⊎ AddStateF 

open FMachine public


simpleSMState : {S : Set}
                (btnStr : String)
                (end : S)
                → SMachineState S -- start
simpleSMState btnStr end .fSM = addButton btnStr emptyFrame
simpleSMState btnStr end .handlSM m  = return' end




--
-- STEPHAN: This was once the place of an error, where I wrote formerly '99.9% correct'
-- but there was an error
--

addBtn2StateMachine : {S : Set}(sm : SMachineState S)
                      (btnStr : String)(end : S)
                      → SMachineState S
addBtn2StateMachine sm btnStr end .fSM = addButton btnStr (sm .fSM)
addBtn2StateMachine sm btnStr end .handlSM (zero , string) = return' end  --NEW BUTTON
addBtn2StateMachine {_} sm btnStr end .handlSM (suc btnNum , string) =
  sm .handlSM (btnNum , string)



base : FMachine StateV
base .Features     = ⊤
base .AddStateF    = ⊥
base .GUIF f (state s0)     = simpleSMState "1 Euro" (state s1)
base .GUIF f (state s1)   = simpleSMState "Get Change" (state s2)
base .GUIF f (state s2)        = simpleSMState "Soda" (state s0)
base .GUIF f (extendedState ())