Idris2Doc : CyBy.Draw.Internal.Graph

CyBy.Draw.Internal.Graph

(source)
Definitions
data NOE : Type -> Type -> Type
  In several places, we decide what to do on a UI event
  based on whether any nodes or edges are selected or being
  hovered over.

  Totality: total
  Visibility: public export
  Constructors:
  
None : NOE a b
  
N : a -> NOE a b
  
E : b -> NOE a b
noe : Maybe a -> Lazy (Maybe b) -> NOE a b
  Creates an `NOE` from two `Maybe`s.

  Totality: total
  Visibility: export
eon : Lazy (Maybe a) -> Maybe b -> NOE a b
  Like `noe`, but edges take precedence.

  Totality: total
  Visibility: export
eons : List a -> Lazy (List b) -> NOE (List a) (List b)
  Creates an `NOE` from two `Lists`s.
  
  This returns `None` in case both lists are empty.

  Totality: total
  Visibility: export
record CDBond : Type
  Bond type used in cyby-draw.
  
  This is an mol-file bond paired with a role used for drawing.

  Totality: total
  Visibility: public export
  Constructor: 
CB : Role -> MolBond -> CDBond

  Projections:
  
.molBond : CDBond -> MolBond
  
.role : CDBond -> Role

  Hints:
  
Cast CDBond Role
  
Eq CDBond
  
ModRole CDBond
  
Show CDBond
.role : CDBond -> Role
  Totality: total
  Visibility: public export
role : CDBond -> Role
  Totality: total
  Visibility: public export
.molBond : CDBond -> MolBond
  Totality: total
  Visibility: public export
molBond : CDBond -> MolBond
  Totality: total
  Visibility: public export
0 CDGraph : Type
  Graph type used for drawing molecules.

  Totality: total
  Visibility: public export
0 CDIGraph : Nat -> Type
  Order-indexed graph type used for drawing molecules.

  Totality: total
  Visibility: public export
toMolGraph : Graph CDBond CDAtom -> MolGraphAT
  Totality: total
  Visibility: export
toMolfile : Graph CDBond CDAtom -> MolfileAT
  Totality: total
  Visibility: export
initGraph : MolGraphAT -> CDGraph
  Initialize a mol-file graph (with perceived atom types) to be used
  in one of the drawing canvases. This includes normalizing the
  molecule to a bond-length of 1.25 Angstrom.

  Totality: total
  Visibility: export
readMolfileE : String -> Either String CDGraph
  Reads and initializes a `CDGraph` from a mol-file string.

  Totality: total
  Visibility: export
readMolfile : String -> CDGraph
  Like `readMolfileE` but returns the empty graph in case of a read error.

  Totality: total
  Visibility: export
adjAtomTypes : CDIGraph k -> CDIGraph k
  Re-calculates the atom types of a mol graph.

  Totality: total
  Visibility: export
newBond : BondOrder -> BondStereo -> MolBond -> MolBond
  Totality: total
  Visibility: export
highlight : List Nat -> CDGraph -> CDGraph
  Highlight the nodes corresponding to the given natural numbers.

  Totality: total
  Visibility: export
groupNr : CDIGraph k -> Fin k -> Maybe Nat
  Returns the number of the abbreviation group of an atom (if any).

  Totality: total
  Visibility: export
inAbbreviation : CDIGraph k -> Fin k -> Bool
  True, if the given node is part of an abbreviation.

  Totality: total
  Visibility: export
maxGroupNr : CDIGraph k -> Nat
  Returns the largest group number in the given graph.

  Totality: total
  Visibility: export
groupNrs : CDIGraph k -> SortedSet Nat
  Returns the group numbers found in a molecule

  Totality: total
  Visibility: export
adjTemplate : CDIGraph k -> CDIGraph m -> CDIGraph m
  Adjusts abbreviation numbers of a template before merging it
  with an existing molecule.
  
  This avoids having several abbreviations with the same number
  in the new (merged) molecule, which would then all be expanded at
  the same time with a single double click.

  Totality: total
  Visibility: export
anyNotInGroup : CDIGraph k -> Fin k -> Nat -> Bool
  True, if any neighbour of the given node is part of the given
  abbreviation (given as its ID).

  Totality: total
  Visibility: export
customLabel : CDIGraph k -> Fin k -> Maybe String
  Custom label to be displayed for a node (if any).

  Totality: total
  Visibility: export
visible : CDIGraph k -> Fin k -> Bool
  An atom is visible, if a) it is not part of an abbreviation, or b),
  at least one of its neighbours is not part of an abbreviation.

  Totality: total
  Visibility: export
labelVisible : Bool -> CDIGraph k -> Fin k -> Bool
  We show an atom's label if a) it is a non-carbon, b) it is an isolate
  carbon (no explicit neighbours), or c) `s.showC` is set to `True`

  Totality: total
  Visibility: export
visibleNodes : CDIGraph k -> List (Fin k)
  Returns a list of those nodes of a molecule that will be visible
  in the drawing, that is, nodes that are not hidden because
  they are part of an abbreviation.

  Totality: total
  Visibility: export
atomsIn : CDIGraph k -> Bounds2D Mol -> List (Fin k)
  Returns the visible nodes that within the given bounds.

  Totality: total
  Visibility: export
visibleNeighbours : CDIGraph k -> Fin k -> List (Fin k)
  Returns the list of visible neighbours of an atome, that is,
  neighbours that are not hidded because they are part of an
  abbreviation.

  Totality: total
  Visibility: export
hiddenNodes : CDIGraph k -> List (Fin k)
  Returns a list of those nodes of a molecule that are hidden
  because they are part of an abbreviation.

  Totality: total
  Visibility: export
visibleEdges : CDIGraph k -> List (Edge k CDBond)
  Returns a list of those edges of a molecule that will be visible
  in the drawing, that is, edges that are not hidden because
  they are part of an abbreviation.

  Totality: total
  Visibility: export
groupNodes : CDIGraph k -> List (Fin k) -> List (Fin k)
  Given a list `ns` of nodes in a molecule, returns a list containing
  also the other nodes belonging to the same abbreviations (if any)
  as the nodes in `ns`.
  transitively via abbreviations.

  Totality: total
  Visibility: export
plusGroupNodes : CDIGraph k -> List (Fin k) -> List (Fin k)
  Given a list `ns` of nodes in a molecule, returns a list containing
  also the other nodes belonging to the same abbreviations (if any)
  as the nodes in `ns`.
  transitively via abbreviations.

  Totality: total
  Visibility: export
pointAt : CDIGraph k -> Fin k -> Point Id
  Returns the position of the given node in a mol graph.

  Totality: total
  Visibility: export
bondAngles : CDIGraph k -> Fin k -> List Angle
  Computes the angles of all visible bonds connecting the given node.

  Totality: total
  Visibility: export
closestNodeList : CoreDims => List (Fin k) -> Point Id -> CDIGraph k -> Maybe (Fin k)
  Returns the node closest to the given point,
  but only if it is closer than the defined atom radius.

  Totality: total
  Visibility: export
closestNodeWhere : CoreDims => (Fin k -> Bool) -> Point Id -> CDIGraph k -> Maybe (Fin k)
  Finds the visible node closest to the given point, but only
  if it is closer than the defined atom radius and it fulfills
  the given predicate.

  Totality: total
  Visibility: export
closestNode : CoreDims => Point Id -> CDIGraph k -> Maybe (Fin k)
  Finds the visible node closest to the given point, but only
  if it is closer than the defined atom radius.

  Totality: total
  Visibility: export
closestEdge : CoreDims => Point Id -> CDIGraph k -> Maybe (Edge k CDBond)
  Finds the visible edge closest to the given point, but only
  if it is closer than the defined atom radius.

  Totality: total
  Visibility: export
closestItem : CoreDims => Point Id -> CDIGraph k -> NOE (Fin k) (Edge k CDBond)
  Returns the item (node or edge) closest to the current mouse position.

  Totality: total
  Visibility: export
approxBounds : CoreDims => CDIGraph k -> Fin k -> Bounds2D Id
  Generously approximates the bounds of an atom in the drawing.

  Totality: total
  Visibility: export
clear : CDGraph -> CDGraph
  Removes all roles from atoms and bonds in the given graph.

  Totality: total
  Visibility: export
cleanup : CDGraph -> CDGraph
  Unset all roles with the exception of `Hover` and `Selected`

  Totality: total
  Visibility: export
hover : CoreDims => (CDBond -> Bool -> Bool) -> (CDAtom -> Bool) -> Point Id -> CDIGraph k -> CDIGraph k
  Adjusts the `Hovering` flag of all atoms and edges in the molecule.
  The visible atom closest to the given point is set to
  `Hover` if it is not further away than `radiusAtom`.
  
  Otherwise, the visible edge closest to the given point is set to
  `Hovering` if it is not further away than `radiusAtom`.
  
  If the atom, over which the mouse hovers is part of an abbreviation,
  all other atoms in the abbreviations will be set to `Hovering` as well.
  
  The `hatom` predicate is used to figure out if we can currently hover over
  a given atom.
  
  The `hbond` predicate is used to figure out if we can currently hover over
  a given bond (its bool argument should be `True`, if the bond is connected
  to at least one atom in an abbreviation group)

  Totality: total
  Visibility: export
ifHover : Role -> CDGraph -> CDGraph
  Adds the given role to the currently hovered atoms

  Totality: total
  Visibility: export
replaceWith : Cast a Role => ModRole a => Role -> Role -> a -> a
  Replaces a given old Role with a given new Role.
  For all other nodes, it removes the new Role.
  
  For example:
  - If 'New' is currently set, it removes 'New' and sets 'Hover'.
  - If 'Hover' is set, it removes 'Hover'.

  Totality: total
  Visibility: export
hoverIfNew : CDGraph -> CDGraph
  'New' is replaced with 'Hover', and any existing 'Hover' roles are removed.

  Totality: total
  Visibility: export
hoveredItem : CDIGraph k -> NOE (Fin k, CDAtom) (Edge k CDBond)
  Returns the currently hovered edges or atoms atoms

  Totality: total
  Visibility: export
selectHovered : SelectMode -> SelectMode -> CDGraph -> CDGraph
  Selects the currently hovered atoms and bonds.
  
  The `SelectMode` flags indicate, if currently selected items should
  be kept or not, or if no item should be selected at all. The first
  value is used for edge selection and the second for node selection.

  Totality: total
  Visibility: export
record SelectZones : Type
  Totality: total
  Visibility: public export
  Constructor: 
SZ : Point Id -> Point Id -> Point Id -> Point Id -> SelectZones

  Projections:
  
.dragLR : SelectZones -> Point Id
  
.dragUL : SelectZones -> Point Id
  
.rotLR : SelectZones -> Point Id
  
.rotUL : SelectZones -> Point Id
.dragUL : SelectZones -> Point Id
  Totality: total
  Visibility: public export
dragUL : SelectZones -> Point Id
  Totality: total
  Visibility: public export
.dragLR : SelectZones -> Point Id
  Totality: total
  Visibility: public export
dragLR : SelectZones -> Point Id
  Totality: total
  Visibility: public export
.rotUL : SelectZones -> Point Id
  Totality: total
  Visibility: public export
rotUL : SelectZones -> Point Id
  Totality: total
  Visibility: public export
.rotLR : SelectZones -> Point Id
  Totality: total
  Visibility: public export
rotLR : SelectZones -> Point Id
  Totality: total
  Visibility: public export
select : Point Id -> Point Id -> CDGraph -> CDGraph
  Selects all nodes that are a) currently being hovered over, or visible
  and in the given rectangle.

  Totality: total
  Visibility: export
isSelected : CDIGraph k -> Bool -> Fin k -> Bool
  Returns `True` if the given node is currently selected.
  
  In case the `includeEdges` flag is set to `True`, this will also
  return `True` if one of the edges connecting the node is currently
  selected.

  Totality: total
  Visibility: export
selectedNodes : CDIGraph k -> Bool -> List (Fin k)
  The list of currently selected nodes.

  Totality: total
  Visibility: export
selectedEdges : CDIGraph k -> List (Fin k, Fin k)
  The list of currently selected edges.

  Totality: total
  Visibility: export
selectedItems : CDIGraph k -> NOE (List (Fin k)) (List (Fin k, Fin k))
  Totality: total
  Visibility: export
selectionCorners : CDGraph -> Maybe (Point Mol, Point Mol)
  Computes the top left and bottom right corner of the bounding box
  containing the currently selected atoms (if any)

  Totality: total
  Visibility: export
selectZones : CoreDims => Point Id -> Point Id -> SelectZones
  Checks, if there is enough space to grab the box in the canvas.

  Totality: total
  Visibility: export
isotopeAt : Isotope -> Point Id -> Role -> CDAtom
  Creates an uncharged atom at the given position and with the given role.

  Totality: total
  Visibility: export
elemAt : Elem -> Point Id -> Role -> CDAtom
  Creates an uncharged atom at the given position and with the given role.

  Totality: total
  Visibility: export
insIsotopeAt : CDIGraph k -> Isotope -> Point Id -> Role -> CDIGraph (S k)
  Inserts an uncharged atom at the given position and with the given
  role.

  Totality: total
  Visibility: export
insElemAt : CDIGraph k -> Elem -> Point Id -> Role -> CDIGraph (S k)
  Inserts an uncharged atom at the given position and with the given
  role.

  Totality: total
  Visibility: export
preferredAngle : Bool -> List Angle -> Angle
  Computes the preferred angle for a new bond based on the bond type
  and angles to already existing bonds.

  Totality: total
  Visibility: export
bestPos : CDIGraph k -> MolBond -> Fin k -> Point Id -> Point Id
  Preferred position for a new atom bound to an existing one based on the
  largest bisector of angles between existing bonds

  Totality: total
  Visibility: export
stepAngles : CoreDims => List Angle
  Equally spaced sequence of `s.angleSteps` angles from 0 until 2pi.

  Totality: total
  Visibility: export
suggestedPos : CoreDims => Bool -> Point Id -> Point Id -> Point Id
  Suggested position for a new atom based on the current mouse position.
  The boolean flag indicates if "Shift" is currently down, in which case
  we just return the current point.

  Totality: total
  Visibility: export
bondTo : CoreDims => CDBond -> Fin k -> Point Id -> Point Id -> CDIGraph k -> Either (CDIGraph k) (CDIGraph (S k))
  Draws a new bond from the given node to the suggested position.
  If another atom is already close to the current mouse position
  or the suggested position, connect the two atoms instead.

  Totality: total
  Visibility: export
nodesToMerge : CoreDims => CDIGraph k -> CDIGraph m -> List (Fin k, Fin m)
  From two graphs, returns pairs of visible nodes closest
  to each other (but no farther apart than `s.radiusAtom`).

  Totality: total
  Visibility: export
mergeCloseNodes : CoreDims => CDIGraph k -> CDGraph
  After moving or rotating the selected nodes in a graph,
  check for pairs of close nodes and merge them.

  Totality: total
  Visibility: export
mergeGraphs' : CoreDims => CDIGraph k -> CDIGraph m -> List (Fin k, (Fin m, CDBond)) -> CDGraph
  Merges two graphs and merges atoms, which are overlapping.
  If bonds should be added between the two graphs, the last argument
  allows a list of the according nodes and its bond type.

  Totality: total
  Visibility: export
mergeGraphs : CoreDims => Point Id -> CDGraph -> CDGraph -> CDGraph
  Add the template to the existing graph depending on clicking on an atom,
  a bond or elsewhere on the canvas.

  Totality: total
  Visibility: export
addBondE : CoreDims => Bool -> Maybe (Point t) -> MolBond -> CDIGraph k -> Either (CDIGraph k) (CDIGraph (S k))
  Attaches an atom to a mol graph.
  
  Depending on the current mouse position and whether "Shift" is
  pressed or not, the drawing tool suggest a different bond length
  and angle for the new bond.

  Totality: total
  Visibility: export
addBond : CoreDims => Bool -> Maybe (Point t) -> MolBond -> CDIGraph k -> CDGraph
  Attaches an atom to a mol graph.
  
  Depending on the current mouse position and whether "Shift" is
  pressed or not, the drawing tool suggest a different bond length
  and angle for the new bond.

  Totality: total
  Visibility: export
addAtom : CoreDims => CDIGraph k -> Isotope -> Point t -> CDGraph
  Adds an uncharged atom of the given isotope at the given position.
  
  This either replaces the currently hovered atom, or it inserts a new
  isolate atom.

  Totality: total
  Visibility: export
setAbbreviationAt : CoreDims => String -> Fin k -> Fin k -> CDIGraph (S m) -> CDIGraph k -> CDGraph
  Totality: total
  Visibility: export
setAbbreviation : CoreDims => Bool -> String -> Point Id -> CDGraph -> CDGraph -> CDGraph
  Replaces the atom or abbreviation at the given position with
  an abbreviation.

  Totality: total
  Visibility: export
expand : CDGraph -> CDGraph
  Expands the currently hovered-over abbreviation (if any)

  Totality: total
  Visibility: export
translateTemplate : CoreDims => Point s -> CDGraph -> CDGraph
  Translating the template to the mouse position and setting the roles to new.

  Totality: total
  Visibility: export
addTemplate : CoreDims => Point s -> CDGraph -> CDGraph -> CDGraph
  Merges a template graph with the current mol graph based on the
  current mouse position.

  Totality: total
  Visibility: export
addTemplateRot : CoreDims => Point s -> Either (Fin n) (Fin n, (Fin k, Point s)) -> CDIGraph k -> CDIGraph n -> CDGraph
  Merges a template graph with the current mol graph based on the
  current mouse position. If an atom is clicked on, the template
  can be rotated around it by the mouse cursor.
  If exactly two atoms (molecule and template) overlap, the template
  can be rotated around the overlapping atoms by holding down the
  the mouse button and moving the cursor.

  Totality: total
  Visibility: export
clearOrphanGroups : List (Fin k) -> CDIGraph k -> CDIGraph k
  Remove the abbreviation labels from orphaned abbreviation atoms.
  The list of nodes have had an edge remove and now belong to potentially
  orphaned abbreviation groups.

  Totality: total
  Visibility: export
deleteSelected : CDGraph -> CDGraph
  Deletes all selected nodes or edge from the graph
  (including nodes selected transitively via abbreviations).
  
  When we delete an edge, we are at risk of creating an orphaned
  abbreviation: An invisible set of abbreviated nodes no longer
  connected to the visible part of the molecule. In such a case,
  we could either delete the whole abbreviation, or make the
  orphaned nodes visible. Here, we opt for the latter. If users
  want to delete the whole abbreviation, they can do so by
  deleting the atom in question.
  
  If no nodes or edges are currently selected, this deletes the
  node or edge that is currently being hovered over.

  Totality: total
  Visibility: export
moveSelected : CoreDims => Point Mol -> Point Mol -> CDGraph -> CDGraph
  Translates the selected atoms in a molecule by a vector given
  as a start and end point.

  Totality: total
  Visibility: export
rotateTempl : CoreDims => Bool -> Point Mol -> Point Mol -> CDGraph -> CDGraph
  Totality: total
  Visibility: export
rotateSelected : CoreDims => Bool -> Point Mol -> Point Mol -> CDGraph -> CDGraph
  Rotates the selected atoms around the center of the selection
  by an angle defined by the two points.
  
  If the `Bool` argument is set to `False`, we use step-wise rotation
  as defined in the `CoreDims` argument, otherwise, we use 
  continuous rotation.

  Totality: total
  Visibility: export
selectedSubgraph : Bool -> CDGraph -> CDGraph
  Extracts the selected subgraph (or the whole graph, if no atoms are
  selected) from a drawing graph.

  Totality: total
  Visibility: export