syntax - 如何在 MMT 中给出绝对 URI？获取 "unbound token: http"和 "ill-formed constant reference"

Question

在 MMT 表面语法中，绝对 URI 对我来说表现出乎意料。在某些地方，我得到 unbound token: http和 ill-formed constant reference错误，而在其他地方它们工作正常。请参阅下面的(非详尽)列表。
绝对 URI 何时起作用？他们什么时候没有？我怎样才能解决这个问题？
以下不起作用，即生成上述错误:

在理论中包含声明:

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

理论中的规则指令:

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

URI 的术语:

namespace http://example.com ❚

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

以下工作:

命名空间指令:

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

文档级别的 fixmeta 指令:

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

文档级别的规则指令:

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

Answer 1

解决方案

在文件的开头，在文档级别发出以下指令:

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

使用 ☞ (“juri”用于 MMT IDE 中的自动完成)在所有绝对 URI(和命名空间导入限定符)之前。
如果您仅在需要将绝对 URI 与正常 MMT 术语区分开来的地方使用此前缀就足够了。
经验法则:如果在某个地方可以使用正常的 MMT 术语，那么您必须使用 ☞如果你想在那里写一个 URI。如果您在 MMT 理论或观点中，这尤其适用。

示例:

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 ❙
❚

解释
没有像 ☞ 这样的机制，对于 MMT 的词法分析器和解析器来说，从单纯的变量名称中消除绝对 URI 的歧义将是非常麻烦的。前者需要解析为 OMMOD或 OMID AST 中的节点，而后者需要解析为 OMV .
加载规则 scala://parser.api.mmt.kwarc.info?MMTURILexer正是基于 ☞ 添加了这样一个消歧过程到 MMT 的词法分析器和解析器。