Fuzion Logo
flang.dev — The Fuzion Language Portal
JavaScript seems to be disabled. Functionality is limited.

quantors.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 quantors
#
#  Author: Fridtjof Siebert (siebert@tokiwa.software)
#
# -----------------------------------------------------------------------

# quantors -- unit type feature containing quantors ∀ and ∃.
#
# quantors provides forAll and exists-quantors for use in contracts qualified
# for analysis.
#
#
quantors is

  # forAll quantors for use in analysis parts of contracts
  #
  # These quantors can be used to check that predicates hold for all values
  # of one or several specific types.
  #
  # NYI: If open generics could be passed as actual generic arguments, we no
  # longer need this code duplication here:
  #   forAll(A..., f A -> bool) bool is intrinsic
  #
  forAll  (A0                                     type, f (A0                                    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll2 (A0, A1                                 type, f (A0, A1                                ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll3 (A0, A1, A2                             type, f (A0, A1, A2                            ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll4 (A0, A1, A2, A3                         type, f (A0, A1, A2, A3                        ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll5 (A0, A1, A2, A3, A4                     type, f (A0, A1, A2, A3, A4                    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll6 (A0, A1, A2, A3, A4, A5                 type, f (A0, A1, A2, A3, A4, A5                ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll7 (A0, A1, A2, A3, A4, A5, A6             type, f (A0, A1, A2, A3, A4, A5, A6            ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll8 (A0, A1, A2, A3, A4, A5, A6, A7         type, f (A0, A1, A2, A3, A4, A5, A6, A7        ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll9 (A0, A1, A2, A3, A4, A5, A6, A7, A8     type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  forAll10(A0, A1, A2, A3, A4, A5, A6, A7, A8, A9 type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9) -> bool) bool is fuzion.std.panic "quantors are for analysis only"

  # short-hand forAll using '∀' symbol
  prefix ∀ (A type, f A -> bool) => forAll f

  # exists quantors for use in analysis parts of contracts
  #
  # These quantors can be used to check that predicates hold for at least one
  # value of one or several specific types.
  #
  # NYI: If open generics could be passed as actual generic arguments, we no
  # longer need this code duplication here:
  #   exists(A..., f A -> bool) bool is intrinsic
  #
  exists  (A0                                     type, f (A0                                    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists2 (A0, A1                                 type, f (A0, A1                                ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists3 (A0, A1, A2                             type, f (A0, A1, A2                            ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists4 (A0, A1, A2, A3                         type, f (A0, A1, A2, A3                        ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists5 (A0, A1, A2, A3, A4                     type, f (A0, A1, A2, A3, A4                    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists6 (A0, A1, A2, A3, A4, A5                 type, f (A0, A1, A2, A3, A4, A5                ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists7 (A0, A1, A2, A3, A4, A5, A6             type, f (A0, A1, A2, A3, A4, A5, A6            ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists8 (A0, A1, A2, A3, A4, A5, A6, A7         type, f (A0, A1, A2, A3, A4, A5, A6, A7        ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists9 (A0, A1, A2, A3, A4, A5, A6, A7, A8     type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8    ) -> bool) bool is fuzion.std.panic "quantors are for analysis only"
  exists10(A0, A1, A2, A3, A4, A5, A6, A7, A8, A9 type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9) -> bool) bool is fuzion.std.panic "quantors are for analysis only"

  # short-hand exists using '∃' symbol
  prefix ∃ (A type, f A -> bool) => exists f

  /*
    NYI: eventually, the following declaration should become possible:

    prefix ∃ (A type, f A -> bool) => !∀ fun bool.prefix ! ∘ f
  */