Re: [Why3-club] inlining functions or explicit predicates
Le 19/02/2019 à 16:02, Jean-Jacques Levy a écrit :
Dear Claude,
(* me again *) I did not notice the appset module.. oh so thanks, I’ll try to
use it. But seems to be many sets:
Fset, appset, impset….
See http://why3.lri.fr/stdlib/
set.Set: theory of mathematical sets
set.Fset: theory of finite mathematical sets
appset.AppSet: data structure for applicative finite sets, similar to
OCaml's Set.Make
impset.ImpSet: data structure for mutable finite sets, that could be
implemented in OCaml as ('a,unit) Hashtbl.t
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Dear Claude, (* me again *) I did not notice the appset module.. oh so thanks, I’ll try to use it. But seems to be many sets: Fset, appset, impset…. Thanks, -JJ- > Le 19 févr. 2019 à 15:50, Claude Marché a écrit : > > > Hello JJ, > > Short answer: with Why3 1.x you should use one of the modules appset.Appset > or impset.Impset to program with finite sets (depending on whether you want a > mutable data structure or not). More precisely you should clone one of these, > giving the value of type 'elt', in a very similar way as you would > instantiate the functor Set.Make in OCaml. > > Longer answer, of the previous mail too, should come soon... > > - Claude > > Le 19/02/2019 à 15:33, Jean-Jacques Levy a écrit : >> Dear Jean-Christophe + Friends, >> me again (* sorry *) .. a quick view about polymorphic equality: >> Equality in logic should be distinct from Equality in regular code, where >> the ghost attribute is prohibited. So if the problem with the ghost values >> is only about aggregated data with ghost components, we could still use >> ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too >> simple minded ? >> Cheers, -JJ- >> ___ >> Why3-club mailing list >> Why3-club@lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Hello JJ, Short answer: with Why3 1.x you should use one of the modules appset.Appset or impset.Impset to program with finite sets (depending on whether you want a mutable data structure or not). More precisely you should clone one of these, giving the value of type 'elt', in a very similar way as you would instantiate the functor Set.Make in OCaml. Longer answer, of the previous mail too, should come soon... - Claude Le 19/02/2019 à 15:33, Jean-Jacques Levy a écrit : Dear Jean-Christophe + Friends, me again (* sorry *) .. a quick view about polymorphic equality: Equality in logic should be distinct from Equality in regular code, where the ghost attribute is prohibited. So if the problem with the ghost values is only about aggregated data with ghost components, we could still use ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too simple minded ? Cheers, -JJ- ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Dear Jean-Christophe + Friends, me again (* sorry *) .. a quick view about polymorphic equality: Equality in logic should be distinct from Equality in regular code, where the ghost attribute is prohibited. So if the problem with the ghost values is only about aggregated data with ghost components, we could still use ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too simple minded ? Cheers, -JJ- ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Dear Jean-Christophe + Friends,
many many functions turned to be ghost functions in Why3.1.2.0. They can no
longer be used in regular code.. which means programs have to be rewritten with
effective implementations of many functions. Gosh !! where is abstraction ?
Why ‘add’, ‘remove’, ‘union’, ‘diff’ on sets are now only usable in logic ? All
this because of polymorphic equality ?? cannot believe it !! Is that problem
only because of equality of records with ghost fields ?
Is there not a finer analysis of ghost values to be done ?
Cheers, -JJ-
> Le 18 févr. 2019 à 15:46, Jean-Christophe Filliatre
> a écrit :
>
>
>> thanks for your answer. So you avoid inconsistent use of equality for
>> records with ghost fields by preventing its usage in regular code. (I
>> have still to understand the meaning of the ‘pure’ attribute).
>
> Basically, the "pure" construct lifts a logic term (or predicate) to the
> program level. But the result is always a ghost program, even if the
> term between the curly brackets of "pure" is 100% executable code.
> For instance, the following
>
> let f (x: int) : int
> = pure { 1 + 2 }
>
> will be rejected, with a message saying "Function f must be explicitly
> marked ghost".
>
>> But in my
>> case, ‘set_1000' was used in regular code, with mappings on an abstract
>> type, which I thnk you do not like too !! (since that abstract type
>> could be a record with ghost fields).
>
> When you are saying "abstract type", I guess you're referring to values
> of type 'a, a type variable of your function. If so, yes, you're right,
> that's the point: the type variable 'a could later be instantiated with
> a type that contains ghost fields.
>
> An abstract type (in the usual ML meaning) is rather a type for which no
> definition is provided, e.g.
>
> type t
>
> In that case, there is nothing wrong in stating the existence of a
> decidable equality:
>
> val (=) (x y: t) : bool ensures { result <-> x=y }
>
> Then you can use this equality in non-ghost programs, e.g.
>
> let f (a b: t) : int
> = if a = b then 1 else 2
>
>
>> Therefore :
>>
>> 1- I should use mappings on concrete scalar types (int, bool) [btw I
>> have also a strange error - see below with bool]
>
> Indeed. [and Julia already answered regarding the error you get]
>
>> 2- I cannot use the ’set’ function of the mappings library when my
>> ‘set_1000’ is used in regular code :-( !
>
> Yes. You have to provide you own, specific version of set. Or live with
> ghost programs only if you never intend to execute them (e.g. by
> extracting them to OCaml). Note that this is perfectly fine.
>
> We can state it otherwise: say you are using "set" to define "set_1000"
> and then you want to extract your program to OCaml to execute it. How
> should "set" be implemented?
>
>> ps/ similar problem with equality in why3.1.2.0 ?
>
> Do you mean a "similar solution to the same problem"? If so, yes.
>
> Please note that this is a non-trivial problem with ghost code (Andrei
> and I once discussed the matter with Rustan, who then figured out he had
> a similar trouble with Dafny), for which we have no simpler solution so far.
>
> You may find this annoying, but surely less annoying than using an
> unsound verification tool :-)
>
> --
> Jean-Christophe
>
>>
>> module BBB
>>
>> use int.Int
>> use list.List
>>
>> type abc = bool
>>
>> let rec split (x : abc) (s: list abc) : (list abc, list abc) =
>> variant {s}
>> match s with
>> | Nil -> (Nil, Nil)
>> | Cons y s' -> if x = y then (Cons x Nil, s') else
>> let (s1', s2) = split x s' in
>>((Cons y s1'), s2)
>> end
>>
>> end
>>
>> hos $ why3 execute bbb.mlw
>> File "bbb.mlw", line 12, characters 20-21:
>> This expression has type bool, but is expected to have type int
>>
>>
>>> Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre
>>> >> > a écrit :
>>>
>>> Dear Jean-Jacques,
>>>
>>> You are making use of a ghost function to define set_1000, namely
>>> function ([<-]) from library map.Map. Consequently, your function
>>> set_1000 must be declared ghost. You can do this by inserting the
>>> "ghost" keyword immediately after "let rec":
>>>
>>> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>>> ...
>>>
>>> Now why3 is going to complain that you must prove termination of
>>> function set_1000, as ghost code must terminate. Here, this is easy, as
>>> parameter "s" decreases:
>>>
>>> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>>> variant { s }
>>> ...
>>>
>>> The definition is now accepted.
>>>
>>> You may wonder why function ([<-]) was declared ghost in the first
>>> place. This is because polymorphic equality is hidden behind this
>>> function. Function ([<-]) is actually syntactic sugar for this function
>>>
>>> let ghost function set (f: map 'a 'b) (x:
Re: [Why3-club] inlining functions or explicit predicates
> thanks for your answer. So you avoid inconsistent use of equality for
> records with ghost fields by preventing its usage in regular code. (I
> have still to understand the meaning of the ‘pure’ attribute).
Basically, the "pure" construct lifts a logic term (or predicate) to the
program level. But the result is always a ghost program, even if the
term between the curly brackets of "pure" is 100% executable code.
For instance, the following
let f (x: int) : int
= pure { 1 + 2 }
will be rejected, with a message saying "Function f must be explicitly
marked ghost".
> But in my
> case, ‘set_1000' was used in regular code, with mappings on an abstract
> type, which I thnk you do not like too !! (since that abstract type
> could be a record with ghost fields).
When you are saying "abstract type", I guess you're referring to values
of type 'a, a type variable of your function. If so, yes, you're right,
that's the point: the type variable 'a could later be instantiated with
a type that contains ghost fields.
An abstract type (in the usual ML meaning) is rather a type for which no
definition is provided, e.g.
type t
In that case, there is nothing wrong in stating the existence of a
decidable equality:
val (=) (x y: t) : bool ensures { result <-> x=y }
Then you can use this equality in non-ghost programs, e.g.
let f (a b: t) : int
= if a = b then 1 else 2
> Therefore :
>
> 1- I should use mappings on concrete scalar types (int, bool) [btw I
> have also a strange error - see below with bool]
Indeed. [and Julia already answered regarding the error you get]
> 2- I cannot use the ’set’ function of the mappings library when my
> ‘set_1000’ is used in regular code :-( !
Yes. You have to provide you own, specific version of set. Or live with
ghost programs only if you never intend to execute them (e.g. by
extracting them to OCaml). Note that this is perfectly fine.
We can state it otherwise: say you are using "set" to define "set_1000"
and then you want to extract your program to OCaml to execute it. How
should "set" be implemented?
> ps/ similar problem with equality in why3.1.2.0 ?
Do you mean a "similar solution to the same problem"? If so, yes.
Please note that this is a non-trivial problem with ghost code (Andrei
and I once discussed the matter with Rustan, who then figured out he had
a similar trouble with Dafny), for which we have no simpler solution so far.
You may find this annoying, but surely less annoying than using an
unsound verification tool :-)
--
Jean-Christophe
>
> module BBB
>
> use int.Int
> use list.List
>
> type abc = bool
>
> let rec split (x : abc) (s: list abc) : (list abc, list abc) =
> variant {s}
> match s with
> | Nil -> (Nil, Nil)
> | Cons y s' -> if x = y then (Cons x Nil, s') else
> let (s1', s2) = split x s' in
> ((Cons y s1'), s2)
> end
>
> end
>
> hos $ why3 execute bbb.mlw
> File "bbb.mlw", line 12, characters 20-21:
> This expression has type bool, but is expected to have type int
>
>
>> Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre
>> > > a écrit :
>>
>> Dear Jean-Jacques,
>>
>> You are making use of a ghost function to define set_1000, namely
>> function ([<-]) from library map.Map. Consequently, your function
>> set_1000 must be declared ghost. You can do this by inserting the
>> "ghost" keyword immediately after "let rec":
>>
>> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>> ...
>>
>> Now why3 is going to complain that you must prove termination of
>> function set_1000, as ghost code must terminate. Here, this is easy, as
>> parameter "s" decreases:
>>
>> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>> variant { s }
>> ...
>>
>> The definition is now accepted.
>>
>> You may wonder why function ([<-]) was declared ghost in the first
>> place. This is because polymorphic equality is hidden behind this
>> function. Function ([<-]) is actually syntactic sugar for this function
>>
>> let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
>> fun y -> if pure {y = x} then v else f y
>>
>> where you can see that polymorphic equality is used to compare y and x.
>> Since we don't know how to provide a polymorphic equality in programs
>> (think of the comparison of records with possible ghost fields that
>> would be erased at runtime), we have no other choice than forbidding its
>> use in regular (i.e. non-ghost) code.
>>
>> As for your question "where to insert the ghost keyword", you can find
>> the answer on page 87 in the PDF manual, Fig. 6.5.
>> http://why3.lri.fr/manual.pdf
>>
>> Cheers
>> --
>> Jean-Christophe
>>
>> On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
>>> Dear Claude,
>>>
>>> thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
>>> (couldn’t find opam upgrade to
Re: [Why3-club] inlining functions or explicit predicates
On Mon, 18 Feb 2019, Jean-Jacques Levy wrote:
> Dear Jean-Christophe and Friends,
> thanks for your answer. So you avoid inconsistent use of equality for records
> with ghost fields by preventing its usage in regular code. (I have still to
> understand the meaning of the ‘pure’ attribute). But in my case, ‘set_1000'
> was
> used in regular code, with mappings on an abstract type, which I thnk you do
> not like too !! (since that abstract type could be a record with ghost
> fields).
>
> Therefore :
>
> 1- I should use mappings on concrete scalar types (int, bool) [btw I have
> also a strange error - see below with bool]
>
> 2- I cannot use the ’set’ function of the mappings library when my ‘set_1000’
> is used in regular code :-( !
>
> Cheers, -JJ-
>
> ps/ similar problem with equality in why3.1.2.0 ?
>
> module BBB
>
> use int.Int
> use list.List
>
> type abc = bool
>
> let rec split (x : abc) (s: list abc) : (list abc, list abc) =
> variant {s}
> match s with
> | Nil -> (Nil, Nil)
> | Cons y s' -> if x = y then (Cons x Nil, s') else
> let (s1', s2) = split x s' in
> ((Cons y s1'), s2)
> end
>
> end
>
> hos $ why3 execute bbb.mlw
> File "bbb.mlw", line 12, characters 20-21:
> This expression has type bool, but is expected to have type int
In code, = is only defined on int. So you would need:
val (=) (x y : abc) : bool ensures { result <-> x=y }
julia
>
>
> Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre
> a écrit :
>
> Dear Jean-Jacques,
>
> You are making use of a ghost function to define set_1000, namely
> function ([<-]) from library map.Map. Consequently, your function
> set_1000 must be declared ghost. You can do this by inserting the
> "ghost" keyword immediately after "let rec":
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
> ...
>
> Now why3 is going to complain that you must prove termination of
> function set_1000, as ghost code must terminate. Here, this is easy, as
> parameter "s" decreases:
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
> variant { s }
> ...
>
> The definition is now accepted.
>
> You may wonder why function ([<-]) was declared ghost in the first
> place. This is because polymorphic equality is hidden behind this
> function. Function ([<-]) is actually syntactic sugar for this function
>
> let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
> fun y -> if pure {y = x} then v else f y
>
> where you can see that polymorphic equality is used to compare y and x.
> Since we don't know how to provide a polymorphic equality in programs
> (think of the comparison of records with possible ghost fields that
> would be erased at runtime), we have no other choice than forbidding its
> use in regular (i.e. non-ghost) code.
>
> As for your question "where to insert the ghost keyword", you can find
> the answer on page 87 in the PDF manual, Fig. 6.5.
> http://why3.lri.fr/manual.pdf
>
> Cheers
> --
> Jean-Christophe
>
> On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
> Dear Claude,
>
> thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
> (couldn’t find opam upgrade to 1.2.0!)
>
> Now I’m facing a new problem with strange ‘ghost’ error.
> -
> module AAA
>
> use list.List
> use map.Map
>
> let rec set_1000 (s : list 'a)(f : map 'a int) =
> match s with
> | Nil -> f
> | Cons x s' -> (set_1000 s' f)[x <- 1000]
> end
>
> end
> -
> why3 execute aaa.mlw
> File "aaa.mlw", line 6, characters 8-16:
> Function set_1000 must be explicitly marked ghost
> -
> So why that message + where to insert the ghost keyword (couldn’t
> find!) ??
>
> Cheers, -JJ-
>
> Le 15 févr. 2019 à 17:08, Claude Marche > a écrit :
>
>
> Dear JJ,
>
> As you remark, Why3 0.88 is now quite outdated and my answer may
> not
> be very accurate. As far as I remember, the former "Inline"
> button was
> applying the transformation "inline_goal" which has the effect of
> inlining the defined function symbols appearing in an outermost
> position in the goal.
>
> The doc for the transformations are obtained when typing `why3
> --list-transforms', and some of them are documented in a bit more
> details in the manual : "inline_*" are documented at the
> beginning of
> http://why3.lri.fr/doc/technical.html#sec128
>
> In Why3 1.x, the user interface for applying transformations is
> much
> more powerful, in your case you would probably want to type
> "unfold
> foo" where "foo" is your
Re: [Why3-club] inlining functions or explicit predicates
Dear Jean-Christophe and Friends,
thanks for your answer. So you avoid inconsistent use of equality for records
with ghost fields by preventing its usage in regular code. (I have still to
understand the meaning of the ‘pure’ attribute). But in my case, ‘set_1000' was
used in regular code, with mappings on an abstract type, which I thnk you do
not like too !! (since that abstract type could be a record with ghost fields).
Therefore :
1- I should use mappings on concrete scalar types (int, bool) [btw I have also
a strange error - see below with bool]
2- I cannot use the ’set’ function of the mappings library when my ‘set_1000’
is used in regular code :-( !
Cheers, -JJ-
ps/ similar problem with equality in why3.1.2.0 ?
module BBB
use int.Int
use list.List
type abc = bool
let rec split (x : abc) (s: list abc) : (list abc, list abc) =
variant {s}
match s with
| Nil -> (Nil, Nil)
| Cons y s' -> if x = y then (Cons x Nil, s') else
let (s1', s2) = split x s' in
((Cons y s1'), s2)
end
end
hos $ why3 execute bbb.mlw
File "bbb.mlw", line 12, characters 20-21:
This expression has type bool, but is expected to have type int
> Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre
> a écrit :
>
> Dear Jean-Jacques,
>
> You are making use of a ghost function to define set_1000, namely
> function ([<-]) from library map.Map. Consequently, your function
> set_1000 must be declared ghost. You can do this by inserting the
> "ghost" keyword immediately after "let rec":
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>...
>
> Now why3 is going to complain that you must prove termination of
> function set_1000, as ghost code must terminate. Here, this is easy, as
> parameter "s" decreases:
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>variant { s }
>...
>
> The definition is now accepted.
>
> You may wonder why function ([<-]) was declared ghost in the first
> place. This is because polymorphic equality is hidden behind this
> function. Function ([<-]) is actually syntactic sugar for this function
>
> let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
>fun y -> if pure {y = x} then v else f y
>
> where you can see that polymorphic equality is used to compare y and x.
> Since we don't know how to provide a polymorphic equality in programs
> (think of the comparison of records with possible ghost fields that
> would be erased at runtime), we have no other choice than forbidding its
> use in regular (i.e. non-ghost) code.
>
> As for your question "where to insert the ghost keyword", you can find
> the answer on page 87 in the PDF manual, Fig. 6.5.
> http://why3.lri.fr/manual.pdf
>
> Cheers
> --
> Jean-Christophe
>
> On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
>> Dear Claude,
>>
>> thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
>> (couldn’t find opam upgrade to 1.2.0!)
>>
>> Now I’m facing a new problem with strange ‘ghost’ error.
>> -
>> module AAA
>>
>> use list.List
>> use map.Map
>>
>> let rec set_1000 (s : list 'a)(f : map 'a int) =
>> match s with
>> | Nil -> f
>> | Cons x s' -> (set_1000 s' f)[x <- 1000]
>> end
>>
>> end
>> -
>> why3 execute aaa.mlw
>> File "aaa.mlw", line 6, characters 8-16:
>> Function set_1000 must be explicitly marked ghost
>> -
>> So why that message + where to insert the ghost keyword (couldn’t find!) ??
>>
>> Cheers, -JJ-
>>
>>> Le 15 févr. 2019 à 17:08, Claude Marche >> > a écrit :
>>>
>>>
>>> Dear JJ,
>>>
>>> As you remark, Why3 0.88 is now quite outdated and my answer may not
>>> be very accurate. As far as I remember, the former "Inline" button was
>>> applying the transformation "inline_goal" which has the effect of
>>> inlining the defined function symbols appearing in an outermost
>>> position in the goal.
>>>
>>> The doc for the transformations are obtained when typing `why3
>>> --list-transforms', and some of them are documented in a bit more
>>> details in the manual : "inline_*" are documented at the beginning of
>>> http://why3.lri.fr/doc/technical.html#sec128
>>>
>>> In Why3 1.x, the user interface for applying transformations is much
>>> more powerful, in your case you would probably want to type "unfold
>>> foo" where "foo" is your function symbol. The documentation is also
>>> visible interactively.
>>>
>>> I don't know how to help more without seeing the exact example you have.
>>>
>>> - Claude
>>>
>>>
>>>
>>> Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit :
Dear Why3 Friends,
is there any doc about the functionality of the "Inline" button in
the Why3 IDE ?
Same for inline_all, inline_goal, inline_trivial..
My current problem is that the inlined version of a trivial function
Re: [Why3-club] inlining functions or explicit predicates
Dear Jean-Jacques,
You are making use of a ghost function to define set_1000, namely
function ([<-]) from library map.Map. Consequently, your function
set_1000 must be declared ghost. You can do this by inserting the
"ghost" keyword immediately after "let rec":
let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
...
Now why3 is going to complain that you must prove termination of
function set_1000, as ghost code must terminate. Here, this is easy, as
parameter "s" decreases:
let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
variant { s }
...
The definition is now accepted.
You may wonder why function ([<-]) was declared ghost in the first
place. This is because polymorphic equality is hidden behind this
function. Function ([<-]) is actually syntactic sugar for this function
let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
fun y -> if pure {y = x} then v else f y
where you can see that polymorphic equality is used to compare y and x.
Since we don't know how to provide a polymorphic equality in programs
(think of the comparison of records with possible ghost fields that
would be erased at runtime), we have no other choice than forbidding its
use in regular (i.e. non-ghost) code.
As for your question "where to insert the ghost keyword", you can find
the answer on page 87 in the PDF manual, Fig. 6.5.
http://why3.lri.fr/manual.pdf
Cheers
--
Jean-Christophe
On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
> Dear Claude,
>
> thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
> (couldn’t find opam upgrade to 1.2.0!)
>
> Now I’m facing a new problem with strange ‘ghost’ error.
> -
> module AAA
>
> use list.List
> use map.Map
>
> let rec set_1000 (s : list 'a)(f : map 'a int) =
> match s with
> | Nil -> f
> | Cons x s' -> (set_1000 s' f)[x <- 1000]
> end
>
> end
> -
> why3 execute aaa.mlw
> File "aaa.mlw", line 6, characters 8-16:
> Function set_1000 must be explicitly marked ghost
> -
> So why that message + where to insert the ghost keyword (couldn’t find!) ??
>
> Cheers, -JJ-
>
>> Le 15 févr. 2019 à 17:08, Claude Marche > > a écrit :
>>
>>
>> Dear JJ,
>>
>> As you remark, Why3 0.88 is now quite outdated and my answer may not
>> be very accurate. As far as I remember, the former "Inline" button was
>> applying the transformation "inline_goal" which has the effect of
>> inlining the defined function symbols appearing in an outermost
>> position in the goal.
>>
>> The doc for the transformations are obtained when typing `why3
>> --list-transforms', and some of them are documented in a bit more
>> details in the manual : "inline_*" are documented at the beginning of
>> http://why3.lri.fr/doc/technical.html#sec128
>>
>> In Why3 1.x, the user interface for applying transformations is much
>> more powerful, in your case you would probably want to type "unfold
>> foo" where "foo" is your function symbol. The documentation is also
>> visible interactively.
>>
>> I don't know how to help more without seeing the exact example you have.
>>
>> - Claude
>>
>>
>>
>> Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit :
>>> Dear Why3 Friends,
>>> is there any doc about the functionality of the "Inline" button in
>>> the Why3 IDE ?
>>> Same for inline_all, inline_goal, inline_trivial..
>>> My current problem is that the inlined version of a trivial function
>>> works with automatic provers, but I cannot find a way of forcing that
>>> inlining.
>>> Many many thanks for you help!
>>> -JJ-
>>> ps/ I’m using old release 0.88.3 :-(
>>> ___
>>> Why3-club mailing list
>>> Why3-club@lists.gforge.inria.fr
>>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Dear Claude, thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1. (couldn’t find opam upgrade to 1.2.0!) Now I’m facing a new problem with strange ‘ghost’ error. - module AAA use list.List use map.Map let rec set_1000 (s : list 'a)(f : map 'a int) = match s with | Nil -> f | Cons x s' -> (set_1000 s' f)[x <- 1000] end end - why3 execute aaa.mlw File "aaa.mlw", line 6, characters 8-16: Function set_1000 must be explicitly marked ghost - So why that message + where to insert the ghost keyword (couldn’t find!) ?? Cheers, -JJ- > Le 15 févr. 2019 à 17:08, Claude Marche a écrit : > > > Dear JJ, > > As you remark, Why3 0.88 is now quite outdated and my answer may not be very > accurate. As far as I remember, the former "Inline" button was applying the > transformation "inline_goal" which has the effect of inlining the defined > function symbols appearing in an outermost position in the goal. > > The doc for the transformations are obtained when typing `why3 > --list-transforms', and some of them are documented in a bit more details in > the manual : "inline_*" are documented at the beginning of > http://why3.lri.fr/doc/technical.html#sec128 > > In Why3 1.x, the user interface for applying transformations is much more > powerful, in your case you would probably want to type "unfold foo" where > "foo" is your function symbol. The documentation is also visible > interactively. > > I don't know how to help more without seeing the exact example you have. > > - Claude > > > > Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit : >> Dear Why3 Friends, >> is there any doc about the functionality of the "Inline" button in the >> Why3 IDE ? >> Same for inline_all, inline_goal, inline_trivial.. >> My current problem is that the inlined version of a trivial function works >> with automatic provers, but I cannot find a way of forcing that inlining. >> Many many thanks for you help! >> -JJ- >> ps/ I’m using old release 0.88.3 :-( >> ___ >> Why3-club mailing list >> Why3-club@lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
Dear JJ, As you remark, Why3 0.88 is now quite outdated and my answer may not be very accurate. As far as I remember, the former "Inline" button was applying the transformation "inline_goal" which has the effect of inlining the defined function symbols appearing in an outermost position in the goal. The doc for the transformations are obtained when typing `why3 --list-transforms', and some of them are documented in a bit more details in the manual : "inline_*" are documented at the beginning of http://why3.lri.fr/doc/technical.html#sec128 In Why3 1.x, the user interface for applying transformations is much more powerful, in your case you would probably want to type "unfold foo" where "foo" is your function symbol. The documentation is also visible interactively. I don't know how to help more without seeing the exact example you have. - Claude Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit : Dear Why3 Friends, is there any doc about the functionality of the "Inline" button in the Why3 IDE ? Same for inline_all, inline_goal, inline_trivial.. My current problem is that the inlined version of a trivial function works with automatic provers, but I cannot find a way of forcing that inlining. Many many thanks for you help! -JJ- ps/ I’m using old release 0.88.3 :-( ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] inlining functions or explicit predicates
Dear Why3 Friends, is there any doc about the functionality of the "Inline" button in the Why3 IDE ? Same for inline_all, inline_goal, inline_trivial.. My current problem is that the inlined version of a trivial function works with automatic provers, but I cannot find a way of forcing that inlining. Many many thanks for you help! -JJ- ps/ I’m using old release 0.88.3 :-( ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
