CASL overloading not possible

[tillmo]

When I upload

spec Nat =
  sorts Pos < Nat
  ops 1:Pos; 1:Nat
end

I get

The name "1" of the symbol is ambiguous. It is already used for either a axiom or a theorem. The symbol "1" is located at http://develop.ontohub.org/ref/1/sandbox/overload:3.14.

see https://develop.ontohub.org/sandbox/overload

This completely prevents CASL overloading.
Solution: IRIs for symbols should also contain their types.

[eugenk]

What format do you propose?

• http://develop.ontohub.org/sandbox/overload//Pos-1
• http://develop.ontohub.org/sandbox/overload//1-Pos
• http://develop.ontohub.org/sandbox/overload//symbols//Pos//1
• http://develop.ontohub.org/sandbox/overload//1%3APos (: is encoded to %3A)

And what do we do if there is a symbol/sentence/mapping/child/etc called like the chosen possibility?

[tillmo]

I think http://develop.ontohub.org/sandbox/overload//1%3APos is the best way, because symbol names might contain a "-". Note that there can also be symbols with name f:Nat->Nat, and then the ">" probably needs to be coded as well.

If there is another item with the same name, it is an error.

[eugenk]

We don't have the information in the XML of Hets to do this. Hets's output is, for example:

    <Symbols>
      <Symbol kind="sort" name="Nat" iri="Nat" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.15-2.17">sort Nat</Symbol>
      <Symbol kind="sort" name="Pos" iri="Pos" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.9-2.11">sort Pos</Symbol>
      <Symbol kind="op" name="1" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Nat</Symbol>
      <Symbol kind="op" name="1" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Pos</Symbol>
    </Symbols>

what we would like to have is something like:

    <Symbols>
      <Symbol kind="sort" name="Nat" iri="Nat" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.15-2.17">sort Nat</Symbol>
      <Symbol kind="sort" name="Pos" iri="Pos" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.9-2.11">sort Pos</Symbol>
      <Symbol kind="op" type="Nat" name="1" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Nat</Symbol>
      <Symbol kind="op" type="Pos" name="1" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Pos</Symbol>
    </Symbols>

or

    <Symbols>
      <Symbol kind="sort" name="Nat" iri="Nat" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.15-2.17">sort Nat</Symbol>
      <Symbol kind="sort" name="Pos" iri="Pos" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:2.9-2.11">sort Pos</Symbol>
      <Symbol kind="op" name="1:Nat" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Nat</Symbol>
      <Symbol kind="op" name="1:Pos" iri="1" range="/Users/eugen/Work/Ontohub/repos/ontologies/overload.casl:3.14">op 1 : Pos</Symbol>
    </Symbols>

[eugenk]

Which output is preferrable?

With name="1:Pos", we also display "1:Pos" in the index page of the symbols.
With type="Pos" name="1", we would add a new database column for the symbols table that contains the generated "locid_name" 1:Pos or we would add a new column for the type.

Do you have other suggestions?

[tillmo]

I would prefer type="Pos" name="1", because it is more general.