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



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 translation.

E.g. (p :: struct_s1 pptr) &-> ''z''
     becomes struct_s1_field_z :: "struct_s1 pptr => 32 word pptr"
     but
     (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>HOL.one_class.one", "_")
   : term
or
   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:
syntax
"_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?

Sincerely,

Rafal Kolanski.





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