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 */