123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513(******************************************************************************)(* *)(* Mulnir *)(* *)(* Frédéric Bour, Tarides *)(* *)(* Menhir *)(* *)(* François Pottier, Inria Paris *)(* Yann Régis-Gianas, PPS, Université Paris Diderot *)(* *)(* Copyright Inria. All rights reserved. This file is distributed under the *)(* terms of the GNU General Public License version 2, as described in the *)(* file LICENSE. *)(* *)(******************************************************************************)moduletypeS1=sig(* Elements are assumed to have a natural total order. *)type'aelement(* Sets. *)type'at(* The empty set. *)valempty:'at(* [is_empty s] tells whether [s] is the empty set. *)valis_empty:'at->boolvalis_not_empty:'at->bool(* [singleton x] returns a singleton set containing [x] as its only
element. *)valsingleton:'aelement->'at(* [is_singleton s] tests whether [s] is a singleton set. *)valis_singleton:'at->bool(* [cardinal s] returns the cardinal of [s]. *)valcardinal:'at->int(* [choose s] returns an arbitrarily chosen element of [s], if [s]
is nonempty, and raises [Not_found] otherwise. *)valchoose:'at->'aelement(** [minimum s] returns [Some x] where [x] is the smallest element of [s],
or [None] if [s] is empty. *)valminimum:'at->'aelementoption(** [maximum s] returns [Some x] where [x] is the largest element of [s],
or [None] if [s] is empty. *)valmaximum:'at->'aelementoption(* [mem x s] returns [true] if and only if [x] appears in the set
[s]. *)valmem:'aelement->'at->bool(* [add x s] returns a set whose elements are all elements of [s],
plus [x]. If [x] was already in [s], [s] is returned unchanged. *)valadd:'aelement->'at->'at(* [remove x s] returns a set whose elements are all elements of
[s], except [x]. If [x] was not in [s], [s] is returned unchanged. *)valremove:'aelement->'at->'at(* [union s1 s2] returns the union of the sets [s1] and [s2]. *)valunion:'at->'at->'at(* [inter s t] returns the set intersection of [s] and [t], that is,
$s\cap t$. *)valinter:'at->'at->'at(* [disjoint s1 s2] returns [true] if and only if the sets [s1] and
[s2] are disjoint, i.e. iff their intersection is empty. *)valdisjoint:'at->'at->bool(* [iter f s] invokes [f x], in turn, for each element [x] of the
set [s]. Elements are presented to [f] in increasing order. *)valiter:('aelement->unit)->'at->unitvaliteri:(int->'aelement->unit)->'at->unitvalrev_iter:('aelement->unit)->'at->unit(* [fold f s seed] invokes [f x accu], in turn, for each element [x]
of the set [s]. Elements are presented to [f] in increasing
order. The initial value of [accu] is [seed]; then, at each new
call, its value is the value returned by the previous invocation
of [f]. The value returned by [fold] is the final value of
[accu]. In other words, if $s = \{ x_1, x_2, \ldots, x_n \}$,
where $x_1 < x_2 < \ldots < x_n$, then [fold f s seed] computes
$([f]\,x_n\,\ldots\,([f]\,x_2\,([f]\,x_1\,[seed]))\ldots)$. *)valfold:('aelement->'b->'b)->'at->'b->'b(** [fold_right f acc x] computes [f acc x] for each element [x] of [s],
in descending order. The initial value of [acc] is [seed]; the final
value is the returned value. *)valfold_right:('a->'belement->'a)->'a->'bt->'a(** [map f s] returns the set whose elements are [f x] for each [x] in [s]. *)valmap:('aelement->'belement)->'at->'bt(** [exists f s] returns [true] if [f x] is true for at least one element
[x] in [s]. *)valexists:('aelement->bool)->'at->bool(** [for_all f s] returns [true] if [f x] is true for all elements [x]
in [s]. *)valfor_all:('aelement->bool)->'at->bool(* [elements s] is a list of all elements in the set [s]. *)valelements:'at->'aelementlist(* [compare] is an ordering over sets. *)valcompare:'at->'at->int(* [equal] implements equality over sets. *)valequal:'at->'at->bool(* [subset s1 s2] returns [true] iff [s1 ⊆ s2]. *)valsubset:'at->'at->bool(* [quick_subset s1 s2] is a fast test for the set inclusion [s1 ⊆ s2].
The sets [s1] and [s2] must be nonempty.
It must be known ahead of time that either [s1] is a subset of [s2] or
these sets are disjoint: that is, [s1 ⊆ s2 ⋁ s1 ∩ s2 = ∅] must hold.
Under this hypothesis, [quick_subset s1 s2] can be implemented simply
by picking an arbitrary element of [s1] (if there is one) and testing
whether it is a member of [s2]. *)valquick_subset:'at->'at->bool(** [diff s1 s2] returns the set of elements that are in [s1] but not in [s2]. *)valdiff:'at->'at->'at(** {1 Decomposing sets}
These functions implement the [Refine.DECOMPOSABLE] interface.
We cannot reference it here as [Refine] is implemented using bitsets,
that would create a reference cycle.
*)(** [compare_minimum s1 s2] compares two sets by their least elements.
Returns a negative number if the least element of [s1] is smaller,
a positive number if the least element of [s2] is smaller, or zero
if both sets are empty or have equal least elements. *)valcompare_minimum:'at->'at->int(** [extract_unique_prefix s1 s2] splits [s1] into two sets:
- The first set contains elements strictly smaller than all elements of [s2]
- The second set contains the remaining elements of [s1]
{b Raises} if [s2] is empty. *)valextract_unique_prefix:'at->'at->'at*'at(** [extract_shared_prefix s1 s2] decomposes [s1] and [s2] into:
- A common prefix (elements present in both [s1] and [s2])
- The remaining parts of [s1] and [s2]
{b Returns} [(common, (rest1, rest2))] where:
- [common] contains elements that are part of both [s1] and [s2]
- [s1 = common U rest1] and [s2 = common U rest2] *)valextract_shared_prefix:'at->'at->'at*('at*'at)(** [sorted_union s] computes the union of an ordered list of sets.
This is an optimized special case of [union] that assumes the list
is already sorted by the set order. *)valsorted_union:'atlist->'at(** [of_list xs] creates a set from a list of elements. *)valof_list:'aelementlist->'at(** [init_interval i j] creates a set containing all integers from [i] to [j].
The behavior is undefined if [i > j]. *)valinit_interval:'aelement->'aelement->'at(** [init_subset i j f] creates a set containing all elements [x] such that
[i ≤ x ≤ j] and [f x] returns [true]. *)valinit_subset:'aelement->'aelement->('aelement->bool)->'at(** [filter f s] returns the set of elements [x] in [s] such that [f x]
returns [true]. *)valfilter:('aelement->bool)->'at->'at(** [filter_map f s] returns the set of elements [y] such that [f x = Some y]
for some element [x] in [s]. *)valfilter_map:('aelement->'belementoption)->'at->'bt(** [split x s] returns [(s1, found, s2)] where:
- [s1] contains all elements strictly smaller than [x]
- [s2] contains all elements strictly larger than [x]
- [found] is [true] if [x] is in [s]
- [s = s1 U {x} U s2] if [found] is [true] *)valsplit:'aelement->'at->'at*bool*'at(** [find f s] returns the first element [x] in [s] such that [f x] is true.
Raises [Not_found] if no such element exists. *)valfind:('aelement->bool)->'at->'aelement(** [find_map f s] returns [Some y] where [y] is the first element such that
[f x = Some y] for some [x] in [s], or [None] if no such element exists. *)valfind_map:('aelement->'boption)->'at->'boption(** [to_seq s] returns a sequence of all elements in [s] in ascending order. *)valto_seq:'at->'aelementSeq.t(** [bind m f] returns the union of [f x] for all elements [x] in [m]. *)valbind:'at->('aelement->'bt)->'bt(** Split a set into consecutive "runs" of elements that share the same class.
{b Parameters}
- [cls : 'a element → 'b element] that assigns a class to each element.
- [xs : 'a t] – the input set to be split.
{b Returns}
A list of pairs. Each pair is made of a class (the result of [cls] for
the run) and the subset of the original elements that belong to that run
(preserving the original order). *)valsplit_by_run:('aelement->'belement)->'at->('belement*'at)list(** [fused_inter_union s1 s2 ~acc] returns [union (inter s1 s2) acc].
This is an optimized version that computes the intersection and union
in a single pass. *)valfused_inter_union:'at->'at->acc:'at->'at(** [rev_map_elements s f] returns a list of [f x] for all elements [x]
in [s], built from the highest to the lowest element. *)valrev_map_elements:'at->('aelement->'b)->'blist(** [map_to_array s f] returns an array of [f x] for all elements [x] in
[s]. *)valmap_to_array:'at->('aelement->'b)->'barray(** [rank x s] returns the number of elements strictly smaller than [x] in the
set [s]. *)valrank:'aelement->'at->intendmoduletypeS0=sigtypeelementtypetincludeS1withtype'aelement:=elementandtype'at:=tendmoduletypeStdSetS1=sigtype'aelttype'atvalempty:'atvalis_empty:'at->boolvalmem:'aelt->'at->boolvaladd:'aelt->'at->'atvalsingleton:'aelt->'atvalremove:'aelt->'at->'atvalunion:'at->'at->'atvalinter:'at->'at->'atvaldisjoint:'at->'at->boolvaldiff:'at->'at->'atvalcompare:'at->'at->intvalequal:'at->'at->boolvalsubset:'at->'at->boolvaliter:('aelt->unit)->'at->unitvalmap:('aelt->'belt)->'at->'btvalfold:('aelt->'b->'b)->'at->'b->'bvalfor_all:('aelt->bool)->'at->boolvalexists:('aelt->bool)->'at->boolvalfilter:('aelt->bool)->'at->'atvalfilter_map:('aelt->'beltoption)->'at->'btvalpartition:('aelt->bool)->'at->'at*'atvalcardinal:'at->intvalelements:'at->'aeltlistvalmin_elt:'at->'aeltvalmin_elt_opt:'at->'aeltoptionvalmax_elt:'at->'aeltvalmax_elt_opt:'at->'aeltoptionvalchoose:'at->'aeltvalchoose_opt:'at->'aeltoptionvalsplit:'aelt->'at->'at*bool*'atvalfind:'aelt->'at->'aeltvalfind_opt:'aelt->'at->'aeltoptionvalfind_first:('aelt->bool)->'at->'aeltvalfind_first_opt:('aelt->bool)->'at->'aeltoptionvalfind_last:('aelt->bool)->'at->'aeltvalfind_last_opt:('aelt->bool)->'at->'aeltoptionvalof_list:'aeltlist->'atvalto_seq_from:'aelt->'at->'aeltSeq.tvalto_seq:'at->'aeltSeq.tvalto_rev_seq:'at->'aeltSeq.tvaladd_seq:'aeltSeq.t->'at->'atvalof_seq:'aeltSeq.t->'atendmoduletypeStdMapS1=sig(** {1 StdMapS1}
This signature provides a parameterized version of the standard library's
{!StdMap.S} signature. It is lifted to work with parameterized keys
['n key] instead of ground ones [key].
{b Note.} The type [('n, 'a) t] represents a map indexed by keys
parameterized by ['n] and carrying values of type ['a]. This is a direct
adaptation of the standard library's {!StdMap.S} signature, generalized to
support parameterized keys.
@see [StdMap.S] (standard library) for the original signature upon which
this is based.
*)type'nkeytype('n,'a)t(** {2 Basic operations} *)(** [empty] is the empty map. *)valempty:('n,'a)t(** [is_empty m] returns [true] if [m] is the empty map. *)valis_empty:('n,'a)t->bool(** [mem k m] returns [true] if key [k] is bound in map [m]. *)valmem:'nkey->('n,'a)t->bool(** [add k d m] returns a map that is the extension of [m] with binding
[k ↦ d]. If [k] was already bound in [m], the old binding is replaced
by the new one. *)valadd:'nkey->'a->('n,'a)t->('n,'a)t(** [update k f m] returns a map same as [m], except that the binding for
[k] is modified by [f]. If the binding for [k] is present in [m],
[f] is called with the current value, otherwise [f] is called with
[None]. The result of [f] determines the binding state for [k] in the
resulting map. *)valupdate:'nkey->('aoption->'aoption)->('n,'a)t->('n,'a)t(** [singleton k d] returns a map containing the single binding [k ↦ d]. *)valsingleton:'nkey->'a->('n,'a)t(** [remove m k] returns a map containing the same bindings as [m], except
that [k] is unbound in the result. *)valremove:'nkey->('n,'a)t->('n,'a)t(** [merge f m1 m2] returns a map with the same bindings as [m1] and [m2],
except that bindings that appear in both maps are combined using [f].
Specifically, for each key [k], if [k] is bound in [m1] to [a1] and in
[m2] to [a2], then [k] is bound in the result to [f k a1 a2]. *)valmerge:('nkey->'aoption->'boption->'coption)->('n,'a)t->('n,'b)t->('n,'c)t(** [union f m1 m2] is an alias for [merge] with the union combinator. *)valunion:('nkey->'a->'a->'aoption)->('n,'a)t->('n,'a)t->('n,'a)t(** {2 Comparisons} *)(** [compare cmp m1 m2] compares the two maps [m1] and [m2] using [cmp]
to compare values. Returns a negative number if [m1] is strictly
smaller than [m2], a positive number if [m1] is strictly greater
than [m2], or zero if they are equal. *)valcompare:('a->'a->int)->('n,'a)t->('n,'a)t->int(** [equal eq m1 m2] returns [true] if the two maps are equal up to
[eq], which compares values. *)valequal:('a->'a->bool)->('n,'a)t->('n,'a)t->bool(** {2 Iteration} *)(** [iter f m] invokes [f k d] for each binding [k ↦ d] in [m].
Bindings are presented in ascending key order. *)valiter:('nkey->'a->unit)->('n,'a)t->unit(** [fold f m seed] computes [f k d acc] for each binding in [m],
in ascending key order. The initial value of [acc] is [seed];
the final value is the returned value. *)valfold:('nkey->'a->'b->'b)->('n,'a)t->'b->'b(** [for_all f m] returns [true] if [f k d] is true for all bindings
[k ↦ d] in [m]. *)valfor_all:('nkey->'a->bool)->('n,'a)t->bool(** [exists f m] returns [true] if [f k d] is true for at least one
binding [k ↦ d] in [m]. *)valexists:('nkey->'a->bool)->('n,'a)t->bool(** {2 Filtering} *)(** [filter f m] returns the map with the same bindings as [m], but
only those bindings [k ↦ d] for which [f k d] returns [true]. *)valfilter:('nkey->'a->bool)->('n,'a)t->('n,'a)t(** [filter_map f m] returns the map with bindings [k ↦ d'] for each
binding [k ↦ d] in [m] such that [f k d] returns [Some d']. *)valfilter_map:('nkey->'a->'boption)->('n,'a)t->('n,'b)t(** [partition f m] returns the pair [(m1, m2)] where [m1] contains
all bindings [k ↦ d] in [m] such that [f k d] is true, and [m2]
contains the others. *)valpartition:('nkey->'a->bool)->('n,'a)t->('n,'a)t*('n,'a)t(** {2 Cardinality} *)(** [cardinal m] returns the number of bindings in [m]. *)valcardinal:('n,'a)t->int(** {2 Bindings extraction} *)(** [bindings m] is the list of all bindings in [m], in ascending order. *)valbindings:('n,'a)t->('nkey*'a)list(** [min_binding m] returns the pair [(k, d)] where [k] is the smallest
key bound in [m] and [d] is its binding. Raises [Not_found] if [m] is
empty. *)valmin_binding:('n,'a)t->('nkey*'a)(** [min_binding_opt m] returns [Some (k, d)] where [(k, d)] is the
smallest key bound in [m], or [None] if [m] is empty. *)valmin_binding_opt:('n,'a)t->('nkey*'a)option(** [max_binding m] returns the pair [(k, d)] where [k] is the largest
key bound in [m] and [d] is its binding. Raises [Not_found] if [m] is
empty. *)valmax_binding:('n,'a)t->('nkey*'a)(** [max_binding_opt m] returns [Some (k, d)] where [(k, d)] is the
largest key bound in [m], or [None] if [m] is empty. *)valmax_binding_opt:('n,'a)t->('nkey*'a)option(** [choose m] returns an arbitrarily chosen binding [(k, d)] from [m].
Raises [Not_found] if [m] is empty. *)valchoose:('n,'a)t->('nkey*'a)(** [choose_opt m] returns [Some (k, d)] if [k] is bound in [m],
or [None] if [m] is empty. *)valchoose_opt:('n,'a)t->('nkey*'a)option(** {2 Splitting} *)(** [split k m] returns [(m1, opt, m2)] where:
- [m1] contains all bindings with keys strictly smaller than [k]
- [m2] contains all bindings with keys strictly larger than [k]
- [opt] is [Some d] if [k] is bound to [d] in [m], or [None] otherwise *)valsplit:'nkey->('n,'a)t->('n,'a)t*'aoption*('n,'a)t(** {2 Find operations} *)(** [find k m] returns the value [d] associated with key [k] in [m].
Raises [Not_found] if [k] is not bound in [m]. *)valfind:'nkey->('n,'a)t->'a(** [find_opt k m] returns [Some d] if [k] is bound to [d] in [m],
or [None] otherwise. *)valfind_opt:'nkey->('n,'a)t->'aoption(** [find_first f m] returns the first binding [(k, d)] such that
[f k d] is true, or raises [Not_found] if no such binding exists. *)valfind_first:('nkey->bool)->('n,'a)t->'nkey*'a(** [find_first_opt f m] returns [Some (k, d)] for the first binding
such that [f k d] is true, or [None] if no such binding exists. *)valfind_first_opt:('nkey->bool)->('n,'a)t->('nkey*'a)option(** [find_last f m] returns the last binding [(k, d)] such that
[f k d] is true, or raises [Not_found] if no such binding exists. *)valfind_last:('nkey->bool)->('n,'a)t->'nkey*'a(** [find_last_opt f m] returns [Some (k, d)] for the last binding
such that [f k d] is true, or [None] if no such binding exists. *)valfind_last_opt:('nkey->bool)->('n,'a)t->('nkey*'a)option(** {2 Mapping} *)(** [map f m] returns the map with the same keys as [m], where each
value [d] has been replaced by [f d]. *)valmap:('a->'b)->('n,'a)t->('n,'b)t(** [mapi f m] returns the map with the same keys as [m], where each
value has been replaced by [f k d] for the corresponding key [k]. *)valmapi:('nkey->'a->'b)->('n,'a)t->('n,'b)t(** {2 Sequences} *)(** [to_seq m] returns a sequence of all bindings in [m], in ascending
key order. *)valto_seq:('n,'a)t->('nkey*'a)Seq.t(** [to_rev_seq m] returns a sequence of all bindings in [m], in descending
key order. *)valto_rev_seq:('n,'a)t->('nkey*'a)Seq.t(** [to_seq_from k m] returns a sequence of all bindings in [m] with keys
greater than or equal to [k]. *)valto_seq_from:'nkey->('n,'a)t->('nkey*'a)Seq.t(** [add_seq s m] returns the map that is the union of [m] and all bindings
in sequence [s]. *)valadd_seq:('nkey*'a)Seq.t->('n,'a)t->('n,'a)t(** [of_seq s] returns the map containing all bindings from sequence [s]. *)valof_seq:('nkey*'a)Seq.t->('n,'a)tend