
   0 | module Chem.Types
   1 | 
   2 | import public Data.List.Quantifiers.Extra
   3 | import public Data.Refined
   4 | import public Data.Refined.Bits16
   5 | import public Data.Refined.Bits8
   6 | import public Data.Refined.Int8
   7 | import Derive.Finite
   8 | import Derive.Prelude
   9 | import Derive.Refined
  10 | 
  11 | %default total
  12 | %language ElabReflection
  13 | 
  14 | --------------------------------------------------------------------------------
  15 | --          Atomic Number
  16 | --------------------------------------------------------------------------------
  17 | 
  18 | ||| Proof that a number is in the range [1,118]
  19 | public export
  20 | 0 IsAtomicNr : Bits8 -> Type
  21 | IsAtomicNr = FromTo 1 118
  22 | 
  23 | ||| A refined integer in the range [1,118]
  24 | public export
  25 | record AtomicNr where
  26 |   constructor MkAtomicNr
  27 |   value : Bits8
  28 |   {auto 0 prf : IsAtomicNr value}
  29 | 
  30 | namespace AtomicNr
  31 |   %runElab derive "AtomicNr" [Show,Eq,Ord,RefinedInteger]
  32 | 
  33 | --------------------------------------------------------------------------------
  34 | --          Mass Number
  35 | --------------------------------------------------------------------------------
  36 | 
  37 | public export
  38 | record MassNr where
  39 |   constructor MkMassNr
  40 |   value : Bits16
  41 |   {auto 0 prf : FromTo 1 511 value}
  42 | 
  43 | export %inline
  44 | Interpolation MassNr where
  45 |   interpolate = show . value
  46 | 
  47 | namespace MassNr
  48 |   %runElab derive "MassNr" [Show,Eq,Ord,RefinedInteger]
  49 | 
  50 | --------------------------------------------------------------------------------
  51 | --          Abundance
  52 | --------------------------------------------------------------------------------
  53 | 
  54 | public export %inline
  55 | MinAbundanceValue : Double
  56 | MinAbundanceValue = 1.0e-100
  57 | 
  58 | public export
  59 | IsAbundance : Double -> Bool
  60 | IsAbundance v = v >= MinAbundanceValue && v <= 1.0
  61 | 
  62 | public export
  63 | record Abundance where
  64 |   constructor MkAbundance
  65 |   value : Double
  66 |   {auto 0 prf : Holds IsAbundance value}
  67 | 
  68 | export %inline
  69 | Interpolation Abundance where
  70 |   interpolate = show . value
  71 | 
  72 | namespace Abundance
  73 |   %runElab derive "Abundance" [Show,Eq,Ord,RefinedDouble]
  74 | 
  75 | public export %inline
  76 | multAbundance : Abundance -> Abundance -> Abundance
  77 | multAbundance a1 a2 =
  78 |   let res = a1.value * a2.value
  79 |    in case hdec0 {p = Holds IsAbundance} res of
  80 |         Just0 _ => MkAbundance res
  81 |         Nothing0 => 1.0e-100
  82 | 
  83 | public export %inline
  84 | Semigroup Abundance where
  85 |   (<+>) = multAbundance
  86 | 
  87 | public export %inline
  88 | Monoid Abundance where
  89 |   neutral = 1.0
  90 | 
  91 | --------------------------------------------------------------------------------
  92 | --          Molecular Mass
  93 | --------------------------------------------------------------------------------
  94 | 
  95 | ||| Molecular mass in g/mol
  96 | |||
  97 | ||| The total mass of ordinary matter of the universe is assumed to be
  98 | ||| approximately 1.5 * 10^50 kg, so we probably shouldn't exceed that by too
  99 | ||| much.
 100 | public export %inline
 101 | MaxMolecularMass : Double
 102 | MaxMolecularMass = 1.0e60
 103 | 
 104 | public export %inline
 105 | IsMolecularMass : Double -> Bool
 106 | IsMolecularMass v = v >= 0.0 && v <= MaxMolecularMass
 107 | 
 108 | ||| Molecular mass (or molecular weight) in g/mol
 109 | public export
 110 | record MolecularMass where
 111 |   constructor MkMolecularMass
 112 |   value : Double
 113 |   {auto 0 prf : Holds IsMolecularMass value}
 114 | 
 115 | export %inline
 116 | Interpolation MolecularMass where
 117 |   interpolate = show . value
 118 | 
 119 | namespace MolecularMass
 120 |   %runElab derive "MolecularMass" [Show,Eq,Ord,RefinedDouble]
 121 | 
 122 | public export %inline
 123 | addMolecularMass : MolecularMass -> MolecularMass -> MolecularMass
 124 | addMolecularMass a1 a2 =
 125 |   let res = a1.value + a2.value
 126 |    in case hdec0 {p = Holds IsMolecularMass} res of
 127 |         Just0 _ => MkMolecularMass res
 128 |         Nothing0 => 1.0e60
 129 | 
 130 | public export %inline
 131 | multMolecularMass : Nat -> MolecularMass -> MolecularMass
 132 | multMolecularMass a1 a2 =
 133 |   let res = cast a1 * a2.value
 134 |    in case hdec0 {p = Holds IsMolecularMass} res of
 135 |         Just0 _ => MkMolecularMass res
 136 |         Nothing0 => 1.0e60
 137 | 
 138 | public export %inline
 139 | Semigroup MolecularMass where
 140 |   (<+>) = addMolecularMass
 141 | 
 142 | public export %inline
 143 | Monoid MolecularMass where
 144 |   neutral = 0.0
 145 | 
 146 | --------------------------------------------------------------------------------
 147 | --          Molar Mass
 148 | --------------------------------------------------------------------------------
 149 | 
 150 | ||| Molar mass in Da
 151 | public export
 152 | record MolarMass where
 153 |   constructor MkMolarMass
 154 |   value : Double
 155 |   -- we use the same range as for `MolecularMass` so that
 156 |   -- the two types are easily interconvertible
 157 |   {auto 0 prf : Holds IsMolecularMass value}
 158 | 
 159 | export %inline
 160 | Interpolation MolarMass where
 161 |   interpolate = show . value
 162 | 
 163 | namespace MolarMass
 164 |   %runElab derive "MolarMass" [Show,Eq,Ord,RefinedDouble]
 165 | 
 166 | export
 167 | molarMass : Double -> MolarMass
 168 | molarMass v =
 169 |   case hdec0 {p = Holds IsMolecularMass} v of
 170 |     Just0 _ => MkMolarMass v
 171 |     Nothing0 => if v < 0.0 then 0 else 1.0e60
 172 | 
 173 | export %inline
 174 | addMolarMass : MolarMass -> MolarMass -> MolarMass
 175 | addMolarMass a1 a2 = molarMass (a1.value + a2.value)
 176 | 
 177 | export %inline
 178 | Semigroup MolarMass where
 179 |   (<+>) = addMolarMass
 180 | 
 181 | export %inline
 182 | Monoid MolarMass where
 183 |   neutral = 0.0
 184 | 
 185 | export %inline
 186 | Cast MolecularMass MolarMass where
 187 |   cast (MkMolecularMass v) = MkMolarMass v
 188 | 
 189 | export %inline
 190 | Cast MolarMass MolecularMass where
 191 |   cast (MkMolarMass v) = MkMolecularMass v
 192 | 
 193 | public export
 194 | interface HasMolarMass a where
 195 |   ||| Extract the molecular mass of an element or isotope.
 196 |   ||| In case of an element, this returns the average molar mass
 197 |   ||| in case of an isotope, it's the same as `exactMass`.
 198 |   mass      : a -> MolarMass
 199 | 
 200 |   ||| Extract the exact molecular mass of an element or isotope.
 201 |   ||| In case of an `Elem`, this returns the exact mass of the most
 202 |   ||| abundant isotope.
 203 |   exactMass : a -> MolarMass
 204 | 
 205 | export
 206 | multByAbundance : Abundance -> MolarMass -> MolarMass
 207 | multByAbundance a m = molarMass (a.value * m.value)
 208 | 
 209 | --------------------------------------------------------------------------------
 210 | --          Charge
 211 | --------------------------------------------------------------------------------
 212 | 
 213 | public export
 214 | record Charge where
 215 |   constructor MkCharge
 216 |   value : Int8
 217 |   {auto 0 prf : FromTo (-15) 15 value}
 218 | 
 219 | export %inline
 220 | Interpolation Charge where
 221 |   interpolate = show . value
 222 | 
 223 | namespace Charge
 224 |   %runElab derive "Charge" [Show,Eq,Ord,RefinedInteger]
 225 | 
 226 | export
 227 | Finite Charge where
 228 |   values = mapMaybe refineCharge [(-16)..16]
 229 | 
 230 | ||| Increase a charge value by one.
 231 | |||
 232 | ||| Returns the unmodified input if it is already the maximal valid value.
 233 | export
 234 | incCharge : Charge -> Charge
 235 | incCharge x =
 236 |   case refineCharge $ x.value+1 of
 237 |     Nothing => x
 238 |     Just y  => y
 239 | 
 240 | ||| Decrease a charge value by one.
 241 | |||
 242 | ||| Returns the unmodified input if it is already the minimal valid value.
 243 | export
 244 | decCharge : Charge -> Charge
 245 | decCharge x =
 246 |   case refineCharge $ x.value-1 of
 247 |     Nothing => x
 248 |     Just y  => y
 249 | 
 250 | --------------------------------------------------------------------------------
 251 | --          HCount
 252 | --------------------------------------------------------------------------------
 253 | 
 254 | public export
 255 | record HCount where
 256 |   constructor MkHCount
 257 |   value : Bits8
 258 |   {auto 0 prf : value < 10}
 259 | 
 260 | export %inline
 261 | Interpolation HCount where
 262 |   interpolate = show . value
 263 | 
 264 | namespace HCount
 265 |   %runElab derive "HCount" [Show,Eq,Ord,RefinedInteger]
 266 | 
 267 | export
 268 | Finite HCount where
 269 |   values = mapMaybe refineHCount [0..9]
 270 | 
 271 | ||| Placeholder for atoms without implicit hydrogens.
 272 | |||
 273 | ||| We can use this instead of `Unit` (`()`), to signal that an atom
 274 | ||| does not have any implicit hydrogens, as oppsed to the implicit
 275 | ||| H-count not having been determined yet.
 276 | |||
 277 | ||| For instance, we can have an implementation of
 278 | ||| `Cast (Atom Elem c p r NoH t ch l) Formula`, because here we
 279 | ||| do not have to add any implicit hydrogens to such an atom,
 280 | ||| while no such implementation should be written for
 281 | ||| `Cast (Atom Elem c p r () t ch l) Formula`, because in this case,
 282 | ||| the `Unit` tag implies that implicit hydrogens have not been
 283 | ||| determined yet.
 284 | public export
 285 | data NoH = HasNoH
 286 | 
 287 | %runElab derive "NoH" [Show,Eq,Ord]
 288 | 
 289 | --------------------------------------------------------------------------------
 290 | --          Radicals
 291 | --------------------------------------------------------------------------------
 292 | 
 293 | ||| Type of radical if any.
 294 | public export
 295 | data Radical = NoRadical | Singlet | Doublet | Triplet
 296 | 
 297 | %runElab derive "Radical" [Show,Eq,Ord,Finite]
 298 | 
 299 | --------------------------------------------------------------------------------
 300 | --          Hybridization
 301 | --------------------------------------------------------------------------------
 302 | 
 303 | ||| Kinds of hybridization
 304 | public export
 305 | data Hybridization : Type where
 306 |   None        : Hybridization
 307 |   Planar      : Hybridization
 308 |   S           : Hybridization
 309 |   SP          : Hybridization
 310 |   SP2         : Hybridization
 311 |   SP3         : Hybridization
 312 |   SP3D1       : Hybridization
 313 |   SP3D2       : Hybridization
 314 |   Tetrahedral : Hybridization
 315 |   Octahedral  : Hybridization
 316 | 
 317 | %runElab derive "Hybridization" [Show,Eq,Ord,Finite]
 318 | 
 319 | --------------------------------------------------------------------------------
 320 | --          Bonds
 321 | --------------------------------------------------------------------------------
 322 | 
 323 | public export
 324 | data BondOrder = Single | Dbl | Triple
 325 | 
 326 | export %inline
 327 | Interpolation BondOrder where
 328 |   interpolate Single        = "1"
 329 |   interpolate Dbl           = "2"
 330 |   interpolate Triple        = "3"
 331 | 
 332 | %runElab derive "BondOrder" [Eq,Show,Ord]
 333 | 
 334 | --------------------------------------------------------------------------------
 335 | --          Error Type
 336 | --------------------------------------------------------------------------------
 337 | 
 338 | public export
 339 | 0 ChemRes : List Type -> Type -> Type
 340 | ChemRes es x = Either (HSum es) x
 341 |