Синтаксическая аббревиатура для типов с Изабель / HOL? - PullRequest
Новая
       14

Синтаксическая аббревиатура для типов с Изабель / HOL?

1 голос
/ 05 ноября 2019

Есть ли способ определить синтаксические замены для типов в Изабель / HOL?

Я хочу сделать что-то вроде этого: 

syntax my_short_list :: "type" ("my-list")
translations "my_short_list" ⇌ (type) "'a list"  ― ‹Could not find syntax to express this ...›

locale foo =
  fixes blub :: "my-list ⇒ my-list"

И хочу, чтобы это интерпретировалось так:

locale foo =
  fixes blub :: "'a list ⇒ 'a list"

(все вхождения my-list заменены текстом 'a list)

Выше приведено следующее сообщение об ошибке: 

Error in syntax translation rule: rhs contains extra variables
"my_short_list" ↝ ("\<^type>List.list" 'a)

Итак, яищу вариант, который является чисто синтаксической заменой без каких-либо проверок макро-гигиены.

Некоторая справка для понимания основной проблемы:

У меня есть локаль с 5 параметрами типа и типом данных Xон принимает все 5 параметров типа, поэтому для каждого использования я должен написать ('a, 'b, 'c, 'd, 'e) X. Очевидно, что имена на практике длиннее, поэтому это стало еще более нечитаемым.

Другие подходы, которые я пробовал:

  1. Определение типов или синонима типа в моей локали. Это недопустимо (см. https://stackoverflow.com/a/19281758/303637).
  2. Просто используйте другой параметр типа для представления ('a, 'b, 'c, 'd, 'e) X и assumes для всех необходимых свойств типа данных. Это много шаблонного, так как мне нужно написатьвниз все свойства, которые обычно генерируются автоматически для определений типов данных.
...