GitLab

The Text.PrettyPrint library has a text function for converting ordinary strings to documents. This function takes the length of the string to be its final size. However, there are use cases where the actual length of this string and the "virtual" length of the document it represents are not necessarily the same. This use case comes up in cases where the resulting "Doc" is rendered to String and a further processor works on that particular string with its own built-in assumptions about how things should be laid out. (In our case, we produce Isabelle/HOL code from Cryptol, which gets rendered by the Isabelle theorem prover. These strings are the tags that correspond to Isabelle's own escape sequences for certain theory specific logical symbols.)

To remedy this, adding a function "sizedText" to the library would suffice:

sizedText :: Int -> String -> Doc
sizedText l s = TextBeside (Str s') l Empty
   where s' = s ++ take (l - length s) (repeat ' ')

Unfortunately this function can not be defined outside the PrettyPrint library itself, This is because the TextBeside constructor is not exported, and there seems to be no other way of accessing the length field otherwise.

Note that in the above code the user given length l can be larger or smaller than the actual length of the string s; so the first argument to take can be positive or negative. In either case the function does the right thing for our use case: If smaller, you get the original string; which messes up the ASCII output a bit but is the right thing to the for the target processor; if larger, then it gets padded with space at the end appropriately to get the ASCII looking right as well.

Our current workaround for this issue is to replicate the library code ourselves and add this function on top, which is a kludge at best that we'd like to avoid.

The function sizedText satisfies the law:

    sizedText (length s) s = text s

and hence agrees with the existing text function for ordinary usage.

Trac metadata

Trac field	Value
Version
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	libraries/pretty
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture