Poly/ML

polyml@lists.polyml.org

2 participants
698 discussions

Poly/ML codetree generation
by yli＠cse.tamu.edu 01 Mar '11

01 Mar '11

Dear David, So far I've been able to generate Poly/ML style codetree for a subset of Spad language used in OpenAxiom. The codetree is written into a text file. As an example, for the following spad function: foo (a : Integer) : Integer == a := a + 1 a I currently generate the following intermediate code: DECL #1{0 uses} = LAMBDA( foo(2) CL=false CR=0 LEV=0 LOCALS=0 ARGS=G ARGLIVES= RES=G CLOS=() BLOCK(BLOCK(DECL #2{0 uses} = RECCONSTR(PARAM(0,1), PARAM(0,2)); BLOCK(DECL #3{0 uses} = GLOBAL (FUN "run_call2(1)", LAMBDAINLINE( runcall2(1) CL=false CR=0 LEV=0 LOCALS=0 ARGS=G ARGLIVES= RES=G CLOS=() LOCAL(1,1) G $(INDIRECT(0, PARAM(0,1)) G, INDIRECT(1, PARAM(0,1)) G)){LAMBDA} ) (*GLOBAL*){early} G $(INDIRECT(0, LOCAL(0, 2)), LIT1 G); DECL #4{0 uses} = LOCAL(0, 3); LOCAL(0, 4) ) ) )){LAMBDA}" I also wrote a ML library which reads in and parses the codetree string. Does my current approach look sensible to you? What would you suggest if improvements are needed? I'm thinking that the next step for me is to call Poly/ML middle functions that would take the codetree and evaluate the entire codetree for a Spad function (and then hopefully a Spad domain.) I've read the code and the documentation in the codetree source code files. Is there any way for me to call the codetree functions as a library in my ML code? Thanks, Yue

2 4

Type abbreviations and pretty-printing of function types
by rda＠lemma-one.com 24 Feb '11

24 Feb '11

In the following, the result type of the function add_abs gets printed out as {a : int, b : string} rather than as AB: type AB = {a : int, b : string}; fun add_abs ({a = a1, b = b1} : AB) ({a = a2, b = b2} : AB) : AB = ( {a = a1 + a2, b = b1 ^ b2} ); structure S1 = struct type AB = {a : int, b : string}; fun add_abs ({a = a1, b = b1} : AB) ({a = a2, b = b2} : AB) : AB = ( {a = a1 + a2, b = b1 ^ b2} ); end; open S1; To get it to print as AB, you have to do something like the following: val (add_abs : AB -> AB -> AB) = fn {a = a1, b = b1} => fn {a = a2, b = b2} => {a = a1 + a2, b = b1 ^ b2}; (which generates less efficient code, doesn't it?), or: signature S2 = sig type AB = {a : int, b : string}; val add_abs : AB -> AB -> AB; end; structure S2 : S2 = S1; This can be quite distracting if you have a structure type with lots of fields or some other complex type with a familiar name (like the type of tactics in an LCF-style theorem-prover). Regards, Rob.

1 0

InternalError: jump too large raised while compiling
by David.Matthews＠prolingua.co.uk 21 Feb '11

21 Feb '11

Thanks. That enabled me to see what was going wrong. I've committed a fix to SVN and the file compiles, at least as far as complaining about some missing declarations, on X86-32 and X86-64. You will need to run make compiler if you want to use the SVN version. Regards, David On 21/02/2011 06:55, Andreas Lochbihler wrote: > Dear David, > > please find attached the ML file that reproduces the error. I ran > Poly/ML on x86, Ubuntu GNU/LInux, both 32-bit and 64-bit. > > Andreas

1 0

Building MS Windows applications
by rda＠lemma-one.com 19 Feb '11

19 Feb '11

I have installed Poly/ML on MS Windows using the precompiled binary. Now I want to start building my own applications. What do I need for the equivalent in MS Windows of the following command line that I would use on UNIX? cc -o hello hello.o -lpolymain -lpolyml I.e., where do I find the polymain and polyml DLLs and what developer kits can I use? E.g., will MinGW work? And which developer kits are recommended? Regards, Rob.

2 4

InternalError: jump too large raised while compiling
by andreas.lochbihler＠kit.edu 19 Feb '11

19 Feb '11

Dear all, I use Isabelle to generate ML code from my formalisation in Isabelle. When I try to load the output ML file in Poly/ML 5.4, I get the following exception: Exception- InternalError: jump too large raised while compiling Exception- Fail "Exception- InternalError: jump too large raised while compiling" raised It occurs when Poly/ML processes a structure with a large function definition (2750 lines of ML code). The same error occurs with Poly/ML 5.3. What could I do to avoid this error? Are there any options to Poly/ML that allow larger jumps? Changing the code itself is difficult as it is automatically generated. If it helps, I can provide the ML file. Regards, Andreas -- Karlsruher Institut f?r Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler(a)kit.edu http://pp.info.uni-karlsruhe.de KIT - Universit?t des Landes Baden-W?rttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

2 1

HTTP protocol socket code
by ldixon＠inf.ed.ac.uk 17 Feb '11

17 Feb '11

[ apologies for cross-posting, the more appropriate sml-list is populated only by spam-bots :( ] Hi, Does anyone know of some HTTP code written in ML? I'd like to programmatically, in ML, do some web-queries... cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

3 2

Re: On understanding Poly/ML function definition IR
by David.Matthews＠prolingua.co.uk 09 Feb '11

09 Feb '11

On 08/02/2011 00:31, Yue Li wrote: > I'm trying to get better understanding about the code tree of Poly/ML > function definition. I would appreciate if I can gain some insights from > you. > > For instance, given the following definition: > > > fun f a b = a + b; The first point to appreciate is that this is syntactic sugar for val rec f = fn a => fn b => op+ (a, b); However this general form isn't the best way of compiling the function. Frequently a curried function is applied to several or all of its arguments e.g. val x = f y z Using the general form would be inefficient. Applying f to y would result in a closure being created on the heap which would then be applied to z. Instead Poly/ML processes "fun" declarations specially. fun f a b = a + b is rewritten as val rec f' = fn <a,b> => a + b and rec f = fn_inline a => fn_inline b => f'<a,b> i.e. a pair of mutually recursive functions, because f' could contain recursive applications of f. The <> here denote multiple arguments in registers or on the stack, something that doesn't have an exact equivalent in ML since every function takes exactly one argument. > The compiler prints out 3 sections of code tree: a block, a lambda and > another block: > > BLOCK(MUTUAL(DECL #2{0 uses} = > LAMBDA( > f(2) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G G > ARGLIVES= > RES=G CLOS=() > BLOCK(BLOCK(DECL #1{0 uses} = RECCONSTR(PARAM(0,1), PARAM(0,2)); > DECL #3{0 uses} = LOCAL(0,1); > DECL #4{0 uses} = INDIRECT(0, LOCAL(0,3)); > DECL #5{0 uses} = INDIRECT(1, LOCAL(0,3)); > GLOBAL (FUN "run_call2(1)", > LAMBDAINLINE( > run_call2(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LOCAL(1,1) G > $(INDIRECT(0, PARAM(0,1)) G, INDIRECT(1, PARAM(0,1)) G)){LAMBDA} > ) (*GLOBAL*){early} G $(RECCONSTR(LOCAL(0,4), LOCAL(0,5)) G) > ) > )){LAMBDA} AND This is the body of "f'". The name "f(2)" represents that it takes two arguments but the name is only used for exception tracing and profiling. It has no significance to ML. > > DECL #1{0 uses} = > LAMBDAINLINE( > f(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LAMBDAINLINE( > f(1)(1) > CL=false CR=0 LEV=0 LOCALS=0 > ARGS=G > ARGLIVES= > RES=G CLOS=() > LOCAL(2,2) G $(PARAM(0,1) G, PARAM(1,1) G)){LAMBDA}){LAMBDA} > ); This is the body of "f". It consists of two inline functions, one inside the other. > RECCONSTR(LOCAL(0,1)) > ) This is the result of a top-level declaration. The final result is a 1-tuple containing a reference to the function "f". Actually because these are all small functions it's likely that the result will be the reference to the code-tree itself so that subsequent uses of "f" at the top-level will expand the code in-line and reduce down to a use of the addition operation. Top-level declarations can be simple function declarations such as this example but just as often they involve extensive computation and return the results as multiple declarations. > I have three questions regarding this block: > > (1) First I'm wondering what do LOCAL(2, 2), and LOCAL(1, 1) refer to? > My understanding so far is that the second number of the LOCAL operator > means the number of DECL, but what does the first number refers to? This is the nesting depth. Zero means local to the function, one means local to the immediately containing function etc. So LOCAL(2,2) G $(PARAM(0,1) G, PARAM(1,1) G)) means: apply the function declared by a DECL #2 two levels out to the first or only parameter of the current function and the first or only parameter of the immediately containing function. (Oh, there's some oddity about the order of multiple parameters). I hope this answers your other questions as well but let me know if you'd like any more clarification. Regards, David

2 1

Isabelle/ML IDE based on jEdit
by makarius＠sketis.net 09 Feb '11

09 Feb '11

The following might be interesting to people working with Standard ML on the Poly/ML platform. The Isabelle2011 release includes an experimental Prover IDE based on Scala and jEdit that can be also used as one for Standard ML, thanks to the tight integration of Poly/ML into the prover environment. Thus semantic annotations produced by the Poly/ML compiler are presented as tool tips and hyperlinks in the source. This is a simple corollary of much more involved prover infrastructure, and David Matthews has provided some functionality to connect to that quite some time ago. See http://isabelle.in.tum.de/download.html for the regular Isabelle download and installation instructions. An editor session can be started like this (from the shell): Isabelle2011/bin/isabelle jedit -l Pure Test.thy Then Test.thy file can be populated like this: theory Test imports Pure begin ML {* fun fact 0 = 1 | fact n = n * fact (n - 1); *} ML {* fact 42 *} end Now it is possible to hover over the ML text while holding CONTROL (or COMMAND on Mac OS X) to see some of the content produced by the Poly/ML IDE support, rendered as tooltips and hyperlinks. Here is another example: ML {* length *} Hovering with CONTROL/COMMAND will expose a hyperlink pointing to the Poly/ML library sources. For non-prover people it might look a bit odd to embed ML text like that into a formal theory file. At a later stage there will be also management for individual ML files. The document model is stateless as far as ML bindings are concerned. Global side-effects via reference variables are an exception to that. (In the Isabelle context mutable state is never used in application code.) Anybody interested in the augmented Isabelle/ML itself should take a look at chapter 0 of http://isabelle.in.tum.de/dist/Isabelle2011/doc/implementation.pdf There is also some support for parallel functional programming using futures, which did not make it into the manual yet. See http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf for some overview. Makarius

1 0

CInterface problem on SPARC/Solaris
by mmoel＠t-online.de 27 Jan '11

27 Jan '11

An HTML attachment was scrubbed... URL: http://lists.inf.ed.ac.uk/mailman/private/polyml/attachments/20110126/948a2…

2 3

Poly/ML 32-bit and memory usage
by noschinl＠in.tum.de 18 Jan '11

18 Jan '11

Hi all, I'm trying to build JinjaThreads, a massive Isabelle theory, using the 32-bit linux version of Poly/ML 5.4.0. The machine is equipped with 6 GiB of RAM and runs a 64-bit linux kernel. After a while, Poly/ML aborts with "Run out of store - interrupting threads". But at this time, the poly process only has allocated around 2.7GiB of memory (VIRT). Why does Poly/ML does not try to allocate more memory? I tried to request a bigger initial heap size with "-H 3500", but this seemed to result in a heap size of 2GiB. As I tested with a small C program, a 32-bit process can allocate (and use) 4070MiB on this machine. Greetings, Lars

1 0

← Newer
1
...
39
40
41
42
43
44
45
...
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