GitLab

This reverts commit 838ed39a.

also compatible with Coq 8.4

Conflicts:
	CHANGES
	Version
	lib/coq/real/Trigonometry.v
	share/provers-detection-data.conf
	src/coq-tactic/why3tac.ml4
	src/transform/compute.ml
	src/transform/simplify_formula.ml

Andrei Paskevich authored Jan 10, 2016 and Guillaume Melquiond committed Feb 05, 2016

split the ppat_ghost field in program patterns into two distinct
conditions:
- ppat_ghost, indicating that the pattern starts as ghost,
  meaning that all variables in it are ghost, too;
- ppat_fail, meaning that the pattern contains a refutable
  ghost subpattern, which makes the match in the extracted code
  impossible, which makes the whole match expression ghost.

Until now, the two conditions were disjunctively combined, making
admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.

On N121-024 we fixed a bug where a state was incorrectly reused during
merge. The fix was to never reuse state when merging. This resulted in a
performance drop.

The new fix now marks states which should not be reused - basically
states that come from raise - and when such a state is present during
merging, we don't reuse. Otherwise, we reuse.  This seems to get us the
performance and passes all tests.

Marking is implemented simply by a flag in states

* mlw_wp.ml:
(mark) allows to set the marked flag of a state
(empty) empty state is not marked
(havoc) havoc doesn't change marked state
(merge_vars, merge_regs) new argument "marked", only create a new
  variable when marked is true, otherwise reuse
(fast_wp) in the case of Eraise, mark the used state

M415-042 pass labels down to conjunctions

Why3 parser groups the loop invariants into a single formula. This patch
allows to have the VC labels on every conjunct

mlw_wp.ml
(fastwp) call wp_expl instead of t_label