CODEWITHSUNDEEP
isabelletheorem-proving
TFuto
TFuto

Reputation: 1462

Isabelle - character and string literal support

How are character and string literals declared in Isabelle? I would like to use a character node value in the trie example of the Isabelle tutorial (declared as 'v option).

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

Upvotes: 2

Views: 1425

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8268

There is the char type, which represents 8-bit characters, and the string type, which is defined as a list of characters. There is also some syntax and pretty printing setup for character and string literals:

typ string
(* char list *)

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

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

Note that string literals must be delimited with two single quotes ''. Character literals must be entered as CHR ''c''. This currently works for most printable ASCII characters, but nothing above 0x7F.

There are functions nat_of_char and char_of_nat to convert between these 8-bit characters and their ANSI codes (reprsented as nat).

There is also the type String.literal, which is essentially a type clone of string that hides the underlying list nature. This is mainly interesting for code generation, since target languages (e.g. Scala) might provide a dedicated string type (as opposed to just a list of characters). Conversion between string and String.literal is with implode and explode.

Note that if you want to export code using strings, you should probably import ~~/src/HOL/Library/Code_Char.thy to translate Isabelle's character type into the target language's character type. And even then, exporting code using string will result in code using lists of characters; you need to explicitly use String.literal in your Isabelle code equations in order to get the proper string type in SML, Scala and OCaml.

There are some thoughts about generalisation of Isabelle's character type to support multibyte characters, but that is still in the future.

Upvotes: 3

Related Questions