avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
--- 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
--- 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
--- 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;