Idris2Doc : Text.Molfile.Parser.Stack

Text.Molfile.Parser.Stack

(source)
Reexports
import public Text.ILex
import public Text.Molfile.Types
Definitions
record MGraph : Type -> Type
  A molecular graph in the making.

  Totality: total
  Visibility: public export
  Constructor: 
MG : (atoms : Nat) -> Ref q (Fin (S atoms)) -> Ref q (SortedMap Nat (Fin (S atoms))) -> Ref q (Maybe (Edge (S atoms) MolBond)) -> MArray q (S atoms) (Adj (S atoms) MolBond MolAtom) -> MGraph q

  Projections:
  
.atom : ({rec:0} : MGraph q) -> Ref q (Fin (S (atoms {rec:0})))
  
.atoms : MGraph q -> Nat
  
.bond : ({rec:0} : MGraph q) -> Ref q (Maybe (Edge (S (atoms {rec:0})) MolBond))
  
.graph : ({rec:0} : MGraph q) -> MArray q (S (atoms {rec:0})) (Adj (S (atoms {rec:0})) MolBond MolAtom)
  
.indices : ({rec:0} : MGraph q) -> Ref q (SortedMap Nat (Fin (S (atoms {rec:0}))))
.atoms : MGraph q -> Nat
  Totality: total
  Visibility: public export
atoms : MGraph q -> Nat
  Totality: total
  Visibility: public export
.atom : ({rec:0} : MGraph q) -> Ref q (Fin (S (atoms {rec:0})))
  Totality: total
  Visibility: public export
atom : ({rec:0} : MGraph q) -> Ref q (Fin (S (atoms {rec:0})))
  Totality: total
  Visibility: public export
.indices : ({rec:0} : MGraph q) -> Ref q (SortedMap Nat (Fin (S (atoms {rec:0}))))
  Totality: total
  Visibility: public export
indices : ({rec:0} : MGraph q) -> Ref q (SortedMap Nat (Fin (S (atoms {rec:0}))))
  Totality: total
  Visibility: public export
.bond : ({rec:0} : MGraph q) -> Ref q (Maybe (Edge (S (atoms {rec:0})) MolBond))
  Totality: total
  Visibility: public export
bond : ({rec:0} : MGraph q) -> Ref q (Maybe (Edge (S (atoms {rec:0})) MolBond))
  Totality: total
  Visibility: public export
.graph : ({rec:0} : MGraph q) -> MArray q (S (atoms {rec:0})) (Adj (S (atoms {rec:0})) MolBond MolAtom)
  Totality: total
  Visibility: public export
graph : ({rec:0} : MGraph q) -> MArray q (S (atoms {rec:0})) (Adj (S (atoms {rec:0})) MolBond MolAtom)
  Totality: total
  Visibility: public export
mgraph : Nat -> F1 q (MGraph q)
  Totality: total
  Visibility: export
record CSTCK : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
CK : (bufSize_ : Nat) -> ByteString -> IBuffer bufSize_ -> Nat -> Nat -> Ref q (LTENat bufSize_) -> Ref q (LTENat bufSize_) -> Ref q (SnocList BytePos) -> Ref q MolLine -> Ref q MolLine -> Ref q MolLine -> Ref q (MGraph q) -> Ref q (SnocList Molfile) -> Ref q (SortedMap Nat String) -> Ref q Nat -> Ref q Bool -> Ref q SDHeader -> Ref q (SnocList StructureData) -> Ref q (Maybe (BBErr MolErr)) -> Ref q (SnocList String) -> Ref q Nat -> CSTCK q

  Projections:
  
.bufSize_ : CSTCK q -> Nat
  
.count : CSTCK q -> Ref q Nat
  
.curOffset_ : CSTCK q -> Nat
  
.cur_ : ({rec:0} : CSTCK q) -> IBuffer (bufSize_ {rec:0})
  
.error_ : CSTCK q -> Ref q (Maybe (BBErr MolErr))
  
.from_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  
.groups : CSTCK q -> Ref q (SortedMap Nat String)
  
.h1 : CSTCK q -> Ref q MolLine
  
.h2 : CSTCK q -> Ref q MolLine
  
.h3 : CSTCK q -> Ref q MolLine
  
.isEmpty : CSTCK q -> Ref q Bool
  
.mgraph : CSTCK q -> Ref q (MGraph q)
  
.pos : CSTCK q -> Ref q Nat
  
.positions_ : CSTCK q -> Ref q (SnocList BytePos)
  
.prevOffset_ : CSTCK q -> Nat
  
.prev_ : CSTCK q -> ByteString
  
.sdhead : CSTCK q -> Ref q SDHeader
  
.sdvals : CSTCK q -> Ref q (SnocList StructureData)
  
.stack_ : CSTCK q -> Ref q (SnocList Molfile)
  
.strings_ : CSTCK q -> Ref q (SnocList String)
  
.till_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))

  Hints:
  
HasBBErr CSTCK MolErr
  
HasBytes CSTCK
  
HasStack CSTCK (SnocList Molfile)
  
HasStringLits CSTCK
.bufSize_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
bufSize_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
.prev_ : CSTCK q -> ByteString
  Totality: total
  Visibility: public export
prev_ : CSTCK q -> ByteString
  Totality: total
  Visibility: public export
.cur_ : ({rec:0} : CSTCK q) -> IBuffer (bufSize_ {rec:0})
  Totality: total
  Visibility: public export
cur_ : ({rec:0} : CSTCK q) -> IBuffer (bufSize_ {rec:0})
  Totality: total
  Visibility: public export
.prevOffset_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
prevOffset_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
.curOffset_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
curOffset_ : CSTCK q -> Nat
  Totality: total
  Visibility: public export
.from_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
from_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
.till_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
till_ : ({rec:0} : CSTCK q) -> Ref q (LTENat (bufSize_ {rec:0}))
  Totality: total
  Visibility: public export
.positions_ : CSTCK q -> Ref q (SnocList BytePos)
  Totality: total
  Visibility: public export
positions_ : CSTCK q -> Ref q (SnocList BytePos)
  Totality: total
  Visibility: public export
.h3 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
.h2 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
.h1 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
h3 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
h2 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
h1 : CSTCK q -> Ref q MolLine
  Totality: total
  Visibility: public export
.mgraph : CSTCK q -> Ref q (MGraph q)
  Totality: total
  Visibility: public export
mgraph : CSTCK q -> Ref q (MGraph q)
  Totality: total
  Visibility: public export
.stack_ : CSTCK q -> Ref q (SnocList Molfile)
  Totality: total
  Visibility: public export
stack_ : CSTCK q -> Ref q (SnocList Molfile)
  Totality: total
  Visibility: public export
.groups : CSTCK q -> Ref q (SortedMap Nat String)
  Totality: total
  Visibility: public export
groups : CSTCK q -> Ref q (SortedMap Nat String)
  Totality: total
  Visibility: public export
.count : CSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
count : CSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
.isEmpty : CSTCK q -> Ref q Bool
  Totality: total
  Visibility: public export
isEmpty : CSTCK q -> Ref q Bool
  Totality: total
  Visibility: public export
.sdhead : CSTCK q -> Ref q SDHeader
  Totality: total
  Visibility: public export
sdhead : CSTCK q -> Ref q SDHeader
  Totality: total
  Visibility: public export
.sdvals : CSTCK q -> Ref q (SnocList StructureData)
  Totality: total
  Visibility: public export
sdvals : CSTCK q -> Ref q (SnocList StructureData)
  Totality: total
  Visibility: public export
.error_ : CSTCK q -> Ref q (Maybe (BBErr MolErr))
  Totality: total
  Visibility: public export
error_ : CSTCK q -> Ref q (Maybe (BBErr MolErr))
  Totality: total
  Visibility: public export
.strings_ : CSTCK q -> Ref q (SnocList String)
  Totality: total
  Visibility: public export
strings_ : CSTCK q -> Ref q (SnocList String)
  Totality: total
  Visibility: public export
.pos : CSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
pos : CSTCK q -> Ref q Nat
  Totality: total
  Visibility: public export
init : (n : Nat) -> IBuffer n -> F1 q (CSTCK q)
  Totality: total
  Visibility: export
setPos : CSTCK q => Nat -> F1' q
  Totality: total
  Visibility: export
incPos : CSTCK q => Nat -> F1 q Nat
  Totality: total
  Visibility: export