[isabelle-dev] Method parsing, YXML and term construction.

[Christian Urban]

Thomas Sewell writes:
 > 
 > BTW, should I have known this already? Is there some part of the
 > documentation that I should have read, but have overlooked?

Sort of. Both functions are used in an example in the Programming 
Tutorial[*] on page 19. What the function check_term does is a bit 
more carefully described on page 52. But for the usage you have
in mind there is only a stub (since a long time ago) on page 92.
I just have not come around of writing this part yet. Help is of 
course very much appreciated. I think what you asked is a "common
idom" in Isabelle and there are bound to be others that will trip 
over this.

Christian


[*] http://isabelle.in.tum.de/nominal/activities/idp/

[isabelle-dev] Method parsing, YXML and term construction.

[Makarius]

On Tue, 9 Feb 2010, Thomas Sewell wrote:

> Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem 
> to be my friends.
>
> In fact, I sort of wish I'd known about them earlier. I remember in one 
> of the record package proofs it was annoying me that I had to construct 
> the types explicitly when it felt like I should be able to construct the 
> term skeleton and appeal to the type resolver. Now I know how.
>
> BTW, should I have known this already? Is there some part of the 
> documentation that I should have read, but have overlooked?

I've checked again: you would have had to be a very keen reader of NEWS, 
where it says for Isabelle2007 (not Isabelle2008 as I claimed):

* Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.)
and type checking (Syntax.check_term etc.), with common combinations
(Syntax.read_term etc.). These supersede former Sign.read_term etc.
which are considered legacy and await removal.

* Pure/Syntax: generic interfaces for type unchecking
(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
with common combinations (Syntax.pretty_term, Syntax.string_of_term
etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
available for convenience, but refer to the very same operations using
a mere theory instead of a full context.

The corresponding section in the Isar Implementation manual is this a 
dummy -- I've been close to touching it during my vacation last week.


These issues of parse/check and uncheck/unparse were once very hot in the 
discussion -- a discussion that was somehow too much localized, though.

Both those asking questions and those giving answers should develop a 
habit of making this a bit more public, i.e. on the isabelle-dev mailing 
list.


Makarius

[isabelle-dev] Method parsing, YXML and term construction.

[Thomas Sewell]

Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem
to be my friends.

In fact, I sort of wish I'd known about them earlier. I remember in one
of the record package proofs it was annoying me that I had to construct
the types explicitly when it felt like I should be able to construct the
term skeleton and appeal to the type resolver. Now I know how.

BTW, should I have known this already? Is there some part of the
documentation that I should have read, but have overlooked?

Yours,
 Thomas.

Makarius wrote:
> On Mon, 8 Feb 2010, Thomas Sewell wrote:
>
>   
>> Specifically, f is a polymorphic constant, x is a simple function 
>> application generated by our ML code, and y is supplied by the user and 
>> must be parsed. So far, our code has simply generated the string 
>> expression "f (x) (y)" and passed it to Syntax.read_term. Using the 
>> parser to get around type problems seems the ugly way through, however.
>> 
>
> Pasting strings together for consumption by the inner syntax engine was 
> never robust, and should never be done in production code.  (Likewise is 
> it a very bad idea to split output by the pretty printing engine, e.g. the 
> result of Syntax.string_of_term.)
>
> In Isabelle2008 we have introduced a clear separation of the raw parsing 
> and type-checking phases.  The Syntax.parse_term function is your friend 
> -- it will parse legal term fragments to produce a certain "preterm" 
> format that can be composed with other preterms and then given to 
> Syntax.check_term (or Syntax.check_terms for several simulataneous 
> operands).
>
>
>   
>> In upgrading to Isabelle-2009 everything got broken, because the input 
>> for y may be wrapped in YXML code to annotate it with position 
>> information, which results in "f (x) (y)" causing a malformed YXML error 
>> (it's a forest, not a tree).
>> 
>
> When introducing the YXML markup around outer syntax tokens that become 
> types/terms later, I was fully aware that any code that manipulates inner 
> syntax source will break.  This should be taken as an opportunity to 
> remove these things from your code.
>
>
>   Makarius
>   

[isabelle-dev] Method parsing, YXML and term construction.

[Makarius]

On Mon, 8 Feb 2010, Thomas Sewell wrote:

> Specifically, f is a polymorphic constant, x is a simple function 
> application generated by our ML code, and y is supplied by the user and 
> must be parsed. So far, our code has simply generated the string 
> expression "f (x) (y)" and passed it to Syntax.read_term. Using the 
> parser to get around type problems seems the ugly way through, however.

Pasting strings together for consumption by the inner syntax engine was 
never robust, and should never be done in production code.  (Likewise is 
it a very bad idea to split output by the pretty printing engine, e.g. the 
result of Syntax.string_of_term.)

In Isabelle2008 we have introduced a clear separation of the raw parsing 
and type-checking phases.  The Syntax.parse_term function is your friend 
-- it will parse legal term fragments to produce a certain "preterm" 
format that can be composed with other preterms and then given to 
Syntax.check_term (or Syntax.check_terms for several simulataneous 
operands).


> In upgrading to Isabelle-2009 everything got broken, because the input 
> for y may be wrapped in YXML code to annotate it with position 
> information, which results in "f (x) (y)" causing a malformed YXML error 
> (it's a forest, not a tree).

When introducing the YXML markup around outer syntax tokens that become 
types/terms later, I was fully aware that any code that manipulates inner 
syntax source will break.  This should be taken as an opportunity to 
remove these things from your code.


Makarius

[isabelle-dev] Method parsing, YXML and term construction.

[Thomas Sewell]

Hello to isabelle-dev.

Suppose some ML code I wrote has terms f, x and y. I'd like to be able 
to produce the function application "f x y" with the catch that f, x and 
y may all have type parameters that need to be adapted to each other. Is 
there any convenient facility for doing this in Isabelle at the 
term-manipulation level?

Specifically, f is a polymorphic constant, x is a simple function 
application generated by our ML code, and y is supplied by the user and 
must be parsed. So far, our code has simply generated the string 
expression "f (x) (y)" and passed it to Syntax.read_term. Using the 
parser to get around type problems seems the ugly way through, however.

In upgrading to Isabelle-2009 everything got broken, because the input 
for y may be wrapped in YXML code to annotate it with position 
information, which results in "f (x) (y)" causing a malformed YXML error 
(it's a forest, not a tree). Helpfully, isabelle strips the YXML 
annotations from the error message as it is printed, making it difficult 
to establish what the cause of the error is.

The simple workaround which I've implemented is to purge the YXML from y 
by passing it to YXML.parse and then flattening the XML tree down to 
only its Text elements. This gets the job done, but it seems like a good 
idea to look for an alternative approach. Assuming I instead construct f 
and x as terms in ML, and pass y to Syntax.read_term as intended, is 
there a helper API for specialising the resulting types so they apply to 
each other?

Yours,
Thomas.

[isabelle-dev] Method parsing, YXML and term construction.

[Florian Haftmann]

Hi Thomas,

Isabelle internalizes expressions in two steps:

(1) parse :: raw string (type string) -> raw term (type term)
(2) check :: raw term (type term) -> internalized term with types
inferred etc. (type term)

It seems to me that most things you want to do can be done using (2) only:

a) read your y using Syntax.read_term
b) assemble your f and x using datatype term, placing type inference
parameters wherever suitable using Type_Infer.param
c) put the term together
d) check it using Syntax.check_term.

Hope this helps,
Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: