Email Gateway (Aug 18 2022 at 16:39): Email Gateway (Aug 18 2022 at 16:39):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Email Gateway (Aug 18 2022 at 16:39):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Sincerely,
Rafal Kolanski.
Last updated: Apr 26 2024 at 16:20 UTC