Mayank Manjrekar (Jul 05 2024 at 03:47): Mayank Manjrekar (Jul 05 2024 at 03:47):I have following definition in my theory
definition bits :: "nat ⇒ nat ⇒ nat ⇒ nat" ("_[[_:_]]" [100, 50, 50]) where
"bits x i j ≡ nat (drop_bit j (take_bit (i+1) x))"
I am noticing that the following computation never completes for me, and the polyml process consumes enormous amount of system resources.
value "(2::rat) powi (0x3f800000[[30:23]] - 127)"
However, this theorem is proved within a second:
theorem "(2::rat) powi (0x3f800000[[30:23]] - 127) = 1"
apply(simp add: bits_def)
done
What is going on here? What can I do to quickly evaluate and test a new definition?
Mathias Fleury (Jul 05 2024 at 05:14):the easiest way is to generate the code with export_code bits in SML and have a look
Mathias Fleury (Jul 05 2024 at 05:15):my guess without having any idea of your imports: you are using the Peano representation of integers instead of an efficient representation (which does not sound like a good idea for 0x3f800000)
Yong Kiam (Jul 05 2024 at 13:47): from a bit of messing around, it looks like value "0x3f800000" by itself will loop
my bad, I had [[simp_trace]] enabled, this isn't true
Mayank Manjrekar (Jul 05 2024 at 16:11):Mathias Fleury said:
my guess without having any idea of your imports: you are using the Peano representation of integers instead of an efficient representation (which does not sound like a good idea for
0x3f800000)
I am importing Complex_Main. Is that okay?
theory Bits
imports Complex_Main
begin
Add "HOL-Library.Code_Target_Nat" for native integers instead of the binary version of Peano…
Mathias Fleury (Jul 05 2024 at 18:05):command "value"
0.185s elapsed time, 0.334s cpu time, 0.000s GC time
Thank you. Could you please also tell me how to profile the "value" command, as you have done here?
Mathias Fleury (Jul 05 2024 at 20:22):hovering with the mouse over the keyword value
Mayank Manjrekar (Jul 05 2024 at 20:40):That is not working for me in Jedit -- I only see that the output 1 :: rat in the tooltip. But, nevermind, I discovered the Timing panel. Thank you!
Mathias Fleury (Jul 08 2024 at 07:05):Control - hover, sorry
Manuel Eberl (Jul 10 2024 at 20:14):Note that a significant part of that time will just be code generation and compilation.
Last updated: Dec 21 2024 at 16:20 UTC