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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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.

Sourceval protect_ref : scope:(unit -> 'a) -> 'b ref -> 'a
Sourceval protect_state : freeze:(unit -> 'st) -> unfreeze:('st -> unit) -> scope:(unit -> 'a) -> 'a
Sourceval atomify : ('a -> 'b) -> 'a -> 'b
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