MODULE Geometry;

(* Geometric predicates and functions. *)

IMPORT Math, R2;

PRED Equal(a, b) IS a = b END;

UI PointTool(Equal);

(* The points "a" and "b" are the same. *)

FUNC p = Mid(a, b) IS 
  p = R2.Times(0.5, R2.Plus(a, b)) 
END;

UI PointTool(Mid);

(* "p" is the midpoint of the segment 
   "(a, b)". *)

PRED Colinear(a, b, c) IS 
  (a, b) PARA (a, c) 
END;

UI PointTool(Colinear);

(* The points "a", "b", and "c" are 
   colinear. *)

FUNC p = HorVer(h, v) IS 
  (E hx, hy, vx, vy :: 
    h = (hx, hy) AND 
    v = (vx, vy) AND 
    p = (vx, hy)) 
END;

UI PointTool(HorVer);

(* "p" is the intersection point of the 
   horizontal line through "h" and the 
   vertical line through "v". *)

FUNC d2 = Dist2(p, q) IS 
  d2 = R2.Length2(R2.Minus(p, q)) 
END;

(* "d2" is the square of the distance 
   between the points "p" and "q". *)

FUNC d = Dist(p, q) IS 
  d = R2.Length(R2.Minus(p, q)) 
END;

(* "d" is the distance between the points 
   "p" and "q". *)

FUNC d2 = DistX2(p, q) IS 
  (E px, py, qx, qy, dx :: 
    p = (px, py) AND 
    q = (qx, qy) AND 
    dx = px - qx AND 
    d2 = dx * dx) 
END;

(* "d" is the square of the distance 
   between the projections of the points 
   "p" and "q" onto the X axis. *)

FUNC d = DistX(p, q) IS 
  d = Math.Sqrt(DistX2(p, q)) 
END;

(* "d" is the distance between the 
   projections of the points "p" and "q" 
   onto the X axis. *)

FUNC d2 = DistY2(p, q) IS 
  (E px, py, qx, qy, dy :: 
    p = (px, py) AND 
    q = (qx, qy) AND 
    dy = py - qy AND 
    d2 = dy * dy) 
END;

(* "d2" is the square of the distance 
   between the projections of the points 
   "p" and "q" onto the Y axis. *)

FUNC d = DistY(p, q) IS 
  d = Math.Sqrt(DistY2(p, q)) 
END;

(* "d" is the distance between the 
   projections of the points "p" and "q" 
   onto the Y axis. *)

FUNC len2 = SegLength2(s) IS 
  (E p, q :: 
    s = (p, q) AND len2 = Dist2(p, q)) 
END;

(* "len2" is the square of the length of 
   the segment "s", where "s" is a pair 
   of points "(p, q)". *)

FUNC len = SegLength(s) IS 
  (E p, q :: 
    s = (p, q) AND len = Dist(p, q)) 
END;

(* "len" is the length of the segment 
   "s", where "s" is a pair of points 
   "(p, q)". *)

PRED CongX(a, b, c, d) IS 
  (E ax, ay, bx, by, cx, cy, dx, dy, s1x, 
     s2x :: 
    a = (ax, ay) AND 
    b = (bx, by) AND 
    c = (cx, cy) AND 
    d = (dx, dy) AND 
    s1x = ax - bx AND 
    s2x = cx - dx AND 
    s1x * s1x = s2x * s2x) 
END;

UI PointTool(CongX);

(* The projections of the segments "ab" 
   and "cd" onto the X axis are 
   congruent. *)

PRED CongY(a, b, c, d) IS 
  (E ax, ay, bx, by, cx, cy, dx, dy, s1y, 
     s2y :: 
    a = (ax, ay) AND 
    b = (bx, by) AND 
    c = (cx, cy) AND 
    d = (dx, dy) AND 
    s1y = ay - by AND 
    s2y = cy - dy AND 
    s1y * s1y = s2y * s2y) 
END;

UI PointTool(CongY);

(* The projections of the segments "ab" 
   and "cd" onto the Y axis are 
   congruent. *)

PRED CongXY(a, b, c, d) IS 
  (E ax, ay, bx, by, cx, cy, dx, dy, s1x, 
     s2y :: 
    a = (ax, ay) AND 
    b = (bx, by) AND 
    c = (cx, cy) AND 
    d = (dx, dy) AND 
    s1x = ax - bx AND 
    s2y = cy - dy AND 
    s1x * s1x = s2y * s2y) 
END;

UI PointTool(CongXY);

(* The projection of the segment "ab" 
   onto the X axis is congruent to the 
   projection of the segment "cd" onto 
   the Y axis. *)

PRED VerSym(a, b, p) IS 
  (E x, ay, by, px, py :: 
    a = (x, ay) AND 
    b = (x, by) AND 
    p = (px, py) AND 
    by - py = py - ay) 
END;

UI PointTool(VerSym);

(* The points "a" and "b" are vertically 
   symmetric about the horizontal line 
   through the point "p". *)

PRED HorSym(a, b, p) IS 
  (E ax, bx, y, px, py :: 
    a = (ax, y) AND 
    b = (bx, y) AND 
    p = (px, py) AND 
    bx - px = px - ax) 
END;

UI PointTool(HorSym);

(* The points "a" and "b" are 
   horizontally symmetric about the 
   vertical line through the point "p". *)

PRED LineSym(a, b, p, q) IS 
  (a, p) CONG (p, b) AND 
  (a, q) CONG (q, b) 
END;

UI PointTool(LineSym);

(* The points "a" and "b" are symmetric 
   about the line through the points "p" 
   and "q". *)