Poly/ML

polyml@lists.polyml.org

1 participants
698 discussions

Type inference issue using signature constraint
by phil.clayton＠lineone.net 12 Jan '16

12 Jan '16

I have an example where a module is type checking fine even though I have introduced a type error into it! I've reduced it down to a small example. It looks like there is a problem using type constraints from a signature where the signature is also required to resolve record components. See attached example for details. Phil

1 0

addPrettyPrinter type security
by rda＠lemma-one.com 11 Jan '16

11 Jan '16

PolyML.addPrettyPrinter checks its printArgTypes parameter carefully when you are installing a pretty-printer for a polymorphic type. As far as I can see it guarantees type security for polymorphic types. However, when you install a pretty-printer for a monomorphic type, the parameter isn't checked at all. E.g., the following code doesn't result in any error messages and ends by crashing poly. datatype MONO = Mono of int; fun pp_mono1 _ (i : int) (Mono j) = ( PolyML.PrettyString (Int.toString (i + j)) ); PolyML.addPrettyPrinter pp_mono1; Mono 42; (* Prints "val it = 42: MONO" - apparently i was 0 *) fun pp_mono2 _ (r : int ref) (Mono _) = ( PolyML.PrettyString (Int.toString (!r)) ); PolyML.addPrettyPrinter pp_mono2; Mono 42; (* Crashes *) Shouldn't processArgTypes be required to have type unit when defining a pretty-printer for a monotype? The patch below implements this check and tries to improve the error message (which is already a bit misleading if you get something wrong for a type with more than one parameter). Regards, Rob. diff --git a/mlsource/MLCompiler/VALUE_OPS.ML b/mlsource/MLCompiler/VALUE_OPS.ML index 1535d4f..9e00f0d 100644 --- a/mlsource/MLCompiler/VALUE_OPS.ML +++ b/mlsource/MLCompiler/VALUE_OPS.ML @@ -958,8 +958,8 @@ struct val typeVars = List.tabulate(arity, fn _ => mkTypeVar (0, false, true, false)) val tupleType = case typeVars of - [] => (* No arg so we can have anything here. *) - mkTypeVar (generalisable, false, false, false) + [] => (* No arg so must have unit. *) + unitType | [arg] => mkFn arg (* Just a single function. *) | args => mkProductType(List.map mkFn args) val addPPType = mkFunctionType(argPrints, mkFunctionType(installType, pretty)) @@ -970,7 +970,7 @@ struct in checkPPType(addPPType, testType, "addPrettyPrint", lex, loc, fn () => - PrettyString "addPrettyPrint element functions must have type 'a * int -> pretty") + PrettyString "addPrettyPrint element functions must have type 'a * int -> pretty, 'b * int -> pretty, ... with one function for each type parameter") end; (* Only report the error when the function is run. Because addPrettyPrint is

2 1

Towards Poly/ML 5.6
by David.Matthews＠prolingua.co.uk 09 Jan '16

09 Jan '16

I've updated the github repository with pre-built compilers for 5.6 Release. This is now the release candidate. Unless there are any significant problems this will be released in the next few weeks. Best wishes for 2016, David

8 18

5.6 failures on OSX
by Michael.Norrish＠nicta.com.au 08 Jan '16

08 Jan '16

Our regression testing from poly's master branch with sources that are fine on 5.5.2 is showing repeated "random" failures on OSX. You can see the build history at https://travis-ci.org/HOL-Theorem-Prover/HOL/builds (ignore the k11-release-prep branch failures). In all of the recent failures of HOL's master, you'll see that it is the "GITPOLY" build on OSX failing. The GITPOLY build on Linux is fine. Unfortunately, the failures are happening at different times in the build. The only thing they seem to have in common is that there is a test (using OS.Process.isSuccess) of the result of another execution ultimately set up with OS.Process.system. The output even somewhat suggests that the child process terminated successfully; could it be that the return code is being randomly mis-interpreted? Michael ________________________________ 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.

2 2

polyml mailing list not searchable by search engines
by artella.coding＠googlemail.com 28 Dec '15

28 Dec '15

For example : https://encrypted.google.com/search?as_q=&as_sitesearch=http%3A%2F%2Flists.… I personally think it would be better to have the mailing list searchable, either by allowing search engines to have access or having a built in site search. Thanks

1 0

Various changes
by David.Matthews＠prolingua.co.uk 20 Nov '15

20 Nov '15

There have been a number of changes added to the git repository over the last weeks and months. This an almost certainly incomplete list. I've tried to include changes that have come up as queries on the mailing list. Added loadHierarchy to PolyML.SavedState. This takes a list of the file names of saved states in order from grandparent, parent to child, and loads them. It functions the same way as loadState except that it allows the parent paths to be specified. Types in structures with opaque signatures are now printed as "?" rather than the print function being inherited. In the debugger, pressing control-C to the debug> prompt returns to the top-level. Actually, what happens is that break-points are disabled and the Thread.Thread.Interrupt exception is raised in the debuggee so it has a chance to clear up. If the debuggee actually catches the interrupt exception then it may not actually return to the top level. There's also a "locals" function in PolyML.Debug to display the local variables. When compiling a file with "use", PolyML.getUseFileName returns the current file name. The floating point precision is now set to 64-bits to avoid inconsistencies depending on whether an intermediate floating point value has been kept in a register or saved into memory. The PolyML.NameSpace structure has been reorganised to split out functions related to the various binding classes into separate sub-structures. The aim is to wrap up the current changes into a new release, probably 5.6 rather than 5.5.3 since there are quite a few changes. That will probably be over the next month or two. David

2 1

loadModule
by David.Matthews＠prolingua.co.uk 10 Nov '15

10 Nov '15

Some new functions have been added to PolyML.SaveState to support "modules". A module is a collection of bindings, primarily structures, signatures and functors, that can be saved and later reloaded. It's mainly aimed at those packaging up binary distributions since a module can only be reloaded into the same binary that exported it, much as with saved states. PolyML.SavedState.savedModule takes a file name and names of structures, signature and functors, together with an optional "on-start-up" function and writes them out as a package. PolyML.SavedState.loadModule takes a name and loads the module. When the module is loaded the "on-start-up" function is executed and the structures, signatures and functors are added to the top-level name space. The module name can either be a file path if it contains a directory separator e.g. ./foo or it is looked up in the path given by POLYMODPATH. There are lower level functions in SavedState that can be used to include values, type constructors and even infix bindings in a module and to import a module into a name space other than the default top-level. The idea is to provide a way for extensions to be packaged up for Poly/ML. There are a number of features that it might be nice to provide but aren't part of the core system. An example would be the Windows GUI modules but I'm sure there are others. I hope it would also encourage contributions. David

1 0

compressing heap images
by Japheth.Lim＠nicta.com.au 02 Nov '15

02 Nov '15

On 21/10/15, Gerwin Klein wrote: > It turns out that with our collection of large Isabelle sessions that we > run regularly, polyml heap image space is becoming a noticeable problem > for us. > We found another way to solve this problem. Isabelle uses saveState to save heaps. If we use saveChild instead, we get a substantial reduction in heap sizes. However, this makes the saved states less portable because they contain the pathname of the parent. Then loading will fail if the heaps are moved to a different path. Here it would be nice if Poly/ML could use relative paths for the parent, and look them up relative to the child. There are other ways to fix this (e.g. chdir before loadState) but I'd rather get the above behaviour from Poly/ML directly. Any thoughts? Japheth ________________________________ 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.

2 4

type real in polyml
by immler＠in.tum.de 30 Oct '15

30 Oct '15

Hi David, Thanks for your answer, I should have subscribed to the polyml mailing list earlier. Using the SSE2 instructions and/or setting the intermediate precision to 64 bit would give a nice and clear semantics to floating point expressions in Poly/ML, so I would be very much looking forward to such a change. Best regards, Fabian > Am 07.10.2015 um 15:56 schrieb David Matthews <David.Matthews at prolingua.co.uk>: > > Hi Fabian, > This was a bit bizarre particularly as when I tried it on Windows there > didn't seem to be a problem. It is a problem with the precision and > when rounding occurs. Poly/ML uses the old x87 floating point unit on > both X86/32 and X86/64. As far as I'm aware all x86/64 machines support > the SSE2 instructions so other compilers use SSE2 instructions on 64-bit > but, by default use the x87 instructions on 32-bit. > > The x87 instructions use 80-bit registers internally and only round to > 64-bits when the registers are stored to double-precision values. The > SSE2 instructions are 64-bit so all the results are the same whether > values are stored to memory or not. The x87 has bits in the control > word that can allow it to compute intermediate results to 80-bit, 64-bit > or 32-bit precision. The question is whether this should be set to > 80-bit or 64-bits? > > Currently Poly/ML sets it to 80-bit precision at the start. As far as > I've been able to ascertain that is what other x86/32 compilers do. The > idea is, I suppose, to compute intermediate results to the best > precision available. It does, though, produce the strange results that > you've encountered. I think the reason for the difference in results is > whether the function can be computed at compile-time or not. > > I'm coming round to the view that it should instead set the FPU to > 64-bits so that intermediate results are the same whether they remain in > the register or are written out to memory and reloaded. It looks as > though the libraries in Visual C set that anyway which is why I only saw > the problem when I tested on Linux. This would also mean that results > would not change when, as I plan, I change to using the SSE2 > instructions on x86/64. > > Best regards, > David > > On 07/10/2015 14:07, Fabian Immler wrote: >> Hi David, >> >> Perhaps I should rephrase my enquiry to: "Do I get any guarantees from the implementation of type real in PolyML"? >> Naively, I would have expected, that every subexpression is evaluated according to the IEEE-754 standard (in double precision). >> >> I skimmed the implementation in libpolyml/reals.cpp, it looks like all intermediate results are stored in and retrieved from memory (real_arg, real_result). Is that sufficient to comply to IEEE-754? I.e., can there not occur "double rounding" (as in [1, section 3.3.1])? Or isn't there the need to use something like FLT_EVAL_METHOD=1 [2,3]? >> >> [1] http://www.springer.com/us/book/9780817647049 >> [2] https://en.wikipedia.org/wiki/C99#IEEE.C2.A0754_floating_point_support >> [3] http://www.cplusplus.com/reference/cfloat/ >> >> Best regards, >> Fabian >> >> >>> Am 07.10.2015 um 12:26 schrieb Fabian Immler <immler at in.tum.de>: >>> >>> Hi David, >>> >>> I noticed some strange behavior when working with type real in PolyML: >>> In the following example, where I have "testres = twosum a", depending on whether I call >>> "testres" or "twosum a" I get different results. >>> >>> If I take the definitions out of the structure Test, the results are the same. They are also the same if e.g. print-statements are inserted in between the assignments to b, s, sb and r. The results are also the same when evaluating inside Isabelle with the debugger turned on. >>> >>> Do you have an idea what is going on there? >>> Is it possible that some intermediate results are kept in higher precision in the FPU? >>> Does the compiler perform some "optimizations" on expressions of type real? >>> >>> Best regards, >>> Fabian >>> >>> >>> structure Test = struct >>> >>> fun one n = (if n = 0 then 100.0 else one (n - 1)); >>> >>> val a : real = one 1; >>> >>> fun twosum a = >>> let >>> val b = 1.0/1243313.0; >>> val s = a + b >>> val sb = s - b >>> val r = s - sb >>> in >>> r >>> end; >>> >>> val testres = twosum a; >>> end; >>> >>> open Test; >>> val a = twosum a >>> val b = testres >>> >>> >>>

2 1

Nested use
by David.Matthews＠prolingua.co.uk 21 Oct '15

21 Oct '15

There's long been an issue with "use" when trying to compile and run files which themselves contain "use". For example if ROOT.ML contains: use "first.ML"; use "second.ML"; The inner calls to "use" are taken relative to whatever the original working directory was set to, which means that ROOT.ML always has to be called with the right directory. It's not possible to call use "/home/david/mydirectory/ROOT.ML"; from an arbitrary directory. I've committed a change to the NestedUse branch which is one possible solution to this. The version of "use" in there records the full path to the parent directory of the file name when a file is "used". If that file then contains a nested call to "use" the file is first checked as previously using the original working directory but if that fails it looks for the name by appending the parent directory to the name given. So in the example above, it would first look for "./first.ML" and only if that does not exist would it look for "/home/david/mydirectory/first.ML". This seems as though it should achieve the desired effect with the minimum change to existing programs but there are other alternatives. For example, should it look first relative to the parent directory? David

3 4

← Newer
1
...
18
19
20
21
22
23
24
...
70
Older →

Jump to page:

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