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) )

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.
Here is your code with some annotations, which gives readable types
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.

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 ?)

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

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:

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/

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
--

-- 
Hi, I'm a .signature virus! Please copy me in your ~/.signature.

_______________________________________________
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

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.

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

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

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