*To*: "C. Diekmann" <diekmann at in.tum.de>*Subject*: Re: [isabelle] A fast implementation of concat for strings?*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Wed, 30 Sep 2015 15:03:44 +0000*Accept-language*: de-DE, de-AT, en-US*Cc*: Christian Sternagel <c.sternagel at gmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAGbqCMwH7jcNOzRYSMV5tfnT9tt-b6or8LmqZkhqQTdNs=G+qg@mail.gmail.com>*References*: <CAGbqCMyN4uqV1qJDsocSN31+=7O9PNn6vnsKiF=AwYhmQm7+-g@mail.gmail.com> <CA+_wRgHvsPWQDBPEqFphYhEVJLK2zmhG_Sacdrrmf90a3YgWjQ@mail.gmail.com> <CAGbqCMwH7jcNOzRYSMV5tfnT9tt-b6or8LmqZkhqQTdNs=G+qg@mail.gmail.com>*Thread-index*: AQHQ+sFsZae/rkIi/kiDJdi+HZiq8p5Tr6EAgAFMswCAAA8HgA==*Thread-topic*: [isabelle] A fast implementation of concat for strings?

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Ã > Am 30.09.2015 um 16:09 schrieb C. Diekmann <diekmann at 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 > > 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 >>> >> > -- RenÃ Thiemann mailto:rene.thiemann at uibk.ac.at Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-53234 University of Innsbruck

**References**:**[isabelle] A fast implementation of concat for strings?***From:*C. Diekmann

**Re: [isabelle] A fast implementation of concat for strings?***From:*Christian Sternagel

**Re: [isabelle] A fast implementation of concat for strings?***From:*C. Diekmann

- Previous by Date: Re: [isabelle] A fast implementation of concat for strings?
- Previous by Thread: Re: [isabelle] A fast implementation of concat for strings?
- Next by Thread: [isabelle] Permanent position at the University of Sussex
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list