diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
commit | 73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (patch) | |
tree | 259852cd3272f2f31a09d75ac24e31ec1aaa8d9e /lib/Impure/ocaml/ImpIOOracles.mli | |
parent | 3570ba2827908b280315c922ba7e43289f6d802a (diff) | |
parent | 035a1a9f4b636206acbae4506c5fc4ef322de0c1 (diff) | |
download | compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.tar.gz compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.zip |
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'lib/Impure/ocaml/ImpIOOracles.mli')
-rw-r--r-- | lib/Impure/ocaml/ImpIOOracles.mli | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/lib/Impure/ocaml/ImpIOOracles.mli b/lib/Impure/ocaml/ImpIOOracles.mli new file mode 100644 index 00000000..6064286a --- /dev/null +++ b/lib/Impure/ocaml/ImpIOOracles.mli @@ -0,0 +1,33 @@ +open ImpPrelude + + +(* +Memoized version of translation from int -> BinNums.positive. +The first arg is an indicative bound on the max int translated: +it pre-computes all positives lower or equal to this bound. +*) +val memo_int2pos: int -> int -> BinNums.positive + +val read_line: unit -> pstring + +val print: pstring -> unit + +val println: pstring -> unit + +val string_of_Z: BinNums.coq_Z -> pstring + +val timer : (('a -> 'b ) * 'a) -> 'b + +val new_exit_observer: (unit -> unit) -> (unit -> unit) ref + +val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit + +val exn2string: exn -> pstring + +val fail: pstring -> 'a + +exception ImpureFail of pstring;; + +val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a + +val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a |