Re: [isabelle] Attribute code called 3 times



On Mon, 12 Mar 2012, Cezary Kaliszyk wrote:

Hi Lukas,

On Sun, Mar 11, 2012 at 2:28 PM, Lukas Bulwahn <bulwahn at 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





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