Re: [isabelle] parse translations



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Makarius schrieb:
> On Fri, 14 Jan 2011, Matthias Schmalz wrote:
> 
>> 1. Consider the following contrieved parse translation translating
>> "foo x. t" to "(\<forall> x. t) \<and> (\<forall> x. t)":
>>
>> term "foo x. True"
>> (with show_types activated) I get
>> "(\<forall> x::'a. True) \<and> (\<forall> x::'b. True)".
>> (The two occurrences of x have different types.)
>>
>> Is it possible to change the parse translation so that
>> term "foo x. True"
>> yields "(\<forall> x::'a. True) \<and> (\<forall> x::'a. True)".
>> (The two occurrences of x have the same type.)
> 
> Not really, at least not at the raw parse tree level. Duplication of
> subtrees as above (and likewise comparison of subtrees for printing)
> looks suspicious.

That is good to know. So I will stop trying.

> Nonetheless, it should work by separating the concrete from the abstract
> syntax.  I.e. "foo" is like a regular binder, and there is an
> abbreviation for the rest. Abbreviations work by higher-order rewriting
> on fully-typed lambda terms.

The binder(s) I actually want to define has the following characteristics:
1. binds several variables (like \<forall>, \<exists>, set comprehension)
2. no simple recursive definition (like set comprehension, unlike
\<forall>, as \<forall> x xs. p == \<forall> x. \<forall> xs. p)
3. the right-hand side of the definition has an extra bound variable
(like set comprehension:
{t | xs. p} == {y. \<exists> xs. y = t \<and> p})
4. the right-hand side binds the bound variables of the left-hand side
several times such as in:
foo xs. p == (\<forall> xs. p) \<and> (\<exists> xs. p)

The multiple bound variables make it hard to work with abbreviations.
I will try to cook something up with overloading (to cope with the
arbitrary number of bound variables). If that does not work out, I will
define (on demand) several constants foo1, foo2, ..., one for each
number of bound variables.

Maybe somebody on the list can point to a running example of a binder
with the above properties? That would be helpful.

Anyway, thanks for the explanations,
Matthias

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNMyPfczhznXSdWggRAlcOAJ99BjR5aGRtjitF4CoPNY4bvIv5eQCeLZoe
/D5T7dSFzOeQlzXAEuswYxc=
=2xd+
-----END PGP SIGNATURE-----





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.