Как указать абсолютный URI в MMT? Получение несвязанного токена: http и неправильная постоянная ссылка

Абсолютные 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 на уровне документа:

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

  • директивы правил на уровне документа:

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

syntax mmt
person ComFreek    schedule 11.11.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Решение

  1. В начале вашего файла введите следующую директиву на уровне документа:

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

  2. Используйте ☞ (juri для автозаполнения в MMT IDE) перед всеми абсолютными URI (и квалификаторами импорта пространства имен).

    Достаточно, если вы используете этот префикс только в тех местах, где необходимо отличить абсолютные URI от обычных терминов MMT.

    Практическое правило: если в каком-то месте можно использовать обычный термин MMT, то вам нужно использовать ☞, если вы хотите написать там URI. Это особенно применимо, если вы придерживаетесь теории или взгляда ММТ.

Пример:

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.

person ComFreek    schedule 11.11.2020