Poly/ML

polyml@lists.polyml.org

3 participants
698 discussions

compilation problem - am I going mad?
by itz＠speakeasy.org 26 Jun '02

26 Jun '02

Sorry for sending this to the request address :( Hi, trying to compile these two files: (* BITSET.sml *) signature BITSET = sig exception Not_found; (* raised by [choose] *) type ty; (* type of bitsets*) val make_bitset : int -> ty ; (* [make_bitset size] creates a new empty bitset containing [size] bits.*) val copy : ty -> ty ; (* [copy v] returns a fresh exact copy of bitset [v].*) val copy_negated : ty -> ty ; (* [copy_negated v] returns a fresh bit vector that is the complement of [v].*) val set : ty -> int -> unit ; (* [set v i] sets the [i]th bit of vector [v].*) val clear : ty -> int -> unit ; (* [clear v i] clears the [i]th bit of vector [v].*) val test : ty -> int -> bool ; (* [test v i] tests the [i]th bit of vector [v].*) val neg : ty -> unit ; (* [neg v] complements the vector [v] in place.*) val band : ty -> ty -> unit ; (* [band v_to v_from] performs a [land] of [v_to] and [v_from], changing [v_to] in place.*) val bor : ty -> ty -> unit ; (* [bor v_to v_from] performs a [lor] of [v_to] and [v_from], changing [v_to] in place.*) val bxor : ty -> ty -> unit ; (* [bxor v_to v_from] performs a [lxor] of [v_to] and [v_from], changing [v_to] in place.*) val bsub : ty -> ty -> unit ; (* [bsub v_to v_from] computes the set difference [v_to - v_from], storing the result in [v_to].*) val is_sub : ty -> ty -> bool ; (* [is_sub v1 v2] tests if vector [v1] is a subset of [v2].*) val is_equal : ty -> ty -> bool ; (* [is_equal v1 v2] tests if vector [v1] is structurally equal to [v2].*) val choose : ty -> int ; (* [choose v] returns an arbitary integer [i] such that [v[i] = true], if there is one, otherwise raises [Not_found]. Equal integers are returned for structurally equal vectors.*) end; (* BITSET.sml ends here *) (* Bitset.sml *) structure Bitset :> BITSET = struct exception Not_found; (* raised by [choose] *) exception Size_mismatch; (* import selected stuff from LargeWord and Array *) val wordSize = LargeWord.wordSize; type word = LargeWord.word; val notb = LargeWord.notb; val << = LargeWord.<< ; val fromLargeInt = LargeWord.fromLargeInt; val andb = LargeWord.andb; val orb = LargeWord.orb; val xorb = LargeWord.xorb; val length = Array.length; val sub = Array.sub; val tabulate = Array.tabulate; val update = Array.update; val modifyi = Array.modifyi; val foldli = Array.foldli; val appi = Array.appi; type ty = { size : int , last_mask : word , bits : word Array.array }; fun make_mask (i: int) = notb (<< (notb (fromLargeInt 0), Word.fromInt i)); fun word_size (s: int) = (s div wordSize) + 1; fun make_bitset s = if s < 0 then raise Size else let val bits = Array.array (word_size s, fromLargeInt 0); val mask = make_mask (s mod wordSize) in { size = size, last_mask = mask, bits = bits } end ; fun copy v = let val s = #size v ; val ws = word_size s ; fun f i = sub (#bits v, i) in { size = s, last_mask = #last_mask v, bits = Array.tabulate (ws, f) } end ; fun copy_negated v = let val last = length (#bits v) - 1; fun f i = if i <> last then notb (sub (#bits v, i)) else andb (#last_mask v, notb (sub (#bits v, i))) in { size = #size v, last_mask = #last_mask v, bits = Array.tabulate (last+1, f) } end ; fun set v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = << (fromLargeInt 1, Word.fromInt bit) in update (#bits v, idx, orb (sub (#bits v, idx), mask)) end; fun clear v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = notb (<< (fromLargeInt 1, Word.fromInt bit)) in update (#bits v, idx, andb (sub (#bits v, idx), mask)) end; fun test v i = let val idx = i div wordSize; val bit = i mod wordSize; val mask = << (fromLargeInt 1, Word.fromInt bit) in andb (sub (#bits v, idx), mask) <> fromLargeInt 0 end; fun neg v = let val last = length (#bits v) - 1; fun f (i, x) = if i <> last then notb x else andb (#last_mask v, notb x) in modifyi f (#bits v, 0, SOME(last+1)) end; fun band to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = andb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bor to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = orb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bxor to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = xorb (sub (#bits from, i), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun bsub to from = if #size from <> #size to then raise Size_mismatch else let fun f (i, x) = andb (notb (sub (#bits from, i)), x) in modifyi f (#bits to, 0, SOME(length (#bits to))) end; fun is_sub v1 v2 = if #size v1 <> #size v2 then raise Size_mismatch else let fun p (i, x, b) = b andalso andb (x, notb (sub (#bits v2, i))) = fromLargeInt 0 in foldli p true (#bits v1, 0, SOME(length (#bits v1))) end; fun is_equal v1 v2 = if #size v1 <> #size v2 then raise Size_mismatch else let fun p (i, x, b) = b andalso x = sub (#bits v2, i) in foldli p true (#bits v1, 0, SOME(length (#bits v1))) end; fun find_bit (w: word) = let fun fb1 i mask = if andb (mask, w) <> fromLargeInt 0 then i else fb1 (i+1) (<< (mask, Word.fromInt 1)) in fb1 0 (fromLargeInt 1) end ; fun choose v = let val ridx = ref ~1; fun f (i, x) = if !ridx = ~1 andalso x <> 0 then ridx := i else () in (appi f (#bits v, 0, SOME(length (#bits v))); if !ridx = ~1 then raise Not_found else let val idx = !ridx; val bit = find_bit (sub (#bits v, idx)) in !ridx * wordSize + bit end) end; end; (* Bitset.sml ends here *) I am getting these errors: > Making Bitset Error: in 'Bitset.sml', line 133. Can't unify Words.LargeWord.word with int (Different type constructors) Found near find_bit(sub( (#bits)(v), idx)) Error: in 'Bitset.sml', line 20. Can't match int to Words.LargeWord.word (Different type constructors) While checking (choose) near structure Bitset :> BITSET = struct exception Not_found exception Size_mismatch val ... = ... type ... ... ... end Error: in 'Bitset.sml', line 20. Can't match int to string -> int (Incompatible types) While checking (make_bitset) near structure Bitset :> BITSET = struct exception Not_found exception Size_mismatch val ... = ... type ... ... ... end Bitset was not declared Exception- Fail "Static errors (pass2)" raised I look at the code forward and backward and really think it is correct. Here's the typing as I see it: bit = find_bit (sub (#bits v, idx)) ^^^ ^^^^^^^^ ^^^ ^^^^^^^ ^^^ int word->int (word array, int)->word word array int !ridx * wordSize + bit ^^^^^ ^^^^^^^^ ^^^ int int int And what in the world has STRING to do with it ?!? February 2002 release of PolyML. -- Ian Zimmerman, Oakland, California, U.S.A. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087 EngSoc adopts market economy: cheap is wasteful, efficient is expensive.

1 1

PolyML on cygwin?
by Tomas.Juknevicius＠nomagic.com 20 May '02

20 May '02

Hello guys/girls, I'm new to this list, also new to polyML :). I have a question: i'm trying to launch the linux version of polyml on CygWin (under win2000) with little success. The executable 'poly' just answers with: ./poly: 1: Syntax error: "(" unexpected when trying to launch it ... Maybe someone knows the solution or has encountered similar situation? PS why i'm trying the linux version on cygwin under win200 and not polyml for win32? Well, actualy, i'm trying to launch the Isabelle system, (which uses polyML) and it has no win32 version. So i'm stuck with Isabelle on cygwin. When I tried to couple Isabelle/cygwin with win32 version of polyML, win32 executable of polyML could not crunch linux style file paths, supplied by Isabelle under cygwin. Hence i'm stuck with the only combination left - run both Isabelle & linux version of polyML under cygwin. Unfortunately, when linux version of polyML is launched under cygwin, it just seems to complain '1: Syntax error: "(" unexpected'. This output apears no matter what parameters i supply for the poly executable :( -- Tomas Juknevicius

2 1

stack trace
by frittinger＠acm.org 14 May '02

14 May '02

Hello, I'm new to PolyML and have some questions concerning debugging and erro= r messages. The function PolyML.exception_trace prints a number behind each functio= n name in the stack trace. Could someone please tell me what this number indicat= es? Is there a way to get the line number of the input file (like njml does= ) where a Match exception is thrown? Thanks in advance, Frank ***********************************************************************= Frank Rittinger Albert-Ludwigs Universit=E4t Freiburg, Institut f=FCr Informatik Georges-Koehler-Allee, Geb. 52 (Room 00-021), 79110 Freiburg, Germany Phone: +49 761 203 8245 Fax: +49 761 203 8242 URL: http://www.informatik.uni-freiburg.de/~rittinge ***********************************************************************=

2 1

beginner questions
by baxter＠math.umn.edu 29 Mar '02

29 Mar '02

The example works nicely, and the system seems very convenient. I made a small C++ dll now using extern "C" and it's fine too. Thanks very much for the help! John On Fri, 29 Mar 2002, David Matthews wrote: > John, > There's nothing special about a DLL for use with Poly/ML. If you can > build a DLL for use with C or Visual Basic then it will work with > Poly/ML. The Windows programming interface in Poly/ML is largely done > by calling Windows system DLLs. To build a DLL you need some sort of > Windows development environment. I've been using Visual C++ but you > should be able to use anything. You will normally need a .DEF file > which contains a list of the functions you want to export from the DLL. > I made a very simple example some time ago and I'm including it as a ZIP > archive. It was done with Visual C++ and includes an ML file which > calls the DLL. You can write your DLL in C++ but all the exported > functions have to use C calling conventions. You really need to look at > the documentation for your development environment to find out how to > construct a DLL. > > Hope that helps. > David. > > > > >> earlier questions by me

1 0

beginner questions
by baxter＠math.umn.edu 28 Mar '02

28 Mar '02

Just starting using polyml and had a couple of questions about using c functions. I read the documentation on the Poly/ML Interface to the C Programming Language but I'm sure I don't get the whole picture. (I've made little c functions for python & tcl in the past but of course that's different.) 1. The documentation gives an example of making a dll for unix using gcc. Since polyml has a very nice Windows interface it looks as if everything works on windows. I'm on windows 2000 for now and I wonder if I need to use the microsoft vc++ compiler to make dll's for that platform, or if other compilers are ok. I guess in any case I need to figure out what symbols the compiler is using for functions(?) but that shouldn't be hard. 2. There didn't seem to be any mention of special header files that are needed when compiling the c libraries. Are there any? Also do I need to make any special type of dll? 3. Since I have yet to make any c functions, my last question is rather excessive, but what about a c++ library? Can one compile it in such a way that polyml can use it? Thanks for any tips, or pointers to things I should have read more carefully! Cheers, John Baxter

1 0

Re: improve.c problem and patch
by David.Matthews＠prolingua.co.uk 25 Mar '02

25 Mar '02

Hi Bow-Yaw, Thanks for reporting that and sending the fix. I'll incorporate it in the next release. Markus Wenzel reported a problem in the disc garbage collector when compiling with GCC 3.0.2 which sounds exactly like this. There hasn't been any discussion of this on the Poly/ML mailing list because, so far, there hasn't been ANY discussion on the mailing list. As far as ml-lex and ml-yacc are concerned, I don't know whether they will work with Poly/ML or not. If they're written entirely in Standard ML they should work fine but if they use some special features of SML/NJ then there may be a problem. Does anyone else know? Regards, David. On Saturday, March 23, 2002, at 12:42 , Bow-Yaw Wang wrote: > > Hi Mr. Matthews: > > I try to build Isabelle2002 with PolyML 4.1.2. But poly > always crashes at "Bad pointer" when closing the database. > It turns out that gcc-3.0.4 has a warning and generates different > code for improve.c. After I made the following change: > > 739c739 > < while (n--) *pt++ = (word) FixupPointer((word *)*pt); > --- >> while (n--) { *pt = (word) FixupPointer((word *)*pt); pt++; } > > the problem goes away. Since I'm not on the mailing list, I'm not > sure if this is a known issue. Just let you know in case the > problem hasn't been reported. > > Currently, I'm working on a project which needs a theorem prover, > external function interface and yacc. PolyML + Isabelle would be > the ideal environment if tools like yacc were available. I'm thinking > using ml-yacc/ml-lex from SMLNJ and compiling everything in PolyML. > Do you by chance know whether it may work? > > Thanks, > > Bow-Yaw

2 1

polyml executables [was Re: improve.c problem and patch]
by bernard＠laas.fr 25 Mar '02

25 Mar '02

Hello, David wrote in last message: > There hasn't been any discussion of this on the Poly/ML mailing list > because, so far, there hasn't been ANY discussion on the mailing list. Let us start one then: I'm writing applications in Poly/ML that I intend to distribute in binary form. Currently, this requires users to download at least the polyml driver from polyml.org and install it. Not a big deal, but certainly an avoidable burden, specially when applications require several similar prerequisites. I think a nice addition to the polyml tools would be one that packs the polyml driver with a database, in a single executable. The tclpro compiler suite, for instance, has a convenient tool for such purposes, that wraps an interpreter with its libraries, code, and possibly data files, into a single executable. A similar "polywrap" tool would be perfect for my purposes. Any plans for such a tool, or on-the-shelf alternatives ? Other opinions ? Bernard. -- Bernard Berthomieu ^ Bernard.Berthomieu(a)laas.fr LAAS / CNRS . /_\ http://www.laas.fr/~bernard 7, avenue du Colonel Roche / \/ \ phone +33/(0)5 61 33 63 63 31077 Toulouse Cedex / \ \ fax +33/(0)5 61 33 64 11 France / \ \ ____________________________________/ \____\___________________________

2 1

Re: Poly/ML Compilation Performance Problem
by David.Matthews＠prolingua.co.uk 25 Mar '02

25 Mar '02

Rob, I've had a look at this and found the problem. It turned out to be much simpler to fix than I'd feared and applying the diffs below reduces the compilation time from around 45 minutes to around 7 seconds! The problem had to do with the way Poly/ML inlines "small" functions. In order to get reasonably efficient code small functions are inserted inline. If they are tail-recursive they can get converted into something like while-loops. I changed this and improved it quite a bit in recent releases but it seems there was something left from a previous attempt at this which was getting in the way. It was causing recursive calls to be expanded inline when they shouldn't have been, leading to a massive code blow-up. It was actually the fact that you had functions of the form val rec f = fn x => fn y => ..... rather than the equivalent "fun" declaration that meant that the problem only showed up in your code and hadn't appeared before. Poly/ML treats fun declarations specially so that a function of the form fun f a b c = ... gets its arguments passed on the stack. That means that we save the cost of creating a closure except when the function is partially applied. That doesn't apply to the equivalent val rec declaration. Perhaps it could but that would require the front end to look quite closely at the body of the outer function to see whether it was simply another function. Let me know how you get on with this. Regards, David. RCS file: /usr/cvsroot/mlsource/MLCompiler/CodeTree/G_CODE.ML,v retrieving revision 1.22 diff -r1.22 G_CODE.ML 1122,1126c1122 < case pt of < Lambda _ => true < | Declar {value, ...} => isSmall (value, sizeOptVal) < | Newenv [c] => isSmall (c, sizeOptVal) < | _ => size pt < !maxInlineSize --- > size pt < !maxInlineSize On Saturday, March 2, 2002, at 01:01 , Rob Arthan wrote: > David, > > Last month, I ported another tool of ours called ClawZ to Poly/ML. > ClawZ is much smaller than the ML parts of ProofPower. Somewhat to my > surprise it contains some code which provokes a performance problem > in the compiler, which ends up taking about 45 minutes to compile the > last 2,400 or so lines of code on a 450MHz Pentium Xeon with 512Mb of > RAM. This is the only case I've encountered where Poly/ML underperforms > SML/NJ.

1 0

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