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
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
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
createTables : Connection → NativeIO Unit
createTables conn =
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))
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)
)
where
convert : List (List (String × SqlVal)) → Maybe (String × String)
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)
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)
postulate btn : FFIButton
postulate fr : FFIFrame
frmBtnTxtBox : Frame
frmBtnTxtBox = addBtn "OK" (addTxtBox "Enter Name" create-frame)
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)
hdlErrorGender : ∀ i → (name : String) → HandlerObject i frmErrorGender
hdlErrorGender i name .method {j} (btn , frm) =
changeGUI frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox j)
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)
hdlExam : ∀ i → (name : String) → HandlerObject i frmExam
hdlExam i name .method {j} (btn , frm) =
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 =
getGenderFromDB name
>>= λ {(just gender) →
hdlAnswerMaleFemale i name (string2Sex gender);
nothing → changeGUI frmErrorGender propOneBtn (hdlErrorGender i name) }
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 =
nativeConnectDB dbFile native>>= λ conn →
createTables conn native>>= λ _ →
insertPatientData conn native>>= λ _ →
nativeReturn _
main : NativeIO Unit
main = prepareDB native>>= λ _ →
compileProgram frmBtnTxtBox (black , propOneBtn) (hdlBtnTxtBox ∞)