0 | module Text.Molfile.Parser.Stack
  1 |
  2 | import Data.Array.Mutable
  3 | import Data.SortedMap as SM
  4 |
  5 | import Syntax.T1
  6 |
  7 | import Text.ILex.Derive
  8 |
  9 | import public Text.ILex
 10 | import public Text.Molfile.Types
 11 |
 12 | %default total
 13 | %language ElabReflection
 14 |
 15 | --------------------------------------------------------------------------------
 16 | -- Stack and State
 17 | --------------------------------------------------------------------------------
 18 |
 19 | %runElab deriveParserState "CSz" "CST"
 20 |   [ "CErr", "H1", "H2", "H3", "Counts", "EndMol", "CDone" -- general states
 21 |   , "SData", "SDValue" -- SD Files
 22 |
 23 |   -- V2000 States
 24 |   , "Coords2", "Sym2", "Chrg2", "Bnd2", "Prop2"
 25 |
 26 |   -- V3000 States
 27 |   , "CountsV3", "ACount", "BCount", "CountEnd", "EmptyV3"
 28 |   , "Atom3", "Index3", "Coords3", "Sym3", "AAMap", "Prop3", "AtomEnd"
 29 |   , "BondBegin", "BondEnd", "Bnd3", "BndProp3"
 30 |   , "RestV3", "SGroup"
 31 |   ]
 32 |
 33 | ||| A molecular graph in the making.
 34 | public export
 35 | record MGraph (q : Type) where
 36 |   constructor MG
 37 |   atoms   : Nat
 38 |   atom    : Ref q (Fin $ S atoms)
 39 |   indices : Ref q (SortedMap Nat $ Fin (S atoms))
 40 |   bond    : Ref q (Maybe $ Edge (S atoms) MolBond)
 41 |   graph   : MArray q (S atoms) (Adj (S atoms) MolBond MolAtom)
 42 |
 43 | export
 44 | mgraph : (atoms : Nat) -> F1 q (MGraph q)
 45 | mgraph atoms = T1.do
 46 |   atm <- ref1 FZ
 47 |   ixs <- ref1 SM.empty
 48 |   bnd <- ref1 Nothing
 49 |   g   <- marray1 (S atoms) (A (cast {from = Elem} C) empty)
 50 |   pure (MG atoms atm ixs bnd g)
 51 |
 52 | public export
 53 | record CSTCK (q : Type) where
 54 |   constructor CK
 55 |   -- text position
 56 |   bufSize_    : Nat
 57 |   prev_       : ByteString
 58 |   cur_        : IBuffer bufSize_
 59 |   prevOffset_ : Nat
 60 |   curOffset_  : Nat
 61 |   from_       : Ref q (LTENat bufSize_)
 62 |   till_       : Ref q (LTENat bufSize_)
 63 |   positions_  : Ref q (SnocList BytePos)
 64 |
 65 |   -- headers
 66 |   h1,h2,h3    : Ref q MolLine
 67 |
 68 |   -- graphs
 69 |   mgraph      : Ref q (MGraph q)
 70 |   stack_      : Ref q (SnocList Molfile)
 71 |   groups      : Ref q (SortedMap Nat String)
 72 |   count       : Ref q Nat
 73 |   isEmpty     : Ref q Bool
 74 |
 75 |   -- sdata
 76 |   sdhead      : Ref q SDHeader
 77 |   sdvals      : Ref q (SnocList StructureData)
 78 |
 79 |   -- utilities
 80 |   error_      : Ref q (Maybe $ BBErr MolErr)
 81 |   strings_    : Ref q (SnocList String)
 82 |   pos         : Ref q Nat
 83 |
 84 | %runElab derive "CSTCK" [HasBBErr,HasBytes,HasStack,HasStringLits]
 85 |
 86 | export
 87 | init : (n : Nat) -> IBuffer n -> F1 q (CSTCK q)
 88 | init n buf = T1.do
 89 |   rf  <- ref1 (first n)
 90 |   rt  <- ref1 (first n)
 91 |   ps  <- ref1 [<]
 92 |   h1  <- ref1 ""
 93 |   h2  <- ref1 ""
 94 |   h3  <- ref1 ""
 95 |   mg  <- mgraph 0
 96 |   gr  <- ref1 mg
 97 |   gs  <- ref1 [<]
 98 |   grp <- ref1 SM.empty
 99 |   cnt <- ref1 Z
100 |   ie  <- ref1 False
101 |   sdh <- ref1 ""
102 |   sdd <- ref1 [<]
103 |   err <- ref1 Nothing
104 |   str <- ref1 [<]
105 |   pos <- ref1 Z
106 |   pure (CK n empty buf 0 0 rf rt ps h1 h2 h3 gr gs grp cnt ie sdh sdd err str pos)
107 |
108 | export %inline
109 | setPos : (sk : CSTCK q) => Nat -> F1' q
110 | setPos n = write1 sk.pos n
111 |
112 | export %inline
113 | incPos : (sk : CSTCK q) => Nat -> F1 q Nat
114 | incPos n = T1.do
115 |   v <- read1 sk.pos
116 |   writeAs sk.pos (v+n) v
117 |