Re: [Caml-list] Bigarray question: Detecting subarrays, overlaps, ...
Gerd Stolpmann i...@gerd-stolpmann.de writes: What I did not understand up to now: It is really easy to keep all this information in a helper data structure. Why extend Bigarray? Gerd A helper data structure would mean keeping track of that information on my own complicating the source and wasting memory at runtime. On the other hand what I suggested only makes use of what is already there in the Bigarray data structure. The functions would only make that information available to the user. I'm not a fan of duplicating information that is already there. Worst case the helper data structure could be wrong due to some bug in the code. MfG Goswin -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] Camlp5 6.04 - configurable name
Hi, New release of Camlp5 (6.04) where: The *names* of all what are built (executables, library) are now configurable, allowing to have 'strict' and 'transitional' modes both installed in the same computer in different places. Example: ./configure --strict make world.opt make install ./configure --transitional name=camlp5t make world.opt make install In that case, executables in transitional mode are camlp5t, camlp5to, camlp5tr and so on... and the library is installed in a directory named camlp5t instead of camlp5. No conflict between the two modes. Download at: http://pauillac.inria.fr/~ddr/camlp5/ Thanks. -- Daniel de Rauglaudre http://pauillac.inria.fr/~ddr/ -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] [VMCAI2012] Professor/Associate professor in Formal Methods
CHALMERS University of Technology, Gothenburg, Sweden Department of Computer Science and Engineering Professor/Associate professor in Formal Methods The Department has 76 faculty members and enrols about 70 PhD students from more than 30 countries. The research spans the whole spectrum, from theoretical underpinnings to applied systems development. There is extensive national and international collaboration with academia and industry all around the world. The Division of Software Technology has around 15 faculty members and 25 postdocs and PhD students. We conduct successful research in functional programming, automatic theorem-proving, hardware design and verification, property-based testing of software, language-based security, and software verification. The scientific area of the new position is Formal Methods, interpreted broadly so as to include at least - formal specification, development and verification of software, - automatic theorem-proving and model-checking, - lightweight formal methods, including testing, - program semantics and analysis. Application deadline: March 22nd For more information see that full advertisement at http://www.chalmers.se/en/about-chalmers/vacancies/Pages/default.aspx (Select Professor/Associate professor in formal methods, published 17/02/2012) -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] types not equal when I expect them to be
The following code fails to compile: - a.ml module Foo = struct module St = struct type t = string let compare = compare end module Map (* : Map.S with type key = St.t *) = Map.Make(St) (* module Map = Map.Make(struct type t = string let compare = compare end) *) end module Bar = struct type t = int Foo.Map.t end module Pack = struct module Foo = Foo module Bar = Bar end open Pack let x : Bar.t = Foo.Map.empty $ ocamlc -c foo.ml File foo.ml, line 20, characters 16-29: (* refers to Foo.Map.empty on last line *) Error: This expression has type 'a Pack.Foo.Map.t = 'a Map.Make(Pack.Foo.St).t but an expression was expected of type Pack.Bar.t = int Map.Make(Foo.St).t So Pack.Foo and Foo are not compatible. By trial and error, I found two ways to resolve the problem: 1) Provide an explicit signature for Foo.Map (uncomment the provided signature), or 2) Inline the structure passed to Map.Make (comment out first definition of Foo.Map and uncomment the second one) But I don't understand why. Can anyone explain the main points. Thank you. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] compiling static preprocessors
Dear camlp4 experts, I'm trying to compile a static version of a preprocessor built from type-conv and sexplib. I've tried: ocamlc dynlink.cma unix.cma \ -I +camlp4 camlp4lib.cma -linkall \ Camlp4Parsers/Camlp4OCamlRevisedParser.cmo \ Camlp4Parsers/Camlp4OCamlParser.cmo \ Camlp4Parsers/Camlp4OCamlRevisedParserParser.cmo \ Camlp4Parsers/Camlp4OCamlParserParser.cmo \ Camlp4Printers/Camlp4AutoPrinter.cmo \ Camlp4Bin.cmo \ -I +site-lib/type-conv pa_type_conv.cma \ -I +site-lib/sexplib pa_sexp_conv.cma \ -o sexppp I've taken the first lines by greping camlp4o.native in ocaml-3.12.1/_build/_log and I've appended what normally follows camlp4o when using sexplib. The command succeeds at building sexppp, but unfortunately, the preprocessor doesn't work as expected: ./my_pp foo.ml gives: Parse error: [semi] expected after [str_item] (in [implem]) for any type followed by with sexp in foo.ml. I am trying to do something crazy or is there a chance to make it work? Cheers, Thomas -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] compiling static preprocessors
Le Thu, 1 Mar 2012 20:58:38 +0100, Thomas Gazagnaire thomas.gazagna...@gmail.com a écrit : ocamlc dynlink.cma unix.cma \ -I +camlp4 camlp4lib.cma -linkall \ Camlp4Parsers/Camlp4OCamlRevisedParser.cmo \ Camlp4Parsers/Camlp4OCamlParser.cmo \ Camlp4Parsers/Camlp4OCamlRevisedParserParser.cmo \ Camlp4Parsers/Camlp4OCamlParserParser.cmo \ Camlp4Printers/Camlp4AutoPrinter.cmo \ Camlp4Bin.cmo \ -I +site-lib/type-conv pa_type_conv.cma \ -I +site-lib/sexplib pa_sexp_conv.cma \ -o sexppp I've taken the first lines by greping camlp4o.native in ocaml-3.12.1/_build/_log and I've appended what normally follows camlp4o when using sexplib. The command succeeds at building sexppp, but unfortunately, the preprocessor doesn't work as expected: ./my_pp foo.ml gives: Parse error: [semi] expected after [str_item] (in [implem]) for any type followed by with sexp in foo.ml. I am trying to do something crazy or is there a chance to make it work? It is because Camlp4Bin.cmo is linked before pa_type_conv.cma and pa_sexp_conv.cma, and so side-effects of theses modules are not yet performed when the camlp4 main function run. Camlp4Bin.cmo must be the last file on the command line. Cheers, -- Jérémie -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] types not equal when I expect them to be
Note that Bar is actually unnecessary. The following code exhibit the exact same behavior: module Foo = struct module St = struct type t = string let compare = compare end module Map (* : Map.S with type key = St.t *) = Map.Make(St) (* module Map = Map.Make(struct type t = string let compare = compare end) *) end module Pack = struct module Foo = Foo end let x : int Foo.Map.t = Pack.Foo.Map.empty The important point is the interface of Map.Make when looked through the environment (for example when rebound by `module F = Map.Make`, then compiled with `ocamlc -i`): functor (Ord : Map.OrderedType) - sig type key = Ord.t type 'a t = 'a Map.Make(Ord).t ... end Note the `'a t = 'a Map.Make(Ord).t` part: this is the result of a so-called strenghening operation, where the abstract types `t` in the signature of the module `M` are noted to be equal to `M.t`; this allows `N` to remain type-compatible with `M` when writing `module N = M`. Now the result of this strenghtening operation in your case is that your module Map defined in Foo has in its signature: type 'a t = 'a Map.Make(Foo.St).t The sorrow and non-intuitive point is that, after rebinding in Pack, Pack.Foo gets the following signature: type 'a t = 'a Map.Make(Pack.Foo.St).t Those two type are not path-compatible because `Pack.Foo.St` is not a path syntactically equal to `Foo.St` -- I'm not sure why the type-checker couldn't check path equality upto known module aliasing, however. Now, why your fixes work: 1. by adding the `: Map.S with type key = ...` signature to your Foo.Map module, you seal the module under the Map.S signature which has its type `'a t` *abstract*. This cancels the effects of strenghtening in the definition of `Foo.Map`. Now, in the definition of Pack, aliasing `module Foo = Foo` re-apply strenghtening, and you get a `Pack.Foo` module with `type 'a t = Foo.Map.t`, so those two are compatible. 2. by applying `struct type t = String let compare = compare` directly instead of naming it `Foo.St`, you apply a module that is not itself a path, so the typing rules change and you get `'a Foo.Map.t` abstract as in the first case. 3. You could also define `St` out of `Foo`, so that types in both Foo and Pack.Foo have `type 'a t = Map.Make(St).t`. You are surely aware that could similarly use stdlib's `String` directly which provides a `compare` operation. I believe this explains the observed behaviour of the type-checker -- the experts will surely correct if I made technical mistakes. I'm not sure however whether this behavior is expected (or could be considered slightly buggy), or if it is imposed by theoretical restrictions or implementation considerations. On Thu, Mar 1, 2012 at 5:38 PM, Ashish Agarwal agarwal1...@gmail.com wrote: The following code fails to compile: - a.ml module Foo = struct module St = struct type t = string let compare = compare end module Map (* : Map.S with type key = St.t *) = Map.Make(St) (* module Map = Map.Make(struct type t = string let compare = compare end) *) end module Bar = struct type t = int Foo.Map.t end module Pack = struct module Foo = Foo module Bar = Bar end open Pack let x : Bar.t = Foo.Map.empty $ ocamlc -c foo.ml File foo.ml, line 20, characters 16-29: (* refers to Foo.Map.empty on last line *) Error: This expression has type 'a Pack.Foo.Map.t = 'a Map.Make(Pack.Foo.St).t but an expression was expected of type Pack.Bar.t = int Map.Make(Foo.St).t So Pack.Foo and Foo are not compatible. By trial and error, I found two ways to resolve the problem: 1) Provide an explicit signature for Foo.Map (uncomment the provided signature), or 2) Inline the structure passed to Map.Make (comment out first definition of Foo.Map and uncomment the second one) But I don't understand why. Can anyone explain the main points. Thank you. -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Re: [Caml-list] compiling static preprocessors
Camlp4Bin.cmo must be the last file on the command line. Thanks Jérémie, this indeed fixes part of the problem. Now, I get a new error message: Fatal error: exception Not_found Raised at file camlp4/Camlp4/Struct/Grammar/Delete.ml, line 131, characters 16-25 Called from file camlp4/Camlp4/Struct/Grammar/Delete.ml, line 146, characters 17-56 Called from file lib/pa_type_conv.ml, line 421, characters 12-62 where pa_type_conv.ml:421 is: DELETE_RULE Gram str_item: module; a_UIDENT; module_binding0 END; So I suppose the OCaml grammar is not yet registered when type-conv tries to remove the rule. Oh dear... Any thoughts on this one? -- Thomas -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
[Caml-list] LOLA 2012 -- call for contributed talks
*** CALL FOR CONTRIBUTED TALKS *** LOLA 2012 Syntax and Semantics of Low Level Languages Sunday 24th June 2012, Dubrovnik, Croatia A LICS 2012-affiliated workshop http://www.ccs.neu.edu/home/amal/lola2012 IMPORTANT DATES Submission deadline Friday 13th April 2012 Author notification Monday 30th April 2012 WorkshopSunday 24th June 2012 SUBMISSION LINK The submissions will be made by easychair at https://www.easychair.org/conferences/?conf=lola2012 DESCRIPTION OF THE WORKSHOP It has been understood since the late 1960s that tools and structures arising in mathematical logic and proof theory can usefully be applied to the design of high level programming languages, and to the development of reasoning principles for such languages. Yet low level languages, such as machine code, and the compilation of high level languages into a low level ones have traditionally been seen as having little or no essential connection to logic. However, a fundamental discovery of this past decade has been that low level languages are also governed by logical principles. From this key observation has emerged an active and fascinating new research area at the frontier of logic and computer science. The practically-motivated design of logics reflecting the structure of low level languages (such as heaps, registers and code pointers) and low level properties of programs (such as resource usage) goes hand in hand with the some of the most advanced contemporary researches in semantics and proof theory, including classical realizability and forcing, double orthogonality, parametricity, linear logic, game semantics, uniformity, categorical semantics, explicit substitutions, abstract machines, implicit complexity and sublinear programming. The LOLA workshop, affiliated with LICS, will bring together researchers interested in many aspects of the relationship between logic and low level languages and programs. Topics of interest include, but are not limited to: Typed assembly languages, Certified assembly programming, Certified and certifying compilation, Proof-carrying code, Program optimization, Modal logic and realizability in machine code, Realizability and double orthogonality in assembly code, Parametricity, modules and existential types, General references, Kripke models and recursive types, Continuations and concurrency, Implicit complexity, sublinear programming and Turing machines, Closures and explicit substitutions, Linear logic and separation logic, Game semantics, abstract machines and hardware synthesis, Monoidal and premonoidal categories, traces and effects. SUBMISSION INFORMATION: LOLA is an informal workshop aiming at a high degree of useful interaction amongst the participants, welcoming proposals for talks on work in progress, overviews of larger programmes, position presentations and short tutorials as well as more traditional research talks describing new results. The programme committee will select the workshop presentations from submitted proposals, which may take the form either of a short abstract or of a longer (published or unpublished) paper describing completed work. PROGRAM CO-CHAIRS: Amal Ahmed (Northeastern University) Aleksandar Nanevski (IMDEA Software) PROGRAM COMMITTEE: Cristiano Calcagno (Imperial College London and Monoidics Limited) Robert Dockins (Princeton University) Martin Hofmann (LMU Munich) Xavier Leroy(INRIA Rocquencourt) Andrzej Murawski(University of Leicester) Sungwoo Park(Pohang University of Science and Technology) Dusko Pavlovic (Royal Holloway, University of London) Andreas Rossberg(Google) -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
