[isabelle] A fast implementation of concat for strings?



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.