
   0 | ||| Some of the refined types in here should probably
   1 | ||| go to their own dedicated module
   2 | module Text.Molfile.Types
   3 | 
   4 | import Data.ByteString
   5 | import Data.SortedMap
   6 | import Derive.Finite
   7 | import Derive.Prelude
   8 | import Derive.Refined
   9 | import Text.ILex
  10 | import public Text.Molfile.SData
  11 | import public Chem
  12 | import public Data.Vect
  13 | 
  14 | %default total
  15 | %language ElabReflection
  16 | %hide Language.Reflection.TT.Count
  17 | 
  18 | --------------------------------------------------------------------------------
  19 | --          V2000 Mol Lines
  20 | --------------------------------------------------------------------------------
  21 | 
  22 | ||| An uninterpreted line in a v2000 mol file
  23 | public export
  24 | record MolLine where
  25 |   constructor MkMolLine
  26 |   value : String
  27 | 
  28 | export %inline
  29 | Interpolation MolLine where
  30 |   interpolate = value
  31 | 
  32 | export %inline
  33 | Cast ByteString MolLine where
  34 |   cast = MkMolLine . toString . dropWhileEnd isNL
  35 | 
  36 | %runElab derive "MolLine" [Show,Eq,Ord,FromString]
  37 | 
  38 | --------------------------------------------------------------------------------
  39 | --          Counts Line
  40 | --------------------------------------------------------------------------------
  41 | 
  42 | ------------------------------
  43 | -- MolVersion
  44 | 
  45 | public export
  46 | data MolVersion = V2000 | V3000
  47 | 
  48 | %runElab derive "MolVersion" [Eq,Ord,Show,Finite]
  49 | 
  50 | export %inline
  51 | Interpolation MolVersion where interpolate = show
  52 | 
  53 | ------------------------------
  54 | -- ChiralFlag
  55 | 
  56 | public export
  57 | data ChiralFlag = NonChiral | Chiral
  58 | 
  59 | %runElab derive "ChiralFlag" [Eq,Ord,Show,Finite]
  60 | 
  61 | export %inline
  62 | Interpolation ChiralFlag where
  63 |   interpolate NonChiral = "0"
  64 |   interpolate Chiral    = "1"
  65 | 
  66 | --------------------------------------------------------------------------------
  67 | --          Atoms
  68 | --------------------------------------------------------------------------------
  69 | 
  70 | ------------------------------
  71 | -- AtomSymbol
  72 | 
  73 | ||| Ast    -> Asterisk
  74 | ||| RSharp -> R# (RGroupLabel)
  75 | public export
  76 | data AtomSymbol = L | A | Q | Ast | LP | RSharp | El Elem
  77 | 
  78 | export
  79 | Interpolation AtomSymbol where
  80 |   interpolate (El x) = symbol x
  81 |   interpolate L      = "L"
  82 |   interpolate A      = "A"
  83 |   interpolate Q      = "Q"
  84 |   interpolate Ast    = "*"
  85 |   interpolate LP     = "LP"
  86 |   interpolate RSharp = "R#"
  87 | 
  88 | %runElab derive "AtomSymbol" [Show,Eq,Finite]
  89 | 
  90 | public export %inline
  91 | Cast Elem AtomSymbol where cast = El
  92 | 
  93 | 
  94 | ------------------------------
  95 | -- StereoParity
  96 | 
  97 | ||| Atom Stereo parity encoded in V2000 CTAB
  98 | public export
  99 | data StereoParity =
 100 |     NoStereo
 101 |   | OddStereo
 102 |   | EvenStereo
 103 |   | AnyStereo
 104 | 
 105 | %runElab derive "StereoParity" [Eq,Ord,Show,Finite]
 106 | 
 107 | export %inline
 108 | Interpolation StereoParity where
 109 |   interpolate NoStereo   = "0"
 110 |   interpolate OddStereo  = "1"
 111 |   interpolate EvenStereo = "2"
 112 |   interpolate AnyStereo  = "3"
 113 | 
 114 | ------------------------------
 115 | -- StereoCareBox
 116 | 
 117 | ||| Stereo care box encoded in V2000
 118 | public export
 119 | data  StereoCareBox = IgnoreStereo | MatchStereo
 120 | 
 121 | export %inline
 122 | Interpolation StereoCareBox where
 123 |   interpolate IgnoreStereo = "0"
 124 |   interpolate MatchStereo  = "1"
 125 | 
 126 | %runElab derive "StereoCareBox" [Eq,Ord,Show,Finite]
 127 | 
 128 | ------------------------------
 129 | -- Valence
 130 | 
 131 | ||| Valence of atoms
 132 | |||
 133 | ||| NOTE: In a V2000 molfile 15 is zero valence,
 134 | ||| while 0 means no marking
 135 | public export
 136 | record Valence where
 137 |   constructor MkValence
 138 |   value : Bits8
 139 |   {auto 0 prf : value <= 15}
 140 | 
 141 | export %inline
 142 | Interpolation Valence where
 143 |   interpolate = show . value
 144 | 
 145 | namespace Valence
 146 |   %runElab derive "Valence" [Show,Eq,Ord,RefinedInteger]
 147 | 
 148 | export
 149 | Finite Valence where
 150 |   values = mapMaybe refineValence [0..15]
 151 | 
 152 | ------------------------------
 153 | -- H0Designator
 154 | 
 155 | ||| Reduntant hydrogen count flag
 156 | public export
 157 | data H0Designator = H0NotSpecified | NoHAllowed
 158 | 
 159 | export %inline
 160 | Interpolation H0Designator where
 161 |   interpolate H0NotSpecified = "0"
 162 |   interpolate NoHAllowed     = "1"
 163 | 
 164 | %runElab derive "H0Designator" [Eq,Ord,Show,Finite]
 165 | 
 166 | ------------------------------
 167 | -- Hydrogen Count
 168 | 
 169 | ||| HCount plus 1: 0 means "not explicitly given"
 170 | ||| 1 means "explicitly 0" and so on.
 171 | public export
 172 | record HydrogenCount where
 173 |   constructor MkHC
 174 |   value : Bits8
 175 |   {auto 0 prf : value <= 5}
 176 | 
 177 | export %inline
 178 | Interpolation HydrogenCount where
 179 |   interpolate = show . value
 180 | 
 181 | namespace HydrogenCount
 182 |   %runElab derive "HydrogenCount" [Show,Eq,Ord,RefinedInteger]
 183 | 
 184 | export
 185 | Finite HydrogenCount where
 186 |   values = mapMaybe refineHydrogenCount [0..5]
 187 | 
 188 | ||| We encode coordinates as a sufficiently precise integer
 189 | ||| to prevent loss of precision during parsing.
 190 | public export
 191 | record Coordinate where
 192 |   constructor MkCoordinate
 193 |   value : Integer
 194 |   {auto 0 prf : FromTo (-9999_9999) 99999_9999 value}
 195 | 
 196 | public export
 197 | Precision : Integer
 198 | Precision = 10000
 199 | 
 200 | export %inline
 201 | Cast Coordinate Double where
 202 |   cast x = cast x.value / cast Precision
 203 | 
 204 | dec : Integer -> String
 205 | dec i = padLeft 4 '0' (show (abs i `mod` Precision))
 206 | 
 207 | disp : Integer -> String
 208 | disp i = show (i `div` Precision) ++ "." ++ dec i
 209 | 
 210 | dispShort : Integer -> String
 211 | dispShort v =
 212 |   case v `mod` Precision of
 213 |     0 => show (v `div` Precision)
 214 |     n => "\{show (v `div` Precision)}.\{dot $ [<] <>< unpack (dec n)}"
 215 | 
 216 |   where
 217 |     dot : SnocList Char -> String
 218 |     dot (t:<'0') = dot t
 219 |     dot sc       = pack (sc <>> [])
 220 | 
 221 | export
 222 | Interpolation Coordinate where
 223 |   interpolate s = padLeft 10 ' ' $
 224 |     if s.value < 0 then "-" ++ disp (abs s.value) else disp s.value
 225 | 
 226 | ||| Space-efficient version of `interpolate` to be used in V3000
 227 | ||| mol files.
 228 | export
 229 | dispCoordShort : Coordinate -> String
 230 | dispCoordShort (MkCoordinate v) =
 231 |   if v < 0 then "-" ++ dispShort (abs v) else dispShort v
 232 | 
 233 | namespace Coordinate
 234 |   %runElab derive "Coordinate" [Show,Eq,Ord,RefinedInteger]
 235 | 
 236 | ||| Convenience alias for `Vect 3 Coordinates`
 237 | public export
 238 | 0 Coordinates : Type
 239 | Coordinates = Vect 3 Coordinate
 240 | 
 241 | public export
 242 | record AtomGroup where
 243 |   constructor G
 244 |   nr    : Nat
 245 |   lbl   : String
 246 | 
 247 | %runElab derive "AtomGroup" [Show,Eq]
 248 | 
 249 | ||| Regular atom loaded from a .mol file.
 250 | |||
 251 | ||| Note: .mol files support additional atom symbols
 252 | ||| (for instance, for queries), but for real-world molecules,
 253 | ||| this is the type to use.
 254 | |||
 255 | ||| The type parameters are used for implicit hydrogens and atom types,
 256 | ||| which are `()` for freshly loaded `MolAtom`s but more specific after
 257 | ||| atom type perception.
 258 | public export
 259 | 0 MolAtom' : (h,t,c : Type) -> Type
 260 | MolAtom' h t c = Atom Isotope Charge Coordinates Radical h t c (Maybe AtomGroup)
 261 | 
 262 | ||| Regular atom loaded from a .mol file.
 263 | |||
 264 | ||| Note: .mol files support additional atom symbols
 265 | ||| (for instance, for queries), but for real-world molecules,
 266 | ||| this is the type to use.
 267 | public export
 268 | 0 MolAtom : Type
 269 | MolAtom = MolAtom' () () ()
 270 | 
 271 | ||| .mol-file atom with perceived atom type and computed
 272 | ||| implicit hydrogen count
 273 | public export
 274 | 0 MolAtomAT : Type
 275 | MolAtomAT = MolAtom' HCount AtomType ()
 276 | 
 277 | public export
 278 | Cast Elem MolAtom where
 279 |   cast el = MkAtom (cast el) 0 [0,0,0] NoRadical () () () Nothing
 280 | 
 281 | --------------------------------------------------------------------------------
 282 | --          Bonds
 283 | --------------------------------------------------------------------------------
 284 | 
 285 | ------------------------------
 286 | -- BondType
 287 | 
 288 | public export
 289 | data QueryBondType : Type where
 290 |   BT            : BondOrder -> QueryBondType
 291 |   Arom          : QueryBondType
 292 |   SngOrDbl      : QueryBondType
 293 |   SngOrAromatic : QueryBondType
 294 |   DblOrAromatic : QueryBondType
 295 |   AnyBond       : QueryBondType
 296 | 
 297 | export %inline
 298 | Interpolation QueryBondType where
 299 |   interpolate (BT b)        = interpolate b
 300 |   interpolate Arom          = "4"
 301 |   interpolate SngOrDbl      = "5"
 302 |   interpolate SngOrAromatic = "6"
 303 |   interpolate DblOrAromatic = "7"
 304 |   interpolate AnyBond       = "8"
 305 | 
 306 | %runElab derive "QueryBondType" [Eq,Show,Ord]
 307 | 
 308 | ------------------------------
 309 | -- BondStereo
 310 | 
 311 | ||| Stereoinformation represented in molfiles
 312 | public export
 313 | data BondStereo = NoBondStereo | Up | Either | Down
 314 | 
 315 | export %inline
 316 | Interpolation BondStereo where
 317 |   interpolate NoBondStereo = "0"
 318 |   interpolate Up           = "1"
 319 |   interpolate Either       = "4"
 320 |   interpolate Down         = "6"
 321 | 
 322 | %runElab derive "BondStereo" [Ord,Eq,Show,Finite]
 323 | 
 324 | ------------------------------
 325 | -- BondTopo
 326 | 
 327 | ||| Bond topology encoded in CTAB V2000
 328 | public export
 329 | data BondTopo = AnyTopology | Ring | Chain
 330 | 
 331 | export %inline
 332 | Interpolation BondTopo where
 333 |   interpolate AnyTopology = "0"
 334 |   interpolate Ring        = "1"
 335 |   interpolate Chain       = "2"
 336 | 
 337 | %runElab derive "BondTopo" [Eq,Show,Ord,Finite]
 338 | 
 339 | public export
 340 | record MolBond where
 341 |   constructor MkBond
 342 |   ||| Flag indicating whether the bond goes from the
 343 |   ||| atom with the smaller index to the one with the larger index
 344 |   ||| or vice versa.
 345 |   |||
 346 |   ||| We need this to figure out in which direction wedged bonds should
 347 |   ||| point.
 348 |   firstSmaller : Bool
 349 |   type         : BondOrder
 350 |   stereo       : BondStereo
 351 | 
 352 | %runElab derive "MolBond" [Eq,Show]
 353 | 
 354 | export %inline
 355 | Cast MolBond BondOrder where cast = type
 356 | 
 357 | export %inline
 358 | Cast BondOrder MolBond where cast t = MkBond False t NoBondStereo
 359 | 
 360 | export %inline
 361 | Cast MolBond BondStereo where cast = stereo
 362 | 
 363 | export %inline
 364 | Cast BondStereo MolBond where cast = MkBond False Single
 365 | 
 366 | --------------------------------------------------------------------------------
 367 | --          MolFile
 368 | --------------------------------------------------------------------------------
 369 | 
 370 | public export
 371 | data SGroupType = SUP | Other
 372 | 
 373 | %runElab derive "SGroupType" [Show,Eq,Finite]
 374 | 
 375 | public export
 376 | 0 MolGraph' : (h,t,c : Type) -> Type
 377 | MolGraph' h t c = Graph MolBond (MolAtom' h t c)
 378 | 
 379 | public export
 380 | 0 MolGraph : Type
 381 | MolGraph = MolGraph' () () ()
 382 | 
 383 | ||| .mol-file graph with perceived atom types and computed
 384 | ||| implicit hydrogen counts
 385 | public export
 386 | 0 MolGraphAT : Type
 387 | MolGraphAT = MolGraph' HCount AtomType ()
 388 | 
 389 | public export
 390 | record Molfile' (h,t,c : Type) where
 391 |   constructor MkMolfile
 392 |   name    : MolLine
 393 |   info    : MolLine
 394 |   comment : MolLine
 395 |   graph   : MolGraph' h t c
 396 |   dat     : List StructureData
 397 | 
 398 | %runElab derive "Molfile'" [Show,Eq]
 399 | 
 400 | export %inline
 401 | emptyMolFile : Molfile' h t c
 402 | emptyMolFile = MkMolfile "" "" "" (G 0 empty) []
 403 | 
 404 | public export
 405 | 0 Molfile : Type
 406 | Molfile = Molfile' () () ()
 407 | 
 408 | public export
 409 | 0 MolfileAT : Type
 410 | MolfileAT = Molfile' HCount AtomType ()
 411 | 
 412 | --------------------------------------------------------------------------------
 413 | --          Error
 414 | --------------------------------------------------------------------------------
 415 | 
 416 | public export
 417 | data MolErr : Type where
 418 |   MCharge     : Integer -> MolErr
 419 |   MMass       : Integer -> MolErr
 420 |   MRadical    : Integer -> MolErr
 421 |   MBondOrder  : Integer -> MolErr
 422 |   MBondStereo : Integer -> MolErr
 423 |   MEntries    : MolErr
 424 |   MAbbr       : MolErr
 425 |   MNode       : Nat -> MolErr
 426 | 
 427 | %runElab derive "MolErr" [Show,Eq]
 428 | 
 429 | export
 430 | Interpolation MolErr where
 431 |   interpolate v = "Invalid " ++ case v of
 432 |     MCharge     x => "charge: \{show x}"
 433 |     MMass       x => "mass number: \{show x}"
 434 |     MRadical    x => "radical: \{show x}"
 435 |     MBondOrder  x => "bond order: \{show x}"
 436 |     MBondStereo x => "bond stereo: \{show x}"
 437 |     MNode       x => "node: \{show x}"
 438 |     MEntries      => ".mol file: More than one entry"
 439 |     MAbbr         => "abbreviation"
 440 |