More ML API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

.gitignore

@@ -78,5 +78,5 @@ src/api/ml/z3.mllib
 src/api/ml/z3_native.c
 src/api/ml/z3_native.ml
 src/api/ml/native.c
-src/api/ml/Z3.ml
+src/api/ml/z3.ml
-src/api/ml/z3_enums.ml
+src/api/ml/enumerations.ml

scripts/mk_util.py

@@ -1428,9 +1428,17 @@ class MLComponent(Component):
                 if IS_WINDOWS:
                     out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
                 out.write('\n\n')
-            mk_dir(os.path.join(BUILD_DIR, 'api', 'ml'))
+            bld_dir = os.path.join(BUILD_DIR, 'api', 'ml')
+            mk_dir(bld_dir)
             libfile = '%s$(LIB_EXT)' % self.lib_name
-            out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
+            for mlfile in get_ml_files(self.src_dir):
+                out.write('%si: %s\n' % (os.path.join('api', 'ml', mlfile),os.path.join(self.to_src_dir, mlfile)))
+                out.write('\tocamlopt -I %s -i %s > %si\n' % (os.path.join('api', 'ml'), os.path.join(self.to_src_dir, mlfile), os.path.join('api', 'ml', mlfile)))
+                out.write('\tocamlopt -I %s -c %si \n' % (os.path.join('api', 'ml'), os.path.join('api','ml', mlfile)))
+            out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
+            for mlfile in get_ml_files(self.src_dir):
+                out.write(' %si' % os.path.join('api','ml', mlfile))
+            out.write('\n')
             out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) -I%s %s/native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
             out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %  os.path.join('api', 'ml', 'native'))
             out.write('ml: %s\n' % libfile)
@@ -2720,6 +2728,7 @@ def mk_z3consts_ml(api_files):
     if not os.path.exists(gendir):
         os.mkdir(gendir)
 
+<<<<<<< HEAD
 <<<<<<< HEAD
     efile  = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
     efile.write('(* Automatically generated file *)\n\n')
@@ -2809,6 +2818,11 @@ def mk_z3consts_ml(api_files):
 
 
 >>>>>>> More new ML API
+=======
+    efile  = open('%s.ml' % os.path.join(gendir, "enumerations"), 'w')
+    efile.write('(* Automatically generated file *)\n\n')
+    efile.write('module Enumerations = struct\n')
+>>>>>>> More ML API
     for api_file in api_files:
         api_file_c = ml.find_file(api_file, ml.name)
         api_file   = os.path.join(api_file_c.src_dir, api_file)
@@ -2854,6 +2868,7 @@ def mk_z3consts_ml(api_files):
                 if m:
                     name = words[1]
                     if name not in DeprecatedEnums:
+<<<<<<< HEAD
 <<<<<<< HEAD
                         efile.write('(** %s *)\n' % name[3:])
                         efile.write('type %s =\n' % name[3:]) # strip Z3_
@@ -2867,11 +2882,28 @@ def mk_z3consts_ml(api_files):
                         efile.write('\n')
 =======
                         efile.write('\n(* %s *)\n' % name)
+=======
+>>>>>>> More ML API
                         efile.write('type %s =\n' % name[3:]) # strip Z3_
-                        efile.write
                         for k, i in decls.iteritems():
+<<<<<<< HEAD
                             efile.write('    | %s \n' % k[3:]) # strip Z3_
 >>>>>>> More new ML API
+=======
+                            efile.write('  | %s \n' % k[3:]) # strip Z3_
+                        efile.write('\n')
+                        efile.write('let %s2int x : int =\n' % (name[3:])) # strip Z3_
+                        efile.write('  match x with\n')
+                        for k, i in decls.iteritems():
+                            efile.write('  | %s -> %d\n' % (k[3:], i))
+                        efile.write('\n')
+                        efile.write('let int2%s x : %s =\n' % (name[3:],name[3:])) # strip Z3_
+                        efile.write('  match x with\n')
+                        for k, i in decls.iteritems():
+                            efile.write('  | %d -> %s\n' % (i, k[3:]))
+                        # use Z3.Exception?
+                        efile.write('  | _ -> raise (Failure "undefined enum value")\n\n')
+>>>>>>> More ML API
                     mode = SEARCHING
                 else:
                     if words[2] != '':
@@ -2882,6 +2914,7 @@ def mk_z3consts_ml(api_files):
                     decls[words[1]] = idx
                     idx = idx + 1
             linenum = linenum + 1
+<<<<<<< HEAD
 <<<<<<< HEAD
     if VERBOSE:
         print "Generated '%s/z3enums.mli'" % ('%s' % gendir)
@@ -2891,6 +2924,11 @@ def mk_z3consts_ml(api_files):
     if VERBOSE:
         print "Generated '%s/z3_enums.ml'" % ('%s' % gendir)
 >>>>>>> More new ML API
+=======
+    efile.write('end\n')
+    if VERBOSE:
+        print "Generated '%s/enumerations.ml'" % ('%s' % gendir)
+>>>>>>> More ML API
 
 def mk_gui_str(id):
     return '4D2F40D8-E5F9-473B-B548-%012d' % id

scripts/update_api.py

@@ -157,9 +157,9 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
                BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
 
 # Mapping to ML types
-Type2ML = { VOID : 'unit', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
+Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
-              STRING : 'string', STRING_PTR : 'char**', 
+            STRING : 'string', STRING_PTR : 'char**', 
-              BOOL : 'lbool', SYMBOL : 'symbol', PRINT_MODE : 'ast_print_mode', ERROR_CODE : 'error_code' }
+            BOOL : 'int', SYMBOL : 'symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
 
 next_type_id = FIRST_OBJ_ID
 
@@ -214,7 +214,7 @@ def type2javaw(ty):
 def type2ml(ty):
     global Type2ML
     if (ty >= FIRST_OBJ_ID):
-        return 'long'
+        return 'int'
     else:
         return Type2ML[ty]
 
@@ -331,6 +331,8 @@ def param2ml(p):
     if k == OUT:
         if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
             return "int"
+        elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
+            return "int"
         elif param_type(p) == STRING:
             return "string"
         else:
@@ -1075,12 +1077,12 @@ def mk_ml():
     if not is_ml_enabled():
         return
     ml_dir      = get_component('ml').src_dir
-    ml_nativef  = os.path.join(ml_dir, 'Z3.ml')
+    ml_nativef  = os.path.join(ml_dir, 'z3.ml')
     ml_wrapperf = os.path.join(ml_dir, 'native.c')
     ml_native   = open(ml_nativef, 'w')
-    ml_native.write('(* Automatically generated file *)\n')
+    ml_native.write('(* Automatically generated file *)\n\n')
-    ml_native.write('\n')
+    ml_native.write('open Enumerations\n\n')
-    ml_native.write('module Z3Native = struct\n\n')
+    ml_native.write('module Z3 = struct\n\n')
     ml_native.write('type context\n')
     ml_native.write('and symbol\n')
     ml_native.write('and ast\n')
@@ -1103,15 +1105,17 @@ def mk_ml():
     ml_native.write('and solver\n')
     ml_native.write('and stats\n')
     ml_native.write('\n')
-    ml_native.write('  exception Z3Exception of string\n\n')
+    ml_native.write('  exception Exception of string\n\n')
     for name, result, params in _dotnet_decls:
-        ml_native.write('  external native_%s : ' % ml_method_name(name))
+        ml_native.write('  external n_%s : ' % ml_method_name(name))
         i = 0;
         for param in params:
             ml_native.write('%s -> ' % param2ml(param))
             i = i + 1
+        if len(params) == 0:
+            ml_native.write(' unit -> ')
         ml_native.write('%s\n' % (type2ml(result)))
-        ml_native.write('    = "Native_Z3_%s"\n\n' % ml_method_name(name))
+        ml_native.write('    = "n_%s"\n\n' % ml_method_name(name))
     # Exception wrappers
     for name, result, params in _dotnet_decls:
         ml_native.write(' let %s ' % ml_method_name(name))
@@ -1128,25 +1132,28 @@ def mk_ml():
         ml_native.write('    ')
         if result != VOID:
             ml_native.write('let res = ')
-        ml_native.write('n_%s(' % (ml_method_name(name)))
+        if len(params) == 0:
-        first = True
+            ml_native.write('n_%s()' % (ml_method_name(name)))
-        i = 0;
+        else:
-        for param in params:
+            ml_native.write('(n_%s ' % (ml_method_name(name)))
-            if first:
+            first = True
-                first = False
+            i = 0;
-            else:
+            for param in params:
-                ml_native.write(', ')
+                if first:
-            ml_native.write('a%d' % i)
+                    first = False
-            i = i + 1
+                else:
-        ml_native.write(')')
+                    ml_native.write(' ')
+                ml_native.write('a%d' % i)
+                i = i + 1
+            ml_native.write(')')
         if result != VOID:
             ml_native.write(' in\n')
         else:
             ml_native.write(';\n')
         if len(params) > 0 and param_type(params[0]) == CONTEXT:
-            ml_native.write('    let err = error_code.fromInt(n_get_error_code(a0)) in \n')
+            ml_native.write('    let err = (Enumerations.int2error_code (n_get_error_code a0)) in \n')
-            ml_native.write('      if err <> Z3_enums.OK then\n')
+            ml_native.write('      if err <> Enumerations.OK then\n')
-            ml_native.write('        raise (z3_exception n_get_error_msg_ex(a0, err.toInt()))\n')
+            ml_native.write('        raise (Exception (n_get_error_msg_ex a0 (error_code2int err)))\n')
             ml_native.write('      else\n')
         if result == VOID:
             ml_native.write('        ()\n')