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

Dear Rafael,

struct A {
  char z;
struct B {
  int x;
  struct A y;
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.

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.
I think syntax translations during type checking might solve your problem. However, I feel that you need a more general framework than the one by Christian Sternagel. In his approach, the overloaded constant is replaced during type checking with another constant whose type is more specific. AFAIK this approach works as follows when it encounters an overloaded constant c during parsing:

1st) Determine the type constraints on c (from surrounding applications/type annotations etc.) 2nd) Check whether these constraints unify with one of the registered translations. If so, replace c appropriately.
3rd) After type checking, raise an error if c still occurs literally in the term.

Your problem looks a bit more difficult because the return type of the overloaded lookup constant not only depends on the arguments' types, but also on the value. For exmple, suppose that the type of sa is known as
"B ptr". What should be the type of "lookup sa x" in
"x = ''y'' | x = ''z'' --> lookup sa x = ..."?

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)"

If this solves your problem, there might be an even simpler solution: Make the field name parameter part of the lookup function name. Every struct declaration gets translated to a list of dereference functions. In your example:

definition lookup_A_z :: "A ptr => char ptr" ("_&->''''z''''")
where "lookup_A_z p == ptr_add p 0"

definition lookup_B_x :: "B ptr => int ptr" ("_&->''''x''''")
where "lookup_B_x p == ptr_add p 0"

definition lookup_B_y :: "B ptr => A ptr" ("_&->''''y''''")
where "lookup_B_y p == ptr_add p 4"

Then, "(p&->''y'')&->''z''" should type check and have type "char ptr", although I have not tested this yet.
Note that if you have multiple structs with the same field name, say

struct C { char x; }

you will get another definition

definition lookup_C_x :: "C ptr => char ptr" ("_&->''''x''''")
where "lookup_C_x == ptr_add p 0"

Now, "p&->''x''" will produce two parse trees, but in most cases, only one will be type correct. If this happens multiple times, parsing becomes increadibly slow because the number of parse trees grows exponentially. In that case, you can have an overloaded constant for every field name and use Christian Sternagel's solution. You only need to register translations for "_&->''x''" and "_&->''y''" etc.

Hope this helps,

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

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