diff --git a/gmlmip.ml b/gmlmip.ml new file mode 100644 index 0000000000000000000000000000000000000000..3243083b607c7487980beb5fc42b6964064db847 --- /dev/null +++ b/gmlmip.ml @@ -0,0 +1,7 @@ + + +(* transforms list of gml formulas (diamond?,number,formula) + to list of consequences (positive?,formula), + here positive? means that the formula must be true in order to make the + given conjunct of modalities true *) +external gml_rules : (bool*int*int) list -> (int*bool) list list = "gmlRules_stub" diff --git a/gmlmip.mli b/gmlmip.mli new file mode 100644 index 0000000000000000000000000000000000000000..dca49b624d8b282335e9ae5e88a0f9e1887dbadc --- /dev/null +++ b/gmlmip.mli @@ -0,0 +1,5 @@ +(* transforms list of gml formulas (diamond?,number,formula) + to list of consequences (positive?,formula), + here positive? means that the formula must be true in order to make the + given conjunct of modalities true *) +val gml_rules : (bool*int*int) list -> (int*bool) list list diff --git a/gmlmip_stub.cc b/gmlmip_stub.cc new file mode 100644 index 0000000000000000000000000000000000000000..54ef0972c30f9bd74d390391547458fdf6458df7 --- /dev/null +++ b/gmlmip_stub.cc @@ -0,0 +1,76 @@ +#define __STDC_LIMIT_MACROS +#define __STDC_FORMAT_MACROS + +#include <utility> // for pair +#include <vector> + +extern "C" { + #include <caml/mlvalues.h> + #include <caml/alloc.h> + #include <caml/memory.h> + #include <caml/custom.h> +} + +#include "GMLMIP-0.1/onestep.h" + +// +using namespace std; + +extern "C" { + CAMLprim value gmlRules_stub(value modalities); +} + +template<class T> +value vector2CamlList(const vector<T>& vec, value (*f)(const T&)) { + CAMLlocal2( cli, cons ); + cli = Val_emptylist; + + for (int i = vec.size() - 1; i >= 0; i--) { + cons = caml_alloc(2, 0); + + Store_field( cons, 0, f(vec[i]) ); // head + Store_field( cons, 1, cli ); // tail + + cli = cons; + } + + return cli ; +} + + + +static CAMLprim value pair2caml(const pair<int,bool>& t) { + CAMLlocal1( abc ); + abc = caml_alloc(2, 0); + Store_field( abc, 0, Val_int(t.first)); + Store_field( abc, 1, Val_bool(t.second)); + return abc; +} + +static CAMLprim value vector2caml(const vector<pair<int,bool> >& vt) { + return vector2CamlList(vt, pair2caml); +} + +CAMLprim value gmlRules_stub(value modalities) { + // parse caml-modalities to a C++ vector + CAMLparam1( modalities ); + value block = modalities; + vector<pair<pair<bool,int>,int> > modvec; + while (Is_block(block)) { + CAMLlocal3( vpos, vcnt, vformula ); + vpos = Field(Field(block, 0), 0); + vcnt = Field(Field(block, 0), 1); + vformula = Field(Field(block, 0), 2); + modvec.push_back(make_pair(make_pair( + Bool_val(vpos), + Int_val(vcnt)), + Int_val(vformula))); + } + // Do one rule step and save result in rulevec + GMLConclusion rulevec = gmlmip_onestep_gml(modvec); + // convert rulevec into ocaml list of pairs + CAMLlocal1( res ); + res = vector2CamlList(rulevec, vector2caml); + CAMLreturn( res ); +} +