Re: [isabelle] Looking for advice regarding typed abbreviation hackery



Dear Rafal,

However, if you only need to succeed in type checking lookup terms
when the second argument is given as a literal string, a similar
approach might work. Instead of looking at the type constraints, you
would have to match for term pattern

Const ("lookup", _) $ (_, <ML representation of "B ptr">) $ (Const
("Cons", _) $ (Const ("String.char.Char", _) $ ... ))

and replace this with a specialized constant lookup_B_y defined as

lookup_B_y p = (ptr_add p 4)::(A ptr)"

I'm a little bit lost as to which context the "you would have to match for" is in. Am I correct in thinking I need some syntax as well as a parse and print translation?

The approach is the same as the adhoc overloading facility by Christian Sternagel (in the current development version in ~~/src/Tools/Adhoc_Overloading). This mechanism adds the translation via Syntax.add_term_check to the type checking phase of terms (and similarly the inverse translation to the printing phase). For more information on this, see the thread on the mailing list starting with this post:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-May/msg00055.html

At this very point in the type checking phase, you'd have to replace the generic constant "lookup" with specialized versions like "lookup_B_y". To determine the right specialized version, you will need the type of the first parameter and the value of the second parameter of lookup. Determining the value of the second parameter could be done with pattern matching. I don't know exactly what the syntax tree looks like at this stage, but you should be able to find that out.

Sincerely,
Andreas






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