Software

Clay Compiler

The Clay compiler has been implemented in Haskell, the file clayc-0.1.1.tar.gz contains the source distribution created with cabal

Clay Library

The Clay library contains several examples of source and generated code I used in my thesis and in some papers. The file 2011iclp-herranz-clay-lib.tgz contains the library.

To use the compiler you just need to define the environment variable CLAYPATH with the directory with the library. Then run the clay compiler with the option -f to generate first order logic and -p to generate Prolog. Let me show a brief example:

$ clay -p clay.lang.Nat
class(clay_lang_Num).

class(clay_lang_MetaNum).

nf(clay_lang_MetaNum, clay_lang_Num).

nf(clay_lang_Meta, clay_lang_MetaNum).

inherits(clay_lang_Num, []).

cases(clay_lang_Num, []).

class(clay_lang_Bool).

class(clay_lang_MetaBool).

nf(clay_lang_MetaBool, clay_lang_Bool).

nf(clay_lang_Meta, clay_lang_MetaBool).

inherits(clay_lang_Bool, []).

cases(clay_lang_Bool, [clay_lang_True, clay_lang_False]).

fields(clay_lang_False, []).

msgtype(clay_lang_MetaBool, mkFalse).

pre(clay_lang_MetaBool, _self, mkFalse, []) :-
   instanceof(_self, clay_lang_MetaBool).

post(clay_lang_MetaBool, _self, mkFalse, [], _result) :-
   instanceof(_result, clay_lang_False),
   project(_result, clay_lang_False, []).

fields(clay_lang_True, []).

msgtype(clay_lang_MetaBool, mkTrue).

pre(clay_lang_MetaBool, _self, mkTrue, []) :-
   instanceof(_self, clay_lang_MetaBool).

post(clay_lang_MetaBool, _self, mkTrue, [], _result) :-
   instanceof(_result, clay_lang_True),
   project(_result, clay_lang_True, []).

msgtype(clay_lang_Bool, and).

pre(clay_lang_Bool, _self, and, [_b]) :-
   instanceof(_self, clay_lang_Bool),
   instanceof(_b, clay_lang_Bool).

post(clay_lang_Bool, _self, and, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_True),
   \+ instanceof(_self, clay_lang_False).

post(clay_lang_Bool, _self, and, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_True),
   instanceof(_result, clay_lang_False).

post(clay_lang_Bool, _self, and, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   eq(clay_lang_Bool, _result, _b),
   \+ instanceof(_self, clay_lang_False).

post(clay_lang_Bool, _self, and, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   eq(clay_lang_Bool, _result, _b),
   instanceof(_result, clay_lang_False).

post(clay_lang_Bool, _self, or, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_False),
   \+ instanceof(_self, clay_lang_True).

post(clay_lang_Bool, _self, or, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_False),
   instanceof(_result, clay_lang_True).

post(clay_lang_Bool, _self, or, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   eq(clay_lang_Bool, _result, _b),
   \+ instanceof(_self, clay_lang_True).

post(clay_lang_Bool, _self, or, [_b], _result) :-
   instanceof(_result, clay_lang_Bool),
   eq(clay_lang_Bool, _result, _b),
   instanceof(_result, clay_lang_True).

pre(clay_lang_Bool, _self, or, [_b]) :-
   instanceof(_self, clay_lang_Bool),
   instanceof(_b, clay_lang_Bool).

msgtype(clay_lang_Bool, or).

post(clay_lang_Bool, _self, neg, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_True),
   \+ instanceof(_self, clay_lang_False).

post(clay_lang_Bool, _self, neg, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ instanceof(_self, clay_lang_True),
   instanceof(_result, clay_lang_True).

post(clay_lang_Bool, _self, neg, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   instanceof(_result, clay_lang_False),
   \+ instanceof(_self, clay_lang_False).

post(clay_lang_Bool, _self, neg, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   instanceof(_result, clay_lang_False),
   instanceof(_result, clay_lang_True).

pre(clay_lang_Bool, _self, neg, []) :-
   instanceof(_self, clay_lang_Bool).

msgtype(clay_lang_Bool, neg).

class(clay_lang_Nat).

class(clay_lang_MetaNat).

nf(clay_lang_MetaNat, clay_lang_Nat).

nf(clay_lang_Meta, clay_lang_MetaNat).

inherits(clay_lang_Nat, [clay_lang_Num]).

cases(clay_lang_Nat, [clay_lang_Zero, clay_lang_Succ]).

fields(clay_lang_Succ, [(pred, clay_lang_Nat)]).

msgtype(clay_lang_MetaNat, mkSucc).

pre(clay_lang_MetaNat, _self, mkSucc, [_pred]) :-
   instanceof(_self, clay_lang_MetaNat),
   instanceof(_pred, clay_lang_Nat).

post(clay_lang_MetaNat, _self, mkSucc, [_pred], _result) :-
   instanceof(_result, clay_lang_Succ),
   project(_result, clay_lang_Succ, [(pred, _pred)]).

post(clay_lang_Nat, _self, pred, [], _result) :-
   instanceof(_result, clay_lang_Nat),
   project(_self, clay_lang_Succ, [(pred, _result)]).

pre(clay_lang_Nat, _self, pred, []) :-
   instanceof(_self, clay_lang_Succ).

msgtype(clay_lang_Nat, pred).

fields(clay_lang_Zero, []).

msgtype(clay_lang_MetaNat, mkZero).

pre(clay_lang_MetaNat, _self, mkZero, []) :-
   instanceof(_self, clay_lang_MetaNat).

post(clay_lang_MetaNat, _self, mkZero, [], _result) :-
   instanceof(_result, clay_lang_Zero),
   project(_result, clay_lang_Zero, []).

msgtype(clay_lang_Nat, even).

pre(clay_lang_Nat, _self, even, []) :-
   instanceof(_self, clay_lang_Nat).

post(clay_lang_Nat, _self, even, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   post_clay_lang_Nat__self_even___result_V(_result),
   post_clay_lang_Nat__self_even___result_W(_NF__n_add, _self).

post(clay_lang_Nat, _self, even, [], _result) :-
   instanceof(_result, clay_lang_Bool),
   \+ post_clay_lang_Nat__self_even___result_V(_result),
   \+ post_clay_lang_Nat__self_even___result_W(_NF__n_add, _self).

:- discontiguous post_clay_lang_Nat__self_even___result_V/1.

post_clay_lang_Nat__self_even___result_V(_result) :-
   instanceof(_result, clay_lang_True).

:- discontiguous post_clay_lang_Nat__self_even___result_W/2.

post_clay_lang_Nat__self_even___result_W(_NF__n_add, _self) :-
   instanceof(_n, clay_lang_Nat),
   reduce(_n<--add(_n), _NF__n_add),
   eq(clay_lang_Nat, _self, _NF__n_add).

sol(clay_lang_Nat, _self, even, [], _result) :-
   instanceof(_self, clay_lang_Zero),
   instanceof(_result, clay_lang_True).

sol(clay_lang_Nat, _self, even, [], _result) :-
   instanceof(_p, clay_lang_Nat),
   reduce(clay_lang_Nat<--mkSucc(_p), _NF_clay_lang_Nat_mkSucc),
   eq(clay_lang_Nat, _self, _NF_clay_lang_Nat_mkSucc),
   reduce(_p<--even<--neg, _NF_send_neg),
   eq(clay_lang_Bool, _result, _NF_send_neg).

post(clay_lang_Nat, _self, half, [], _result) :-
   instanceof(_result, clay_lang_Nat),
   reduce(_result<--add(_result), _NF__result_add),
   eq(clay_lang_Nat, _self, _NF__result_add).

pre(clay_lang_Nat, _self, half, []) :-
   instanceof(_self, clay_lang_Nat),
   reduce(_self<--even, _NF__self_even),
   reduce(clay_lang_Bool<--mkTrue, _NF_clay_lang_Bool_mkTrue),
   eq(_, _NF__self_even, _NF_clay_lang_Bool_mkTrue).

msgtype(clay_lang_Nat, half).

post(clay_lang_Nat, _self, add, [_n], _result) :-
   instanceof(_result, clay_lang_Nat),
   \+ instanceof(_self, clay_lang_Zero),
   \+ instanceof(_self, clay_lang_Succ).

post(clay_lang_Nat, _self, add, [_n], _result) :-
   instanceof(_result, clay_lang_Nat),
   \+ instanceof(_self, clay_lang_Zero),
   reduce(clay_lang_Nat<--mkSucc(_self<--pred<--add(_n)), _NF_clay_lang_Nat_mkSucc),
   eq(clay_lang_Nat, _result, _NF_clay_lang_Nat_mkSucc).

post(clay_lang_Nat, _self, add, [_n], _result) :-
   instanceof(_result, clay_lang_Nat),
   eq(clay_lang_Nat, _result, _n),
   \+ instanceof(_self, clay_lang_Succ).

post(clay_lang_Nat, _self, add, [_n], _result) :-
   instanceof(_result, clay_lang_Nat),
   eq(clay_lang_Nat, _result, _n),
   reduce(clay_lang_Nat<--mkSucc(_self<--pred<--add(_n)), _NF_clay_lang_Nat_mkSucc),
   eq(clay_lang_Nat, _result, _NF_clay_lang_Nat_mkSucc).

pre(clay_lang_Nat, _self, add, [_n]) :-
   instanceof(_self, clay_lang_Nat),
   instanceof(_n, clay_lang_Nat).

msgtype(clay_lang_Nat, add).