# HG changeset patch # User haftmann # Date 1284545795 -7200 # Node ID 7565c649e7dd25f0d85cdb8d12950d301a86e043 # Parent 20db6db55a6b06e7826093d8a45be05830d6b774# Parent 7a0fcee7a2a393035e270bbe439783f819aba6c2 merged diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 15 12:16:35 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 diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 15 12:16:35 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, diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Sep 15 12:16:35 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.$$$ ":" |-- diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 15 12:16:35 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 () diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 15 12:16:35 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 = diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 15 12:16:35 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}) diff -r 7a0fcee7a2a3 -r 7565c649e7dd src/Tools/Metis/metis.ML --- a/src/Tools/Metis/metis.ML Wed Sep 15 12:11:11 2010 +0200 +++ b/src/Tools/Metis/metis.ML Wed Sep 15 12:16:35 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. *)