0 | module Chem.Isotope
 1 |
 2 | import Chem.Data
 3 | import Chem.Elem
 4 | import Chem.Types
 5 | import Derive.Prelude
 6 |
 7 | %default total
 8 | %language ElabReflection
 9 |
10 | ||| An element paired with an optional mass number.
11 | |||
12 | ||| If the mass number is `Nothing`, a value of this type represents
13 | ||| a natural mixture of isotopes.
14 | public export
15 | record Isotope where
16 |   constructor MkI
17 |   elem : Elem
18 |   mass : Maybe MassNr
19 |
20 | %runElab derive "Isotope" [Show,Eq]
21 |
22 | export %inline
23 | Cast Isotope Elem where cast = elem
24 |
25 | export %inline
26 | Cast Elem Isotope where cast e = MkI e Nothing
27 |
28 | export %inline
29 | Cast Isotope AromElem where cast (MkI e _) = cast e
30 |
31 | export %inline
32 | Cast AromElem Isotope where cast (MkAE e _) = cast e
33 |
34 | export
35 | HasMolarMass Isotope where
36 |   mass (MkI e $ Just m) = maybe (mass e) exactMass (isotopeData e m)
37 |   mass (MkI e Nothing)  = mass e
38 |
39 |   exactMass (MkI e $ Just m) = maybe (exactMass e) exactMass (isotopeData e m)
40 |   exactMass (MkI e Nothing)  = exactMass e
41 |
42 | ||| An element paired with an optional mass number plus a
43 | ||| boolean flag representing aromaticity.
44 | |||
45 | ||| If the mass number is `Nothing`, a value of this type represents
46 | ||| a natural mixture of isotopes.
47 | public export
48 | record AromIsotope where
49 |   constructor MkAI
50 |   elem : Elem
51 |   mass : Maybe MassNr
52 |   arom : Bool
53 |   {auto 0 prf : ValidAromatic elem arom}
54 |
55 | %runElab derive "AromIsotope" [Show,Eq]
56 |
57 | export %inline
58 | Cast AromIsotope Elem where cast = elem
59 |
60 | export %inline
61 | Cast Elem AromIsotope where cast e = MkAI e Nothing False
62 |
63 | export %inline
64 | Cast AromIsotope AromElem where cast (MkAI e m a) = MkAE e a
65 |
66 | export %inline
67 | Cast AromElem AromIsotope where cast (MkAE e a) = MkAI e Nothing a
68 |
69 | export %inline
70 | Cast AromIsotope Isotope where cast (MkAI e m a) = MkI e m
71 |
72 | export %inline
73 | Cast Isotope AromIsotope where cast (MkI e m) = MkAI e m False
74 |
75 | export
76 | HasMolarMass AromIsotope where
77 |   mass (MkAI e (Just m) _) = maybe (mass e) exactMass (isotopeData e m)
78 |   mass (MkAI e Nothing _)  = mass e
79 |
80 |   exactMass (MkAI e (Just m) _) = maybe (exactMass e) exactMass (isotopeData e m)
81 |   exactMass (MkAI e Nothing _)  = exactMass e
82 |