Синтаксис преобразователя инфиксного отношения в Isabelle

Дано

notation
  rtranclp  ("(_^**)" [1000] 1000)

Я могу писать, учитывая инфикс op ⇒

"op ⇒⇧*⇧* x x'"

но не намного читабельнее и красивее

"x ⇒⇧*⇧* x'"

Я знаю, что для каждого конкретного отношения (в данном случае ⇒) я могу установить для него аббревиатуру. Но могу ли я решить это вообще, т.е. для любого инфиксного отношения?

Если да, могу ли я распространить это на несколько отношений и другие аргументы? Например, учитывая два инфиксных отношения ⇒ и ▹ и еще один термин y, я хочу настроить его так, чтобы я мог писать

x (⇒;▹)⇗y⇖ x'

(обратите внимание на использование инфикса) вместо

foo op ⇒ op ▹ y x x'

(где, в моем случае, имеет тип foo :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'a ⇒ 'a).


syntax isabelle
person Joachim Breitner    schedule 24.09.2014    source источник
comment
Я сам постоянно возвращаюсь к этому вопросу, но никогда не задумывался над ним серьезно. Возможно я должен. Кстати: ваши последние два примера несколько сбивают меня с толку (что такое foo и почему y используется дважды?). Не могли бы вы уточнить?   -  person chris    schedule 24.09.2014
comment
Я доработал пример.   -  person Joachim Breitner    schedule 24.09.2014

Ответы (1)


arrow_upward
3
arrow_downward

Я считаю, что общее решение для всех инфиксных отношений невозможно, потому что синтаксический анализатор не знает о символах отношений в отдельности. Как видно из реализации в mixfix.ML, объявление инфикса с символом отношения < эквивалентно двум объявлениям миксфикса, а именно "op <" и "(_ < _)" с соответствующими приоритетами.

Однако есть более общее и элегантное решение, чем введение сокращений для всех комбинаций предикатов и преобразователей предикатов. Во-первых, введите синтаксическую категорию для реляционных символов. Чтобы также получить правильный вывод, добавьте синтаксический маркер _infix

nonterminal rel
syntax (output) "_infix" :: "rel ⇒ logic" ("_")

Затем объявите синтаксическую константу _rtranclp_rel для инфиксного использования с инфиксными отношениями.

syntax "_rtranclp_rel" :: "logic ⇒ rel ⇒ logic ⇒ logic" ("(_ _⇧*⇧* _)")
translations "_rtranclp_rel x R y" ⇀ "CONST rtranclp R x y"
translations "_rtranclp_rel x (_infix R) y" ↽ "CONST rtranclp R x y"

Теперь добавьте перевод синтаксиса в ваше отношение rel, которое вы хотите использовать с _rtranclp_rel:

consts rel :: "nat ⇒ nat ⇒ bool" (infix "⇒" 100)

syntax "_rel_infix" :: rel ("⇒")
translations "_rel_infix" ⇀ "CONST rel"
translations "_rel_infix" ↽ "_infix (CONST rel)"

Затем Изабель сможет правильно разобрать и красиво напечатать x ⇒⇧*⇧* z. Обратите внимание, однако, что все полностью примененные экземпляры rtranclp являются инфиксным символом, напечатанным красиво (например, rtranclp R x y, независимо от того, является ли отношение инфиксным символом.

Затем этот механизм работает и для вашей функции foo:

consts foo :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'a ⇒ 'a ⇒ bool"

syntax "_foo_rel" :: "logic ⇒ rel ⇒ rel ⇒ logic ⇒ logic ⇒ logic" ("_ '(_;_')⇗_⇖ _")
translations "_foo_rel x R S y z" ⇀ "CONST foo R S x y z"
translations "_foo_rel x (_infix R) (_infix S) y z" ↽ "CONST foo R S x y z"

Конечно, приоритеты в аннотациях миксфиксов должны быть скорректированы до разумных. Можно даже сделать это рекурсивно. Например:

syntax "_rtranclp_rel2" :: "rel ⇒ rel" ("_⇧*⇧*")
translations "_rtranclp_rel2 R" ⇀ "CONST rtranclp R"
translations "_rtranclp_rel2 (_infix R)" ↽ "_infix (CONST rtranclp R)"

term "x (⇒⇧*⇧*;⇒)⇗y⇖ z"
person Andreas Lochbihler    schedule 24.09.2014
comment
Вероятно, никто никогда не работал с этим должным образом (я думаю, что мое предложение выше - не лучшее решение проблемы). Если вы считаете, что это должно поддерживаться по умолчанию, вы можете опубликовать сообщение в списке рассылки разработчиков и посмотреть, сочтут ли его полезным другие. Затем есть шанс получить его в Pure (инфикс определен в Pure, поэтому HOL уже поздно). - person Andreas Lochbihler; 24.09.2014