Idris2Doc : Geom.Point

Geom.Point

(source)
Definitions
record AffineTransformation : Type
  An affine transformation is a linear transformation (currently, a rotation
  or scaling) followed by a translation in the new coordinate system.
  
  We use affine transformations to keep track of the coordinate system
  we are currently in. In the UI, if a user zooms in or moves the canvas,
  the coordinates we get from the UI must be adjusted by reversing these
  transformations in order to get the correct canvas coordinates. These
  need then again be adjusted (by a scaling factor) to get the coordinates
  of the molecule.
  
  In order to make sure these transformations and adjustments are not
  forgotten, we index all `Point`s we work with the the affine transformation
  of the coordinate system they come from. Via function `convert`, points
  from one coordinate system can be converted to the corresponding points in
  another one.

  Totality: total
  Visibility: public export
  Constructor: 
AT : LinearTransformation -> Vector Id -> AffineTransformation

  Projections:
  
.transform : AffineTransformation -> LinearTransformation
  
.translate : AffineTransformation -> Vector Id

  Hints:
  
Bounded (Bounds2D t)
  
Cast (Point s) (Point t)
  
Eq (Point t)
  
GetPoint (Point t)
  
Interpolation (Point t)
  
Interpolation (Bounds2D t)
  
ModPoint (Point t)
  
Monoid (Bounds2D t)
  
Monoid AffineTransformation
  
Ord (Point t)
  
Semigroup (Bounds2D t)
  
Semigroup AffineTransformation
  
Show (Point t)
.transform : AffineTransformation -> LinearTransformation
  Totality: total
  Visibility: public export
transform : AffineTransformation -> LinearTransformation
  Totality: total
  Visibility: public export
.translate : AffineTransformation -> Vector Id
  Totality: total
  Visibility: public export
translate : AffineTransformation -> Vector Id
  Totality: total
  Visibility: public export
Id : AffineTransformation
  The identity transformation

  Totality: total
  Visibility: public export
scaling : Scale -> AffineTransformation
  An affine transformation consisting only of a scaling by the given factor.

  Totality: total
  Visibility: export
inverse : AffineTransformation -> AffineTransformation
  Computes the inverse of an affine transformation so that
  `t <+> inverse t` is the identity (`Id`; modulo rounding errors)

  Totality: total
  Visibility: export
translate : Vector Id -> AffineTransformation
  Creates an affine transformation corresponding to a translation
  by the given vector.

  Totality: total
  Visibility: export
record Point : AffineTransformation -> Type
  A point in an affine space such as the user interface or the
  coordinate system of the molecule.
  
  Unlike `Vector`, a `Point` is somewhat of an abstract entity.
  We can compute a vector for connecting two points, but we cannot
  add two points together (that does not make sense). Likewise, the
  difference between two points results in the vector connecting
  the two.
  
  A point is indexed by the `AffineTransformation` corresponding to its
  coordinate system. See @AffineTransformation for some more details.

  Totality: total
  Visibility: public export
  Constructor: 
P : Double -> Double -> Point t

  Projections:
  
.x : Point t -> Double
  
.y : Point t -> Double

  Hints:
  
Cast (Point s) (Point t)
  
Eq (Point t)
  
GetPoint (Point t)
  
Interpolation (Point t)
  
ModPoint (Point t)
  
Ord (Point t)
  
Show (Point t)
.x : Point t -> Double
  Totality: total
  Visibility: public export
x : Point t -> Double
  Totality: total
  Visibility: public export
.y : Point t -> Double
  Totality: total
  Visibility: public export
y : Point t -> Double
  Totality: total
  Visibility: public export
origin : Point t
  The origin at `(0,0)`.

  Totality: total
  Visibility: export
negate : Neg ty => ty -> ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: prefix operator, level 10
(-) : Point t -> Point t -> Vector (t .transform)
  The difference between two points is the vector connecting
  the points.

  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 8
prefix operator, level 10
convert : Point s -> Point t
  Convert a point from one affine space to its image in another
  affine space.

  Totality: total
  Visibility: export
interface GetPoint : Type -> Type
  Interface for converting a value to a point in the affine space
  represented by transformation `t`.

  Parameters: a
Methods:
  
gtrans : AffineTransformation
  
point : a -> Point gtrans

Implementations:
  
GetPoint (Vect 3 Coordinate)
  
GetPoint MolAtom
  
GetPoint MolAtomAT
  
GetPoint (Point t)
gtrans : GetPoint a => AffineTransformation
  Totality: total
  Visibility: public export
point : {auto __con : GetPoint a} -> a -> Point gtrans
  Totality: total
  Visibility: public export
0 GPoint : (a : Type) -> GetPoint a => Type
  Totality: total
  Visibility: public export
0 GVect : (a : Type) -> GetPoint a => Type
  Totality: total
  Visibility: public export
interface ModPoint : Type -> Type
  Interface for modification of a value `a` by modifying its points in the
  affine space.

  Parameters: a
Methods:
  
mtrans : AffineTransformation
  
modPoint : (Point mtrans -> Point mtrans) -> a -> a

Implementations:
  
ModPoint (Vect 3 Coordinate)
  
ModPoint MolAtom
  
ModPoint MolAtomAT
  
ModPoint a => ModPoint (Graph b a)
  
ModPoint a => ModPoint (IGraph k b a)
  
ModPoint (Point t)
mtrans : ModPoint a => AffineTransformation
  Totality: total
  Visibility: public export
modPoint : {auto __con : ModPoint a} -> (Point mtrans -> Point mtrans) -> a -> a
  Totality: total
  Visibility: public export
0 MPoint : (a : Type) -> ModPoint a => Type
  Totality: total
  Visibility: public export
0 MVect : (a : Type) -> ModPoint a => Type
  Totality: total
  Visibility: public export
setPoint : {auto {conArg:5321} : ModPoint a} -> MPoint a -> a -> a
  Places an object at a new point in space.

  Totality: total
  Visibility: export
pointId : GetPoint a => a -> Point Id
  Return the coordinates of a point in the reference affine space.

  Totality: total
  Visibility: export
translate : {auto {conArg:5377} : ModPoint a} -> MVect a -> a -> a
  Translate an object in 2D space by the given vector.

  Totality: total
  Visibility: export
scale : ModPoint a => Scale -> a -> a
  Scale an object in 2D space by the given factor.

  Totality: total
  Visibility: export
rotateAt : {auto {conArg:5470} : ModPoint a} -> MPoint a -> Angle -> a -> a
  Rotates an object by the given angle around the given poin

  Totality: total
  Visibility: export
rotate : ModPoint a => Angle -> a -> a
  Rotates an object by the given angle around the origin

  Totality: total
  Visibility: export
distance : GetPoint a => a -> a -> Double
  Calculate the distance between two objects.

  Totality: total
  Visibility: export
distanceFromZero : GetPoint a => a -> Double
  Calculate the distance of an object from zero.

  Totality: total
  Visibility: export
near : GetPoint a => a -> a -> Double -> Bool
  Checks, if two objects are no further apart than `delta`.

  Totality: total
  Visibility: export
center2d : {auto {conArg:5759} : GetPoint a} -> Foldable t => t a -> GPoint a
  Computes the center of mass of a set of points.

  Totality: total
  Visibility: export
apply : Matrix -> Point t -> Point t
  Transform a point by applying a transformation patrix.

  Totality: total
  Visibility: export
perpendicularPoint : Point k -> Point k -> Double -> Bool -> Point k
  Calculates a perpendicual point to the line from the first line point
  with a certain distance. The `positive` flag is to choose the direction
  from the line (positive -> right top, negative -> left bottom).

  Totality: total
  Visibility: export
intersect : Point t -> Point t -> Point t -> Point t -> Maybe (Point t)
  Tries to compute the intersection of two lines
  from points p11 to p12 and p21 to p22.
  
  This tries to solve the following system of equations:
  
    (I)  : `x11 + r * (x12 - x11) = x21 + s * (x22 - x21)`
    (II) : `y11 + r * (y12 - y11) = y21 + s * (y22 - y21)`

  Totality: total
  Visibility: export
distanceToLine : Point t -> Point t -> Point t -> Maybe Double
  Computes the distance of a point `p` from a line defined
  by two of its points (`pl1` and `pl2`).

  Totality: total
  Visibility: export
alignBond : Point t -> Point t -> Point t -> Point t -> Point t -> Point t
  Given two reference points `pr1` and `pr2`, as well as
  two points `p1` and `p2`, returns a linear transformation
  which will superimpose `p1` with `pr1` and `p2` with `pr2`.
  
  The linear transformation consists of the following steps:
   1. translate `p1` to the origin
   2. scale by the factor `|pr2-pr1|/|p2-p1|`.
   3. rotate by `(angle (pr2-pr1) - angle(p2-p1))`
   4. translate to `pr1`.

  Totality: total
  Visibility: export
circularFreeSweep : (n : Nat) -> IsSucc n => Point t -> List (Point t) -> (Angle, Angle)
  For a given point `p` and a list of points surrounding
  `p`, computes the start and step angle to distribute
  `n` additional points in the largest free section around
  `p`.
  
  This utility can be used to find the ideal placement of
  a new bond to an atom with other surrounding atoms already
  placed.

  Totality: total
  Visibility: export
perpendicularTo : Point t -> Point t -> Point t -> Vector (transform t)
  For two given points, generates a vector perpendicular to the
  line connecting `x` and `y` and pointing towards a third given
  point `c`.
  
  This can be used to, for instance, place a double bond in the inner
  side of a ring, or construct the center of a ring fused to another.

  Totality: total
  Visibility: export
perpendicularFrom : Point t -> Point t -> Point t -> Vector (transform t)
  Like `perpendicularTo` but points away from the given center.

  Totality: total
  Visibility: export