From dcd6f1f69736ace570ead5e544b670dfa0a1b42c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 11 Dec 2012 21:39:52 +0000 Subject: [PATCH] More ML API Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 4 +-- scripts/mk_util.py | 44 ++++++++++++++++++++++++++++++--- scripts/update_api.py | 57 ++++++++++++++++++++++++------------------- 3 files changed, 75 insertions(+), 30 deletions(-) diff --git a/.gitignore b/.gitignore index a3fa5e919..a1a8b7f6b 100644 --- a/.gitignore +++ b/.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_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 d324e5206..bd6495d1b 100644 --- a/scripts/mk_util.py +++ b/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 diff --git a/scripts/update_api.py b/scripts/update_api.py index 72fd32702..971e6eab1 100644 --- a/scripts/update_api.py +++ b/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', - 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 @@ -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('\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 +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))) - 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')