--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 11:21:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 11:21:25 2010 +0200
@@ -45,7 +45,7 @@
val invert_const: string -> string
val ascii_of: string -> string
val undo_ascii_of: string -> string
- val strip_prefix: string -> string -> string option
+ val strip_prefix_and_undo_ascii: string -> string -> string option
val make_schematic_var : string * int -> string
val make_fixed_var : string -> string
val make_schematic_type_var : string * int -> string
@@ -163,7 +163,7 @@
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
-fun strip_prefix s1 s =
+fun strip_prefix_and_undo_ascii s1 s =
if String.isPrefix s1 s then
SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
else
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 11:21:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jul 26 11:21:25 2010 +0200
@@ -223,15 +223,15 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
- (case strip_prefix tvar_prefix v of
+ (case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
- (case strip_prefix type_const_prefix x of
+ (case strip_prefix_and_undo_ascii type_const_prefix x of
SOME tc => Term.Type (invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
- case strip_prefix tfree_prefix x of
+ case strip_prefix_and_undo_ascii tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
@@ -241,10 +241,10 @@
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case strip_prefix tvar_prefix v of
+ (case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => Type (make_tvar w)
| NONE =>
- case strip_prefix schematic_var_prefix v of
+ case strip_prefix_and_undo_ascii 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*)
@@ -261,7 +261,7 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case strip_prefix const_prefix a of
+ case strip_prefix_and_undo_ascii const_prefix a of
SOME b =>
let val c = invert_const b
val ntypes = num_type_args thy c
@@ -279,14 +279,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix type_const_prefix a of
+ case strip_prefix_and_undo_ascii type_const_prefix a of
SOME b =>
Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix tfree_prefix a of
+ case strip_prefix_and_undo_ascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix fixed_var_prefix a of
+ case strip_prefix_and_undo_ascii 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
@@ -302,16 +302,16 @@
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case strip_prefix schematic_var_prefix v of
+ (case strip_prefix_and_undo_ascii 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 strip_prefix const_prefix x of
+ (case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix fixed_var_prefix x of
+ case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -322,10 +322,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case strip_prefix const_prefix x of
+ (case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix fixed_var_prefix x of
+ case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
hol_term_from_metis_PT ctxt t))
@@ -405,9 +405,9 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case strip_prefix schematic_var_prefix a of
+ case strip_prefix_and_undo_ascii schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case strip_prefix tvar_prefix a of
+ | NONE => case strip_prefix_and_undo_ascii 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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 11:21:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 11:21:25 2010 +0200
@@ -11,7 +11,16 @@
type arity_clause = Metis_Clauses.arity_clause
type fol_clause = Metis_Clauses.fol_clause
+ datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+ datatype quantifier = AForall | AExists
+ datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+ datatype 'a formula =
+ AQuant of quantifier * 'a list * 'a formula |
+ AConn of connective * 'a formula list |
+ APred of 'a fo_term
+
val axiom_prefix : string
+ val conjecture_prefix : string
val write_tptp_file :
theory -> bool -> bool -> bool -> Path.T
-> fol_clause list * fol_clause list * fol_clause list * fol_clause list
@@ -30,7 +39,7 @@
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIff
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype 'a formula =
AQuant of quantifier * 'a list * 'a formula |
AConn of connective * 'a formula list |
@@ -51,7 +60,9 @@
| string_for_connective AAnd = "&"
| string_for_connective AOr = "|"
| string_for_connective AImplies = "=>"
+ | string_for_connective AIf = "<="
| string_for_connective AIff = "<=>"
+ | string_for_connective ANotIff = "<~>"
fun string_for_formula (AQuant (q, xs, phi)) =
string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
string_for_formula phi
@@ -141,8 +152,6 @@
val conjecture_prefix = "conj_"
val arity_clause_prefix = "clsarity_"
-fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
-
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
@@ -180,6 +189,7 @@
fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
+ | formula_for_fo_literals [lit] = formula_for_fo_literal lit
| formula_for_fo_literals (lit :: lits) =
AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])
@@ -191,7 +201,7 @@
fun problem_line_for_axiom full_types
(clause as FOLClause {axiom_name, kind, ...}) =
- Fof (hol_ident axiom_prefix axiom_name, kind,
+ Fof (axiom_prefix ^ ascii_of axiom_name, kind,
formula_for_axiom full_types clause)
fun problem_line_for_class_rel_clause
@@ -214,10 +224,10 @@
|> formula_for_fo_literals)
fun problem_line_for_conjecture full_types
- (clause as FOLClause {axiom_name, kind, literals, ...}) =
- Fof (hol_ident conjecture_prefix axiom_name, kind,
- map (fo_literal_for_literal full_types) literals
- |> formula_for_fo_literals |> mk_anot)
+ (clause as FOLClause {clause_id, kind, literals, ...}) =
+ Fof (conjecture_prefix ^ Int.toString clause_id,
+ kind, map (fo_literal_for_literal full_types) literals
+ |> formula_for_fo_literals |> mk_anot)
fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
@@ -269,7 +279,7 @@
16383 (* large number *)
else if full_types then
0
- else case strip_prefix const_prefix s of
+ else case strip_prefix_and_undo_ascii const_prefix s of
SOME s' => num_type_args thy (invert_const s')
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
@@ -364,7 +374,7 @@
(conjectures, axiom_clauses, extra_clauses, helper_clauses,
class_rel_clauses, arity_clauses) =
let
- val explicit_forall = true (* FIXME *)
+ val explicit_forall = true (* ### FIXME *)
val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
val class_rel_lines =
map problem_line_for_class_rel_clause class_rel_clauses