Agda: Task: set 'show' free to its original purpose: printing Haskell representations of data

[GoogleCodeExporter]

In the Agda code base, show is (ab)used for pretty-printing things to display in error messages, debug messages, producing file names, etc.

However, the purpose of show is to print a Haskell representation, see also
http://hackage.haskell.org/package/pretty-show

Step 1: Replace uses of show in error messages, world communication etc. by uses of Agda.Utils.Pretty.prettyShow (and implement missing Pretty instances).

Step 2: Define a class and instances for debug printing and use it instead of show in debug print-outs. One could parametrize debug printing by a level of detail, see e.g.
http://hackage.haskell.org/package/prettyclass-1.0.0.0/docs/Text-PrettyPrint-HughesPJClass.html#t:PrettyLevel

Step 3: Derive or define Show instances for the datatypes of the Agda codebase.
Collections should be printed as Fully.Qualified.DataType.fromList ...

Original issue reported on code.google.com by [email protected] on 5 Oct 2014 at 12:48

[andreasabel]

I did step 1 for Abstract.Name.

[andreasabel]

A show case for using pretty-show during debugging

This is the transcript of a debugging session 2020-06-03 for #4709 carried out partially with @nad.

Installing pretty-show

...and a toy run

cabal install pretty-show
ppsh --help
ppsh --html > foo.html
[Just 'a',Nothing]
^D
open foo.html

Starting a ghci debug session for agda

• Copy your testcase.agda into agda root directory (cannot :cd in ghci).
• Remove -Werr from Agda.cabal

cabal v1-repl Agda

Wait a couple of minutes until all 371 modules are loaded.

Inside ghci

We want to debug something in Agda.Syntax.Concrete.Operators starting line 624:

:m + Agda.Main
let main = runAgda []
:break Agda.Syntax.Concrete.Operators 624
:main testcase.agda

This stops at our breakpoint.

Inspecting values using ppsh

Now let us inspect some values in scope, say p :: Pattern.

prettyShow p
print p

The latter produces a horrible blob, the Haskell representation of the pattern p. We can explore it using ppsh.

• Cut and paste the blob into a file blob.hs. (Alternatively, we could paste it into stdin when running ppsh.)
• Convert it into html and open in a browser. We don't want to see the boring contents of constructors Range, ArgInfo and Fixity'.

ppsh --html --hide=Range --hide=ArgInfo --hide=Fixity\' < blob.hs > blob.html
open blob.html

Here we can collapse and expand parts and thus explore the value interactively.

Evaluating stuff in ghci

We can bring some functions into scope and evaluate.

:m + Agda.Syntax.Concrete.Operators
patternQNames p

We can step, e.g. staying inside the current module.

:stepmodule

Just a single :step is usually to fine-grained, e.g., getting us into the >>= function of the TCM monad.

Maybe the best way to step is to set the next breakpoint and then :continue.

[nad]

* Remove `-Werr` from `Agda.cabal`

I wonder why GHCi complains when GHC doesn't.

[nad]

* Remove `-Werr` from `Agda.cabal`

I wonder why GHCi complains when GHC doesn't.

Today I loaded up and ran Agda in GHCi 8.10.2 without changing Agda.cabal. (Occasionally the program crashed due to a segmentation fault.) Sometimes when I changed a Haskell file reloading only took a few seconds.