euclidean.domain

-- ~~~~~~~~~~~~~~~~ TYPES ~~~~~~~~~~~~~~~~
type Shape
type Point <: Shape -- This type describes a point. Example usage: 
-- Point A, B, C
-- AutoLabel A, B, C
type Linelike <: Shape -- This type describes a plane. Example usage: 
-- Plane p
-- AutoLabel p
type Ray <: Linelike -- This type describes a ray. See construction of a ray below.
type Line <: Linelike -- This type describes a line. See construction of a line below.
type Segment <: Linelike -- This type describes a line segment. See construction of a line segment below.

type Angle <: Shape -- This type describes an angle. See construction of an angle below.

type Triangle <: Shape -- This type describes a triangle. See construction of a triangle below.
type Quadrilateral <: Shape -- This type describes a quadrilateral. See construction of a quadrilateral below.
type Rectangle <: Quadrilateral -- This type describes a rectangle. See construction of a rectangle below.
type Circle <: Shape -- This type describes a circle. See construction of a circle below.

type Plane <: Shape -- This type describes a plane. Example usage: 
-- Plane p
-- AutoLabel p

-- ~~~~~~~~~~~~~~~~ CONSTRUCTORS ~~~~~~~~~~~~~~~~
-- Lines and Points
constructor Segment(Point p, Point q) -- This constructor creates a line segment from two points. Example usage: 
-- Point A, B
-- Segment AB := Segment(A, B)
-- AutoLabel A, B
constructor Ray(Point base, Point direction) -- This constructor creates a ray from two points, a base and a direction point. Example usage: 
-- Point A, B
-- Ray rayAB := Ray(A, B)
-- AutoLabel A, B
constructor Line(Point p, Point q) -- This constructor creates a line from two points. Example usage: 
-- Point A, B
-- Line lineAB := Line(A, B)
-- AutoLabel A, B
constructor Midpoint(Linelike l) -> Point -- This constructor creates a point as the midpoint of a line. Example usage: 
-- Point A, B
-- Segment segmentAB
-- segmentAB := Segment(A, B)
-- Point midpointAB := Midpoint(AB)
-- AutoLabel A, B, midpointAB

-- Angles
constructor InteriorAngle(Point p, Point q, Point r) -> Angle -- This constructor creates an angle from three points. Example usage: 
-- Point A, B, C
-- Angle angleABC := InteriorAngle(A, B, C)
-- AutoLabel A, B, C

-- Polygons/Shapes
constructor Triangle(Point p, Point q, Point r) -- This constructor creates a triangle from three points. Example usage: 
-- Point A, B, C
-- Triangle triangleABC := Triangle(A, B, C)
-- AutoLabel A, B, C
constructor Rectangle(Point p, Point q, Point r, Point s) -- This constructor creates a rectangle from four points. Example usage: 
-- Point A, B, C, D
-- Rectangle rectangleABCD := Rectangle(A, B, C, D)
-- AutoLabel A, B, C, D
constructor Quadrilateral(Point p, Point q, Point r, Point s) -- This function creates a quadrilateral from four points. Example usage: 
-- Point A, B, C, D
-- Quadrilateral quadrilateralABCD := Quadrilateral(A, B, C, D)
-- AutoLabel A, B, C, D
constructor CircleR(Point center, Point radius) -> Circle -- This constructor creates a circle from a center point and a radius point. Example usage: 
-- Point A, B
-- Circle circleAB := CircleR(A, B)
-- AutoLabel A, B

-- ~~~~~~~~~~~~~~~~ FUNCTIONS ~~~~~~~~~~~~~~~~
-- Lines and Points
function Bisector(Angle) -> Ray -- This function creates a ray as the angle bisector of an angle. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- Ray bisectorABC := Bisector(angleABC)
-- AutoLabel A, B, C, bisectorABC
function PerpendicularBisector(Segment, Point) -> Segment -- This function creates a perpendicular bisector from a line segment. Example usage: 
-- Point A, B, C
-- Segment AB
-- AB := Segment(A, B)
-- Segment perpendicularBisectorAB := PerpendicularBisector(AB, C)
-- AutoLabel A, B, C
function PerpendicularBisectorLabelPts(Segment, Point, Point) -> Segment -- This function creates a perpendicular bisector from a segment to bisect, a base point, and a direction point. Example usage: 
-- Point A, B, C, D, d
-- Segment AB, CD
-- AB := Segment(A, B)
-- CD := Segment(C, D)
-- PerpendicularBisectorLabelPts(AB, C, d)
-- AutoLabel A, B, C, D, d

-- Polygons/Shapes
function MidSegment(Triangle, Point, Point) -> Segment -- This function creates a midsegment from a triangle and two points on the triangle. Example usage: 
-- Point A, B, C, D, E
-- Triangle triangleABC := Triangle(A, B, C)
-- Segment midsegmentDE := MidSegment(triangleABC, D, E)
-- AutoLabel A, B, C, D, E
function Radius(Circle c, Point p) -> Segment -- This function creates a radius from a circle and a point on the circle. Example usage: 
-- Point A, B
-- Circle circleAB
-- circleAB := CircleR(A, B)
-- Segment radiusAB := Radius(circleAB, B)
-- AutoLabel A, B
function Chord(Circle c, Point p, Point q) -> Segment -- This function creates a chord from a circle and two points on the circle. Example usage: 
-- Point A, B, C
-- Circle circleAB
-- circleAB := CircleR(A, B)
-- Segment chordAC := Chord(circleAB, A, C)
-- AutoLabel A, B, C
function Diameter(Circle c, Point p, Point q) -> Segment -- This function creates a diameter from a circle and two points. Example usage: 
-- Point A, B
-- Circle circleAB
-- 
-- Segment diameterAC := Diameter(circleAB, A, B)
-- AutoLabel A, B

-- Unimplemented
-- function Sum(Angle, Angle) -> Angle
-- function Intersection(Linelike, Linelike) -> Point
-- function Altitude(Triangle, Angle) -> Segment
-- function Endpoint(Segment) -> Point

-- ~~~~~~~~~~~~~~~~ PREDICATES ~~~~~~~~~~~~~~~~
-- Lines and Points
predicate On(Point, Linelike) -- This predicate makes a point be on a line. Example usage: 
-- Point A, B
-- Line lineAB
-- lineAB := Line(A, B)
-- On(A, lineAB)
-- AutoLabel A, B
predicate In(Point, Plane) -- This predicate makes a point be in a plane. Example usage: 
-- Point A, B
-- Plane planeAB
-- planeAB := Plane(A, B)
-- In(A, planeAB)
-- AutoLabel A, B
predicate Midpoint(Linelike, Point) -- This predicate makes a point be the midpoint of a line. Example usage: 
-- Point A, B, C
-- Segment segmentAB
-- segmentAB := Segment(A, B)
-- Midpoint(segmentAB, C)
-- AutoLabel A, B, C
predicate Collinear(Point, Point, Point) -- This predicate makes three points collinear. Example usage: 
-- Point A, B, C
-- Segment AB, BC
-- AB := Segment(A, B)
-- BC := Segment(B, C)
-- Collinear(A, B, C)
predicate ParallelMarker1(Linelike, Linelike) -- This predicate marks two lines parallel. Only use if Parallel precedes it. Example usage: 
-- Point A, B, C, D
-- Line lineAB, lineCD
-- lineAB := Line(A, B)
-- lineCD := Line(C, D)
-- Parallel(lineAB, lineCD)
-- ParallelMarker1(lineAB, lineCD)
-- AutoLabel A, B, C, D
predicate EqualLengthMarker(Linelike, Linelike) -- This predicate only marks two segments with a tick indicating that they have equal length. Only use if EqualLength precedes it. Example usage: 
-- Point A, B, C, D
-- Segment segmentAB, segmentCD
-- segmentAB := Segment(A, B)
-- segmentCD := Segment(C, D)
-- EqualLength(segmentAB, segmentCD)
-- EqualLengthMarker(segmentAB, segmentCD)
-- AutoLabel A, B, C, D
predicate EqualLength(Linelike, Linelike) -- This predicate makes two segments have equal length. Example usage: 
-- Point A, B, C, D
-- Segment segmentAB, segmentCD
-- segmentAB := Segment(A, B)
-- segmentCD := Segment(C, D)
-- EqualLength(segmentAB, segmentCD)
-- AutoLabel A, B, C, D
predicate Parallel(Linelike, Linelike) -- This predicate makes two lines parallel. Example usage: 
-- Point A, B, C, D
-- Line lineAB, lineCD
-- lineAB := Line(A, B)
-- lineCD := Line(C, D)
-- Parallel(lineAB, lineCD)
-- AutoLabel A, B, C, D

-- Angles
predicate Acute(Angle) -- This predicate makes an angle acute. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- Acute(angleABC)
-- AutoLabel A, B, C
predicate Obtuse(Angle) -- This predicate makes an angle obtuse. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- Obtuse(angleABC)
-- AutoLabel A, B, C
predicate RightMarked(Angle) -- This predicate makes an angle right and marks it with a square. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- RightMarked(angleABC)
-- AutoLabel A, B, C
predicate RightUnmarked(Angle) -- This predicate makes an angle right and does not mark it with a square. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- RightUnmarked(angleABC)
-- AutoLabel A, B, C
predicate AngleBisector(Angle, Linelike) -- This predicate makes a ray be the angle bisector of an angle. Example usage: 
-- Point A, B, C
-- Angle angleABC
-- angleABC := InteriorAngle(A, B, C)
-- Ray rayABC
-- rayABC := Ray(A, B)
-- AngleBisector(angleABC, rayABC)
-- AutoLabel A, B, C
predicate EqualAngleMarker(Angle, Angle) -- This predicate only marks two angles with a tick indicating that they have equal measure. Only use if EqualAngle precedes it. Example usage: 
-- Point A, B, C, D, E, F
-- Angle angleABC, angleDEF
-- angleABC := InteriorAngle(A, B, C)
-- angleDEF := InteriorAngle(D, E, F)
-- EqualAngle(angleABC, angleDEF)
-- EqualAngleMarker(angleABC, angleDEF)
-- AutoLabel A, B, C, D, E, F
predicate EqualAngle(Angle, Angle) -- This predicate makes two angles have equal measure. Example usage: 
-- Point A, B, C, D, E, F
-- Angle angleABC, angleDEF
-- angleABC := InteriorAngle(A, B, C)
-- angleDEF := InteriorAngle(D, E, F)
-- EqualAngle(angleABC, angleDEF)
-- AutoLabel A, B, C, D, E, F

-- Polygons/Shapes
predicate Parallelogram(Quadrilateral) -- This predicate makes a quadrilateral a parallelogram. Example usage: 
-- Point A, B, C, D
-- Quadrilateral quadrilateralABCD
-- quadrilateralABCD := Quadrilateral(A, B, C, D)
-- Parallelogram(quadrilateralABCD)
-- AutoLabel A, B, C, D
predicate OnCircle(Circle, Point) -- This predicate makes a point be on a circle. Example usage: 
-- Point A, B, C
-- Circle circleAB
-- circleAB := CircleR(A, B)
-- OnCircle(circleAB, C)
-- AutoLabel A, B, C
predicate CircleCenter(Circle, Point) -- Do not use.
predicate Incenter(Point, Triangle) -- This predicate makes a point be the incenter of a triangle. Example usage: 
-- Point A, B, C, D
-- Triangle triangleABC
-- triangleABC := Triangle(A, B, C)
-- Incenter(D, triangleABC)
-- AutoLabel A, B, C, D
predicate Orthocenter(Point, Triangle) -- This predicate makes a point be the orthocenter of a triangle. Example usage: 
-- Point A, B, C, D
-- Triangle triangleABC
-- triangleABC := Triangle(A, B, C)
-- Orthocenter(D, triangleABC)
-- AutoLabel A, B, C, D
predicate Centroid(Point, Triangle) -- This predicate makes a point be the centroid of a triangle. Example usage: 
-- Point A, B, C, D
-- Triangle triangleABC
-- triangleABC := Triangle(A, B, C)
-- Centroid(D, triangleABC)
-- AutoLabel A, B, C, D
predicate Circumcenter(Point, Triangle) -- This predicate makes a point be the circumcenter of a triangle. Example usage: 
-- Point A, B, C, D
-- Triangle triangleABC
-- triangleABC := Triangle(A, B, C)
-- Circumcenter(D, triangleABC)
-- AutoLabel A, B, C, D