# HG changeset patch # User haftmann # Date 1290811814 -3600 # Node ID 813a6f68cec29758cee8db330d5eb081c2076179 # Parent 4375cc6f1a7ebfbd2161527f06b4e6362a2b5db2# Parent 4f2c3e842ef89b011df8608b81767cd234b1e433 merged diff -r 4f2c3e842ef8 -r 813a6f68cec2 NEWS --- a/NEWS Fri Nov 26 23:49:49 2010 +0100 +++ b/NEWS Fri Nov 26 23:50:14 2010 +0100 @@ -104,14 +104,13 @@ avoid confusion with finite sets. INCOMPATIBILITY. * Quickcheck's generator for random generation is renamed from "code" to -"random". INCOMPATIBILITY. +"random". INCOMPATIBILITY. * Theory Multiset provides stable quicksort implementation of sort_key. * Quickcheck now has a configurable time limit which is set to 30 seconds by default. This can be changed by adding [timeout = n] to the quickcheck -command. The time limit for auto quickcheck is still set independently, -by default to 5 seconds. +command. The time limit for Auto Quickcheck is still set independently. * New command 'partial_function' provides basic support for recursive function definitions over complete partial orders. Concrete instances @@ -357,11 +356,26 @@ (and "ms" and "min" are no longer supported) INCOMPATIBILITY. +* Metis and Meson now have configuration options "meson_trace", "metis_trace", + and "metis_verbose" that can be enabled to diagnose these tools. E.g. + + using [[metis_trace = true]] + * Nitpick: - Renamed options: nitpick [timeout = 77 s] ~> nitpick [timeout = 77] nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777] INCOMPATIBILITY. + - Now requires Kodkodi 1.2.9. INCOMPATIBILITY. + - Added support for partial quotient types. + - Added local versions of the "Nitpick.register_xxx" functions. + - Added "whack" option. + - Allow registration of quotient types as codatatypes. + - Improved "merge_type_vars" option to merge more types. + - Removed unsound "fast_descrs" option. + - Added custom symmetry breaking for datatypes, making it possible to reach + higher cardinalities. + - Prevent the expansion of too large definitions. * Changed SMT configuration options: - Renamed: @@ -650,7 +664,7 @@ Tracing is then active for all invocations of the simplifier in subsequent goal refinement steps. Tracing may also still be enabled or -disabled via the ProofGeneral settings menu. +disabled via the Proof General settings menu. * Separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact' replace the former 'hide' KIND command. Minor diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Fri Nov 26 23:50:14 2010 +0100 @@ -46,7 +46,7 @@ structure Meson : MESON = struct -val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false) +val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 26 23:50:14 2010 +0100 @@ -31,8 +31,8 @@ open Metis_Translate -val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false) -val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true) +val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false) +val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun verbose_warning ctxt msg = diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 26 23:50:14 2010 +0100 @@ -440,7 +440,7 @@ val smt_iter_timeout_divisor = 2 val smt_monomorph_limit = 4 -fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = +fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i = let val ctxt = Proof.context_of state fun iter timeout iter_num outcome0 msecs_so_far facts = @@ -534,6 +534,7 @@ val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated val {outcome, used_facts, run_time_in_msecs} = smt_filter_loop params remote state subgoal (map_filter smt_fact facts) + val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) val outcome = outcome |> Option.map failure_from_smt_failure val message = case outcome of @@ -547,8 +548,9 @@ in try_command_line (proof_banner auto) (apply_on_subgoal subgoal subgoal_count ^ - command_call method (map (fst o fst) used_facts)) ^ - minimize_line minimize_command (map (fst o fst) used_facts) + command_call method (map fst other_lemmas)) ^ + minimize_line minimize_command + (map fst (other_lemmas @ chained_lemmas)) end | SOME failure => string_for_failure "SMT solver" failure in diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 26 23:50:14 2010 +0100 @@ -24,7 +24,9 @@ val command_call : string -> string list -> string val try_command_line : string -> string -> string val minimize_line : ('a list -> string) -> 'a list -> string - val metis_proof_text : metis_params -> text_result + val split_used_facts : + (string * locality) list + -> (string * locality) list * (string * locality) list val isar_proof_text : isar_params -> metis_params -> text_result val proof_text : bool -> isar_params -> metis_params -> text_result end; @@ -159,15 +161,15 @@ fun used_facts_in_tstplike_proof fact_names = atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names) -fun used_facts fact_names = - used_facts_in_tstplike_proof fact_names - #> List.partition (curry (op =) Chained o snd) +val split_used_facts = + List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) fun metis_proof_text (banner, full_types, minimize_command, tstplike_proof, fact_names, goal, i) = let - val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof + val (chained_lemmas, other_lemmas) = + split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof) val n = Logic.count_prems (prop_of goal) in (metis_line banner full_types i n (map fst other_lemmas) ^ @@ -912,14 +914,14 @@ in do_proof end fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (other_params as (_, full_types, _, tstplike_proof, + (metis_params as (_, full_types, _, tstplike_proof, fact_names, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = metis_proof_text other_params + val (one_line_proof, lemma_names) = metis_proof_text metis_params fun isar_proof_for () = case isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor tstplike_proof conjecture_shape fact_names @@ -940,8 +942,8 @@ |> the_default "\nWarning: The Isar proof construction failed." in (one_line_proof ^ isar_proof, lemma_names) end -fun proof_text isar_proof isar_params other_params = +fun proof_text isar_proof isar_params metis_params = (if isar_proof then isar_proof_text isar_params else metis_proof_text) - other_params + metis_params end; diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/HOL/ex/Normalization_by_Evaluation.thy --- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 23:49:49 2010 +0100 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri Nov 26 23:50:14 2010 +0100 @@ -66,7 +66,7 @@ lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" - by normalization rule+ + by normalization lemma "rev [a, b, c] = [c, b, a]" by normalization value [nbe] "rev (a#b#cs) = rev cs @ [b, a]" value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])" @@ -108,10 +108,13 @@ lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization value [nbe] "Suc 0 \ set ms" +(* non-left-linear patterns, equality by extensionality *) + lemma "f = f" by normalization lemma "f x = f x" by normalization lemma "(f o g) x = f (g x)" by normalization lemma "(f o id) x = f x" by normalization +lemma "(id :: bool \ bool) = id" by normalization value [nbe] "(\x. x)" (* Church numerals: *) diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/Pure/library.ML --- a/src/Pure/library.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/Pure/library.ML Fri Nov 26 23:50:14 2010 +0100 @@ -546,7 +546,7 @@ fun forall2 P [] [] = true | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys - | forall2 P _ _ = false; + | forall2 P _ _ = raise UnequalLengths; fun map_split f [] = ([], []) | map_split f (x :: xs) = diff -r 4f2c3e842ef8 -r 813a6f68cec2 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Nov 26 23:49:49 2010 +0100 +++ b/src/Tools/nbe.ML Fri Nov 26 23:50:14 2010 +0100 @@ -18,7 +18,7 @@ val apps: Univ -> Univ list -> Univ (*explicit applications*) val abss: int -> (Univ list -> Univ) -> Univ (*abstractions as closures*) - val same: Univ -> Univ -> bool + val eq_Univ: Univ * Univ -> bool val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context val trace: bool Unsynchronized.ref @@ -170,11 +170,6 @@ | Abs of (int * (Univ list -> Univ)) * Univ list (*abstractions as closures*); -fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys - | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l - | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys - | same _ _ = false; - (* constructor functions *) @@ -188,6 +183,28 @@ | apps (Const (name, xs)) ys = Const (name, ys @ xs) | apps (BVar (n, xs)) ys = BVar (n, ys @ xs); +fun satisfy_abs (abs as ((n, f), xs)) some_k = + let + val ys = case some_k + of NONE => replicate n (BVar (0, [])) + | SOME k => map_range (fn l => BVar (k + l, [])) n; + in (apps (Abs abs) ys, ys) end; + +fun maxidx (Const (_, xs)) = fold maxidx xs + | maxidx (DFree _) = I + | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1) + | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE)); + +fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys) + | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l + | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys) + | eq_Univ (x as Abs abs, y) = + let + val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0) + in eq_Univ (x, apps y ys) end + | eq_Univ (x, y as Abs _) = eq_Univ (y, x) + | eq_Univ _ = false; + (** assembling and compiling ML code from terms **) @@ -241,7 +258,7 @@ val name_const = prefix ^ "Const"; val name_abss = prefix ^ "abss"; val name_apps = prefix ^ "apps"; - val name_same = prefix ^ "same"; + val name_eq = prefix ^ "eq_Univ"; in val univs_cookie = (Univs.get, put_result, name_put); @@ -267,7 +284,7 @@ fun nbe_abss 0 f = f `$` ml_list [] | nbe_abss n f = name_abss `$$` [string_of_int n, f]; -fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")"; +fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))"; end; @@ -353,7 +370,7 @@ val (samepairs, args') = subst_nonlin_vars args; val s_args = map assemble_arg args'; val s_rhs = if null samepairs then assemble_rhs rhs - else ml_if (ml_and (map (uncurry nbe_same) samepairs)) + else ml_if (ml_and (map nbe_eq samepairs)) (assemble_rhs rhs) default_rhs; val eqns = if is_eval then [([ml_list (rev (dicts @ s_args))], s_rhs)]