module GUI.GUIFeaturesPart5extended where

open import GUI.GUIFeatures
open import GUI.GUIFeaturesPart2
open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)
open import GUI.GUIFeaturesPart4 hiding ( cancelNewStateSM ; cancelStateAdded ; cancelFeatureAdded  )

open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.Product
open import Data.Sum
open import Data.String.Base

open import NativeIO

open import GUI.GUIDefinitions

open import GUI.GUICompilationFeatures using (compileFeatureVM)


data StatesBasicVM : Set where
  pay change soda serveSoda  open' close : StatesBasicVM

basicVM : FMachine StatesBasicVM
basicVM  .Features = ⊤
basicVM  .AddStateF = ⊥
basicVM  .GUIF f (inj₁ pay)        =
         simpleSMState "Pay" (inj₁ change)
basicVM  .GUIF f (inj₁ change)     =
         simpleSMState "Get Change" (inj₁ soda)
basicVM  .GUIF f (inj₁ soda)       =
         simpleSMState "Soda" (inj₁ serveSoda)
basicVM  .GUIF f (inj₁ serveSoda)  =
         simpleSMState "Serve Soda" (inj₁ open')
basicVM  .GUIF f (inj₁ open')      =
         simpleSMState "Open" (inj₁ close)
basicVM  .GUIF f (inj₁ close)      =
         simpleSMState "Close" (inj₁ pay) 
basicVM  .GUIF f (inj₂ ())

newState : {A B : Set} → A ⊎ B ⊎ ⊤
newState = (inj₂ (inj₂ tt))

{- handler for the new state to be added to the tea machine -}
teaNewStateSM :  (bev : String)
                 (fm : FMachine StatesBasicVM)
                 →    SMachineState
                      (StatesBasicVM ⊎ fm .AddStateF ⊎ ⊤)
                      {-newState-}
teaNewStateSM bev fm = simpleSMState (primStringAppend "Serve " bev) (inj₁ open')


data FeatureBev : String → Set where
  yes no : (str : String) → FeatureBev str


{- add the new state to the feature machine -}
BevMAddNewState :  (bev : String)
                   (fm : FMachine StatesBasicVM)
                   → FMachine StatesBasicVM
BevMAddNewState bev fm =
  addOneStateFMachine fm (teaNewStateSM bev fm)

{- add a dummy feature "FeatureBev" to the feature machine -}
BevMAddFeature :  (bev : String)
                  (fm : FMachine StatesBasicVM)
                  → FMachine StatesBasicVM
BevMAddFeature bev fm = addDummyFeatures
                         (BevMAddNewState bev fm)
                         (FeatureBev bev)

{- redefine in the feature machine one button -}
Bev :  (bev : String)
       (fm : FMachine StatesBasicVM)
       → FMachine StatesBasicVM
Bev bev fm .Features   = BevMAddFeature bev fm .Features
Bev bev fm .AddStateF  = BevMAddFeature bev fm .AddStateF
Bev bev fm .GUIF (f , (yes .bev)) (inj₁ soda) =
      addBtn2StateMachine
      (  BevMAddFeature bev fm .GUIF
         (f , (yes bev)) (inj₁ soda))
         bev newState
Bev bev fm .GUIF f  s = BevMAddFeature bev fm .GUIF f s

{- handler for the new state to be added to the cancel machine -}
cancelNewStateSM : (fm : FMachine StatesBasicVM) →
                    SMachineState (StatesBasicVM ⊎ fm .AddStateF ⊎ ⊤) {-newState-}
cancelNewStateSM fm = simpleSMState "Cancelling" (inj₁ pay)

{- add the state to the old feature machine -}
cancelStateAdded : FMachine StatesBasicVM → FMachine StatesBasicVM
cancelStateAdded fm = addOneStateFMachine fm (cancelNewStateSM fm)

{- add a dummy feature "FeatureCancel" to the feature machine -}
cancelFeatureAdded : FMachine StatesBasicVM → FMachine StatesBasicVM
cancelFeatureAdded fm = addDummyFeatures
                         (cancelStateAdded fm)
                         FeatureCancel

{- redefine in the feature machine one button -}
Cancel :  FMachine StatesBasicVM
          → FMachine StatesBasicVM
Cancel fm .Features = cancelFeatureAdded fm .Features
Cancel fm .AddStateF  = cancelFeatureAdded fm .AddStateF
Cancel fm .GUIF (f , yesCancel) (inj₁ soda) =
      addBtn2StateMachine (cancelFeatureAdded fm .GUIF (f , yesCancel) (inj₁ soda))
                          "Cancel" newState
Cancel fm .GUIF f  s = cancelFeatureAdded fm .GUIF f s

{- add the Dummy free feature -}
FreeMAddFeature : FMachine StatesBasicVM
                  → FMachine StatesBasicVM
FreeMAddFeature fm = addDummyFeatures fm FeatureFree

{- redefine the pay button to free in case feature free is yesFree -}
Free :  FMachine StatesBasicVM
        → FMachine StatesBasicVM
Free fm .Features   = FreeMAddFeature fm .Features
Free fm .AddStateF  = FreeMAddFeature fm .AddStateF
Free fm .GUIF (f , yesFree) (inj₁ pay) =
      simpleSMState "Free" (inj₁ soda)
Free fm .GUIF (f , yesFree) (inj₁ open') =
      simpleSMState "Skip" (inj₁ pay)
Free fm .GUIF f  s  = FreeMAddFeature fm .GUIF f s

main1 : NativeIO Unit
main1 = compileFeatureVM (Bev "Tea" (Cancel basicVM)) ((_ , yesCancel) , (yes "Tea")) (inj₁ pay)

main2 : NativeIO Unit
main2 = compileFeatureVM (Free basicVM) (_ , yesFree) (inj₁ pay) --

multiFeatureMachine : FMachine StatesBasicVM
multiFeatureMachine = Free (Cancel (Bev "Tea" basicVM))

multiVendingMachine : List String →  FMachine StatesBasicVM
multiVendingMachine [] = basicVM
multiVendingMachine (str ∷ l) = Bev str (multiVendingMachine l)

multiVendingMachineYes : (l : List String) → multiVendingMachine l .Features
multiVendingMachineYes [] = _
multiVendingMachineYes (str ∷ l) = multiVendingMachineYes l , yes str

multiVendingMachineNative : List String → NativeIO Unit
multiVendingMachineNative l = compileFeatureVM
                               (multiVendingMachine l)
                               (multiVendingMachineYes l)
                               (inj₁ pay)
main : NativeIO Unit
main = multiVendingMachineNative ("Tea" ∷ "Water" ∷ "Coffee" ∷ [])


main' : NativeIO Unit
main' = compileFeatureVM
       multiFeatureMachine
       (((_ , (yes "Tea")) , yesCancel) , yesFree) (inj₁ pay)