[isabelle-dev] Issues with "interpretations"

[Andreas Lochbihler]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>