Stream: Beginner Questions

Topic: ✔ "Extracting" field names from records

pdc20 (Jan 22 2022 at 03:02):

Hi, new to zulip.

So let's say I have a record that looks like

record rec =
    a :: nat
    b :: int
    c :: string
    d :: nat set

I'd like to have the ability to generate a set that includes each field name if it is set to (SOME x. True). For example, let's say we have

⦇a=2,b=4,c=(SOME x. True),d=(SOME x. True)⦈

Then the set we would generate looks like {c,d}.
Unfortunately, I found that c and d actually have different types (rec ⇒ string and rec ⇒ nat set respectively). So now I'm wondering: is it possible to essentially extract the names of the fields such that they are not bounded to their codomain types so that I can put these names in the same set?

Florian Sextl (Jan 22 2022 at 10:45):

Would it be sufficient for you to get the field names as HOL strings or do you strictly require the field name bindings (i.e. the constant names of the selector functions)? Either way, I'd recommend to get the required information via some ML hack. The Record structure found in ~~/src/HOL/Tools/record.ML has e.g. the method get_recT_fields which would help extracting the fields from a record type.

Lukas Stevens (Jan 22 2022 at 10:49):

Also I think it would be more idiomatic to use undefined instead of SOME x. True.

pdc20 (Jan 22 2022 at 11:54):

Florian Sextl said:

Would it be sufficient for you to get the field names as HOL strings or do you strictly require the field name bindings (i.e. the constant names of the selector functions)? Either way, I'd recommend to get the required information via some ML hack. The Record structure found in ~~/src/HOL/Tools/record.ML has e.g. the method get_recT_field which would help extracting the fields from a record type.

Either strings or field name bindings would be nice, whichever is easier for now. For the ML hack, is there a way to do it without editing the original record.ML file?

pdc20 (Jan 22 2022 at 11:56):

Lukas Stevens said:

Also I think it would be more idiomatic to use undefined instead of SOME x. True.

I'm using (SOME x. True) to follow the style of a project I'm building on but thanks for the suggestion!

Florian Sextl (Jan 22 2022 at 12:08):

pdc20 said:

For the ML hack, is there a way to do it without editing the original record.ML file?

Yes, you can either write an own ML file and include it with the ML_filecommand or just have a ML block inside your theory file like this:

ML ‹  fun get_fields rec_trm = ... ›

You can then define an own command that registers a new term with the field name set, but for further questions I'd refer you to the Isabelle/ML cookbook and the #Isabelle/ML stream.

Notification Bot (Jan 24 2022 at 06:42):

pdc20 has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC