Email Gateway (Aug 18 2022 at 17:52): Email Gateway (Aug 18 2022 at 17:52):From: Brian Huffman <brianh@cs.pdx.edu>
Why can't I define two constants with the same base-name (but
different qualifiers) in the same local theory? The following code,
which tries to define "one.foo == True" and "two.foo == False", gives
a "Duplicate fixed variable(s)" error message. It works just fine if I
split it into two separate local_setup commands, however.
local_setup {*
fn lthy =>
let
val qual = Binding.qualify true
val ((t1, (s1, thm1)), lthy) = lthy |>
Local_Theory.define
((qual "one" @{binding foo}, NoSyn),
((qual "one" @{binding foo_def}, []), @{term "True"}))
val ((t2, (s2, thm2)), lthy) = lthy |>
Local_Theory.define
((qual "two" @{binding foo}, NoSyn),
((qual "two" @{binding foo_def}, []), @{term "False"}))
in
lthy
end
*}
I should explain why I want to do this: The reason is that I (along
with a few other people) am working on a tool for importing Haskell
datatype definitions into Isabelle. We are using a form of "soft
typing", so type constructors are defined as Isabelle constants, along
with the data constructors. The problem is that in Haskell, type names
and constructor names are in separate name spaces, and it is quite
common for a Haskell type and its data constructor to have the same
name, e.g.
data MyBool = MyBool Bool
I want to add qualifiers to distinguish these in Isabelle, something
like "type.MyBool" and "term.MyBool". However, since the
implementation of the tool uses local theories (which as I understand
is the recommended programming practice), it runs into the "Duplicate
fixed variable" error I mentioned above.
Will local theories in a later version of Isabelle be able to use
qualifiers to distinguish names?
While I am still using Isabelle2011, is there a workaround that will
let me avoid the error, while still generating the top-level qualified
constant names that I want? Or will I have to "un-localize" the tool
so that it uses top-level theories directly instead of local theories?
Email Gateway (Aug 18 2022 at 17:53):From: Makarius <makarius@sketis.net>
On Wed, 29 Jun 2011, Brian Huffman wrote:
Why can't I define two constants with the same base-name (but different
qualifiers) in the same local theory? The following code, which tries to
define "one.foo == True" and "two.foo == False", gives a "Duplicate
fixed variable(s)" error message. It works just fine if I split it into
two separate local_setup commands, however.local_setup {*
fn lthy =>
let
val qual = Binding.qualify true
val ((t1, (s1, thm1)), lthy) = lthy |>
Local_Theory.define
((qual "one" @{binding foo}, NoSyn),
((qual "one" @{binding foo_def}, []), @{term "True"}))
val ((t2, (s2, thm2)), lthy) = lthy |>
Local_Theory.define
((qual "two" @{binding foo}, NoSyn),
((qual "two" @{binding foo_def}, []), @{term "False"}))
in
lthy
end
*}
This is according to the specifications. The auxiliary context of the
local theory target presents newly defined terms as fixed variables, but
these cannot be qualified. (There are no kernel checks for that for
performance reasons, but the overall system will make problems when the
principle "consts: qualified, fixes: unqualified" is violated.)
The restriction holds only as long as the aux. context is active, i.e. you
can introduce artificial boundaries as workaround, using
Local_Theory.init/exit or reinit operations in a way that I cannot tell on
the spot, without some study of the current state of the sources.
data MyBool = MyBool Bool
I want to add qualifiers to distinguish these in Isabelle, something
like "type.MyBool" and "term.MyBool".
It is probably easier to avoid this clash by using the conventional
Isabelle naming scheme in such situations: terms are called "foo", types
are called "foo_type". A suffix will always be orthogonal to name spaces
prefixes and qualifiers.
If you do not want to present it like that to the end user, you can
additionally augment the global const name space afterwards using
Sign.const_alias etc. -- this looks to be the least intrusive workaround
at the moment.
Will local theories in a later version of Isabelle be able to use
qualifiers to distinguish names?
Depends if I manage to localize HOL/datatype and record without it.
Records have their own small qualifiers with potential duplication of base
names, but it is possible that one can somehow avoid getting into the same
trouble as above. If not, I not to devise some tricks to overcome the
limitation somehow.
While I am still using Isabelle2011, is there a workaround that will let
me avoid the error, while still generating the top-level qualified
constant names that I want? Or will I have to "un-localize" the tool so
that it uses top-level theories directly instead of local theories?
This is also possible, see Inductive.add_inductive_global, for example.
(Operations called "global" are generally considered a bit fashioned,
potentially being discontinued when localization has advanced further.)
Makarius
Email Gateway (Aug 18 2022 at 17:53):From: Brian Huffman <brianh@cs.pdx.edu>
Thanks for the suggestion; I will have a closer look at the alias
operations on name spaces. My original plan was to maintain separate
name_space values for my embedded types and terms, with syntax rules
that would select the appropriate one based on context (similar to the
system currently used for parsing/printing Isabelle type expressions).
However, I was under the (mistaken) impression that
Name_Space.intern/extern were only able to fill in/hide qualifiers; I
didn't know about the support for aliases. It looks like I should be
able to use aliases with name suffixes to get everything to work with
local theories.
Last updated: Apr 26 2024 at 04:17 UTC