diff --git a/.gitignore b/.gitignore index f2a31c21e..95c44e557 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ callgrind.out.* # OCaml generated files *.a *.cma +*.cmo *.cmi *.cmxa ocamlz3 @@ -71,5 +72,5 @@ doc/code 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_enums.ml +src/api/ml/z3.ml +src/api/ml/enumerations.ml diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4249a04b0..31e64b10e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -672,6 +672,9 @@ def get_cs_files(path): def get_java_files(path): return filter(lambda f: f.endswith('.java'), os.listdir(path)) +def get_ml_files(path): + return filter(lambda f: f.endswith('.ml'), os.listdir(path)) + def find_all_deps(name, deps): new_deps = [] for dep in deps: @@ -1284,9 +1287,17 @@ class MLComponent(Component): def mk_makefile(self, out): if is_ml_enabled(): - 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) @@ -2522,11 +2533,9 @@ def mk_z3consts_ml(api_files): if not os.path.exists(gendir): os.mkdir(gendir) - efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w') + efile = open('%s.ml' % os.path.join(gendir, "enumerations"), 'w') efile.write('(* Automatically generated file *)\n\n') - # efile.write('module z3_enums = struct\n\n'); - - + efile.write('module Enumerations = struct\n') 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) @@ -2572,11 +2581,21 @@ def mk_z3consts_ml(api_files): if m: name = words[1] if name not in DeprecatedEnums: - efile.write('\n(* %s *)\n' % name) efile.write('type %s =\n' % name[3:]) # strip Z3_ - efile.write for k, i in decls.iteritems(): - efile.write(' | %s \n' % k[3:]) # strip Z3_ + 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') mode = SEARCHING else: if words[2] != '': @@ -2587,10 +2606,9 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 - efile.write('\n') - # efile.write'end\n'); + efile.write('end\n') if VERBOSE: - print "Generated '%s/z3_enums.ml'" % ('%s' % gendir) + print "Generated '%s/enumerations.ml'" % ('%s' % gendir) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index 9acdf1040..b8295405e 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -156,9 +156,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', - STRING : 'string', STRING_PTR : 'char**', - BOOL : 'lbool', SYMBOL : 'symbol', PRINT_MODE : 'ast_print_mode', ERROR_CODE : 'error_code' } +Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', + STRING : 'string', STRING_PTR : 'char**', + BOOL : 'int', SYMBOL : 'symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } next_type_id = FIRST_OBJ_ID @@ -212,7 +212,7 @@ def type2javaw(ty): def type2ml(ty): global Type2ML if (ty >= FIRST_OBJ_ID): - return 'long' + return 'int' else: return Type2ML[ty] @@ -328,9 +328,9 @@ def param2ml(p): k = param_kind(p) if k == OUT: if param_type(p) == INT or param_type(p) == UINT: - return "int*" + return "int" elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: - return "long*" + return "int" elif param_type(p) == STRING: return "string" else: @@ -1075,12 +1075,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('\n') - ml_native.write('module Z3Native = struct\n\n') + ml_native.write('(* Automatically generated file *)\n\n') + ml_native.write('open Enumerations\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 +1103,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 +1130,28 @@ def mk_ml(): ml_native.write(' ') if result != VOID: ml_native.write('let res = ') - ml_native.write('n_%s(' % (ml_method_name(name))) - first = True - i = 0; - for param in params: - if first: - first = False - else: - ml_native.write(', ') - ml_native.write('a%d' % i) - i = i + 1 - ml_native.write(')') + if len(params) == 0: + ml_native.write('n_%s()' % (ml_method_name(name))) + else: + ml_native.write('(n_%s ' % (ml_method_name(name))) + first = True + i = 0; + for param in params: + if first: + first = False + else: + 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(' if err <> Z3_enums.OK then\n') - ml_native.write(' raise (z3_exception n_get_error_msg_ex(a0, err.toInt()))\n') + ml_native.write(' let err = (Enumerations.int2error_code (n_get_error_code a0)) in \n') + ml_native.write(' if err <> Enumerations.OK then\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')