Idris2Doc : Geom.Angle

Geom.Angle

(source)
Definitions
Epsilon : Double
  Totality: total
  Visibility: public export
TwoPi : Double
  Totality: total
  Visibility: export
normalize : Double -> Double
  Convert a floating point number to an angle
  in the interval [0, 2 * pi).

  Totality: total
  Visibility: export
record Angle : Type
  A normalized angle in the range [0,2 * pi).

  Totality: total
  Visibility: public export
  Constructor: 
A : (value : Double) -> (0 org : Double) -> {auto 0 _ : value = normalize org} -> Angle

  Projections:
  
0 .org : Angle -> Double
  The original floating point number from which the angle
  was created.
  
0 .prf : ({rec:0} : Angle) -> value {rec:0} = normalize (org {rec:0})
  Proof that we did not forget the normalization step.
  
.value : Angle -> Double
  The normalized value

  Hints:
  
Eq Angle
  
Ord Angle
  
Show Angle
.value : Angle -> Double
  The normalized value

  Totality: total
  Visibility: public export
value : Angle -> Double
  The normalized value

  Totality: total
  Visibility: public export
0 .org : Angle -> Double
  The original floating point number from which the angle
  was created.

  Totality: total
  Visibility: public export
0 org : Angle -> Double
  The original floating point number from which the angle
  was created.

  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Angle) -> value {rec:0} = normalize (org {rec:0})
  Proof that we did not forget the normalization step.

  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Angle) -> value {rec:0} = normalize (org {rec:0})
  Proof that we did not forget the normalization step.

  Totality: total
  Visibility: public export
angle : Double -> Angle
  Convenience constructor for angles.
  
  It is safe to invoke `A` directly, but one has to deal
  with the proofing stuff.

  Totality: total
  Visibility: export
halfPi : Angle
  Totality: total
  Visibility: export
twoThirdPi : Angle
  Totality: total
  Visibility: export
threeHalfPi : Angle
  Totality: total
  Visibility: export
pi : Angle
  Totality: total
  Visibility: export
zero : Angle
  Totality: total
  Visibility: export
fullSteps : Nat -> Angle
  Totality: total
  Visibility: export
delta : Angle -> Angle -> Angle
  Returns the absolute distance between two angles
  
  Unlike `minDelta`, this just subtracts the smaller angle
  from the larger one. Therefore, `delta zero halfPi = halfPi`
  and `delta zero threeHalfPi = threeHalfPi`.

  Totality: total
  Visibility: export
(+) : Angle -> Angle -> Angle
  Addition of two angles

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 8
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
(-) : Angle -> Angle -> Angle
  Difference between two angles

  Totality: total
  Visibility: export
  Fixity Declarations:
  infixl operator, level 8
prefix operator, level 10
negate : Angle -> Angle
  The inverse of an angle so that `x + negate x == 0`
  (modulo rounding errors).

  Totality: total
  Visibility: export
  Fixity Declaration: prefix operator, level 10
(*) : Double -> Angle -> Angle
  Multiplication of an angle with a constant factor

  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 9
divide : Nat -> Angle -> Angle
  Divides an angle into `n` equal part.
  
  Returns the angle unmodified in case `n` equals zero.

  Totality: total
  Visibility: export
minDelta : Angle -> Angle -> Angle
  Returns the shortest distance between two angles.
  (either clockwise or counterclockwise.)
  
  Unlike `delta`, this computes the *smaller* angle
  between the two input values.
  Therefore, `minDelta zero halfPi = minDelta zero threeHalfPi = halfPi`.

  Totality: total
  Visibility: export
toDegree : Angle -> Double
  Convert and angle to centigrees

  Totality: total
  Visibility: export
fromDegree : Double -> Angle
  Convert an angle in centigrees to one in radians

  Totality: total
  Visibility: export
bisector : Angle -> Angle -> Angle
  Angle bisector counterclockwise

  Totality: total
  Visibility: export
closestAngle : Angle -> List Angle -> Maybe Angle
  From a list of angles, returns the one closest to the given angle

  Totality: total
  Visibility: export
enclosingAngles : Angle -> List Angle -> Maybe (Angle, Angle)
  Given an angle `phi` plus a list of angles, returns from the
  list two angles `a` and `b`, so that `phi` lies between `a` and `b`
  with no other angle closer to `phi`.
  
  Note: In case of this being successful, `phi` will always lie counter
        clockwise of the first returned angle and the second returned
        angle will lie counter-clockwise of `phi`.

  Totality: total
  Visibility: export
largestBisector : List Angle -> Angle
  Totality: total
  Visibility: export
record Arc : Type
  An arc of `segs` segments connecting two existing nodes.
  
  Used for creating rings and bridges when placing molecules.

  Totality: total
  Visibility: public export
  Constructor: 
MkArc : Angle -> Angle -> Double -> Double -> Arc

  Projections:
  
.angle : Arc -> Angle
  Total angle of the arc
  
.distance : Arc -> Double
  Distance between the center of the arc and the middle
  of a segment.
  
.radius : Arc -> Double
  Radius of the arc
  
.step : Arc -> Angle
  Angle of a single segment of the arc

  Hints:
  
Eq Arc
  
Show Arc
.angle : Arc -> Angle
  Total angle of the arc

  Totality: total
  Visibility: public export
angle : Arc -> Angle
  Total angle of the arc

  Totality: total
  Visibility: public export
.step : Arc -> Angle
  Angle of a single segment of the arc

  Totality: total
  Visibility: public export
step : Arc -> Angle
  Angle of a single segment of the arc

  Totality: total
  Visibility: public export
.radius : Arc -> Double
  Radius of the arc

  Totality: total
  Visibility: public export
radius : Arc -> Double
  Radius of the arc

  Totality: total
  Visibility: public export
.distance : Arc -> Double
  Distance between the center of the arc and the middle
  of a segment.

  Totality: total
  Visibility: public export
distance : Arc -> Double
  Distance between the center of the arc and the middle
  of a segment.

  Totality: total
  Visibility: public export
ngonAngle : (n : Nat) -> {auto 0 _ : LTE 3 n} -> Angle
  Angle at the corner of a regular n-gon

  Totality: total
  Visibility: export
ngonRadius : Double -> (n : Nat) -> {auto 0 _ : LTE 3 n} -> Double
  Radius of a regular n-gon with side length `side`.
  
  This is the distance from the center of the n-gon to one of its
  corners.

  Totality: total
  Visibility: export
ngonDistance : Double -> (n : Nat) -> {auto 0 _ : LTE 3 n} -> Double
  Distance from the center of a regular n-gon with side length `side`
  to the middle of one of its sides.

  Totality: total
  Visibility: export
ngon : Double -> (n : Nat) -> {auto 0 _ : LTE 3 n} -> Arc
  Totality: total
  Visibility: export
arc : (n : Nat) -> {auto 0 _ : IsSucc n} -> Double -> Double -> Arc
  Computes the dimensions of an arc that connects two
  existing nodes (with a distance of `d` between the nodes)
  by inserting `n` additional nodes between them.
  
  The arc is optimized in such a way that the distance between two
  adjacent nodes is as close to `len` as possible.
  
  Note: If `len` is too short, that is `(n+1) * len < d`, this returns
        close to - but not exactly - a straight line. Client code is
        responsible to choose `len` in such a manner, that an arc
        with a reasonable minimal curvature is constructed,
        for instance by setting the minimal `len`
        at `(1+delta)*d / (n+1)` with `delta > 0`.

  Totality: total
  Visibility: export