Re: [polyml] PolyML.pointerEq

2014-02-05 Thread Brian Campbell
On 30/01/14 11:03, David Matthews wrote: ... The only safe way to maintain identity of cells is to use a counter or a ref. An alternative to a ref is to use a locally generated exception and this may be more efficient than a ref. As a work-around to avoid the problem with duplication in the

Re: [polyml] PolyML.pointerEq

2014-01-30 Thread David Matthews
Brian, The intention of PolyML.pointerEq is that if pointerEq(x, y) is true then x = y will be true, assuming the type of x and y admits equality. It is really intended for use where a user function wants to test for equality in some general sense and knowing that actually the values are the

Re: [polyml] PolyML.pointerEq

2014-01-30 Thread Makarius
On Thu, 30 Jan 2014, David Matthews wrote: The intention of PolyML.pointerEq is that if pointerEq(x, y) is true then x = y will be true, assuming the type of x and y admits equality. It is really intended for use where a user function wants to test for equality in some general sense and

Re: [polyml] PolyML.pointerEq

2014-01-30 Thread David Matthews
On 30/01/2014 11:40, Makarius wrote: The puristic approach to structutal equality in SML turns out as a benefit these days, when the system runs with loosened brakes on multicore hardware. Neither the JVM nor OCaml could afford that (but I think Haskell / GHC does). The measurements I did

[polyml] PolyML.pointerEq

2014-01-29 Thread Brian Campbell
What semantics, if any, does PolyML.pointerEq have? In particular, is it supposed to be guaranteed that if pointerEq (x,y) is true, then it will remain true after GC? My reason for asking is that I've been having trouble with assertion failures in HOL when reducing large terms. The