[isabelle-dev] Issues with "interpretations"

[Jasmin Christian Blanchette]

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