VSL - The data.collection_sigs Structure

# Copyright 2011  Petter Urkedal
#
# This file is part of the Viz Standard Library <http://www.vizlang.org/>.
#
# The Viz Standard Library (VSL) is free software: you can redistribute it
# and/or modify it under the terms of the GNU Lesser General Public License as
# published by the Free Software Foundation, either version 3 of the License,
# or (at your option) any later version.
#
# The VSL 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 Lesser General Public License for
# more details.
#
# You should have received a copy of the GNU Lesser General Public License
# along with the VSL.  If not, see <http://www.gnu.org/licenses/>.


# Z.  Collection Signatures

open prelude.ubiquitous


# Z.Z.  A Collection

sig a_collection
    type t
    type elt


    # Z.Z.Z.  Iteration and Transformations

    val fold : (elt → β → β) → t → β → β

    val foldr : (elt → β → β) → t → β → β

    val for_all : (elt → bool) → t → bool

    val for_some : (elt → bool) → t → bool

    val count : (elt → bool) → t → int

    val card : t → int

    val iter : (elt → effect ψ unit) → t → effect ψ unit

    val iterr : (elt → effect ψ unit) → t → effect ψ unit


sig a_collection'
    type t α
    type elt α


    # Z.Z.Z.  Iteration and Transformations

    val fold : (elt α → β → β) → t α → β → β

    val foldr : (elt α → β → β) → t α → β → β

    val for_all : (elt α → bool) → t α → bool

    val for_some : (elt α → bool) → t α → bool

    val count : (elt α → bool) → t α → int

    val card : t α → int

    val iter : (elt α → effect ψ unit) → t α → effect ψ unit

    val iterr : (elt α → effect ψ unit) → t α → effect ψ unit


# Z.Z.  An Indexed Family

sig an_indexed_family'
    include a_collection'

    type index

    #?ffoc {#
    in tagged include a_collection'.[t α = t α, elt α = index × elt α]
    in scheme include a_collection'.[t α = t α, elt α = index]
    #?ffoc #}


# Z.Z.  A Set

sig a_set
    include a_collection


    # Z.Z.Z.  Building or Querying

    val empty : t

    val is_empty : t → bool

    val singleton : elt → t

    val contains : elt → t → bool

    val add : elt → t → t

    val remove : elt → t → t

    val pop : elt → t → option t


    # Z.Z.Z.  Transformations

    val map : (elt → elt) → t → t

    val filter : (elt → bool) → t → t

    val filter_map : (elt → option elt) → t → t


    # Z.Z.Z.  Binary Operations

    val eq : t → t → bool

    val subeq : t → t → bool

    val union : t → t → t

    val isecn : t → t → t

    val complement : t → t → t


sig an_ordered_set
    include a_set

    val pop_min : t → option (elt × t)

    val pop_max : t → option (elt × t)


# Z.Z.  A Map

sig a_map'
    include an_indexed_family'


    # Z.Z.Z.  Building or Querying

    val empty : t α

    val is_empty : t α → bool

    val singleton : index → elt α → t α

    val contains : index → t α → bool

    val find : index → t α → option α

    val add : index → elt α → t α → t α

    val remove : index → t α → t α

    val pop : index → t α → option (elt α × t α)


    # Z.Z.Z.  Transformations

    val map : (elt α → elt β) → t α → t β

    val mapi : (index → elt α → elt β) → t α → t β

    val filter : (elt α → bool) → t α → t α


    # Z.Z.Z.  Binary Operations

    val eq_for : (α → β → bool) → t α → t β → bool

    val subeq_for : (α → β → bool) → t α → t β → bool

    val left_union : t α → t α → t α

    val left_isecn : t α → t α → t α

    val complement : t α → t α → t α

    #?ffoc {#

    in tagged
	val map : (elt α → elt β) → t α → t β

	val filter : (elt α → bool) → t α → t α

	val filter_map : (elt α → option (elt β)) → t α → t β

    in scheme
	val eq : t α → t β → bool

	val subeq : t α → t β → bool

	val map : (index → index) → t α → t α

	val filter : (index → bool) → t α → t α

	val filter_map : (index → option index) → t α → t α

    #?ffoc #}


# Z.Z.  An Ordered Map

sig an_ordered_map'
    include a_map'

    #?ffoc {#

    in tagged
	val min : t α → option (index × elt α)

	val max : t α → option (index × elt α)

	val pop_min : t α → option (index × elt α × t α)

	val pop_max : t α → option (index × elt α × t α)

    in scheme
	val min : t α → option index

	val max : t α → option index

	val pop_min : t α → option (index × t α)

	val pop_max : t α → option (index × t α)

    #?ffoc #}