How to give an absolute URI in MMT? Getting "unbound token: http" and "ill-formed constant reference"

Question

Absolute URIs behave unexpectedly for me in MMT surface syntax. In some places, I get unbound token: http and ill-formed constant reference errors while at other places they work fine. See the (non-exhaustive) list below.

When do absolute URIs work? When do they not? How can I fix this?

The following don't work, i.e. generate the errors mentioned above:

• include declarations in theories:

  theory test =
    include http://cds.omdoc.org/urtheories?LF ❙
  ❚
  

• rule directives in theories:

  theory test =
    rule scala://api.mmt.kwarc.info?SomeClass ❙
  ❚
  

• URIs in terms:

  namespace http://example.com ❚
  
  theory test =
    someFunction ❙
    someConstant ❙
    c = someFunction http://example.com?test?someConstant ❙
  ❚
  

The following work:

• namespace directives:

  namespace http://cds.omdoc.org/urtheories ❚
  

• fixmeta directives at document level:

  fixmeta http://cds.omdoc.org/urtheories?LF ❚
  

• rule directives at document level:

  rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
  

Answer 1

Solution

1. At beginning of your file, issue the following directive at document level:

   rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
   

2. Use ☞ ("juri" for autocompletion in MMT IDEs) in front of all absolute URIs (and namespace import qualifiers).

   It suffices if you use this prefix only at places where it is necessary to disambiguate absolute URIs from normal MMT terms.

   Rule of thumb: if at some place a normal MMT term can be used, then you have to use ☞ if you want to write an URI there. This especially applies if you are within an MMT theory or view.

Example:

rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❙

theory test =
  include ☞http://cds.omdoc.org/urtheories?LF ❙
❚

// A namespace import qualifier "abbreviation" ❚
import abbreviation https://example.com/very-long-uri ❚

theory test2 =
  include ☞abbreviation:?test3 ❙
❚

Explanation

Without a mechanism like ☞, it would be very cumbersome for MMT's lexer and parser to disambiguate an absolute URI from a mere variable name. The former would need to be parsed as an OMMOD or OMID node in the AST, whereas the latter would need to be parsed as an OMV.

Loading the rule scala://parser.api.mmt.kwarc.info?MMTURILexer adds exactly such a disambiguation process based on ☞ to MMT's lexer and parser.