Email Gateway (Aug 18 2022 at 18:34): Email Gateway (Aug 18 2022 at 18:34):From: John Munroe <munddr@gmail.com>
Hi,
I'm trying to declare an attribute using
declare [[foo = 3]]
I have this ML code:
ML {*
Config.declare_global "foo" (K (Config.Int 2));
*}
But it complains about *** Unknown attribute: "foo". Is something else
needed for registering attributes?
Help will be appreciated. Thank you.
John
Email Gateway (Aug 18 2022 at 18:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,
The idiom I was taught by Makarius is
ML {*
val foo = Attrib.setup_config_int @{binding "foo"} (K 2);
*}
declare [[foo = 3]]
ML {*
Config.get @{context} foo;
*}
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 18:34):From: John Munroe <munddr@gmail.com>
Thanks. I can't seem to find Attrib.setup_config_int in Isabelle2011.
Assuming it's the same as Attrib.config_int, the following still gives
me an error:
ML {*
val foo = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
*}
declare [[foo = 3]]
John
Email Gateway (Aug 18 2022 at 18:34):From: Makarius <makarius@sketis.net>
On Sat, 22 Oct 2011, John Munroe wrote:
I can't seem to find Attrib.setup_config_int in Isabelle2011.
It is there in the current official release, which is Isabelle2011-1.
Assuming it's the same as Attrib.config_int, the following still gives
me an error:ML {*
val foo = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
*}declare [[foo = 3]]
The ML foo above is a pair (config, setup). The setup component needs to
be applied to the theory context using the 'setup' command in Isar.
Makarius
Email Gateway (Aug 18 2022 at 18:35):From: John Munroe <munddr@gmail.com>
Thanks. Can I try to imitate the setup_config_int function with:
ML {*
val (_,setup) = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
val _ = Context.>> (Context.map_theory setup)
val foo_raw = Config.declare_global "foo" (K (Config.Int 2));
val foo = Config.int foo_raw
*}
declare [[ foo = 3 ]]
But reading the attribute with
ML {*
val max_stuff_arty = Config.get_global @{theory} max_stuff_arity
*}
gives 2 rather than 3. Am I missing something here?
Thanks for the help.
John
Email Gateway (Aug 18 2022 at 18:35):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,
This declares the attribute "foo" twice, which is a bad idea. Try this (tested with Isabelle2011):
ML {*
val (foo, setup) = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
val _ = Context.>> (Context.map_theory setup)
*}
declare [[ foo = 3 ]]
ML {*
val max_stuff_arty = Config.get_global @{theory} foo
*}
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 18:35):From: Makarius <makarius@sketis.net>
Yes, you have dropped the actual foo value representing the config option
in ML, and defined a separate one that is not linked to the attribute name
space at all. The name suffixes "_global" and "_raw" that you have seen
in the Pure sources have been chosen to indicate that there is something
unusual -- normal user-space code is neither global nor raw.
This is how it works:
ML {* val (foo, foo_setup) = Attrib.config_int "foo" (K 2) *}
setup foo_setup
declare [[ foo = 3 ]]
ML {* Config.get @{context } foo *}
See also section "1.1.5 Configuration options" of the fine Isabelle/Isar
Implementation manual
http://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/implementation.pdf
It even includes some examples of the above kind.
Anyway, are you really stuck with old Isabelle2011? Isabelle2011-1 has
slightly better support for ML programming in the Isabelle/jEdit Prover
IDE than Isabelle2011 from 8 months ago.
Makarius
Last updated: Apr 30 2024 at 04:19 UTC