--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:14:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:15:07 2010 +0200
@@ -18,7 +18,6 @@
structure Metis_Tactics : METIS_TACTICS =
struct
-open Clausifier
open Metis_Clauses
exception METIS of string * string
@@ -70,10 +69,10 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (CombTVar (x, _)) = Metis.Term.Var x
- | hol_type_to_fol (CombTFree (s, _)) = Metis.Term.Fn (s, [])
- | hol_type_to_fol (CombType ((s, _), tps)) =
- Metis.Term.Fn (s, map hol_type_to_fol tps);
+fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s
+ | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, [])
+ | metis_term_from_combtyp (CombType ((s, _), tps)) =
+ Metis.Term.Fn (s, map metis_term_from_combtyp tps);
(*These two functions insert type literals before the real literals. That is the
opposite order from TPTP linkup, but maybe OK.*)
@@ -81,7 +80,7 @@
fun hol_term_to_fol_FO tm =
case strip_combterm_comb tm of
(CombConst ((c, _), _, tys), tms) =>
- let val tyargs = map hol_type_to_fol tys
+ let val tyargs = map metis_term_from_combtyp tys
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
| (CombVar ((v, _), _), []) => Metis.Term.Var v
@@ -89,12 +88,12 @@
fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
| hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
- Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
+ Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
-fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
+fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
| hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
@@ -105,7 +104,7 @@
fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
- val tylits = if p = "equal" then [] else map hol_type_to_fol tys
+ val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
| hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
@@ -223,22 +222,23 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-fun fol_type_to_isa _ (Metis.Term.Var v) =
+fun hol_type_from_metis_term _ (Metis.Term.Var v) =
(case strip_prefix tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
- | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
+ | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix type_const_prefix x of
- SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
+ SOME tc => Term.Type (invert_const tc,
+ map (hol_type_from_metis_term ctxt) tys)
| NONE =>
case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
- | NONE => raise Fail ("fol_type_to_isa: " ^ x));
+ | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
(*Maps metis terms to isabelle terms*)
-fun hol_term_from_fol_PT ctxt fol_tm =
+fun hol_term_from_metis_PT ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
- val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
+ 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
@@ -298,8 +298,8 @@
end
(*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_fol_FT ctxt fol_tm =
- let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
+fun hol_term_from_metis_FT ctxt fol_tm =
+ 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
@@ -312,8 +312,8 @@
SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
- SOME v => Free (v, fol_type_to_isa ctxt ty)
- | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
+ 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]), _])) =
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
@@ -327,17 +327,17 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
SOME v => Free (v, dummyT)
- | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
- hol_term_from_fol_PT ctxt t))
- | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
- hol_term_from_fol_PT ctxt t)
+ | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
+ hol_term_from_metis_PT ctxt t))
+ | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t);
+ hol_term_from_metis_PT ctxt t)
in fol_tm |> cvt end
-fun hol_term_from_fol FT = hol_term_from_fol_FT
- | hol_term_from_fol _ = hol_term_from_fol_PT
+fun hol_term_from_metis FT = hol_term_from_metis_FT
+ | hol_term_from_metis _ = hol_term_from_metis_PT
fun hol_terms_from_fol ctxt mode skolems fol_tms =
- let val ts = map (hol_term_from_fol mode ctxt) fol_tms
+ let val ts = map (hol_term_from_metis mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
@@ -398,7 +398,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_fol mode ctxt y
+ val t = hol_term_from_metis mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(trace_msg (fn() => "List.find failed for the variable " ^ x ^
@@ -599,7 +599,7 @@
(* ------------------------------------------------------------------------- *)
fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (cnf_axiom thy false th)
+ if raw then th else the_single (Clausifier.cnf_axiom thy false th)
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
@@ -715,7 +715,7 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
+ map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -774,15 +774,16 @@
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
fun generic_metis_tac mode ctxt ths i st0 =
- let val _ = trace_msg (fn () =>
+ let
+ val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- (Meson.MESON (maps neg_clausify)
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt i) st0
+ Meson.MESON (maps Clausifier.neg_clausify)
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+ ctxt i st0
handle ERROR msg => raise METIS ("generic_metis_tac", msg)
end
handle METIS (loc, msg) =>
@@ -800,7 +801,8 @@
fun method name mode =
Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths)))
+ METHOD (fn facts => HEADGOAL (CHANGED_PROP
+ o generic_metis_tac mode ctxt (facts @ ths)))))
val setup =
type_lits_setup