Source file `IFSeqSig.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(******************************************************************************)
(*                                                                            *)
(*                                     Feat                                   *)
(*                                                                            *)
(*                        François Pottier, Inria Paris                       *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the MIT license, as described in the file LICENSE.               *)
(******************************************************************************)

(**A signature for implicit finite sequences.

   These sequences are implicit, which means that they are not explicitly
   represented in memory as actual sequences of elements; instead, they are
   described by a data structure which contains enough information to produce
   an arbitrary element upon request. This design decision imposes some
   constraints on the operations that can be efficiently supported; for
   instance, [filter] is not supported.

   This signature forms an applicative functor. *)
module type IFSEQ_BASIC = sig

  (**['a seq] is the type of sequences whose elements have type ['a]. *)
  type 'a seq

  (**Constructors. *)

  (**[empty] is a sequence of length zero. *)
  val empty: 'a seq

  (**[zero] is a synonym for [empty]. *)
  val zero : 'a seq

  (**[singleton x] is a sequence of length one whose single element is [x]. *)
  val singleton: 'a -> 'a seq

  (**[one] is a synonym for [singleton]. *)
  val one:       'a -> 'a seq

  (**[rev xs] is the reverse of the sequence [xs]. *)
  val rev: 'a seq -> 'a seq

  (**[sum s1 s2] is the concatenation of the sequences [s1] and [s2]. *)
  val sum    : 'a seq -> 'a seq -> 'a seq

  (**[(++)] is a synonym for [sum]. *)
  val ( ++ ) : 'a seq -> 'a seq -> 'a seq

  (**[product s1 s2] is the Cartesian product of the sequences [s1] and [s2].
     Its length is the product of the lengths of [s1] and [s2]. The first pair
     component is considered most significant. *)
  val product: 'a seq -> 'b seq -> ('a * 'b) seq

  (**[( ** )] is a synonym for [product]. *)
  val ( ** ) : 'a seq -> 'b seq -> ('a * 'b) seq

  (**[map phi s] is the image of the sequence [s] through the function [phi].
     If the user wishes to work with sequences of pairwise distinct elements,
     then [phi] should be injective. If furthermore the user wishes to work
     with sequences that enumerate all elements of a type, then [phi] should
     be surjective. *)
  val map: ('a -> 'b) -> 'a seq -> 'b seq

  (**[up i j] is the sequence of the integers from [i] included up to [j]
     excluded. *)
  val up: int -> int -> int seq

  (* Observations. *)

  (**The type [index] is the type of integers used to represent indices and
     lengths. *)
  type index

  (**[length s] is the length of the sequence [s]. *)
  val length: 'a seq -> index

  (**[get s i] is the [i]-th element of the sequence [s]. The index [i] must
     be comprised between zero included and [length s] excluded. *)
  val get: 'a seq -> index -> 'a

  (**[foreach s k] iterates over all elements of the sequence [s]. Each
     element in turn is passed to the loop body [k]. *)
  val foreach: 'a seq -> ('a -> unit) -> unit

  (**[to_seq s k] produces an explicit representation of the sequence [s] as a
     sequence in the sense of OCaml's standard library module [Seq]. This
     sequence is prepended in front of the existing sequence [k]. *)
  val to_seq: 'a seq -> 'a Seq.t -> 'a Seq.t

end

(**This signature extends {!IFSEQ_BASIC} with more operations. *)
module type IFSEQ_EXTENDED = sig

  include IFSEQ_BASIC

  (**Iterated sum. *)
  val bigsum: 'a seq list -> 'a seq

  (**Indexed iterated sum. *)
  val exists: 'a list -> ('a -> 'b seq) -> 'b seq

  (**[sample m s k] is an explicit sequence of at most [m] elements extracted
     out of the implicit sequence [s], prepended in front of the existing
     sequence [k]. If [length s] is at most [m], then all elements of [s] are
     produced. Otherwise, a random sample of [m] elements extracted out of [s]
     is produced. *)
  val sample: int -> 'a seq -> 'a Seq.t -> 'a Seq.t

end