Add gmlmip files

gmlmip.ml

+
+
+(* 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"

gmlmip.mli

+(* 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

gmlmip_stub.cc

+#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 );
+}
+