Изабель - символьная и строковая литерал

Question

Как обозначаются символьные и строковые литералы в Изабель? Я хотел бы использовать значение символьного узла в примере trie учебника 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, чтобы перевести символ характера Изабеллы в тип символа целевого языка. И даже тогда экспорт кода с использованием string приведет к коду с использованием списков символов; вам необходимо явно использовать String.literal в ваших уравнениях кода Изабель, чтобы получить правильный тип строки в SML, Scala и OCaml.

Есть некоторые мысли об обобщении характера характера Изабеллы для поддержки многобайтовых символов, но это все еще в будущем.