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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
