Hi Florian,
to me the liberal flag seems rather ad-hoc. Wouldn't a proper
hierarchical naming solve this problem (maybe by introducing an
automatic "sub-module" Internal/Auto/Whatever for any theory T, such
that automatic names may be referred to by using T.Whatever.automatic_name).
Admittedly, after reading once more through the above paragraph, my own
suggestion seems rather ad-hoc ... Nevertheless, maybe it gives rise to
discussion ;)
cheers
chris
On 10/07/2010 09:23 AM, Florian Haftmann wrote:
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
"P foo"
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a mechanism which analyzes
parts of a theory (most prominently constants and theorems) and
generated new constants and theorems from them. The result, in
particular the new constants, are highly unpredictable, and the user is
not really interested in the number or names of the new constants. The
situation is somehow similar to the predicate compiler, but even less
tamed. To ensure that the new constants do not clash with existing
ones, the bindings for them have to be distilled carefully and a rather
unsatisfactory way. I am asking myself whether this could be
dramatically simplified by giving bindings a »liberal« flag: this could
be set e.g. using a function Binding.liberal :: binding -> binding; on
declaration in a namespace, the basename of a liberal binding would be
modified if it would clash with an existing declaration. User-space
binding would stay non-liberal an issue an error on clashing.
I think such a liberal binding mechanism would be helpful for all kind
of tools which provide automatic, rather unpredictable theory extensions.
Any opinions?
Florian
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
