package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (4)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

doc/rocq-runtime.lib/Util/index.html

Module UtilSource

This module contains numerous utility functions on strings, lists, arrays, etc.

Mapping under pairs

Sourceval on_fst : ('a -> 'b) -> ('a * 'c) -> 'b * 'c
Sourceval on_snd : ('a -> 'b) -> ('c * 'a) -> 'c * 'b
Sourceval map_pair : ('a -> 'b) -> ('a * 'a) -> 'b * 'b

Folding under pairs

Sourceval fold_fst : ('c -> 'a -> 'c * 'a) -> 'c -> ('a * 'b) -> 'c * ('a * 'b)
Sourceval fold_snd : ('c -> 'b -> 'c * 'b) -> 'c -> ('a * 'b) -> 'c * ('a * 'b)

Equality on pairs

Sourceval eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b) -> ('a * 'b) -> bool

Mapping under triplets

Sourceval on_pi1 : ('a -> 'b) -> ('a * 'c * 'd) -> 'b * 'c * 'd
Sourceval on_pi2 : ('a -> 'b) -> ('c * 'a * 'd) -> 'c * 'b * 'd
Sourceval on_pi3 : ('a -> 'b) -> ('c * 'd * 'a) -> 'c * 'd * 'b
Projections from triplets
Sourceval pi1 : ('a * 'b * 'c) -> 'a
Sourceval pi2 : ('a * 'b * 'c) -> 'b
Sourceval pi3 : ('a * 'b * 'c) -> 'c
Chars.
Sourceval is_letter : char -> bool
Sourceval is_digit : char -> bool
Sourceval is_ident_tail : char -> bool
Sourceval is_blank : char -> bool
Empty type
Sourcemodule Empty : sig ... end
Strings.
Sourcemodule String = CString
Sourceval subst_command_placeholder : string -> string -> string

Substitute %s in the first chain by the second chain

Lists.
Sourcemodule List = CList
Sourceval (@) : 'a list -> 'a list -> 'a list
Arrays.
Sourcemodule Array = CArray
Sets.
Sourcemodule Set = CSet
Maps.
Sourcemodule Map = CMap
Matrices.
Sourceval matrix_transpose : 'a list list -> 'a list list
Functions.
Sourceval identity : 'a -> 'a
Sourceval (%>) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

Left-to-right function composition:

f1 %> f2 is fun x -> f2 (f1 x).

f1 %> f2 %> f3 is fun x -> f3 (f2 (f1 x)).

f1 %> f2 %> f3 %> f4 is fun x -> f4 (f3 (f2 (f1 x)))

etc.

Sourceval const : 'a -> 'b -> 'a
Sourceval iterate : ('a -> 'a) -> int -> 'a -> 'a
Sourceval repeat : int -> ('a -> unit) -> 'a -> unit
Sourceval app_opt : ('a -> 'a) option -> 'a -> 'a
Delayed computations.
Sourcetype 'a delayed = unit -> 'a
Sourceval delayed_force : 'a delayed -> 'a
Sourceval try_finally : ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b

try_finally f x g y applies the main code f to x and returns the result after having applied the finalization code g to y. If the main code raises the exception exn, the finalization code is executed and exn is raised. If the finalization code itself fails, the exception returned is always the one from the finalization code. Credit X.Leroy, D.Remy.

Enriched exceptions
Sourcetype iexn = Exninfo.iexn
  • deprecated (8.12) please use [Exninfo.iexn]
Sourceval iraise : Exninfo.iexn -> 'a
  • deprecated (8.12) please use [Exninfo.iraise]
Misc.
Sourcetype ('a, 'b) union = ('a, 'b) CSig.union =
  1. | Inl of 'a
  2. | Inr of 'b
    (*

    Union type

    *)
Sourcemodule Union : sig ... end
Sourceval map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union

Alias for Union.map

Sourcetype 'a until = 'a CSig.until =
  1. | Stop of 'a
  2. | Cont of 'a
    (*

    Used for browsable-until structures.

    *)
Sourcetype ('a, 'b) eq = ('a, 'b) CSig.eq =
  1. | Refl : ('a, 'a) eq
Sourceval sym : ('a, 'b) eq -> ('b, 'a) eq
Sourcemodule Compare : sig ... end

Helpers to write comparison functions

Sourceval open_utf8_file_in : string -> in_channel

Open an utf-8 encoded file and skip the byte-order mark if any.

Sourceval set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a)

A trick which can typically be used to store on the fly the computation of values in the "when" clause of a "match" then retrieve the evaluated result in the r.h.s of the clause