Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Record package and user qualifier support

view this post on Zulip Email Gateway (May 30 2024 at 14:08):

From: Nicolas Méric <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,

do you know if the record package supports names with user qualifiers?

With the following code, the "state" record is added to the theory:

theory Test_Record
  imports "HOL-Examples.Records"

begin

ML‹
val state_b = Binding.make ("state",  Position.none)

val state_attr_b = Binding.make ("a", Position.none)

val create_record = Record.add_record {overloaded=false} ([],state_b) NONE
                                      ((state_attr_b, \<^typ>‹int›,
Mixfix.NoSyn) |> single)
                               |> Theory.setup
›

end

But if I add a qualifier to the binding state_b, like this :

theory Test_Record
  imports "HOL-Examples.Records"

begin

ML‹
val state_b = Binding.make ("state",  Position.none)
                     |> Binding.qualify false "A"

val state_attr_b = Binding.make ("a", Position.none)

val create_record = Record.add_record {overloaded=false} ([],state_b) NONE
                                      ((state_attr_b, \<^typ>‹int›,
Mixfix.NoSyn) |> single)
                               |> Theory.setup
›

end

the definition fails with the following error:

Undeclared type constructor: "Test_Record.state.A.state_ext"
in declaration of constant "state_ext"
Failed to define record "A.state"

Is it a feature or a bug?

Best regards.

Nicolas Méric

view this post on Zulip Email Gateway (May 31 2024 at 09:12):

From: Thomas Sewell <tals4@cam.ac.uk>
Nicolas Méric
30/05/2024 15:08
qualify

Hi Nicolas.

That looks like a bug. Some of the record package depends on naming schemes, e.g. the relationship between a field name f and its related updator f_update and a record type name r and its related record extension constructor r_ext. Probably this is done incorrectly somewhere if you add a qualifier to the name via this part of the ML interface.

I seem to recall that the record package does work if you qualify everything by entering a local scope, however. I'm not sure if that's helpful.

If it's important to make this work for whatever you're doing, it might not be that difficult to fix things up. To my understanding, though, nobody has looked at the record package much in quite a while.

All the best,
Thomas.

Last updated: Jan 04 2025 at 20:18 UTC