Re: [isabelle] Invoking parse translations for subterms inside my parse translation? [SOLVED]

Dear All,

It turns out I was missing something simple. I finally tracked down a function called ProofContext.decode_term. It turns out that this function converts the "syntactic-style" term I've been having trouble with into one that can be passed to Syntax.check_term to get a properly typed term.

So, here's a "before" term:
 Const ("_constrain", "_") $ Free ("p", "_") $
   (Free ("pptr", "_") $ Free ("struct_s1", "_"))

(note that _constrain is not a constant)

and here it is after passing it through ProofContext.decode:
   Const ("_type_constraint_",
          "StructExample.struct_s1 TypedHeap.pptr
           ⇒ StructExample.struct_s1 TypedHeap.pptr") $
     Free ("p", "_")

Note that all constants are now identified by their proper names, so Syntax.check_term can deal with them.

Perhaps my discovery will be of service to someone else in the future.


Rafal Kolanski.

On 10/12/10 15:06, Rafal Kolanski wrote:
Dear Isabelle Gurus,

I am doing a tricky parse_translation where the term I substitute in
depends on the type of the left-hand-side term that gets passed into the

E.g. (p :: struct_s1 pptr) &-> ''z''
becomes struct_s1_field_z :: "struct_s1 pptr => 32 word pptr"
(p :: struct_s2 pptr) &-> ''x''
becomes struct_s2_field_x :: "struct_s2 pptr => struct_s1 pptr"

This means that in my parse_translation I need to type-check the LHS
term, and I'd also like to get at the string on the right-hand side.

I've got all the underlying infrastructure and examples working, but I
really, really need to invoke the parse translation mechanism for my LHS
subterm (to figure out the pointer type) and to be able to call
HOLogic.dest_string on my RHS.

Otherwise I get something like (for example):
Const ("\\<^const>Pointers.addr_add", "_") $ Free ("p", "_") $
Const ("\\<^const>", "_")
: term
Const ("_constrain", "_") $ Free ("p", "_") $
(Free ("pptr", "_") $ Free ("struct_s1", "_"))
: term

Needless to say, passing these to read_term won't work as they're not
strings, passing them to check_term will fail because those constants
aren't real constants (e.g. "_constrain" is not a constant).

So what do I pass them to such that it figures out the syntax and gives
me back a term I can either use or pass into check_term with dummy types?

My actual syntax is:
"_struct_get_field" :: "('v, 'p, 't) ptr_t ⇒ string ⇒ ('v, 'p, 't2) ptr_t"
(infixl "&→" 51)

I've been looking through the code for a few hours. I've also looked at
the "alternative" mechanism of Syntax.add_term_check, but I can't figure
out how to use it to do what I want. I don't think any documentation for
it exists. Perhaps someone's scribbled some notes on it?

As this relates to my PhD, which is on a tighter schedule than my other
work, I'd really appreciate hints towards a practical solution rather
than an elegant/generic one. I hope I'm just missing something obvious
rather than doing it all wrong.

Does anyone have any advice?


Rafal Kolanski.

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