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) =
    (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
    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)
                      (StatesBasic  fm .AddStateF  )
noacNewStateSM noa fm =
   (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)) =
                                       fm .GUIF (f , yesNOAC noa) (position (prescribeMedication ≥15)))
                                       (noacName noa)
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
    go : (m : GUIMethod (extendedState2GUI noa (prescribeMedication <15))) 
       (StatesBasic  extendedMachine noa .AddStateF)
       (extendedMachine noa .GUIF (tt , yesNOAC noa)) (position warfarin))
      -eventually-> warfarinStateExtended noa
    go (zero , z) = hasReached
    go (suc () , _)


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)