0 | module Text.Smiles.Types
  1 |
  2 | import Chem
  3 | import Derive.Finite
  4 | import Derive.Prelude
  5 | import Derive.Refined
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Chirality
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| Index for tetrahedral chirality flags as given in the
 15 | ||| OpenSMILES specification
 16 | public export
 17 | record TBIx where
 18 |   constructor MkTBIx
 19 |   value : Bits8
 20 |   {auto 0 prf : FromTo 1 20 value}
 21 |
 22 | export %inline
 23 | Interpolation TBIx where
 24 |   interpolate = show . value
 25 |
 26 | namespace TBIx
 27 |   %runElab derive "TBIx" [Show,Eq,Ord,RefinedInteger]
 28 |
 29 | export
 30 | Finite TBIx where
 31 |   values = mapMaybe refineTBIx [1..20]
 32 |
 33 | ||| Index for octahedral chirality flags as given in the
 34 | ||| OpenSMILES specification
 35 | public export
 36 | record OHIx where
 37 |   constructor MkOHIx
 38 |   value : Bits8
 39 |   {auto 0 prf : FromTo 1 20 value}
 40 |
 41 | export %inline
 42 | Interpolation OHIx where
 43 |   interpolate = show . value
 44 |
 45 | namespace OHIx
 46 |   %runElab derive "OHIx" [Show,Eq,Ord,RefinedInteger]
 47 |
 48 | export
 49 | Finite OHIx where
 50 |   values = mapMaybe refineOHIx [1..20]
 51 |
 52 | ||| Chirality flag of a bracket atom
 53 | public export
 54 | data Chirality =
 55 |   None | CW | CCW | TH1 | TH2 | AL1 | AL2 | SP1 | SP2 | SP3 | TB TBIx | OH OHIx
 56 |
 57 | export
 58 | Interpolation Chirality where
 59 |   interpolate None   = ""
 60 |   interpolate CW     = "@@"
 61 |   interpolate CCW    = "@"
 62 |   interpolate TH1    = "@TH1"
 63 |   interpolate TH2    = "@TH2"
 64 |   interpolate AL1    = "@AL1"
 65 |   interpolate AL2    = "@AL2"
 66 |   interpolate SP1    = "@SP1"
 67 |   interpolate SP2    = "@SP2"
 68 |   interpolate SP3    = "@SP3"
 69 |   interpolate (TB x) = "@TB\{x}"
 70 |   interpolate (OH x) = "@OH\{x}"
 71 |
 72 | %runElab derive "Chirality" [Ord,Eq,Show,Finite]
 73 |
 74 | --------------------------------------------------------------------------------
 75 | --          Atoms
 76 | --------------------------------------------------------------------------------
 77 |
 78 | ||| Proof that an element (plus aromaticity flag) is a valid subset
 79 | ||| element that can appear without being wrapped in a pair of
 80 | ||| brackets.
 81 | public export
 82 | data ValidSubset : Elem -> Bool -> Type where
 83 |   VB  : ValidSubset B b
 84 |   VC  : ValidSubset C b
 85 |   VN  : ValidSubset N b
 86 |   VO  : ValidSubset O b
 87 |   VF  : ValidSubset F False
 88 |   VP  : ValidSubset P b
 89 |   VS  : ValidSubset S b
 90 |   VCl : ValidSubset Cl False
 91 |   VBr : ValidSubset Br False
 92 |   VI  : ValidSubset I False
 93 |
 94 | export %hint
 95 | 0 toValidArom : ValidSubset e b => ValidAromatic e b
 96 | toValidArom {b = False}       = VARest
 97 | toValidArom {b = True} @{VB}  = VAB
 98 | toValidArom {b = True} @{VC}  = VAC
 99 | toValidArom {b = True} @{VN}  = VAN
100 | toValidArom {b = True} @{VO}  = VAO
101 | toValidArom {b = True} @{VP}  = VAP
102 | toValidArom {b = True} @{VS}  = VAS
103 |
104 | public export
105 | data SmilesAtom : Type where
106 |   SubsetAtom :
107 |        (elem       : Elem)
108 |     -> (arom       : Bool)
109 |     -> {auto 0 prf : ValidSubset elem arom}
110 |     -> SmilesAtom
111 |   Bracket : Atom AromIsotope Charge () () HCount () Chirality () -> SmilesAtom
112 |
113 | %runElab derive "SmilesAtom" [Show,Eq]
114 |
115 | export
116 | subset : List SmilesAtom
117 | subset =
118 |   [ SubsetAtom B False, SubsetAtom C True
119 |   , SubsetAtom C False, SubsetAtom B True
120 |   , SubsetAtom N False, SubsetAtom N True
121 |   , SubsetAtom O False, SubsetAtom O True
122 |   , SubsetAtom P False, SubsetAtom P True
123 |   , SubsetAtom S False, SubsetAtom S True
124 |   , SubsetAtom F False, SubsetAtom Cl False
125 |   , SubsetAtom Br False, SubsetAtom I False
126 |   ]
127 |
128 | export
129 | Cast SmilesAtom Elem where
130 |   cast (SubsetAtom elem arom) = elem
131 |   cast (Bracket x)            = cast x.elem
132 |
133 | export
134 | Cast SmilesAtom Isotope where
135 |   cast (SubsetAtom elem arom) = MkI elem Nothing
136 |   cast (Bracket x)            = cast x.elem
137 |
138 | export
139 | Cast SmilesAtom AromIsotope where
140 |   cast (SubsetAtom elem arom) = MkAI elem Nothing arom
141 |   cast (Bracket x)            = x.elem
142 |
143 | export %inline
144 | Cast SmilesAtom AromElem where
145 |   cast = cast . cast {to = AromIsotope}
146 |
147 | export %inline
148 | bracket : AromIsotope -> Chirality -> HCount -> Charge -> SmilesAtom
149 | bracket a c h ch = Bracket (MkAtom a ch () () h () c ())
150 |
151 | export %inline
152 | isArom : SmilesAtom -> Bool
153 | isArom (SubsetAtom _ a) = a
154 | isArom (Bracket a)      = a.elem.arom
155 |
156 | %inline
157 | aromElem : Elem -> Bool -> String
158 | aromElem e True  = toLower $ symbol e
159 | aromElem e False = symbol e
160 |
161 | export
162 | encodeCharge : Charge -> String
163 | encodeCharge 0    = ""
164 | encodeCharge 1    = "+"
165 | encodeCharge (-1) = "-"
166 | encodeCharge v    = if v.value > 0 then "+\{v}" else "\{v}"
167 |
168 | export
169 | encodeH : HCount -> String
170 | encodeH 0 = ""
171 | encodeH 1 = "H"
172 | encodeH n = "H\{n}"
173 |
174 | encodeElem : Elem -> Bool -> String
175 | encodeElem e True  = toLower $ Elem.symbol e
176 | encodeElem e False = symbol e
177 |
178 | export
179 | encodeAtom : SmilesAtom -> String
180 | encodeAtom (SubsetAtom e b)  = encodeElem e b
181 | encodeAtom (Bracket $ MkAtom (MkAI e mn ar) chrg () () h () ch ()) =
182 |   let mns := maybe "" (show . value) mn
183 |    in "[\{mns}\{encodeElem e ar}\{ch}\{encodeH h}\{encodeCharge chrg}]"
184 |
185 | export %inline
186 | aromIsotope : Maybe MassNr -> AromElem -> AromIsotope
187 | aromIsotope m (MkAE e a) = MkAI e m a
188 |
189 | export %inline
190 | Interpolation SmilesAtom where
191 |   interpolate = encodeAtom
192 |
193 | --------------------------------------------------------------------------------
194 | --          Bonds
195 | --------------------------------------------------------------------------------
196 |
197 | ||| An natural number in the range [0,99] representing a ring opening
198 | ||| or -closure in a SMILES string
199 | public export
200 | record RingNr where
201 |   constructor MkRingNr
202 |   value : Bits8
203 |   0 prf : value <= 99
204 |
205 | export %inline
206 | Interpolation RingNr where
207 |   interpolate n = if n.value >= 10 then "%\{show n.value}" else show n.value
208 |
209 | namespace RingNr
210 |   %runElab derive "RingNr" [Show,Eq,Ord,RefinedInteger]
211 |
212 | export
213 | Finite RingNr where
214 |   values = mapMaybe refineRingNr [0..99]
215 |
216 | ||| A bond in a SMILES string
217 | public export
218 | data SmilesBond = Sngl | Arom | Dbl | Trpl | Quad | FW | BW
219 |
220 | export
221 | Cast SmilesBond BondOrder where
222 |   cast Dbl  = Dbl
223 |   cast Trpl = Triple
224 |   cast _    = Single
225 |
226 | export %inline
227 | Interpolation SmilesBond where
228 |   interpolate Sngl = "-"
229 |   interpolate Arom = ":"
230 |   interpolate Dbl  = "="
231 |   interpolate Trpl = "#"
232 |   interpolate Quad = "$"
233 |   interpolate FW   = "/"
234 |   interpolate BW   = "\\"
235 |
236 | %runElab derive "SmilesBond" [Show,Eq,Ord, Finite]
237 |
238 | public export
239 | record Ring where
240 |   constructor R
241 |   ring   : RingNr
242 |   bond   : Maybe SmilesBond
243 |
244 | %runElab derive "Ring" [Show,Eq,Finite]
245 |
246 | export
247 | Interpolation Ring where
248 |   interpolate (R r (Just b)) = "\{b}\{r}"
249 |   interpolate (R r Nothing)  = "\{r}"
250 |
251 | public export
252 | 0 SmilesGraph : Type
253 | SmilesGraph = Graph SmilesBond SmilesAtom
254 |