Poly/ML

polyml@lists.polyml.org

695 discussions

[isabelle] Opaque ascription for SML code generation
by dm＠prolingua.co.uk 13 Jun '16

13 Jun '16

Pretty-printing isn't part of the ML standard so it's not always clear how to do it properly. There have been various changes over the years. In particular, printing exception packets is difficult because the packet can contain values of types that exist only where the exception is raised. In the example below, "t" may not actually be exported from the signature. So, Poly/ML puts the print function that applies where the exception is raised into the exception packet and uses that if it needs to print the packet. There are no plans to change this. There have been some changes around the printing of types exported through opaque matching. When a structure matches a signature containing a type through opaque matching the semantics says that this creates a new type "name". Poly/ML creates a new ref to hold the pretty print function for the new type. Previously this was initialised to the pretty print function for the implementing type but this was changed in 5.6.1 to default to printing "?". It later became clear that this was too restrictive when the signature contained a datatype (e.g. "test" below) so there was a further change in commit 29985b1c in git master. So now if you install pretty printers both within the structure, (*1*) below, for the exception, and outside the signature (*2*) it will work as you expect. David On 12/06/2016 15:22, Makarius wrote: > After the Isabelle2016 release, we have discontinued SML/NJ and old > versions of Poly/ML, so there is a bit more flexibility now in canonical > patterns for Isabelle/ML. > > The example with structure A3 from above is the difficult one, notably > the situation "does not work (overrides pp for int)". Defining the pp > outside of the structure basically works, but exceptions are not printed > correctly. This is how the problem with opaque ascription was discovered > many years ago, and the abstype solution took over. > > > Here is an update of the example A3 from Stackoverflow above, using > Isabelle2016 with its bundled Poly/ML 5.6: > > ML ? > structure A :> > sig > type t > exception BAD of t > datatype test = Test of t > val a: t > val print: t -> string > end = > struct > > type t = int > > exception BAD of t > datatype test = Test of t > > val a = 42 > > fun print i = "{" ^ Int.toString i ^ "}" > > (*1*) > (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => > PolyML.PrettyString (print x))*) > end; > > (*2*) > (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => > PolyML.PrettyString (A.print x))*) > ? > > ML ?A.a; A.Test A.a; A.BAD A.a? > > > This leads to a mix of results, depending on the place where the pretty > printer is installed. > > I still don't see how to get a simple and robust pretty printer setup, > so we can't use opaque ascription ? unless David Matthews wants to > refine that again for a future release of Poly/ML. > > > Makarius > >

1 0

Foreign and cShort
by kostirya＠gmail.com 25 May '16

25 May '16

is it error? > cat foo.c short foo (short x) { return x+1; } > clang -shared -o foo.so foo.c > cat foo.sml open Foreign; val mylib = loadLibrary "foo.so" fun foo x = buildCall1 ((getSymbol mylib "foo"), cShort, cShort) x val r = foo ~5 val _ = print ( (Int.toString r) ^ "\n" ) > env LD_LIBRARY_PATH=. poly --script foo.sml 65532 P.S. Polyml is from git 5 days ago.

2 2

Some questions about Foreign
by kostirya＠gmail.com 25 May '16

25 May '16

Hello. I have some questions about Foreign. 1. How to convert OS.IO.iodesc (from socket) into cUint (uintptr_t)? 2. C function is need 'const struct timespec *timeout' argument. Where struct timespec is: struct timespec { time_t tv_sec; long tv_nsec; }; Do I understand correctly that this is cOptionPtr (cStruct2 (cInt32, cLong)) ? But how can I call this from polyml? I call as SAME (3, 0) and got error: Exception- Foreign "cOptionPtr must be applied to a pointer type" raised Best regard.

2 2

NetHostDB.fromString
by kostirya＠gmail.com 24 May '16

24 May '16

Hello. NetHostDB.fromString have error: > poly Poly/ML 5.6 Release > NetHostDB.toString (valOf(NetHostDB.fromString "127.0.0.1")); val it = "0.0.0.127": string > NetHostDB.toString (valOf(NetHostDB.fromString "10.0.0.34")); val it = "0.0.0.10": string > NetHostDB.toString (valOf(NetHostDB.fromString "10.1.1.34")); val it = "10.1.1.34": string MLton: > cat 1.sml val _ = print (NetHostDB.toString (valOf(NetHostDB.fromString "127.0.0.1"))) > mlton 1.sml > ./1 127.0.0.1>

2 2

Stack trace : condensed form
by artella.coding＠googlemail.com 15 May '16

15 May '16

Hi, is it possible to get a condensed stack trace where recursive calls are collapsed into one line in the printout of the stack trace? For example suppose that I have : *************************************************************** (* test.ml *) PolyML.Compiler.debug := true; open PolyML.Debug; breakAt("test.ml",12); fun is_divisible(n : int, currentDivisor : int) = if currentDivisor <= n - 1 then n mod currentDivisor = 0 orelse is_divisible(n, currentDivisor + 1) else false; (* This is line 12 *) fun is_prime(n : int) : bool = if n = 2 then true else not(is_divisible(n, 2)); fun main() = is_prime(11); *************************************************************** Then upon running as follows : > poly > use "test.ml"; > main(); test.ml line:12 function:is_divisible false; (* This is line 12 *) > stack(); > test.ml line:12 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:8 function:is_divisible test.ml line:18 function:is_prime test.ml line:21 function:main test.ml line:4 function:? val it = (): unit debug > The recursive call to "is_divisible" takes up most of the space of the printout of the stack trace. Is it a possible to get a condensed form of this printout, for example something like : test.ml line:12 function:is_divisible test.ml line:8 function:is_divisible [***repeated 9 times***] test.ml line:18 function:is_prime test.ml line:21 function:main test.ml line:4 function:? Thanks

1 0

Debugging : breakAt
by artella.coding＠googlemail.com 14 May '16

14 May '16

Hi, suppose that I have the following code ("basics.ml") : ******************************** (* basics.ml *) fun is_divisible(n : int, currentDivisor : int) = if currentDivisor <= n - 1 then n mod currentDivisor = 0 orelse is_divisible(n, currentDivisor + 1) else false; (* This is line 9 *) fun is_prime(n : int) : bool = if n = 2 then true else not(is_divisible(n, 2)); ******************************** Then if I do : > rlwrap poly > PolyML.Compiler.debug := true; > use "basics.ml"; > open PolyML.Debug; > breakAt("basics.ml",9); > is_prime(15); then I am finding that the debugger is not stopping at the desired line. Is there anything that I am doing wrong? (I am using the latest compiler sources from github). Thanks

2 2

Poly/ML changes history
by rda＠lemma-one.com 14 May '16

14 May '16

I have a recollection of a list somewhere on the Poly/ML website giving a brief description of what had changed in each version of Poly/ML, but I can?t find it any more. Am I just being unobservant or was I imagining things? The specific question I wanted to answer was: which version introduced polyc? Regards, Rob.

3 2

determining if an outstream is a tty
by Michael.Norrish＠nicta.com.au 07 May '16

07 May '16

The Basis library documentation for OS.IO suggests that it should be possible to get one's hand on a primitive reader or writer iodesc by pulling things apart to get PrimIO values. Doing type-directed programming, I thought I might do this for a TextIO.outstream with > val getIOD = (fn TextPrimIO.WR r => #ioDesc r) o #1 o TextIO.StreamIO.getWriter o TextIO.getOutstream; val getIOD = fn: TextIO.outstream -> OS.IO.iodesc option This has the right type (and I couldn't see any other way of getting the right type). Unfortunately, I can't run it: > getIOD TextIO.stdOut; Exception Io raised while writing to stdOut. terminating the session. If this had worked, I then hoped to be able to call Posix.FileSys.iodToFD on the value, if there was one, and to then eventually call Posix.ProcEnv.isatty on the result of that, if present. Is there a right way to do this? Many thanks, 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 3

Posix implementation raising Fail exception
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

As can be seen in https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/124717527 our use of Posix waiting is occasionally causing a Fail exception to be raised from inside the Posix implementation (there's no Fail exception with that message in our source code, and our code *is* doing a wait at that point). I'm afraid this doesn't seem easy to reproduce. 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.

3 6

reliably crashing 5.6 on OSX 10.11.4
by Michael.Norrish＠nicta.com.au 25 Apr '16

25 Apr '16

The attached tarball (derived from a prefix of the HOL4 sources) reliably (every one of the tens of attempts I've made so far) crashes PolyML 5.6 on my Macbook Pro with Assertion failed: (save_vec_addr < save_vec+1000), function push, file save_vec.cpp, line 70. Abort trap: 6 Just change into the crashpoly directory and do poly --use usethis.ML If the call to Posix.Process.sleep in multiLib.sml is made for a much shorter length of time (pass 15 instead of 15000 to the genthms call, say), it works as expected. I also got 3/3 crashes with the time delay at 5000. I have tried to remove extraneous material from the tarball, but I'd be very surprised if it was minimal. 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.

3 3

← Newer
1
...
14
15
16
17
18
19
20
...
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