(obsolete) Qualified Sorts

This page is obsolete and should be removed soon. See Module System instead.

Qualified Sorts

Sorts introduced in distinct modules will now be distinct sorts.

All sorts will be fully qualified in KORE with the module in which they were introduced. For example, if module M1 introduces sort Exp for the first time, and then modules M2 and M3 both import M1 and add more stuff to Exp, and then module M4 imports M2 and M3 and does more with Exp, then in all these 4 modules, in KORE, the Exp sort will actually be M1.Exp. On the other hand, if there is no M1 but only M2 and M3 each introducing their own sort Exp and M4 imports both M2 and M3, then M2 will refer to its Exp as M2.Exp, M3 will refer to its Exp sort as M3.Exp, and M4 will refer to the two distinct Exp sorts as M2.Exp and M3.Exp.

The above is, again, valid for KORE definitions. So in KORE definitions the sort name will already tell you where the sort was declared! So one less complex API method needed. Of course, at the level of Full K, in the frontend, things will be a bit more complicated, because we want users to just write Exp. The front end will attempt to infer a unique module name M so that M.Exp makes sense, and if not possible, it will issue an error. Of course, users will also be given the option to tag sorts with module names in order to disambiguate. For example, if they write M.Exp then the frontend will start searching for Exp starting with module M, and if module M0 is found unambiguously to have defined sort Exp, then M.Exp will be replaced with M0.Exp in the generated KORE.

The main reason for the feature above is to allow us to define language translators in K. For example, I may want to define a translator from C to Java. In that case, I have to define a module that imports both C and Java. Now if C and Java happen to each have a sort named Exp, then we are in trouble. We do not want to have to modify any of the existing semantics in order to define a translator from one to the other. With the above, we can now write something like this:

syntax Java.Exp ::= "translate" C.Exp

The only tricky issue here is whether we can re-declare a sort Exp in a module M2 that imports a module M1 which already declares sort Exp. I think we should simply disallow that, because otherwise things can get too complicated; I don't think we really need this generality. Also, one is supposed to know what one imports, so one should not override an imported sort name "by mistake".