
   0 | module Text.Molfile.Parser.Util
   1 | 
   2 | import Data.ByteString
   3 | import Data.SortedMap as SM
   4 | import Data.Array.Mutable
   5 | import Data.Finite
   6 | import Syntax.T1
   7 | import Text.Molfile.Parser.Stack
   8 | 
   9 | %default total
  10 | 
  11 | --------------------------------------------------------------------------------
  12 | -- Readers and Utilities
  13 | --------------------------------------------------------------------------------
  14 | 
  15 | ||| Isotopes recognized directly by the parser.
  16 | |||
  17 | ||| In addition to the regular element symbols, this includes "D" and "T"
  18 | ||| for deuterium and tritium.
  19 | export
  20 | isos : List Isotope
  21 | isos = MkI H (Just 2) :: MkI H (Just 3) :: map (`MkI` Nothing) values
  22 | 
  23 | ||| Converts the given byte string to a string, removing any trailing
  24 | ||| end of line characters (`'\n'` and `'\r'`).
  25 | export
  26 | stringTillEOL : ByteString -> String
  27 | stringTillEOL = toString . dropWhileEnd isNL
  28 | 
  29 | %inline
  30 | toCoord : Integer -> Coordinate
  31 | toCoord = fromMaybe 0 . refineCoordinate
  32 | 
  33 | export
  34 | coord : ByteString -> Coordinate
  35 | coord (BS n bv) = go n
  36 |   where
  37 |     postdot : Integer -> Nat -> (k : Nat) -> (x : Ix k n) => Integer
  38 |     postdot n 0     _     = n
  39 |     postdot n (S x) 0     = postdot (n*10) x 0
  40 |     postdot n (S x) (S k) = postdot (n*10 + decimaldigit (bv `ix` k)) x k
  41 | 
  42 |     predot : Integer -> (k : Nat) -> (x : Ix k n) => Integer
  43 |     predot n (S k) = case bv `ix` k of
  44 |       46 => postdot n 4 k
  45 |       b  => predot (n*10 + decimaldigit b) k
  46 |     predot n 0     = n * 10_000
  47 | 
  48 |     go : (k : Nat) -> (x : Ix k n) => Coordinate
  49 |     go (S k) = case bv `ix` k of
  50 |       32 => go k
  51 |       45 => toCoord (negate $ predot 0 k) -- 45 = '-'
  52 |       b  => toCoord (predot (decimaldigit b) k)
  53 |     go 0     = 0
  54 | 
  55 | public export
  56 | 0 ErrPair : Type
  57 | ErrPair = (ByteString,MolErr)
  58 | 
  59 | public export %inline
  60 | SPACE : Bits8
  61 | SPACE = 32
  62 | 
  63 | export %inline
  64 | refineInt :
  65 |      {auto cst : Cast Integer a}
  66 |   -> (a -> Maybe b)
  67 |   -> (a -> MolErr)
  68 |   -> ByteString
  69 |   -> Either ErrPair b
  70 | refineInt f err bs =
  71 |  let va      := cast {to = a} (integer $ trim bs)
  72 |      Just vb := f va | Nothing => Left (bs, err va)
  73 |   in Right vb
  74 | 
  75 | export
  76 | blockcharge : ByteString -> Either ErrPair Charge
  77 | blockcharge bs =
  78 |   case decimalSep SPACE bs of
  79 |     0 => Right 0
  80 |     1 => Right 3
  81 |     2 => Right 2
  82 |     3 => Right 1
  83 |     5 => Right (-1)
  84 |     6 => Right (-2)
  85 |     7 => Right (-3)
  86 |     n => Left (bs,MCharge n)
  87 | 
  88 | export %inline
  89 | charge : ByteString -> Either ErrPair Charge
  90 | charge = refineInt refineCharge (MCharge . cast)
  91 | 
  92 | export %inline
  93 | massNr : ByteString -> Either ErrPair MassNr
  94 | massNr = refineInt refineMassNr (MMass . cast)
  95 | 
  96 | export
  97 | radical : ByteString -> Either ErrPair Radical
  98 | radical bs =
  99 |   case decimalSep SPACE bs of
 100 |     1 => Right Singlet
 101 |     2 => Right Doublet
 102 |     3 => Right Triplet
 103 |     0 => Right NoRadical
 104 |     n => Left (bs, MRadical n)
 105 | 
 106 | export
 107 | sgroupType : ByteString ->  SGroupType
 108 | sgroupType bs =
 109 |   case toString $ trim bs of
 110 |     "SUP" => SUP
 111 |     _     => Other
 112 | 
 113 | export
 114 | bondOrder : ByteString -> Either ErrPair BondOrder
 115 | bondOrder bs =
 116 |   case decimalSep SPACE bs of
 117 |     1 => Right Single
 118 |     2 => Right Dbl
 119 |     3 => Right Triple
 120 |     n => Left (bs, MBondOrder n)
 121 | 
 122 | export
 123 | bondStereo : ByteString -> Either ErrPair BondStereo
 124 | bondStereo bs =
 125 |   case decimalSep SPACE bs of
 126 |     0 => Right NoBondStereo
 127 |     1 => Right Up
 128 |     3 => Right Either
 129 |     4 => Right Either
 130 |     6 => Right Down
 131 |     n => Left (bs, MBondStereo n)
 132 | 
 133 | export %inline
 134 | nat : ByteString -> Nat
 135 | nat = cast . decimalSep SPACE
 136 | 
 137 | export
 138 | node : {k : _} -> ByteString -> Either ErrPair (Fin k)
 139 | node bs =
 140 |   case tryNatToFin (pred $ nat bs) of
 141 |     Just n  => Right n
 142 |     Nothing => Left (bs, MNode $ nat bs)
 143 | 
 144 | export
 145 | uedge : {k : _} -> Fin k -> ByteString -> Either ErrPair (Edge k ())
 146 | uedge x bs =
 147 |   case tryNatToFin (pred $ nat bs) >>= \y => mkEdge x y () of
 148 |     Just n  => Right n
 149 |     Nothing => Left (bs, MNode $ nat bs)
 150 | 
 151 | export %inline
 152 | setMass : MassNr -> Isotope -> Isotope
 153 | setMass v = {mass := Just v}
 154 | 
 155 | export %inline
 156 | groupLbl : SortedMap Nat String -> AtomGroup -> AtomGroup
 157 | groupLbl m g@(G n l) = maybe g (G n) (lookup n m)
 158 | 
 159 | parameters (ixs : SortedMap Nat (Fin k))
 160 |   export
 161 |   lkpNode : ByteString -> Either ErrPair (Fin k)
 162 |   lkpNode bs =
 163 |     case lookup (nat bs) ixs of
 164 |       Just n  => Right n
 165 |       Nothing => Left (bs, MNode $ nat bs)
 166 | 
 167 |   export
 168 |   lkpEdge : Fin k -> ByteString -> Either ErrPair (Edge k ())
 169 |   lkpEdge x bs =
 170 |     case lookup (nat bs) ixs >>= \y => mkEdge x y () of
 171 |       Just n  => Right n
 172 |       Nothing => Left (bs, MNode $ nat bs)
 173 | 
 174 | --------------------------------------------------------------------------------
 175 | -- Expressions
 176 | --------------------------------------------------------------------------------
 177 | 
 178 | ||| From a given string, generates a list of string by badding
 179 | ||| it in all possible ways with spaces, so that each of them is
 180 | ||| exactly `n` characters long.
 181 | |||
 182 | ||| For instance, `fill 3 "C"` will return `["  C", " C ", "C  "]`.
 183 | export
 184 | fill : Nat -> String -> List String
 185 | fill n s = go [<] (n `minus` length s) 0
 186 |   where
 187 |     go : SnocList String -> Nat -> Nat -> List String
 188 |     go ss 0     j = ss <>> [s ++ replicate j ' ']
 189 |     go ss (S k) j =
 190 |       go (ss:< (replicate (S k) ' ' ++ s ++ replicate j ' ')) k (S j)
 191 | 
 192 | ||| Expressions we recognize as line breaks.
 193 | |||
 194 | ||| Note: To simplify things, we do currently not recognize a single
 195 | |||       line feed character (`'\r'`) as a valid line break.
 196 | export
 197 | newline : RExp True
 198 | newline = '\n' <|> "\r\n"
 199 | 
 200 | ||| A space or a decimal digit.
 201 | export
 202 | sdigit : RExp True
 203 | sdigit = ' ' <|> digit
 204 | 
 205 | ||| An arbitrary number of spaces and zeroes, followed by a linebreak.
 206 | |||
 207 | ||| If we find this, it typically means we can stop interpreting a
 208 | ||| line of data and fill in default values (for instance, with V2000
 209 | ||| atom and bond definitions).
 210 | export
 211 | zeroes : RExp True
 212 | zeroes = star (' ' <|> '0') >> newline
 213 | 
 214 | export
 215 | spaces : RExp False
 216 | spaces = star ' '
 217 | 
 218 | public export
 219 | m_end : RExp True
 220 | m_end = "M  END" >> spaces
 221 | 
 222 | --------------------------------------------------------------------------------
 223 | -- State Transitions
 224 | --------------------------------------------------------------------------------
 225 | 
 226 | parameters {auto sk : CSTCK q}
 227 | 
 228 |   ||| Writes a custom error with proper bounds based on the given
 229 |   ||| `ByteString`.
 230 |   |||
 231 |   ||| The bounds are computed from the current position and the size
 232 |   ||| and offset of the bytestring, which is supposed to be a substring
 233 |   ||| of the one stored in the `bytes_` filed.
 234 |   export
 235 |   fail : ErrPair -> F1' q
 236 |   fail (BS l $ BV _ o2 _, x) = T1.do
 237 |     BS _ (BV _ o1 _) <- read1 (bytes sk)
 238 |     p                <- getPosition
 239 |     let ps := addCol (o2 `minus` o1) p
 240 |         pe := addCol l ps
 241 |     write1 sk.error_ (Just $ B (Custom x) $ BS ps pe)
 242 | 
 243 |   ||| Convenience alias for `fail p >> pure CErr`.
 244 |   export
 245 |   failErr : ErrPair -> F1 q CST
 246 |   failErr p = fail p >> pure CErr
 247 | 
 248 |   export %inline
 249 |   h1,h2,h3 : ByteString -> F1 q CST
 250 |   h1 bs = writeAs sk.h1 (cast bs) H2
 251 |   h2 bs = writeAs sk.h2 (cast bs) H3
 252 |   h3 bs = writeAs sk.h3 (cast bs) Counts
 253 | 
 254 |   ||| Modifies the current atom in the mol graph
 255 |   export
 256 |   modAtom : (MolAtom -> MolAtom) -> F1' q
 257 |   modAtom f = T1.do
 258 |     mg <- read1 sk.mgraph
 259 |     x  <- read1 mg.atom
 260 |     modify mg.graph x {label $= f}
 261 | 
 262 |   ||| Modifies the current atom in the mol graph
 263 |   export
 264 |   modBond : (MolBond -> MolBond) -> F1' q
 265 |   modBond f = T1.do
 266 |     mg <- read1 sk.mgraph
 267 |     mod1 mg.bond (map $ map f)
 268 | 
 269 |   ||| Returns the current position in the bytestring
 270 |   ||| and increases it by the given number of bytes.
 271 |   export %inline
 272 |   inc : Nat -> F1 q Nat
 273 |   inc k = read1 sk.pos >>= \n => writeAs sk.pos (k+n) n
 274 | 
 275 |   ||| Converts the next `len` bytes of the recognized byte string
 276 |   ||| using the given convertion function.
 277 |   export
 278 |   read : (ByteString -> a) -> (len : Nat) -> F1 q a
 279 |   read f len = T1.do
 280 |     bs <- read1 sk.bytes_
 281 |     p  <- inc len
 282 |     pure (f $ substring p len bs)
 283 | 
 284 |   ||| Converts the remainder of the recognized byte string to a `String`,
 285 |   ||| trimming any newline characters from its end.
 286 |   export
 287 |   remString : F1 q String
 288 |   remString = T1.do
 289 |     p  <- read1 sk.pos
 290 |     bs <- read1 sk.bytes_
 291 |     pure (stringTillEOL $ drop p bs)
 292 | 
 293 |   ||| Finalizes the current molecule
 294 |   export
 295 |   end : F1' q
 296 |   end = T1.do
 297 |     h1  <- replace1 sk.h1 ""
 298 |     h2  <- replace1 sk.h2 ""
 299 |     h3  <- replace1 sk.h3 ""
 300 |     sds <- getList sk.sdvals
 301 |     replace1 sk.isEmpty False >>= \case
 302 |       False => T1.do
 303 |         mg   <- read1 sk.mgraph
 304 |         grps <- replace1 sk.groups SM.empty
 305 |         lupdNodes mg.graph $ {label $= map (groupLbl grps)}
 306 |         g  <- Array.Core.unsafeFreeze mg.graph
 307 |         push1 sk.stack_ (MkMolfile h1 h2 h3 (G _ $ IG g) sds)
 308 |       True  => push1 sk.stack_ (MkMolfile h1 h2 h3 (G 0 empty) sds)
 309 | 
 310 |   sdheader : ByteString -> F1 q CST
 311 |   sdheader bs = writeAs sk.sdhead (readHeader bs) SDValue
 312 | 
 313 |   endSDValue : F1 q CST
 314 |   endSDValue = T1.do
 315 |     hd <- read1 sk.sdhead
 316 |     v  <- getStr
 317 |     push1 sk.sdvals (SD hd $ fromMaybe "" $ refineSDValue v)
 318 |     pure SData
 319 | 
 320 | ||| Sets the isotope of the current atom
 321 | export
 322 | setIso : CST -> Isotope -> Step1 q CSz CSTCK
 323 | setIso x i = \(_ # t) => let _ # t := modAtom {elem := i} t in x # t
 324 | 
 325 | --------------------------------------------------------------------------------
 326 | -- Structure Data
 327 | --------------------------------------------------------------------------------
 328 | 
 329 | ||| Transition steps for structure data header entries.
 330 | export
 331 | sdata : Steps q CSz CSTCK
 332 | sdata =
 333 |   [ newline ("$$$$" >> newline) (end >> pure H1)
 334 |   , cexpr  "$$$$" (end >> pure CDone)
 335 |   , convline ( '>' >> star dot >> newline) sdheader
 336 |   ]
 337 | 
 338 | ||| Transition steps for structure data value entries.
 339 | export
 340 | sdvalue : Steps q CSz CSTCK
 341 | sdvalue =
 342 |   [ newline newline endSDValue
 343 |   , convline (dots >> newline) (pushStr Stack.SDValue . stringTillEOL)
 344 |   ]
 345 |