1 Nov 2006 06:40

design problem

```Hi all,
I've the following code to write types and functions in an extensible
way, so to re-use my code a bit. Everything seems working fine.

I've two questions:
- Is there a better way of achieving a similar result ? Here I'm using
polymorphic variants, but I'm wondering if somebody already cooked
something together by using variants and camlp4 extensions...
- At the moment type errors are pretty horrible. How can I coerce these
functions to give prettier errors ? I've tried to coerce the function
f in the *_aux functions below, but of course this is not possible as
it needs to be polymorphic by design ...

thanks :)
p

(* my basic data type *)
type 'a termpc =
[`And of 'a * 'a
|`Or of 'a * 'a
|`Not of 'a
|`Atom of string
]
;;

(* a simple normal form function *)
let nnfpc_aux f = function
|`Not ( `Not x   )  -> f x
|`Not ( `And(x,y) ) -> `Or  (f (`Not x), f (`Not y) )
|`Not ( `Or (x,y) ) -> `And (f (`Not x), f (`Not y) )
```

1 Nov 2006 07:53

Re: design problem

```From: Pietro Abate <Pietro.Abate <at> anu.edu.au>

> I've the following code to write types and functions in an extensible
> way, so to re-use my code a bit. Everything seems working fine.
>
> I've two questions:
> - Is there a better way of achieving a similar result ? Here I'm using
>   polymorphic variants, but I'm wondering if somebody already cooked
>   something together by using variants and camlp4 extensions...

No idea, but polymorphic variants are supposed to be good at this
If you like modules, you might want to try combining with private row
types and recursive modules (see the paper in publications), but
whether it helps or not depends on the size of your code.

> - At the moment type errors are pretty horrible. How can I coerce these
>   functions to give prettier errors ? I've tried to coerce the function
>   f in the *_aux functions below, but of course this is not possible as
>   it needs to be polymorphic by design ...

You can perfectly write polymorphic type annotations.
after inference.
Note that I removed the catch-all cases in your pattern-matchings, are
they greatly reduce the interest of using polymorphic
variants. However I had to leave one for `Not, as otherwise the
parameter would not be extensible.

I also enclose a version using private row types, which separates
positive and negative cases, so as to remove all catch-all cases.
```

1 Nov 2006 13:12

Functional programming using caml light

```Hello,
in this book ( http://caml.inria.fr/pub/docs/fpcl/index.html ), there is
the following grammar (chapter 10.3, on streams etc...) :

Expr ::= Mult
| Mult + Expr
| Mult - Expr

[...]

after factoring common prefixes, the author obtains :

Expr ::= Mult RestExpr

RestExpr ::= + Mult RestExpr
|- Mult RestEXpr
|(* nothing *)

[...]

But I don't obtain the same result for RestExpr :

RestExpr ::= + Mult Expr
|- Mult Expr
| (* nothing *)

Am I wrong ? (and why ?)

----------------------------------

```

1 Nov 2006 13:42

Re: Functional programming using caml light

```ciol wrote:

> after factoring common prefixes, the author obtains :
>
> Expr ::= Mult RestExpr
>
> RestExpr ::= + Mult RestExpr
>             |- Mult RestEXpr
>             |(* nothing *)
>
> [...]
>
> But I don't obtain the same result for RestExpr :
>
> RestExpr ::= + Mult Expr
>             |- Mult Expr
>             | (* nothing *)
>

_Sorry_, it's an error, I obtain :
RestExpr ::= + Expr
| - Expr
| (* nothing *)

But I've just realized that the author's solution is in fact the same as
mine (he replaced Expr in RestExpr by Mult RestExpr. But why ? Isn't it
more complicated ? The result in caml will be identical  wont it be ?

_______________________________________________
Caml-list mailing list. Subscription management:
```

1 Nov 2006 14:02

Bedwyr 1.0

```Hi list,

We would like to announce the first release of a new system written in
OCaml. Bedwyr is an extended logic programming language that allows
model-checking directly on syntactic expressions possibly containing
bindings.

We believe that it's an interesting tool for computer scientists, as
it allows simple reasoning on declarative specifications, with several
good examples, notably bisimulation checking for the pi-calculus.
Other examples include type systems, games, logics, etc.

But another interest for the caml-list readers might be the re-usable
core components of Bedwyr, notably higher-order pattern unification
and term indexing. Although we don't distribute these separately, I'd
be happy to do so if anybody is interested.

You will find a general description of Bedwyr below this message.
More details can be found on Bedwyr website:
http://slimmer.gforge.inria.fr/bedwyr/

Sincerely,

Bedwyr developers

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Bedwyr
A proof-search approach to model checking
http://slimmer.gforge.inria.fr/bedwyr/
```

2 Nov 2006 01:27

Executable stacks in ocaml

```Hi,

I am one of the gentoo maintainers of ocaml and we had a couple of QA
reports saying that binaries produced by ocaml had the stack marked as
executable (I understand this is a problem for hardened systems as it
can cause security issues).

Is there a way to tell ocaml to mark the stack as non-executable
or is it part of the compiler design and thus can't be changed?

Thanks,
/Alexandre
--

--
```
```_______________________________________________
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
```
2 Nov 2006 05:35

augmented camlp4 ASTs

```Hello,

Trying to measure the feasibility/cost of doing a couple of things with
camlp4.  I like the camlp4 capability of adding constructions to the
grammar.  However, I sometimes want to do nonlocal transformations on
the contents, and the fact that I always must immediately return an
expression on the right hand side bothers me.  I can call the parsing
part of camlp4 to get an MLast.expr, but the MLast grammar is fixed and
cannot have productions added to it.  One way to get an extensible
grammar would be to project one-to-one into (not onto) a looser AST
type, something like:

type delimiter = char * char

type separator = char

type sexp =
Atom of string
| Series of delimiter * separator * sexp array
| SpecialForm of string * sexp array * sexp array;;

(I haven't handled everything here, like infix operators.)

Then all the quotations of MLast.expr could be rewritten to target this
grammar, and the parser could be copied to write into these
expressions.  When future EXTEND statements add things, the
corresponding entries in the AST could be added.

The downside is obviously that our exhaustiveness checking is defeated.
Always the price one pays for dynamicism.
```

2 Nov 2006 09:43

Re: Executable stacks in ocaml

```> I am one of the gentoo maintainers of ocaml and we had a couple of QA
> reports saying that binaries produced by ocaml had the stack marked as
> executable (I understand this is a problem for hardened systems as it
> can cause security issues).
>
> Is there a way to tell ocaml to mark the stack as non-executable
> or is it part of the compiler design and thus can't be changed?

I wasn't familiar with this "executable stack" business, but a bit of
searching led to this useful page at Gentoo which you might know already:
http://www.gentoo.org/proj/en/hardened/gnu-stack.xml

The brief answer is that no part of OCaml executes code located in the
stack, especially not the assembly code generated by ocamlopt.

The issue, if I understand correctly, is to inform the assembler
and/or linker of this fact.  The page above lists several approaches,
all of which seem to be applicable to OCaml, but some need more
patching than other.  You're welcome to explore the options on your
own and let us (caml <at> inria.fr) know of your conclusions.

- Xavier Leroy

_______________________________________________
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

```

2 Nov 2006 21:58

Re: Functional programming using caml light

```c'est bon j'ai trouvé, ma grammaire ne gère pas l'associativité à gauche  :
sur cet exemple "1 - 3 + 5", je vais l'analyser comme Moins (1, Plus (3,
5)), alors que c'est évidemment Plus (Moins (1, 3), 5)

désolé.

_______________________________________________
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

```
2 Nov 2006 23:44

Printing of types

```When looking at inferred types in the presence of modules and
combinations of abstract and concrete types, the results are often quite
puzzling.  For small pieces of code, it is not a big issue.  When one is
using 4th-order functors (!), with a mixture of abstract and concrete
types, a fair amount of type synonyms, error message become extremely
difficult to interpret!

Below is some (largish for an email) code that demonstrates this.  It
seems difficult to show how puzzling this gets with much smaller code,
although one can indeed reproduce the behaviour with smaller code.
Consider first
module Sig = struct
type domain_is_field
type domain_is_ring
module type DOMAIN = sig
type kind
type v
val z : v
end
module type COLL = sig
module Dom : DOMAIN
type coll
end
end

module Doms = struct
open Sig
module FDomain = struct
type kind = domain_is_field
type v = float
```