Text.Molfile.Parser.Stack

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 : Ref q Nat -> Ref q Nat -> Ref q (SnocList Position) -> 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 (BoundedErr MolErr)) -> Ref q ByteString -> Ref q (SnocList String) -> Ref q Nat -> CSTCK q

Projections:

.bytes_ : CSTCK q -> Ref q ByteString
.col_ : CSTCK q -> Ref q Nat
.count : CSTCK q -> Ref q Nat
.error_ : CSTCK q -> Ref q (Maybe (BoundedErr MolErr))
.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
.line_ : CSTCK q -> Ref q Nat
.mgraph : CSTCK q -> Ref q (MGraph q)
.pos : CSTCK q -> Ref q Nat
.positions_ : CSTCK q -> Ref q (SnocList Position)
.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)

Hints:

HasBytes CSTCK
HasError CSTCK MolErr
HasPosition CSTCK
HasStack CSTCK (SnocList Molfile)
HasStringLits CSTCK

.line_ : CSTCK q -> Ref q Nat

Totality: total
Visibility: public export

line_ : CSTCK q -> Ref q Nat

Totality: total
Visibility: public export

.col_ : CSTCK q -> Ref q Nat

Totality: total
Visibility: public export

col_ : CSTCK q -> Ref q Nat

Totality: total
Visibility: public export

.positions_ : CSTCK q -> Ref q (SnocList Position)

Totality: total
Visibility: public export

positions_ : CSTCK q -> Ref q (SnocList Position)

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 (BoundedErr MolErr))

Totality: total
Visibility: public export

error_ : CSTCK q -> Ref q (Maybe (BoundedErr MolErr))

Totality: total
Visibility: public export

.bytes_ : CSTCK q -> Ref q ByteString

Totality: total
Visibility: public export

bytes_ : CSTCK q -> Ref q ByteString

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 : F1 q (CSTCK q)

Totality: total
Visibility: export