blob: 2b19d14a304aee8d4a3e717f9e4aaeab3b640d1f (
plain)
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
|
# `Impure`: importing OCaml functions as non-deterministic ones.
The principle of this library is to encode the type `A -> B` of an
OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type
of an axiomatized monad that can be interpreted as `B -> Prop`. In
other word, this encoding abstracts an OCaml function as a function
returning a postcondition on its possible results (ie a relation between its
parameter and its result). Side-effects are simply ignored. And
reasoning on such a function is only possible in partial correctness.
See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo).
## Credits
[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr).
## Code Overview
- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms.
- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction.
- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style).
- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles.
- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles.
[ImpExtern](ImpExtern.v) exports all these impure operators.
- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles.
|
