search

salmans / Razor

5 stars 0 forks source link

Pretty print theories #17

Open ramsdell opened 9 years ago

ramsdell commented 9 years ago

The !t command should produce a pretty printed version of the input theory.

salmans commented 9 years ago

@ramsdell : Asking Razor to show it when it is given as the input theory produces gibberish. Pretty printing would make it readable. I never liked the pretty printer libraries available for Haskell, so I recommend the one I wrote for CPSA in module CPSA.Lib.Pretty. It's a translation into Haskell of the one in "ML for the Working Programmer". The alogithm is by Lawrence C. Paulson, who simplified an algorithm by Derek C. Oppen.

Derek C. Oppen, Prettyprinting, ACM Transactions on Programming Languages and Systems, Vol 2, No. 4, October 1980, Pages 465-483.

The Prolog module pp in contrib/cpsa implements the same algorithm.