got rid of support for Kodkodi < 1.2.14
authorblanchet
Wed Dec 12 11:18:06 2012 +0100 (2012-12-12)
changeset 504879486641e691b
parent 50486 d5dc28fafd9d
child 50488 1b3eb579e08b
got rid of support for Kodkodi < 1.2.14
src/HOL/Nitpick_Examples/minipick.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Dec 12 03:47:02 2012 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Dec 12 11:18:06 2012 +0100
     1.3 @@ -438,6 +438,7 @@
     1.4        JavaNotFound => "unknown"
     1.5      | JavaTooOld => "unknown"
     1.6      | KodkodiNotInstalled => "unknown"
     1.7 +    | KodkodiTooOld => "unknown"
     1.8      | Normal ([], _, _) => "none"
     1.9      | Normal _ => "genuine"
    1.10      | TimedOut _ => "unknown"
     2.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Dec 12 03:47:02 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Dec 12 11:18:06 2012 +0100
     2.3 @@ -158,6 +158,7 @@
     2.4      JavaNotFound |
     2.5      JavaTooOld |
     2.6      KodkodiNotInstalled |
     2.7 +    KodkodiTooOld |
     2.8      Normal of (int * raw_bound list) list * int list * string |
     2.9      TimedOut of int list |
    2.10      Error of string * int list
    2.11 @@ -305,6 +306,7 @@
    2.12    JavaNotFound |
    2.13    JavaTooOld |
    2.14    KodkodiNotInstalled |
    2.15 +  KodkodiTooOld |
    2.16    Normal of (int * raw_bound list) list * int list * string |
    2.17    TimedOut of int list |
    2.18    Error of string * int list
    2.19 @@ -316,12 +318,12 @@
    2.20     rel_expr_func: rel_expr -> 'a -> 'a,
    2.21     int_expr_func: int_expr -> 'a -> 'a}
    2.22  
    2.23 -fun is_new_kodkodi_version () =
    2.24 +fun is_kodkodi_too_old () =
    2.25    case getenv "KODKODI_VERSION" of
    2.26 -    "" => false
    2.27 +    "" => true
    2.28    | s => dict_ord int_ord (s |> space_explode "."
    2.29                               |> map (the_default 0 o Int.fromString),
    2.30 -                           [1, 2, 13]) = GREATER
    2.31 +                           [1, 2, 14]) = LESS
    2.32  
    2.33  (** Auxiliary functions on Kodkod problems **)
    2.34  
    2.35 @@ -525,10 +527,7 @@
    2.36  fun int_reg_name j = "$i" ^ base_name j
    2.37  
    2.38  fun tuple_name x = n_ary_name x "A" "P" "T"
    2.39 -fun rel_name new_kodkodi (n, j) =
    2.40 -  n_ary_name (n, if new_kodkodi then j
    2.41 -                 else if j >= 0 then 2 * j
    2.42 -                 else 2 * ~j - 1) "s" "r" "m"
    2.43 +fun rel_name x = n_ary_name x "s" "r" "m"
    2.44  fun var_name x = n_ary_name x "S" "R" "M"
    2.45  fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
    2.46  fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
    2.47 @@ -540,8 +539,7 @@
    2.48  fun block_comment "" = ""
    2.49    | block_comment comment = prefix_lines "// " comment ^ "\n"
    2.50  
    2.51 -fun commented_rel_name new_kodkodi (x, s) =
    2.52 -  rel_name new_kodkodi x ^ inline_comment s
    2.53 +fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
    2.54  
    2.55  fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
    2.56    | string_for_tuple (TupleIndex x) = tuple_name x
    2.57 @@ -592,8 +590,8 @@
    2.58    | string_for_tuple_assign (AssignTupleSet (x, ts)) =
    2.59      tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
    2.60  
    2.61 -fun string_for_bound new_kodkodi (zs, tss) =
    2.62 -  "bounds " ^ commas (map (commented_rel_name new_kodkodi) zs) ^ ": " ^
    2.63 +fun string_for_bound (zs, tss) =
    2.64 +  "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
    2.65    (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
    2.66    (if length tss = 1 then "" else "]") ^ "\n"
    2.67  
    2.68 @@ -696,8 +694,6 @@
    2.69  
    2.70  fun write_problem_file out problems =
    2.71    let
    2.72 -    val new_kodkodi = is_new_kodkodi_version ()
    2.73 -    val rel_name = rel_name new_kodkodi
    2.74      fun out_outmost_f (And (f1, f2)) =
    2.75          (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
    2.76        | out_outmost_f f = out_f f prec_And
    2.77 @@ -850,7 +846,7 @@
    2.78                              settings) ^
    2.79                "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
    2.80                implode (map string_for_tuple_assign tuple_assigns) ^
    2.81 -              implode (map (string_for_bound new_kodkodi) bounds) ^
    2.82 +              implode (map string_for_bound bounds) ^
    2.83                (if int_bounds = [] then
    2.84                   ""
    2.85                 else
    2.86 @@ -883,31 +879,28 @@
    2.87  val scan_nat =
    2.88    Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
    2.89    >> (the o Int.fromString o space_implode "")
    2.90 -fun scan_rel_name new_kodkodi =
    2.91 +val scan_rel_name =
    2.92    ($$ "s" |-- scan_nat >> pair 1
    2.93     || $$ "r" |-- scan_nat >> pair 2
    2.94     || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
    2.95    >> (fn ((n, j), SOME _) => (n, ~j - 1)
    2.96 -       | ((n, j), NONE) => (n, if new_kodkodi then j
    2.97 -                               else if j mod 2 = 0 then j div 2
    2.98 -                               else ~(j + 1) div 2))
    2.99 +       | ((n, j), NONE) => (n, j))
   2.100  val scan_atom = $$ "A" |-- scan_nat
   2.101  fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
   2.102  fun parse_list scan = parse_non_empty_list scan || Scan.succeed []
   2.103  val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]"
   2.104  val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]"
   2.105 -fun parse_assignment new_kodkodi =
   2.106 -  (scan_rel_name new_kodkodi --| $$ "=") -- parse_tuple_set
   2.107 -fun parse_instance new_kodkodi =
   2.108 +val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set
   2.109 +val parse_instance =
   2.110    Scan.this_string "relations:"
   2.111 -  |-- $$ "{" |-- parse_list (parse_assignment new_kodkodi) --| $$ "}"
   2.112 +  |-- $$ "{" |-- parse_list parse_assignment --| $$ "}"
   2.113  
   2.114 -fun extract_instance new_kodkodi =
   2.115 +val extract_instance =
   2.116    fst o Scan.finite Symbol.stopper
   2.117              (Scan.error (!! (fn _ =>
   2.118                                  raise SYNTAX ("Kodkod.extract_instance",
   2.119                                                "ill-formed Kodkodi output"))
   2.120 -                            (parse_instance new_kodkodi)))
   2.121 +                            parse_instance))
   2.122    o strip_blanks o raw_explode
   2.123  
   2.124  val problem_marker = "*** PROBLEM "
   2.125 @@ -918,15 +911,15 @@
   2.126    Substring.string o fst o Substring.position "\n\n"
   2.127    o Substring.triml (size marker)
   2.128  
   2.129 -fun read_next_instance new_kodkodi s =
   2.130 +fun read_next_instance s =
   2.131    let val s = Substring.position instance_marker s |> snd in
   2.132      if Substring.isEmpty s then
   2.133        raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
   2.134      else
   2.135 -      read_section_body instance_marker s |> extract_instance new_kodkodi
   2.136 +      read_section_body instance_marker s |> extract_instance
   2.137    end
   2.138  
   2.139 -fun read_next_outcomes new_kodkodi j (s, ps, js) =
   2.140 +fun read_next_outcomes j (s, ps, js) =
   2.141    let val (s1, s2) = Substring.position outcome_marker s in
   2.142      if Substring.isEmpty s2 orelse
   2.143         not (Substring.isEmpty (Substring.position problem_marker s1
   2.144 @@ -938,17 +931,16 @@
   2.145          val s = Substring.triml (size outcome_marker) s2
   2.146        in
   2.147          if String.isSuffix "UNSATISFIABLE" outcome then
   2.148 -          read_next_outcomes new_kodkodi j (s, ps, j :: js)
   2.149 +          read_next_outcomes j (s, ps, j :: js)
   2.150          else if String.isSuffix "SATISFIABLE" outcome then
   2.151 -          read_next_outcomes new_kodkodi j
   2.152 -                           (s, (j, read_next_instance new_kodkodi s2) :: ps, js)
   2.153 +          read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
   2.154          else
   2.155            raise SYNTAX ("Kodkod.read_next_outcomes",
   2.156                          "unknown outcome " ^ quote outcome)
   2.157        end
   2.158    end
   2.159  
   2.160 -fun read_next_problems new_kodkodi (s, ps, js) =
   2.161 +fun read_next_problems (s, ps, js) =
   2.162    let val s = Substring.position problem_marker s |> snd in
   2.163      if Substring.isEmpty s then
   2.164        (ps, js)
   2.165 @@ -958,17 +950,14 @@
   2.166          val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
   2.167                           |> Int.fromString |> the
   2.168          val j = j_plus_1 - 1
   2.169 -      in
   2.170 -        read_next_problems new_kodkodi
   2.171 -                           (read_next_outcomes new_kodkodi j (s, ps, js))
   2.172 -      end
   2.173 +      in read_next_problems (read_next_outcomes j (s, ps, js)) end
   2.174    end
   2.175    handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
   2.176                                          "expected number after \"PROBLEM\"")
   2.177  
   2.178 -fun read_output_file new_kodkodi path =
   2.179 +fun read_output_file path =
   2.180    (false,
   2.181 -   read_next_problems new_kodkodi (Substring.full (File.read path), [], [])
   2.182 +   read_next_problems (Substring.full (File.read path), [], [])
   2.183     |>> rev ||> rev)
   2.184    handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
   2.185  
   2.186 @@ -999,7 +988,6 @@
   2.187  fun uncached_solve_any_problem overlord deadline max_threads max_solutions
   2.188                                 problems =
   2.189    let
   2.190 -    val new_kodkodi = is_new_kodkodi_version ()
   2.191      val j = find_index (curry (op =) True o #formula) problems
   2.192      val indexed_problems = if j >= 0 then
   2.193                               [(j, nth problems j)]
   2.194 @@ -1048,7 +1036,7 @@
   2.195                        " > " ^ File.shell_path out_path ^
   2.196                        " 2> " ^ File.shell_path err_path)
   2.197                val (io_error, (ps, nontriv_js)) =
   2.198 -                read_output_file new_kodkodi out_path
   2.199 +                read_output_file out_path
   2.200                  ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
   2.201                val js = triv_js @ nontriv_js
   2.202                val first_error =
   2.203 @@ -1073,6 +1061,8 @@
   2.204                    JavaTooOld
   2.205                  else if has_error "NoClassDefFoundError" then
   2.206                    KodkodiNotInstalled
   2.207 +                else if is_kodkodi_too_old () then
   2.208 +                  KodkodiTooOld
   2.209                  else if first_error <> "" then
   2.210                    Error (first_error, js)
   2.211                  else if io_error then
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Dec 12 03:47:02 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Dec 12 11:18:06 2012 +0100
     3.3 @@ -191,7 +191,12 @@
     3.4    \\"kodkodi-x.y.z\" directory's full path to " ^
     3.5    Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
     3.6    " on a line of its own."
     3.7 -
     3.8 +fun kodkodi_too_old_message () =
     3.9 +  "The installed Kodkodi version is too old. To install a newer version, \
    3.10 +  \download the package from \"http://www21.in.tum.de/~blanchet/#software\" \
    3.11 +  \and add the \"kodkodi-x.y.z\" directory's full path to " ^
    3.12 +  Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
    3.13 +  " on a line of its own."
    3.14  val max_unsound_delay_ms = 200
    3.15  val max_unsound_delay_percent = 2
    3.16  
    3.17 @@ -817,6 +822,9 @@
    3.18            | KK.KodkodiNotInstalled =>
    3.19              (print_nt kodkodi_not_installed_message;
    3.20               (found_really_genuine, max_potential, max_genuine, donno + 1))
    3.21 +          | KK.KodkodiTooOld =>
    3.22 +            (print_nt kodkodi_too_old_message;
    3.23 +             (found_really_genuine, max_potential, max_genuine, donno + 1))
    3.24            | KK.Normal ([], unsat_js, s) =>
    3.25              (update_checked_problems problems unsat_js; show_kodkod_warning s;
    3.26               (found_really_genuine, max_potential, max_genuine, donno))