has_repr and has_to_string type classes

[leodemoura]

The current type class has_to_string is similar to the Show Haskell typeclass.
The instances for string and char produced quoted values.

"abc" => "abc"
'a' => "a"

This is inconvenient since we often just need to convert a value (char, nat, string, int, etc) into a "plain" string (no quotes). @johoelzl suggested we add a has_repr type class. The idea is to rename the current has_to_string type class to has_repr, and add a new has_to_string whose instances are supposed to produce plain (i.e., no quotes) strings.

[johoelzl]

The idea behind Python's repr is that eval (repr x) = x for most data types. I guess this is also a behaviour we want from repr.

https://docs.python.org/3/library/functions.html#repr

[avigad]

A small correction to what @leodemoura wrote: currently we have

#eval to_string 'a'   -- "'a'"
#eval to_string "abc" -- "̈\"abc"\"

[leodemoura]

@avigad Note that #eval to_string ... applies the has_to_string twice.
#eval automatically applies the has_to_string instance. This behavior is consistent with the other programming languages (e.g., Haskell). The to_string application is applying the has_to_string too. This is why you got "'a'" and "\"abc\"". After the refactoring, #eval will automatically apply the has_repr instance (like Haskell applies the Show instance).
Thus, we will have

#eval to_string 'a' -- "a"
#eval to_string "abc" -- "abc"

-- But, the same example with `repl` will produce the weird double quotes.
#eval repr 'a'   -- "'a'"
#eval repr "abc" -- "̈\"abc\""

[leodemoura]

The commits above close this issue.
We may still have some rough spots (e.g., a has_expr A instance which should be has_to_string A).