问题描述
在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的词法分析器和解析器中。