Text.Molfile.Types

(source)

Some of the refined types in here should probably
go to their own dedicated module

Reexports

import public Text.Molfile.SData
import public Chem
import public Data.Vect

Definitions

record MolLine : Type

  An uninterpreted line in a v2000 mol file

Totality: total
Visibility: public export
Constructor:

MkMolLine : String -> MolLine

Projection:

.value : MolLine -> String

Hints:

Cast ByteString MolLine
Eq MolLine
FromString MolLine
Interpolation MolLine
Ord MolLine
Show MolLine

.value : MolLine -> String

Totality: total
Visibility: public export

value : MolLine -> String

Totality: total
Visibility: public export

data MolVersion : Type

Totality: total
Visibility: public export
Constructors:

V2000 : MolVersion
V3000 : MolVersion

Hints:

Eq MolVersion
Finite MolVersion
Interpolation MolVersion
Ord MolVersion
Show MolVersion

data ChiralFlag : Type

Totality: total
Visibility: public export
Constructors:

NonChiral : ChiralFlag
Chiral : ChiralFlag

Hints:

Eq ChiralFlag
Finite ChiralFlag
Interpolation ChiralFlag
Ord ChiralFlag
Show ChiralFlag

data AtomSymbol : Type

  Ast    -> Asterisk
  RSharp -> R# (RGroupLabel)

Totality: total
Visibility: public export
Constructors:

L : AtomSymbol
A : AtomSymbol
Q : AtomSymbol
Ast : AtomSymbol
LP : AtomSymbol
RSharp : AtomSymbol
El : Elem -> AtomSymbol

Hints:

Cast Elem AtomSymbol
Eq AtomSymbol
Finite AtomSymbol
Interpolation AtomSymbol
Show AtomSymbol

data StereoParity : Type

  Atom Stereo parity encoded in V2000 CTAB

Totality: total
Visibility: public export
Constructors:

NoStereo : StereoParity
OddStereo : StereoParity
EvenStereo : StereoParity
AnyStereo : StereoParity

Hints:

Eq StereoParity
Finite StereoParity
Interpolation StereoParity
Ord StereoParity
Show StereoParity

data StereoCareBox : Type

  Stereo care box encoded in V2000

Totality: total
Visibility: public export
Constructors:

IgnoreStereo : StereoCareBox
MatchStereo : StereoCareBox

Hints:

Eq StereoCareBox
Finite StereoCareBox
Interpolation StereoCareBox
Ord StereoCareBox
Show StereoCareBox

record Valence : Type

  Valence of atoms
  
  NOTE: In a V2000 molfile 15 is zero valence,
  while 0 means no marking

Totality: total
Visibility: public export
Constructor:

MkValence : (value : Bits8) -> {auto 0 _ : value <= 15} -> Valence

Projections:

0 .prf : ({rec:0} : Valence) -> value {rec:0} <= 15
.value : Valence -> Bits8

Hints:

Eq Valence
Finite Valence
Interpolation Valence
Ord Valence
Show Valence

.value : Valence -> Bits8

Totality: total
Visibility: public export

value : Valence -> Bits8

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Valence) -> value {rec:0} <= 15

Totality: total
Visibility: public export

0 prf : ({rec:0} : Valence) -> value {rec:0} <= 15

Totality: total
Visibility: public export

data H0Designator : Type

  Reduntant hydrogen count flag

Totality: total
Visibility: public export
Constructors:

H0NotSpecified : H0Designator
NoHAllowed : H0Designator

Hints:

Eq H0Designator
Finite H0Designator
Interpolation H0Designator
Ord H0Designator
Show H0Designator

record HydrogenCount : Type

  HCount plus 1: 0 means "not explicitly given"
  1 means "explicitly 0" and so on.

Totality: total
Visibility: public export
Constructor:

MkHC : (value : Bits8) -> {auto 0 _ : value <= 5} -> HydrogenCount

Projections:

0 .prf : ({rec:0} : HydrogenCount) -> value {rec:0} <= 5
.value : HydrogenCount -> Bits8

Hints:

Eq HydrogenCount
Finite HydrogenCount
Interpolation HydrogenCount
Ord HydrogenCount
Show HydrogenCount

.value : HydrogenCount -> Bits8

Totality: total
Visibility: public export

value : HydrogenCount -> Bits8

Totality: total
Visibility: public export

0 .prf : ({rec:0} : HydrogenCount) -> value {rec:0} <= 5

Totality: total
Visibility: public export

0 prf : ({rec:0} : HydrogenCount) -> value {rec:0} <= 5

Totality: total
Visibility: public export

record Coordinate : Type

  We encode coordinates as a sufficiently precise integer
  to prevent loss of precision during parsing.

Totality: total
Visibility: public export
Constructor:

MkCoordinate : (value : Integer) -> {auto 0 _ : FromTo -99999999 999999999 value} -> Coordinate

Projections:

0 .prf : ({rec:0} : Coordinate) -> FromTo -99999999 999999999 (value {rec:0})
.value : Coordinate -> Integer

Hints:

Cast Coordinate Double
Eq Coordinate
GetPoint (Vect 3 Coordinate)
Interpolation Coordinate
ModPoint (Vect 3 Coordinate)
Ord Coordinate
Show Coordinate

.value : Coordinate -> Integer

Totality: total
Visibility: public export

value : Coordinate -> Integer

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Coordinate) -> FromTo -99999999 999999999 (value {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : Coordinate) -> FromTo -99999999 999999999 (value {rec:0})

Totality: total
Visibility: public export

Precision : Integer

Totality: total
Visibility: public export

dispCoordShort : Coordinate -> String

  Space-efficient version of `interpolate` to be used in V3000
  mol files.

Totality: total
Visibility: export

0 Coordinates : Type

  Convenience alias for `Vect 3 Coordinates`

Totality: total
Visibility: public export

record AtomGroup : Type

Totality: total
Visibility: public export
Constructor:

G : Nat -> String -> AtomGroup

Projections:

.lbl : AtomGroup -> String
.nr : AtomGroup -> Nat

Hints:

Eq AtomGroup
Show AtomGroup

.nr : AtomGroup -> Nat

Totality: total
Visibility: public export

nr : AtomGroup -> Nat

Totality: total
Visibility: public export

.lbl : AtomGroup -> String

Totality: total
Visibility: public export

lbl : AtomGroup -> String

Totality: total
Visibility: public export

0 MolAtom' : Type -> Type -> Type -> Type

  Regular atom loaded from a .mol file.
  
  Note: .mol files support additional atom symbols
  (for instance, for queries), but for real-world molecules,
  this is the type to use.
  
  The type parameters are used for implicit hydrogens and atom types,
  which are `()` for freshly loaded `MolAtom`s but more specific after
  atom type perception.

Totality: total
Visibility: public export

0 MolAtom : Type

  Regular atom loaded from a .mol file.
  
  Note: .mol files support additional atom symbols
  (for instance, for queries), but for real-world molecules,
  this is the type to use.

Totality: total
Visibility: public export

0 MolAtomAT : Type

  .mol-file atom with perceived atom type and computed
  implicit hydrogen count

Totality: total
Visibility: public export

data QueryBondType : Type

Totality: total
Visibility: public export
Constructors:

BT : BondOrder -> QueryBondType
Arom : QueryBondType
SngOrDbl : QueryBondType
SngOrAromatic : QueryBondType
DblOrAromatic : QueryBondType
AnyBond : QueryBondType

Hints:

Eq QueryBondType
Interpolation QueryBondType
Ord QueryBondType
Show QueryBondType

data BondStereo : Type

  Stereoinformation represented in molfiles

Totality: total
Visibility: public export
Constructors:

NoBondStereo : BondStereo
Up : BondStereo
Either : BondStereo
Down : BondStereo

Hints:

Cast MolBond BondStereo
Cast BondStereo MolBond
Eq BondStereo
Finite BondStereo
Interpolation BondStereo
Ord BondStereo
Show BondStereo

data BondTopo : Type

  Bond topology encoded in CTAB V2000

Totality: total
Visibility: public export
Constructors:

AnyTopology : BondTopo
Ring : BondTopo
Chain : BondTopo

Hints:

Eq BondTopo
Finite BondTopo
Interpolation BondTopo
Ord BondTopo
Show BondTopo

record MolBond : Type

Totality: total
Visibility: public export
Constructor:

MkBond : Bool -> BondOrder -> BondStereo -> MolBond

Projections:

.firstSmaller : MolBond -> Bool

  Flag indicating whether the bond goes from the
  atom with the smaller index to the one with the larger index
  or vice versa.
  
  We need this to figure out in which direction wedged bonds should
  point.

.stereo : MolBond -> BondStereo

.type : MolBond -> BondOrder

Hints:

Cast MolBond BondOrder
Cast BondOrder MolBond
Cast MolBond BondStereo
Cast BondStereo MolBond
Eq MolBond
Show MolBond

.firstSmaller : MolBond -> Bool

  Flag indicating whether the bond goes from the
  atom with the smaller index to the one with the larger index
  or vice versa.
  
  We need this to figure out in which direction wedged bonds should
  point.

Totality: total
Visibility: public export

firstSmaller : MolBond -> Bool

  Flag indicating whether the bond goes from the
  atom with the smaller index to the one with the larger index
  or vice versa.
  
  We need this to figure out in which direction wedged bonds should
  point.

Totality: total
Visibility: public export

.type : MolBond -> BondOrder

Totality: total
Visibility: public export

type : MolBond -> BondOrder

Totality: total
Visibility: public export

.stereo : MolBond -> BondStereo

Totality: total
Visibility: public export

stereo : MolBond -> BondStereo

Totality: total
Visibility: public export

data SGroupType : Type

Totality: total
Visibility: public export
Constructors:

SUP : SGroupType
Other : SGroupType

Hints:

Eq SGroupType
Finite SGroupType
Show SGroupType

0 MolGraph' : Type -> Type -> Type -> Type

Totality: total
Visibility: public export

0 MolGraph : Type

Totality: total
Visibility: public export

0 MolGraphAT : Type

  .mol-file graph with perceived atom types and computed
  implicit hydrogen counts

Totality: total
Visibility: public export

record Molfile' : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor:

MkMolfile : MolLine -> MolLine -> MolLine -> MolGraph' h t c -> List StructureData -> Molfile' h t c

Projections:

.comment : Molfile' h t c -> MolLine
.dat : Molfile' h t c -> List StructureData
.graph : Molfile' h t c -> MolGraph' h t c
.info : Molfile' h t c -> MolLine
.name : Molfile' h t c -> MolLine

Hints:

Eq h => Eq t => Eq c => Eq (Molfile' h t c)
Show h => Show t => Show c => Show (Molfile' h t c)

.name : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

name : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

.info : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

info : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

.comment : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

comment : Molfile' h t c -> MolLine

Totality: total
Visibility: public export

.graph : Molfile' h t c -> MolGraph' h t c

Totality: total
Visibility: public export

graph : Molfile' h t c -> MolGraph' h t c

Totality: total
Visibility: public export

.dat : Molfile' h t c -> List StructureData

Totality: total
Visibility: public export

dat : Molfile' h t c -> List StructureData

Totality: total
Visibility: public export

emptyMolFile : Molfile' h t c

Totality: total
Visibility: export

0 Molfile : Type

Totality: total
Visibility: public export

0 MolfileAT : Type

Totality: total
Visibility: public export

data MolErr : Type

Totality: total
Visibility: public export
Constructors:

MCharge : Integer -> MolErr
MMass : Integer -> MolErr
MRadical : Integer -> MolErr
MBondOrder : Integer -> MolErr
MBondStereo : Integer -> MolErr
MEntries : MolErr
MAbbr : MolErr
MNode : Nat -> MolErr

Hints:

Eq MolErr
HasBBErr CSTCK MolErr
Interpolation MolErr
Show MolErr