Re: [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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.