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 |   prev_      : Ref q ByteString
 57 |   cur_       : Ref q ByteString
 58 |   offset_    : Ref q Nat
 59 |   relpos_    : Ref q Integer
 60 |   len_       : Ref q Nat
 61 |   positions_ : Ref q (SnocList BytePos)
 62 |
 63 |   -- headers
 64 |   h1,h2,h3   : Ref q MolLine
 65 |
 66 |   -- graphs
 67 |   mgraph     : Ref q (MGraph q)
 68 |   stack_     : Ref q (SnocList Molfile)
 69 |   groups     : Ref q (SortedMap Nat String)
 70 |   count      : Ref q Nat
 71 |   isEmpty    : Ref q Bool
 72 |
 73 |   -- sdata
 74 |   sdhead     : Ref q SDHeader
 75 |   sdvals     : Ref q (SnocList StructureData)
 76 |
 77 |   -- utilities
 78 |   error_     : Ref q (Maybe $ BBErr MolErr)
 79 |   strings_   : Ref q (SnocList String)
 80 |   pos        : Ref q Nat
 81 |
 82 | %runElab derive "CSTCK" [HasBBErr,HasBytes,HasStack,HasStringLits]
 83 |
 84 | export
 85 | init : F1 q (CSTCK q)
 86 | init = T1.do
 87 |   pr <- ref1 empty
 88 |   fl <- ref1 empty
 89 |   ro <- ref1 Z
 90 |   rr <- ref1 0
 91 |   ll <- ref1 Z
 92 |   ps <- ref1 [<]
 93 |   h1  <- ref1 ""
 94 |   h2  <- ref1 ""
 95 |   h3  <- ref1 ""
 96 |   mg  <- mgraph 0
 97 |   gr  <- ref1 mg
 98 |   gs  <- ref1 [<]
 99 |   grp <- ref1 SM.empty
100 |   cnt <- ref1 Z
101 |   ie  <- ref1 False
102 |   sdh <- ref1 ""
103 |   sdd <- ref1 [<]
104 |   err <- ref1 Nothing
105 |   str <- ref1 [<]
106 |   pos <- ref1 Z
107 |   pure (CK pr fl ro rr ll ps h1 h2 h3 gr gs grp cnt ie sdh sdd err str pos)
108 |
109 | export %inline
110 | setPos : (sk : CSTCK q) => Nat -> F1' q
111 | setPos n = write1 sk.pos n
112 |
113 | export %inline
114 | incPos : (sk : CSTCK q) => Nat -> F1 q Nat
115 | incPos n = T1.do
116 |   v <- read1 sk.pos
117 |   writeAs sk.pos (v+n) v
118 |