Chem.Query

Definitions

0 TargetBond : Type

  The type of bond we use at the target molecule of
  a substructure search

Totality: total
Visibility: public export

0 QueryBond : Type

  The type of bond we use at the query molecule of
  a substructure search

Totality: total
Visibility: public export

matchBond : QueryBond -> TargetBond -> Bool

  Default matcher for bonds in a substructure search

Totality: total
Visibility: export

qbond : Cast b BondOrder => AromBond b -> AromBond BondOrder

Totality: total
Visibility: export

record TotH : Type

  Total number (explicit and implicit) of hydrogens bound to an atom.

Totality: total
Visibility: public export
Constructor: 

TH : Nat -> TotH

Projection: 

.count : TotH -> Nat

.count : TotH -> Nat

Totality: total
Visibility: public export

count : TotH -> Nat

Totality: total
Visibility: public export

0 TargetAtom : Type

  Atom type we use for the target in a substructure search.
  
  Note: `TotH` is a counter corresponding to the total number (explicit and
  implicit) of hydrogen atoms bound to an atom.

Totality: total
Visibility: public export

record ExplicitH : Type

  Number of explicit hydrogens bound to an atom.

Totality: total
Visibility: public export
Constructor: 

EH : Nat -> ExplicitH

Projection: 

.count : ExplicitH -> Nat

.count : ExplicitH -> Nat

Totality: total
Visibility: public export

count : ExplicitH -> Nat

Totality: total
Visibility: public export

0 QueryAtom : Type

  Atom type we use for the query in a substructure search.
  
  Note: `ExplicitH` is a counter corresponding to number of explicit
  hydrogens bound to an atom.

Totality: total
Visibility: public export

matchAtom : QueryAtom -> TargetAtom -> Bool

  Default matcher for atoms in a substructure search

Totality: total
Visibility: export

0 QueryGraph : Type

  Graph type we use for the query in substructure searches.

Totality: total
Visibility: public export

0 TargetGraph : Type

  Graph type we use for the target in substructure searches.

Totality: total
Visibility: public export

toTarget : Cast b BondOrder => Cast e Isotope => Cast c Charge => IGraph k (AromBond b) (Atom e c p r h t ch l) -> Cast h HCount => IGraph k TargetBond TargetAtom

  Convert an aromatized molecular graph to a target graph to be
  used in a subgraph query.

Totality: total
Visibility: export

toQuery : Cast b BondOrder => Cast e Isotope => Cast c Charge => IGraph k (AromBond b) (Atom e c p r h t ch l) -> Graph QueryBond QueryAtom

  Convert an aromatized molecular graph to a query graph to be
  used in a subgraph query.

Totality: total
Visibility: export

smilesQuery : SmilesGraphAT -> QueryGraph

  Convert a SMILES graph to one used as a query in a substructure search.

Totality: total
Visibility: export

smilesTarget : SmilesGraphAT -> TargetGraph

  Convert a SMILES graph to one used as a target in a substructure search.

Totality: total
Visibility: export

molQuery : MolGraphAT -> QueryGraph

  Convert a .mol-file graph to one used as a query in a substructure search.

Totality: total
Visibility: export

molTarget : MolGraphAT -> TargetGraph

  Convert a .mol-file graph to one used as a target in a substructure search.

Totality: total
Visibility: export

substructureI : IGraph q QueryBond QueryAtom -> IGraph t TargetBond TargetAtom -> Maybe (Vect q (Fin t))

  Tries to find a mapping from the query graph to the target graph
  
  TODO: Add support for a search limit to make this provably total!

Totality: total
Visibility: export

substructure : QueryGraph -> TargetGraph -> Maybe (List Nat)

  Tries to find a mapping from the query graph to the target graph.
  
  The mapping is returned as a list of node indices. If you need stronger
  quarantees about the indices, consider using `substructureI` for
  order-indexed graphs.

Totality: total
Visibility: export