有没有办法在 Isabelle 中为自定义数据类型添加语法？

问题描述

所以我有两种自定义数据类型：

datatype ('a,'t) action = ACTION (name: "'a") (args: "'t list") ("⌈_ _⌋")

和

datatype ('a,'t) multiaction = MULTIACTION "('a,'t) action multiset" ("⟨(_)⟩")

它们都使用给定的符号，但是每当我想以它们漂亮的印刷格式使用这些数据结构时，它看起来有点多余。例如：

value "⟨{#⌈a b⌋,⌈c d⌋#}⟩"

我想做的是在没有多组括号的情况下输入上述内容，使其看起来像这样：

value "⟨⌈a b⌋,⌈c d⌋⟩"

我尝试过的是使用语法：

syntax
  "_maction" :: "args ⇒ ('a,'t) multiaction" ("⟨_⟩" [0] 60)
translations
  "⟨x⟩" == "CONST MULTIACTION {#x#}"

但是当我尝试使用某些数据类型时：

value "⟨⌈''x'' [1,2,3::int]⌋⟩"

但是我收到了一个排序良好的错误，我不知道为什么会出现这种错误。我可以帮忙吗？

提前致谢！

解决方法

也许，您希望将 multiset 语法提升为 multiaction？在这种情况下，您可能还希望取消 multiset 的相关定义（如评论中所述，理想情况下，您希望为此使用 datatype/lift_definition 基础架构） :

datatype ('a,'t) action = ACTION (name: "'a") (args: "'t list") ("⌈_ _⌋")
datatype ('a,'t) multiaction = MULTIACTION "('a,'t) action multiset"

(*this should not be lifted manually: use the integration of
the datatype and lifting infrastructure*)
fun add_multiaction :: 
  "('a,'b) action ⇒ ('a,'b) multiaction ⇒ ('a,'b) multiaction"
  where "add_multiaction x (MULTIACTION xs) = MULTIACTION (add_mset x xs)"

abbreviation MAempty :: "('a,'t) multiaction" ("⟨#⟩") where
  "MAempty ≡ MULTIACTION {#}"

syntax
  "_multiaction" :: "args ⇒ ('a,'t) multiaction" ("⟨(_)⟩")
translations
  "⟨x,xs⟩" == "CONST add_multiaction x ⟨xs⟩"
  "⟨x⟩" == "CONST add_multiaction x ⟨#⟩"

value "⟨⌈''x'' [1,2,3::int]⌋,⌈''x'' [1,3::int]⌋⟩"

---

我必须承认，我并不完全确定我是否完全理解您想要达到的目标：我提供的第一个想法是基于对问题的不太透彻的理解。

---

伊莎贝尔版本：Isabelle2021-RC6