0 | module Chem.Atom
  1 |
  2 | import Chem.Data
  3 | import Chem.Elem
  4 | import Chem.Formula
  5 | import Data.Maybe.Upper
  6 | import Data.Nat
  7 | import Derive.Prelude
  8 |
  9 | %language ElabReflection
 10 | %default total
 11 |
 12 | ||| Generic atom type
 13 | |||
 14 | ||| Depending on an atom's origin and use case, different
 15 | ||| fields hold values of different types. Typically, if a
 16 | ||| field holds no information of interest, the corresponding
 17 | ||| type should be set to `Unit` (`()`).
 18 | |||
 19 | ||| @el  : Element label. This can be `Elem`, `AromElem` or
 20 | |||        a more general type that can be used for queries
 21 | |||        for instance
 22 | |||
 23 | ||| @chg : Type representing the charge of an atom
 24 | |||
 25 | ||| @pos : Coordinates, representing the position of an atom
 26 | |||
 27 | ||| @rad : Type holding information about the atom being
 28 | |||        a radical or not
 29 | |||
 30 | ||| @hyd : Implicit hydrogen count
 31 | |||
 32 | ||| @tpe : Atom type. This is used to describe not only
 33 | |||        the chemical element but also the atom's connectivity
 34 | |||        and, possibly, hybridisation
 35 | |||
 36 | ||| @chr : Chirality information
 37 | |||
 38 | ||| @lbl : Generic label holding additional information. This is
 39 | |||        placed last, so that an atom becomes a `Traversable`
 40 | |||        w.r.t. the label
 41 | public export
 42 | record Atom (el,chg,pos,rad,hyd,tpe,chr,lbl : Type) where
 43 |   constructor MkAtom
 44 |   elem      : el
 45 |   charge    : chg
 46 |   position  : pos
 47 |   radical   : rad
 48 |   hydrogen  : hyd
 49 |   type      : tpe
 50 |   chirality : chr
 51 |   label     : lbl
 52 |
 53 | %runElab derive "Atom" [Show,Eq]
 54 |
 55 | export %inline
 56 | Functor (Atom e c p r h t ch) where
 57 |   map f = {label $= f}
 58 |
 59 | export %inline
 60 | Foldable (Atom e c p r h t ch) where
 61 |   foldr f acc at  = f at.label acc
 62 |   foldl f acc at  = f acc at.label
 63 |   null at         = False
 64 |   foldlM f acc at = f acc at.label
 65 |   toList at       = [at.label]
 66 |   foldMap f at    = f at.label
 67 |
 68 | public export
 69 | Traversable (Atom e c p r h t ch) where
 70 |   traverse f (MkAtom e c p r h t ch l) = MkAtom e c p r h t ch <$> f l
 71 |
 72 | export
 73 | Cast e Elem => Cast (Atom e c p r NoH t ch l) Formula where
 74 |   cast a = singleton (cast a.elem) 1
 75 |
 76 | export
 77 | Cast e Elem => Cast (Atom e c p r HCount t ch l) Formula where
 78 |   cast a = singleton (cast a.elem) 1 <+> singleton H (cast a.hydrogen.value)
 79 |
 80 | public export
 81 | interface HasMolecularMass a where
 82 |   molecularMass      : a -> MolecularMass
 83 |   exactMolecularMass : a -> MolecularMass
 84 |
 85 | export
 86 | HasMolecularMass NoH where
 87 |   molecularMass      _ = 0.0
 88 |   exactMolecularMass _ = 0.0
 89 |
 90 | export
 91 | HasMolecularMass HCount where
 92 |   molecularMass      m = multMolecularMass (cast m.value) (cast $ mass H)
 93 |   exactMolecularMass m = multMolecularMass (cast m.value) (cast $ exactMass H)
 94 |
 95 | export
 96 | HasMolarMass e => HasMolecularMass h => HasMolecularMass (Atom e c p r h t ch x) where
 97 |   molecularMass      a = cast (mass a.elem) <+> molecularMass a.hydrogen
 98 |   exactMolecularMass a =
 99 |     cast (exactMass a.elem) <+> exactMolecularMass a.hydrogen
100 |