0 | module Text.Molfile.Parser.Stack
2 | import Data.Array.Mutable
3 | import Data.SortedMap as SM
7 | import Text.ILex.Derive
9 | import public Text.ILex
10 | import public Text.Molfile.Types
13 | %language ElabReflection
19 | %runElab deriveParserState "CSz" "CST"
20 | [ "CErr", "H1", "H2", "H3", "Counts", "EndMol", "CDone"
21 | , "SData", "SDValue"
24 | , "Coords2", "Sym2", "Chrg2", "Bnd2", "Prop2"
27 | , "CountsV3", "ACount", "BCount", "CountEnd", "EmptyV3"
28 | , "Atom3", "Index3", "Coords3", "Sym3", "AAMap", "Prop3", "AtomEnd"
29 | , "BondBegin", "BondEnd", "Bnd3", "BndProp3"
30 | , "RestV3", "SGroup"
35 | record MGraph (q : Type) where
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)
44 | mgraph : (atoms : Nat) -> F1 q (MGraph q)
45 | mgraph atoms = T1.do
47 | ixs <- ref1 SM.empty
49 | g <- marray1 (S atoms) (A (cast {from = Elem} C) empty)
50 | pure (MG atoms atm ixs bnd g)
53 | record CSTCK (q : Type) where
58 | positions_ : Ref q (SnocList Position)
61 | h1,h2,h3 : Ref q MolLine
64 | mgraph : Ref q (MGraph q)
65 | stack_ : Ref q (SnocList Molfile)
66 | groups : Ref q (SortedMap Nat String)
68 | isEmpty : Ref q Bool
71 | sdhead : Ref q SDHeader
72 | sdvals : Ref q (SnocList StructureData)
75 | error_ : Ref q (Maybe $
BoundedErr MolErr)
76 | bytes_ : Ref q ByteString
77 | strings_ : Ref q (SnocList String)
80 | %runElab derive "CSTCK" [HasPosition,HasError,HasBytes,HasStack,HasStringLits]
83 | init : F1 q (CSTCK q)
94 | grp <- ref1 SM.empty
103 | pure (CK l c ps h1 h2 h3 gr gs grp cnt ie sdh sdd err bs str pos)