Remove real type from standard library #495

This removes all functions which previously operated on the real data
type, including any related constants (such as PI).

modules/wyrt/src/whiley/lang/Math.whiley

@@ -39,20 +39,6 @@ ensures x < 0 ==> r == -x:
     else:
         return x
 
-/**
- * Return absolute value of real variable.
- */
-public function abs(real x) -> (real r)
-// if input positive, then result equals input
-ensures x >= 0.0 ==> r == x
-// if input negative, then result equals negated input
-ensures x < 0.0 ==> r == -x:
-    //
-    if x < 0.0:
-        return -x
-    else:
-        return x
-
 /**
  * Return maximum of two integer variables
  */
@@ -67,20 +53,6 @@ ensures r == a || r == b:
     else:
         return a
 
-/**
- * Return maximum of two real variables
- */
-public function max(real a, real b) -> (real r)
-// Return cannot be smaller than either parameter
-ensures r >= a && r >= b
-// Return value must equal one parameter
-ensures r == a || r == b:
-    //
-    if a < b:
-        return b
-    else:
-        return a
-
 /**
  * Return minimum of two integer variables
  */
@@ -95,20 +67,6 @@ ensures r == a || r == b:
     else:
         return a
 
-/**
- * Return minimum of two real variables
- */
-public function min(real a, real b) -> (real r)
-// Return cannot be greater than either parameter
-ensures r <= a && r <= b
-// Return value must equal one parameter
-ensures r == a || r == b:
-    //
-    if a > b:
-        return b
-    else:
-        return a
-
 /**
  * Return integer value raised to a given power.
  */
@@ -123,65 +81,6 @@ requires exponent > 0:
         i = i + 1
     return r
 
-/**
- * Return largest integer which is less-than-or-equal to
- * the given value
- */
-public function floor(real x) -> (int result)
-// Return is greater-than-or-equal to input
-ensures ((real) result) <= x
-// Input value is between return and return plus one
-ensures ((real) result + 1) > x:
-    //
-    int num = numerator(x)
-    int den = denominator(x)
-    int r = num / den
-    if x < 0.0 && den != 1:
-        return r - 1
-    else:
-        return r
-
-/**
- * Return smallest integer which is greater-than-or-equal to
- * the given value
- */
-public function ceil(real x) -> (int result)
-// Return is greater-than-or-equal to input
-ensures x <= ((real) result)
-// Input value is between return and return less one
-ensures ((real) result - 1) < x:
-    //
-    int num = numerator(x)
-    int den = denominator(x)
-    int r = num / den
-    if x > 0.0 && den != 1:
-        return r + 1
-    else:
-        return r
-
-/**
- * Round an arbitrary number to the nearest integer,
- * following the "round half away from zero" protocol.
- */
-public function round(real x) -> (int r)
-// Difference between input and return is 0.5 or less
-ensures max(x,(real) r) - min(x, (real) r) <= 0.5:
-    //
-    if x >= 0.0:
-        return floor(x + 0.5)
-    else:
-        return ceil(x - 0.5)
-
-/**
- * The constant PI to 20 decimal places.  Whilst this is clearly an
- * approximation, it should be sufficient for most purposes.
- */
-constant PI is 3.14159265358979323846
-
-constant E is 2.718281828459045
-
-constant ERROR is 0.00000000000000000001
-
 // Based on an excellent article entitled "Integer Square Roots"
 // by Jack W. Crenshaw, published in the eetimes, 1998.
 public function isqrt(int x) -> (int r)
@@ -193,22 +92,4 @@ ensures r >= 0:
     while square <= x:
         square = square + delta
         delta = delta + 2
-    return (delta/2) - 1
-
-// The following is a first approximation at this.  It computes the
-// square root of a number to within a given error threshold.
-public native function sqrt(int x, real error) -> (real r)
-    requires x >= 0
-    ensures r >= 0.0
-
-public function sqrt(real x, real error) -> (real r)
-requires x >= 0.0
-ensures r >= 0.0:
-    //
-    int numerator = numerator(x)
-    int denominator = denominator(x)
-    return sqrt(numerator,error) / sqrt(denominator,error)
-
-native function numerator(real x) -> (int n)
-
-native function denominator(real x) -> (int n)
+    return (delta/2) - 1