# HG changeset patch # User wenzelm # Date 1256658597 -3600 # Node ID ea4e3f1eee69c01a03d45fee3a3b7bf63446336a # Parent 66eddea44a67d33c64df04b994335c471edf434e# Parent cf8da4f3f92b1e4aee833d9c2ded5ac51c0ca706 merged diff -r 66eddea44a67 -r ea4e3f1eee69 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Tue Oct 27 16:16:12 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Tue Oct 27 16:49:57 2009 +0100 @@ -21,8 +21,6 @@ val trace = Unsynchronized.ref false; fun trace_msg msg = if ! trace then tracing (msg ()) else (); -structure Recon = ResReconstruct; - val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*) @@ -211,14 +209,14 @@ | strip_happ args x = (x, args); fun fol_type_to_isa _ (Metis.Term.Var v) = - (case Recon.strip_prefix ResClause.tvar_prefix v of - SOME w => Recon.make_tvar w - | NONE => Recon.make_tvar v) + (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of + SOME w => ResReconstruct.make_tvar w + | NONE => ResReconstruct.make_tvar v) | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = - (case Recon.strip_prefix ResClause.tconst_prefix x of - SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys) + (case ResReconstruct.strip_prefix ResClause.tconst_prefix x of + SOME tc => Term.Type (ResReconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys) | NONE => - case Recon.strip_prefix ResClause.tfree_prefix x of + case ResReconstruct.strip_prefix ResClause.tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => error ("fol_type_to_isa: " ^ x)); @@ -227,10 +225,10 @@ let val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case Recon.strip_prefix ResClause.tvar_prefix v of - SOME w => Type (Recon.make_tvar w) + (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of + SOME w => Type (ResReconstruct.make_tvar w) | NONE => - case Recon.strip_prefix ResClause.schematic_var_prefix v of + case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -247,14 +245,14 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case Recon.strip_prefix ResClause.const_prefix a of + case ResReconstruct.strip_prefix ResClause.const_prefix a of SOME b => - let val c = Recon.invert_const b - val ntypes = Recon.num_typargs thy c + let val c = ResReconstruct.invert_const b + val ntypes = ResReconstruct.num_typargs thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = Recon.num_typargs thy c + val ntyargs = ResReconstruct.num_typargs thy c in if length tys = ntyargs then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ @@ -265,13 +263,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case Recon.strip_prefix ResClause.tconst_prefix a of - SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) + case ResReconstruct.strip_prefix ResClause.tconst_prefix a of + SOME b => + Type (Term.Type (ResReconstruct.invert_type_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case Recon.strip_prefix ResClause.tfree_prefix a of + case ResReconstruct.strip_prefix ResClause.tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case Recon.strip_prefix ResClause.fixed_var_prefix a of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -282,16 +281,16 @@ fun fol_term_to_hol_FT ctxt fol_tm = let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case Recon.strip_prefix ResClause.schematic_var_prefix v of + (case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case Recon.strip_prefix ResClause.const_prefix x of - SOME c => Const (Recon.invert_const c, dummyT) + (case ResReconstruct.strip_prefix ResClause.const_prefix x of + SOME c => Const (ResReconstruct.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Recon.strip_prefix ResClause.fixed_var_prefix x of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -302,13 +301,15 @@ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case Recon.strip_prefix ResClause.const_prefix x of - SOME c => Const (Recon.invert_const c, dummyT) + (case ResReconstruct.strip_prefix ResClause.const_prefix x of + SOME c => Const (ResReconstruct.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Recon.strip_prefix ResClause.fixed_var_prefix x of + case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) - | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t) + | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); + fol_term_to_hol_RAW ctxt t)) + | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); + fol_term_to_hol_RAW ctxt t) in cvt fol_tm end; fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt @@ -382,9 +383,9 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case Recon.strip_prefix ResClause.schematic_var_prefix a of + case ResReconstruct.strip_prefix ResClause.schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case Recon.strip_prefix ResClause.tvar_prefix a of + | NONE => case ResReconstruct.strip_prefix ResClause.tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) @@ -451,7 +452,7 @@ in cterm_instantiate [(refl_x, c_t)] REFL_THM end; fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy (Const (c, _)) = (ResReconstruct.num_typargs thy c handle TYPE _ => 0) | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) @@ -522,7 +523,7 @@ val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) + (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end; val factor = Seq.hd o distinct_subgoals_tac; diff -r 66eddea44a67 -r ea4e3f1eee69 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Tue Oct 27 16:16:12 2009 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Tue Oct 27 16:49:57 2009 +0100 @@ -346,11 +346,16 @@ fold Thm.weaken (rev sorted_clauses) False_thm end in - case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of + case + let val the_solver = ! solver + in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end + of SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => ( if !trace_sat then tracing ("Proof trace from SAT solver:\n" ^ - "clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^ + "clauses: " ^ ML_Syntax.print_list + (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) + (Inttab.dest clause_table) ^ "\n" ^ "empty clause: " ^ Int.toString empty_id) else (); if !quick_and_dirty then @@ -388,8 +393,9 @@ val msg = "SAT solver found a countermodel:\n" ^ (commas o map (fn (term, idx) => - Syntax.string_of_term_global @{theory} term ^ ": " - ^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false"))) + Syntax.string_of_term_global @{theory} term ^ ": " ^ + (case assignment idx of NONE => "arbitrary" + | SOME true => "true" | SOME false => "false"))) (Termtab.dest atom_table) in raise THM (msg, 0, []) diff -r 66eddea44a67 -r ea4e3f1eee69 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Tue Oct 27 16:16:12 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Tue Oct 27 16:49:57 2009 +0100 @@ -370,13 +370,13 @@ (* string * solver -> unit *) - fun add_solver (name, new_solver) = + fun add_solver (name, new_solver) = CRITICAL (fn () => let val the_solvers = !solvers; val _ = if AList.defined (op =) the_solvers name then warning ("SAT solver " ^ quote name ^ " was defined before") else (); - in solvers := AList.update (op =) (name, new_solver) the_solvers end; + in solvers := AList.update (op =) (name, new_solver) the_solvers end); (* ------------------------------------------------------------------------- *) (* invoke_solver: returns the solver associated with the given 'name' *)