-- \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 :
-}