Tentative de modélisation de prescriptions pharmaceutiques en Idris

Pharma.idr

data Actif : Type where
  Paracetamol : Actif
  Morphine : Actif

record Substance where
  constructor MkSubstance
  principeActif : Actif
  dosageMg : Nat

data Patient : Type where
   Adulte : Patient
   Enfant : (poids : Nat) -> Patient

data Posologie : Type where
  Acceptable : Posologie
  Dangereuse : Posologie
  Mortelle : Posologie

dosage : Patient -> Substance -> Posologie
dosage Adulte (MkSubstance Paracetamol dosageMg) =
  if dosageMg <= 4
  then Acceptable
  else if dosageMg <= 10
       then Dangereuse
       else Mortelle
dosage Adulte (MkSubstance Morphine dosageMg) =
  if dosageMg <= 1
  then Acceptable
  else if dosageMg <= 2
       then Dangereuse
       else Mortelle
dosage (Enfant poids) (MkSubstance Paracetamol dosageMg) =
  case (poids `divMod` 10) of
   (MkDivMod quotient remainder remainderSmall) => case isLTE dosageMg quotient of
       (Yes prf) => ?hole_0
       (No contra) => ?hole_


dosage (Enfant poids) (MkSubstance Morphine dosageMg) =
  if dosageMg > 0 then Mortelle else Acceptable

Vecteur : Type
Vecteur = Nat

data Preparation : (p : Patient) -> (poso : Posologie) -> Type where
  Prep : (substance : Substance) -> Preparation p (dosage p substance)

preparation : (patient : Patient) -> (preparation : Preparation patient poso) -> Dec (poso = Acceptable)
preparation Adulte (Prep (MkSubstance Paracetamol patient)) = ?hole___1
preparation (Enfant poids) (Prep (MkSubstance Paracetamol patient)) with (poids `divMod` 9)
  preparation (Enfant (remainder + (quotient * 10))) (Prep (MkSubstance Paracetamol dosage)) | (MkDivMod quotient remainder remainderSmall) =
     case isLTE dosage quotient of
       (Yes prf) => Yes ?hole1
       (No contra) => ?hole____
preparation Adulte (Prep (MkSubstance Morphine patient)) = ?hole__0
preparation (Enfant poids) (Prep (MkSubstance Morphine Z)) = Yes Refl
preparation (Enfant poids) (Prep (MkSubstance Morphine (S x))) = No $ \ Refl impossible