Re: [isabelle] parse translations

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.

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.


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