Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:21):

From: "C. Diekmann" <diekmann@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:22):

From: Christian Sternagel <c.sternagel@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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:22):

From: "C. Diekmann" <diekmann@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 11:22):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Cornelius,

something strange is going on here. I just tested your example in the generated code with „test 10000“ and even in „ghci“ the answer is immediate. So I’m currently confused why it takes so long in Isabelle.

theory Test
imports Show
"~~/src/HOL/Library/Code_Char"
"~~/src/HOL/Library/Code_Target_Int"
"~~/src/HOL/Library/Code_Binary_Nat"

begin

definition test :: "integer ⇒ string" where
"test n = show (replicate (nat (int_of_integer n))
''xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx'')"

export_code test in Haskell module_name Test file Code
end

Cheers,
René

Last updated: Nov 21 2024 at 12:39 UTC