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

【问题标题】：Is there a way to add syntax for a custom datatype in Isabelle?有没有办法在 Isabelle 中为自定义数据类型添加语法？
【发布时间】：2021-02-22 04:12:57
【问题描述】：

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

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]⌋⟩"

但是我得到了一个很好的排序错误，我不知道它为什么会发生。我可以帮忙吗？

提前致谢！

【问题讨论】：

pt 类型是什么？
另外，multiaction 类型的用途是什么？您可以将其作为类型同义词引入。
另外，'wellsortedness error' 通常意味着没有正确设置代码生成。它不应该与语法有关。
@ManuelEberl 抱歉，这是一个多动作，而不是 pt。我会解决的。在实际代码中，该数据类型（最初称为“pt”）中不仅仅是多操作，所以我认为我不能使用类型同义词。

标签： functional-programming isabelle algebraic-data-types

【解决方案1】：

也许，您希望将multiset 语法提升为multiaction？在这种情况下，您可能还希望解除 multiset 的相关定义（如 cmets 中所述，理想情况下，您将希望为此使用 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,2,3::int]⌋⟩"

我不得不承认，如果我完全理解您想要达到的目标，我并不完全确定：我提供的第一个想法是基于对问题的不彻底理解而想到的。

伊莎贝尔版本：伊莎贝尔2021-RC6

【讨论】：