quantor.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)
#
# -----------------------------------------------------------------------
# quantor -- unit type feature containing quantors ∀ and ∃.
#
# quantor provides for_all and exists-quantors for use in contracts qualified
# for analysis.
#
#
public quantor is
# for_all 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:
# for_all(A..., f A -> bool) bool => intrinsic_constructor
#
for_all (A0 type, f (A0 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all2 (A0, A1 type, f (A0, A1 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all3 (A0, A1, A2 type, f (A0, A1, A2 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all4 (A0, A1, A2, A3 type, f (A0, A1, A2, A3 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all5 (A0, A1, A2, A3, A4 type, f (A0, A1, A2, A3, A4 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all6 (A0, A1, A2, A3, A4, A5 type, f (A0, A1, A2, A3, A4, A5 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all7 (A0, A1, A2, A3, A4, A5, A6 type, f (A0, A1, A2, A3, A4, A5, A6 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all8 (A0, A1, A2, A3, A4, A5, A6, A7 type, f (A0, A1, A2, A3, A4, A5, A6, A7 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all9 (A0, A1, A2, A3, A4, A5, A6, A7, A8 type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
for_all10(A0, A1, A2, A3, A4, A5, A6, A7, A8, A9 type, f (A0, A1, A2, A3, A4, A5, A6, A7, A8, A9) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
# short-hand for_all using '∀' symbol
public prefix ∀ (A type, f A -> bool) => for_all 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 => intrinsic_constructor
#
exists (A0 type, f (A0 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
exists2 (A0, A1 type, f (A0, A1 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
exists3 (A0, A1, A2 type, f (A0, A1, A2 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
exists4 (A0, A1, A2, A3 type, f (A0, A1, A2, A3 ) -> bool) bool => fuzion.std.panic "quantors are for analysis only"
exists5 (A0, A1, A2, A3, A4 type, f (A0, A1, A2, A3, A4 ) -> bool) bool => 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 => 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 => 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 => 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 => 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 => fuzion.std.panic "quantors are for analysis only"
# short-hand exists using '∃' symbol
public 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
*/