{-# OPTIONS --allow-unsolved-metas #-}
module GUI.GUIFeaturesPart8Paper 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


-- postulate Workflow : Set
-- postulate aWorkflow : Workflow

featureImplementation : Workflow → Workflow
featureImplementation x = activity "Feature" x

trivialWorkflow         :  Workflow
defaultOrderBloodTests  :  Workflow → Workflow
orderBloodTestsER       :  Workflow → Workflow

workflowBloodTestER : Workflow
workflowBloodTestER = orderBloodTestsER (defaultOrderBloodTests trivialWorkflow)

trivialWorkflow = endEvent "End"
defaultOrderBloodTests x = activity "Order Blood Test" x
orderBloodTestsER x = activity "orderBloodTestER" x


ExecutableIOProgram = IO Unit








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


adaptStateSMachineState : {S S' : Set}(ss' : S → S')
                     (smState : MachineState S)
                     → MachineState S'
adaptStateSMachineState ss' smState .view  = smState .view
adaptStateSMachineState ss' smState .handleUserInput m = mapStateMachineHandl ss' (smState .handleUserInput m)

adaptStateMachine : (S S' : Set)(ss' : S → S')(s's : S' → S)
                    → StateMachine S → StateMachine S'
adaptStateMachine S S' ss' s's sm s' = adaptStateSMachineState ss' (sm (s's s')) --ss' (s's s') s' (sm (s's s'))

-- \GUIFeaturesPartEightPaper
extendStateMachine : (S S' : Set)(sm : StateMachine S)
                     (new : (s' : S') → MachineState (S ⊎ S'))
                     → StateMachine (S ⊎ S')
extendStateMachine _ _ sm new (inj₁ s) .view = sm s .view
extendStateMachine _ _ sm new (inj₁ s) .handleUserInput m = mapStateMachineHandl inj₁ (sm s .handleUserInput m)
extendStateMachine _ _ sm new (inj₂ s') = new s'

{-
extendStateMachine' : (B S S' : Set)(sm : StateMachine (B ⊎ S))
                     (new : (s' : S') → MachineState (B ⊎ (S ⊎ S')))
                     → StateMachine (B ⊎ (S ⊎ S'))
extendStateMachine' _ _ sm new (inj₁ b) .view = sm (inj₁ b) .view
extendStateMachine' _ _ sm new (inj₂ (inj₁ s)) .view = sm (inj₂ s) .view
extendStateMachine' _ _ sm new (inj₁ b) .handleUserInput m = mapStateMachineHandl inj₁ (sm s .handleUserInput m)
extendStateMachine' _ _ sm new (inj₁ s) .handleUserInput m = mapStateMachineHandl inj₁ (sm s .handleUserInput m)
extendStateMachine' _ _ sm new (inj₂ (inj₂ s)) = new s'
-}



extendStateMachOneState :  {S : Set} (sm : StateMachine S)
                     (new : MachineState (S ⊎ Void)) → StateMachine (S ⊎ Void)

extendStateMachOneState{S} sm new = extendStateMachine S Void sm (λ _ → new)

mapS⊎[S'⊎S''] : {S S' S'' : Set}
                → S ⊎ S' ⊎ S''
                → (S ⊎ S') ⊎ S''
mapS⊎[S'⊎S''] (inj₁ s) = inj₁ (inj₁ s)
mapS⊎[S'⊎S''] (inj₂ (inj₁ s')) = inj₁ (inj₂ s')
mapS⊎[S'⊎S''] (inj₂ (inj₂ s'')) = inj₂ s''

map[S⊎S']⊎S''] : {S S' S'' : Set}
                → (S ⊎ S') ⊎ S''
                → S ⊎ S' ⊎ S''
map[S⊎S']⊎S''] (inj₁ (inj₁ s)) = inj₁ s
map[S⊎S']⊎S''] (inj₁ (inj₂ s')) = inj₂ (inj₁ s')
map[S⊎S']⊎S''] (inj₂ s'') = inj₂ (inj₂ s'')


extendSMachFixedState : {S S' S'' : Set}
                        (sm : StateMachine (S ⊎ S'))
                        (new : (s'' : S'')
                        → MachineState (S ⊎ (S' ⊎ S'')))
                        → StateMachine (S ⊎ (S' ⊎ S''))
extendSMachFixedState {S} {S'} {S''} sm new =
    adaptStateMachine ((S ⊎ S') ⊎ S'') (S ⊎ S' ⊎ S'') map[S⊎S']⊎S''] mapS⊎[S'⊎S''] (extendStateMachine (S ⊎ S') S'' sm (λ s'' → adaptStateSMachineState {S ⊎ (S' ⊎ S'')} {(S ⊎ S') ⊎ S''} mapS⊎[S'⊎S''] (new s''))) --(inj₂ (inj₂ s'')) (inj₂ s'') (new s'')))

extendSMachFixedState1 : {S S' : Set}
                         (sm : StateMachine (S ⊎ S'))
                         (new : MachineState (S ⊎ (S' ⊎ Void)))
                              → StateMachine (S ⊎ (S' ⊎ Void))
extendSMachFixedState1 sm new = extendSMachFixedState sm (λ _ → new)


{-   FEATURE MACHINE -}
-- \GUIFeaturesPartEightPaper
FeatureMachineNaive : (F S : Set) → Set
FeatureMachineNaive F S = (f : F) → StateMachine S


{-
FeatureMachine : (F : Set)(B : Set)(S' : Set) → Set
FeatureMachine F B S' = (f : F) → StateMachine (B  ⊎ S')
-}

-- \GUIFeaturesPartEightPaper
FeatureMachine : (F B S : Set)  → Set
FeatureMachine F B S = (f : F) → StateMachine (B ⊎ S)


adaptFeatureMachine' : {F : Set}{S S' : Set}(ss' : S → S')(s's : S' → S)
                     (fm : FeatureMachineNaive F S) → FeatureMachineNaive F S'
adaptFeatureMachine' {F}{S}{S'} ss' s's fm f = adaptStateMachine S S' ss' s's (fm f)


{-
adaptFeatureMachine : {F : Set}{B S S' : Set}(ss' : S → S')(s's : S' → S)
                     (fm : FeatureMachineNaive F B S) → FeatureMachineNaive F B S'
adaptFeatureMachine {F}{B}{S}{S'} ss' s's fm f
    = adaptStateMachine (B ⊎ S) (B ⊎ S') (mapSum (λ b → b)  ss') (mapSum (λ b → b)  s's)   (fm f)
-}


extendFeatureMachineGen : {F : Set}{S S' : Set}
                       (fm : FeatureMachineNaive F S)
                       (new : (f : F) (s' : S')
                               → MachineState (S ⊎ S'))
                      → FeatureMachineNaive F (S ⊎ S')
extendFeatureMachineGen {_}{S}{S'} fm new f s = extendStateMachine S S' (fm f) (new f) s




extendFeatureMachineStates : {F : Set} {S S' S'' : Set}
                           (fm : FeatureMachineNaive F (S ⊎ S'))
                          (new : (f : F)(s'' : S'')
                           → MachineState (S ⊎ (S' ⊎ S'')))
                          → FeatureMachineNaive F (S ⊎ (S' ⊎ S''))
extendFeatureMachineStates fm new f = extendSMachFixedState (fm f) (new f)

extendFeatureMachineState' :  
                              {F : Set} {S S' : Set} 
                              (fm : FeatureMachineNaive F (S ⊎ S'))
                              (new : MachineState (S ⊎ (S' ⊎ Void)))
                              → FeatureMachineNaive F (S ⊎ (S' ⊎ Void))
extendFeatureMachineState' fm new f = extendSMachFixedState (fm f) (λ _ → new)


-- \GUIFeaturesPartEightPaper
addStateToFeatureMachine : {F B S' : Set} (fm : FeatureMachine F B S')
                            (new : MachineState (B ⊎ (S' ⊎ Void)))
                            → FeatureMachine F B (S' ⊎ Void)
addStateToFeatureMachine fm new f = extendSMachFixedState (fm f) (λ _ → new)


adaptFeatureMachine : {F F' : Set}(f'f : F' →  F)
                     {S : Set}
                     (fm : FeatureMachineNaive F S)
                     → FeatureMachineNaive F' S
adaptFeatureMachine f'f fm f' = fm (f'f f')


extendFeatureFMachineNaive : {F F' : Set}{S : Set}
                     (fm : FeatureMachineNaive F S)
                      → FeatureMachineNaive (F × F') S
extendFeatureFMachineNaive fm = adaptFeatureMachine proj₁ fm


-- \GUIFeaturesPartEightPaper
addFeatureToFeatureMachine : {F B F' S : Set}
                              (fm : FeatureMachine F B S)
                              → FeatureMachine (F × F') B S
addFeatureToFeatureMachine fm = adaptFeatureMachine proj₁ fm


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

basicVM : FeatureMachineNaive Void (StatesBasicVM ⊎ ∅)
basicVM  f (inj₁ pay)        =
         simpleSMState "Pay" (inj₁ change)
basicVM  f (inj₁ change)     =
         simpleSMState "Get Change" (inj₁ soda)
basicVM  f (inj₁ soda)       =
         simpleSMState "Soda" (inj₁ serveSoda) 
basicVM  f (inj₁ serveSoda)  =
         simpleSMState "Serve Soda" (inj₁ open')
basicVM  f (inj₁ open')      =
         simpleSMState "Open" (inj₁ close)
basicVM  f (inj₁ close)      =
         simpleSMState "Close" (inj₁ pay) 
basicVM  f (inj₂ ())

{- handler for the new state to be added to the tea machine -}
teaNewStateSM : {Extra : Set}
                → MachineState (StatesBasicVM ⊎ Extra ⊎ Void) --newState
teaNewStateSM = simpleSMState "Serve Tea" (inj₁ open')


{- add the new state to the feature machine -}
TeaMAddState : {F : Set}{S : Set}(fm :  FeatureMachineNaive F (StatesBasicVM ⊎ S))
                         → FeatureMachineNaive F (StatesBasicVM ⊎ (S ⊎ Void))
TeaMAddState fm = addStateToFeatureMachine fm teaNewStateSM


{- add a dummy feature "FeatureTea" to the feature machine -}
TeaMAddFeature : {F : Set}{S : Set}
                (fm : FeatureMachineNaive F S)
                 → FeatureMachineNaive (F × FeatureTea) S
TeaMAddFeature fm = extendFeatureFMachineNaive fm

TeaMAdaptFeature : {F : Set}{S : Set}
                    (fm : FeatureMachineNaive (F × FeatureTea) (StatesBasicVM ⊎ (S ⊎ Void)))
                     →  FeatureMachineNaive (F × FeatureTea) (StatesBasicVM ⊎ (S ⊎ Void))
TeaMAdaptFeature fm (f , yesTea) (inj₁ soda) =
       addBtn2StateMachine  (fm (f , yesTea) (inj₁ soda)) "Tea" newState
TeaMAdaptFeature fm f s = fm f s


Tea : {F : Set}{S : Set}
      (fm : FeatureMachineNaive F (StatesBasicVM ⊎ S))
      → FeatureMachineNaive (F × FeatureTea) (StatesBasicVM ⊎ (S ⊎ Void))
Tea fm = TeaMAdaptFeature    (TeaMAddFeature (TeaMAddState fm))


-- example
teaMachine : FeatureMachineNaive (Void × FeatureTea) (StatesBasicVM ⊎ ∅ ⊎ Void)
teaMachine = Tea basicVM


{- handler for the new state to be added to the cancel machine -}
cancelNewStateSM : {Extra : Set}
                → MachineState (StatesBasicVM ⊎ Extra ⊎ Void) -- newState
cancelNewStateSM = simpleSMState "Cancelling" (inj₁ pay)


{- add the new state to the feature machine -}
CancelMAddState : {F : Set}{S : Set}(fm :  FeatureMachineNaive F (StatesBasicVM ⊎ S))
                         → FeatureMachineNaive F (StatesBasicVM ⊎ (S ⊎ Void))
CancelMAddState fm = addStateToFeatureMachine fm cancelNewStateSM


{- add a dummy feature "FeatureCancel" to the feature machine -}
CancelMAddFeature : {F : Set}{S : Set}
                (fm : FeatureMachineNaive F S)
                 → FeatureMachineNaive (F × FeatureCancel) S
CancelMAddFeature fm = extendFeatureFMachineNaive fm

CancelMAdaptFeature : {F : Set}{S : Set}
                    (fm : FeatureMachineNaive (F × FeatureCancel) (StatesBasicVM ⊎ (S ⊎ Void)))
                     →  FeatureMachineNaive (F × FeatureCancel) (StatesBasicVM ⊎ (S ⊎ Void))
CancelMAdaptFeature fm (f , yesCancel) (inj₁ soda) =
       addBtn2StateMachine  (fm (f , yesCancel) (inj₁ soda)) "Cancel" newState
CancelMAdaptFeature fm f s = fm f s


Cancel : {F : Set}{S : Set}
      (fm : FeatureMachineNaive F (StatesBasicVM ⊎ S))
      → FeatureMachineNaive (F × FeatureCancel) (StatesBasicVM ⊎ (S ⊎ Void))
Cancel fm = CancelMAdaptFeature    (CancelMAddFeature (CancelMAddState fm))

cancelTeaMachine : FeatureMachineNaive ((Void × FeatureTea) × FeatureCancel)
                                        (StatesBasicVM ⊎ (∅ ⊎ Void) ⊎ Void)
cancelTeaMachine = Cancel (Tea basicVM)

{- add a dummy feature "FeatureFree" to the feature machine -}
FreeMAddFeature : {F : Set}{S : Set}
                 (fm : FeatureMachineNaive F S)
                  → FeatureMachineNaive (F × FeatureFree) S
FreeMAddFeature fm = extendFeatureFMachineNaive fm



FreeMAdaptFeature : {F : Set}{S : Set}
                       (fm : FeatureMachineNaive (F × FeatureFree) (StatesBasicVM ⊎ S))
                     →  FeatureMachineNaive (F × FeatureFree) (StatesBasicVM ⊎ S)
FreeMAdaptFeature fm (f , yesFree) (inj₁ pay) =
       simpleSMState "Free" (inj₁ soda)
FreeMAdaptFeature fm f s = fm f s

Free : {F : Set}{S : Set}
      (fm : FeatureMachineNaive F (StatesBasicVM ⊎ S))
      → FeatureMachineNaive (F × FeatureFree) (StatesBasicVM ⊎ S)
Free fm = FreeMAdaptFeature   (FreeMAddFeature fm)

freeCancelTeaMachine : FeatureMachineNaive
                       (((Void × FeatureTea) × FeatureCancel) × FeatureFree)
                       (StatesBasicVM ⊎ (∅ ⊎ Void) ⊎ Void)
freeCancelTeaMachine = Free (Cancel (Tea basicVM))

compileWorkflowToProgram : Workflow → ExecutableIOProgram

main : ExecutableIOProgram
main = compileWorkflowToProgram workflowBloodTestER

compileWorkflowToProgram w =
   do
     win ← createWindowFFI
     compile win guiProgram


   where
     guiProgram : GUI
     guiProgram = businessModel2GUI w



-- main1 : IO Unit
-- main1 = {!!} --compileSMachine (basicVM _)  (inj₁ pay)


--main : NativeIO Unit
--main = compileSMachine {!!} {!!} --(Free (Cancel (Tea basicVM)) (((_ , yesTea ) , yesCancel) , noFree))  (inj₁ pay)