# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 49347c6354b53dcbdca3fb8c30d781f9988d3d1c # Parent 123f0944e29fc52b5e5eb453b0fea04ff940fc21 parse optional type system specification diff -r 123f0944e29f -r 49347c6354b5 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 @@ -9,6 +9,8 @@ signature METIS_TACTICS = sig + type type_system = ATP_Translate.type_system + val metisN : string val metisF_N : string val metisFT_N : string @@ -20,7 +22,8 @@ val metisF_tac : Proof.context -> thm list -> int -> tactic val metisFT_tac : Proof.context -> thm list -> int -> tactic val metisHO_tac : Proof.context -> thm list -> int -> tactic - val metisX_tac : Proof.context -> thm list -> int -> tactic + val metisX_tac : + Proof.context -> type_system option -> thm list -> int -> tactic val setup : theory -> theory end @@ -69,7 +72,7 @@ val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 = +fun FOL_SOLVE type_sys (mode :: fallback_modes) ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) @@ -85,7 +88,7 @@ val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths val (mode, sym_tab, {axioms, old_skolems, ...}) = - prepare_metis_problem ctxt mode cls ths + prepare_metis_problem ctxt mode type_sys cls ths val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms @@ -145,7 +148,7 @@ ("Falling back on " ^ quote (Binding.qualified_name_of (method_binding_for_mode mode)) ^ "..."); - FOL_SOLVE fallback_modes ctxt cls ths0) + FOL_SOLVE type_sys fallback_modes ctxt cls ths0) val neg_clausify = single @@ -164,19 +167,18 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun generic_metis_tac modes ctxt ths i st0 = +fun generic_metis_tac modes type_sys ctxt ths i st0 = let val _ = trace_msg ctxt (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) + fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1 in if exists_type type_has_top_sort (prop_of st0) then (verbose_warning ctxt "Proof state contains the universal sort {}"; Seq.empty) else - Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE modes ctxt cls ths) 1) - ctxt i st0 + Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 end val metis_modes = [HO, FT] @@ -185,28 +187,37 @@ val metisHO_modes = [HO] val metisX_modes = [New] -val metis_tac = generic_metis_tac metis_modes -val metisF_tac = generic_metis_tac metisF_modes -val metisFT_tac = generic_metis_tac metisFT_modes -val metisHO_tac = generic_metis_tac metisHO_modes -val metisX_tac = generic_metis_tac metisX_modes +val metis_tac = generic_metis_tac metis_modes NONE +val metisF_tac = generic_metis_tac metisF_modes NONE +val metisFT_tac = generic_metis_tac metisFT_modes NONE +val metisHO_tac = generic_metis_tac metisHO_modes NONE +fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt (* Whenever "X" has schematic type variables, we treat "using X by metis" as - "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. + "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on extensionality not being applied) and brings few benefits. *) val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method modes ths ctxt facts = - let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in +fun method modes (type_sys, ths) ctxt facts = + let + val (schem_facts, nonschem_facts) = List.partition has_tvar facts + val type_sys = type_sys |> Option.map type_sys_from_string + in HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths)) + CHANGED_PROP + o generic_metis_tac modes type_sys ctxt (schem_facts @ ths)) end + fun setup_method (modes as mode :: _) = Method.setup (method_binding_for_mode mode) - (Attrib.thms >> (METHOD oo method modes)) + ((if mode = New then + Scan.lift (Scan.option (Args.parens Parse.short_ident)) + else + Scan.succeed NONE) + -- Attrib.thms >> (METHOD oo method modes)) val setup = [(metis_modes, "Metis for FOL and HOL problems"), diff -r 123f0944e29f -r 49347c6354b5 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -10,6 +10,7 @@ signature METIS_TRANSLATE = sig type type_literal = ATP_Translate.type_literal + type type_system = ATP_Translate.type_system datatype mode = FO | HO | FT | New @@ -26,7 +27,7 @@ val reveal_old_skolem_terms : (string * term) list -> term -> term val string_of_mode : mode -> string val prepare_metis_problem : - Proof.context -> mode -> thm list -> thm list + Proof.context -> mode -> type_system option -> thm list -> thm list -> mode * int Symtab.table * metis_problem end @@ -306,10 +307,12 @@ | NONE => TrueI) | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" +val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light) + (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt New conj_clauses fact_clauses = +fun prepare_metis_problem ctxt New type_sys conj_clauses fact_clauses = let - val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) Const_Arg_Types, Light) + val type_sys = type_sys |> the_default default_type_sys val explicit_apply = NONE val clauses = conj_clauses @ fact_clauses val (atp_problem, _, _, _, _, _, sym_tab) = @@ -322,7 +325,7 @@ (New, sym_tab, {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) end - | prepare_metis_problem ctxt mode conj_clauses fact_clauses = + | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = let val thy = Proof_Context.theory_of ctxt (* The modes FO and FT are sticky. HO can be downgraded to FO. *) diff -r 123f0944e29f -r 49347c6354b5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 31 16:38:36 2011 +0200 @@ -385,7 +385,7 @@ val parse_key = Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!") - >> implode_param + >> implode_param val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?" || Parse.$$$ "!")