[isabelle] Looking for advice regarding typed abbreviation hackery



Dear Isabelle Gurus,

I'm trying to put together a representation of C structures using records, coupled with a memory model that involves pointers. There is an operation I'm trying to express elegantly, however, that is giving me quite a bit of trouble: dereference-and-get-address-of-field.

For example take these two C structures:
struct A {
  char z;
};
struct B {
  int x;
  struct A y;
};
These have correspondingly obvious isabelle record representations (with names prefixed to prevent collisions).

If we have some variable "sa" holding a pointer to a struct A in memory, then the dereference-and-get-address-of-field operator (denoted &->) should look something like this: sa&->''x''
representing the C code: &(sa->x)
This will add the structure offset of field "x" to the address contained in the pointer "sa" and retype it as a pointer to an int.

Doing the one-step case, as with "x" is possible using overloaded functions with a manual constraint on the return type, but what I really want is chaining, for example: sa&->y&->z should give a char pointer of z within struct A within struct B.

This is where I'm completely stuck. In my case, a "pointer" is just an address with a phantom type variable representing the type of value it points to. I have a function per record that given a string name of the field, gives its offset within the corresponding structure. I have a function that given a variable pointing to a structure of some type, returns the relevant lookup function. The problem is the return value, since it's type varies based on which field name one requests.

I am aware that this is probably not the neatest way to go about it. However, I really want to have a nice-looking textual representation for the user, and ugly details under the carpet if necessary to make that possible.

The generic problem boils down to (simplified pseudo-Isabelle):

consts (overloaded)
  get_lookup_table_for :: "'a itself => string => 'b"
consts (overloaded)
  -- "lookup table for structure A"
  lookup_A :: "'a ptr => string => 'b ptr"
  -- "lookup table for structure B"
  lookup_B :: "'a ptr => string => 'b ptr"
then define:
  "get_lookup_table_for TYPE(A) = lookup_A"
  "get_lookup_table_for TYPE(B) = lookup_B"
  "lookup_A p ''y'' = (ptr_add p 4)::(B ptr)"
  "lookup_B p ''z'' = (ptr_add p 0)::(char ptr)"

to finally get a function:
  "lookup p name = get_lookup_table_for (TYPE(p)) p name"
which can be chained like so:
  lookup (lookup sa ''y'') ''z''
and that should give something, which will either have the type "char ptr" inferred, or, if constrained to type "char ptr" can still be reasoned about.

I wish to avoid having to constrain the type returned by almost every single structure field lookup when annotating code.

As such, I welcome *any* method which will work, no matter how clunky. If it involves ML hackery, no problem.

Would any of you have some kind of recommendation for me? I saw some posts a while back about doing syntax translations pre and post type checking, but I'm unsure how to apply them to this situation seeing as I need the type of "sa" to be able to infer the type of the lookup result.

Sincerely hopeful,

Rafal Kolanski.





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