why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-06-18T07:59:37Zhttps://gitlab.inria.fr/why3/why3/-/issues/99Simplification of array initializer for generated Why3 code2019-06-18T07:59:37ZDAILLER SylvainSimplification of array initializer for generated Why3 codeFor array initializer of Why3 automatically generated code, some simplifications can sometimes be done. This ticket is about writing a transformations to simplify these array initialization.
This is relevant to new_ide only (correspondin...For array initializer of Why3 automatically generated code, some simplifications can sometimes be done. This ticket is about writing a transformations to simplify these array initialization.
This is relevant to new_ide only (corresponding draft branch is array_initializer).DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/88Improve handling of premises2018-08-29T13:46:22ZGuillaume MelquiondImprove handling of premises1. Add a meta on top of the toplevel goals (`split_theory`? IDE?) for display purpose.
2. Systematically add a transformation node that performs `split` and `intro` on a VC (can be disabled by a configuration option).
3. Modify `split_go...1. Add a meta on top of the toplevel goals (`split_theory`? IDE?) for display purpose.
2. Systematically add a transformation node that performs `split` and `intro` on a VC (can be disabled by a configuration option).
3. Modify `split_goal` so that it splits the last labeled disjunction in the context.
4. Remove the implicit `introduce_premises` used for display purpose.https://gitlab.inria.fr/why3/why3/-/issues/79first_order_matching may instantiate matching variables using bound variables2018-02-02T10:06:21ZCLOCHARD Martinfirst_order_matching may instantiate matching variables using bound variablesThe routine first_order_matching within src/transform/reduction_engine.ml
does not contains any checks to prevent the unification of a matching variable
with a term containing a bound variable. As a consequence, we can prove false
in the...The routine first_order_matching within src/transform/reduction_engine.ml
does not contains any checks to prevent the unification of a matching variable
with a term containing a bound variable. As a consequence, we can prove false
in the following module (using transformation compute_specified to prove the
second goal):
```
module Soundness
use import int.Int
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z
meta rewrite lemma A
lemma Fail : p (fun x -> f0 x x x)
lemma Absurd : false
end
```
DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/34typing of transformation argument should not ignore coercion2017-11-17T09:25:39ZMARCHE Claudetyping of transformation argument should not ignore coercionIn a context like
```
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
goal g : ...
```
one should be able to something like
```
cut (3 = (4:byte))
```
Instead, we get:
Parsing error: This...In a context like
```
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
goal g : ...
```
one should be able to something like
```
cut (3 = (4:byte))
```
Instead, we get:
Parsing error: This term has type byte, but is expected to have type intDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/25Do not require the user to provide the labels in replace parameters2017-11-10T11:36:56ZRaphaël Rieu-HelftDo not require the user to provide the labels in replace parametersThe first parameter of the "replace" transformation is only matched if the user provides all the labels of the term to be replaced. Is this necessary ?The first parameter of the "replace" transformation is only matched if the user provides all the labels of the term to be replaced. Is this necessary ?DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/24Apply coercions in replace parameters2019-12-09T16:36:28ZRaphaël Rieu-HelftApply coercions in replace parametersCoercions are not applied to the parameters of the replace transformation, forcing the user to specify them (and to go look for the correct name if there are several coercions with the same name in the source).Coercions are not applied to the parameters of the replace transformation, forcing the user to specify them (and to go look for the correct name if there are several coercions with the same name in the source).https://gitlab.inria.fr/why3/why3/-/issues/23Add a revert transformation2017-12-20T13:30:45ZDAILLER SylvainAdd a revert transformationMake a general revert transformation.
"revert x" should transform a context:
Delta, x: t, Delta' |- G
into
Delta, x : t |- Delta' "->" G
with "->" meaning -> for hypotheses and forall quantification for symbols.
Eventually use this...Make a general revert transformation.
"revert x" should transform a context:
Delta, x: t, Delta' |- G
into
Delta, x : t |- Delta' "->" G
with "->" meaning -> for hypotheses and forall quantification for symbols.
Eventually use this revert for other transformations like induction, induction_pr etcDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/20recursive destruct2019-04-29T11:25:34ZDAILLER Sylvainrecursive destructCurrently, destruct only destruct the logic connector (/\, \/, =>) at the head of a formula. It could recursively be called on the generated new hypotheses.
This should be implemented as a new name or boolean parameter.Currently, destruct only destruct the logic connector (/\, \/, =>) at the head of a formula. It could recursively be called on the generated new hypotheses.
This should be implemented as a new name or boolean parameter.https://gitlab.inria.fr/why3/why3/-/issues/17Error in transformation remove2019-05-10T14:06:32ZDAILLER SylvainError in transformation removeThe error returned by remove should be improved. Instead of "ident not yet declared", it should print something like "cannot remove x since it appears in H".The error returned by remove should be improved. Instead of "ident not yet declared", it should print something like "cannot remove x since it appears in H".DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/14Add simpl2018-01-05T14:19:32ZDAILLER SylvainAdd simplAdd a transformation that does less reductions/rewriting than compute_in_goal. It should be similar to the Coq tactics simpl or red.Add a transformation that does less reductions/rewriting than compute_in_goal. It should be similar to the Coq tactics simpl or red.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/13Compute inside an hypothesis2018-01-05T14:19:50ZDAILLER SylvainCompute inside an hypothesisAdd a transformation having the same behavior as compute_in_goal for an hypothesis.Add a transformation having the same behavior as compute_in_goal for an hypothesis.DAILLER SylvainDAILLER Sylvain