-- \GUIFeaturesMonadicPaper
module GUI.GUIFeaturesMonadicPaper where

open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.Product hiding (swap)
open import Data.Sum renaming (map to map+)
open import Data.String.Base
open import Size

open import SizedIO.Base renaming (IO to IO∞; IO' to IO) hiding (_>>=_ ; _>>_ ; return)

open import NativeIO

open import GUI.GUIDefinitions

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)
open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)
open import GUI.GUIFeaturesPart8Paper

open import SizedIO.Console
{-
mapStateMachineState : {S S' : Set}(f : S → S')
                   → StateMachineState S
                   → StateMachineState S'
mapStateMachineState {S}{S'} f m = ?
-}

-- StateMachineMonadic A S
--  is like an StateMachine, but it has additional return values in A

-- \GUIFeaturesMonadicPaper
StateMachineMonadic : (A  S : Set) → Set
StateMachineMonadic A S  = S → MachineState (S ⊎ A)

FeatureMachineMonadic : (A F S : Set) → Set
FeatureMachineMonadic A F S = (f : F) → StateMachineMonadic A S

mapMachineState : {S S' : Set}(f : S → S')(sm : MachineState S)
                    → MachineState S'
mapMachineState f sm .view = sm .view
mapMachineState f sm .handleUserInput m = mapStateMachineHandl f (sm .handleUserInput m)


mapStateMachineReturnMonadic : {A A' : Set}(f : A → A'){S : Set}
                           (machine : StateMachineMonadic A S)
                           → StateMachineMonadic A' S
mapStateMachineReturnMonadic {A} {A'} f {S} machine  s =
     mapMachineState  (map+ (λ x → x) f) (machine s)


mapFeatureMach : {A F A' : Set}(g : A → A'){S : Set}
                           (machine : FeatureMachineMonadic A F S)
                           → FeatureMachineMonadic A' F S
mapFeatureMach {A} {F} {A'} g {S} machine  f s =
     mapMachineState  (map+ (λ x → x) g) (machine f s)




-- we can combine two monadic StateMachines, where the first one
--   possibly terminates in states of the second one
-- and the second one possibly terminates in states of the first one:

combineStateMachineMonadic : {S S' : Set}
                         (machine1 : StateMachineMonadic S' S)
                         (machine2 : StateMachineMonadic S S')
                         → StateMachine (S ⊎ S')
combineStateMachineMonadic machine1 machine2 (inj₁ s) = machine1 s
combineStateMachineMonadic machine1 machine2 (inj₂ s') = mapMachineState swap (machine2 s')


-- a feature machine is transformed into an S Machine
-- by having as states   F × S
-- and for state (f , s) using machine
--    fmachine f s
featureMachine2StateMachine : {F S : Set}
                          (fmachine : FeatureMachineNaive F S)
                          → StateMachine (F × S)
featureMachine2StateMachine {F} {S} fmachine  (f , s) =
         mapMachineState (λ s → (f , s)) (fmachine f s)


-- auxiliary functions  used in the map in the next operation
featureMachineMonadic2StateMachineMonadicaux   : {F : Set}{S : Set}{S' : Set}
       (f : F)
       (ss' : S ⊎ S')
       → F × S ⊎ S'  -- Σ[ f ∈ F ](S f) ⊎ S'
featureMachineMonadic2StateMachineMonadicaux {F} {S} {S'} f (inj₁ s)
   = inj₁ (f , s)
featureMachineMonadic2StateMachineMonadicaux {F} {S} {S'} f (inj₂ s')
  = inj₂ s'

-- take a monadic F machine with rerturn values in S'
-- into a monadic S machine with rerturn values in S'
featureMachineMonadic2StateMachineMonadic : {F : Set}{S : Set}{S' : Set}
                          (fmachine : FeatureMachineMonadic  S' F S)
                          → StateMachineMonadic S' (F ×  S)
featureMachineMonadic2StateMachineMonadic {F} {S} {S'} fmachine (f , s)
     = mapMachineState (featureMachineMonadic2StateMachineMonadicaux f) (fmachine f s)

combineStateFeatureMachineaux : {F S : Set}{S' : Set}
                                    (f : F)
                                    (s's : S' ⊎ S)
                                    → S ⊎ (F ×  S')
combineStateFeatureMachineaux {F} {S} {S'} f (inj₁ s') = inj₂ (f , s')
combineStateFeatureMachineaux {F} {S} {S'} f (inj₂ s) = inj₁ s

-- we combine one monadic S machine with return values in
--  a feature and state of a second machine
-- with a monadic feature machine  with return values
-- into the states of the first machine

-- \GUIFeaturesMonadicPaper
combineStateFeatureMachine : {F S S' : Set}
                         (machine₁ : StateMachineMonadic (F ×  S') S)
                         (machine₂ : FeatureMachineMonadic S F S')
                         → StateMachine (S ⊎ (F ×  S'))
combineStateFeatureMachine {F} {S} {S'} machine₁ machine₂ (inj₁ s) = machine₁ s
combineStateFeatureMachine {F} {S} {S'} machine₁ machine₂ (inj₂ (f , s')) =
   mapMachineState  (combineStateFeatureMachineaux f) (machine₂ f s')

mapStateMachineHandlMonadic : {A S S' : Set}(f : S → S')
                       (p : IO consoleI ∞ (S ⊎ A))
                       → IO consoleI ∞ (S' ⊎ A)
mapStateMachineHandlMonadic f p = mapIO' (map+ f λ a → a ) p

extendStateMachineMonadic : {A S S' : Set} (sm : StateMachineMonadic A S)
                              (new : (s' : S')
                                     → MachineState ((S ⊎ S') ⊎ A) {-(inj₂ s')-})
                 → StateMachineMonadic A (S ⊎ S')
extendStateMachineMonadic  sm new (inj₁ s) .view = sm s .view
extendStateMachineMonadic  sm new (inj₁ s) .handleUserInput m = mapStateMachineHandlMonadic inj₁ (sm s .handleUserInput m)
extendStateMachineMonadic  sm new (inj₂ s') = new s'



adaptStateMachineStateMonadic : {A S S' : Set}(ss' : S → S'){-(s : S)(s' : S')-}
                     (smState : MachineState (S ⊎ A) {-s-})
                     → MachineState (S' ⊎ A) {-s'-}
adaptStateMachineStateMonadic ss' {-s s'-} smState .view  = smState .view
adaptStateMachineStateMonadic ss' {-s s'-} smState .handleUserInput m = mapStateMachineHandlMonadic ss' (smState .handleUserInput m)


adaptStateMachineMonadic : {A S S' : Set}(ss' : S → S')(s's : S' → S)
                (sm : StateMachineMonadic  A S)
                → StateMachineMonadic A S'
adaptStateMachineMonadic ss' s's sm s' = adaptStateMachineStateMonadic ss' {-(s's s')-} {-s'-} (sm (s's s'))

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




extendSMachFixedStateMonadic : {A S S' S'' : Set}
                        (sm : StateMachineMonadic  A (S ⊎ S'))
                        (new : (s'' : S'')
                        → MachineState ((S ⊎ (S' ⊎ S'')) ⊎ A) {-(inj₂ (inj₂ s''))-})
                        → StateMachineMonadic A (S ⊎ (S' ⊎ S''))
extendSMachFixedStateMonadic {A} {S} {S'} {S''} sm new =
    adaptStateMachineMonadic map[S⊎S']⊎S''] mapS⊎[S'⊎S'']
    (extendStateMachineMonadic sm
       (λ s'' → adaptStateSMachineState {(S ⊎ S' ⊎ S'') ⊎ A}
                {((S ⊎ S') ⊎ S'') ⊎ A} mapS⊎[S'⊎S'']⊎A
                {-(inj₂ (inj₂ s''))-} {-(inj₂ s'')-} ((new s''))))


extendFMachFixedStateMonadic : {A : Set}{F : Set} {S S' S'' : Set}
                           (fm : FeatureMachineMonadic A F (S ⊎ S'))
                          (new : (f : F)(s'' : S'')
                           → MachineState ((S ⊎ (S' ⊎ S'')) ⊎ A) {-(inj₂ (inj₂ s''))-})
                          → FeatureMachineMonadic A F (S ⊎ (S' ⊎ S''))
extendFMachFixedStateMonadic fm new f = extendSMachFixedStateMonadic (fm f) (new f)

extendFMachFixedState1Monadic : {A : Set} {F : Set} {S S' : Set}
                         (fm : FeatureMachineMonadic A F (S ⊎ S'))
                         (new : MachineState ((S ⊎ (S' ⊎ ⊤)) ⊎ A) {-(inj₂ (inj₂ _))-})
                          → FeatureMachineMonadic A F (S ⊎ (S' ⊎ ⊤))
extendFMachFixedState1Monadic fm new f = extendSMachFixedStateMonadic (fm f) (λ _ →  new )

adaptFeatureFMachMonadic : {A F F' : Set}(f'f : F' →  F)
                     {S : Set}
                     (fm : FeatureMachineMonadic A F S)
                     → FeatureMachineMonadic A F' S
adaptFeatureFMachMonadic f'f fm f' = fm (f'f f')


extendFeatureFMachMonadic : {A F F' : Set}
                  {S : Set}
                  (fm : FeatureMachineMonadic A F S)
                  → FeatureMachineMonadic A (F × F') S
extendFeatureFMachMonadic fm = adaptFeatureFMachMonadic proj₁ fm

-- Now as before but the states depend on the feature

-- FMachine where the states depend on the feature
FeatureMachineMonadicΣ  : (A : Set)(F : Set)(S : F → Set) → Set
FeatureMachineMonadicΣ A F S = (f : F) → StateMachineMonadic A (S f)

-- auxiliary functions  used in the map in the next operation
featureMachineMonadic2StateMachineMonadicauxΣ   : {F : Set}{S : F → Set}{S' : Set}
       (f : F)
       (ss' : S f ⊎ S')
       → Σ F S ⊎ S'  -- Σ[ f ∈ F ](S f) ⊎ S'
featureMachineMonadic2StateMachineMonadicauxΣ {F} {S} {S'} f (inj₁ s)
   = inj₁ (f , s)
featureMachineMonadic2StateMachineMonadicauxΣ {F} {S} {S'} f (inj₂ s')
  = inj₂ s'

-- take a monadic F machine with rerturn values in S'
-- into a monadic S machine with rerturn values in S'
featureMachineMonadic2StateMachineMonadicΣ : {F : Set}{S : F → Set}{S' : Set}
                          (fmachine : FeatureMachineMonadicΣ S' F S)
                          → StateMachineMonadic S' (Σ F S)
featureMachineMonadic2StateMachineMonadicΣ {F} {S} {S'} fmachine (f , s)
     = mapMachineState (featureMachineMonadic2StateMachineMonadicauxΣ f) (fmachine f s)

combineStateFeatureMachineauxΣ : {F S : Set}{S' : F → Set}
                                    (f : F)
                                    (s's : S' f ⊎ S)
                                    → S ⊎ (Σ F S')
combineStateFeatureMachineauxΣ {F} {S} {S'} f (inj₁ s') = inj₂ (f , s')
combineStateFeatureMachineauxΣ {F} {S} {S'} f (inj₂ s) = inj₁ s

-- we combine one monadic S machine with return values in
--  a feature and state of a second machine
-- with a monadic feature machine  with return values
-- into the states of the first machine

combineStateFeatureMachineΣ : {F S : Set}{S' : F →  Set}
                         (machine1 : StateMachineMonadic (Σ F S') S)
                         (machine2 : FeatureMachineMonadicΣ S F S')
                         → StateMachine (S ⊎ (Σ F S'))
combineStateFeatureMachineΣ {F} {S} {S'} machine1 machine2 (inj₁ s) = machine1 s
combineStateFeatureMachineΣ {F} {S} {S'} machine1 machine2 (inj₂ (f , s')) =
   mapMachineState  (combineStateFeatureMachineauxΣ f) (machine2 f s')


{-
combineStateMachineFeatureMachine : {S S' F : Set}
                                (machine1 : StateMachineMonadic S' S)
                                (machine2 :
-}