https://github.com/EasyCrypt/easycrypt
Revision 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC, committed by Pierre-Yves Strub on 26 February 2018, 15:04:53 UTC
The elements of prover [...] have one of the following forms, where s
is a string:

s (add s to the use-only list)
+s (add include s to the include/exclude list)
-s (add exclude s to the include/exclude list)

The include/exclude list is ordered, so that later instructions can
supersede earlier ones. The use-only list was not ordered, but now
is. The relative order of the use-only and include/exclude lists
is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover
[+"Alt-Ergo" "Z3"] are equivalent.

The semantics is that the use-only list is first interpreted (if it's
empty, one starts with the current provers as the base), and only then
are the instructions of the include/exclude list applied to it, in
order.

There was already the special use-only instruction "ALL". Now, there is
also the use-only instruction "CLEAR", which clears the use-only list,
but may be superseded by the use-only instructions that follow.

Examples (assuming "Z3" and "Alt-Ergo" are only known provers):
prover []. (* a no-op *)
prover [+"Z3"]  (* adds just "Z3" to whatever current provers are *)
prover [-"Z3"]  (* removes just "Z3" from whatever current provers are *)
prover ["ALL"]  (* results in "Z3", "Alt-Ergo" *)
prover ["CLEAR"]  (* results in nothing *)
prover ["CLEAR" +"Z3"]  (* results in just "Z3" *)
prover [+"Z3" "CLEAR"]  (* results in just "Z3" *)
prover ["CLEAR" "Z3"]  (* result in just "Z3" *)
prover ["Z3" "CLEAR"]  (* results in nothing *)
prover [-"Z3" "ALL"]  (* results in "Alt-Ergo" *)
prover [+"Z3" "ALL" -"Z3"]  (* results in "Alt-Ergo" *)
prover [-"Z3" "ALL" +"Z3"]  (* results in "Z3", "Alt-Ergo" *)
1 parent 5115c89
History
Tip revision: 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC
Added clean way to clear the list of current provers.
Tip revision: 36f7f5a
File Mode Size
config
examples
lint
scripts
src
system
theories
.dir-locals.el -rw-r--r-- 285 bytes
.gitignore -rw-r--r-- 504 bytes
.merlin -rw-r--r-- 230 bytes
.travis.yml -rw-r--r-- 2.0 KB
COPYRIGHT -rw-r--r-- 581 bytes
COPYRIGHT.yaml -rw-r--r-- 596 bytes
MANIFEST -rw-r--r-- 690 bytes
Makefile -rw-r--r-- 5.0 KB
Makefile.system -rw-r--r-- 478 bytes
README.md -rw-r--r-- 6.1 KB
_tags -rw-r--r-- 791 bytes
myocamlbuild.ml -rw-r--r-- 2.3 KB

README.md

back to top