sizedText function for Text.PrettyPrint
|Reported by:||lerkok||Owned by:||simonmar|
|Keywords:||text, sizedText, pretty printing, Text.PrettyPrint||Cc:||Christian.Maeder@…|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Rev(s):|
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.
sizedText satisfies the law:
sizedText (length s) s = text s
and hence agrees with the existing
text function for ordinary usage.