{-# OPTIONS --allow-unsolved-metas #-}
module GUI.GUIFeaturesPart8CompiledVendingMachinePaper where

open import Data.Unit renaming (⊤ to Void)
open import Data.Empty renaming (⊥ to ∅)
open import Data.List
open import Data.Product
open import Data.Sum renaming (map to mapSum)
open import Data.String.Base

open import NativeIO renaming (NativeIO to IO;
                               nativeReturn to return;
                               _native>>=_ to _>>=_;
                               _native>>_ to _>>_)

open import GUI.Vers1.GUIDefinitions
open import GUI.Vers1.GUICompilation hiding (main)

open import GUI.GUICompilationFeatures using (compileSMachine)

open import GUI.GUIFeatures using (FeatureTea; FeatureCancel; FeatureFree; yesTea; yesCancel; noFree; yesFree)
open import GUI.GUIFeaturesPart2Paper hiding (FeatureMachine ; FeatureMachineNaive; IO) -- using (SMachineState; fSM; handlSM; SMachine; simpleSMState; addBtn2StateMachinee; addBtn2StateMachine) --hiding (FMachine)
open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)
open import GUI.Vers1.GUIExampleLib
open import GUI.Vers1.BusinessProcess
open import GUI.Vers1.BusinessProcess renaming (BusinessProcess to Workflow)
open import GUI.Vers1.RasterificFFI
open import GUI.BusinessProcessMedExLib
open import GUI.GUIFeaturesPart8Paper hiding (main)
open import GUI.GUICompilationFeaturesPaper

-- compileGUI' : {S : Set}(sm : StateMachine S)(s : S) → NativeIO Unit
-- FeatureMachineNaive F S = (f : F) → StateMachine S
test : FeatureMachineNaive Void (StatesBasicVM ⊎ ∅)
test = basicVM


mainBasicVendingMachine : ExecutableIOProgram
mainBasicVendingMachine = compileGUI' (basicVM tt) (inj₁ pay) -- compileGUI'  basicVM ?

main : ExecutableIOProgram
main = compileGUI' (freeCancelTeaMachine (((tt , yesTea ) , yesCancel) , noFree )) (inj₁ pay)