Использование синтаксиса/переводов с локалями

Question

Есть ли какой-либо известный хак, который позволяет настраивать синтаксис определений внутри данной локали, используя механизм синтаксиса/перевода? Все мои попытки «очевидного» решения порождают ошибки типа, которые, как мне кажется, вызваны синтаксисом/переводом, еще не сделанным «locale-aware».

Answer 1

Необработанные трансформации АСТ с syntax и translations не могут использоваться внутри локалей в Isabelle2016. Существует временное решение для констант и типов, декларация которых не зависит от параметров локали. Вам просто нужно выпустить объявление синтаксиса за пределами локали для соответствующей константы из теории фона. Ниже приводится доказательство концепции:

locale test = fixes a :: nat begin 
definition foo :: "nat ⇒ nat" where "foo x = x" 
end 

syntax "_foo" :: "nat ⇒ bool" ("FOO") 
translations "FOO" ↽ "CONST test.foo" 

context test begin 
term foo 

Этот способ не работает для констант, которые зависят от параметров местности, потому что тогда константа в теории фона принимает эти параметры в качестве дополнительных аргументов и языковой стандарт устанавливает аббревиатуру, которая складывается до того, как пользовательский синтаксический перевод срабатывает.