MODULE Angle;

IMPORT Math, R2, Geometry, Rel;

(* Functions and predicates on 
   angles. Unless stated otherwise, 
   all angles are in radians. *)

CONST Degree = Math.Pi / 180;

(* "Degree" is the value of one 
   degree in radians. *)

PRED Right(a, b, c) IS 
  R2.Dot(R2.Minus(a, b), 
         R2.Minus(c, b)) = 0 
END;

UI PointTool(Right);

(* The angle "abc" is right. True if 
   "a = b" or "b = c". *)

FUNC theta = Acute(a, b, c) IS 
  (E v1, v2, l1, l2 :: 
    v1 = R2.Minus(a, b) AND 
    v2 = R2.Minus(c, b) AND 
    l1 = R2.Length(v1) AND 
    l2 = R2.Length(v2) AND 
    theta ~ 1.5 AND 
    COS(theta) * l1 * l2 = 
      R2.Dot(v1, v2)) 
END;

(* Return the angle "abc" as an acute 
   angle in the closed interval "[0, 
   Pi]". Requires "a # b" and "b # 
   c". *)

FUNC theta = CC(a, b, c) IS 
  (E p = Rel.Inv(c, b, a) :: 
    theta = ATAN(CDR(p), CAR(p))) 
END;

(* Return the angle in the half-open 
   interval "(-Pi, Pi]" that the ray 
   "ba" forms with the ray "bc", 
   measured counter-clockwise from 
   "ba". Requires "a # b" and "b # 
   c". *)

PRED OnBisector(p, a, b, c) IS 
  (E d ~ c :: 
    (d, b) CONG (b, a) AND 
    (d, p) CONG (p, a) AND 
    Geometry.Colinear(b, d, c)) 
END;

UI PointTool(OnBisector);

(* The point "p" is on the line 
   bisecting the acute angle "abc". *)

PRED Cong(a, b, c, d, e, f) IS 
  (E g ~ d, h ~ f :: 
    Geometry.Colinear(e, d, g) AND 
    Geometry.Colinear(e, f, h) AND 
    (a, b) CONG (g, e) AND 
    (h, e) CONG (c, b) AND 
    (c, a) CONG (g, h)) 
END;

UI PointTool(Cong);

(* The angle "abc" is congruent to 
   the angle "def". *)