[mercury-users] Exchanging 'rules' between OCaml and Mercury

[Guillaume Yziquel]

Le Tuesday 07 Jun 2011 à 11:51:20 (+1000), Paul Bone a écrit :
> On Tue, Jun 07, 2011 at 12:06:00AM +0200, Guillaume Yziquel wrote:
> > 
> > So how would you do you live in harmony with the Mercury GC when
> > building Mercury data structures from foreign code and then invoking
> > Mercury code from foreign code on these data structures? Is there any
> > example of such code lying around on the net?
> 
> If you want to pass the data back and forth you might want to choose a
> particular format and then write code, possibly in both OCaml and Mercury that
> reads and writes this 'canonical' format.

Hmmm. No. I really want one big binary blob and have things purely
functional and immutable. The Dypgen parser generator is also some sort of
purely functional logic-programming DSL, and doing I/O doesn't fit well
with that framework.

I'd rather take time to sort out runtime issues when exchanging data
through the C FFIs than introduce side-effects in that code.

> This first option can be extended.  You could write code that writes data
> structures and readers/writers for either language when given a description of
> the data structure.  To save you some time you could pick the Mercury format
> for the canonical representation and take advantage of io.read and io.write -
> OCaml probably also has an equivalent.  This approach also works very well for
> network communication but might be overkill for your intended purpose.

My intended purpose is to write a compiler in mixed OCaml/Mercury code.
One big binary blob. Mercury code for the type system solver.

(By the way, I see that Mercury is GPL. Does the GPL licence extend to
the generated code? Would my compiler be GPL? More importantly, if my
compiler generates Mercury code, would the generated code be GPL?)

> Alternatively, if you just care about getting the data into Mercury, running
> some query and getting a simple answer out.  Then I'd suggest exporting
> predicates from Mercury that help you construct the data you like and calling
> those from OCaml.

Yes, that's what I'm currently doing. Here's the kind of code I intend
to develop:


	yziquel at seldon:~/$ cat typecheck.m 
	:- module typecheck.

	:- interface.

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

	:- implementation.

	:- pragma foreign_decl("C", "#include <caml/mlvalues.h>").

	:- type term.
	:- pragma foreign_type("C", term, "value").

	:- type typ.
	:- pragma foreign_type("C", typ, "value").

	:- type prop --->
		term_definition(term, term)	;
		term_typed(term, typ)		.

	:- func	define_term(term, term) = prop.
		define_term(Term1, Term2) = term_definition(Term1, Term2).
	:- pragma foreign_export("C", define_term(in, in) = out, "define_term").

	:- func	type_term(term, typ) = prop.
		type_term(Term, Type) = term_typed(Term, Type).
	:- pragma foreign_export("C", type_term(in, in) = out, "type_term").

	:- pred	typecheck(term::in, typ::out, prop::in).
	:- pragma foreign_export("C", typecheck(in, out, in), "typecheck").
		typecheck(Term, Type, Prop) :- Prop = term_typed(Term, Type).



	yziquel at seldon:~$ cat typeCheck_stubs.c 
	#include "typecheck.mh"
	#include <caml/alloc.h>

	CAMLprim value ocaml_define_term (value ml_term1, value ml_term2) {
		/* mlterm1 and ml_term2 are OCaml integers. */
		MR_Word result = define_term(ml_term1, ml_term2);
		return caml_copy_nativeint(result);
	}

	CAMLprim value ocaml_type_term (value ml_term, value ml_typ) {
		/* ml_term and ml_typ are OCaml integers. */
		MR_Word result = type_term(ml_term, ml_typ);
		return caml_copy_nativeint(result);
	}

	CAMLprim value ocaml_typecheck (value ml_term, value ml_prop) {
		/* ml_term is an OCaml integer and ml_prop is an OCaml
		   nativeint. */
		value ml_typ;
		MR_Word prop			= Nativeint_val(ml_prop);
		MR_bool ok			= typecheck(ml_term, &ml_typ, prop);
		value result			= caml_alloc_small(2, 0);
		if (MR_YES == ok) {
			Field(result, 0)	= Val_true;
			Field(result, 1)	= ml_typ;
		} else {
			Field(result, 0)	= Val_false;
			Field(result, 1)	= Val_long(0);
		}
		return result;
	}



I haven't yet worked out the map datastructure in Mercury code, but
essentially, I wish to use functions such as ocaml_define_term() and
ocaml_type_term() to generate propositions and add them to some purely
functional map in Mercury. Then make a call to ocaml_typecheck() to
do some type inference. In fact, lots and lots of calls to
ocaml_typecheck() as type inference is done incrementally during parsing
(I'm designing it so that the only compiler passes are parsing and code
emission).

The issue is that the Mercury values I build live throughout multiple
calls to Mercury code, and I'm wondering if it's legitimate. For now,
this seems to work.

Thanks for your advice.

-- 
     Guillaume Yziquel
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------