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

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> 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.