search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Why Int2Float have 3 arguments now #773

Open denis-bogdanas opened 10 years ago

denis-bogdanas commented 10 years ago

branch unified-builtins2

What is the equivalent of the old one-argument Int2Float? If there are similar changes in builtins, please document them.

dwightguth commented 10 years ago

53, 11

On Thu, Jul 31, 2014 at 3:44 PM, Denis Bogdanas notifications@github.com wrote:

branch unified-builtins2

What is the equivalent of the old one-argument Int2Float? If there are similar changes in builtins, please document them.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/773.

denis-bogdanas commented 10 years ago

Could you be more explicit please?

dwightguth commented 10 years ago

Int2Float creates a float with a particular precision and exponent range. You are still using Maude, which has that hacky incorrect implementation of floating point arithmetic. It's based on doubles, so to use it you create a double, which has 53 bits of precision and 11 bits of exponent. On Jul 31, 2014 4:47 PM, "Denis Bogdanas" notifications@github.com wrote:

Could you be more explicit please?

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/773#issuecomment-50823417.

denis-bogdanas commented 10 years ago

Got it. I would like to see all those builtins documented, with explanation on what every argument means.

dwightguth commented 9 years ago

We should probably add module comments to the new KORE prelude explaining each of the operations found there.