0 | module Text.Smiles.Parser

  2 | import Chem

  3 | import Data.Finite

  4 | import Data.SnocVect

  5 | import Derive.Prelude

  6 | import Syntax.T1

  7 | import Text.ILex

  8 | import Text.ILex.Derive

  9 | import Text.Smiles.Types

 11 | %default total

 12 | %language ElabReflection

 19 | drop : List a -> List a

 20 | drop (_::t) = t

 21 | drop []     = []

 24 | doubleHead : List a -> List a

 25 | doubleHead l@(h::_) = h::l

 26 | doubleHead []       = []

 28 | public export

 29 | data SmilesErr : Type where

 30 |   RingBondMismatch   : SmilesErr

 31 |   UnclosedRing       : SmilesErr

 32 |   ManyEntries        : SmilesErr

 35 | Interpolation SmilesErr where

 36 |   interpolate RingBondMismatch = "Ring bonds do not match"

 37 |   interpolate UnclosedRing     = "Unclosed ring"

 38 |   interpolate ManyEntries      = "More than one molecule"

 40 | %runElab derive "SmilesErr" [Eq,Show]

 42 | public export

 43 | 0 SmilesParseErr : Type

 44 | SmilesParseErr = ParseError SmilesErr

 46 | data DOB : Type where

 47 |   No  : DOB

 48 |   Dot : DOB

 49 |   Bnd : SmilesBond -> DOB

 51 | record RingInfo n where

 52 |   constructor R

 53 |   start : Fin n

 54 |   nr    : RingNr

 55 |   atom  : SmilesAtom

 56 |   bond  : Maybe SmilesBond

 57 |   pos   : BytePos

 59 | record AtomInfo n where

 60 |   constructor A

 61 |   node  : Fin n

 62 |   atom  : SmilesAtom

 64 | smilesBond : (xa,ya : Bool) -> SmilesBond

 65 | smilesBond True True = Arom

 66 | smilesBond _    _    = Sngl

 68 | ringBond : (b,c : Maybe SmilesBond) -> (x,y : SmilesAtom) -> Maybe SmilesBond

 69 | ringBond Nothing Nothing   x y = Just $ smilesBond (isArom x) (isArom y)

 70 | ringBond Nothing (Just x)  _ _ = Just x

 71 | ringBond (Just x) Nothing  _ _ = Just x

 72 | ringBond (Just x) (Just y) _ _ = if x == y then Just x else Nothing

 74 | lookupRing : RingNr -> List (RingInfo n) -> Maybe (RingInfo n)

 75 | lookupRing r []      = Nothing

 76 | lookupRing r (x::xs) = case compare r (nr x) of

 77 |   LT => Nothing

 78 |   EQ => Just x

 79 |   GT => lookupRing r xs

 81 | insert : RingInfo n -> List (RingInfo n) -> List (RingInfo n)

 82 | insert r []      = [r]

 83 | insert r (x::xs) = if r.nr < x.nr then r::x::xs else x::insert r xs

 85 | delete : RingNr -> List (RingInfo n) -> List (RingInfo n)

 86 | delete r []      = []

 87 | delete r (x::xs) = if r == x.nr then xs else x::delete r xs

 89 | ringBondMismatch : Ring -> BytePos -> BBErr SmilesErr

 90 | ringBondMismatch r p =

 91 |  let bs := BB p $ incLen (length "\{r}") p

 92 |   in B (Custom RingBondMismatch) bs

 94 | record ST where

 95 |   constructor S

 96 |   cnt   : Nat

 97 |   stck  : List (AtomInfo cnt)

 98 |   atoms : SnocVect cnt SmilesAtom

 99 |   bonds : List (Edge cnt SmilesBond)

100 |   rings : List (RingInfo cnt)

102 | empty : ST

103 | empty = S 0 [] [<] [] []

105 | toGraph : ST -> Either (BBErr SmilesErr) SmilesGraph

106 | toGraph (S n _ a b [])                = Right $ G n (mkGraph (cast a) b)

107 | toGraph (S _ _ _ _ (R _ r _ b p ::_)) =

108 |  let bs := BB p $ incLen (length "\{R r b}") p

109 |   in Left $ B (Custom UnclosedRing) bs

111 | weakenST : List (AtomInfo n) -> List (AtomInfo $ S n)

112 | weakenST x = believe_me x

114 | weakenBS : List (Edge n e) -> List (Edge (S n) e)

115 | weakenBS x = believe_me x

117 | weakenRS : List (RingInfo n) -> List (RingInfo (S n))

118 | weakenRS x = believe_me x

120 | plainAtom : SmilesAtom -> ST -> ST

121 | plainAtom a1 (S c (A n a::ss) sa bs rs) =

122 |   let bs2 := edge n (smilesBond (isArom a) (isArom a1)) :: weakenBS bs

123 |       st2 := A last a1 :: weakenST ss

124 |    in S (S c) st2 (sa:<a1) bs2 (weakenRS rs)

125 | plainAtom a1 st = st

127 | atomWithBond : SmilesBond -> SmilesAtom -> ST -> ST

128 | atomWithBond b a1 (S c (A n _::ss) sa bs rs) =

129 |   let bs2 := edge n b :: weakenBS bs

130 |       st2 := A last a1 :: weakenST ss

131 |    in S (S c) st2 (sa:<a1) bs2 (weakenRS rs)

132 | atomWithBond b a1 st = st

134 | dottedAtom : SmilesAtom -> ST -> ST

135 | dottedAtom a1 (S c st sa bs rs) =

136 |   S (S c) (A last a1 :: weakenST st) (sa:<a1) (weakenBS bs) (weakenRS rs)

138 | addRing : BytePos -> Ring -> ST -> Either (BBErr SmilesErr) ST

139 | addRing p (R r mb1) st =

140 |   case st.stck of

141 |     A n1 a1::_ => case lookupRing r st.rings of

142 |       Just (R n2 nr a2 mb2 p) => case ringBond mb1 mb2 a1 a2 of

143 |         Just b  => case mkEdge n1 n2 b of

144 |           Just e  => Right $ {bonds $= (e::), rings $= delete r} st

145 |           Nothing => Right st -- impossible

146 |         Nothing => Left (ringBondMismatch (R r mb1) p)

147 |       Nothing => Right $ {rings $= insert (R n1 r a1 mb1 p)} st

148 |     [] => Right st -- impossible

155 | record SSTCK (q : Type) where

156 |   constructor SS

157 |   bufSize_    : Nat

158 |   prev_       : ByteString

159 |   cur_        : IBuffer bufSize_

160 |   prevOffset_ : Nat

161 |   curOffset_  : Nat

162 |   from_       : Ref q (LTENat bufSize_)

163 |   till_       : Ref q (LTENat bufSize_)

164 |   positions_  : Ref q (SnocList BytePos)

165 |   st          : Ref q ST

166 |   dob         : Ref q DOB

167 |   mass        : Ref q (Maybe MassNr)

168 |   elem        : Ref q AromElem

169 |   chirality   : Ref q Chirality

170 |   hcount      : Ref q HCount

171 |   charge      : Ref q Charge

172 |   error_      : Ref q (Maybe $ BBErr SmilesErr)

173 |   stack_      : Ref q (SnocList SmilesGraph)

175 | %runElab derive "SSTCK" [HasBytes, HasBBErr, HasStack]

177 | init : (n : Nat) -> IBuffer n -> F1 q (SSTCK q)

178 | init n buf = T1.do

179 |   rf  <- ref1 (first n)

180 |   rt  <- ref1 (first n)

181 |   ps  <- ref1 [<]

182 |   s   <- ref1 empty

183 |   db  <- ref1 Dot

184 |   ms  <- ref1 Nothing

185 |   el  <- ref1 (MkAE C False)

186 |   cy  <- ref1 (the Chirality None)

187 |   hc  <- ref1 (the HCount 0)

188 |   ch  <- ref1 (the Charge 0)

189 |   er  <- ref1 Nothing

190 |   st  <- ref1 [<]

191 |   pure (SS n empty buf 0 0 rf rt ps s db ms el cy hc ch er st)

193 | %runElab deriveParserState "SSz" "SST"

194 |   [ "Chain", "NewBranch", "SRing", "Closed", "Err", "Atom"

195 |   , "BMass","BElem","BChiral","BHCount","BCharge","BEnd"

196 |   ]

198 | endGraph : SSTCK q -> F1 q (Maybe (BBErr SmilesErr))

199 | endGraph sk = T1.do

200 |   st    <- replace1 sk.st empty

201 |   write1 sk.dob Dot

202 |   let Right g := toGraph st | Left err => pure (Just err)

203 |   [<] <- replace1 sk.positions_ [<]

204 |     | _:<p => pure $ Just (B (Unclosed "(") (BB p p))

205 |   case g.order of

206 |     0 => pure Nothing

207 |     _ => push1 sk.stack_ g >> pure Nothing

209 | onAtom : SmilesAtom -> Step1 q SSz SSTCK

210 | onAtom a = \sk,t =>

211 |  let s # t := read1 sk.st t

212 |   in case read1 sk.dob t of

213 |        No    # t => writeAs sk.st (plainAtom a s) SRing t

214 |        Bnd b # t =>

215 |         let _ # t := write1 sk.dob No t

216 |          in writeAs sk.st (atomWithBond b a s) SRing t

217 |        Dot # t  =>

218 |         let _ # t := write1 sk.dob No t

219 |          in writeAs sk.st (dottedAtom a s) SRing t

221 | onRing : Ring -> Step1 q SSz SSTCK

222 | onRing r = \sk,t =>

223 |   let p # t := startPos t

224 |       s # t := read1 sk.st t

225 |    in case addRing p r s of

226 |         Right s2 => writeAs sk.st s2 SRing t

227 |         Left  x  => failWith x Err t

229 | bracket : (sk : SSTCK q) => F1 q SST

230 | bracket t =

231 |   let m  # t := replace1 sk.mass Nothing t

232 |       e  # t := read1 sk.elem t

233 |       cy # t := replace1 sk.chirality None t

234 |       h  # t := replace1 sk.hcount 0 t

235 |       ch # t := replace1 sk.charge 0 t

236 |    in onAtom (bracket (aromIsotope m e) cy h ch) sk t

238 | mass : (RExp True, Step q SSz SSTCK)

239 | mass = bytes (plus digit) wrt

240 |   where

241 |     %inline wrt : (sk : SSTCK q) =>  ByteString ->F1 q SST

242 |     wrt bs = writeAs sk.mass (refineMassNr $ cast $ decimal bs) BElem

244 | elem : List (RExp True, Step q SSz SSTCK)

245 | elem = writeVals interpolate elem BChiral values

247 | chirality : List (RExp True, Step q SSz SSTCK)

248 | chirality = writeVals interpolate chirality BHCount values

250 | hc : List (RExp True, Step q SSz SSTCK)

251 | hc = step "H1" (wrt 1) :: vals encodeH (\v => \sk,t => wrt v t) values

252 |   where

253 |     wrt : HCount -> (sk : SSTCK q) => F1 q SST

254 |     wrt c = writeAs sk.hcount c BCharge

256 | chrg : List (RExp True, Step q SSz SSTCK)

257 | chrg =

258 |      step "+1" (wrt 1)

259 |   :: step "-1" (wrt (-1))

260 |   :: step "++" (wrt 2)

261 |   :: step "--" (wrt (-2))

262 |   :: vals encodeCharge (\v => \sk,t => wrt v t) values

263 |   where

264 |     wrt : Charge -> (sk : SSTCK q) => F1 q SST

265 |     wrt c = writeAs sk.charge c BEnd

267 | bend : List (RExp True, Step q SSz SSTCK)

268 | bend = [close ']' bracket]

270 | atom : List (RExp True, Step q SSz SSTCK)

271 | atom = opn' '[' BMass :: vals encodeAtom onAtom subset

273 | ring : List (RExp True, Step q SSz SSTCK)

274 | ring = vals interpolate onRing values

276 | bond : List (RExp True, Step q SSz SSTCK)

277 | bond = step '.' dot :: vals interpolate wrt values

278 |   where

279 |     %inline wrt   : SmilesBond -> Step1 q SSz SSTCK

280 |     wrt b = \sk,t => writeAs sk.dob (Bnd b) Atom t

282 |     dot : (k : SSTCK q) => F1 q SST

283 |     dot = writeAs k.dob Dot Atom

285 | openClose : List (RExp True, Step q SSz SSTCK)

286 | openClose = [opn '(' op, close ')' cls]

287 |   where

288 |     op,cls : (k : SSTCK q) => F1 q SST

289 |     op = read1 k.st >>= \s => writeAs k.st ({stck $= doubleHead} s) NewBranch

290 |     cls = read1 k.st >>= \s => writeAs k.st ({stck $= drop} s) Closed

292 | space : List (RExp True, Step q SSz SSTCK)

293 | space = [bytes (plus $ oneof [' ', '\t']) (const end), step nl end]

294 |   where

295 |     nl : RExp True

296 |     nl = "\r\n" <|> '\n' <|> '\r'

298 |     end : (sk : SSTCK q) => F1 q SST

299 |     end = T1.do

300 |       Nothing <- endGraph sk | Just x => failWith x Err

301 |       pure Chain

303 | smilesTrans : Lex1 q SSz SSTCK

304 | smilesTrans =

305 |   lex1

306 |     [ E Chain     $ dfa (atom ++ space)

307 |     , E Atom      $ dfa atom

308 |     , E SRing     $ dfa (atom ++ ring ++ bond ++ openClose ++ space)

309 |     , E NewBranch $ dfa (atom ++ bond)

310 |     , E Closed    $ dfa (atom ++ bond ++ openClose ++ space)

311 |     , E BMass     $ dfa (mass :: elem)

312 |     , E BElem     $ dfa elem

313 |     , E BChiral   $ dfa (chirality ++ hc ++ chrg ++ bend)

314 |     , E BHCount   $ dfa (hc ++ chrg ++ bend)

315 |     , E BCharge   $ dfa (chrg ++ bend)

316 |     , E BEnd      $ dfa bend

317 |     ]

319 | smilesErr : Arr32 SSz (SSTCK q -> F1 q (BBErr SmilesErr))

320 | smilesErr =

321 |   arr32 SSz (unexpected [])

322 |     [ E BMass   $ unclosedIfNLorEOI "[" []

323 |     , E BElem   $ unclosedIfNLorEOI "[" []

324 |     , E BChiral $ unclosedIfNLorEOI "[" []

325 |     , E BHCount $ unclosedIfNLorEOI "[" []

326 |     , E BEnd    $ unclosedIfNLorEOI "[" []

327 |     ]

329 | smilesEOI :

330 |      SST

331 |   -> SSTCK q

332 |   -> F1 q (Either (BBErr SmilesErr) (List SmilesGraph))

333 | smilesEOI st sk =

334 |   case st == Chain || st == SRing || st == Closed of

335 |     False => arrFail SSTCK smilesErr st sk

336 |     True  => endGraph sk >>= \case

337 |       Just x  => pure (Left x)

338 |       Nothing => getList sk.stack_ >>= pure . Right

340 | public export

341 | smiles : P1 q (BBErr SmilesErr) (List SmilesGraph)

342 | smiles = P Chain init smilesTrans snocChunk smilesErr smilesEOI

345 | export %inline

346 | parseSmiles : Origin -> String -> Either SmilesParseErr (List SmilesGraph)

347 | parseSmiles = parseString smiles

349 | test : String -> IO ()

350 | test s =

351 |   case parseSmiles Virtual s of

352 |     Right x => for_ x $ \(G _ g) => putStrLn (pretty interpolate interpolate g)

353 |     Left x  => putStrLn "\{x}"

356 | readSmilesFrom :

357 |      {auto has : Has SmilesParseErr es}

358 |   -> Origin

359 |   -> String

360 |   -> ChemRes es SmilesGraph

361 | readSmilesFrom o s =

362 |   case parseSmiles o s of

363 |     Left  x   => Left (inject x)

364 |     Right []  => Right (G 0 empty)

365 |     Right [g] => Right g

366 |     Right _   =>

367 |       Left (inject $ toParseError o s (B (Custom ManyEntries) NoBounds))

369 | export %inline

370 | readSmiles : Has SmilesParseErr es => String -> ChemRes es SmilesGraph

371 | readSmiles = readSmilesFrom Virtual

377 | export %inline

378 | readSmiles' : String -> Either String SmilesGraph

379 | readSmiles' =

380 |   mapFst (interpolate . project1) . readSmiles {es = [SmilesParseErr]}