--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 16:56:22 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 17:48:07 2010 +0100
@@ -319,6 +319,8 @@
int_expr_func: int_expr -> 'a -> 'a
}
+(** Auxiliary functions on ML representation of Kodkod problems **)
+
(* 'a fold_expr_funcs -> formula -> 'a -> 'a *)
fun fold_formula (F : 'a fold_expr_funcs) formula =
case formula of
@@ -512,18 +514,7 @@
filter (is_relevant_setting o fst) (#settings p1)
= filter (is_relevant_setting o fst) (#settings p2)
-val created_temp_dir = Unsynchronized.ref false
-
-(* bool -> string * string *)
-fun serial_string_and_temporary_dir_for_overlord overlord =
- if overlord then
- ("", getenv "ISABELLE_HOME_USER")
- else
- let
- val dir = getenv "ISABELLE_TMP"
- val _ = if !created_temp_dir then ()
- else (created_temp_dir := true; File.mkdir (Path.explode dir))
- in (serial_string (), dir) end
+(** Serialization of problem **)
(* int -> string *)
fun base_name j =
@@ -901,6 +892,8 @@
map out_problem problems
end
+(** Parsing of solution **)
+
(* string -> bool *)
fun is_ident_char s =
Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
@@ -1016,6 +1009,21 @@
is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250
+(** Main Kodkod entry point **)
+
+val created_temp_dir = Unsynchronized.ref false
+
+(* bool -> string * string *)
+fun serial_string_and_temporary_dir_for_overlord overlord =
+ if overlord then
+ ("", getenv "ISABELLE_HOME_USER")
+ else
+ let
+ val dir = getenv "ISABELLE_TMP"
+ val _ = if !created_temp_dir then ()
+ else (created_temp_dir := true; File.mkdir (Path.explode dir))
+ in (serial_string (), dir) end
+
(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let