{-# 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)