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

module GUI.GUIFeaturesPart2Paper where



open import Size
open import Data.Product
open import Data.Sum
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 IOorig) 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


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

UserInput = FrameMethod
IO = λ S → IOorig consoleI ∞ S

View = Frame


machineInputHandler : (S : Set)(v : View) → Set
machineInputHandler State v = (input : UserInput v) → IO State

record MachineState (State : Set) : Set where 
  field
    view    : View
    handleUserInput  : machineInputHandler State view

StateMachine : Set → Set
StateMachine State = (s : State) → MachineState State

open MachineState public


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

_⊎state_ = _⊎_

record FeatureMachineNaive : Set₁ where 
  field
    Features  : Set
    State     : Set
    Machine   : (f : Features) → StateMachine State



record FeatureMachine (BaseState : Set) : Set₁ where 
  field  
     Features    : Set
     AddedState  : Set
     Machine : (f : Features) → StateMachine (BaseState ⊎state AddedState) 
  State : Set
  State =  BaseState ⊎ AddedState 

open FeatureMachine public


simpleSMState : {S : Set}
                (btnStr : String)
                (end : S)
                → MachineState S
simpleSMState btnStr end .view = addButton btnStr emptyFrame
simpleSMState btnStr end .handleUserInput m  = return' end

addBtn2StateMachine : {S : Set}(sm : MachineState S)
                      (btnStr : String)(end : S)
                      → MachineState S
addBtn2StateMachine sm btnStr end .view = addButton btnStr (sm .view)
addBtn2StateMachine sm btnStr end .handleUserInput (zero , string) = return' end  --NEW BUTTON
addBtn2StateMachine sm btnStr end .handleUserInput (suc btnNum , string) =
  sm .handleUserInput (btnNum , string)


disjointChoiceState : {S : Set}
                      (btnStr1 : String) (end1 : S)
                      (btnStr2 : String) (end2 : S)
                      → MachineState S
disjointChoiceState btnStr1 end1 btnStr2 end2
                    = addBtn2StateMachine
                      (simpleSMState btnStr1  end1)
                      btnStr2
                      end2

addChoice2State : {S : Set}(sm : MachineState S)
                  (btnStr : String)(end : S)
                  → MachineState S
addChoice2State sm btnStr = addBtn2StateMachine sm btnStr



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




baseF : FeatureMachine StateV
baseF .Features = ⊤
baseF .AddedState = ⊥
baseF .Machine f (inj₁ s0) = simpleSMState "1Euro" (inj₁ s1)
baseF .Machine f (inj₁ s1) = simpleSMState "Get Change" (inj₁ s2)
baseF .Machine f (inj₁ s2) = simpleSMState "Soda" (inj₁ s0)
baseF .Machine f (inj₂ ())