- 31 May, 2017 7 commits
-
-
Mário Pereira authored
-
Mário Pereira authored
-
Mário Pereira authored
-
Mário Pereira authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 30 May, 2017 1 commit
-
-
Mário Pereira authored
-
- 29 May, 2017 2 commits
-
-
Jean-Christophe Filliâtre authored
-
Mário Pereira authored
-
- 27 May, 2017 1 commit
-
-
Andrei Paskevich authored
The current syntax is "{| <term> |}", which is shorter than "pure { <term> }", and does not require a keyword. Better alternatives are welcome. As for type inference, we infer the type pf the term under Epure without binding destructible type variables in the program. In particular, let ghost fn x = {| x + 1 |} will not typecheck. Indeed, even if we detect that the result is [int], the type of the formal parameter [x[ is not inferred in the process, and thus stays at ['xi]. Another problem is related to the fact that variable and function namespaces are not yet separated when we perform type inference. Thus both fuctions let ghost fn (x: int) = let x a = a in {| x + 5 |} and let ghost fn (x: int) = let x a = a in {| x 5 |} will not typecheck, since the type of [x] is ['a -> 'a] when we infer the type for the Epure term, but it becomes [int], when we construct the final program expression. Probably, the only reasonable solution is to keep variables and functions in the same namespace, so that [x] simply can not be used in annotations after being redefined as a program function.
-
- 25 May, 2017 3 commits
-
-
Andrei Paskevich authored
We cannot split ite's and matches created in this way, and it is hard to control how much goes into them. Try for now to only convert bool-valued ite's.
-
Andrei Paskevich authored
Otherwise, fastWP gets splitted back to classical right away.
-
Andrei Paskevich authored
turns out, Alt-Ergo really dislikes unsplitted premises
-
- 24 May, 2017 6 commits
-
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-
Andrei Paskevich authored
Prevent introduce_premises from splitting too aggressively on the left-hand side: - under quantifiers: "forall x. P /\ Q" =/=> "(forall x. P) /\ (forall x. Q)" - match-with: "match t with A -> P | B -> Q" =/=> "(t = A -> P) /\ (t = B -> Q)" - if-then-else: "if f then P else Q" =/=> "(f -> P) /\ (not f -> Q)" - equivalence: "P <-> Q" =/=> "(P -> Q) /\ (Q -> P)" Those splits duplicate formulas, hinder readability and do not really simplify anything. Moreover, in case of a split under a quantifier, they create several universal premises for provers to instantiate, instead of just one. TODO: introduce_premises should be able to split under a single-branch match. However, this requires special treatment in Introduce.dequant, since the pattern should be rather skolemized than used as a condition.
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 23 May, 2017 8 commits
-
-
Mário Pereira authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
Let's see if this helps our provers to instantiate the axiom.
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
- 22 May, 2017 9 commits
-
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
Andrei Paskevich authored
Instead, we put a "stop_split" over the subsequent postcondition under the (begin > end + 1) assumption. When this assumption is unrealizable (strict for), this allows us to discharge the whole branch as a single goal.
-
-
MARCHE Claude authored
-
Andrei Paskevich authored
We will want to use stop_split higher in the VC formulas.
-
MARCHE Claude authored
Conflicts: examples/fibonacci.mlw examples/fibonacci/why3session.xml examples/fibonacci/why3shapes.gz examples/koda_ruskey/why3session.xml examples/koda_ruskey/why3shapes.gz examples/schorr_waite_via_recursion/why3session.xml examples/schorr_waite_via_recursion/why3shapes.gz examples/tests-provers/bv/why3session.xml examples/tests-provers/bv/why3shapes.gz examples/tests-provers/ieee_float/why3session.xml examples/tree_of_array/why3session.xml examples/tree_of_array/why3shapes.gz examples/vstte12_bfs/why3session.xml examples/vstte12_bfs/why3shapes.gz theories/int.why theories/real.why
-
MARCHE Claude authored
The underlying Monoid does not need to be commutative, and is indeed not in example fibonacci.mlw
-
Guillaume Melquiond authored
-
- 21 May, 2017 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-