-- \GUIFeaturesMonadicExampleAdvancedPaper
module GUI.GUIFeaturesMonadicExampleAdvancedPaper where

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

open import NativeIO

open import GUI.GUIDefinitions

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

open import GUI.GUIFeaturesPart2Paper using (MachineState; StateMachine; simpleSMState; addBtn2StateMachine;disjointChoiceState)
open import GUI.GUIFeaturesPart8Paper using (newState)
open import GUI.GUIFeaturesMonadicPaper

open import GUI.GUIFeaturesPart5extendedMedication using (NOAC; FeatureNOAC; yesNOAC ; noacName  ;dabigatran ; noac ; noNOAC)
open import GUI.GUIFeaturesMonadicExamplePaper using (continue; terminate)


data Medication : Set where
  warfarin : Medication
  heparin  : Medication
  noac     : NOAC → Medication


{-
This state machine allows for run-time feature adaption according to the emergencyRoom requirements
of the prescription workflow. For example, the E.R. doesn't need to prescribe NOAC medications
but might additionally need to treat the patient.
-}
data StatesCallMachine : Set where
  enterCrCl        : StatesCallMachine
  emergencyRoom    : StatesCallMachine
  startState       : StatesCallMachine

{-
This is the workflow that is executed by both departments in the same manner.
Therefore, it is the base workflow .
-}
data StatesBasic : Set where
  prescribeMed      : StatesBasic
  warfarin          : StatesBasic
  heparin           : StatesBasic
  dischargePatient  : Medication → StatesBasic

{-
This is the additional feature for the E.R. room to treat a patient.
We compose it via run-time feature adaption to show the capabilities of the system.
-}
data FeatureTreatment : Set where
  yesTreatment noTreatment : FeatureTreatment


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

callMachine noa emergencyRoom =
  --
  -- Note: the E.R. department does additional blood work, such as testing for liver disease
  -- 
  disjointChoiceState "Hepatic impairment"  (terminate (noNOAC noa , yesTreatment , extended (extended triv)))
                      "Liver function o.k." (terminate (noNOAC noa , yesTreatment , extended (extended triv)))
callMachine noa startState =
  --
  -- Run-time feature adaption for the respective department (either emergency room department or anticoagulant clinit)
  --
  disjointChoiceState  "Adapt for E.R."  (continue emergencyRoom)
                       "Adapt for Clinic" (continue enterCrCl)


basicMachine : FeatureMachineMonadic ⊤  ⊤ (StatesBasic ⊎ (⊥ ⊎ ⊥))
basicMachine f (position prescribeMed) =
  disjointChoiceState "Warfarin" (position (continue warfarin))
                      "Heparin"  (position (continue heparin))
basicMachine f (position warfarin) =
  simpleSMState "Warfarin prescribed" (position (continue (dischargePatient warfarin)))
basicMachine f (position heparin) =
  simpleSMState "Heparin prescribed" (position (continue (dischargePatient heparin)))
  
basicMachine f (position (dischargePatient x)) =
   simpleSMState "Discharge patient" (terminate _)
basicMachine f (extended (position ()))
basicMachine f (extended (extended ()))



--
-- Below is the feature definition for NOAC medications
--

{- handler for the new state to be added to the noac feature machine -}
noacNewStateSM : {A  : Set} {Extra : Set}(noa : NOAC)
                → MachineState ((StatesBasic ⊎ Extra ⊎ ⊤) ⊎ A)
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 (without any adaptions yet) 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

{- final adaption according to feature -}
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


--
-- Below is the feature definition for the patient treatment in the E.R. room
--
--

noacNewStateSMnoTreatment : {A  : Set} {Extra : Set}(noa : NOAC)
                → MachineState ((StatesBasic ⊎ Extra ⊎ ⊤) ⊎ A)
noacNewStateSMnoTreatment noa = simpleSMState "no Treatment" (continue (position (dischargePatient (noac noa))))

NoacMAddNewStateTreatment : {A : Set}{F : Set}{S : Set}(noa : NOAC)
                         → (fm :  FeatureMachineMonadic A F (StatesBasic ⊎ S))
                         → FeatureMachineMonadic A F (StatesBasic ⊎ (S ⊎ ⊤))
NoacMAddNewStateTreatment noa fm = extendFMachFixedState1Monadic fm (noacNewStateSMnoTreatment noa)


NoacMAddFeatureTreatment : {A F : Set}{S : Set}(noa : NOAC)
                (fm : FeatureMachineMonadic A F S)
                 → FeatureMachineMonadic A (F × FeatureTreatment) S
NoacMAddFeatureTreatment noa fm = extendFeatureFMachMonadic fm


--
-- Workflow adaption for patient treatment in the E.R. room
--
NoacMAdaptFeatureTreatment : {A F : Set}{S : Set}(noa : NOAC)
                    (fm : FeatureMachineMonadic A (F × FeatureTreatment) (StatesBasic ⊎ (S ⊎ ⊤)))
                     →  FeatureMachineMonadic A (F × FeatureTreatment) (StatesBasic ⊎ (S ⊎ ⊤))
NoacMAdaptFeatureTreatment noa fm (f , yesTreatment) (inj₂ (inj₂ tt))
                              =
                              disjointChoiceState  "Antiarrhythmic drug" (continue (continue prescribeMed))
                                                   "No treatment" (continue (continue prescribeMed))

NoacMAdaptFeatureTreatment noa fm (f , selection) s = fm (f , selection) s



--
-- Below we compose the base workflow with the feature 'NOAC'
-- In this way we get the workflow for the Anticoagulant Clinic
--

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

--
-- Here we compose the Anticoagulant Clinit workflow
-- with the workflow that is needed for the E.R. room
--

NoacFeatureMachine :  {S : Set}(noa : NOAC)
       (fm : FeatureMachineMonadic StatesCallMachine ⊤ (StatesBasic ⊎ S)) →
       (_ × FeatureNOAC noa) × FeatureTreatment → StateMachineMonadic _ (StatesBasic ⊎ (S ⊎ ⊤) ⊎ ⊤)
NoacFeatureMachine = λ noa fm  →
   NoacMAdaptFeatureTreatment{_}{_ × FeatureNOAC noa} -- <-- add run-time feature adaption for the E.R. room
                        noa
                        (NoacMAddNewStateTreatment
                          noa
                          (NoacMAddFeatureTreatment noa
                           (NoacFeatureMachine1 noa fm))) -- <--- compose with Anticoagulant Clinic


-- \GUIFeaturesMonadicExamplePaper
composedMachine : (noa :  NOAC ) → StateMachine (StatesCallMachine ⊎
                                              Σ (Σ ⊤ (λ v → FeatureNOAC noa)) (λ v → FeatureTreatment) ×
                                              (StatesBasic ⊎ (_ ⊎ ⊤) ⊎ ⊤))
composedMachine = λ noa →
  combineStateFeatureMachine
  ((mapStateMachineReturnMonadic (λ { (fnoa , (fTreat , s)) → ((triv , fnoa) , fTreat) , s }) (callMachine noa)))
  (NoacFeatureMachine noa (mapFeatureMach (λ _ → startState) basicMachine))

--
-- Compile the composed workflow to an executable workflow with a GUI as its view
--
noacMachineCompiled : GUI
noacMachineCompiled =
--
-- we use here static workflow composition to select the availiable NOAC:
  compileToGUI' (composedMachine dabigatran) (position startState) 

--
-- Compile the executable workflow to a program with main (program entry):
--
main : NativeIO Unit
main = compileRegularGUI noacMachineCompiled