[Agda] Printing strings in the emacs mode

Discussion:

Guillaume Brunerie

2017-11-21 02:37:37 UTC

Hi all,

I’m using an Agda program to generate some Agda code. I’m not using
reflection, I’m just using Agda as a regular functional programming
language to generate strings, that I then want to copy-paste in a
different file.

For now, I didn’t bother with compilation, so I’m just defining terms
of type String (from the standard library), and then I use C-c C-n in
order to get their normal form.

My problem is that in the result of C-c C-n, the string is surrounded
by quotes, and the new lines are escaped as \n, which makes it a bit
annoying to copy-paste, as I have to do a search and replace
afterwards.

Is there a way to use something like C-c C-n in order to get the
normal form of a term of type String, but have it printed properly,
without escaping the new lines and without the quotes before and
after?

Thanks,
Best,
Guillaume

Ulf Norell

2017-11-21 05:39:12 UTC

Permalink

You can use C-u C-u C-c C-n. This normalises `show TERM` and
prints the resulting string without quotes and escapes. It grabs
whatever `show` happens to be in scope, so in your case you could
define `show = id`.

/ Ulf

On Tue, Nov 21, 2017 at 3:37 AM, Guillaume Brunerie <

Post by Guillaume Brunerie
Hi all,
Iâm using an Agda program to generate some Agda code. Iâm not using
reflection, Iâm just using Agda as a regular functional programming
language to generate strings, that I then want to copy-paste in a
different file.
For now, I didnât bother with compilation, so Iâm just defining terms
of type String (from the standard library), and then I use C-c C-n in
order to get their normal form.
My problem is that in the result of C-c C-n, the string is surrounded
by quotes, and the new lines are escaped as \n, which makes it a bit
annoying to copy-paste, as I have to do a search and replace
afterwards.
Is there a way to use something like C-c C-n in order to get the
normal form of a term of type String, but have it printed properly,
without escaping the new lines and without the quotes before and
after?
Thanks,
Best,
Guillaume
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Guillaume Brunerie

2017-11-21 13:09:38 UTC

Permalink

Great, thanks, it works!

I had tried C-u C-u C-c C-n already but with the `show` in
Data.String, and somehow it printed even more escapes. But with `show
= id`, it works, thanks!

Guillaume

Post by Ulf Norell
You can use C-u C-u C-c C-n. This normalises `show TERM` and
prints the resulting string without quotes and escapes. It grabs
whatever `show` happens to be in scope, so in your case you could
define `show = id`.
/ Ulf
On Tue, Nov 21, 2017 at 3:37 AM, Guillaume Brunerie

Post by Guillaume Brunerie
Hi all,
I’m using an Agda program to generate some Agda code. I’m not using
reflection, I’m just using Agda as a regular functional programming
language to generate strings, that I then want to copy-paste in a
different file.
For now, I didn’t bother with compilation, so I’m just defining terms
of type String (from the standard library), and then I use C-c C-n in
order to get their normal form.
My problem is that in the result of C-c C-n, the string is surrounded
by quotes, and the new lines are escaped as \n, which makes it a bit
annoying to copy-paste, as I have to do a search and replace
afterwards.
Is there a way to use something like C-c C-n in order to get the
normal form of a term of type String, but have it printed properly,
without escaping the new lines and without the quotes before and
after?
Thanks,
Best,
Guillaume
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel

2017-11-21 15:03:47 UTC

Permalink

Just to remind the world, Haskell's "show" prints the *Haskell*
representation of data. (Usually the AST.)

Thus, extra escapes when showing strings.

--Andreas, keeper of law and order

Post by Guillaume Brunerie
Great, thanks, it works!
I had tried C-u C-u C-c C-n already but with the `show` in
Data.String, and somehow it printed even more escapes. But with `show
= id`, it works, thanks!
Guillaume

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/

Setzer A.G.

2017-11-23 21:02:19 UTC

Permalink

If your output is actually a string, you could create an interactive program and let it print it out for you.
The ooAgda library https://github.com/agda/ooAgda has in examples/consoleExamples currently three simple examples of console programs (more to come soon ...) See READMEconsolePrograms.txt

Anton
________________________________________
From: Agda [agda-***@lists.chalmers.se] on behalf of Guillaume Brunerie [***@gmail.com]
Sent: 21 November 2017 02:37
To: agda list
Subject: [Agda] Printing strings in the emacs mode

Hi all,

I’m using an Agda program to generate some Agda code. I’m not using
reflection, I’m just using Agda as a regular functional programming
language to generate strings, that I then want to copy-paste in a
different file.

For now, I didn’t bother with compilation, so I’m just defining terms
of type String (from the standard library), and then I use C-c C-n in
order to get their normal form.

My problem is that in the result of C-c C-n, the string is surrounded
by quotes, and the new lines are escaped as \n, which makes it a bit
annoying to copy-paste, as I have to do a search and replace
afterwards.

Is there a way to use something like C-c C-n in order to get the
normal form of a term of type String, but have it printed properly,
without escaping the new lines and without the quotes before and
after?

Thanks,
Best,
Guillaume