Hello Abhishek,
The Why3 API for building terms, theories and proof tasks is designed to
forbid the construction of ill-typed terms. This includes a protection
against dangerous traps such as variable name capture. It means that you
can never assume that a logic variable is uniquely characterized by its
[string] name. The right "object" that represent a logic variable is the
type [vsymbol]. For example if you introduce twice a [vsymbol] with
accidentally the same name, such as
let var_x : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh "x")
Ty.ty_int
let another_var_x : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh
"x") Ty.ty_int
then these are effectively two distinct variable symbols. The string
identifier is there essentially only for printing variables. Notice that
if you print a term that contains both [var_x] and [another_varx]_, then
one of them will be renamed, typically to "x1".
Notice that, unlike what you said below, Ident.fresh *does not* rename
the variable, renaming only occurs at printing.
Incidentally, if you want to check if two objects of type [vsymbol] are
equal, use [Term.vs_equal] (see http://why3.lri.fr/api/Term.html)
This discipline for naming/scoping/typing variables is there to help you
to avoid mistakes (such as unexpected name capture) so use it!
Essentially, whenever you think about a logic variable, do not think
about a [string], think about a [vsymbol], everywhere.
If you are not able to cope with that discipline, then explain you
problem in more details please, maybe with Ocaml code excerpts.
- Claude
Le 06/04/2018 à 18:19, Abhishek Kumar a écrit :
Hello Claude
Thank you for your reply. The issue with the method described in the
tutorial is that the original vsymbol used in the construction of the
term is not in the scope in my case, which is the case for the
tutorial. I am not sure how to construct a vsymbol with the same name
as a given string for quantifying. The "Ident.fresh" creates a new
variable name (by suffixing 1,2..). Thus, given a name, I am unable to
get the corresponding vsymbol in a term to quantify over. In the
tutorial this problem doesn't arise because the original vsymbol is
still in the scope.
Is there a function to get a vsymbol from name (I could not find from
the API doc) given a term?
Thanks a lot, for your help!
Abhishek
On Thu, Apr 5, 2018 at 4:49 PM, Claude Marché <claude.mar...@inria.fr
<mailto:claude.mar...@inria.fr>> wrote:
Hello,
Did you try to carefully follow the section
http://why3.lri.fr/doc/api.html#sec30
<http://why3.lri.fr/doc/api.html#sec30> of the manual?
You cannot quantity over a variable using only the *string* name
of that
variable, you need to use the *vsymbol*
In other words, to build formula "forall x. t", you need to
introduce a
vsymbol say var_x of name "x", use it in the construction of the
term t,
and then call
Term.t_forall_close [var_x] t
- Claude
Le 04/04/2018 à 10:51, Abhishek Kumar a écrit :
> Hello
> I have to quantify over a variable in a term, but I only have
the term
> and the variable name (string). How can I create the corresponding
> vsymbol to pass to `t_forall_close`. Is there a function to get the
> vsymbol of a particular name in a term?
>
> eg.
> enclose (name: string) (t: Term) = (* returnns forall name : t *)
>
> Thanks a lot
> Abhishek
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
<mailto:Why3-club@lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
<https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
<mailto:Why3-club@lists.gforge.inria.fr>
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
<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
