-- \GUIFeaturesMonadicExamplePaper
module GUI.GUIFeaturesMonadicExamplePaper where

open import Data.Unit renaming (tt to triv)
open import Data.Empty
open import Data.List
open import Data.Product hiding (swap)
open import Data.Sum renaming (inj₁ to position; inj₂ to extended)
open import Data.Sum
open import Data.String.Base

open import NativeIO

open import GUI.GUIDefinitions

open import GUI.GUICompilationFeaturesPaper using (compileStateMachine;compileToGUI';compileRegularGUI)

open import GUI.GUIFeatures using (FeatureTea; FeatureCancel; FeatureFree; yesTea; yesCancel; noFree; yesFree)
open import GUI.GUIFeaturesPart2Paper using (MachineState; view; handleUserInput; StateMachine; simpleSMState; addBtn2StateMachine;disjointChoiceState)
open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)
open import GUI.GUIFeaturesPart8Paper using (newState)
open import GUI.GUIFeaturesMonadicPaper

open import GUI.GUIFeaturesPart5extendedMedication hiding (basicMachine ; noacNewStateSM ; NoacMAddNewState ; NoacMAddFeature ; StatesBasic)
-- open import GUI.GUIFeaturesPart6Medication hiding (basicMachine ; noacNewStateSM ; NoacMAddNewState ; NoacMAddFeature ; NoacMAdaptFeature ; NoacFMachine )


data StatesCallMachine : Set where
  enterCrCl   : StatesCallMachine


data StatesBasic : Set where
--   enterCrCl               : StatesBasic
  prescribeMed     : StatesBasic
  warfarin                : StatesBasic
  dischargePatient        : Medication → StatesBasic



continue : {A B  : Set} (a : A) → A ⊎ B
continue a = position a

terminate : {A B  : Set} (b : B) → A ⊎ B
terminate b = extended b

{-
callMachine : {F S : Set}(f : F)(noa : NOAC) → SMachineMonadic ((F × FeatureNOAC noa) × StatesBasic)
                          StatesCallMachine
-}

-- \GUIFeaturesMonadicExamplePaper
callMachine : (noa : NOAC) → StateMachineMonadic (FeatureNOAC noa × StatesBasic)
                          StatesCallMachine
-- \GUIFeaturesMonadicExamplePaper
callMachine noa enterCrCl =
  disjointChoiceState  "CrCl < 15"  (terminate (noNOAC noa , prescribeMed))
                       "CrCl ≥ 15"  (terminate (yesNOAC noa ,  prescribeMed))


callMachine' : {F S  : Set}(f : F)(noa : NOAC)
         → StateMachineMonadic ((F × FeatureNOAC noa) ×
                                (StatesBasic ⊎ S ))
                          StatesCallMachine
callMachine' f noa enterCrCl =
  disjointChoiceState  "CrCl < 15"  (terminate ((f , noNOAC noa) , inj₁ prescribeMed))
                       "CrCl ≥ 15"  (terminate ((f , yesNOAC noa) , inj₁ prescribeMed))


{-
  addBtn2StateMachine
     (simpleSMState "CrCl < 15" (terminate (noNOAC noa , prescribeMed)))
      "CrCl ≥ 15"
     (terminate (yesNOAC noa ,  prescribeMed))
-}
callMachineFeatured : {F S  : Set}(f : F)(noa : NOAC)
                      → StateMachineMonadic ((F × FeatureNOAC noa) ×
                                         (StatesBasic ⊎ S ))
                          StatesCallMachine
callMachineFeatured f noa =
    mapStateMachineReturnMonadic (λ {( fnoa , s) → ((f , fnoa) , position s)}) (callMachine noa)

basicMachine : FeatureMachineMonadic ⊤  ⊤ (StatesBasic ⊎ (⊥ ⊎ ⊥))
{-
basicMachine f (position enterCrCl) =
   addBtn2StateMachine
  (simpleSMState "CrCl < 15" (position (continue (prescribeMed <15))))
  "CrCl ≥ 15"
  (position (continue (prescribeMed ≥15)))
-}
basicMachine f (position prescribeMed) =
  simpleSMState "Warfarin" (position (continue warfarin))
basicMachine f (position warfarin) =
  simpleSMState "Warfarin prescribed" (position (continue (dischargePatient warfarin)))
basicMachine f (position (dischargePatient x)) =
   simpleSMState "Discharge patient" (terminate _)
basicMachine f (extended (position ()))
basicMachine f (extended (extended ()))


{- handler for the new state to be added to the tea machine -}
noacNewStateSM : {A  : Set} {Extra : Set}(noa : NOAC)
                → MachineState ((StatesBasic ⊎ Extra ⊎ ⊤) ⊎ A) {-newState-}
noacNewStateSM noa = simpleSMState (noacName noa) (continue (position (dischargePatient (noac noa))))

{- add the new state to the feature machine -}
NoacMAddNewState : {A : Set}{F : Set}{S : Set}(noa : NOAC)
                         → (fm :  FeatureMachineMonadic A F (StatesBasic ⊎ S))
                         → FeatureMachineMonadic A F (StatesBasic ⊎ (S ⊎ ⊤))
NoacMAddNewState noa fm = extendFMachFixedState1Monadic fm (noacNewStateSM noa)

{- add a dummy feature NOAC to the feature machine -}
NoacMAddFeature : {A F : Set}{S : Set}(noa : NOAC)
                (fm : FeatureMachineMonadic A F S)
                 → FeatureMachineMonadic A (F × (FeatureNOAC noa)) S
NoacMAddFeature noa fm = extendFeatureFMachMonadic fm

NoacMAdaptFeature : {A F : Set}{S : Set}(noa : NOAC)
                    (fm : FeatureMachineMonadic A (F × (FeatureNOAC noa)) (StatesBasic ⊎ (S ⊎ ⊤)))
                     →  FeatureMachineMonadic A (F × (FeatureNOAC noa)) (StatesBasic ⊎ (S ⊎ ⊤))
NoacMAdaptFeature noa fm (f , yesNOAC .noa)
                             (position prescribeMed) =
                               addBtn2StateMachine
                                 (fm (f , yesNOAC noa) (position prescribeMed))
                                 (noacName noa)
                                 (continue newState)
NoacMAdaptFeature noa fm (f , selection) s = fm (f , selection) s

NoacFeatureMachine : {A F : Set}{S : Set}(noa : NOAC)
      (fm : FeatureMachineMonadic A F (StatesBasic ⊎ S))
      → FeatureMachineMonadic A (F × FeatureNOAC noa) (StatesBasic ⊎ (S ⊎ ⊤))
NoacFeatureMachine noa fm = NoacMAdaptFeature
                        noa
                        (NoacMAddNewState
                          noa
                          (NoacMAddFeature noa fm))


NoacMachine : (noa :  NOAC ) → StateMachine (StatesCallMachine ⊎
                                         (⊤ × FeatureNOAC noa)
                                         × (StatesBasic ⊎ (⊥ ⊎ ⊥) ⊎ ⊤))
-- \GUIFeaturesMonadicExamplePaper
NoacMachine noa =
  combineStateFeatureMachine
  (callMachineFeatured triv noa)
  (NoacFeatureMachine noa (mapFeatureMach (λ _ → enterCrCl) basicMachine))

noacMachineCompiled : GUI
noacMachineCompiled = compileToGUI' (NoacMachine dabigatran) (position enterCrCl)


main : NativeIO Unit
main = compileRegularGUI noacMachineCompiled