|
| 1 | +-- ~~~~~~~~~~~~~~~~ TYPES ~~~~~~~~~~~~~~~~ |
| 2 | +type Shape |
| 3 | +type Point <: Shape -- This type describes a point. Example usage: |
| 4 | +-- Point A, B, C |
| 5 | +-- AutoLabel A, B, C |
| 6 | +type Linelike <: Shape -- This type describes a plane. Example usage: |
| 7 | +-- Plane p |
| 8 | +-- AutoLabel p |
| 9 | +type Ray <: Linelike -- This type describes a ray. See construction of a ray below. |
| 10 | +type Line <: Linelike -- This type describes a line. See construction of a line below. |
| 11 | +type Segment <: Linelike -- This type describes a line segment. See construction of a line segment below. |
| 12 | + |
| 13 | +type Angle <: Shape -- This type describes an angle. See construction of an angle below. |
| 14 | + |
| 15 | +type Triangle <: Shape -- This type describes a triangle. See construction of a triangle below. |
| 16 | +type Quadrilateral <: Shape -- This type describes a quadrilateral. See construction of a quadrilateral below. |
| 17 | +type Rectangle <: Quadrilateral -- This type describes a rectangle. See construction of a rectangle below. |
| 18 | +type Circle <: Shape -- This type describes a circle. See construction of a circle below. |
| 19 | + |
| 20 | +type Plane <: Shape -- This type describes a plane. Example usage: |
| 21 | +-- Plane p |
| 22 | +-- AutoLabel p |
| 23 | + |
| 24 | +-- ~~~~~~~~~~~~~~~~ CONSTRUCTORS ~~~~~~~~~~~~~~~~ |
| 25 | +-- Lines and Points |
| 26 | +constructor Segment(Point p, Point q) -- This constructor creates a line segment from two points. Example usage: |
| 27 | +-- Point A, B |
| 28 | +-- Segment AB := Segment(A, B) |
| 29 | +-- AutoLabel A, B |
| 30 | +constructor Ray(Point base, Point direction) -- This constructor creates a ray from two points, a base and a direction point. Example usage: |
| 31 | +-- Point A, B |
| 32 | +-- Ray rayAB := Ray(A, B) |
| 33 | +-- AutoLabel A, B |
| 34 | +constructor Line(Point p, Point q) -- This constructor creates a line from two points. Example usage: |
| 35 | +-- Point A, B |
| 36 | +-- Line lineAB := Line(A, B) |
| 37 | +-- AutoLabel A, B |
| 38 | +constructor Midpoint(Linelike l) -> Point -- This constructor creates a point as the midpoint of a line. Example usage: |
| 39 | +-- Point A, B |
| 40 | +-- Segment segmentAB |
| 41 | +-- segmentAB := Segment(A, B) |
| 42 | +-- Point midpointAB := Midpoint(AB) |
| 43 | +-- AutoLabel A, B, midpointAB |
| 44 | + |
| 45 | +-- Angles |
| 46 | +constructor InteriorAngle(Point p, Point q, Point r) -> Angle -- This constructor creates an angle from three points. Example usage: |
| 47 | +-- Point A, B, C |
| 48 | +-- Angle angleABC := InteriorAngle(A, B, C) |
| 49 | +-- AutoLabel A, B, C |
| 50 | + |
| 51 | +-- Polygons/Shapes |
| 52 | +constructor Triangle(Point p, Point q, Point r) -- This constructor creates a triangle from three points. Example usage: |
| 53 | +-- Point A, B, C |
| 54 | +-- Triangle triangleABC := Triangle(A, B, C) |
| 55 | +-- AutoLabel A, B, C |
| 56 | +constructor Rectangle(Point p, Point q, Point r, Point s) -- This constructor creates a rectangle from four points. Example usage: |
| 57 | +-- Point A, B, C, D |
| 58 | +-- Rectangle rectangleABCD := Rectangle(A, B, C, D) |
| 59 | +-- AutoLabel A, B, C, D |
| 60 | +constructor Quadrilateral(Point p, Point q, Point r, Point s) -- This function creates a quadrilateral from four points. Example usage: |
| 61 | +-- Point A, B, C, D |
| 62 | +-- Quadrilateral quadrilateralABCD := Quadrilateral(A, B, C, D) |
| 63 | +-- AutoLabel A, B, C, D |
| 64 | +constructor CircleR(Point center, Point radius) -> Circle -- This constructor creates a circle from a center point and a radius point. Example usage: |
| 65 | +-- Point A, B |
| 66 | +-- Circle circleAB := CircleR(A, B) |
| 67 | +-- AutoLabel A, B |
| 68 | + |
| 69 | +-- ~~~~~~~~~~~~~~~~ FUNCTIONS ~~~~~~~~~~~~~~~~ |
| 70 | +-- Lines and Points |
| 71 | +function Bisector(Angle) -> Ray -- This function creates a ray as the angle bisector of an angle. Example usage: |
| 72 | +-- Point A, B, C |
| 73 | +-- Angle angleABC |
| 74 | +-- angleABC := InteriorAngle(A, B, C) |
| 75 | +-- Ray bisectorABC := Bisector(angleABC) |
| 76 | +-- AutoLabel A, B, C, bisectorABC |
| 77 | +function PerpendicularBisector(Segment, Point) -> Segment -- This function creates a perpendicular bisector from a line segment. Example usage: |
| 78 | +-- Point A, B, C |
| 79 | +-- Segment AB |
| 80 | +-- AB := Segment(A, B) |
| 81 | +-- Segment perpendicularBisectorAB := PerpendicularBisector(AB, C) |
| 82 | +-- AutoLabel A, B, C |
| 83 | +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: |
| 84 | +-- Point A, B, C, D, d |
| 85 | +-- Segment AB, CD |
| 86 | +-- AB := Segment(A, B) |
| 87 | +-- CD := Segment(C, D) |
| 88 | +-- PerpendicularBisectorLabelPts(AB, C, d) |
| 89 | +-- AutoLabel A, B, C, D, d |
| 90 | + |
| 91 | +-- Polygons/Shapes |
| 92 | +function MidSegment(Triangle, Point, Point) -> Segment -- This function creates a midsegment from a triangle and two points on the triangle. Example usage: |
| 93 | +-- Point A, B, C, D, E |
| 94 | +-- Triangle triangleABC := Triangle(A, B, C) |
| 95 | +-- Segment midsegmentDE := MidSegment(triangleABC, D, E) |
| 96 | +-- AutoLabel A, B, C, D, E |
| 97 | +function Radius(Circle c, Point p) -> Segment -- This function creates a radius from a circle and a point on the circle. Example usage: |
| 98 | +-- Point A, B |
| 99 | +-- Circle circleAB |
| 100 | +-- circleAB := CircleR(A, B) |
| 101 | +-- Segment radiusAB := Radius(circleAB, B) |
| 102 | +-- AutoLabel A, B |
| 103 | +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: |
| 104 | +-- Point A, B, C |
| 105 | +-- Circle circleAB |
| 106 | +-- circleAB := CircleR(A, B) |
| 107 | +-- Segment chordAC := Chord(circleAB, A, C) |
| 108 | +-- AutoLabel A, B, C |
| 109 | +function Diameter(Circle c, Point p, Point q) -> Segment -- This function creates a diameter from a circle and two points. Example usage: |
| 110 | +-- Point A, B |
| 111 | +-- Circle circleAB |
| 112 | +-- |
| 113 | +-- Segment diameterAC := Diameter(circleAB, A, B) |
| 114 | +-- AutoLabel A, B |
| 115 | + |
| 116 | +-- Unimplemented |
| 117 | +-- function Sum(Angle, Angle) -> Angle |
| 118 | +-- function Intersection(Linelike, Linelike) -> Point |
| 119 | +-- function Altitude(Triangle, Angle) -> Segment |
| 120 | +-- function Endpoint(Segment) -> Point |
| 121 | + |
| 122 | +-- ~~~~~~~~~~~~~~~~ PREDICATES ~~~~~~~~~~~~~~~~ |
| 123 | +-- Lines and Points |
| 124 | +predicate On(Point, Linelike) -- This predicate makes a point be on a line. Example usage: |
| 125 | +-- Point A, B |
| 126 | +-- Line lineAB |
| 127 | +-- lineAB := Line(A, B) |
| 128 | +-- On(A, lineAB) |
| 129 | +-- AutoLabel A, B |
| 130 | +predicate In(Point, Plane) -- This predicate makes a point be in a plane. Example usage: |
| 131 | +-- Point A, B |
| 132 | +-- Plane planeAB |
| 133 | +-- planeAB := Plane(A, B) |
| 134 | +-- In(A, planeAB) |
| 135 | +-- AutoLabel A, B |
| 136 | +predicate Midpoint(Linelike, Point) -- This predicate makes a point be the midpoint of a line. Example usage: |
| 137 | +-- Point A, B, C |
| 138 | +-- Segment segmentAB |
| 139 | +-- segmentAB := Segment(A, B) |
| 140 | +-- Midpoint(segmentAB, C) |
| 141 | +-- AutoLabel A, B, C |
| 142 | +predicate Collinear(Point, Point, Point) -- This predicate makes three points collinear. Example usage: |
| 143 | +-- Point A, B, C |
| 144 | +-- Segment AB, BC |
| 145 | +-- AB := Segment(A, B) |
| 146 | +-- BC := Segment(B, C) |
| 147 | +-- Collinear(A, B, C) |
| 148 | +predicate ParallelMarker1(Linelike, Linelike) -- This predicate marks two lines parallel. Only use if Parallel precedes it. Example usage: |
| 149 | +-- Point A, B, C, D |
| 150 | +-- Line lineAB, lineCD |
| 151 | +-- lineAB := Line(A, B) |
| 152 | +-- lineCD := Line(C, D) |
| 153 | +-- Parallel(lineAB, lineCD) |
| 154 | +-- ParallelMarker1(lineAB, lineCD) |
| 155 | +-- AutoLabel A, B, C, D |
| 156 | +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: |
| 157 | +-- Point A, B, C, D |
| 158 | +-- Segment segmentAB, segmentCD |
| 159 | +-- segmentAB := Segment(A, B) |
| 160 | +-- segmentCD := Segment(C, D) |
| 161 | +-- EqualLength(segmentAB, segmentCD) |
| 162 | +-- EqualLengthMarker(segmentAB, segmentCD) |
| 163 | +-- AutoLabel A, B, C, D |
| 164 | +predicate EqualLength(Linelike, Linelike) -- This predicate makes two segments have equal length. Example usage: |
| 165 | +-- Point A, B, C, D |
| 166 | +-- Segment segmentAB, segmentCD |
| 167 | +-- segmentAB := Segment(A, B) |
| 168 | +-- segmentCD := Segment(C, D) |
| 169 | +-- EqualLength(segmentAB, segmentCD) |
| 170 | +-- AutoLabel A, B, C, D |
| 171 | +predicate Parallel(Linelike, Linelike) -- This predicate makes two lines parallel. Example usage: |
| 172 | +-- Point A, B, C, D |
| 173 | +-- Line lineAB, lineCD |
| 174 | +-- lineAB := Line(A, B) |
| 175 | +-- lineCD := Line(C, D) |
| 176 | +-- Parallel(lineAB, lineCD) |
| 177 | +-- AutoLabel A, B, C, D |
| 178 | + |
| 179 | +-- Angles |
| 180 | +predicate Acute(Angle) -- This predicate makes an angle acute. Example usage: |
| 181 | +-- Point A, B, C |
| 182 | +-- Angle angleABC |
| 183 | +-- angleABC := InteriorAngle(A, B, C) |
| 184 | +-- Acute(angleABC) |
| 185 | +-- AutoLabel A, B, C |
| 186 | +predicate Obtuse(Angle) -- This predicate makes an angle obtuse. Example usage: |
| 187 | +-- Point A, B, C |
| 188 | +-- Angle angleABC |
| 189 | +-- angleABC := InteriorAngle(A, B, C) |
| 190 | +-- Obtuse(angleABC) |
| 191 | +-- AutoLabel A, B, C |
| 192 | +predicate RightMarked(Angle) -- This predicate makes an angle right and marks it with a square. Example usage: |
| 193 | +-- Point A, B, C |
| 194 | +-- Angle angleABC |
| 195 | +-- angleABC := InteriorAngle(A, B, C) |
| 196 | +-- RightMarked(angleABC) |
| 197 | +-- AutoLabel A, B, C |
| 198 | +predicate RightUnmarked(Angle) -- This predicate makes an angle right and does not mark it with a square. Example usage: |
| 199 | +-- Point A, B, C |
| 200 | +-- Angle angleABC |
| 201 | +-- angleABC := InteriorAngle(A, B, C) |
| 202 | +-- RightUnmarked(angleABC) |
| 203 | +-- AutoLabel A, B, C |
| 204 | +predicate AngleBisector(Angle, Linelike) -- This predicate makes a ray be the angle bisector of an angle. Example usage: |
| 205 | +-- Point A, B, C |
| 206 | +-- Angle angleABC |
| 207 | +-- angleABC := InteriorAngle(A, B, C) |
| 208 | +-- Ray rayABC |
| 209 | +-- rayABC := Ray(A, B) |
| 210 | +-- AngleBisector(angleABC, rayABC) |
| 211 | +-- AutoLabel A, B, C |
| 212 | +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: |
| 213 | +-- Point A, B, C, D, E, F |
| 214 | +-- Angle angleABC, angleDEF |
| 215 | +-- angleABC := InteriorAngle(A, B, C) |
| 216 | +-- angleDEF := InteriorAngle(D, E, F) |
| 217 | +-- EqualAngle(angleABC, angleDEF) |
| 218 | +-- EqualAngleMarker(angleABC, angleDEF) |
| 219 | +-- AutoLabel A, B, C, D, E, F |
| 220 | +predicate EqualAngle(Angle, Angle) -- This predicate makes two angles have equal measure. Example usage: |
| 221 | +-- Point A, B, C, D, E, F |
| 222 | +-- Angle angleABC, angleDEF |
| 223 | +-- angleABC := InteriorAngle(A, B, C) |
| 224 | +-- angleDEF := InteriorAngle(D, E, F) |
| 225 | +-- EqualAngle(angleABC, angleDEF) |
| 226 | +-- AutoLabel A, B, C, D, E, F |
| 227 | + |
| 228 | +-- Polygons/Shapes |
| 229 | +predicate Parallelogram(Quadrilateral) -- This predicate makes a quadrilateral a parallelogram. Example usage: |
| 230 | +-- Point A, B, C, D |
| 231 | +-- Quadrilateral quadrilateralABCD |
| 232 | +-- quadrilateralABCD := Quadrilateral(A, B, C, D) |
| 233 | +-- Parallelogram(quadrilateralABCD) |
| 234 | +-- AutoLabel A, B, C, D |
| 235 | +predicate OnCircle(Circle, Point) -- This predicate makes a point be on a circle. Example usage: |
| 236 | +-- Point A, B, C |
| 237 | +-- Circle circleAB |
| 238 | +-- circleAB := CircleR(A, B) |
| 239 | +-- OnCircle(circleAB, C) |
| 240 | +-- AutoLabel A, B, C |
| 241 | +predicate CircleCenter(Circle, Point) -- Do not use. |
| 242 | +predicate Incenter(Point, Triangle) -- This predicate makes a point be the incenter of a triangle. Example usage: |
| 243 | +-- Point A, B, C, D |
| 244 | +-- Triangle triangleABC |
| 245 | +-- triangleABC := Triangle(A, B, C) |
| 246 | +-- Incenter(D, triangleABC) |
| 247 | +-- AutoLabel A, B, C, D |
| 248 | +predicate Orthocenter(Point, Triangle) -- This predicate makes a point be the orthocenter of a triangle. Example usage: |
| 249 | +-- Point A, B, C, D |
| 250 | +-- Triangle triangleABC |
| 251 | +-- triangleABC := Triangle(A, B, C) |
| 252 | +-- Orthocenter(D, triangleABC) |
| 253 | +-- AutoLabel A, B, C, D |
| 254 | +predicate Centroid(Point, Triangle) -- This predicate makes a point be the centroid of a triangle. Example usage: |
| 255 | +-- Point A, B, C, D |
| 256 | +-- Triangle triangleABC |
| 257 | +-- triangleABC := Triangle(A, B, C) |
| 258 | +-- Centroid(D, triangleABC) |
| 259 | +-- AutoLabel A, B, C, D |
| 260 | +predicate Circumcenter(Point, Triangle) -- This predicate makes a point be the circumcenter of a triangle. Example usage: |
| 261 | +-- Point A, B, C, D |
| 262 | +-- Triangle triangleABC |
| 263 | +-- triangleABC := Triangle(A, B, C) |
| 264 | +-- Circumcenter(D, triangleABC) |
| 265 | +-- AutoLabel A, B, C, D |
0 commit comments