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

Question

绝对 URI 在 MMT 表面语法中的行为对我来说出乎意料。在某些地方，我得到 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 http://cds.omdoc.org/urtheories?LF ❚

文档级别的规则指令：

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

Answer 1

解决方案

在文件的开头，在文档级别发出以下指令：
```
rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚
```
在所有绝对 URI（和命名空间导入限定符）前面使用 ☞（MMT IDE 中的自动完成的“juri”）。

如果您仅在需要从正常 MMT 术语中消除绝对 URI 歧义的地方使用此前缀就足够了。

经验法则： 如果在某些地方可以使用正常的 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 的歧义将非常麻烦。前者需要在 AST 中解析为 OMMOD 或 OMID 节点，而后者需要解析为 OMV.

加载规则scala://parser.api.mmt.kwarc.info?MMTURILexer正是将基于☞的这种消歧过程添加到MMT的词法分析器和解析器中。

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

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

syntax

mmt

解决方案

说明