From 1579da02b0e49c079afe95df9fb7b36f32b9dc2a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 11 Dec 2012 15:07:33 +0000 Subject: [PATCH] More new ML API Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 9 ++-- scripts/mk_util.py | 25 +++++++++ scripts/update_api.py | 121 ++++++++++++++++++++++++------------------ 3 files changed, 99 insertions(+), 56 deletions(-) diff --git a/.gitignore b/.gitignore index 9c9707c4b..2ae719b85 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,5 @@ *~ *.pyc -*.pyo -# Ignore callgrind files -callgrind.out.* # .hpp files are automatically generated *.hpp .z3-trace @@ -45,6 +42,7 @@ bld_rel_x64/* # Auto generated files. config.log config.status +configure install_tactic.cpp mem_initializer.cpp gparams_register_modules.cpp @@ -56,8 +54,6 @@ src/api/api_log_macros.cpp src/api/dll/api_dll.def src/api/dotnet/Enumerations.cs src/api/dotnet/Native.cs -src/api/dotnet/Properties/AssemblyInfo.cs -src/api/dotnet/Microsoft.Z3.xml src/api/python/z3consts.py src/api/python/z3core.py src/ast/pattern/database.h @@ -78,3 +74,6 @@ src/api/ml/z3native_stubs.c src/api/ml/z3native.ml src/api/ml/z3enums.ml src/api/ml/z3.mllib +src/api/ml/z3_native.c +src/api/ml/z3_native.ml +src/api/ml/z3_enums.ml diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 7a054256d..d019e24e9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2431,6 +2431,8 @@ def mk_bindings(api_files): mk_z3consts_ml(api_files) _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK cp_z3py_to_build() + if is_ml_enabled(): + mk_z3consts_ml(api_files) # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): @@ -2718,6 +2720,7 @@ def mk_z3consts_ml(api_files): if not os.path.exists(gendir): os.mkdir(gendir) +<<<<<<< HEAD efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') efile.write('(* Automatically generated file *)\n\n') efile.write('(** The enumeration types of Z3. *)\n\n') @@ -2799,6 +2802,13 @@ def mk_z3consts_ml(api_files): efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') efile.write('(* Automatically generated file *)\n\n') efile.write('(** The enumeration types of Z3. *)\n\n') +======= + efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w') + efile.write('(* Automatically generated file *)\n\n') + # efile.write('module z3_enums = struct\n\n'); + + +>>>>>>> More new 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) @@ -2844,6 +2854,7 @@ def mk_z3consts_ml(api_files): if m: name = words[1] if name not in DeprecatedEnums: +<<<<<<< HEAD efile.write('(** %s *)\n' % name[3:]) efile.write('type %s =\n' % name[3:]) # strip Z3_ for k, i in decls.iteritems(): @@ -2854,6 +2865,13 @@ def mk_z3consts_ml(api_files): efile.write('(** Convert int to %s*)\n' % name[3:]) efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_ efile.write('\n') +======= + 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_ +>>>>>>> More new ML API mode = SEARCHING else: if words[2] != '': @@ -2864,8 +2882,15 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 +<<<<<<< HEAD if VERBOSE: print "Generated '%s/z3enums.mli'" % ('%s' % gendir) +======= + efile.write('\n') + # efile.write'end\n'); + if VERBOSE: + print "Generated '%s/z3_enums.ml'" % ('%s' % gendir) +>>>>>>> More new 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 945496781..c1bb22a44 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 : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', - STRING : 'string', STRING_PTR : 'char**', - BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } +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' } next_type_id = FIRST_OBJ_ID @@ -1069,9 +1069,7 @@ def mk_bindings(): exe_c.write("}\n") def ml_method_name(name): - result = '' - name = name[3:] # Remove Z3_ - return result + return name[3:] # Remove Z3_ def mk_ml(): if not is_ml_enabled(): @@ -1080,10 +1078,57 @@ def mk_ml(): ml_nativef = os.path.join(ml_dir, 'z3_native.ml') ml_wrapperf = os.path.join(ml_dir, 'z3_native.c') ml_native = open(ml_nativef, 'w') - ml_native.write('// Automatically generated file\n') + ml_native.write('(* Automatically generated file *)\n') ml_native.write('\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') + ml_native.write('and sort = private ast\n') + ml_native.write('and func_decl = private ast\n') + ml_native.write('and app = private ast\n') + ml_native.write('and pattern = private ast\n') + ml_native.write('and params\n') + ml_native.write('and param_descrs\n') + ml_native.write('and model\n') + ml_native.write('and func_interp\n') + ml_native.write('and func_entry\n') + ml_native.write('and fixedpoint\n') + ml_native.write('and ast_vector\n') + ml_native.write('and ast_map\n') + ml_native.write('and goal\n') + ml_native.write('and tactic\n') + ml_native.write('and probe\n') + ml_native.write('and apply_result\n') + 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') for name, result, params in _dotnet_decls: - ml_native.write(' external %s : (' % ml_method_name(name)) + ml_native.write(' external native_%s : ' % ml_method_name(name)) + i = 0; + for param in params: + ml_native.write('%s -> ' % param2ml(param)) + i = i + 1 + ml_native.write('%s\n' % (type2ml(result))) + ml_native.write(' = "Native_Z3_%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)) + 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(' = \n') + 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: @@ -1091,50 +1136,24 @@ def mk_ml(): first = False else: ml_native.write(', ') - ml_native.write('%s a%d' % (param2ml(param), i)) + ml_native.write('a%d' % i) i = i + 1 - ml_native.write('%s)\n' % (type2ml(result))) - # ml_native.write(' = "NATIVE_%s"' % ml_method_name(name)) - # ml_native.write('\n\n') - # # Exception wrappers - # for name, result, params in _dotnet_decls: - # java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) - # first = True - # i = 0; - # for param in params: - # if first: - # first = False - # else: - # java_native.write(', ') - # java_native.write('%s a%d' % (param2java(param), i)) - # i = i + 1 - # java_native.write(')') - # if len(params) > 0 and param_type(params[0]) == CONTEXT: - # java_native.write(' throws Z3Exception') - # java_native.write('\n') - # java_native.write(' {\n') - # java_native.write(' ') - # if result != VOID: - # java_native.write('%s res = ' % type2java(result)) - # java_native.write('INTERNAL%s(' % (java_method_name(name))) - # first = True - # i = 0; - # for param in params: - # if first: - # first = False - # else: - # java_native.write(', ') - # java_native.write('a%d' % i) - # i = i + 1 - # java_native.write(');\n') - # if len(params) > 0 and param_type(params[0]) == CONTEXT: - # java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') - # java_native.write(' if (err != Z3_error_code.Z3_OK)\n') - # java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') - # if result != VOID: - # java_native.write(' return res;\n') - # java_native.write(' }\n\n') - # java_native.write('}\n') + 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(' else\n') + if result == VOID: + ml_native.write(' ()\n') + else: + ml_native.write(' res\n') + ml_native.write('\n') + ml_native.write('\nend\n') ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper.write('// Automatically generated file\n\n') ml_wrapper.write('#include \n')