Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,


> On 17 Sep 2016, at 14:49, Rob Arthan  wrote:
…
> … I am getting a segfault somewhere in the
> ProofPower parser generator. I will report again when I have
> isolated that.

To the list of three issues in my previous e-mail, I can now add:

4) In some circumstances a function call can lead to a segfault.

I’ve attached a short extract from the parser generator code that demonstrates 
the problem. 
If you execute the body of the function empty_non_terminals interactively
with the parameter bound to the test data, then nothing goes wrong.
If you call the function with the test data as parameter (as on the last line 
of the
attached file) you get a segfault.

Regards,

Rob.



slrp-bug-cutdown.ML
Description: Binary data
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Update to code-generator and run-time system interface

[Rob Arthan]

David,

I have been having a go at building ProofPower with the latest updates.
Here is some miscellaneous feedback:

1) Are these two errors in the configure output harmless? (This is on
Mac OS X using Apple’s Xcode tools.)

checking for __attribute__((visibility("hidden")))... no
clang: error: unsupported option '-print-multi-os-directory'
clang: error: no input files
checking that generated files are newer than configure… done

2) SML90.explode crashes. The following patch fixes this:

--- a/basis/SML90.sml
+++ b/basis/SML90.sml
@@ -81,9 +81,8 @@ struct
 fun ord "" = raise Ord | ord s = Char.ord(String.sub(s, 0))
 
 fun chr i = str(Char.chr i)
-(* Because single character strings are represented by the characters
-   themselves we just need to coerce String.explode. *)
-val explode: string -> string list = RunCall.unsafeCast(String.explode)
+
+val explode: string -> string list = map str o String.explode
 val implode = String.concat
 
 type instream = TextIO.instream and outstream = TextIO.outstream

3) If I configure with —enable-intinf-as-int, make compiler fails:

Use: basis/IMPERATIVE_IO.sml
Use: basis/ImperativeIO.sml
Use: basis/TextIO.sml
Exception- InternalError: findEntry - not found raised while compiling

make[3]: *** [polyexport.o] Error 1
make[2]: *** [all-recursive] Error 1
make[1]: *** [all] Error 2
make: *** [compiler] Error 2

Not being able to build with —enable-intinf-as-int  isn’t a stopper for me,
but when I press on, I am getting a segfault somewhere in the
ProofPower parser generator. I will report again when I have
isolated that.

Regards,

Rob.

> On 16 Sep 2016, at 13:24, David Matthews  
> wrote:
> 
> I have now pushed a major update to git master which is the result of work 
> going back to the beginning of the year.  It covers a number of areas but 
> largely the code-generator and the run-time system interface.
> 
> The basic design of much of the low-level parts of Poly/ML dated back to the 
> early days.  While it has changed a lot in detail the overall structure has 
> remained the same.  The idea was to bring the whole thing up to date.
> 
> The run-time system interface has been redesigned and instead of a vector of 
> entries to the run-time system the ML code now uses a form of 
> foreign-function interface to call individual functions.  The advantage is 
> that it is much easier to add new functions.  In addition when building an 
> executable it is possible for the linker to select only the parts of 
> libpolyml that are actually required for the application, at least if the 
> static library version is used.  It should be possible to adapt the 
> foreign-function interface it uses to speed up calls made using the Foreign 
> structure, although that's not done at the moment.
> 
> The code-generator has been rewritten particularly the register assignment.  
> The previous version had been the result of a series of adaptations to new 
> architectures over the years.  The new version focusses solely on the X86.  
> I'm still working on this.  Doing this has needed a temporary, slow, 
> code-generator which is why it has taken until now to push this to git master.
> 
> The representation of strings has been simplified.  Previously, single 
> character strings were represented by the character itself as a tagged value. 
>  This was largely a relic of SML 90 which didn't have a separate char type.  
> That has been removed and all strings are now represented as a vector of 
> bytes.  This speeds up string operations since the code no longer has to 
> consider the special case.
> 
> SSE2 instructions are now used for floating point on the X86/64. Floating 
> point support in the new code-generator is rudimentary at the moment and not 
> to the same extent as the previous code-generator.
> 
> The handling of return addresses from functions has been simplified.  A 
> consequence of this is that when pieces of code are compiled they are stored 
> in a separate area of memory rather than in the general heap and not 
> garbage-collected.  It is no longer possible to get an exception trace so 
> PolyML.exception_trace has no effect.  The debugger handles this much better 
> anyway.
> 
> Although the focus has been on the X86 the portable byte-code interpreter has 
> been improved and is significantly faster.
> 
> The system has had some basic testing but there are bound to be bugs in 
> something as complex as this.  I'm also continuing to work on improvements.  
> When testing this it is essential to run "make compiler" at least once and 
> generally twice to build the new compiler and then build the compiler itself 
> with the new compiler.
> 
> David
> ___
> polyml mailing list
> polyml@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk

Re: [polyml] Equality Type Parameter in Datatype Declaration

[Bernard Berthomieu]

Many thanks Matthew for the clarification. Subtle :-)

Since datatype declarations declare both a type operator
and constructors, I think the explanation deserves to appear
in http://mlton.org/EqualityTypeVariable, last part.
The last two declarations declare identical type operators, but
not identical constructors, right ?

  Bernard.

On 9/17/16 1:42 PM, Matthew Fluet wrote:

I think that the reasoning is that the type function induced by a
datatype (which maps the type variables to the fresh type name) is
ignorant of equality type variables, but the type schemes induced by
the constructors do respect equality type variables.

Thus, with

   datatype ('a, ''b) t = A of 'a | B of ''b

both

   fun f (x: (int, real) t) = x

and

   val l : ((int, real) t) list = []

type check (with MLton), since "(int, real) t" can always be
successfully elaborated.

As noted previously,

   val t1 = B 1.0

does not type check, because the type scheme of C cannot be
instantiated with "real", a non-equality type.

At first, I was surprised by the following

   val t2 : (int, real) t = A 1

which does not type check; in MLton, we report:

   Pattern and expression disagree.
 pattern:(_, []) t
 expression: (_, []) t
 in: t2: (int, real) t = A 1

But, this is fine --- the type annotation on the pattern successfully
elaborates, but type inference of the expression (constructor A
applied to 1) yields "(int, ''B) t" for some fresh unification type
variable ''B and this unification type variable is an equality type
variable and cannot be unified with "real".

-Matthew




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Equality Type Parameter in Datatype Declaration

[Bernard Berthomieu]

Hello,

Funnily (where my belief came from ?), the page about equality type
variables on mlton.org (http://mlton.org/EqualityTypeVariable)
says that they play no special role in either type bindings or
datatype bindings, contradicting the compiler ...

  BB.

On 9/16/16 10:42 PM, Bernard Berthomieu wrote:

David,

Yes, you are right; p19 applies to type functions (abbreviations),
not to type constructors introduced by datatype.
My understanding was that both obeyed the same rule, but I guess
it is not the case (can't find anything about it in the book ..).
mlton also rejects (C 1.0), by the way.

  BB.

On 9/16/16 10:25 PM, David Matthews wrote:

Bernard,
That refers to a "type function" not a datatype binding.
type ''a t = ''a * ''a
creates a type function and indeed Poly/ML ignores the equality 
attribute in that case.  A datatype binding creates a new "type name" 
and that is dealt with elsewhere.


The fact that both mlton and hamlet behave the same way as Poly/ML 
makes me feel confident that it is SML/NJ that is wrong.  Hamlet is 
based very closely on the semantics so it's usually the best way of 
checking out these sorts of questions.


Regards,
David

On 16/09/2016 20:59, Bernard Berthomieu wrote:

Hello,

Besides any printing/elaboration problem with polyml 5.6:

In polyml 5.5:


datatype ''a t = C of ''a;

datatype ''a t = C of ''a

C 1.0;

Error-Type error in function application.
   Function: C : ''a -> ''a t
   Argument: 1.0 : real
   Reason: Can't unify ''a to real (Requires equality type)
Found near C 1.0
Static Errors

In sml-nj 110.77:

- datatype ''a t = C of ''a;
datatype 'a t = C of 'a
- C 1.0;
val it = C 1.0 : real t


polyml interprets the type variable ''a in the declaration of t as an
equality type,
while sml-nj interprets it as a regular type variable.

I like the treatment of polyML :-), but I guess it is not standard:

The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19:
"... In particular, the equality attribute has no significance in a
bound
 variable of a type function; for example ... "

So, unless I'm mistaken, sml-nj is right.

  Bernard.

On 9/16/16 9:41 PM, David Matthews wrote:

Rob,
Actually what I was trying to find was the bit that says that the
equality attribute in a type variable used as a datatype parameter
should be honoured where it isn't when used as a type parameter.

> type ''a t = ''a * ''a;
type 'a t = 'a * 'a
> (1.0, 2.0): real t;
val it = (1.0, 2.0): real t
>  datatype ''a t = C of ''a;
datatype 'a t = C of ''b   This prints wrongly
>  C 1.0;
poly: : error: Type error in function application.
   Function: C : ''a -> ''a t
   Argument: 1.0 : real
   Reason: Can't unify ''a to real (Requires equality type)
Found near C 1.0
Static Errors

I'm sure I looked into this a long time ago and a check with hamlet
agrees with Poly/ML so I'm confident it's right; I just haven't been
able to find the reference.

Regards,
David

On 16/09/2016 20:18, Rob Arthan wrote:


David,


On 16 Sep 2016, at 19:19, David Matthews
 wrote:

I've checked hamlet and mlton and they both reject it so I think in
this case Poly/ML is right and SML/NJ is wrong.  I can't point to
the bit of the definition that says that, though.


It's in Appendix C:  "Of [the type names listed in the initial static
basis] all except exn and real admit equality".

Regards,

Rob.


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml





___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml



___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml