Re: [isabelle] A fast implementation of concat for strings?
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 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.
> 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
>> 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
>> Currently, concat is a huge bottleneck:
>> value[code] "replicate 1000
>> value[code] "concat (replicate 1000
This archive was generated by a fusion of
Pipermail (Mailman edition) and