module GUI.GUIFeaturesPart5extendedMedication where

open import GUI.GUIFeatures
open import GUI.GUIFeaturesPart2
open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)
open import GUI.GUIFeaturesPart4 hiding ( cancelNewStateSM ; cancelStateAdded ; cancelFeatureAdded  )


open import Data.Fin
open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.Maybe.Base
open import Data.Product
open import Data.Sum renaming (inj₁ to position; inj₂ to extended)
open import Data.String.Base

open import NativeIO

open import GUI.GUIDefinitions

open import GUI.GUICompilationFeatures using (compileFeatureVM; compileFeatureVMToGUI)
import GUI.GUICompilation renaming (compile to compileRegularGUI)

open import GUI.GUIModelVers3

open import GUI.GUIFeaturesPart5extended using (newState)

data RenalCat : Set where
  <15 ≥15 : RenalCat

data NOAC : Set where
  dabigatran apixaban : NOAC


noacName : NOAC → String
noacName dabigatran = "Dabigatran"
noacName apixaban = "Apixaban"

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


data StatesBasic : Set where
  enterCrCl               : StatesBasic
  prescribeMedication     : RenalCat → StatesBasic
  warfarin                : StatesBasic
  dischargePatient        : Medication → StatesBasic




basicMachine : FMachine StatesBasic
basicMachine  .Features = ⊤
basicMachine  .AddStateF = ⊥
basicMachine .GUIF f (position enterCrCl) =
  addBtn2StateMachine
    (simpleSMState "CrCl < 15" (position (prescribeMedication <15)))
    "CrCl ≥ 15"
    (position (prescribeMedication ≥15))

basicMachine .GUIF f (position (prescribeMedication renVal)) =
  simpleSMState "Warfarin" (position warfarin)

basicMachine .GUIF f (position warfarin) =
  simpleSMState "Warfarin prescribed" (position (dischargePatient warfarin))

basicMachine .GUIF f (position (dischargePatient x)) =
  simpleSMState "Discharge patient" (position enterCrCl)
basicMachine .GUIF f (extended ())



basicState2GUI : StatesBasic → GUI
basicState2GUI x = compileFeatureVMToGUI basicMachine tt (position x)

basicState2GUIState : StatesBasic → GuiState
basicState2GUIState x = state (basicState2GUI x) notStarted


--
-- States
--
crClStateBasic : GuiState
crClStateBasic = basicState2GUIState enterCrCl

prescribeMedicationStateBasic : RenalCat → GuiState
prescribeMedicationStateBasic rCat = basicState2GUIState (prescribeMedication rCat)


warfarinStateBasic : GuiState
warfarinStateBasic = basicState2GUIState warfarin



theoremWarfarinBasic : crClStateBasic -eventually-> warfarinStateBasic
theoremWarfarinBasic = next go
  where
    go : (m : GUIMethod (basicState2GUI enterCrCl)) →
      guiNextaux (basicState2GUI enterCrCl) m
      (basicState2GUI enterCrCl .method m) skippedIOcmds
      -eventually-> warfarinStateBasic
    go (zero , tt) = next (λ _ → hasReached)
    go (suc zero , tt) = next (λ _ → hasReached)
    go (suc (suc ()) , tt)



{- handler for the new state to be added to the dabigatran machine -}

-- NOTE: this is the state that is similar to "Warfarin prescribed"
--       it means we are in the subsequent state of prescribing a medication
--
noacNewStateSM : (noa : NOAC)
                 (fm : FMachine StatesBasic)
                 →    SMachineState
                      (StatesBasic ⊎ fm .AddStateF ⊎ ⊤)
                      {-newState-}
noacNewStateSM noa fm =
 simpleSMState
   (noacName noa)
   (position (dischargePatient (noac noa)))


data FeatureNOAC : NOAC → Set where
  yesNOAC noNOAC : (noa : NOAC) → FeatureNOAC noa


{- add the new state to the feature machine -}
NoacMAddNewState : (noa : NOAC)
                   (fm : FMachine StatesBasic)
                   → FMachine StatesBasic
NoacMAddNewState noa fm =
  addOneStateFMachine fm (noacNewStateSM noa fm)


{- add a dummy feature "FeatureNoac" to the feature machine -}
NoacMAddFeature :  (noa : NOAC)
                  (fm : FMachine StatesBasic)
                  → FMachine StatesBasic
NoacMAddFeature noa fm = addDummyFeatures
                         (NoacMAddNewState noa fm)
                         (FeatureNOAC noa)


{- redefine in the feature machine one button -}
NoacRedefine : (noa : NOAC)
               (fm : FMachine StatesBasic)
              → FMachine StatesBasic
NoacRedefine noa fm .Features   = NoacMAddFeature noa fm .Features
NoacRedefine noa fm .AddStateF  = NoacMAddFeature noa fm .AddStateF
NoacRedefine noa fm .GUIF (f , yesNOAC .noa)
                                   (position (prescribeMedication  ≥15)) =
                                   addBtn2StateMachine
                                     (NoacMAddFeature
                                       noa
                                       fm .GUIF (f , yesNOAC noa) (position (prescribeMedication ≥15)))
                                       (noacName noa)
                                       newState
NoacRedefine noa fm .GUIF f  s = NoacMAddFeature noa fm .GUIF f s


extendedMachine : NOAC → FMachine StatesBasic
extendedMachine noa = (NoacRedefine noa basicMachine)

extendedState2GUI : NOAC → StatesBasic → GUI
extendedState2GUI noa x = compileFeatureVMToGUI (extendedMachine noa) (tt , yesNOAC noa) (position x)

extendedState2GUIState : NOAC → StatesBasic → GuiState
extendedState2GUIState noa x = state (extendedState2GUI noa x) notStarted


--
-- States
--
crClStateExtended : NOAC → GuiState
crClStateExtended noa = extendedState2GUIState noa enterCrCl

prescribeMedicationStateExtended : NOAC → RenalCat → GuiState
prescribeMedicationStateExtended noa rCat =
  extendedState2GUIState noa (prescribeMedication rCat)

warfarinStateExtended : NOAC → GuiState
warfarinStateExtended noa = extendedState2GUIState noa warfarin


theoremWarfarinExtended : (noa : NOAC) →
                          (prescribeMedicationStateExtended noa <15) -eventually-> (warfarinStateExtended noa)
theoremWarfarinExtended noa = next go
  where
    go : (m : GUIMethod (extendedState2GUI noa (prescribeMedication <15))) →
      state
      (GUI.GUICompilationFeatures.compileToGUI
       (StatesBasic ⊎ extendedMachine noa .AddStateF)
       (extendedMachine noa .GUIF (tt , yesNOAC noa)) (position warfarin))
      notStarted
      -eventually-> warfarinStateExtended noa
    go (zero , z) = hasReached
    go (suc () , _)


--
-- MAIN
--

mainNOAC : NOAC → NativeIO Unit
mainNOAC noa = compileFeatureVM (extendedMachine noa) (tt , yesNOAC noa) (position enterCrCl)


basicGUI : GUI
basicGUI = compileFeatureVMToGUI basicMachine tt (position enterCrCl)

mainBasic : NativeIO Unit
mainBasic = compileFeatureVM basicMachine tt (position enterCrCl)