[Caml-list] Call for Participation: VSTTE 2009
* * * * VSTTE 2009 * * * *Workshop on Verified Software * *Theory Tools and Experiments * *(affiliated with Formal Methods Week) * * * * *** Call For Participation *** * * * * November 2, 2009* * Eindhoven, the Netherlands * *http://vstte09.lri.fr/ * * * * The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments.Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. Program === 09:00-10:00 - Rajeev Joshi, NASA JPL US TBA 10:30-11:30 - Discovering Specifications for Unknown Procedures with Separation Logic Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He and Wei-Ngan Chin. On Essential Program Annotations and Completeness of Verifying Compilers Bernhard Beckert, Thorsten Bormer and Vladimir Klebanov. 11:30-12:30 - Jim Woodcock, University of York UK TBA 13:30-14:30 - Pascal Cuoq, CEA France TBA 14:30-15:30 - SMT Solvers: New Oracles for the HOL Theorem Prover Tjark Weber. An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems Daisuke Ishii, Kazunori Ueda and Hiroshi Hosobe. 16:00-17:00 - John McDermott, Naval Research Lab US TBA Kalou Cabrera Castillos, INRIA Nancy France TBA Registration Participants can register for any combination of FM2009 activities, inclusing VSTTE 2009, at http://www.win.tue.nl/fmweek/Registration.html Deadline for (normal) registration is October 19. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Papers: PLPV 2010
Call For Papers Programming Languages meets Program Verification (PLPV) 2010 http://slang.soe.ucsc.edu/plpv10/ Tuesday, January 19, 2010 Madrid, Spain Affiliated with POPL 2010 Overview: The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example is dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms. Another example is extended static checking systems like Spec#, which extends C# with pre- and postconditions along with a static verifier for these contracts. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage cross-pollination between different communities, we seek a broad the scope for PLPV. In particular, submissions may have diverse foundations for verification (type-based, Hoare-logic-based, etc), target diverse kinds of programming languages (functional, imperative, object-oriented, etc), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, etc). Submissions: Submissions should fall into one of the following three categories: 1. Regular research papers that describe new work on the above or related topics. Submissions in this category have an upper limit of 12 pages, but shorter submissions are also encouraged. 2. Work-in-progress reports should describe new work that is ongoing and may not be fully completed or evaluated. Submissions in this category should be at most 6 pages in total length. 3. Proposals for challenge problems which the author believes is are useful benchmarks or important domains for language-based program verification techniques. Submissions in this category should be at most 6 pages in total length. Submissions should be prepared with SIGPLAN two-column conference format. Submitted papers must adhere to the SIGPLAN republication policy. Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. Papers should be submitted through Easychair, at http://www.easychair.org/conferences/?conf=plpv2010 Publication: Accepted papers will be published by the ACM and appear in the ACM digital library. Student Attendees: Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found on the workshop web page. PAC also offers support for companion travel. Important Dates: * Electronic submission: October 8, 2009, 11:59pm Samoa time (UTC-11) * Notification: November 8, 2009 * Final version: November 17, 2009 * Workshop: January 19, 2010 Organizers: * Cormac Flanagan (University of California, Santa Cruz) * Jean-Christophe Filliâtre (CNRS) Program Committee: * Adam Chlipala (Harvard University) * Ranjit Jhala (University of California, San Diego) * Joseph Kiniry (University College Dublin) * Rustan Leino (Microsoft Research) * Xavier Leroy (INRIA Paris-Rocquencourt) * Conor McBride (University of Strathclyde) * Andrey Rybalchenko (Max Planck Institute for Software Systems) * Tim Sheard (Portland State University) * Stephanie Weirich (University of Pennsylvania) ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Partially hiding modules in packages
Hi, Alexey Rodriguez a écrit : My question is about how to hide modules (or parts thereof) in an ocaml package from the outside world (users of the package). * Add the file foobar.mli which contains the signatures of Foo and Bar but hiding Foo.unsafe_change. I think it could work, but I would have to repeat much of the Foo and Bar interfaces. I tried this but it didn't work, ocaml complains as follows: That's the solution we followed in Mlpost (http://mlpost.lri.fr/) and it works fine (you may have a look at the Makefile.in in mlpost sources). Indeed, you have to repeat (parts of) the modules interfaces, but since it is where we put all the ocamldoc documentation, in a single file, it appears to be a satisfying solution. -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Why don't you use batteries?
I like writing my own libraries when I need some. Unfortunately, many people do that. Why do you say unfortunately? What was important in my answer was not the words my own libraries but the words I like. And you cannot find unfortunate that some people like programming :-) (But, of course, if this is to recode an existing library without any pleasure, I agree with you.) -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Why don't you use batteries?
8) Other (please explain) I like writing my own libraries when I need some. (But don't misread me: I don't see myself as a concurrent to Batteries, and I think you guys are doing a great job.) -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Second Call for Papers: VSTTE 2009
Due to many requests, the submission deadline for the VSTTE workshop has been extended. * * * * VSTTE 2009 * * * *Workshop on Verified Software * *Theory Tools and Experiments * * * *(affiliated with Formal Methods Week) * * * * November 2, 2009* * Eindhoven, the Netherlands * *http://vstte09.lri.fr/ * * * *Deadline for submissions: Sep 11, 2009* * * * FM 2009 is the sixteenth in a series of symposia of the Formal Methods Europe association, and the second one that is organized as a world congress. Ten years after FM'99, the 1st World Congress, the formal methods communities from all over the world will once again have an opportunity to meet. FM 2009 will be both an opportunity to celebrate, and an opportunity to join in when enthusiastic researchers and practitioners from a diversity of backgrounds and schools come together to discuss their ideas and experiences. The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments. Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. This includes topics like: * Program logic * Specification and verification techniques * Tool support for specification languages * Tool for various design methodologies * Tool integration and plug-ins * Automation in formal verification * Tool comparisons and benchmark repositories * Combination of tools and techniques (e.g. formal vs. semiformal, software specification vs. engineering techniques) * Customizing tools for particular applications Papers about tool architectures, and their achievements are most welcome. The contributed papers, which should report on previously unpublished work, can reflect current and preliminary work in areas of software verification. New technical results, overviews of new developments in software verification projects, short papers accompanying tool demonstrations, as well as position papers on how to further advance the goal of verified software are all welcome. SUBMISSION PROCEDURE VSTTE proceedings will be published as a special issue of the Software Tools for Technology Transfer (STTT) journal. Submitted papers should not have been submitted elsewhere for publication. Papers should use Springer-Verlag's STTT package ftp://ftp.springer.de/pub/tex/latex/svjour/sttt/, and should not exceed 15 pages including appendices. Papers are processed through the EasyChair conference management system. IMPORTANT DATES === Submission deadline September 11, 2009, 11:59pm Samoa time (UTC-11) Notification of acceptance October 2, 2009 Final version October 16, 2009 PROGRAM COMMITTEE = * David Deharbe, Dimap UFRN, Brazil * Dino Distefano, Queen Mary University of London, UK * Jean-Christophe Filliâtre (co-chair), CNRS, France * Leo Freitas (co-chair), University of York, UK * John McDermott, Naval Research Laboratory, USA * Yannick Moy, AdaCore, France * Arnaud Venet, Kestrel Technology, USA CONTACT === Leo Freitas, l...@cs.york.ac.uk Department of Computer Science University of York, YO10 5DD York, UK Tel: (+44) (0) 1904 434753 Jean-Christophe Filliatre, jean-christophe.fillia...@lri.fr CNRS / INRIA Saclay - Ile-de-france - ProVal Parc Orsay Universite, batiment N 4, rue Jacques Monod 91893 Orsay Cedex FRANCE Tel: (+33) (0)1 74 85 42 27 FURTHER INFORMATION === Further information will be put on the workshop web-page http://vstte09.lri.fr/. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] ocamlgraph predecessors
Hi, Benjamin Ylvisaker wrote: I have been using ocamlgraph for a while, and have been generally happy with it. I experienced some poor performance with moderately large graphs (10-100k vertices) recently, which led me to look through the source code a little. It seems that doing anything with the predecessors of a vertex, even just getting a list of them, requires scanning through all the vertices in a graph. This seems a little crazy to me. Am I missing something? Is there some kind of work-around that gives reasonable performance for predecessor operations (i.e. not O(|V|)). Not providing predecessors in constant time was a deliberate choice in Ocamlgraph. (A graph is basically a map which binds any vertex to the set of its successors, and that's it.) If you need efficient access to the predecessors, you have several workarounds: - implement your own graph data structure; after all, ocamlgraph was designed to clearly separate data structures and algorithms, so that you will still be able to use graph algorithms on your own graphs. - use the graph data structure Imperative.Digraph.ConcreteBidirectional, which is the only graph data structure in Ocamlgraph providing predecessors in constant time; it is actually the contribution of a user (Ted Kremenek) who experienced the same need as yourself. - memoize the results of the predecessors function (either in a modified version of the data structure or externally if your algorithm allows it). Hope this helps, -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Physical counterpart to Pervasives.compare?
Pascal Cuoq a écrit : Elnatan Reisner wrote: Is there something that can complete this analogy: (=) is to (==) as Pervasives.compare is to ___? The simple solution is to number at creation the objects that you want to physically compare, using an additional field. You can do that while hash-consing your values, which has many other benefits than allowing physical comparison, as explained in this paper: http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf Ocaml code for hash-consing can be found on that page: http://www.lri.fr/~filliatr/software.en.html Hope this helps, -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Papers: VSTTE 2009
We apologise if you receive this message more than once. * * * * VSTTE 2009 * * * *Workshop on Verified Software * *Theory Tools and Experiments * * * *(affiliated with Formal Methods Week) * * * * November 2, 2009* * Eindhoven, the Netherlands * *http://vstte09.lri.fr/ * * * *Deadline for submissions: Sep 4, 2009 * * * * FM 2009 is the sixteenth in a series of symposia of the Formal Methods Europe association, and the second one that is organized as a world congress. Ten years after FM'99, the 1st World Congress, the formal methods communities from all over the world will once again have an opportunity to meet. FM 2009 will be both an opportunity to celebrate, and an opportunity to join in when enthusiastic researchers and practitioners from a diversity of backgrounds and schools come together to discuss their ideas and experiences. The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments. Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. This includes topics like: * Program logic * Specification and verification techniques * Tool support for specification languages * Tool for various design methodologies * Tool integration and plug-ins * Automation in formal verification * Tool comparisons and benchmark repositories * Combination of tools and techniques (e.g. formal vs. semiformal, software specification vs. engineering techniques) * Customizing tools for particular applications Papers about tool architectures, and their achievements are most welcome. The contributed papers, which should report on previously unpublished work, can reflect current and preliminary work in areas of software verification. New technical results, overviews of new developments in software verification projects, short papers accompanying tool demonstrations, as well as position papers on how to further advance the goal of verified software are all welcome. SUBMISSION PROCEDURE Submitted papers should not have been submitted elsewhere for publication, should use the Springer-Verlag's package ftp://ftp.springer.de/pub/tex/latex/svjour/sttt/, and should not exceed 15 pages including appendices. Papers will be processed through the EasyChair conference management system. IMPORTANT DATES === Submission deadline September 4, 2009, 11:59pm Samoa time (UTC-11) Notification of acceptance October 2, 2009 Final version October 16, 2009 CONTACT === Leo Freitas, l...@cs.york.ac.uk Department of Computer Science University of York, YO10 5DD York, UK Tel: (+44) (0) 1904 434753 Jean-Christophe Filliatre, jean-christophe.fillia...@lri.fr CNRS / INRIA Saclay - Ile-de-france - ProVal Parc Orsay Universite, batiment N 4, rue Jacques Monod 91893 Orsay Cedex FRANCE Tel: (+33) (0)1 74 85 42 27 FURTHER INFORMATION === Further information will be put on the workshop web-page http://vstte09.lri.fr/. ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Papers: PLPV 2010
Call For Papers Programming Languages meets Program Verification (PLPV) 2010 http://slang.soe.ucsc.edu/plpv10/ Tuesday, January 19, 2010 Madrid, Spain Affiliated with POPL 2010 Overview: The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example is dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms. Another example is extended static checking systems like Spec#, which extends C# with pre- and postconditions along with a static verifier for these contracts. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage cross-pollination between different communities, we seek a broad the scope for PLPV. In particular, submissions may have diverse foundations for verification (type-based, Hoare-logic-based, etc), target diverse kinds of programming languages (functional, imperative, object-oriented, etc), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, etc). Submissions: Submissions should fall into one of the following three categories: 1. Regular research papers that describe new work on the above or related topics. Submissions in this category have an upper limit of 12 pages, but shorter submissions are also encouraged. 2. Work-in-progress reports should describe new work that is ongoing and may not be fully completed or evaluated. Submissions in this category should be at most 6 pages in total length. 3. Proposals for challenge problems which the author believes is are useful benchmarks or important domains for language-based program verification techniques. Submissions in this category should be at most 6 pages in total length. Submissions should be prepared with SIGPLAN two-column conference format. Submitted papers must adhere to the SIGPLAN republication policy. Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. Publication: Accepted papers will be published by the ACM and appear in the ACM digital library. Student Attendees: Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found on the workshop web page. PAC also offers support for companion travel. Important Dates: * Electronic submission: October 8, 2009, 11:59pm Samoa time (UTC-11) * Notification: November 8, 2009 * Final version: November 17, 2009 * Workshop: January 19, 2010 Organizers: * Cormac Flanagan (University of California, Santa Cruz) * Jean-Christophe Filliâtre (CNRS) Program Committee: * Adam Chlipala (Harvard University) * Ranjit Jhala (University of California, San Diego) * Joseph Kiniry (University College Dublin) * Rustan Leino (Microsoft Research) * Xavier Leroy (INRIA Paris-Rocquencourt) * Conor McBride (University of Strathclyde) * Andrey Rybalchenko (Max Planck Institute for Software Systems) * Tim Sheard (Portland State University) * Stephanie Weirich (University of Pennsylvania) ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Call for Papers: PLMMS 2009
The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be co-located with TPHOLs 2009. General Information The scope of this workshop is at the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes present-day computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to: * Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems. * Mathematical modeling languages used for programming: covers the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational world view? * Programming languages with mathematical specifications: covers advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality. * Language elements for program verification: covers specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way? These issues have a very colorful history. Many PL innovations first appeared in either CA or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in MMS design that may be relevant to future programming languages, or conversely novel PL principles that improve upon implementation and deployment of MMS. Why are all the languages of mainstream CA systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modeling? How can MMS regain the upper hand on issues of genericity and modularity? What are the biggest barriers to using a more mainstream language as a host language for a CAS or PA/ATP? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details * Submission deadline: May 11, 2009 (Apia, Samoa time) * Author Notification: June 22, 2009 * Final Papers Due: July 10, 2009 * Workshop: August 21, 2009 Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas AM University (Co-Chair) * Jean-Christophe Filliâtre, CNRS Université Paris Sud * Predrag Janicic, University of Belgrade * Jaakko Järvi, Texas AM University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (Co-Chair) * Makarius Wenzel
Re: Re : [Caml-list] ocamlgraph ConcreteBidirectional and Dot
I have a question related to this: Is there a reason for the absence of a ConcreteBidirectionalLabeled graph in the API? Simply an historical reason: the module ConcreteBidirectional is an external contribution (by Ted Kremenek), which was only recently added to Ocamlgraph. Anybody can contribute to a ConcreteBidirectionalLabeled module and we'll happily add it to Ocamlgraph. -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Parsing 64-bit ints in 32-bit OCaml
Jon Harrop a écrit : I'm just trying to write efficient functions for div and mod by three. I'd like to handle 32- and 64-bit machines with the same code so I tried: let gcd3 = match Sys.word_size with | 32 - 715827883 | 64 - 3074457345618258603 | _ - failwith Unknown word size That works perfectly in 64-bit but breaks OCaml's parser in 32-bit, which dies with: Integer literal exceeds the range of representable integers of type int As a workaround, I replaced it with: | 64 - Int64.to_int 3074457345618258603L Is there a better workaround? I also bump into the same problem from time to time, and I usually replace the large constant by a (launch time) computation, such as (0x lsl 16) lor 0x for 0x for instance. In your case, it could simply be (3074457 * 100 + 345618) * 100 + 258603 But your solution is equally good (the int64 is boxed but is simpler to read). -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] announce : Mlpost 0.5
Dear list, We are pleased to announce the first release of Mlpost, an Ocaml interface to MetaPost, a powerful software to draw pictures to be embedded in LaTeX documents. Mlpost is free software under LGPL license and is available at http://mlpost.lri.fr/ Some examples are available online (thanks to Martin Jambon's caml2html): http://mlpost.lri.fr/examples/ You can have a look at Mlpost's API online: http://mlpost.lri.fr/doc/Mlpost.html Have fun with Mlpost, -- the Mlpost authors, Romain Bardou, Johannes Kanig, Stéphane Lescuyer and Jean-Christophe Filliâtre ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] New Ocaml Plug-in for NetBeans
Lukasz Stafiniak a écrit : On Tue, Jul 29, 2008 at 4:16 PM, Damien Doligez [EMAIL PROTECTED] wrote: OCaml 3.11 has extended .annot files that will allow external tools to do that. Also, it tells you which function calls are tail calls and which are normal calls. Cool! Are the http://osp.janestcapital.com/files/ocamlwizard.pdf project participants following this? Would be nice to hear their progress report :) They tried, indeed (I'm kind of helping in that projet, so I'm aware of the progress). Unfortunately, even with the CVS version of Ocaml, the .annot files appear to lack some information. But the solution currently followed by Ocamlwizard is along the lines of .annot files, and may even rely on these files in future version of Ocaml. -- Jean-Christophe ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Problem with module inclusion
Fabrice Marchant a écrit :
Here is a counter functor : *)
[...]
(* before Counters, that would be modified this way :
*)
module Counters ( X : Map.OrderedType ) :
sig
module XMap :
sig
type 'a t = 'a Map.Make(X).t
val empty : 'a t
val add : X.t - 'a - 'a t - 'a t
val find : X.t - 'a t - 'a
val fold : (X.t - 'a - 'b - 'b) - 'a t - 'b - 'b
val equal : ('a - 'a - bool) - 'a t - 'a t - bool
end
type t = int XMap.t
val equal : t - t - bool
val zeroes : t
val incr : t - X.t - t
end
=
struct
module XMap = MapPlus ( Map.Make( X ) )
type t = int XMap.t
let equal = XMap.equal ( = )
let zeroes = XMap.empty
let incr map e =
(XMap.add e
(try succ (XMap.find e map)
with Not_found - 1)) map
end
(* unfortunately this doesn't work : how to access 'to_list' function through
the Counters module ? With StringCounters.XMap.to_list ?
I'm confused. Should the Counters signature be modified ?
You need
- either to export to_list in signature of XMap above as
val to_list : 'a t - (X.t * 'a) list
and then you'll be able to write StringCounters.XMap.to_list in your
example
- or to re-export it in module Counters, as
let to_list = XMap.to_list
and to declare it in signature of module Counters, as
val to_list : t - (X.t * int) list
and then to use it as StringCounters.to_list in your example.
Hope this helps,
--
Jean-Christophe
___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] Tries are to sequences as ? is to trees
Jon Harrop a écrit : So tries let us associate sequences with values. What data structure lets us associate trees with values? In Okasaki's book, there is a Section 10.3.2 Generalized Tries which addresses exactly this problem. The solution proposed is more efficient than building the list of elements with fold. -- Jean-Christophe Filliâtre http://www.lri.fr/~filliatr/ ___ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
