Poly/ML March 2015

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

Inspecting structures
by ramana.kumar＠gmail.com 27 Jan '16

27 Jan '16

Is there a way to look at the contents (i.e. signature) of a structure without opening it? (I suppose you could just open it then call a lot of PolyML.Compiler.forgetXXX, but that's quite tedious) Also, is it possible to retrieve the long path of an identifier in scope? Something that will, for example, take the rev in scope and say that it came from List. Finally, what about searching for an identifier that would come into scope if you opened some structures?

3 5

error building from SVN
by Michael.Norrish＠nicta.com.au 11 Aug '15

11 Aug '15

My Travis CI builds of HOL using a Subversion checkout of Poly (as opposed to the released version, which I also check), are failing to build Poly with the error below. (See also https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/56529081). Is this expected, or some quirk of the Travis setup? Michael -- Error- in './basis/FinalPolyML.sml', line 1607. Value or constructor (decodeBinary) has not been declared Error- in './basis/FinalPolyML.sml', line 1608. Value or constructor (encodeBinary) has not been declared Exception trace for exception - Fail raised in mlsource/MLCompiler/MAKE_.ML line 423 MAKE_().useIntoEnv(2) <top level> CODETREE().genCode(3)(1) COMPILER_BODY().baseCompiler(3)executeCode(1) End of trace Exception trace for exception - Fail raised in mlsource/MLCompiler/MAKE_.ML line 423 MAKE_().useIntoEnv(2) <top level> CODETREE().genCode(3)(1) COMPILER_BODY().baseCompiler(3)executeCode(1) End of trace ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

9 18

polyc and poly --script
by rene.neumann＠in.tum.de 24 Mar '15

24 Mar '15

Hi, two completely orthogonal questions/remarks for PolyML 5.5.1: 1.) When building PolyML with '--with-system-libffi' the '-lffi' part is missing in the linker line in polyc. 2.) Is it somehow possible to see if an ML file is run via 'poly --script' or as a standalone executable? Because for the one the logic has to be wrapped in 'fun main ()', and for the other it should not :). (Ie, what I want: if is_script then main() else () ) Thanks, Ren? -- Ren? Neumann Institut f?r Informatik (I7) Technische Universit?t M?nchen Boltzmannstr. 3 85748 Garching b. M?nchen Tel: +49-89-289-17232 Office: MI 03.11.055

4 9

emacs SML mode
by dm＠prolingua.co.uk 20 Mar '15

20 Mar '15

Peter, I'm copying this to the Poly/ML list as you suggested. It would be nice to have SML emacs mode working with Poly/ML for those who would like to use it but my feeling is that it is rather old-fashioned. Poly/ML now supports a much more extensive interface designed for an IDE. The best example of this is Isabelle's ML mode. See http://sketis.net/2014/isabellepide-as-ide-for-standard-ml which has a nice screen-shot. Lucas Dixon and I both had a go at producing IDEs which were completely independent of Isabelle but we didn't get as far as Makarius has. It all works by having the Poly/ML compiler as a function which takes a large set of parameters most of which have simple defaults. All the interaction with the compiler is through ML functions. The default REPL just calls the compiler with streams connected to the console but it's very easy for a user to replace the REPL with something else. The Isabelle IDE is just using the Poly/ML compiler function but passing in parameters which capture error messages and also allow browsing of the parse-tree to get information about the types. So far the debugger hasn't been fully integrated with this but it's something I have in mind. The format that the default REPL uses for error messages was one that was used by various compilers at one time and it used to be possible to parse it automatically. If there's a more up-to-date format I'm happy to change to it. I don't know if anyone is parsing the current format automatically and would be inconvenienced by a change. David On 03/12/2014 03:26, Peter Gammie wrote: > Dave, > > I?ve been talking to Stefan about the SML mode for emacs that he > maintains. I?m hoping to use it with Poly/ML and it is starting to > come together. > > Stefan observed that it would be super-helpful if Poly/ML generated > errors in a standard format, such as e.g. the one that GCC or clang > use, as far as that makes sense. > > Would you be open to that? I could try to crank out some patches to > Poly/ML if so. > > BTW I am wondering how people interact with Poly/ML?s repl. With more > hacking it is likely to be somewhat emacs-friendly, but I?m still > struggling to understand how people have done it in the past. > > For instance, I presently more-or-less just load all modules into > poly with a series of ?use?s in dependency order. Now I?d like to use > the debugger and it seems I have to hack all this scaffolding to do > so. From the looks of it Isabelle does the same. > > Feel free to reply via the Poly/ML list if you prefer. > > Thanks for the awesome system. I hope I can make some use of the > concurrency! > > thanks, peter >

9 17

forgetVal(ue)
by peteg42＠gmail.com 15 Mar '15

15 Mar '15

David, I?ve been trying to repurpose your Poly/ML test harness, that encapsulates the tests in private namespaces. With some head scratching I got it to somewhat work, so thanks for that. One remaining nit is that the treatment of forgetVal(ue) does not take into account the current namespace. Did you have a reason for leaving it out of the PolyML.NameSpace.nameSpace record? cheers, peter

2 1

Typo in Socket.select
by hiroya.ebine1＠gmail.com 11 Mar '15

11 Mar '15

In Poly/ML source code, polyml/basis/Socket.sml, Socket.select function declared like this: val select: { rds: sock_desc list, wrs : sock_desc list, exs : sock_desc list, timeOut: Time.time option } -> { rds: sock_desc list, wrs : sock_desc list, exs : sock_desc list } But, basis library says: select {rds, wrs, exs, timeout} (http://sml-family.org/Basis/socket.html#SIG:SOCKET.select:VAL) It seems a typo. Argument "timeOut" shoud be "timeout". Please fix it or tell me where post a patch. Sorry for poor english. Thank you.

2 1

Debugging the debugger
by Brian.Campbell＠ed.ac.uk 07 Mar '15

07 Mar '15

Hi, I've encountered a few bugs when using the debugger, and I've managed to distill them down into a useful form. The first is that the compiler is too keen to avoid multiple calls to the debugger in one line. For example, if I debug the function below, 1 fun f n = 2 let val l = [1,2,3,4] 3 val x = map (fn y => y+n) l 4 in x 5 end then stepOver() will skip line 3, because the compiler places the only call to the debugger inside the anonymous function. I've been working around this by adding an extra newline after map. The second is that when support was added to stop execution when an exception is raised, it used the same code as when an exception exits a function, and pops an extra entry off the debug stack. The stepOver and stepOut functions get very confused as a result. I've hacked my copy to check whether the name ends in -raise before popping the stack, but there's probably a more elegant solution. Finally, the tracing doesn't seem to like datatypes declared inside structures: structure S = struct datatype t = A of int fun f (x:t) = x; end; > PolyML.Debug.trace true; val it = (): unit > S.f (S.A 5); S.f Exception- Subscript raised I can examine the value of x in the debugger, though, but my attempts to make the way tracing prints values more like the debugger toplevel haven't been successful. Best regards, Brian

2 1

extremely bad performance on some mllex generated code
by michael.norrish＠nicta.com.au 03 Mar '15

03 Mar '15

(I'll attempt to attach the tgz file to this message, but if 817KB is too big and this bounces or the attachment is dropped, I'll make it available separately.) If compiled with Poly/ML, the attached program performs abysmally on the provided testcase.sml input file. Within seconds of beginning, it attempts to allocate more memory than my machine has (16GB), and basically brings it to its knees. If compiled with mlton, the testcase doesn't seem to cause any obvious memory allocation, and finishes in less than a second. You can also compile with Moscow ML, though I haven?t included the build instructions in the Makefile. The execution of the mosml executable doesn't seem to allocate any memory either, and it terminates cleanly (after 17s). Though slow this is still preferable to Poly/ML's behaviour. This is with Poly/ML 5.5.2 on > Linux telemachus 3.2.0-75-generic #110-Ubuntu SMP Tue Dec 16 19:11:55 UTC 2014 x86_64 x86_64 x86_64 GNU/Linux The Makefile generates two executables (if you have mlton and poly in your PATH): pholdeptool and mholdeptool. You can run them on the testcase, e.g.: pholdeptool testcase.sml The lexer code looks to me to be tail-recursive, and the program only accumulates a binary tree containing 15 strings. So it really does seem as if Poly/ML is doing something buggy. (The program is lexing the test-case (which uncompresses to a 30MB file) in an extremely simple way, but performing a useful analysis.) Michael

2 3

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 March 2015