Hi Jasmin,
> 1. As long as we define new interpretations (hook types) in the HOL image, we
can
> reorganize the imports to avoid the evil scenarios. Problems arise when users
define
> their own interpretations.
I already ran into scenario 3 without registering my own interpretations just by using
code_datatype (which internally uses interpretation, too). Here's the example:
theory A imports Main begin
typedecl foo
consts Foo :: foo
end
theory B imports A begin
code_datatype Foo
end
theory C imports A begin
code_datatype Foo
end
theory D imports A B begin
end
This gives the same error message as in your scenario 3:
Clash of specifications for constant "Typerep.typerep_class.typerep":
"ScratchB.typerep_foo_inst.typerep_foo_def"
"ScratchA.typerep_foo_inst.typerep_foo_def"
> 4. If anybody has any ideas on how to address Scenario 3, please let me know!
I don't think that scenario 3 is the one to address. IMO the hooks should behave as if
they were executed in the name space of the datatype declaration, so size is doing
something sensible already. Rather do I think that it seems worthwhile to address scenario
2 by making name space merges more liberal. If there is a duplicate declaration of a
constant, one could check whether the declarations of the constants are equivalent, and
accept if so. Since I am not familiar with the internals, I do not know whether such a
change is feasible in the current implementation.
Andreas
On 02/04/14 15:34, Jasmin Christian Blanchette wrote:
Hi all,
My work on (co)datatypes and my desire to move "Quickcheck_Narrowing" out of HOL and into Library have lead
me to discover several issues with the interpretation mechanism ("Pure/interpretation.ML") that is used to
hook into various modules (e.g., the "size"-generating extension to "datatype"s). I will summarize
my findings below. It might well be that this is already (at least partially) known to some of you.
In the following, I will talk concretely about datatype and their various hooks (size,
Quickcheck random, Quickcheck narrowing, etc.), but the same issues can arise in
principle with all the other hooking-mechanism based on
"Pure/interpretation.ML".
Generally, the issues arise when a datatype is introduced in theory A and a
hook is registered in theory B, and A does not import B.
Scenario 1: Two Types, One Name
In this scenario, we introduce two datatypes with the same base name ("t") in
two different theories:
theory A
imports "~~/src/HOL/Datatype"
begin
datatype t = T
end
theory B
imports "~~/src/HOL/Datatype"
begin
datatype t = U | V
end
Then we get a name clash at merge time when pulling in a new hook (such as the one
defined by "Typerep" below):
theory C
imports A B "~~/src/HOL/Typerep"
begin
end
*** Duplicate constant declaration "C.typerep_t_inst.typerep_t" vs.
"C.typerep_t_inst.typerep_t" (line 1 of "/Users/blanchet/bugs/scenarios/C.thy")
*** At command "theory" (line 1 of "/Users/blanchet/bugs/scenarios/C.thy")
The examples above are self-contained and can be tested directly against a "HOL" or a
"Pure" image.
What's happening here is that the "Typerep" is generating theorems that contain the name "t" but not the unambiguous
names "A.t" vs. "B.t", and since the merge takes place in "C", the prefix is "C." for both.
Interestingly, the "size" hook bypasses the problem by overriding the path using
"Sign.root_path" and "Sign.add_path". For example, this works:
theory C2
imports A B "~~/src/HOL/Fun_Def"
begin
thm A.size B.size
end
Hence, my original idea was to solve the "name clash" problem for all types by replicating the
"size" trick, and perhaps to move the logic up either to the individual hooks or even to
"Pure/interpretation.ML". However, this does not solve all problems, as we will see in Scenario 2.
Scenario 2: The Diamond
theory D
imports "~~/src/HOL/Datatype"
begin
datatype t = T
end
theory E
imports D "~~/src/HOL/Fun_Def"
begin
end
theory F
imports D "~~/src/HOL/Fun_Def"
begin
end
theory G
imports E F
begin
end
*** Duplicate constant declaration "D.t.t_size" vs. "D.t.t_size"
The problem is that these constants are defined by both E and F with the same
name, so the merge in G fails.
Scenario 3: The Specification Duplicate
I thought I could work around the issue raised by Scenario 2 by having Isabelle generate names that
combine the original theory name where the type was introduced and that where the merge took place
that generated the name. In other words, generate "E.D.t.t_size" and
"F.D.t.t_size" above. I tried this out, and it *almost* works. For the above theory G, it
gives
*** Clash of specifications for constant "Nat.size_class.size":
*** "F.D.t.size_t_inst.size_t_def" (line 1 of "~/bugs/scenarios/F.thy")
*** "E.D.t.size_t_inst.size_t_def" (line 1 of "~/bugs/scenarios/E.thy")
*** At command "theory" (line 1 of "/Users/blanchet/bugs/scenarios/G.thy")
Here the problem is that we overloaded the same constant "Nat.size_class.size" twice for the same type. It
happens to be harmless here because "size" is well behaved (i.e. if we disabled the check in
"Pure/defs.ML", I believe we still couldn't derive "False"). I cannot think of a workaround.
What does this mean in practice?
1. As long as we define new interpretations (hook types) in the HOL image, we
can reorganize the imports to avoid the evil scenarios. Problems arise when
users define their own interpretations.
2. In particular, moving "Quickcheck_Narrowing" outside HOL and into Library
raises this issue in JinjaThreads. I will see if I can reorganize the imports.
3. Despite the failure with Scenario 3, the way "size" does things looks
superior to the other approach, and I'm tempted to standardize on this for the old-style
and new-style datatype hooks. I have patches ready already (cf. testboard). Please stop
me if you disagree.
4. If anybody has any ideas on how to address Scenario 3, please let me know!
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
