MODULE Rel;

(* Functions for specifying 
   coordinates relative to some 
   other coordinate system. *)

IMPORT R2;

FUNC q = C1(p, a) IS 
  q = R2.Plus(p, a) 
END;

UI PointTool(C1);

(* "q" is "a" shifted by "p". *)

FUNC q = C2(p, a, b) IS 
  q = p REL (a, b) 
END;

UI PointTool(C2);

(* For completeness, "q" is "p REL 
   (a, b)", namely "q" is the point 
   "p" in the coordinate system in 
   which "a" is the origin and "b" 
   is the tip of the unit x-vector. 
*)

FUNC q = C3(p, a, b, c) IS 
  (E xVec, yVec, px, py :: 
    p = (px, py) AND 
    xVec = 
      R2.Times(px, R2.Minus(b, a)) AND 
    yVec = 
      R2.Times(py, R2.Minus(c, a)) AND 
    q = 
      R2.Plus(a, R2.Plus(xVec, yVec))) 
END;

UI PointTool(C3);

(* "q" is the point "p" in the 
   skewed coordinate system in 
   which "a" is the origin, "b" is 
   the tip of the unit x-vector, 
   and "c" is the tip of the unit 
   y-vector. *)

FUNC q = Inv(p, a, b) IS 
  (E ab, ac, ap, abLen, abLen2,
     qx, qy :: 
    ab = R2.Minus(b, a) AND 
    ac = (-CDR(ab), CAR(ab)) AND 
    ap = R2.Minus(p, a) AND 
    abLen = R2.Length(ab) AND 
    abLen2 = abLen * abLen AND 
    q = (qx, qy) AND 
    qx = R2.Dot(ap, ab) / abLen2 AND 
    qy = R2.Dot(ap, ac) / abLen2) 
END;

UI PointTool(Inv);

(* This function is equivalent to 
   "p = q REL (a, b)", but it can 
   be used functionally to 
   establish useful hints if "p", 
   "a", and "b" are already hinted. 
*)

FUNC x = InvX(p, a, b) IS 
  (E ab, ap, abLen2 :: 
    ab = R2.Minus(b, a) AND 
    ap = R2.Minus(p, a) AND 
    abLen2 = R2.Length2(ab) AND 
    x = R2.Dot(ap, ab) / abLen2) 
END;

(* This function is equivalent to 
   "(E y :: p = (x, y) REL (a, b))".
   It can be used functionally to 
   establish useful hints if "p", 
   "a", and "b" are already hinted. 
*)

FUNC y = InvY(p, a, b) IS 
  (E abx, aby, ac, ap, acLen2 :: 
    (abx, aby) = R2.Minus(b, a) AND 
    ac = (-aby, abx) AND 
    ap = R2.Minus(p, a) AND 
    acLen2 = R2.Length2(ac) AND 
    y = R2.Dot(ap, ac) / acLen2) 
END;

(* This function is equivalent to 
   "(E x :: p = (x, y) REL (a, b))".
   It can be used functionally to 
   establish useful hints if "p", 
   "a", and "b" are already hinted. 
*)

PRED X(p, a, b, x) IS 
  (E y = InvY(p, a, b) :: 
    p = (x, y) REL (a, b)) 
END;

UI PointTool(X);

(* This constraint is equivalent to
   "(E y :: p = (x, y) REL (a, b))",
   except that it picks a smart hint
   for "y". *)

PRED Y(p, a, b, y) IS 
  (E x = InvX(p, a, b) :: 
    p = (x, y) REL (a, b)) 
END;

UI PointTool(Y);

(* This constraint is equivalent to
   "(E x :: p = (x, y) REL (a, b))",
   except that it picks a smart hint
   for "x". *)