[isabelle-dev] Printing integers in Isabelle/ML

[Makarius]

On Thu, 18 Sep 2014, Florian Haftmann wrote:

> When printing integers, there is a funny historic artefact:
>
> 	Library.string_of_int :: int -> string
> 	  examples 1705, ~42 -- ie. ML syntax
>
> 	Library.signed_string_of_int :: int -> string
> 	  examples 1705, -42 -- ie. conventional syntax
>
> 	ML_Syntax.print_int is an alias for Library.string_of_int
>
> What is particularly confusing about string_of_int vs.
> signed_string_of_int that actually both return »signed« strings.  The
> naive expectation would be something like:
>
> 	Library.string_of_int :: int -> string
> 	  examples 1705, -42 -- ie. conventional syntax
>
> 	ML_Syntax.print_int :: int -> string
> 	  examples 1705, ~42 -- ie. ML syntax
>
> But there would be a considerable amount of code to be checked and
> sorted out then -- without support from the type system.

That is indeed historic, but still up-to-date.  The name "funny historic 
artefact" is a bit strong for this: it is correct within the margin of 
what we usually do in Isabelle sources. Despite a strong tradition to get 
names right, if change is put to the extreme it will break things in 
subtle ways.

An important principle of Isabelle/ML names is that a change of semantics 
needs to correlate to a change of name.  Thus string_of_int cannot be 
changed as sketched above, without causing mass confusion over many years, 
with various different versions of Isabelle and tools based on Isabelle 
out there.

When I introduced signed_string_of_int in 2006, the idea was that it 
covers the cases where there is actually a sign to print, while the 
existing string_of_int covers only the "nat" part of type int.  At the 
same time string_of_int retained its traditional meaning for ML notation 
of negative ints.


 	Makarius