Isabelle - 字符和字符串文字支持

Question

在Isabelle中如何声明字符和字符串文字？我想在Isabelle教程的示例中使用字符节点值（声明为'v option）。

datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list" 

Answer 1

还有就是char类型，其表示8位字符，并string类型，其被定义为字符的列表。也有一些语法和漂亮的打印设置的字符和字符串：

typ string 
(* char list *) 

term "''foobar''" 
(* ''foobar'' :: char list *) 

value "hd ''foobar''" 
(* CHR ''f'' :: char *) 

注意字符串文字必须用两个单引号''分隔。字符文字必须输入为CHR ''c''。这目前适用于大多数可打印的ASCII字符，但没有超出0x7F。

有功能nat_of_char和char_of_nat来转换这些8位字符和他们的ANSI代码（编号为nat）。

还有类型String.literal，它基本上是一个类型克隆string隐藏潜在的列表性质。由于目标语言（例如Scala）可能会提供专用字符串类型（而不仅仅是字符列表），因此这对于代码生成来说非常有趣。 string和String.literal之间的转换为implode和explode。

请注意，如果要使用字符串导出代码，则应该导入~~/src/HOL/Library/Code_Char.thy以将Isabelle的字符类型转换为目标语言的字符类型。即使如此，使用string导出代码将导致使用字符列表的代码;您需要在Isabelle代码方程中明确使用String.literal以便在SML，Scala和OCaml中获得正确的字符串类型。

对于支持多字节字符的Isabelle字符类型的普遍化有一些想法，但这仍然是未来。