Quelle iStream.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** {5 Purely functional streams}

  Contrarily to OCaml module [Stream], these are meant to be used purely
  functionally. This implies in particular that accessing an element does not
  discard it. *)

type +'a t
(** Type of pure streams. *)

type 'a node =
| Nil
| Cons of 'a * 'a t
(** View type to decompose and build streams. *)

(** {6 Constructors} *)

val empty : 'a t
(** The empty stream. *)

val cons : 'a -> 'a t -> 'a t
(** Append an element in front of a stream. *)

val thunk : (unit -> 'a node) -> 'a t
(** Internalize the laziness of a stream. *)

(** {6 Destructors} *)

val is_empty : 'a t -> bool
(** Whethere a stream is empty. *)

val peek : 'a t -> 'a node
(** Return the head and the tail of a stream, if any. *)

(** {6 Standard operations}

    All stream-returning functions are lazy. The other ones are eager. *)

val app : 'a t -> 'a t -> 'a t
(** Append two streams. Not tail-rec. *)

val map : ('a -> 'b) -> 'a t -> 'b t
(** Mapping of streams. Not tail-rec. *)

val iter : ('a -> unit) -> 'a t -> unit
(** Iteration over streams. *)

val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
(** Fold over streams. *)

val concat : 'a t t -> 'a t
(** Appends recursively a stream of streams. *)

val map_filter : ('a -> 'b option) -> 'a t -> 'b t
(** Mixing [map] and [filter]. Not tail-rec. *)

val concat_map : ('a -> 'b t) -> 'a t -> 'b t
(** [concat_map f l] is the same as [concat (map f l)]. *)

(** {6 Conversions} *)

val of_list : 'a list -> 'a t
(** Convert a list into a stream. *)

val to_list : 'a t -> 'a list
(** Convert a stream into a list. *)

(** {6 Other}*)

val force : 'a t -> 'a t
(** Forces the whole stream. *)

quality99%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.