Блог

Абсолютные 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 ❚
    

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

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

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

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

Решение

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

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

2. Используйте ☞ («juri» для автозаполнения в IDE MMT) перед всеми абсолютными 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 or OMID в AST, тогда как последний должен быть проанализирован как an OMV .

Загрузка правила scala://parser.api.mmt.kwarc.info?MMTURILexer добавляет точно такой процесс устранения неоднозначности, основанный на ☞ лексере и синтаксическом анализаторе MMT.