# HG changeset patch # User haftmann # Date 1288098057 -7200 # Node ID 2c77c2e5788742d889196b81d5f15c1d60e16041 # Parent 9b6e918682d577215bfd9476534699aff4c9aab6# Parent eddda8e38360b6ba342a07064b9f7090c777fe5c merged diff -r eddda8e38360 -r 2c77c2e57887 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 14:06:22 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 15:00:57 2010 +0200 @@ -316,11 +316,10 @@ fun get_prover ctxt args = let - val thy = ProofContext.theory_of ctxt fun default_prover_name () = hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." - fun get_prover name = (name, Sledgehammer.get_prover thy false name) + fun get_prover name = (name, Sledgehammer.get_prover ctxt false name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name diff -r eddda8e38360 -r 2c77c2e57887 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 14:06:22 2010 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 15:00:57 2010 +0200 @@ -228,7 +228,7 @@ val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")"; val _ = Outer_Syntax.local_theory - "partial_function" "define partial function" Keyword.thy_goal + "partial_function" "define partial function" Keyword.thy_decl ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec))) >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec)); diff -r eddda8e38360 -r 2c77c2e57887 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 14:06:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 15:00:57 2010 +0200 @@ -63,7 +63,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val get_prover : theory -> bool -> string -> prover + val get_prover : Proof.context -> bool -> string -> prover val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * Proof.state @@ -410,30 +410,35 @@ | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError -fun run_smt_solver remote ({timeout, ...} : params) minimize_command +fun run_smt_solver ctxt remote ({timeout, ...} : params) minimize_command ({state, subgoal, subgoal_count, axioms, ...} : prover_problem) = let val {outcome, used_facts, run_time_in_msecs} = SMT_Solver.smt_filter remote timeout state (map_filter (try dest_Untranslated) axioms) subgoal + val outcome' = outcome |> Option.map failure_from_smt_failure (* FIXME *) val message = - if outcome = NONE then + case outcome of + NONE => try_command_line (proof_banner false) (apply_on_subgoal subgoal subgoal_count ^ command_call smtN (map fst used_facts)) ^ minimize_line minimize_command (map fst used_facts) - else - "" + | SOME (SMT_Solver.Other_Failure message) => message + | SOME _ => string_for_failure (the outcome') in - {outcome = outcome |> Option.map failure_from_smt_failure, - used_axioms = used_facts, run_time_in_msecs = SOME run_time_in_msecs, - message = message} + {outcome = outcome', used_axioms = used_facts, + run_time_in_msecs = SOME run_time_in_msecs, message = message} end -fun get_prover thy auto name = - if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name) - else run_atp auto name (get_atp thy name) +fun get_prover ctxt auto name = + let val thy = ProofContext.theory_of ctxt in + if is_smt_prover name then + run_smt_solver ctxt (String.isPrefix remote_prefix name) + else + run_atp auto name (get_atp thy name) + end fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) auto minimize_command @@ -452,7 +457,7 @@ fun go () = let fun really_go () = - get_prover thy auto name params (minimize_command name) problem + get_prover ctxt auto name params (minimize_command name) problem |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some", message)) val (outcome_code, message) = diff -r eddda8e38360 -r 2c77c2e57887 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 14:06:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 15:00:57 2010 +0200 @@ -92,7 +92,8 @@ state axioms = let val thy = Proof.theory_of state - val prover = get_prover thy false prover_name + val ctxt = Proof.context_of state + val prover = get_prover ctxt false prover_name val msecs = Time.toMilliseconds timeout val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".") val {goal, ...} = Proof.goal state diff -r eddda8e38360 -r 2c77c2e57887 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Oct 26 14:06:22 2010 +0200 +++ b/src/Pure/Isar/code.ML Tue Oct 26 15:00:57 2010 +0200 @@ -542,7 +542,7 @@ val (rep, lhs) = dest_comb full_lhs handle TERM _ => bad "Not an abstract equation"; val (rep_const, ty) = dest_Const rep; - val (tyco, sorts) = ((apsnd o map) (snd o dest_TVar) o dest_Type o domain_type) ty + val (tyco, Ts) = (dest_Type o domain_type) ty handle TERM _ => bad "Not an abstract equation" | TYPE _ => bad "Not an abstract equation"; val _ = case some_tyco of SOME tyco' => if tyco = tyco' then () @@ -553,8 +553,8 @@ else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); val _ = check_eqn thy { allow_nonlinear = false, allow_consts = false, allow_pats = false } thm (lhs, rhs); - val _ = if forall (Sign.subsort thy) (sorts ~~ map snd vs') then () - else error ("Sort constraints on type arguments are weaker than in abstype certificate.") + val _ = if forall (Sign.of_sort thy) (Ts ~~ map snd vs') then () + else error ("Type arguments do not satisfy sort constraints of abstype certificate."); in (thm, tyco) end; fun assert_eqn thy = error_thm (gen_assert_eqn thy true);