Poly/ML

polyml@lists.polyml.org

2 participants
711 discussions

a couple of how-tos
by Michael.Norrish＠nicta.com.au 27 Feb '08

27 Feb '08

I'm playing with porting HOL4 from Moscow ML to PolyML, and have found it a reasonably pleasant task so far (Moscow ML's out-of-date Basis Library is the major annoyance). However, there are a couple of things I don't quite see how to do: * how do I install a pretty-printer in my top-level loop so that my special data-types get printed nicely? Moscow ML offers Meta.installPP, and my scouring of the mailing list suggests I might use RunCall.Inner.install_pp. This is of type ((string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) -> int -> 'a -> 'b -> unit) -> unit What do the various parameters given to the printing function mean? The first emits actual text, and the int is perhaps the linewidth, but what about the others? * Is there a way of doing a pointer-equality comparison on arbitrary values in order to give an efficient approximation of normal equality? In MoscowML there's an Obj.magic that can be used to turn 'a into an int (the underlying pointer I think). Is there something similar I can use in Poly? Many thanks, Michael.

2 1

a how-to answered already
by Michael.Norrish＠nicta.com.au 27 Feb '08

27 Feb '08

I see there is a PolyML.pointerEq.. Michael.

1 0

Re: Compiling PolyML on Windows
by David.Matthews＠prolingua.co.uk 19 Feb '08

19 Feb '08

Dave Berry wrote: > I've just downloaded PolyML to have a play about with it. What do I > need in order to compile it on Windows? I see from the docs that it > uses standard GNU tools, so do I need Cygwin plus the GNU C++ compiler? Hi Dave, I'm copying this to the Poly/ML mailing list since it may be of wider interest. You basically have three options for building Poly/ML on Windows. 1. Cygwin. You can build it in Cygwin, which essentially provides a Posix environment on Windows. In particular it supports signals which aren't a Windows concept. When built on Windows Poly/ML has to be run within a shell. 2. Mingw+Msys. Mingw contains the GNU compiler for Windows. Msys provides a shell for Mingw so that the configure script will run. This builds Poly/ML as a native Windows application which has a simple GUI. 3. Microsoft C++. The Poly/ML source includes a Visual C++ 6.0 workspace and project. This can be used to build a native Windows application. Poly/ML also requires the Microsoft assembler, MASM. I think there are versions of Microsoft C++ and MASM that can be downloaded free of charge for personal use. Which of these is easiest depends on what you already have and also what environment you are building for. David.

1 0

CPU timers in polyml
by Brian.Campbell＠ed.ac.uk 16 Feb '08

16 Feb '08

Hello everyone, I'm using the Timer structure from the basis library to measure the CPU time used during execution. Comparing the times returned by Timer.checkCPUTimes with those reported by the shell, the nongc times look suspiciously like they include the gc times as well. Shouldn't these be subtracted? Thanks, Brian Campbell

2 1

C finalizers or weak pointer mechanism?
by jstanley＠galois.com 15 Feb '08

15 Feb '08

Hello everyone, I'm currently attempting to interact with a C library via the CInterface. So far so good, but there are times when the C functions I invoke do allocation in the C heap. Is there a finalizer registration mechanism available in Poly/ML that I can use to invoke appropriate tear-down functions in the C library when Poly/ML is done with the wrapped vol? If not, is there a weak pointer mechanism available that would allow me to accomplish the same? References to some example code that does this would be ideal (and appreciated) in either of the above cases. Thanks much, Joel Stanley jstanley(a)galois.com

4 4

Re: Interrupts in Poly/ML 5.1
by David.Matthews＠prolingua.co.uk 10 Feb '08

10 Feb '08

Rob, I'm copying this to Poly/ML mailing list since I think there are issues here that may affect other users. The handling of console interrupt (control-C, SIGINT) changed quite significantly in 5.1 as a result of changing from a single threaded model to multiple threads. It's complicated because there are significant differences in the way Mac OS X and Linux handle signals with multiple threads. Since there may be Isabelle users reading this it's worth pointing out that Isabelle replaces the default Poly/ML SIGINT handler with its own handler using Signal.signal. This uses Thread.Thread.broadcastInterrupt to send an Interrupt exception to all the threads, effectively the same as using the "f" option in the default handler. I removed the "s" option from the handler since ultimately this depended on the old "Process" mechanism for parallelism. The alternative top-level shell worked by having a second list of runnable processes and the effect of typing "s" in the control-C handler was to switch between these. With the current thread mechanism the run queue is handled by the kernel so this didn't really make sense and I couldn't see how to handle sub-shells with the new mechanism. The other problems are to do with the way signals are handled when there are multiple threads. Even if there is only a single ML thread and the Thread structure is not used Poly/ML is actually running at least two threads. The "main thread" is responsible primarily for garbage collection and is normally blocked waiting the ML code, which runs on a separate thread. When control-C is pressed the operating system sends the SIGINT to one of these threads. In Mac OS X, in particular, it always sends the signal to the main thread. The ML thread continues to run in parallel. While I was writing this I realised that there was a possible solution to the problems that this created and which you noticed. Previously the handler for SIGINT actually ran the loop that read from the terminal and looked at the "f", "c", "q", "t" etc codes. I've now changed this so that when SIGINT arrives it simply sets a flag. Some time later one of the ML threads (which one is indeterminate) runs the default console interrupt handler if an alternative one has not been set up. This allows the "t" (traceback) option to work since it is actually running on an ML thread. It also avoids the race conditions that arise if both the interrupt handler and the ML code are reading from the terminal at the same time, but only if the thread that runs the interrupt handler is the same as the one reading from the terminal. That will, of course, be the case if there is only one ML thread. This is still quite messy. I would prefer to get rid of the default interrupt handler that reads from the terminal altogether and switch to requiring the user to set up a handler for SIGINT using the Signal structure. Regards, David. Rob Arthan wrote: > David, > > Thanks for the prompt fix. In fact, I should confess that my current > approach in ProofPower only uses the length of the hierarchy list and > not the values of the strings in it, so I don't actually need the fix at > the moment. > > ProofPower now builds and tests on Poly/ML 5.1 on both Linux and Mac OS > X, but I have some problems with keyboard interrupts. First of all two > comments, I note that the s(witch) command is no longer available and it > seems as if the t(race) command is never able to print a trace. > > On both OSs the f(ail) and q(uit) command seem to behave differently > from 4.2.0. There is also a separate problem on Mac OS X when an > interrupt arrives while poly (or my executable with the read-eval-print > loop tailored for ProofPower) is waiting for input rather than > excecuting a function. I need to do some more investigation into the > common problem, so the rest of this e-mail is about the Mac OS > X-specific problem. (As I am using Mac OS X version 10.3.9 which is a > bit long in the tooth, I am wondering whether Poly/ML 5.1 just isn't > supported on it). > > Here is the sort of thing that happens (this is copied out of Terminal > with "\n"s added by me to show where I had to hit return to make > something happen): > > rda]- poly > Poly/ML 5.1 Release > > ^C > =>?\n > # ;\n > Error: Value or constructor (?) has not been declared Found near ? > > Static errors (pass2) > > > ^C\n > > ^D\n > =>?\n > Type q(uit - Exit from system) > c(ontinue running) > f(ail - Raise an exception) > or t(race - Get a trace of calls) > =>rda]- > > On the last line of the above, I didn't type anything: the "=>" prompt > appeared and I just waited a few seconds and then poly exited (which > would also have happened if I hadn't typed the second "?" fairly > quickly). It feels as if there are two separate threads responding to > keyboard gestures in an uncoordinated way. > > Regards, > > Rob.

2 1

How to return void from a callback function
by homma＠gf6.so-net.ne.jp 31 Dec '07

31 Dec '07

Hi, I wrote a program(glut01.sml) that uses GLUT library through Poly/ML's CInterface infrastructure on Mac OS X. But it doesn't work. It aborts with an IOException after "glutDisplayFunc". An execution log(glut-exec.log) and an error message (glut-error.log) are attached. I thought there are some problems around the callback function. So I wrote 2nd program(glut02.sml). As you see, I changed the "glutDisplayFunc" to accept a function that returns "LONG" (which is wrong by the definition of the original function) instead of "VOID". And it works fine(does not abort). Also, I wrote some test code(prog01.c, prog01.sml) those have the same problem as glut01.sml. And a wrong "fixed" version(prog02.c, prog02.sml) that works as I intent. What is the right way to write a callback function that returns (void) without writing it as returning long value? best regards, Daisuke Homma

2 2

funny error: not a type construction
by itz＠madbat.mine.nu 28 Dec '07

28 Dec '07

I get this: Exception- Fail "Invalid type (not a type construction)" raised The context: I run a toplevel built by compiling Vesa Karvonen's "extended-basis" library and doing PolyML.export (_, PolyML.rootFunction). Into this toplevel I load the enclosed Word31 module. My guess is this happens because extended-basis rebinds some basis types which are normally special-cased by the poly pretty-printer, but aren't recognized as special anymore after the rebinding. Anyway, it works ok with the normal poly. Who's to "blame"? And is there a workaround? structure Word31 :> WORD = struct infix 8 << >> ~>> type word = Word32.word val wordSize = 31 val toLarge = Word32.toLarge val toLargeWord = toLarge fun toLargeX w = let open Word32 in if andb (w, 0wx40000000) = 0wx0 then toLargeX w else toLargeX (orb (w, 0wx80000000)) end val toLargeWordX = toLargeX fun fromLarge wl = let open Word32 in andb (fromLarge wl, 0wx7fffffff) end val fromLargeWord = fromLarge val toLargeInt = Word32.toLargeInt fun toLargeIntX w = let open Word32 in if andb (w, 0wx40000000) = 0wx0 then toLargeIntX w else toLargeIntX (orb (w, 0wx80000000)) end fun fromLargeInt i = let open Word32 in andb (fromLargeInt i, 0wx7fffffff) end val toInt = Word32.toInt fun toIntX w = let open Word32 in if andb (w, 0wx40000000) = 0wx0 then toIntX w else toIntX (orb (w, 0wx80000000)) end fun fromInt i = let open Word32 in andb (fromInt i, 0wx7fffffff) end val andb = Word32.andb val orb = Word32.orb val xorb = Word32.xorb fun notb w = let open Word32 in andb (notb w, 0wx7fffffff) end fun w << i = let open Word32 in andb (w << i, 0wx7fffffff) end val op >> = Word32.>> fun w ~>> i = let open Word32 in if andb (w, 0wx40000000) = 0wx0 then w ~>> i else orb (w ~>> i, 0wx40000000) end fun w1 + w2 = let open Word32 in andb (w1 + w2, 0wx7fffffff) end fun w1 - w2 = let open Word32 in andb (w1 - w2, 0wx7fffffff) end fun w1 * w2 = let open Word32 in andb (w1 * w2, 0wx7fffffff) end val op div = Word32.div val op mod = Word32.mod val compare = Word32.compare val op < = Word32.< val op > = Word32.> val op <= = Word32.<= val op >= = Word32.>= fun ~ w = let open Word32 in andb (~ w, 0wx7fffffff) end val min = Word32.min val max = Word32.max val fmt = Word32.fmt val toString = Word32.toString fun scan radix getc strm = let open Word32 in case scan radix getc strm of NONE => NONE | res as SOME (w, strm') => if andb (w, 0wx80000000) = 0wx0 then res else raise Overflow end val fromString = StringCvt.scanString (scan StringCvt.HEX) (* the rest is for building on top of Vesa Karvonen's mltonlib extensions *) type largeable_large = LargeWord.word type bitwise = word val numBytes = 4 local fun mk idx w = Word8Vector.tabulate (numBytes, fn i => (Word8.fromLarge o LargeWord.>>) (toLarge w, Word.<< (Word.fromInt (idx i), 0w3))) in val toBigBytes = mk (fn i => Int.- (Int.- (numBytes, 1), i)) val toLittleBytes = mk (fn i => i) end val toWord8 = Word8.fromLarge o toLarge val toWord8X = toWord8 val fromWord8 = fromLarge o Word8.toLarge val fromWord8X = fromLarge o Word8.toLargeX local fun mk fold bs = if numBytes <> Word8Vector.length bs then raise Subscript else fold (fn (b, w) => Word32.orb (Word32.<< (w, 0w8), fromWord8 b)) (Word32.fromInt 0) bs in val fromBigBytes = mk Word8Vector.foldl val fromLittleBytes = mk Word8Vector.foldr end val isoWord8 = (toWord8, fromWord8) val isoWord8X = (toWord8X, fromWord8X) val toWord = Word.fromLarge o toLarge val toWordX = Word.fromLarge o toLargeX val fromWord = fromLarge o Word.toLarge val fromWordX = fromLarge o Word.toLargeX val isoWord = (toWord, fromWord) val isoWordX = (toWordX, fromWordX) val toFixedInt = Int32.fromLarge o toLargeInt val fromFixedInt = fromLargeInt o Int32.toLarge val toFixedIntX = Int32.fromLarge o toLargeIntX val isoFixedInt = (toFixedInt, fromFixedInt) val isoFixedIntX = (toFixedIntX, fromFixedInt) val isoLarge = (toLarge, fromLarge) val isoLargeInt = (toLargeInt, fromLargeInt) val isoLargeX = (toLargeX, fromLarge) val isoLargeIntX = (toLargeIntX, fromLargeInt) val isoInt = (toInt, fromInt) val isoIntX = (toIntX, fromInt) val isoLargeWord = isoLarge val isoLargeWordX = isoLargeX val isoBigBytes = (toBigBytes, fromBigBytes) val isoLittleBytes = (toLittleBytes, fromLittleBytes) fun op == (w1, w2) = w1 = w2 fun op != (w1, w2) = w1 <> w2 fun inRange (w1, w2) w = if w1 > w2 then raise Domain else w1 <= w andalso w <= w2 fun isEven w = (w andb 0wx1) = 0wx0 fun isOdd w = (w andb 0wx1) = 0wx1 fun isZero w = w = 0wx0 type bounded = word type bounded_ex = word val minValue = 0wx0 val maxValue = 0wx7fffffff val largestPrime = maxValue val bounds = (minValue, maxValue) type formattable = word type scannable = word type intable = word type largeable = word type equality = word type equality_ex = word type ordered = word type ordered_ex = word type shiftable = word type stringable = word type stringable_ex = word type wordable = word type formattable_format = StringCvt.radix type scannable_format = StringCvt.radix val embString = (toString, fromString) type t = word end (* Because we are using opaque signature matching we have to install type-dependent functions OUTSIDE the structure. *) local open RuntimeCalls structure Conversion = RunCall.Run_exception1 ( type ex_type = string; val ex_iden = EXC_conversion ); exception Conversion = Conversion.ex; (* The string may be either 0wnnn or 0wxXXX *) fun convWord s : Word31.word = let val radix = (* The word value must consist of at least 0w and a digit. *) if String.sub(s, 2) = #"x" then StringCvt.HEX else StringCvt.DEC in case StringCvt.scanString (Word31.scan radix) s of NONE => raise Conversion "Invalid word8 constant" | SOME res => res end (* Install the pretty printer for Word31.word *) fun pretty(p, _, _, _) _ _ x = p("0wx" ^ Word31.toString x) in val it: unit = RunCall.addOverload convWord "convWord" val it: unit = RunCall.Inner.install_pp pretty end; (* Add the overloaded operators. *) RunCall.addOverload Word31.~ "~"; RunCall.addOverload Word31.+ "+"; RunCall.addOverload Word31.- "-"; RunCall.addOverload Word31.* "*"; RunCall.addOverload Word31.div "div"; RunCall.addOverload Word31.mod "mod"; RunCall.addOverload Word31.< "<"; RunCall.addOverload Word31.> ">"; RunCall.addOverload Word31.<= "<="; RunCall.addOverload Word31.>= ">="; -- Ham is for reading, not for eating.

3 4

Accessing the x from a "SOME x" option datatype expression
by karabot＠gmail.com 22 Dec '07

22 Dec '07

Hello, Isabelle has the following definition under HOL: consts the :: "'a option => 'a" primrec "the (Some x) = x" I am wondering if there is anything equivalent in ML? TIA, George

3 2

Re: Q: meta programming (runtime code generation) in PolyML ?
by David.Matthews＠prolingua.co.uk 17 Dec '07

17 Dec '07

I thought I'd sent this to the list but I put the wrong address and I've only just realised! Basile STARYNKEVITCH wrote: > Does PolyML provide facilities to generate (machine) code at runtime (on > Linux/AMD64 or Linux/x86), either in a type safe way (in the spirit of > MetaML or MetaOcaml) or in a more low level unsafe way (e.g. like LLVM, > Libjit, GNU lightning, ....) No, the best solution is certainly to generate ML code and then run that through the compiler. It might be possible to interact with the compiler at a different level if an interface were provided to do that and there are really two levels where that might be possible. The compiler first parses the source into an abstract syntax tree and then runs over that to do type-checking. After that it generates a second "code tree" from the parse tree. The code tree goes through the optimiser which generates a new, optimised version and feeds this into the machine-dependent code-generator. You can see the results of the various phases by turning on the parsetree, codetree, codetreeAfterOpt and assemblyCode flags in PolyML.Compiler. There's little advantage in generating the abstract syntax tree (parse tree) compared with feeding in ML source directly. Generating the code tree is a possible route in and might be a way to make use of the back-end of the compiler if you had a programming language with a different type system from ML's. Since there's no checking of code tree for type-safety or validity you would be very much on your own. Actually, that was the way the original Poly/ML compiler was developed. Originally, Poly was a compiler for the Poly language written in Poly and the ML part was a separate front end that took Standard ML and generated the code tree. Only much later was the whole thing translated into ML and the Poly compiler removed. David.

1 0

← Newer
1
...
56
57
58
59
60
61
62
...
72
Older →

Jump to page:

2026

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