Gibt es einen bekannten Hack, der benutzerdefinierte Syntax für Definitionen in einem bestimmten Gebietsschema mithilfe des Syntax-/Übersetzungsmechanismus ermöglicht? Alle meine Versuche einer "offensichtlichen" Lösung erzeugen Typfehler, von denen ich glaube, dass sie dadurch verursacht werden, dass die Syntax/Übersetzung noch nicht "lokalitätsbewusst" ist.Verwenden von Syntax/Übersetzungen mit Gebietsschemas
Rohe AST-Transformationen mit syntax und translations können nicht innerhalb von Locales in Isabelle2016 verwendet werden. Es gibt eine Problemumgehung für Konstanten und Typen, deren Deklaration nicht von den Ländereinstellungsparametern abhängt. Sie müssen lediglich die Syntaxdeklaration außerhalb der Locale für die entsprechende Konstante aus der Hintergrundtheorie ausgeben. Im Folgenden finden Sie eine Proof of Concept:
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
Diese Problemumgehung funktioniert nicht für Konstanten, die auf Parameter des Lokals ab, weil dann konstant im Hintergrund Theorie dieser Parameter als zusätzliche Argumente übernimmt und das Gebietsschema eine Abkürzung installiert, die wird gefaltet, bevor die benutzerdefinierte Syntaxübersetzung ausgelöst wird.
OK, danke. Leider hat die Definition, für die ich eine Syntaxumwandlung durchführen möchte, in meinem Fall einen Typ, der von den Gebietsschema-Parametern abhängt. Ich muss nur auf irgendeine Syntax dafür verzichten. –
Typen können nicht von den lokalen Parametern abhängen. Wenn es also nur darum geht, die gleichen Typvariablen zu verwenden, funktioniert die obige Problemumgehung immer noch. –
Entschuldigung, ja, Sie haben Recht. Ich wollte damit sagen, dass der Typ der betreffenden Definition von den Typvariablen des Gebietsschemas abhängt und die Definition selbst von den Parametern des Gebietsschemas abhängt. –