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
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)
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')
featureMachine2StateMachine : {F S : Set}
(fmachine : FeatureMachineNaive F S)
→ StateMachine (F × S)
featureMachine2StateMachine {F} {S} fmachine (f , s) =
mapMachineState (λ s → (f , s)) (fmachine f s)
featureMachineMonadic2StateMachineMonadicaux : {F : Set}{S : Set}{S' : Set}
(f : F)
(ss' : S ⊎ S')
→ F × S ⊎ S'
featureMachineMonadic2StateMachineMonadicaux {F} {S} {S'} f (inj₁ s)
= inj₁ (f , s)
featureMachineMonadic2StateMachineMonadicaux {F} {S} {S'} f (inj₂ s')
= inj₂ 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
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) )
→ 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')
(smState : MachineState (S ⊎ A) )
→ MachineState (S' ⊎ A)
adaptStateMachineStateMonadic ss' smState .view = smState .view
adaptStateMachineStateMonadic ss' 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' (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) )
→ 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
((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) )
→ 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) )
→ 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
FeatureMachineMonadicΣ : (A : Set)(F : Set)(S : F → Set) → Set
FeatureMachineMonadicΣ A F S = (f : F) → StateMachineMonadic A (S f)
featureMachineMonadic2StateMachineMonadicauxΣ : {F : Set}{S : F → Set}{S' : Set}
(f : F)
(ss' : S f ⊎ S')
→ Σ F S ⊎ S'
featureMachineMonadic2StateMachineMonadicauxΣ {F} {S} {S'} f (inj₁ s)
= inj₁ (f , s)
featureMachineMonadic2StateMachineMonadicauxΣ {F} {S} {S'} f (inj₂ s')
= inj₂ 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
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')