[Agda] PrettyPrint.agda

[Yoriyuki Yamagata]

Hi, Nil.


Nils Anders Danielsson さんは書きました:
>
> Do you need to use impossible/undefined in the code? Maybe some
> invariants should be strengthened.
>
>   
Yes, it can be strengthened.  I'm working on it.

In the Haskell code, type RDoc = Doc, but it is guaranteed  to  not 
contain Above, Beside constructor at the top level.  I'm trying to 
represent this invariant by type.  Namely, define RDoc as a type 
constructed from Doc using same constructors  of Doc but Above, Beside.

Another issue is division by 0, but it could be fixed by defining some 
argument's type as ℕ.

> There are a number of pretty-printing libraries for Haskell. Some of
> them are documented in these papers:
>
>   

Thank you for the suggestion.  I will look to them.

-- 
Yoriyuki Yamagata (Research Scientist)
National Institute of Advanced Industrial Science and Technology
E-mail: yoriyuki.yamagata at aist.go.jp
Tel:+81-6-4863-5036 FAX:+81-6-4863-5052
http://staff.aist.go.jp/yoriyuki.yamagata/index.html.en