-- \GUIFeaturesPartEightMedicationPaper
module GUI.GUIFeaturesPart8MedicationPaper where

open import Data.Unit renaming (⊤ to Void)
open import Data.Empty renaming (⊥ to ∅)
open import Data.List
open import Data.Product
open import Data.Sum renaming (inj₁ to position; inj₂ to extended)
open import Data.String.Base

open import Data.Fin

open import NativeIO

open import GUI.GUIDefinitions

open import GUI.GUIModelVers3 using (GuiState ; state ; notStarted; _-eventually->_; next; hasReached)

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

open import GUI.GUIFeatures using (FeatureTea; FeatureCancel; FeatureFree; yesTea; yesCancel; noFree; yesFree)
open import GUI.GUIFeaturesPart2Paper using (StateMachine ; MachineState; simpleSMState; addBtn2StateMachine;disjointChoiceState;addChoice2State)
--(SMachineState; fSM; handlSM; SMachine; simpleSMState; addBtn2StateMachine) --hiding (FMachine)
--open import GUI.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel; main1 ; main2)

open import GUI.GUIFeaturesPart8Paper using (FeatureMachine; FeatureMachineNaive; newState; addStateToFeatureMachine; extendFeatureFMachineNaive ; addFeatureToFeatureMachine)

open import GUI.GUIFeaturesPart5extendedMedication using (RenalCat ; NOAC ; Medication ; StatesBasic ;
                                                          enterCrCl ; prescribeMedication ; warfarin ; dischargePatient ;
                                                          <15 ; ≥15 ; noac ; FeatureNOAC;
                                                          yesNOAC ; noNOAC ;
                                                          dabigatran ; apixaban) renaming (noacName to noac2Name)


{-
We can probably show:
∀ f : Features -> fm : (NOAC (basemachine)) -> warfarinTheorem holds

but ∀ f1 f2 : Features ->  theoremHolds ...
This cannot work in general or is not easy to implement

but since both the basic machine with Warfarin and
the feature machines of the NOACs pattern match on the renalCat, we can perhaps show:
  if the renalCat is "<15", then any NOAC in any feature combinaton, cannot be prescribed.

-}


-- \GUIFeaturesPartEightMedicationPaper
basicMachine : FeatureMachine Void StatesBasic ∅
basicMachine f (position enterCrCl) =
  disjointChoiceState  "CrCl < 15"  (position (prescribeMedication <15))
                       "CrCl ≥ 15"  (position (prescribeMedication ≥15))
basicMachine f (position (prescribeMedication renalVal)) =
  simpleSMState "Warfarin" (position warfarin)
basicMachine f (position warfarin) =
  simpleSMState "Warfarin prescribed" (position (dischargePatient warfarin))
basicMachine f (position (dischargePatient x)) =
  simpleSMState "Discharge patient" (position enterCrCl)
basicMachine f (extended ())

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


{- add the new state to the feature machine -}
-- \GUIFeaturesPartEightMedicationPaper
NoacMAddNewState : {F S : Set}(noa : NOAC)
                   → (fm :  FeatureMachine F StatesBasic S)
                   → FeatureMachine F StatesBasic(S ⊎ Void)
NoacMAddNewState noa fm = addStateToFeatureMachine fm (noacNewStateSM noa)


{- add a dummy feature NOAC to the feature machine -}
-- \GUIFeaturesPartEightMedicationPaper
NoacMAddFeature : {F B S : Set}(noa : NOAC)(fm : FeatureMachine F B S)
                 → FeatureMachine (F × (FeatureNOAC noa)) B S
NoacMAddFeature noa fm = addFeatureToFeatureMachine fm


-- \GUIFeaturesPartEightMedicationPaper
NoacMAdaptFeature :
    {F S : Set}(noa : NOAC)
    (fm : FeatureMachine (F × (FeatureNOAC noa)) StatesBasic (S ⊎ Void))
    →  FeatureMachine (F × (FeatureNOAC noa)) StatesBasic (S ⊎ Void)
NoacMAdaptFeature noa fm  (f , yesNOAC .noa)
                          (position (prescribeMedication  ≥15))
    = addChoice2State  (fm (f , yesNOAC noa) (position (prescribeMedication  ≥15)))
                      (noac2Name noa) newState
NoacMAdaptFeature noa fm (f , selection) s = fm (f , selection) s


NoacFeatureMachine : {F : Set}{S : Set}(noa : NOAC)
     → FeatureMachineNaive F  (StatesBasic ⊎ S)
     → FeatureMachineNaive (F × FeatureNOAC noa) (StatesBasic ⊎ (S ⊎ Void))
-- \GUIFeaturesPartEightMedicationPaper
NoacFeatureMachine noa fm = NoacMAdaptFeature noa
                            (NoacMAddNewState noa
                            (NoacMAddFeature noa fm))

NoacFeatureMachine' : (noa : NOAC)
     → FeatureMachineNaive (Void × FeatureNOAC noa) (StatesBasic ⊎ (∅  ⊎ Void))

NoacFeatureMachine' noa =  NoacMAdaptFeature noa
                          (NoacMAddNewState noa
                          (NoacMAddFeature noa basicMachine))



NoacFeatureMachine2 : (noa1 noa2 : NOAC)
      → FeatureMachineNaive ((Void × FeatureNOAC noa2) × FeatureNOAC noa1)
                            (StatesBasic ⊎ (∅ ⊎ Void) ⊎ Void)
      --(Void × FeatureNOAC noa1 × FeatureNOAC noa2) (StatesBasic ⊎ (∅ ⊎ Void ⊎ Void))
-- \GUIFeaturesPartEightMedicationPaper
NoacFeatureMachine2 noa1 noa2 =
    NoacFeatureMachine noa1 (NoacFeatureMachine noa2 basicMachine)







NoacFeatureMachine2GUI : {F : Set}{S : Set}(f : F)(noa : NOAC)(state : StatesBasic ⊎ S ⊎ Void)
      (fm : FeatureMachineNaive F (StatesBasic ⊎ S))
      → GUI
-- \GUIFeaturesPartEightMedicationPaper
NoacFeatureMachine2GUI {F}{S} f noa sta fm =
  compile2GUI ((NoacFeatureMachine noa fm) (f , yesNOAC noa)) sta
--  where
--    machine : FeatureMachineNaive (F × FeatureNOAC noa) (StatesBasic ⊎ S ⊎ Void)
--    machine = (NoacFeatureMachine noa fm)


NoacFeatureMachine2GUIState : {F : Set}{S : Set}(f : F)(noa : NOAC)(state : StatesBasic ⊎ S ⊎ Void)
      (fm : FeatureMachineNaive F (StatesBasic ⊎ S))
      → GuiState
NoacFeatureMachine2GUIState {F}{S} f noa sta fm =
  state
    (NoacFeatureMachine2GUI f noa sta fm)
    notStarted


--
-- States (non generic version is 1 NOAC Feature + Base)
--
prescribeMedicationStateExtendedGeneric : {F : Set}{S : Set}(noa : NOAC)
                                      → (rCat : RenalCat)
                                      → FeatureMachineNaive F (StatesBasic ⊎ S)
                                      → F
                                      → GuiState
prescribeMedicationStateExtendedGeneric {F} noa rCat machine f =
  NoacFeatureMachine2GUIState
    (f , yesNOAC noa)
    noa
    (position (prescribeMedication rCat))
    (NoacFeatureMachine noa machine)


prescribeMedicationStateExtended : (noa : NOAC) → (rCat : RenalCat) → GuiState
prescribeMedicationStateExtended  noa rCat =
  prescribeMedicationStateExtendedGeneric noa rCat basicMachine _



prescribeMedicationState :
  (noa1 : NOAC)
  (noa2 : NOAC)
   → (rCat : RenalCat)
   → GuiState
prescribeMedicationState noa1 noa2 rCat =
  prescribeMedicationStateExtendedGeneric
    noa2
    rCat
    (NoacFeatureMachine noa1 basicMachine)
    (tt , yesNOAC noa1)


warfarinStateExtendedGeneric : {F : Set}{S : Set}(noa : NOAC)
                                      → FeatureMachineNaive F (StatesBasic ⊎ S)
                                      → F
                                      → GuiState
warfarinStateExtendedGeneric {F} noa machine f =
  NoacFeatureMachine2GUIState
    (f , yesNOAC noa)
    noa
    (position warfarin)
    (NoacFeatureMachine noa machine)


warfarinStateExtended : (noa : NOAC) → GuiState
warfarinStateExtended noa =
  warfarinStateExtendedGeneric noa basicMachine _


warfarinState :
  (noa1 : NOAC)
  (noa2 : NOAC)
   → GuiState
warfarinState noa1 noa2 =
  warfarinStateExtendedGeneric
    noa2
    (NoacFeatureMachine noa1 basicMachine)
    (tt , yesNOAC noa1)

-- drop the 'extended'

-- \GUIFeaturesPartEightMedicationPaper
theoremWarfarin : ∀ (noa1 noa2 : NOAC) →
  prescribeMedicationState noa1 noa2 <15 -eventually->  warfarinState noa1 noa2
theoremWarfarin noa1 noa2 = next go
  where
    go : (m
       : GUIMethod
         (NoacFeatureMachine2GUI ((tt , yesNOAC noa1) , yesNOAC noa2) noa2
          (position (prescribeMedication <15))
          (NoacFeatureMachine noa2 (NoacFeatureMachine noa1 basicMachine)))) →
      state
      (compile2GUI -- (StatesBasic ⊎ ((∅ ⊎ Void) ⊎ Void) ⊎ Void)
       (NoacFeatureMachine noa2
        (NoacFeatureMachine noa2 (NoacFeatureMachine noa1 basicMachine)) -- TODO: ERROR DOUBLE noa2!!
        (((tt , yesNOAC noa1) , yesNOAC noa2) , yesNOAC noa2))
       (position warfarin))
      notStarted
      -eventually-> warfarinState noa1 noa2
    go (zero , _) = hasReached
    go (suc () , _)


theoremWarfarinExtended : (noa : NOAC) → (prescribeMedicationStateExtended noa <15) -eventually-> (warfarinStateExtended noa)
theoremWarfarinExtended noa = next go
  where
    go : (m
       : GUIMethod
         (NoacFeatureMachine2GUI (tt , yesNOAC noa) noa
          (position (prescribeMedication <15))
          (NoacFeatureMachine noa basicMachine))) →
      state
      (compile2GUI -- (StatesBasic ⊎ (∅ ⊎ Void) ⊎ Void)
       (NoacFeatureMachine noa (NoacFeatureMachine noa basicMachine)
        ((tt , yesNOAC noa) , yesNOAC noa))
       (position warfarin))
      notStarted
      -eventually-> warfarinStateExtended noa
    go (zero , z) = hasReached
    go (suc () , _)

mainBasic : NativeIO Unit
mainBasic = compileStateMachine (basicMachine _) (position enterCrCl)

mainOld : NativeIO Unit
mainOld = compileStateMachine
         (NoacFeatureMachine {Void}  dabigatran basicMachine  (_ , yesNOAC dabigatran)) (position enterCrCl) --()


main : NativeIO Unit
-- \GUIFeaturesPartEightMedicationPaper
main = compileRegularGUI (NoacFeatureMachine2GUI _ dabigatran (position enterCrCl) basicMachine)