src/HOL/Tools/Nunchaku/nunchaku_commands.ML

--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:25 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:30 2017 +0200
@@ -25,7 +25,8 @@
    ("bound_increment", "2"),
    ("debug", "false"),
    ("falsify", "true"),
-   ("initial_bound", "2"),
+   ("min_bound", "2"),
+   ("max_bound", "none"),
    ("max_genuine", "1"),
    ("max_potential", "1"),
    ("overlord", "false"),
@@ -164,6 +165,7 @@
       #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type;
     val read_term_polymorphic =
       Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt);
+
     val lookup_term_list_option_polymorphic =
       AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic);
 
@@ -172,6 +174,11 @@
         Const x => x
       | t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t));
 
+    fun lookup_none_option lookup' name =
+      (case lookup name of
+        SOME "none" => NONE
+      | _ => SOME (lookup' name))
+
     val solvers = lookup_strings "solvers";
     val falsify = lookup_bool "falsify";
     val assms = lookup_bool "assms";
@@ -180,7 +187,8 @@
     val expect = lookup_string "expect";
 
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf";
-    val initial_bound = lookup_int "initial_bound";
+    val min_bound = lookup_int "min_bound";
+    val max_bound = lookup_none_option lookup_int "max_bound";
     val bound_increment = lookup_int "bound_increment";
     val whacks = lookup_bool_assigns read_term_polymorphic "whack";
     val cards = lookup_int_range_assigns read_type_polymorphic "card";
@@ -204,8 +212,8 @@
        expect = expect};
 
     val scope_of_search_params =
-      {wfs = wfs, whacks = whacks, initial_bound = initial_bound, bound_increment = bound_increment,
-       cards = cards, monos = monos};
+      {wfs = wfs, whacks = whacks, min_bound = min_bound, max_bound = max_bound,
+       bound_increment = bound_increment, cards = cards, monos = monos};
 
     val output_format_params =
       {verbose = verbose, debug = debug, max_potential = max_potential, max_genuine = max_genuine,