Email Gateway (Aug 18 2022 at 19:17): Email Gateway (Aug 18 2022 at 19:17):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Hi all,
I want to define an attribute, that takes a string as an argument
with the code below:
ML {* fun attr s = let val _ = warning s in
(Thm.rule_attribute (fn _ => fn y => y)) end *}
setup {* Attrib.setup (Binding.name "map_const")
(Scan.lift Parse.string >> attr) "..." *}
lemma [map_const "foo"]: True
by simp
However upon defining the lemma, "foo" is printed 3 times. Is there a
good reason why the attribute code is called 3 times and is it
possible to get it called only once?
Regards,
Cezary
Email Gateway (Aug 18 2022 at 19:17):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Cezary,
This effect is due to the Haftmann and Wenzel "local theory sandwich".
It's once called for the auxillary context, once for the local context,
and once for the theory context.
It somewhat stores the data in three different layers.
However, when you lookup data, you will probably only see one version
from the one layer you are working in.
What's the point of getting it called only once anyway?
Lukas
Email Gateway (Aug 18 2022 at 19:17):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Hi Lukas,
On Sun, Mar 11, 2012 at 2:28 PM, Lukas Bulwahn <bulwahn@in.tum.de> wrote:
It somewhat stores the data in three different layers.
However, when you lookup data, you will probably only see one version from
the one layer you are working in.
This answers the question, thanks!
What's the point of getting it called only once anyway?
For certain theorems that are not of the valid format I want to print
a warning, and this warning is printed zero or three times. So far I
ignored the "Context.generic" argument, and checking that it is a
theory should to do the job.
Regards,
Cezary
On 03/10/2012 11:38 PM, Cezary Kaliszyk wrote:
Hi all,
I want to define an attribute, that takes a string as an argument
with the code below:ML {* fun attr s = let val _ = warning s in
(Thm.rule_attribute (fn _ => fn y => y)) end *}
setup {* Attrib.setup (Binding.name "map_const")
(Scan.lift Parse.string>> attr) "..." *}
lemma [map_const "foo"]: True
by simpHowever upon defining the lemma, "foo" is printed 3 times. Is there a
good reason why the attribute code is called 3 times and is it
possible to get it called only once?Regards,
Cezary
Email Gateway (Aug 18 2022 at 19:18):From: Makarius <makarius@sketis.net>
On Mon, 12 Mar 2012, Cezary Kaliszyk wrote:
Hi Lukas,
On Sun, Mar 11, 2012 at 2:28 PM, Lukas Bulwahn <bulwahn@in.tum.de> wrote:
It somewhat stores the data in three different layers.
However, when you lookup data, you will probably only see one version from
the one layer you are working in.This answers the question, thanks!
What's the point of getting it called only once anyway?
For certain theorems that are not of the valid format I want to print a
warning, and this warning is printed zero or three times.
The exact number of applications of declarations/attributes depends on the
context :-) For the usual targets it is often 3 -- the Haftmann/Wenzel
sandwich. There can be any number of further applications in a different
context, e.g. via interpretation.
Attributes that do not like a certain shape of argument (after it has
passed through several transformations by morphisms) may ignore it and
produce a warning (not an error!) to inform the user. The system
maintains Context_Position.is_visible/is_visible_proof to discern
situations where the user might be looking from ones hidden somewhere at
the bottom of the logical foundations etc.
Here is an example:
attribute_setup warning = {*
Scan.lift Args.name >> (fn s =>
Thm.rule_attribute (fn context => fn th =>
(Context_Position.if_visible_proof context warning s; th))) *}
declare TrueI [warning foo]
locale xxx
begin
declare TrueI [warning foo]
end
class yyy = fixes yyy :: 'a
begin
declare TrueI [warning foo]
end
This does the job for Isabelle2011-1. Since precise context visibility is
relevant for the Prover IDE, I am in the process to refine it further for
the next release (repository versions should be discussed on isabelle-dev
as usual.)
So far I ignored the "Context.generic" argument, and checking that it is
a theory should to do the job.
Rule of thumb (1): Do not ignore a context by default. There are very few
situations where things work properly without the local context.
Rule of thumb (2): The theory serves mainly foundational purposes, and is
rarely relevant to the user. Checking for Context.Theory makes things
global-only.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC