search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.85k stars 256 forks source link

Print for humans #3857

Open seebees opened 1 year ago

seebees commented 1 year ago

Summary

The print function is for humans to look at output.

Background and Motivation

Humans enjoy whitespace. While JSON can be printed as one big string on a single line, no reasonable human wants to read this.

The Dafny print function stuffs everything onto a single line :( It would be so nice to have the output be easily readable.

Proposed Feature

Consider

datatype Foo = Foo(bar: string, baz: string)
print [Foo("What part", "am I?")];

This will output [Module_Compile.Foo.Foo(What part, am I?)]

Instead do this

[
  Module_Compile.Foo.Foo(
    bar: "What part",
    baz: "am I?"
  )
]

Alternatives

No response

robin-aws commented 1 year ago

I'd be much happier with this functionality in a user code library rather than Dafny itself. Since you mention JSON, that's a much smaller scope to handle than arbitrary Dafny values, so perhaps we can add that feature to https://github.com/dafny-lang/libraries/pull/51 as a fast-follow after getting it merged.