# HG changeset patch # User blanchet # Date 1314275107 -7200 # Node ID a330c0608da82c1e59c6d9a1a7997b3e122c60bf # Parent ba22ed224b20b6376eb56f6aeff02559bdbf9b05 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics diff -r ba22ed224b20 -r a330c0608da8 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Aug 25 14:25:06 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Aug 25 14:25:07 2011 +0200 @@ -9,14 +9,16 @@ signature METIS_RECONSTRUCT = sig + type type_enc = ATP_Translate.type_enc + exception METIS of string * string val hol_clause_from_metis : - Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm - -> term + Proof.context -> type_enc -> int Symtab.table -> (string * term) list + -> Metis_Thm.thm -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val replay_one_inference : - Proof.context -> (string * term) list -> int Symtab.table + Proof.context -> type_enc -> (string * term) list -> int Symtab.table -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : @@ -33,38 +35,39 @@ exception METIS of string * string -fun atp_name_from_metis s = - case find_first (fn (_, (s', _)) => s' = s) metis_name_table of +fun atp_name_from_metis type_enc s = + case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of SOME ((s, _), (_, swap)) => (s, swap) | _ => (s, false) -fun atp_term_from_metis (Metis_Term.Fn (s, tms)) = - let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in - ATerm (s, tms |> map atp_term_from_metis |> swap ? rev) +fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) = + let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in + ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev) end - | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, []) + | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, []) -fun hol_term_from_metis ctxt sym_tab = - atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE +fun hol_term_from_metis ctxt type_enc sym_tab = + atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE -fun atp_literal_from_metis (pos, atom) = - atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot -fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, [])) - | atp_clause_from_metis lits = - lits |> map atp_literal_from_metis |> mk_aconns AOr +fun atp_literal_from_metis type_enc (pos, atom) = + atom |> Metis_Term.Fn |> atp_term_from_metis type_enc + |> AAtom |> not pos ? mk_anot +fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, [])) + | atp_clause_from_metis type_enc lits = + lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr fun reveal_old_skolems_and_infer_types ctxt old_skolems = map (reveal_old_skolem_terms old_skolems) #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) -fun hol_clause_from_metis ctxt sym_tab old_skolems = +fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems = Metis_Thm.clause #> Metis_LiteralSet.toList - #> atp_clause_from_metis + #> atp_clause_from_metis type_enc #> prop_from_atp ctxt false sym_tab #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems) -fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms = - let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms +fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms = + let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms val _ = trace_msg ctxt (fn () => " calling type inference:") val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts @@ -111,10 +114,10 @@ val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] in cterm_instantiate substs th end; -fun assume_inference ctxt old_skolems sym_tab atom = +fun assume_inference ctxt type_enc old_skolems sym_tab atom = inst_excluded_middle (Proof_Context.theory_of ctxt) - (singleton (hol_terms_from_metis ctxt old_skolems sym_tab) + (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) (Metis_Term.Fn atom)) (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying @@ -122,7 +125,7 @@ sorts. Instead we try to arrange that new TVars are distinct and that types can be inferred from terms. *) -fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th = +fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th = let val thy = Proof_Context.theory_of ctxt val i_th = lookth th_pairs th val i_th_vars = Term.add_vars (prop_of i_th) [] @@ -130,7 +133,7 @@ fun subst_translation (x,y) = let val v = find_var x (* We call "reveal_old_skolems_and_infer_types" below. *) - val t = hol_term_from_metis ctxt sym_tab y + val t = hol_term_from_metis ctxt type_enc sym_tab y in SOME (cterm_of thy (Var v), t) end handle Option.Option => (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ @@ -255,7 +258,7 @@ (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) val select_literal = negate_head oo make_last -fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 = +fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 = let val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => @@ -271,7 +274,7 @@ let val thy = Proof_Context.theory_of ctxt val i_atom = - singleton (hol_terms_from_metis ctxt old_skolems sym_tab) + singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) (Metis_Term.Fn atom) val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) @@ -300,10 +303,11 @@ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; -fun refl_inference ctxt old_skolems sym_tab t = +fun refl_inference ctxt type_enc old_skolems sym_tab t = let val thy = Proof_Context.theory_of ctxt - val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t + val i_t = + singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end @@ -313,11 +317,11 @@ val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} -fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr = +fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr = let val thy = Proof_Context.theory_of ctxt val m_tm = Metis_Term.Fn atom val [i_atom, i_tm] = - hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr] + hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr] val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls @@ -336,7 +340,8 @@ #> the #> unmangled_const_name)) in if s = metis_predicator orelse s = predicator_name orelse - s = metis_type_tag orelse s = type_tag_name then + s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag + orelse s = type_tag_name then path_finder tm ps (nth ts p) else if s = metis_app_op orelse s = app_op_name then let @@ -377,21 +382,22 @@ val factor = Seq.hd o distinct_subgoals_tac -fun one_step ctxt old_skolems sym_tab th_pairs p = +fun one_step ctxt type_enc old_skolems sym_tab th_pairs p = case p of (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atom) => - assume_inference ctxt old_skolems sym_tab f_atom + assume_inference ctxt type_enc old_skolems sym_tab f_atom | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1 + inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1 |> factor | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => - resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2 + resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1 + f_th2 |> factor | (_, Metis_Proof.Refl f_tm) => - refl_inference ctxt old_skolems sym_tab f_tm + refl_inference ctxt type_enc old_skolems sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inference ctxt old_skolems sym_tab f_lit f_p f_r + equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r fun flexflex_first_order th = case Thm.tpairs_of th of @@ -443,7 +449,8 @@ end end -fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs = +fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf) + th_pairs = if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then (* Isabelle sometimes identifies literals (premises) that are distinct in @@ -458,7 +465,7 @@ (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf) + val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf) |> flexflex_first_order |> resynchronize ctxt fol_th val _ = trace_msg ctxt diff -r ba22ed224b20 -r a330c0608da8 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:25:06 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:25:07 2011 +0200 @@ -74,9 +74,9 @@ "t => t'", where "t" and "t'" are the same term modulo type tags. In Isabelle, type tags are stripped away, so we are left with "t = t" or "t => t". Type tag idempotence is also handled this way. *) -fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth = +fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth = let val thy = Proof_Context.theory_of ctxt in - case hol_clause_from_metis ctxt sym_tab old_skolems mth of + case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of Const (@{const_name HOL.eq}, _) $ _ $ t => let val ct = cterm_of thy t @@ -91,14 +91,7 @@ fun clause_params type_enc = {ordering = Metis_KnuthBendixOrder.default, - orderLiterals = - (* Type axioms seem to benefit from the positive literal order, but for - compatibility we keep the unsigned order for Metis's default - "partial_types" mode. *) - if is_type_enc_fairly_sound type_enc then - Metis_Clause.PositiveLiteralOrder - else - Metis_Clause.UnsignedLiteralOrder, + orderLiterals = Metis_Clause.UnsignedLiteralOrder, orderTerms = true} fun active_params type_enc = {clause = clause_params type_enc, @@ -133,7 +126,7 @@ val (sym_tab, axioms, old_skolems) = prepare_metis_problem ctxt type_enc cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = - reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth + reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") @@ -155,7 +148,7 @@ val proof = Metis_Proof.proof mth val result = axioms - |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof + |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used diff -r ba22ed224b20 -r a330c0608da8 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Thu Aug 25 14:25:06 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Aug 25 14:25:07 2011 +0200 @@ -18,13 +18,14 @@ val metis_equal : string val metis_predicator : string val metis_app_op : string - val metis_type_tag : string + val metis_systematic_type_tag : string + val metis_ad_hoc_type_tag : string val metis_generated_var_prefix : string val trace : bool Config.T val verbose : bool Config.T val trace_msg : Proof.context -> (unit -> string) -> unit val verbose_warning : Proof.context -> string -> unit - val metis_name_table : ((string * int) * (string * bool)) list + val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list val reveal_old_skolem_terms : (string * term) list -> term -> term val prepare_metis_problem : Proof.context -> type_enc -> thm list -> thm list @@ -39,8 +40,10 @@ val metis_equal = "=" val metis_predicator = "{}" -val metis_app_op = "." -val metis_type_tag = ":" +val metis_app_op = Metis_Name.toString Metis_Term.appName +val metis_systematic_type_tag = + Metis_Name.toString Metis_Term.hasTypeFunctionName +val metis_ad_hoc_type_tag = "**" val metis_generated_var_prefix = "_" val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) @@ -51,11 +54,13 @@ if Config.get ctxt verbose then warning ("Metis: " ^ msg) else () val metis_name_table = - [((tptp_equal, 2), (metis_equal, false)), - ((tptp_old_equal, 2), (metis_equal, false)), - ((prefixed_predicator_name, 1), (metis_predicator, false)), - ((prefixed_app_op_name, 2), (metis_app_op, false)), - ((prefixed_type_tag_name, 2), (metis_type_tag, true))] + [((tptp_equal, 2), (K metis_equal, false)), + ((tptp_old_equal, 2), (K metis_equal, false)), + ((prefixed_predicator_name, 1), (K metis_predicator, false)), + ((prefixed_app_op_name, 2), (K metis_app_op, false)), + ((prefixed_type_tag_name, 2), + (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag + | _ => metis_ad_hoc_type_tag, true))] fun old_skolem_const_name i j num_T_args = old_skolem_const_prefix ^ Long_Name.separator ^ @@ -114,32 +119,34 @@ val prepare_helper = Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs) -fun metis_term_from_atp (ATerm (s, tms)) = +fun metis_term_from_atp type_enc (ATerm (s, tms)) = if is_tptp_variable s then Metis_Term.Var (Metis_Name.fromString s) else - let - val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms) - |> the_default (s, false) - in - Metis_Term.Fn (Metis_Name.fromString s, - tms |> map metis_term_from_atp |> swap ? rev) - end -fun metis_atom_from_atp (AAtom tm) = - (case metis_term_from_atp tm of + (case AList.lookup (op =) metis_name_table (s, length tms) of + SOME (f, swap) => (f type_enc, swap) + | NONE => (s, false)) + |> (fn (s, swap) => + Metis_Term.Fn (Metis_Name.fromString s, + tms |> map (metis_term_from_atp type_enc) + |> swap ? rev)) +fun metis_atom_from_atp type_enc (AAtom tm) = + (case metis_term_from_atp type_enc tm of Metis_Term.Fn x => x | _ => raise Fail "non CNF -- expected function") - | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom" -fun metis_literal_from_atp (AConn (ANot, [phi])) = - (false, metis_atom_from_atp phi) - | metis_literal_from_atp phi = (true, metis_atom_from_atp phi) -fun metis_literals_from_atp (AConn (AOr, phis)) = - maps metis_literals_from_atp phis - | metis_literals_from_atp phi = [metis_literal_from_atp phi] -fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = + | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom" +fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) = + (false, metis_atom_from_atp type_enc phi) + | metis_literal_from_atp type_enc phi = + (true, metis_atom_from_atp type_enc phi) +fun metis_literals_from_atp type_enc (AConn (AOr, phis)) = + maps (metis_literals_from_atp type_enc) phis + | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi] +fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) = let fun some isa = - SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList + SOME (phi |> metis_literals_from_atp type_enc + |> Metis_LiteralSet.fromList |> Metis_Thm.axiom, isa) in if ident = type_tag_idempotence_helper_name orelse @@ -164,7 +171,7 @@ in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end | NONE => TrueI |> Isa_Raw |> some end - | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" + | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula" (* Function to generate metis clauses, including comb and type clauses *) fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses = @@ -205,8 +212,8 @@ *) (* "rev" is for compatibility. *) val axioms = - atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) - |> rev + atp_problem + |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev in (sym_tab, axioms, old_skolems) end end;