[isabelle] Invoking parse translations for subterms inside my parse translation?
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Invoking parse translations for subterms inside my parse translation?
- From: Rafal Kolanski <rafalk at cse.unsw.edu.au>
- Date: Fri, 10 Dec 2010 15:06:48 +1100
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:18.104.22.168) Gecko/20101027 Thunderbird/3.1.6
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>HOL.one_class.one", "_")
Const ("_constrain", "_") $ Free ("p", "_") $
(Free ("pptr", "_") $ Free ("struct_s1", "_"))
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)
(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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and