<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">If there are fixed-size integers in ML that raise
an exception on overflow, it should be possible to just do
appropriate code_printing setup similar to what
Code_Target_Numeral does. We already have to somehow magically
map Isabelle's "int" type to ML's "IntInf" type, so all we have
to do is to locally map it to ML's fixed size "int" instead, I
think.<br>
</font></p>
<p><font size="+1">Manuel<br>
</font></p>
<br>
<div class="moz-cite-prefix">On 2017-11-08 15:36, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:8c40b7e2-dc7a-6a0f-6782-68a62e2afc0d@in.tum.de">
<br>
<br>
On 08/11/2017 14:13, Makarius wrote:
<br>
<blockquote type="cite">On 08/11/17 12:35, Tobias Nipkow wrote:
<br>
<blockquote type="cite">
<br>
On 07/11/2017 23:13, Makarius wrote:
<br>
<blockquote type="cite">For Flyspeck-Tame a small performance
loss remains. It might be worth
<br>
trying to configure the Isabelle/HOL codegen to use FixedInt
instead of
<br>
regular (unbounded) Int. Thus it could become faster with
Poly/ML 5.7.1
<br>
than with 5.6.
<br>
</blockquote>
<br>
Just as for Isabelle itself, I don't want generated code to
abort with
<br>
overflow or even worse to overflow silently.
<br>
</blockquote>
<br>
I also don't want to see FixedInt used routinely instead of
proper
<br>
mathematical Int.
<br>
<br>
The idea above is to provide an option for the HOL codegen that
is used
<br>
specifically for applications like Flyspeck-Tame. It is mainly a
<br>
question to codegen experts, if that can be done easily.
<br>
</blockquote>
<br>
Then I misunderstood. An optional use of FixedInt for languages
where overflow raises an exception is fine with me.
<br>
<br>
<blockquote type="cite">If the answer is "no", I personally don't
mind. Flyspeck-Tame runs
<br>
de-facto only in background builds: 1-2h more or less does not
matter so
<br>
much. Its classic runtime was actually 10h total, now we are at
7h.
<br>
</blockquote>
<br>
In which case I would say that providing such an option should be
balanced with the complexity it requires or introduces.
<br>
<br>
Tobias
<br>
<br>
<blockquote type="cite">
<br>
Makarius
<br>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>