The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 27 Mar 2013 09:31:39 +0000,
Andrew Kennedy 
<akenn AT microsoft.com>
 a écrit :

> Hello
> 
> I have a seemingly simple problem: I want to pretty-print a large
> term inside Coq, simply by writing a function
> 
>    pretty : Tm -> string
> 
> and then be able to compute the string and look at it inside Proof
> General, or coqtop. But when using "Compute" or "Print" the string
> remains "within quotes", and the newlines remain escaped. Example:
> 
> Welcome to Coq 8.4pl1 (January 2013)
> 
> Coq < Require Import String.
> [Loading ML file z_syntax_plugin.cmxs ... done]
> [Loading ML file quote_plugin.cmxs ... done]
> [Loading ML file newring_plugin.cmxs ... done]
> [Loading ML file ascii_syntax_plugin.cmxs ... done]
> [Loading ML file string_syntax_plugin.cmxs ... done]
> 
> Coq < Open Scope string_scope.
> 
> Coq < Example s := "this is one line\n".
> s is defined
> 
> Coq < Example ss := s++s++s++s++s++s++s.
> ss is defined
> 
> Coq < Compute ss.
>      = "this is one line\nthis is one line\nthis is one line\nthis is
> one line\n this is one line\nthis is one line\nthis is one line\n"
>      : string
> 
> 
> I want a way of *actually* *printing* the darn thing. Is there a way?
> 
> (Yes, I have considered simply using Notations for my Tm type, with
> format specifiers that incorporate line breaks, etc. But sometimes
> it's just easier to write a function into string, as one would do in
> ML or Haskell.)
> 
> Cheers
> Andrew.

In Coq, there is no escape mechanism at all.
"\n" strands for '\' + 'n' (two chars).

If you want a newline, just do:

Example s :=
"this is one line
".

I know it can completely break your indentation, but it does not use
the "010"%char hack someone mentionned.

I do not know if it is architecture dependant (if under windows it
will give a different string).

A simple hack would be to write down your escaper your self (a string →
string which changes "\n" into newline).

I have not written a Format version of the Ocaml libraries in Coq, but
if someone is interested, I can try to write one.

And in Coq, we can even write a "format: string → Type" such that for
instance,

format "Hello %s, it is %d o'clock.\n" = string → Z → string

so that we could have a

printf : ∀ s, format s

and

Compute printf "Hello %s, it is %d o'clock.\n" "John" 8.

would return:

"Hello John, it is 8 o'clock.
"