如何在MMT中给出绝对URI？获取“未绑定令牌：http”和“格式错误的常量引用”

如何解决如何在MMT中给出绝对URI？获取“未绑定令牌：http”和“格式错误的常量引用”

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

解决方法

解决方案

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

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

在所有绝对URI（和名称空间导入限定符）之前使用☞（在MMT IDE中为自动完成功能，使用“ juri”。）

仅在需要将绝对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与单纯的变量名进行歧义将非常麻烦。在AST中，前者需要解析为OMMOD或OMID节点，而在AST中则需要解析为OMV。

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