open import Data.Bool
open import Relation.Nullary
open import Data.String renaming (_==_ to _==strb_; _++_ to _++s_)
module GUIgeneric.GUIModelAdvancedExampleExtendedWithDB where
open import GUIgeneric.Prelude renaming (inj₁ to secondButton; inj₂ to firstButton)
open import GUIgeneric.PreludeGUIWithDBTmp renaming (WxColor to Color) hiding (IOInterfaceˢ)
open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUIWithDB
open import GUIgeneric.GUIExampleWithDB using (oneColumnLayout;propOneBtn)
open import GUIgeneric.GUIExampleLibWithDB
open import StateSizedIO.writingOOsUsingIOVers4ReaderMethods renaming(execˢⁱ to execᵢ ; returnˢⁱ to returnᵢ)
open import GUIgeneric.GUIModelWithDB
open import GUIgeneric.GUIModelAdvancedWithDB
open import Data.Sum hiding (map)
open import GUIgeneric.GUIExampleWithDB using (addTxtBox; black; changeGUI)
renaming (addButton to addBtn)
open import Data.Integer
open import Data.Fin
-- DB imports
--
open import StateSizedIO.LIB.DB.Schema
open import StateSizedIO.LIB.DB.Serialization
open import StateSizedIO.LIB.DB.Query
open import StateSizedIO.LIB.DB.Interface
open import StateSizedIO.LIB.HDBC.HDBC
--
-- Database
--
dbFile : String
dbFile = "/tmp/patients.db"
patientTable : TableType
patientTable = ("name" , string , notNull , isPrimKey) ∷
("gender" , string , notNull , notPrimKey) ∷
("pain" , string , notNull , notPrimKey) ∷
[]
patientSchema : Schema
patientSchema = ("patients" , patientTable) ∷
[]
onlyTable : Fin 1
onlyTable = zero
--
-- Low level DB
--
createTables : Connection → NativeIO Unit
createTables conn =
-- drop tables
dropTableIfExisits conn "patients" native>>= λ _ →
nativeRun conn "CREATE TABLE patients (
name STRING NOT NULL,
gender STRING NOT NULL,
pain STRING NOT NULL,
PRIMARY KEY(name))"
[] native>>= λ _ →
nativeReturn _
insertPatientData : Connection → NativeIO Unit
insertPatientData conn = insertRows conn patientSchema onlyTable list
where
list : List (String × String × String × ⊤)
list = ("Isabelle" , "f" , "n" , tt) ∷
("Mary" , "f" , "y" , tt) ∷
("Peter" , "m" , "y" , tt) ∷
("John" , "m" , "n" , tt) ∷
[]
PatientTuples : Set
PatientTuples = List (String × String × String)
getPatientFromDB : (name : String) →
IO GuiLev1Interface ∞ (Maybe (String × String)) -- (List (List (String × SqlVal)))
getPatientFromDB = (\ (name : String) →
exec (dbCmd (connect dbFile)) λ conn →
exec (dbCmd (prepare conn ("SELECT * from patients where name = '" ++Str name ++Str "'"))) λ statement →
exec (dbCmd (execute statement [])) λ _ →
exec (dbCmd (fetchAllRowsAL' statement)) λ res →
exec (dbCmd (printList res)) λ _ →
return (convert res)-- res
)
where
convert : List (List (String × SqlVal)) → Maybe (String × String) -- gender × pain
convert [] = nothing
convert ([] ∷ xs₁) = nothing
convert ((x ∷ []) ∷ xs₁) = nothing
convert ((x ∷ x₁ ∷ []) ∷ xs₁) = nothing
convert (((fieldname1 , value1) ∷ (fieldname2 , value2) ∷ (fieldname3 , value3) ∷ xs) ∷ xs₁) = just (toStringSqlVal value2 , toStringSqlVal value3)
{- ([] ∷ []) = {!!}
convert (((fieldName , valueGender) ∷ (fieldName , valueGender) ∷ []) ∷ xs) = {!xs!}
-}
maybeStringString2Sting1 : Maybe (String × String) → Maybe String
maybeStringString2Sting1 (just (s0 , s1)) = just s0
maybeStringString2Sting1 nothing = nothing
maybeStringString2Sting2 : Maybe (String × String) → Maybe String
maybeStringString2Sting2 (just (s0 , s1)) = just s1
maybeStringString2Sting2 nothing = nothing
getGenderFromDB : (name : String) →
IO GuiLev1Interface ∞ (Maybe String)
getGenderFromDB name = getPatientFromDB name >>= λ s →
return (maybeStringString2Sting1 s)
getPainInfoFromDB : (name : String) →
IO GuiLev1Interface ∞ (Maybe String)
getPainInfoFromDB name = getPatientFromDB name >>= λ s →
return (maybeStringString2Sting2 s)
--
-- START GUI CODE
--
--
postulate btn : FFIButton
postulate fr : FFIFrame
-- private postulate strExample : String
frmBtnTxtBox : Frame
frmBtnTxtBox = addBtn "OK" (addTxtBox "Enter Name" create-frame)
-- mypropBtnTxtBox' : properties frmBtnTxtBox
-- mypropBtnTxtBox' : black , propOneBtn
oneBtnFrame : String → Frame
oneBtnFrame str = addBtn str create-frame
frmExam : Frame
frmExam = oneBtnFrame "Examination"
frmErrorPain : Frame
frmErrorPain = oneBtnFrame "Error in Db - no pain info"
frmErrorGender : Frame
frmErrorGender = oneBtnFrame "Error in Db - no gender info"
frmPainKill : Frame
frmPainKill = oneBtnFrame "Prescribe Painkillers"
frmPreg : Frame
frmPreg = oneBtnFrame "Check for Preg"
frmXRay : Frame
frmXRay = oneBtnFrame "X-Ray"
frmTreatm : Frame
frmTreatm = oneBtnFrame "Treatment"
frmDecideCheckups : Frame
frmDecideCheckups = oneBtnFrame "Decide On Checkups"
frmFinished : Frame
frmFinished = addTxtBox "Finished" create-frame
data Sex : Set where
male female : Sex
bool2Sex : Bool → Sex
bool2Sex true = female
bool2Sex false = male
string2Sex : String → Sex
string2Sex str = bool2Sex (str ==Str "f")
string2Bool : String → Bool
string2Bool str = (str ==Str "y")
mutual
hdlErrorPain : ∀ i → (name : String) → HandlerObject i frmErrorPain
hdlErrorPain i name .method {j} (btn , frm) =
changeGUI frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox j)-- frmExam propOneBtn (hdlExam j name)
hdlErrorGender : ∀ i → (name : String) → HandlerObject i frmErrorGender
hdlErrorGender i name .method {j} (btn , frm) =
changeGUI frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox j)-- frmExam propOneBtn (hdlExam j name)
-- changeGUI frmExam propOneBtn (hdlExam j name)
hdlBtnTxtBox : ∀ i → HandlerObject i frmBtnTxtBox
hdlBtnTxtBox i .method {j} (btn , ffitxtbox , frm) =
exec (getTextFromTxtBox ffitxtbox) λ name →
exec (putStrLn name) λ _ →
changeGUI frmExam propOneBtn (hdlExam i name)
-- return (noChange , hdlBtnTxtBox j)
hdlExam : ∀ i → (name : String) → HandlerObject i frmExam
hdlExam i name .method {j} (btn , frm) =
-- exec (putStrLn "Patient in Pain (y/n)?") λ _ →
-- exec getLine λ s →
getPainInfoFromDB name
>>= λ {(just pain) →
hdlAnswerPain i name (string2Bool pain) ;
nothing → changeGUI frmErrorPain propOneBtn (hdlErrorPain i name) }
hdlAnswerPain : (i : Size)(name : String)(b : Bool)
→ HandlerIOType i frmExam
hdlAnswerPain i name true =
changeGUI frmPainKill propOneBtn (hdlPainKill i name)
hdlAnswerPain i name false = hdlCheckMaleFemale i name
hdlCheckMaleFemale : {str : String} (i : Size) (name : String)
→ HandlerIOType i (oneBtnFrame str)
hdlCheckMaleFemale i name =
-- exec (putStrLn "Female or Male (f/m)?") λ _ →
-- exec getLine λ s →
getGenderFromDB name
>>= λ {(just gender) →
hdlAnswerMaleFemale i name (string2Sex gender);
nothing → changeGUI frmErrorGender propOneBtn (hdlErrorGender i name) }
-- hdlAnswerMaleFemale i name (string2Sex s)
hdlAnswerMaleFemale : (i : Size){str : String}(name : String)(g : Sex)
→ HandlerIOType i (oneBtnFrame str)
hdlAnswerMaleFemale i name female =
changeGUI frmPreg propOneBtn (hdlPreg i name )
hdlAnswerMaleFemale i name male =
changeGUI frmXRay propOneBtn (hdlXRay i name)
hdlPainKill : ∀ i → (name : String) → HandlerObject i frmPainKill
hdlPainKill i name .method {j} (btn , frm) = hdlCheckMaleFemale i name
hdlPreg : ∀ i → (name : String) → HandlerObject i frmPreg
hdlPreg i name .method {j} (btn , frm) =
changeGUI frmXRay propOneBtn (hdlXRay j name)
hdlXRay : ∀ i → (name : String) → HandlerObject i frmXRay
hdlXRay i name .method {j} (btn , frm) =
changeGUI frmTreatm propOneBtn (hdlTreatm j name)
hdlTreatm : ∀ i → (name : String) → HandlerObject i frmTreatm
hdlTreatm i name .method {j} (btn , frm) =
changeGUI frmDecideCheckups propOneBtn (hdlDecideCheckups j name)
hdlDecideCheckups : ∀ i → (name : String) → HandlerObject i frmDecideCheckups
hdlDecideCheckups i name .method {j} (btn , frm) =
changeGUI frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox j)
hdlFinished : ∀ i → (name : String) → HandlerObject i frmFinished
hdlFinished i name .method {j} ()
prepareDB : NativeIO Unit
prepareDB =
-- connect
nativeConnectDB dbFile native>>= λ conn →
createTables conn native>>= λ _ →
insertPatientData conn native>>= λ _ →
nativeReturn _
main : NativeIO Unit
main = prepareDB native>>= λ _ →
compileProgram frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox ∞)
{-
stateExam : ModelGuiState
stateExam = state frmExam propOneBtn
(hdlExam ∞) notStarted
stateExam₁ : (c : methodsG frmExam) → ModelGuiState
stateExam₁ = modelGuiNext stateExam
stateExam₂ : (c : methodsG frmExam) (str : String)
→ ModelGuiState
stateExam₂ c str = modelGuiNext (stateExam₁ c) str
stateExamNoPain₁ : (c : methodsG frmExam) → ModelGuiState
stateExamNoPain₁ c = (state frmExam propOneBtn (hdlExam ∞)
(started c
(exec' getLine λ str →
fmap ∞
(handlerReturnTypeToStateAndGuiObj
frmExam
propOneBtn (hdlExam ∞))
(hdlAnswerMaleFemale ∞ (string2Sex str)))))
stateExamNoPain₂ : (c : methodsG frmExam)
(str : String) → ModelGuiState
stateExamNoPain₂ c str = modelGuiNext (stateExamNoPain₁ c) str
statePreg : ModelGuiState
statePreg = state frmPreg propOneBtn
(hdlPreg ∞) notStarted
statePainKill : ModelGuiState
statePainKill = state frmPainKill propOneBtn
(hdlPainKill ∞) notStarted
statePainKill₁ : (c : methodsG frmPainKill) → ModelGuiState
statePainKill₁ c = modelGuiNext statePainKill c
statePainKill₂ : (c : methodsG frmPainKill)
(str : String) → ModelGuiState
statePainKill₂ c str = modelGuiNext (statePainKill₁ c) str
stateXRay : ModelGuiState
stateXRay = state frmXRay propOneBtn
(hdlXRay ∞) notStarted
stateTreatm : ModelGuiState
stateTreatm = state frmTreatm propOneBtn
(hdlTreatm ∞) notStarted
mutual
examGoesThruXRay :
(path : stateExam -gui-> stateTreatm)
→ path goesThru stateXRay
examGoesThruXRay (execᵢ c f) =
inj₂ (exam₁GoesThruXRay c (f _))
examGoesThruXRay (returnᵢ () )
exam₁GoesThruXRay : (c : methodsG frmExam)
(path : stateExam₁ c -gui-> stateTreatm)
→ path goesThru stateXRay
exam₁GoesThruXRay c (execᵢ str f) =
inj₂ (exam₂GoesThruXRay c str (f _))
exam₁GoesThruXRay c (returnᵢ ())
exam₂GoesThruXRay :
(c : methodsG frmExam) (str : String)
(path : stateExam₂ c str -gui-> stateTreatm)
→ path goesThru stateXRay
exam₂GoesThruXRay c str path with (string2Bool str)
... | true = painKillGoesThruXRay path
... | false = stateExamNoPain₁GoesThruXRay c path
stateExamNoPain₁GoesThruXRay : (c : methodsG frmExam)
(path : stateExamNoPain₁ c -gui-> stateTreatm)
→ path goesThru stateXRay
stateExamNoPain₁GoesThruXRay c (execᵢ str f) =
inj₂ (stateExamNoPain₂GoesThruXRay c str (f _))
stateExamNoPain₁GoesThruXRay c (returnᵢ ())
stateExamNoPain₂GoesThruXRay : (c : methodsG frmExam)(str : String)
(path : stateExamNoPain₂ c str -gui-> stateTreatm)
→ path goesThru stateXRay
stateExamNoPain₂GoesThruXRay c str path with (string2Sex str)
... | male = XRayGoesThruXRay path
... | female = checkPregGoesThruXRay path
painKillGoesThruXRay : (path : statePainKill -gui-> stateTreatm)
→ path goesThru stateXRay
painKillGoesThruXRay (execᵢ c f) = inj₂ (painKill₁GoesThruXRay c (f _))
painKillGoesThruXRay (returnᵢ ())
painKill₁GoesThruXRay : (c : methodsG frmPainKill)
(path : statePainKill₁ c -gui-> stateTreatm)
→ path goesThru stateXRay
painKill₁GoesThruXRay c (execᵢ str f) = inj₂ (painKill₂GoesThruXRay c str (f _))
painKill₁GoesThruXRay c (returnᵢ ())
painKill₂GoesThruXRay : (c : methodsG frmPainKill)
(str : String)
(path : statePainKill₂ c str -gui-> stateTreatm)
→ path goesThru stateXRay
painKill₂GoesThruXRay c str path with (string2Sex str)
... | male = XRayGoesThruXRay path
... | female = checkPregGoesThruXRay path
checkPregGoesThruXRay : (path : statePreg -gui-> stateTreatm)
→ path goesThru stateXRay
checkPregGoesThruXRay (execᵢ c f) = inj₂ (XRayGoesThruXRay (f _))
checkPregGoesThruXRay (returnᵢ ())
XRayGoesThruXRay : (path : stateXRay -gui-> stateTreatm)
→ path goesThru stateXRay
XRayGoesThruXRay path = goesThruSelf path
mutual
examEventuallyTreatm
: stateExam -eventually-> stateTreatm
examEventuallyTreatm = next λ c →
exam₁EventuallyTreatm c
exam₁EventuallyTreatm : (c : methodsG frmExam) →
stateExam₁ c -eventually-> stateTreatm
exam₁EventuallyTreatm c = next λ str → exam₂EventuallyTreatm c str
exam₂EventuallyTreatm :
(c : methodsG frmExam) (str : String)
→ (stateExam₂ c str) -eventually-> stateTreatm
exam₂EventuallyTreatm c str with (string2Bool str)
... | true = painKillEventuallyTreatm
... | false = examNoPain₁EventuallyTreatm c
painKillEventuallyTreatm : statePainKill -eventually-> stateTreatm
painKillEventuallyTreatm = next λ c → painKill₁EventuallyTreatm c
painKill₁EventuallyTreatm : (c : methodsG frmPainKill)
→ statePainKill₁ c -eventually-> stateTreatm
painKill₁EventuallyTreatm c = next λ str → painKill₂EventuallyTreatm c str
painKill₂EventuallyTreatm : (c : methodsG frmPainKill)
(str : String)
→ statePainKill₂ c str -eventually-> stateTreatm
painKill₂EventuallyTreatm c str with (string2Sex str)
... | male = xRayEventuallyTreatm
... | female = checkPregEventuallyTreatm
examNoPain₁EventuallyTreatm : (c : methodsG frmExam)
→ (stateExamNoPain₁ c) -eventually-> stateTreatm
examNoPain₁EventuallyTreatm c = next λ str →
examNoPain₂EventuallyTreatm c str
examNoPain₂EventuallyTreatm : (c : methodsG frmExam)
(str : String)
→ (stateExamNoPain₂ c str) -eventually-> stateTreatm
examNoPain₂EventuallyTreatm c str with (string2Sex str)
... | male = xRayEventuallyTreatm
... | female = checkPregEventuallyTreatm
checkPregEventuallyTreatm : statePreg -eventually-> stateTreatm
checkPregEventuallyTreatm = next λ c → xRayEventuallyTreatm
xRayEventuallyTreatm : stateXRay -eventually-> stateTreatm
xRayEventuallyTreatm = next λ c → treatmEventuallyTreatm
treatmEventuallyTreatm : stateTreatm -eventually-> stateTreatm
treatmEventuallyTreatm = hasReached
-}