Update build system for ml api

src/api/ml/Makefile

@@ -0,0 +1,14 @@
+# to set ARGS, invoke as e.g.:  $ make ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS'
+ARGS=
+
+
+default: z3.ml z3.mli z3_stubs.c
+
+
+%.ml %.mli %_stubs.c: ../%_api.h %.0.idl x3.ml x3V3.ml x3V3.mli \
+	error_handling.idl mlx_get_app_args.idl mlx_get_array_sort.idl mlx_get_datatype_sort.idl mlx_get_domains.idl mlx_get_error_msg.idl mlx_get_pattern_terms.idl mlx_get_tuple_sort.idl mlx_mk_context_x.idl mlx_mk_datatypes.idl mlx_mk_numeral.idl mlx_mk_sort.idl mlx_mk_symbol.idl mlx_model.idl mlx_numeral_refine.idl mlx_parse_smtlib.idl mlx_sort_refine.idl mlx_statistics.idl mlx_symbol_refine.idl mlx_term_refine.idl \
+	generate_mlapi.sh add_error_checking.V3.sed add_error_checking.sed preprocess.sed postprocess.sed reverse.sed
+	./generate_mlapi.sh $(ARGS)
+
+clean:
+	rm -f z3.ml z3.mli z3_stubs.c

src/api/ml/Makefile.build

@@ -0,0 +1,69 @@
+# Makefile to compile OCaml interface to Z3
+#
+# Parameters: ARGS and DEPS environment variables
+# ARGS is passed through to the Makefile that generates the OCaml interface
+# DEPS is a sequence of files that are deleted when the OCaml interface changes
+
+SRC_ML=../../../src/api/ml
+ifeq (${OS}, Windows_NT)
+# the BLD_ML path ends up stored in z3.cm{,x}a, so it must be in windows format
+BLD_ML=$(shell cygpath -m $(CURDIR))
+CFLAGS=-ccopt -wd4090 -ccopt -I$(SRC_ML)/..
+XCDBG=-g $(CFLAGS)
+XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS)
+# ole32 is needed by camlidl (COM support)
+XLIB=-cclib ole32.lib
+AR=lib /nologo /LIBPATH:../../build ../../z3.lib /out:
+O=obj
+A=lib
+else
+BLD_ML=$(CURDIR)
+CFLAGS=-ccopt -Wno-discard-qual -ccopt -Wno-unused-variable -ccopt -I$(SRC_ML)/..
+XCDBG=-g -ccopt -g $(CFLAGS)
+XCOPT=-ccopt -O3 -ccopt -fomit-frame-pointer $(CFLAGS)
+XLIB=
+AR=ar rcs # note trailing space is significant
+O=o
+A=a
+endif
+
+
+all: z3.cma z3.cmxa ocamlz3
+
+
+# keep these files to avoid repeatedly rebuilding them
+.PRECIOUS: $(SRC_ML)/z3.ml $(SRC_ML)/z3.mli $(SRC_ML)/z3_stubs.c z3.ml z3.mli z3_stubs.c z3_theory_stubs.c
+
+# regenerate OCaml API if needed
+$(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c: $(SRC_ML)/Makefile
+	make -C $(SRC_ML) z3.mli z3.ml z3_stubs.c
+
+# copy OCaml API from src to build directories
+%.mli %.ml %_stubs.c %_theory_stubs.c: $(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c Makefile
+	cp $(SRC_ML)/z3.mli $(SRC_ML)/z3.ml $(SRC_ML)/z3_stubs.c $(SRC_ML)/z3_theory_stubs.c .
+
+# OCaml library module for native code clients
+%.cmxa %.cmi lib%stubs.a %.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
+	rm -f $(DEPS)
+	ocamlopt.opt -c $(XCOPT) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
+	$(AR)libz3stubs.$(A) z3.$(O) z3_stubs.$(O) z3_theory_stubs.$(O)
+	ocamlopt.opt -a -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs z3.cmx -o z3.cmxa
+	rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.$(O) z3.cmx
+
+# OCaml library module for byte code clients
+%.cma %.cmi lib%stubs_dbg.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
+	rm -f $(DEPS)
+	ocamlc.opt -c $(XCDBG) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
+	$(AR)libz3stubs_dbg.$(A) z3_stubs.$(O) z3_theory_stubs.$(O)
+	ocamlc.opt -custom -a $(CXDBG) -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs_dbg z3.cmo -o z3.cma
+	rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.cmo
+
+
+# OCaml custom toplevel system pre-linked with Z3
+ocamlz3: z3.cma Makefile
+	ocamlmktop -o ocamlz3 z3.cma -cclib -L.
+
+
+clean: Makefile
+	make -C $(SRC_ML) clean
+	rm -rf Makefile libz3stubs.$(A) libz3stubs_dbg.$(A) ocamlz3 ocamlz3.dSYM z3.$(O) z3.$(A) z3.cma z3.cmi z3.cmo z3.cmx z3.cmxa z3.ml z3.mli z3_stubs.$(O) z3_stubs.c z3_theory_stubs.$(O) z3_theory_stubs.c 

src/api/ml/generate_mlapi.sh

@@ -0,0 +1,53 @@
+#!/bin/bash
+
+# Script to generate the Z3 OCaml API
+#
+# Assumes that environment variables are set to provide access to the following commands: camlidl, gcc, grep, sed
+#
+# This script uses 'gcc -E' as the C preprocessor, other C preprocessors may work but have not been tested.
+#
+# Invoke with "-DUNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
+# Invoke with "-DLEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
+
+
+# add calls to error checking routine
+# convert from doxygen to ocamldoc markup and other syntactic munging
+# ../z3_api.h -> z3V3_api.idl
+sed -f add_error_checking.V3.sed -f preprocess.sed ../z3_api.h > z3V3_api.idl
+
+# z3.idl (z3V3_api.idl x3V3.mli x3V3.ml) -> z3V3_stubs.c, z3V3.mli, z3V3.ml
+gcc -E -w -P -CC -xc -DCAMLIDL -DMLAPIV3 $@ z3.0.idl > z3V3.idl
+camlidl -nocpp z3V3.idl
+
+# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10
+grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$"         z3V3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/renameV3.sed
+grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3V3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g"              >> /tmp/renameV3.sed
+
+# rename.sed to substitute out type equations for enums and options, then postprocess
+cp -f z3V3.mli z3V3.ml /tmp
+sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.mli > z3V3.mli
+sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.ml  > z3V3.ml
+
+# ../z3_api.h -> z3_api.idl
+sed -f add_error_checking.sed -f preprocess.sed ../z3_api.h > z3_api.idl
+
+# z3.idl (z3_api.idl x3.ml) -> z3_stubs.c, z3.mli, z3.ml
+gcc -E -w -P -CC -xc -I. -DCAMLIDL $@ z3.0.idl > z3.idl
+camlidl -nocpp z3.idl
+
+# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10
+grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$"         z3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/rename.sed
+grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g"              >> /tmp/rename.sed
+
+# rename.sed to substitute out type equations for enums and options, then postprocess
+cp z3.mli z3.ml /tmp
+sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.mli > z3.mli
+sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.ml > z3.ml
+
+
+# append Z3.V3 module onto Z3 module
+cat z3V3.mli >> z3.mli
+cat z3V3.ml >> z3.ml
+sed "1,22d" z3V3_stubs.c >> z3_stubs.c
+
+rm -f z3V3_api.idl z3V3.idl z3V3.ml z3V3.mli z3V3_stubs.c z3_api.idl z3.idl

src/api/ml/postprocess.sed

@@ -0,0 +1,8 @@
+# remove 'z3_' and 'Z3_' prefixes on names
+
+s/{\!Z3\./{\!/g
+s/\([^_]\)[zZ]3_/\1/g
+
+# remove cyclic definitions introduced by substituting type equations
+
+s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g

src/api/ml/reverse.sed

@@ -0,0 +1,3 @@
+# output lines of input in reverse order
+
+1!G;h;$!d

src/api/ml/z3.0.idl

@@ -91,11 +91,6 @@ quote(c,"#define xstr(s) str(s)");
 quote(c,"#define str(s) #s");
 
 
-// Suppress "warning C4090: 'function' : different 'const' qualifiers" as
-// CamlIDL does not seem to get this right.
-quote(c,"#pragma warning(disable:4090)");
-
-
 #ifndef MLAPIV3
 
 #define DEFINE_TYPE(T) typedef [abstract] void* T