Re: [isabelle] A fast implementation of concat for strings?

Dear Christian,

thanks for the pointer.

  value[code] "show (replicate 1000
took 56.196s (or 47.544s if not run in parallel with another
value[code]) on my machine.

Am I using it wrong or is the string just too long?

By the way, the dependency on the afp website to
Datatype_Order_Generator is wrong, it should be Deriving.


2015-09-29 20:19 GMT+02:00 Christian Sternagel <c.sternagel at>:
> Dear Cornelius,
> are you aware of the "Show" AFP entry? Maybe the (at least in Haskell,
> standard) trick for "constant time concatenation" that is used there is of
> interest for you. Moreover it is possible to generate show-functions (what
> you call "toString") automatically for data types.
> cheers
> chris
> On Tue, Sep 29, 2015, 16:07 C. Diekmann <diekmann at> wrote:
>> Dear list,
>> I recently learned that the Isabelle pretty printer for large datatype
>> constructs can be quite slow.
>> Andreas explained that not printing (only evaluating) the result
>> helps, for example
>> value [code] "let x = expression in ()"
>> To get some debug output, I started writing custom toString functions
>> in HOL to print some complicated datatypes. This was sufficiently
>> fast.
>> value [code] "let x = expression in something_toString x"
>> However, as datatypes get more complex, my toString functions also get
>> slow. My question: Is there a fast implementation of concat for
>> strings?
>> Currently, concat is a huge bottleneck:
>> value[code] "replicate 1000
>> ''xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx''"
>> (*5.895s*)
>> value[code] "concat (replicate 1000
>> ''xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx'')"
>> (*67.556s*)
>> Best,
>>   Cornelius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.