简化自然的漂亮印刷

Question

假设我写了一个用于反转列表的函数.我想用value命令测试它,只是为了向自己保证我可能做对了.但输出看起来很可怕:

value "reverse [1,8,3]"
> "[1 + 1 + 1, 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)), 1]" :: "'a list"

如果我告诉Isabelle将这些数字字符视为自然,输出会更糟:

value "reverse [1::nat,8,3]"
> "[Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), Suc 0]" :: "nat list"

有时候我会求助于使用字符串,但对于所有这些撇号而言,这看起来有点滑稽:

value "reverse [''1'',''8'',''3'']"
> "[''3'', ''8'', ''1'']" :: "char list list"

我可以指示伊莎贝尔漂亮的打印机打印Suc (Suc (Suc 0))的3,等等？也许通过放弃一些神奇的咒语,syntax或translations命令？

---

这是我的完整示例,如果您想将其粘贴到Isabelle中:

theory Scratch imports Main begin

fun reverse where 
  "reverse [] = []"
| "reverse (x#xs) = reverse xs @ [x]"

value "reverse [1,8,3]"
value "reverse [1::nat,8,3]"
value "reverse [''1'',''8'',''3'']"

end

Answer 1

简短回答:我的第一个想法是使用类型int,因为(不像nat)它的代码生成器设置默认使用二进制数字表示.

"~~/src/HOL/Library/Code_Target_Nat"正如naT建议的那样,如果您不想使用Suc表示形式,那么导入也是一个好主意nat.

说明: Isabelle中的数字使用在Num.thy;中定义的构造函数进行编码; 例如,5是.的缩写numeral (Bit1 (Bit0 One)).这里One,Bit0和Bit1有型的构造num.numeral重载,适用于任何具有a 1和关联的类型+.以下是代码方程式numeral:

lemma numeral_code [code]:
  "numeral One = 1"
  "numeral (Bit0 n) = (let m = numeral n in m + m)"
  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"

如果我们生成代码5::'a::numeral,则on 1和+on类型'a被视为未解释的常量,因此它们保留在输出中:(1 + 1) + (1 + 1) + 1.

生成代码5::nat的工作原理相同,除了我们做的有代码1和+对类型nat,在以下方面Suc.从而(1 + 1) + (1 + 1) + 1进一步减少到Suc (Suc (Suc (Suc (Suc 0)))).

类型int不同.代码生成器设置Int.thy使用三个构造函数,用于类型int:Pos和Neg类型num => int,以及0.甲code_abbrev声明导致每次出现numeral在类型num => int将被代替Pos代码生成过程中.代码运行后,Pos然后numeral在Isabelle显示结果之前返回.因此5::int评估为公正5.

特殊代码设置理论: src/HOL/Library包含一些用于自定义数字代码生成的不同理论.

• "~~/src/HOL/Library/Code_Target_Nat"告诉代码生成器使用目标语言(例如SML或Haskell)的内置数字作为类型nat.例如,5::nat通常将其翻译为SML numeral (Bit1 (Bit0 One)); 但是,加载此库后,它将5在SML中进行转换.之后将结果value转换回伊莎贝尔数字表示.

• "~~/src/HOL/Library/Code_Target_Int"是相同的,但对于类型int而不是nat.

• "~~/src/HOL/Library/Code_Target_Numeral"只需加载前两个库.它只影响类型nat,并int在课堂上,没有任何其他类型numeral.

• "~~/src/HOL/Library/Code_Binary_Nat"配置nat在相同的风格作为默认代码设置为int:与构造0和nat_of_num::num => nat和code_abbrev声明.有了这个库,value "5::nat"也会返回5.