Poly/ML February 2016

polyml@lists.polyml.org

7 participants
9 discussions

linking polyML modules to C
by dtopham＠gmail.com 09 Nov '18

09 Nov '18

After more experimenting with GUI in SML, I would like to now try calling an SML module from a C program. That way, the GUI could be built using traditional imperative techniques and the program logic could be written in SML. I see how to call a C function from SML, but and not so clear on how to call an SML function from a C program. I want to build code using polyc and then link with a C main program, but could anyone show me a simple example of calling that function and getting its return value? for example, I have defined: fun sum i n f = if i > n then 0.0 else f i + sum (i+1) n f ; fun int2real x = real x ; in linkToC.sml and #include <iostream> #include <fstream> std::ofstream ofs; int main() { std::cout << sum(1,10,int2real) << std::endl; ofs.open("table.dat"); for(int i = 0; i < 20; i++) ofs << i << '\t' << sum(1,i,int2real) << std::endl; } in linkToC.cpp Looking in the polyc script, I thought adding the -c option might allow me to build the object code which I could then link to the sml functions, but it complains about not having a main. Could someone point me in the right direction? Thanks, Dave On Mon, Dec 15, 2014 at 11:44 AM, David Topham <dtopham at gmail.com> wrote: > David, Thank you so much! I really appreciate your help with this. Your > sample below builds fine with polyc on my system (PolyML 5.5.2). I am using > a minimal Linux distribution named TinyCore ( > http://distro.ibiblio.org/tinycorelinux/) which comes with OpenMotif > 2.3.3 It runs in a virtual machine within another computer only taking up > a few hundred MBs! > > I am going to use it to help my students explore Discrete Math next > semester (this textbook uses SML for that purpose: > http://cs.wheaton.edu/~tvandrun/dmfp/). > > I also found a reasonably current project using PolyML and Motif here: > http://www.lemma-one.com/ProofPower/index/ > > ...however it was built on PolyML 4 and has not yet been ported to the > newer version (e.g. depends on PolyML.commit which no longer seems to be > supported). > > Happy Holidays to everyone in the PolyML community! > > -David Topham > > >> Re: GUI Interface (David Matthews) >> >> I've experimented with building a stand-alone executable with Motif and >> succeeded in getting it to work for me using polyc. (It required >> building Poly/ML with --with-x). I took the example from >> http://www.polyml.org/docs/Motif.html and wrapped it up in a function. >> I did find a problem, though. It looks as though the function has to >> suspend itself with something like Posix.Process.pause otherwise nothing >> happens. I seem to recall that the Motif stuff is handled on a separate >> thread to allow the REPL to continue to accept commands. With a >> stand-alone application there isn't a REPL so without the "pause" it >> terminates immediately. >> >> David >> >> open XWindows ; >> open Motif ; >> >> fun main() = >> let >> val shell = >> XtAppInitialise "" "xed" "Editor" [] [XmNwidth 400, XmNheight 400] ; >> >> val main = XmCreateMainWindow shell "main" [] ; >> >> val bar = XmCreateMenuBar main "bar" [] ; >> >> val fileMenu = XmCreateCascadeButton bar "file" [XmNlabelString "File"] ; >> val editMenu = XmCreateCascadeButton bar "edit" [XmNlabelString "Edit"] ; >> val viewMenu = XmCreateCascadeButton bar "view" [XmNlabelString "View"] ; >> val helpMenu = XmCreateCascadeButton bar "help" [XmNlabelString "Help"] ; >> >> val command = XmCreateText main "command" [XmNeditMode >> XmSINGLE_LINE_EDIT] ; >> >> val hscroll = XmCreateScrollBar main "hscroll" [XmNorientation >> XmHORIZONTAL] ; >> val vscroll = XmCreateScrollBar main "vscroll" [XmNorientation >> XmVERTICAL] ; >> >> val work = XmCreateDrawingArea main "work" [] ; >> in >> >> XtManageChildren [fileMenu, editMenu, viewMenu, helpMenu] ; >> XtManageChildren [bar, command, hscroll, vscroll, work] ; >> >> XmMainWindowSetAreas main bar command hscroll vscroll work ; >> >> XtManageChild main ; >> XtRealizeWidget shell; >> Posix.Process.pause() >> end; >> >> >> ------------------------------ >> >> _______________________________________________ >> polyml mailing list >> polyml at inf.ed.ac.uk >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> End of polyml Digest, Vol 110, Issue 12 >> *************************************** >> >> -- >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336. >> >>

2 3

Reducing the size of on-disk saved state
by matthew.fernandez＠gmail.com 31 Mar '16

31 Mar '16

Hi Poly folk, I am an Isabelle/HOL user interested in reducing the on-disk size of my Isabelle/HOL heaps. These are read and written via the save state functionality in Poly/ML. Saved states compress very well via conventional algorithms. On a representative Isabelle/HOL heap I see the following: $ ls -lh -r--r--r-- 1 matthew matthew 1.7G Feb 10 11:22 MyHeap -r--r--r-- 1 matthew matthew 279M Feb 10 11:22 MyHeap.bz2 -r--r--r-- 1 matthew matthew 331M Feb 10 11:22 MyHeap.gz -r--r--r-- 1 matthew matthew 173M Feb 10 11:22 MyHeap.xz I would like to propose integrating compression into the save state functionality itself. The runtime of Bzip and XZ are probably slow enough to irritate some users, but Gzip is reasonably fast for the benefit it shows. Gzipping saved states would require linking against zlib or something similar. David Matthews has suggested the save state code detect whether a state is compressed or not on loading and act accordingly, which would provide a nice transition path for users with existing saved states. I'm interested in hearing others' opinions about this proposal. If we feel this is something reasonable to do, I'll work on implementing this. When replying to this email, please CC me directly as I'm not subscribed to the list. Thanks, Matthew

5 15

Fixed precision int and compatibility
by David.Matthews＠prolingua.co.uk 24 Feb '16

24 Feb '16

Thanks for the various comments on fixed precision integer. I've now implemented two different mechanisms for compatibility with arbitrary precision int. There is a configure option --enable-intinf-as-int. This causes polyimport to build the basis library with int as arbitrary precision integer rather than fixed precision. The second mechanism is to build a module. Calling PolyML.loadModule "IntAsIntInf"; loads a module that sets the compiler's default overloading to arbitrary precision and loads replacements for most of the basis library. I added modules to Poly/ML 5.6 as a way of providing extensions to the existing basis library and this is the first example. Note that this assumes that "poly" has been installed using "make install" and the module has been copied to its installation location. If you're testing it within the build tree you need PolyML.loadModule "modules/IntAsIntInf/IntAsIntInf"; There are a few cases that aren't covered but they are only likely to affect a few people. Specifically, when installing pretty printers the "depth" argument is always FixedInt.int. There may be a few other case where functions are tightly integrated into the compiler. The IntAsIntInf module covers most of the basis library but currently excludes socket IO and a few other cases. It can probably be extended as necessary. David

2 2

Poly/ML on Stackoverflow
by makarius＠sketis.net 18 Feb '16

18 Feb '16

Dear friends of the best unknown programming language on the planet. Someone with sufficiently many points on Stackoverflow has recently created a "polyml" tag. I have already brushed up its wiki http://stackoverflow.com/tags/polyml/info and added the tag to some existing questions. Often there is the odd situation that people ask questions about "ml" or "sml" and can only think of "smlnj" as the one and only implementation. People on this mailing list should know better, and are invited to populate the "polyml" section of Stackoverflow further. (It has presently 2 followers and 18 questions.) It is also possible to vote for questions and answers that are relevant for Poly/ML, and thus improve its visibility. Makarius

2 1

Fixed precision int
by David.Matthews＠prolingua.co.uk 10 Feb '16

10 Feb '16

Anthony, I'm copying the mailing list to my replies because this is of general interest. On 10/02/2016 16:02, Anthony Fox wrote: > I just occurred to me that I could have done: > > structure Int :> INTEGER = IntInf > > if I wanted IntInf everywhere (rather than having the choice of fixed ot arbitrary). I still think it would be nice to have a command line option for this? At the very least, this way of getting the old behaviour should be advertised. > That would work if you use the Int structure but there are lots of places that pick up the default "int". For instance, if you have an overloaded function: fun f x y = x+y; that will fall back to the default "int". Also, all the library functions that use "int" e.g. Array.sub, String.size, List.length or TextIO.inputN, will still have the fixed precision int. I'm inclined to think that having a "configure" option would be the answer. David

3 3

Fixed precision int
by David.Matthews＠prolingua.co.uk 10 Feb '16

10 Feb '16

On 10/02/2016 16:18, Anthony Fox wrote: >> Can you provide some more information and try to narrow the problem down? There certainly shouldn't be bus errors or segmentation faults anywhere. > > I removed the files > > $POLYDIR/lib/libpoly* > > before doing an Poly/ML install and that seemed to fix things. OK. The libraries have the same version number as the last release so that may cause problems. I seem to recall reading that one was supposed to increment the version number just before a release but maybe it would be better to increment the version immediately after so that versions from git always have a different version from the last release. David

1 0

Fixed precision int
by David.Matthews＠prolingua.co.uk 10 Feb '16

10 Feb '16

On 10/02/2016 15:41, Anthony Fox wrote: > This is significant change. Would it be possible to make this user selectable? MLton has the command line flag > > -default-type intinf > > when IntInf is preferred for Int. Perhaps there could be a switch to "configure". It's really a question of how the basis library is built. > I had been programming on the basis that Int was arbitrary precision in Poly/ML. I certainly need IntInf in places and it was very convenient to not have to worry about this sort of thing. Having to use ?to? and ?from? functions is a nuisance. I?ve attempted to update my code for this change and the diff was > > 19 files changed, 334 insertions(+), 275 deletions(-) > > In itself this wasn?t too bad. However, after this I have less confidence in the robustness of the code. Poly/ML programmer?s have not needed to insert ?handle Overflow? before now, which is great advantage over ?performance obsessed? compilers. > > Anyhow, HOL4 doesn?t build using the FixedPrecisionInt branch. An early problem was due to Position.int no longer being the same as Int.int. Then I got a > > Segmentation fault: 11 > > error when trying to build a parser. This problem may be related to > > Bus error: 10 > > errors that I?ve been getting. For example, if I use polyc to compile > > val main = PolyML.rootFunction > > then the resulting program gives this bus error when trying to process anything (such as ?val x = 1;?). Can you provide some more information and try to narrow the problem down? There certainly shouldn't be bus errors or segmentation faults anywhere. David

1 0

Fixed precision int
by David.Matthews＠prolingua.co.uk 10 Feb '16

10 Feb '16

From the start int in Poly/ML has been arbitrary precision. After around thirty years I think it's time to make a change. The current plan is to introduce a fixed precision integer type and use that as the default int. Arbitrary precision will remain as LargeInt.int/IntInf.int. The reason for the change is that it is becoming clear that having arbitrary precision int as the only integer type imposes restrictions on the code both as regards the integer type itself but also more widely. The arbitrary precision type in Poly/ML is implemented using a tagged representation. Small values that will fit in 31/63 bits are represented as the value shifted one bit left and with the bottom bit set. Larger values are represented as pointers to arrays of bytes, either in the GMP format or Poly's own format. Since pointers are always word-aligned it's possible to distinguish the two forms by looking at the bottom bit. The "tag-bit" also serves another purpose. The garbage-collector can use it to distinguish pointers from non-pointers so all non-pointer values, e.g. bool, char and word, are represented using the tagged form. Arbitrary precision operations are handled directly by the code-generator. The idea is that when the values are small, as they usually are, the machine can execute the appropriate instruction directly. For example, addition is generated as an add instruction. It is preceded by a test on the tags and followed by a test for overflow. If the arguments were not tagged or the result overflowed there is a call into the run-time system. This emulates the instruction and returns with the result in the correct register. Emulation has limitations. Currently only (in)equality, comparison, addition and subtraction are emulated. Other operations such as multiplication and division involve calls to assembly code. This means that code that makes significant use of arithmetic incurs overheads even if it only ever uses small values. There is also a more subtle cost. Because emulating addition and subtraction could involve allocating memory on the heap for the long-format result every addition and subtraction could result in a garbage-collection. This means that the registers, which could be holding intermediate results, have to be treated as the roots for the GC. That in turn means that they must always contain either valid pointers or tagged values. This sometimes involves adding extra instructions simply to ensure this is the case. It also means that whenever the code returns from the run-time system to ML all the registers have to be loaded with known values, adding to the cost of a RTS call. The plan is to retain the existing arbitrary precision using the current tagged values but remove emulation. All arbitrary precision operations will involve an ML function call to the assembly code. This will compute the result directly if it is short and call into the run-time system if it is long. This is actually likely to faster than the current scheme if the values are long. Some cases, for example equality between an arbitrary precision value and a short constant, can continue to be handled by the code-generator since they do not require emulation. Fixed precision int will be based on the current short format i.e. 31 bits on 32-bit machines, 63 bits on 63-bit machines. Operations on these can be handled directly by the code-generator. These changes are currently being tested in the FixedPrecisionInt branch. This requires at least one, preferably two, calls to "make compiler" to build a version of the compiler that generates fixed precision operations. For backwards compatibility it does not yet gain all the advantages of the change; in particular it still clears all the registers on return from the run-time system.

1 0

ML debugging within Isabelle/PIDE
by makarius＠sketis.net 04 Feb '16

04 Feb '16

Dear users of the best unknown programming language in the world. Isabelle/ML is based on Poly/ML and thus benefits from the source-level debugger of that implementation of Standard ML. The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context. More explanations with a screenshot on http://sketis.net/2016/ml-debugging-within-the-prover-ide Makarius

2 11

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML February 2016