--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 15 12:16:08 2010 +0200
@@ -126,7 +126,9 @@
fun nice_name (full_name, _) NONE = (full_name, NONE)
| nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
+ if String.isPrefix "$" full_name then
+ (full_name, SOME the_pool)
+ else case Symtab.lookup (fst the_pool) full_name of
SOME nice_name => (nice_name, SOME the_pool)
| NONE =>
let
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 15 12:16:08 2010 +0200
@@ -676,7 +676,7 @@
val preprocess_options = Predicate_Compile_Aux.Options {
expected_modes = NONE,
- proposed_modes = NONE,
+ proposed_modes = [],
proposed_names = [],
show_steps = false,
show_intermediate_results = false,
@@ -685,6 +685,7 @@
show_mode_inference = false,
show_compilation = false,
show_caught_failures = false,
+ show_invalid_clauses = false,
skip_proof = true,
no_topmost_reordering = false,
function_flattening = true,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 12:16:08 2010 +0200
@@ -139,16 +139,24 @@
(Term_Graph.strong_conn gr) thy))
end
-fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
+datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
+ | Single_Pred of (mode * string option) list
+
+fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
let
fun chk s = member (op =) raw_options s
+ val proposed_modes = case proposed_modes of
+ Single_Pred proposed_modes => [(const, proposed_modes)]
+ | Multiple_Preds proposed_modes => map
+ (apfst (Code.read_const (ProofContext.theory_of lthy))) proposed_modes
in
Options {
expected_modes = Option.map (pair const) expected_modes,
- proposed_modes = Option.map (pair const o map fst) proposed_modes,
+ proposed_modes =
+ map (apsnd (map fst)) proposed_modes,
proposed_names =
- the_default [] (Option.map (map_filter
- (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
+ maps (fn (predname, ms) => (map_filter
+ (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
@@ -156,6 +164,7 @@
show_mode_inference = chk "show_mode_inference",
show_compilation = chk "show_compilation",
show_caught_failures = false,
+ show_invalid_clauses = chk "show_invalid_clauses",
skip_proof = chk "skip_proof",
function_flattening = not (chk "no_function_flattening"),
specialise = chk "specialise",
@@ -174,7 +183,7 @@
val const = Code.read_const thy raw_const
val T = Sign.the_const_type thy const
val t = Const (const, T)
- val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
+ val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const)
in
if is_inductify options then
let
@@ -208,9 +217,13 @@
val mode_and_opt_proposal = parse_mode_expr --
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
+
val opt_modes =
Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
- Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
+ (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
+ (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
+ || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
+ --| Parse.$$$ ")") (Multiple_Preds [])
val opt_expected_modes =
Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 12:16:08 2010 +0200
@@ -99,7 +99,7 @@
(* Different options for compiler *)
datatype options = Options of {
expected_modes : (string * mode list) option,
- proposed_modes : (string * mode list) option,
+ proposed_modes : (string * mode list) list,
proposed_names : ((string * mode) * string) list,
show_steps : bool,
show_proof_trace : bool,
@@ -108,6 +108,7 @@
show_modes : bool,
show_compilation : bool,
show_caught_failures : bool,
+ show_invalid_clauses : bool,
skip_proof : bool,
no_topmost_reordering : bool,
function_flattening : bool,
@@ -119,7 +120,7 @@
compilation : compilation
};
val expected_modes : options -> (string * mode list) option
- val proposed_modes : options -> (string * mode list) option
+ val proposed_modes : options -> string -> mode list option
val proposed_names : options -> string -> mode -> string option
val show_steps : options -> bool
val show_proof_trace : options -> bool
@@ -128,6 +129,7 @@
val show_modes : options -> bool
val show_compilation : options -> bool
val show_caught_failures : options -> bool
+ val show_invalid_clauses : options -> bool
val skip_proof : options -> bool
val no_topmost_reordering : options -> bool
val function_flattening : options -> bool
@@ -703,7 +705,7 @@
datatype options = Options of {
expected_modes : (string * mode list) option,
- proposed_modes : (string * mode list) option,
+ proposed_modes : (string * mode list) list,
proposed_names : ((string * mode) * string) list,
show_steps : bool,
show_proof_trace : bool,
@@ -712,6 +714,7 @@
show_modes : bool,
show_compilation : bool,
show_caught_failures : bool,
+ show_invalid_clauses : bool,
skip_proof : bool,
no_topmost_reordering : bool,
function_flattening : bool,
@@ -724,7 +727,7 @@
};
fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) = #proposed_modes opt
+fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
(#proposed_names opt) (name, mode)
@@ -735,7 +738,7 @@
fun show_mode_inference (Options opt) = #show_mode_inference opt
fun show_compilation (Options opt) = #show_compilation opt
fun show_caught_failures (Options opt) = #show_caught_failures opt
-
+fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt
fun skip_proof (Options opt) = #skip_proof opt
fun function_flattening (Options opt) = #function_flattening opt
@@ -752,7 +755,7 @@
val default_options = Options {
expected_modes = NONE,
- proposed_modes = NONE,
+ proposed_modes = [],
proposed_names = [],
show_steps = false,
show_intermediate_results = false,
@@ -761,6 +764,7 @@
show_mode_inference = false,
show_compilation = false,
show_caught_failures = false,
+ show_invalid_clauses = false,
skip_proof = true,
no_topmost_reordering = false,
function_flattening = false,
@@ -773,8 +777,8 @@
}
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
- "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
- "detect_switches", "specialise", "no_topmost_reordering"]
+ "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
+ "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
fun print_step options s =
if show_steps options then tracing s else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 12:16:08 2010 +0200
@@ -402,8 +402,8 @@
| NONE => ()
fun check_proposed_modes preds options modes errors =
- case proposed_modes options of
- SOME (s, ms) => (case AList.lookup (op =) modes s of
+ map (fn (s, _) => case proposed_modes options s of
+ SOME ms => (case AList.lookup (op =) modes s of
SOME inferred_ms =>
let
val preds_without_modes = map fst (filter (null o snd) modes)
@@ -413,15 +413,16 @@
error ("expected modes were not inferred:\n"
^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
- ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
- ^ cat_lines errors ^
+ ^ (if show_invalid_clauses options then
+ ("For the following clauses, the following modes could not be inferred: " ^ "\n"
+ ^ cat_lines errors) else "") ^
(if not (null preds_without_modes) then
"\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
else ""))
else ()
end
| NONE => ())
- | NONE => ()
+ | NONE => ()) preds
(* importing introduction rules *)
@@ -1505,7 +1506,6 @@
fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
preds all_modes param_vs clauses =
let
- val collect_errors = false
fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
fun add_needs_random s (false, m) = ((false, m), false)
| add_needs_random s (true, m) = ((true, m), needs_random s m)
@@ -1551,7 +1551,7 @@
(modes @ extra_modes)) modes
val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
- if collect_errors then
+ if show_invalid_clauses options then
fixp_with_state (fn (modes, errors) =>
let
val (modes', new_errors) = split_list (iteration modes)
@@ -2702,8 +2702,8 @@
all_modes_of_typ T
val all_modes =
map (fn (s, T) =>
- (s, case (proposed_modes options) of
- SOME (s', ms) => if s = s' then ms else generate_modes s T
+ (s, case proposed_modes options s of
+ SOME ms => ms
| NONE => generate_modes s T)) preds
val params =
case intrs of
@@ -2721,7 +2721,7 @@
let
val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
in
- ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args
+ ho_args_of_typ (snd (dest_Const p)) args
end
val param_vs = map (fst o dest_Free) params
fun add_clause intr clauses =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 12:16:08 2010 +0200
@@ -67,7 +67,7 @@
val options = Options {
expected_modes = NONE,
- proposed_modes = NONE,
+ proposed_modes = [],
proposed_names = [],
show_steps = false,
show_intermediate_results = false,
@@ -76,6 +76,7 @@
show_mode_inference = false,
show_compilation = false,
show_caught_failures = false,
+ show_invalid_clauses = false,
skip_proof = false,
compilation = Random,
inductify = true,
@@ -89,7 +90,7 @@
val debug_options = Options {
expected_modes = NONE,
- proposed_modes = NONE,
+ proposed_modes = [],
proposed_names = [],
show_steps = true,
show_intermediate_results = true,
@@ -98,6 +99,7 @@
show_mode_inference = true,
show_compilation = false,
show_caught_failures = true,
+ show_invalid_clauses = false,
skip_proof = false,
compilation = Random,
inductify = true,
@@ -113,13 +115,15 @@
fun set_function_flattening b
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re})
@@ -127,13 +131,15 @@
fun set_fail_safe_function_flattening b
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
no_topmost_reordering = re})
@@ -141,13 +147,15 @@
fun set_no_higher_order_predicate ss
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
- show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+ show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+ show_invalid_clauses = s_ic, skip_proof = s_p,
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
--- a/src/Tools/Metis/metis.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/Tools/Metis/metis.ML Wed Sep 15 12:16:08 2010 +0200
@@ -179,7 +179,7 @@
(* Pointer equality using the run-time system. *)
(* ------------------------------------------------------------------------- *)
-fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y);
+fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y) (* MODIFIED by Jasmin Blanchette *)
(* ------------------------------------------------------------------------- *)
(* Timing function applications. *)