Re: [isabelle-dev] [isabelle] New representation of naturals in Code_Target_Numeral decreases generated code performance
Hi Florian, newtype in Haskell is not always for free, see for example Joachim's blog post: http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html Andreas On 19/09/13 12:58, Florian Haftmann wrote: Hi Peter, When using Code_Target_Numeral instead of the old Efficient_Nat, the code generator wraps some funny dummy-datatype (nat = Nat of int) around my natural numbers. What was the reason behind this change, and is there a way to produce code working with plain IntInf? There have been two reasons: * Proper datatype abstractions: negative integers are not natural numbers; no explicit check necessary for subtraction of natural numbers. * When Haskell type classes or Scala implicits are involved, it is necessary that the mapping of HOL types to target language types is injective. The coping with this was nightmare in the previous situation and is now straight-forward. As a preface, I have checked these change previously against Flyspeck_Tame and did not notice any performance difference. For one of my benchmarks (heavy use of arrays in Imperative-HOL) this results in doubling the runtime under PolyML. Under mlton, its only around 15% slower. Quoting Andreas: In many cases, such type copies do not affect performance, because the compiler can get rid of such type copies after type checking. However, when they are nested into some other polymorphic type, this is not always possible. Maybe, arrays fall into that class. I am not sure about that. If this is the case then I wonder how the contract in Haskell that »newtype« declarations are always compiled away is accomplished in Haskell. Or maybe there is some ML subtlety creeping in here? Maybe we should contact David Matthews on that. Another possibility is that the code setup for Imperative-HOL contains a performance flaw. Have you a change to figure out which functions are the top-wasters in your benchmark? Then we could inspect these. Hope this helps, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
[...]
font management, etc. ;( Obviously, the choice of UI frameworks does
matter in everyday work on UIs.
All UI frameworks I've seen so far are crap. A UI framework alone does not
give
you a real editor, you would have to implement that yourself.
It is, of course, just not true that you have to do everything yourself.
To illustrate my claim that the choice of the UI framework does matter,
consider the notorious sub/super-scripting problem for Isabelle theories.
Swing doesn't have it, the really powerful Netbeans editor doesn't
(or didn't, when I last looked), but JFace/SWT *does*:
I just skimmed the API documentation (the JavaDoc, yes, the JavaDoc),
found the StyledText (which is used by the JFace TextEditor, which is used by
the Eclipse text editors), found the setStyleRange(StyleRange) method,
and found the rise parameter in the StyleRange.
From there, with the assistence of WindowBuilder for layouting etc.,
I got the attached subscript/superscript demo working immediately.
At the core, one just creates StyleRanges and set them to the widget:
styledText.setStyleRanges(new StyleRange[] {
keyword(0, 7), subScript(s1, 1), subScript(s2, 1), superScript(s3, 5) });
private StyleRange subScript(int start, int length) {
StyleRange r = new StyleRange();
r.start = start;
r.length = length;
r.rise = -4;
r.font = scriptFont;
return r;
}
we knew that already from the start. (You were actually the one to see good
OO
design in Swing and its pluggable LAFs.)
I still maintain that Swing has a large amount of good OO design, and
in particular a very neat model/view separation. Also, it is a good
place to see how far one gets by the consistent application of proven
design patterns. My expressed current preference for JFace/SWT stems from
- its speed
- its modern widgets, e.g. tables that have attached trees for folding rows
- its use of the platform's native widget set, which does wonders for usability
Maybe you want to help them getting SWT into a form that they can catch up
with
the display qualities of Isabelle/jEdit (sub/superscripts, hyperlinks and
formal
markup in tooltips etc.). I had to bend Java 2D and Swing quite a bit to make
this work, but it has to be repeated for SWT
These features are all availabe in Eclipse editor and hence supported
by the overall editing framework. To make this very clear: nobody uses
SWT by itself. The Eclipse platform consists of three layers,
with according resonsibilities:
1) SWT: wrapper for the native widget set, quite a few editor-specific
custom widgets. This is intentionally kept with minimal functionality,
because it needs to be ported to different platforms.
2) JFace: the viewers implement model/view separation (the model-view-controller
pattern), and add editor-specifics, such as syntax-coloring, annotation bars,
auto-completion, and much much more. In general, there is one Viewer type
for one SWT widget type, and it makes the minimal widget useful
to applications.
3) Eclipse: adds functionality concerning the editing environment:
resources on the disk, opening/closing/re-arranging/... of editors and
views, matching files types to their editors, etc. (This is sometimes
called the view-handler pattern [1]). The usage is actually
very simple, once one has grasped isolated the essential points from
the generality of the overall platform. At least, my students were able
to create views and editors after one lecture on the plugin and
window handling concepts.
The layers 2+3 offer extensive means of customization.
To come back to the above example, one does, of course, not set
StyleRanges on the SWT widget oneself. One registers with the
JFace TextViewer's syntax highlighting mechanism and produces
them on demand -- for instance from the semantic markup offered
by Isabelle/Scala.
-- and all the portability issues
will probably come back once again in a different form.
Actually, probably not: the Eclipse IDE is widely used on the platforms
that Isabelle supports and the IBM engineers are doing a constantly great
job at keeping the differences under the hood of SWT and the whole system
running. Since the Eclipse/JFace/SWT stack is actually used in industry
for end-user applications, there is a lot of pressure to succeed.
The available delta-pack makes it straightforward to package
an application for different platforms.
I hope to have clarified my earlier claims in this way.
I'm also always happy to answer more specific questions
if they arise.
Cheers,
Holger
[1] Buschmann et al.: Pattern-oriented software architecture. Wiley.
package subsuper;
import org.eclipse.swt.SWT;
import org.eclipse.swt.custom.StyleRange;
import org.eclipse.swt.custom.StyledText;
import org.eclipse.swt.graphics.Color;
import org.eclipse.swt.graphics.Font;
import org.eclipse.swt.graphics.FontData;
import org.eclipse.swt.layout.FillLayout;
import org.eclipse.swt.widgets.Display;
import
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] General code_abort'd constant
Hi Jasmin, I moved this thread from users to devel, because we are now referring to changesets ;-). I would appreciate if all these code_aborts that you mention were consolidated to use Code.abort. I second this. Cf. http://goo.gl/4kR3vu :) See now 788730ab7da4, which replaces all code_abort in HOL/Library with Code.abort. There are still two code_aborts in HOL (in Predicate and Enum) that Code.abort should subsume, but Code.abort can only be defined in String.thy due to the error message parameter it takes, and Predicate and Enum do not import String. As I am not familiar with the HOL import graph, I don't know whether one could easily change it such that Code.abort is available in Predicate and Enum. But even if it is, this is probably not going to happen before the release. Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Some proposed extensions to the Isabelle library
Hello,The attached file contains a fairly heterogeneous collection of potential extensions to the Isabelle library, which I've been developing as part of some projects that I'm working on. I think that other Isabelle users may find them useful.Please let me know if you'd rather receive these in smaller chunks, if anything needs more explanations, if anything should be changed to conform to Isabelle library styles/conventions, etc.I also have a general question about library vs. AFP. There seem to be clear cases of things that should go into the library (e.g. new theorems on lists or sets) and clear cases of things that should go into the AFP (e.g. a theory of context-free grammars). But some cases are less clear to me; for example, while lattices are in the library, I noticed that categories are in the AFP (well, categories are used much less frequently than lattices, so perhaps that's a criterion). More concretely, I've been working on a couple of developments (not included in the attached file) that I can imagine going into either place:A theory of indexed products, modeled via maps and also modeled via functions.A theory of ranges over orders/lattices, part of which use the indexed products mentioned above.Does anybody have any guidance? Out of curiosity, have theories ever moved between library and AFP, in either direction?Thank you in advance and best regards. ProposedLibraryExtensions.thy Description: Binary data smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
