(* Copyright (C) 1992, Digital Equipment Corporation                 *)
(* All rights reserved.                                              *)
(* See the file COPYRIGHT for a full description.                    *)
(*                                                                   *)
(* Last modified on Mon Oct 31 09:05:57 PST 1994 by heydon           *)

(* Definitions for CLOSE and APPLY so they will have slot
   numbers in the top-level scope. *)

PROC res := CLOSE() IS SKIP END;

PROC APPLY() IS SKIP END;

(* Definitions for the built-in predicates and functions. 
   To avoid name conflicts, these names all begin with "_". *)

PRED _HOR(a, b) IS 
  (E x1, x2, y :: 
    REAL(x1) AND 
    REAL(x2) AND 
    REAL(y) AND 
    a = (x1, y) AND 
    b = (x2, y)) 
END;

PRED _VER(a, b) IS 
  (E x, y1, y2 :: 
    REAL(y1) AND 
    REAL(y2) AND 
    REAL(x) AND 
    a = (x, y1) AND 
    b = (x, y2)) 
END;

FUNC y = _UMINUS(x) IS 0 = x + y END;

FUNC z = _MINUS(x, y) IS x = y + z END;

FUNC z = _DIVIDE(x, y) IS x = y * z END;

FUNC y = _CAR(x) IS (E z :: x = (y, z)) END;

FUNC y = _CDR(x) IS (E z :: x = (z, y)) END;

PRIVATE FUNC len = _SegLenSq(s) IS
  (E a, b, ax, ay, bx, by, dx, dy ::
    s = (a, b) AND
    a = (ax, ay) AND
    b = (bx, by) AND
    dx = bx - ax AND
    dy = by - ay AND
    len = dx * dx + dy * dy)
END;

PRED _CONG(a, b) IS
  _SegLenSq(a) = _SegLenSq(b)
END;

PRIVATE FUNC v = _Delta(ab) IS
  (E a, b, ax, ay, bx, by, vx, vy ::
    ab = (a, b) AND
    a = (ax, ay) AND
    b = (bx, by) AND
    v = (vx, vy) AND
    bx = vx + ax AND
    by = vy + ay)
END;

PRIVATE PRED _ParaVects(v1, v2) IS
  (E v1x, v1y, v2x, v2y ::
    v1 = (v1x, v1y) AND
    v2 = (v2x, v2y) AND
    v1x * v2y = v1y * v2x)
END;

PRED _PARA(a, b) IS 
  (E ad, bd ::
    ad = _Delta(a) AND
    bd = _Delta(b) AND
    _ParaVects(ad, bd))
END;

FUNC q = _REL(p, ab) IS 
  (E px, py, qx, qy,
     a, b, ax, ay, bx, by, dx, dy,
     xx, yy, xy, yx, dx2, dy2 :: 
    ab = (a, b) AND 
    a = (ax, ay) AND 
    b = (bx, by) AND 
    p = (px, py) AND 
    q = (qx, qy) AND 
    bx = dx + ax AND 
    by = dy + ay AND 
    xx = px * dx AND 
    yy = py * dy AND 
    xy = px * dy AND 
    yx = py * dx AND 
    xx = dx2 + yy AND 
    dy2 = xy + yx AND 
    qx = ax + dx2 AND 
    qy = ay + dy2) 
END;