numeric.fz

# This file is part of the Fuzion language implementation.
#
# The Fuzion language implementation is free software: you can redistribute it
# and/or modify it under the terms of the GNU General Public License as published
# by the Free Software Foundation, version 3 of the License.
#
# The Fuzion language implementation is distributed in the hope that it will be
# useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License along with The
# Fuzion language implementation.  If not, see <https://www.gnu.org/licenses/>.


# -----------------------------------------------------------------------
#
#  Tokiwa Software GmbH, Germany
#
#  Source code of Fuzion standard library feature numeric
#
#  Author: Fridtjof Siebert (siebert@tokiwa.software)
#
# -----------------------------------------------------------------------

# numeric -- parent of all numeric features
#
module:public numeric : property.hashable, property.orderable is

  public is_zero => numeric.this = numeric.this.zero
  public is_one  => numeric.this = numeric.this.one

  # basic operations: 'prefix +' (identity)
  public prefix + numeric.this
    pre
      safety: +!numeric.this
  => numeric.this

  # basic operations: 'prefix -' (negation)
  public prefix - numeric.this
    pre
      safety: -!numeric.this
  => numeric.this.zero - numeric.this

  # basic operations: 'infix +' (addition)
  public infix +  (other numeric.this) numeric.this
    pre
      safety: (numeric.this +! other)
  => abstract

  # basic operations: 'infix -' (subtraction)
  public infix -  (other numeric.this) numeric.this
    pre
      safety: (numeric.this -! other)
  => abstract

  # basic operations: 'infix *' (multiplication)
  public infix *  (other numeric.this) numeric.this
    pre
      safety: (numeric.this *! other)
  => abstract

  # basic operations: 'infix /' (division)
  public infix /  (other numeric.this) numeric.this
    pre
      safety: (numeric.this /! other)
      safety: (other != numeric.this.zero)
  => abstract

  # basic operations: 'infix %' (division remainder)
  public infix %  (other numeric.this) numeric.this
    pre
      safety: (numeric.this %! other)
      safety: (other != numeric.this.zero)
  => abstract

  # basic operations: 'infix **' (exponentiation)
  public infix ** (other numeric.this) numeric.this
    pre
      safety: (numeric.this **! other)
      safety: (other ≥ numeric.this.zero)
  => abstract


  # preconditions for basic operations: true if the operation's result is
  # representable for the given values
  #
  # This does not check if the operation is defined (i.e, it
  # returns true for '3/!0' or '0**!0'.)
  #
  public prefix +! bool => true
  public prefix -! bool => abstract
  public infix +! (other numeric.this) bool => abstract
  public infix -! (other numeric.this) bool => abstract
  public infix *! (other numeric.this) bool => abstract
  public infix /! (other numeric.this) bool => abstract
  public infix %! (other numeric.this) bool => abstract
  public infix **!(other numeric.this) bool => abstract


  # overflow checking operations
  public prefix -? num_option numeric.this => - numeric.this
  public infix +? (other numeric.this) num_option numeric.this => numeric.this + other
  public infix -? (other numeric.this) num_option numeric.this => numeric.this - other
  public infix *? (other numeric.this) num_option numeric.this => numeric.this * other
  public infix **?(other numeric.this) num_option numeric.this => abstract

  # saturating  operations
  public prefix -^  numeric.this => - numeric.this
  public infix +^ (other numeric.this) numeric.this => numeric.this + other
  public infix -^ (other numeric.this) numeric.this => numeric.this - other
  public infix *^ (other numeric.this) numeric.this => numeric.this * other
  public infix **^(other numeric.this) numeric.this => abstract


  public sign => if numeric.this = numeric.this.zero then 0 else if numeric.this > numeric.this.zero then 1 else -1

  public abs => if sign ≥ 0 then numeric.this else -numeric.this


  # the u32 value corresponding to this
  # note: potential fraction will be discarded
  # NYI replace this by as_u32?
  to_u32 u32
    pre
      debug: (numeric.this ≥ numeric.this.zero)
  =>
    if (numeric.this ≥ numeric.this.one) ((numeric.this - numeric.this.one).to_u32 + 1)
    else 0


  # this numeric value as an u8
  public as_u8 u8
    pre
      debug: (numeric.this ≥ numeric.this.zero)
  => abstract


  # find the highest power of b that is less or equal than numeric.this.
  #
  module highest(b numeric.this) numeric.this
    pre
      debug: (numeric.this.sign ≥ 0)
    post
      debug: (numeric.this = numeric.this.zero: result = numeric.this.one)
      debug: (numeric.this != numeric.this.zero: numeric.this / b < result ≤ numeric.this)
  # NYI: original postcondition code should cause a compiler error since
  # result.infix <= expects an argument of type T while integer.this =>
  # not of type T.
  #
  #     integer.this != zero: integer.this / b < result <= integer.this
  =>
    for
      bs := numeric.this.one, bs * b
    while numeric.this / b ≥ bs


  # is this part of given set
  #
  # NYI: infix operators currently always use dynamic binding on the lhs and pass
  # the rhs as an argument.  If we would support an 'rinfix ∈' that would use the
  # rhs for dynamic binding and the lhs as argument, we could define '∈' in Set T
  # and it would work for all set types.
  #
  public element_of(s container.Set numeric.this) => s.contains numeric.this
  public infix ∈ (s container.Set numeric.this) => numeric.this.element_of s

  # is this not part of given set
  #
  public not_element_of(s container.Set numeric.this) => !element_of s
  public infix ∉ (s container.Set numeric.this) => numeric.this.not_element_of s


  # -----------------------------------------------------------------------
  #
  # type features:


  # identity element for 'infix +'
  #
  public type.zero numeric.this => abstract


  # identity element for 'infix *'
  #
  public type.one  numeric.this => abstract


  # the value corresponding to v in whatever integer implementation we have,
  # maximum in case of overflow
  #
  public type.from_u32(v u32) numeric.this =>
    if v = 0 zero else (from_u32 v-1) +^ one


  # the constant '2' in whatever integer implementation we have, maximum in case of overflow
  #
  public type.two => from_u32 2


  # the constant '10' in whatever integer implementation we have, maximum in case of overflow
  #
  public type.ten => from_u32 10


  # equality
  #
  public type.equality(a, b numeric.this) bool => abstract


  # total order
  #
  public type.lteq(a, b numeric.this) bool => abstract


  # monoid of numeric with infix + operation.  Will create sum of all elements it
  # is applied to.
  #
  public type.sum : Monoid numeric.this is
    public redef infix ∙ (a, b numeric.this) => a + b
    public redef e => zero


  # monoid of numeric with infix * operation.  Will create product of all elements
  # it is applied to.
  #
  public type.product : Monoid numeric.this is
    public redef infix ∙ (a, b numeric.this) => a * b
    public redef e => one


  # monoid of numeric with infix +^ operation.  Will create sum of all elements it
  # is applied to, stopping at max/min value in case of overflow.
  #
  public type.sum_saturating : Monoid numeric.this is
    public redef infix ∙ (a, b numeric.this) => a +^ b
    public redef e => zero


  # monoid of numeric with infix *^ operation.  Will create product of all elements
  # it is applied to, stopping at max/min value in case of overflow.
  #
  public type.product_saturating : Monoid numeric.this is
    public redef infix ∙ (a, b numeric.this) => a *^ b
    public redef e => one