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



Dear Christian,

thanks for the pointer.

But
  value[code] "show (replicate 1000
''xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx'')"
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.

Best,
  Cornelius

2015-09-29 20:19 GMT+02:00 Christian Sternagel <c.sternagel at gmail.com>:
> 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 in.tum.de> 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.