0 | module Chem.Elem
  1 |
  2 | import public Chem.Types
  3 | import Derive.Finite
  4 | import Derive.Prelude
  5 | import Derive.Refined
  6 |
  7 | %language ElabReflection
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          The Elements
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| The chemical elements encoded as an enum type
 15 | public export
 16 | data Elem =
 17 |     H                                                                                  | He
 18 |   | Li | Be                                                   | B  | C  | N  | O  | F  | Ne
 19 |   | Na | Mg                                                   | Al | Si | P  | S  | Cl | Ar
 20 |   | K  | Ca | Sc | Ti | V  | Cr | Mn | Fe | Co | Ni | Cu | Zn | Ga | Ge | As | Se | Br | Kr
 21 |   | Rb | Sr | Y  | Zr | Nb | Mo | Tc | Ru | Rh | Pd | Ag | Cd | In | Sn | Sb | Te | I  | Xe
 22 |   | Cs | Ba | La
 23 |             | Ce | Pr | Nd | Pm | Sm | Eu | Gd
 24 |             | Tb | Dy | Ho | Er | Tm | Yb | Lu
 25 |                  | Hf | Ta | W  | Re | Os | Ir | Pt | Au | Hg | Tl | Pb | Bi | Po | At | Rn
 26 |   | Fr | Ra | Ac
 27 |             | Th | Pa | U  | Np | Pu | Am | Cm
 28 |             | Bk | Cf | Es | Fm | Md | No | Lr
 29 |                  | Rf | Db | Sg | Bh | Hs | Mt | Ds | Rg | Cn | Nh | Fl | Mc | Lv | Ts | Og
 30 |
 31 | %runElab derive "Elem" [Show, Eq, Ord, Finite]
 32 |
 33 | export %inline
 34 | Interpolation Elem where
 35 |   interpolate = show
 36 |
 37 | --------------------------------------------------------------------------------
 38 | --          Conversion from and to AtomicNr
 39 | --------------------------------------------------------------------------------
 40 |
 41 | ||| This is a proof that we can safely compute an atomic number
 42 | ||| from each element's index
 43 | export
 44 | 0 indexLemma : (e : Elem) -> IsAtomicNr (conIndexElem e + 1)
 45 |
 46 | ||| Compute the atomic number of an element
 47 | public export %inline
 48 | atomicNr : Elem -> AtomicNr
 49 | atomicNr e = MkAtomicNr (conIndexElem e + 1) @{indexLemma e}
 50 |
 51 | ||| Compute the element from an atomic number
 52 | public export
 53 | fromAtomicNr : AtomicNr -> Elem
 54 |
 55 | ||| Return the chemical symbol of an element.
 56 | public export %inline
 57 | symbol : Elem -> String
 58 | symbol = show
 59 |
 60 | --------------------------------------------------------------------------------
 61 | --          Basic Properties
 62 | --------------------------------------------------------------------------------
 63 |
 64 | export
 65 | isNobleGas : Elem -> Bool
 66 | isNobleGas He = True
 67 | isNobleGas Ne = True
 68 | isNobleGas Ar = True
 69 | isNobleGas Kr = True
 70 | isNobleGas Rn = True
 71 | isNobleGas _  = False
 72 |
 73 | export
 74 | isHalogen : Elem -> Bool
 75 | isHalogen F  = True
 76 | isHalogen Cl = True
 77 | isHalogen Br = True
 78 | isHalogen I  = True
 79 | isHalogen _  = False
 80 |
 81 | export
 82 | isNonmetal : Elem -> Bool
 83 | isNonmetal H  = True
 84 | isNonmetal C  = True
 85 | isNonmetal N  = True
 86 | isNonmetal P  = True
 87 | isNonmetal O  = True
 88 | isNonmetal S  = True
 89 | isNonmetal Se = True
 90 | isNonmetal e  = isNobleGas e || isHalogen e
 91 |
 92 | export
 93 | isMetalloid : Elem -> Bool
 94 | isMetalloid B  = True
 95 | isMetalloid Si = True
 96 | isMetalloid Ge = True
 97 | isMetalloid As = True
 98 | isMetalloid Sb = True
 99 | isMetalloid Te = True
100 | isMetalloid _  = False
101 |
102 | export
103 | isMetal : Elem -> Bool
104 | isMetal e = not (isNonmetal e || isMetalloid e)
105 |
106 | --------------------------------------------------------------------------------
107 | --          Aromaticity
108 | --------------------------------------------------------------------------------
109 |
110 | ||| Proof that only valid elements are marked as aromatic
111 | public export
112 | data ValidAromatic : Elem -> Bool -> Type where
113 |   VAB    : ValidAromatic B  True
114 |   VAC    : ValidAromatic C  True
115 |   VAN    : ValidAromatic N  True
116 |   VAO    : ValidAromatic O  True
117 |   VAP    : ValidAromatic P  True
118 |   VAS    : ValidAromatic S  True
119 |   VASe   : ValidAromatic Se True
120 |   VAAs   : ValidAromatic As True
121 |   VARest : ValidAromatic e False
122 |
123 | ||| An element paired with a boolean flag indicating whether the atom
124 | ||| in question is part of an aromatic system.
125 | public export
126 | record AromElem where
127 |   constructor MkAE
128 |   elem : Elem
129 |   arom : Bool
130 |   {auto 0 prf : ValidAromatic elem arom}
131 |
132 | %runElab derive "AromElem" [Show,Eq]
133 |
134 | export
135 | Interpolation AromElem where
136 |   interpolate (MkAE e b) = if b then toLower (show e) else show e
137 |
138 | export %inline
139 | Cast AromElem Elem where cast = elem
140 |
141 | export %inline
142 | Cast Elem AromElem where cast e = MkAE e False
143 |
144 | public export %inline
145 | nonAromElem : (e : Elem) -> AromElem
146 | nonAromElem e = MkAE e False
147 |
148 | public export %inline
149 | aromElem : (e : Elem) -> (0 p : ValidAromatic e True) => AromElem
150 | aromElem e = MkAE e True
151 |
152 | export
153 | Finite AromElem where
154 |   values =
155 |     [ aromElem B, aromElem C, aromElem N, aromElem O, aromElem P, aromElem S
156 |     , aromElem Se, aromElem As] ++ map nonAromElem values
157 |
158 | --------------------------------------------------------------------------------
159 | --          Implementations
160 | --------------------------------------------------------------------------------
161 |
162 | -- the following lengthy and not very interesting implementations
163 | -- are kept at the end of the file to get a better overview over the
164 | -- exported functions and types
165 |
166 | indexLemma H  = %search
167 | indexLemma He = %search
168 | indexLemma Li = %search
169 | indexLemma Be = %search
170 | indexLemma B  = %search
171 | indexLemma C  = %search
172 | indexLemma N  = %search
173 | indexLemma O  = %search
174 | indexLemma F  = %search
175 | indexLemma Ne = %search
176 | indexLemma Na = %search
177 | indexLemma Mg = %search
178 | indexLemma Al = %search
179 | indexLemma Si = %search
180 | indexLemma P  = %search
181 | indexLemma S  = %search
182 | indexLemma Cl = %search
183 | indexLemma Ar = %search
184 | indexLemma K  = %search
185 | indexLemma Ca = %search
186 | indexLemma Sc = %search
187 | indexLemma Ti = %search
188 | indexLemma V  = %search
189 | indexLemma Cr = %search
190 | indexLemma Mn = %search
191 | indexLemma Fe = %search
192 | indexLemma Co = %search
193 | indexLemma Ni = %search
194 | indexLemma Cu = %search
195 | indexLemma Zn = %search
196 | indexLemma Ga = %search
197 | indexLemma Ge = %search
198 | indexLemma As = %search
199 | indexLemma Se = %search
200 | indexLemma Br = %search
201 | indexLemma Kr = %search
202 | indexLemma Rb = %search
203 | indexLemma Sr = %search
204 | indexLemma Y  = %search
205 | indexLemma Zr = %search
206 | indexLemma Nb = %search
207 | indexLemma Mo = %search
208 | indexLemma Tc = %search
209 | indexLemma Ru = %search
210 | indexLemma Rh = %search
211 | indexLemma Pd = %search
212 | indexLemma Ag = %search
213 | indexLemma Cd = %search
214 | indexLemma In = %search
215 | indexLemma Sn = %search
216 | indexLemma Sb = %search
217 | indexLemma Te = %search
218 | indexLemma I  = %search
219 | indexLemma Xe = %search
220 | indexLemma Cs = %search
221 | indexLemma Ba = %search
222 | indexLemma La = %search
223 | indexLemma Ce = %search
224 | indexLemma Pr = %search
225 | indexLemma Nd = %search
226 | indexLemma Pm = %search
227 | indexLemma Sm = %search
228 | indexLemma Eu = %search
229 | indexLemma Gd = %search
230 | indexLemma Tb = %search
231 | indexLemma Dy = %search
232 | indexLemma Ho = %search
233 | indexLemma Er = %search
234 | indexLemma Tm = %search
235 | indexLemma Yb = %search
236 | indexLemma Lu = %search
237 | indexLemma Hf = %search
238 | indexLemma Ta = %search
239 | indexLemma W  = %search
240 | indexLemma Re = %search
241 | indexLemma Os = %search
242 | indexLemma Ir = %search
243 | indexLemma Pt = %search
244 | indexLemma Au = %search
245 | indexLemma Hg = %search
246 | indexLemma Tl = %search
247 | indexLemma Pb = %search
248 | indexLemma Bi = %search
249 | indexLemma Po = %search
250 | indexLemma At = %search
251 | indexLemma Rn = %search
252 | indexLemma Fr = %search
253 | indexLemma Ra = %search
254 | indexLemma Ac = %search
255 | indexLemma Th = %search
256 | indexLemma Pa = %search
257 | indexLemma U  = %search
258 | indexLemma Np = %search
259 | indexLemma Pu = %search
260 | indexLemma Am = %search
261 | indexLemma Cm = %search
262 | indexLemma Bk = %search
263 | indexLemma Cf = %search
264 | indexLemma Es = %search
265 | indexLemma Fm = %search
266 | indexLemma Md = %search
267 | indexLemma No = %search
268 | indexLemma Lr = %search
269 | indexLemma Rf = %search
270 | indexLemma Db = %search
271 | indexLemma Sg = %search
272 | indexLemma Bh = %search
273 | indexLemma Hs = %search
274 | indexLemma Mt = %search
275 | indexLemma Ds = %search
276 | indexLemma Rg = %search
277 | indexLemma Cn = %search
278 | indexLemma Nh = %search
279 | indexLemma Fl = %search
280 | indexLemma Mc = %search
281 | indexLemma Lv = %search
282 | indexLemma Ts = %search
283 | indexLemma Og = %search
284 |
285 | fromAtomicNr 6   = C
286 | fromAtomicNr 8   = O
287 | fromAtomicNr 7   = N
288 | fromAtomicNr 1   = H
289 | fromAtomicNr 2   = He
290 | fromAtomicNr 3   = Li
291 | fromAtomicNr 4   = Be
292 | fromAtomicNr 5   = B
293 | fromAtomicNr 9   = F
294 | fromAtomicNr 10  = Ne
295 | fromAtomicNr 11  = Na
296 | fromAtomicNr 12  = Mg
297 | fromAtomicNr 13  = Al
298 | fromAtomicNr 14  = Si
299 | fromAtomicNr 15  = P
300 | fromAtomicNr 16  = S
301 | fromAtomicNr 17  = Cl
302 | fromAtomicNr 18  = Ar
303 | fromAtomicNr 19  = K
304 | fromAtomicNr 20  = Ca
305 | fromAtomicNr 21  = Sc
306 | fromAtomicNr 22  = Ti
307 | fromAtomicNr 23  = V
308 | fromAtomicNr 24  = Cr
309 | fromAtomicNr 25  = Mn
310 | fromAtomicNr 26  = Fe
311 | fromAtomicNr 27  = Co
312 | fromAtomicNr 28  = Ni
313 | fromAtomicNr 29  = Cu
314 | fromAtomicNr 30  = Zn
315 | fromAtomicNr 31  = Ga
316 | fromAtomicNr 32  = Ge
317 | fromAtomicNr 33  = As
318 | fromAtomicNr 34  = Se
319 | fromAtomicNr 35  = Br
320 | fromAtomicNr 36  = Kr
321 | fromAtomicNr 37  = Rb
322 | fromAtomicNr 38  = Sr
323 | fromAtomicNr 39  = Y
324 | fromAtomicNr 40  = Zr
325 | fromAtomicNr 41  = Nb
326 | fromAtomicNr 42  = Mo
327 | fromAtomicNr 43  = Tc
328 | fromAtomicNr 44  = Ru
329 | fromAtomicNr 45  = Rh
330 | fromAtomicNr 46  = Pd
331 | fromAtomicNr 47  = Ag
332 | fromAtomicNr 48  = Cd
333 | fromAtomicNr 49  = In
334 | fromAtomicNr 50  = Sn
335 | fromAtomicNr 51  = Sb
336 | fromAtomicNr 52  = Te
337 | fromAtomicNr 53  = I
338 | fromAtomicNr 54  = Xe
339 | fromAtomicNr 55  = Cs
340 | fromAtomicNr 56  = Ba
341 | fromAtomicNr 57  = La
342 | fromAtomicNr 58  = Ce
343 | fromAtomicNr 59  = Pr
344 | fromAtomicNr 60  = Nd
345 | fromAtomicNr 61  = Pm
346 | fromAtomicNr 62  = Sm
347 | fromAtomicNr 63  = Eu
348 | fromAtomicNr 64  = Gd
349 | fromAtomicNr 65  = Tb
350 | fromAtomicNr 66  = Dy
351 | fromAtomicNr 67  = Ho
352 | fromAtomicNr 68  = Er
353 | fromAtomicNr 69  = Tm
354 | fromAtomicNr 70  = Yb
355 | fromAtomicNr 71  = Lu
356 | fromAtomicNr 72  = Hf
357 | fromAtomicNr 73  = Ta
358 | fromAtomicNr 74  = W
359 | fromAtomicNr 75  = Re
360 | fromAtomicNr 76  = Os
361 | fromAtomicNr 77  = Ir
362 | fromAtomicNr 78  = Pt
363 | fromAtomicNr 79  = Au
364 | fromAtomicNr 80  = Hg
365 | fromAtomicNr 81  = Tl
366 | fromAtomicNr 82  = Pb
367 | fromAtomicNr 83  = Bi
368 | fromAtomicNr 84  = Po
369 | fromAtomicNr 85  = At
370 | fromAtomicNr 86  = Rn
371 | fromAtomicNr 87  = Fr
372 | fromAtomicNr 88  = Ra
373 | fromAtomicNr 89  = Ac
374 | fromAtomicNr 90  = Th
375 | fromAtomicNr 91  = Pa
376 | fromAtomicNr 92  = U
377 | fromAtomicNr 93  = Np
378 | fromAtomicNr 94  = Pu
379 | fromAtomicNr 95  = Am
380 | fromAtomicNr 96  = Cm
381 | fromAtomicNr 97  = Bk
382 | fromAtomicNr 98  = Cf
383 | fromAtomicNr 99  = Es
384 | fromAtomicNr 100 = Fm
385 | fromAtomicNr 101 = Md
386 | fromAtomicNr 102 = No
387 | fromAtomicNr 103 = Lr
388 | fromAtomicNr 104 = Rf
389 | fromAtomicNr 105 = Db
390 | fromAtomicNr 106 = Sg
391 | fromAtomicNr 107 = Bh
392 | fromAtomicNr 108 = Hs
393 | fromAtomicNr 109 = Mt
394 | fromAtomicNr 110 = Ds
395 | fromAtomicNr 111 = Rg
396 | fromAtomicNr 112 = Cn
397 | fromAtomicNr 113 = Nh
398 | fromAtomicNr 114 = Fl
399 | fromAtomicNr 115 = Mc
400 | fromAtomicNr 116 = Lv
401 | fromAtomicNr 117 = Ts
402 | fromAtomicNr 118 = Og
403 |
404 | -- since we are dealing with primitive `Bits8` here,
405 | -- Idris needs our help to figure out that we have reached the end
406 | -- of possible inputs.
407 | fromAtomicNr x   =
408 |   assert_total $
409 |   idris_crash "fromAtomicNr called with invalid AtomicNr: \{show x}"
410 |