Stream: Beginner Questions

Topic: ✔ built-in functions to convert int to char?

Chengsong Tan (Feb 09 2022 at 09:30):

Hi all,

Is there some nice built-in support in Isabelle for converting a nat to a char?
I am writing a function to enumerate all possible char values in isabelle:

fun all_chars :: "nat ⇒ char list"
  where
"all_chars 0 = [char_of 0]"
|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"

I went through this answer
https://stackoverflow.com/questions/33393926/isabelle-character-and-string-literal-support
and somehow functions nat_of_char and char_of_nat wasn't there in the String.thy file.
I did find something called char_of, but somehow isabelle complains about it,

saying that

Additional type variable(s) in specification of "all_chars_graph": 'a
Extra type variables on rhs: "'a"
The error(s) above occurred in definition "all_chars_sumC_def":
  "all_chars_sumC ≡ λx. THE_default undefined (all_chars_graph TYPE('a) x)"

How can I fix this? If I need to write one on my own, how should char_of_nat defined to be simple?

Thanks a lot,
Chengsong

Chengsong Tan (Feb 09 2022 at 09:39):

fun all_chars :: "nat ⇒ char list"
  where
"all_chars 0 = [CHR 0x00]"
|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"

Somehow this does the trick.
Can someone explain, please?

Maximilian Schaeffeler (Feb 09 2022 at 11:29):

of_char has the polymorphic type 'a => nat, thus in the expression of_char 0 the type of 0is also 'a (an additional type variable, that cannot be deduced from the function arguments). In the second equation (Suc case), the type of of_char can be specialized to nat => char, as Suc i has type nat.

A simpler definition would be:

definition all_chars :: "nat ⇒ char list" where
"all_chars n = map char_of [0..n]"

Chengsong Tan (Feb 09 2022 at 18:44):

Maximilian Schaeffeler said:

of_char has the polymorphic type 'a => nat, thus in the expression of_char 0 the type of 0is also 'a (an additional type variable, that cannot be deduced from the function arguments). In the second equation (Suc case), the type of of_char can be specialized to nat => char, as Suc i has type nat.

A simpler definition would be:

definition all_chars :: "nat ⇒ char list" where
"all_chars n = map char_of [0..n]"

Thanks a lot! That's a nice definition, except you need [0..n] needs n to be an int (which sounds weird to me as upto means "up to a positive number " right?

Notification Bot (Feb 09 2022 at 19:35):

Chengsong Tan has marked this topic as resolved.

Maximilian Schaeffeler (Feb 10 2022 at 08:14):

No, n is of type nat not int in this definition.
There's also a version of this syntax that does not include n:

definition "all_chars n = map char_of [0..<n]"

Last updated: Dec 21 2024 at 16:20 UTC