--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Jul 22 08:37:46 2010 +0200
@@ -9,7 +9,6 @@
signature ATP_MANAGER =
sig
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
- type name_pool = Sledgehammer_TPTP_Format.name_pool
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
{debug: bool,
@@ -38,7 +37,7 @@
type prover_result =
{outcome: failure option,
message: string,
- pool: name_pool option,
+ pool: string Symtab.table,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
@@ -108,7 +107,7 @@
type prover_result =
{outcome: failure option,
message: string,
- pool: name_pool option,
+ pool: string Symtab.table,
relevant_thm_names: string list,
atp_run_time_in_msecs: int,
output: string,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Thu Jul 22 08:37:46 2010 +0200
@@ -19,7 +19,6 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
-open Clausifier
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
@@ -133,14 +132,14 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
-fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) =
- (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
+fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
+ c = (if pos then "c_False" else "c_True")
| is_false_literal _ = false
-fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) =
+fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_True") orelse
(not pol andalso c = "c_False")
| is_true_literal _ = false;
-fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
+fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals
(* making axiom and conjecture clauses *)
fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
@@ -152,7 +151,7 @@
raise TRIVIAL ()
else
(skolems,
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
end
@@ -180,12 +179,12 @@
Symtab.map_entry c (Integer.add 1)
| count_combterm (CombVar _) = I
| count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+fun count_literal (FOLLiteral (_, t)) = count_combterm t
+fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
fun cnf_helper_thms thy raw =
map (`Thm.get_name_hint)
- #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true)
+ #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
val optional_helpers =
[(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
@@ -233,10 +232,11 @@
val helper_clauses =
get_helper_clauses thy is_FO full_types conjectures extra_cls
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val classrel_clauses = make_classrel_clauses thy subs supers'
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
(Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses,
+ class_rel_clauses, arity_clauses))
end
@@ -255,7 +255,7 @@
(* get clauses and prepare them for writing *)
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt;
- val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
+ val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
case filtered_clauses of
@@ -264,7 +264,7 @@
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
- |> cnf_rules_pairs thy true
+ |> Clausifier.cnf_rules_pairs thy true
val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Jul 22 08:37:46 2010 +0200
@@ -492,7 +492,6 @@
else
0
val settings = [("solver", commas_quote kodkod_sat_solver),
- ("skolem_depth", "-1"),
("bit_width", string_of_int bit_width),
("symmetry_breaking", "20"),
("sharing", "3"),
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Jul 22 08:37:46 2010 +0200
@@ -547,59 +547,74 @@
skolem_depth =
let
val incrs = map (Integer.add 1)
- fun aux ss Ts js depth polar t =
+ fun aux ss Ts js skolemizable polar t =
let
fun do_quantifier quant_s quant_T abs_s abs_T t =
- if not (loose_bvar1 (t, 0)) then
- aux ss Ts js depth polar (incr_boundvars ~1 t)
- else if depth <= skolem_depth andalso
- is_positive_existential polar quant_s then
- let
- val j = length (!skolems) + 1
- val sko_s = skolem_prefix_for (length js) j ^ abs_s
- val _ = Unsynchronized.change skolems (cons (sko_s, ss))
- val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
- map Bound (rev js))
- val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
- in
- if null js then s_betapply Ts (abs_t, sko_t)
- else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
- end
- else
- Const (quant_s, quant_T)
- $ Abs (abs_s, abs_T,
- if is_higher_order_type abs_T then
- t
+ (if not (loose_bvar1 (t, 0)) then
+ aux ss Ts js skolemizable polar (incr_boundvars ~1 t)
+ else if is_positive_existential polar quant_s then
+ let
+ val j = length (!skolems) + 1
+ val (js', (ss', Ts')) =
+ js ~~ (ss ~~ Ts)
+ |> filter (fn (j, _) => loose_bvar1 (t, j + 1))
+ |> ListPair.unzip ||> ListPair.unzip
+ in
+ if skolemizable andalso length js' <= skolem_depth then
+ let
+ val sko_s = skolem_prefix_for (length js') j ^ abs_s
+ val _ = Unsynchronized.change skolems (cons (sko_s, ss'))
+ val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T),
+ map Bound (rev js'))
+ val abs_t = Abs (abs_s, abs_T,
+ aux ss Ts (incrs js) skolemizable polar t)
+ in
+ if null js' then
+ s_betapply Ts (abs_t, sko_t)
else
- aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
- (depth + 1) polar t)
+ Const (@{const_name Let}, abs_T --> quant_T) $ sko_t
+ $ abs_t
+ end
+ else
+ raise SAME ()
+ end
+ else
+ raise SAME ())
+ handle SAME () =>
+ Const (quant_s, quant_T)
+ $ Abs (abs_s, abs_T,
+ if is_higher_order_type abs_T then
+ t
+ else
+ aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+ skolemizable polar t)
in
case t of
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
+ @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ $ aux ss Ts js skolemizable polar t2
| @{const Pure.conjunction} $ t1 $ t2 =>
- @{const Pure.conjunction} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
+ @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
+ $ aux ss Ts js skolemizable polar t2
| @{const Trueprop} $ t1 =>
- @{const Trueprop} $ aux ss Ts js depth polar t1
+ @{const Trueprop} $ aux ss Ts js skolemizable polar t1
| @{const Not} $ t1 =>
- @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
+ @{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1
| Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| @{const "op &"} $ t1 $ t2 =>
- s_conj (pairself (aux ss Ts js depth polar) (t1, t2))
+ s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
| @{const "op |"} $ t1 $ t2 =>
- s_disj (pairself (aux ss Ts js depth polar) (t1, t2))
+ s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
| @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
- $ aux ss Ts js depth polar t2
+ @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ $ aux ss Ts js skolemizable polar t2
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
- t0 $ t1 $ aux ss Ts js depth polar t2
+ t0 $ t1 $ aux ss Ts js skolemizable polar t2
| Const (x as (s, T)) =>
if is_inductive_pred hol_ctxt x andalso
not (is_well_founded_inductive_pred hol_ctxt x) then
@@ -609,7 +624,7 @@
if gfp then (lbfp_prefix, @{const "op |"})
else (ubfp_prefix, @{const "op &"})
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
- |> aux ss Ts js depth polar
+ |> aux ss Ts js skolemizable polar
fun neg () = Const (pref ^ s, T)
in
case polar |> gfp ? flip_polarity of
@@ -627,12 +642,13 @@
else
Const x
| t1 $ t2 =>
- s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1,
- aux ss Ts [] depth Neut t2)
- | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
+ s_betapply Ts (aux ss Ts [] false polar t1,
+ aux ss Ts [] skolemizable Neut t2)
+ | Abs (s, T, t1) =>
+ Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1)
| _ => t
end
- in aux [] [] [] 0 Pos end
+ in aux [] [] [] true Pos end
(** Function specialization **)
@@ -1216,7 +1232,7 @@
(** Preprocessor entry point **)
-val max_skolem_depth = 4
+val max_skolem_depth = 3
fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
boxes, ...}) finitizes monos t =
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 22 08:37:46 2010 +0200
@@ -18,20 +18,20 @@
TVarLit of name * name
datatype arity_clause = ArityClause of
{axiom_name: string, conclLit: arLit, premLits: arLit list}
- datatype classrel_clause = ClassrelClause of
+ datatype class_rel_clause = ClassRelClause of
{axiom_name: string, subclass: name, superclass: name}
datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
+ CombTVar of name |
+ CombTFree of name |
+ CombType of name * combtyp list
datatype combterm =
CombConst of name * combtyp * combtyp list (* Const and Free *) |
CombVar of name * combtyp |
CombApp of combterm * combterm
- datatype literal = Literal of bool * combterm
- datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
+ datatype fol_literal = FOLLiteral of bool * combterm
+ datatype fol_clause =
+ FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: fol_literal list, ctypes_sorts: typ list}
val type_wrapper_name : string
val schematic_var_prefix: string
@@ -59,11 +59,11 @@
val is_skolem_const_name: string -> bool
val num_type_args: theory -> string -> int
val type_literals_for_types : typ list -> type_literal list
- val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+ val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
val type_of_combterm : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
- val literals_of_term : theory -> term -> literal list * typ list
+ val literals_of_term : theory -> term -> fol_literal list * typ list
val conceal_skolem_terms :
int -> (string * term) list -> term -> (string * term) list * term
val reveal_skolem_terms : (string * term) list -> term -> term
@@ -75,8 +75,6 @@
structure Metis_Clauses : METIS_CLAUSES =
struct
-open Clausifier
-
val type_wrapper_name = "ti"
val schematic_var_prefix = "V_";
@@ -85,7 +83,7 @@
val tvar_prefix = "T_";
val tfree_prefix = "t_";
-val classrel_clause_prefix = "clsrel_";
+val class_rel_clause_prefix = "clsrel_";
val const_prefix = "c_";
val type_const_prefix = "tc_";
@@ -288,8 +286,8 @@
(**** Isabelle class relations ****)
-datatype classrel_clause =
- ClassrelClause of {axiom_name: string, subclass: name, superclass: name}
+datatype class_rel_clause =
+ ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
fun class_pairs _ [] _ = []
@@ -300,14 +298,14 @@
fun add_supers sub = fold (add_super sub) supers
in fold add_supers subs [] end
-fun make_classrel_clause (sub,super) =
- ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+fun make_class_rel_clause (sub,super) =
+ ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
ascii_of super,
subclass = `make_type_class sub,
superclass = `make_type_class super};
-fun make_classrel_clauses thy subs supers =
- map make_classrel_clause (class_pairs thy subs supers);
+fun make_class_rel_clauses thy subs supers =
+ map make_class_rel_clause (class_pairs thy subs supers);
(** Isabelle arities **)
@@ -352,27 +350,27 @@
in (classes', multi_arity_clause cpairs) end;
datatype combtyp =
- TyVar of name |
- TyFree of name |
- TyConstr of name * combtyp list
+ CombTVar of name |
+ CombTFree of name |
+ CombType of name * combtyp list
datatype combterm =
CombConst of name * combtyp * combtyp list (* Const and Free *) |
CombVar of name * combtyp |
CombApp of combterm * combterm
-datatype literal = Literal of bool * combterm
+datatype fol_literal = FOLLiteral of bool * combterm
-datatype hol_clause =
- HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
- literals: literal list, ctypes_sorts: typ list}
+datatype fol_clause =
+ FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+ literals: fol_literal list, ctypes_sorts: typ list}
(*********************************************************************)
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)
(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
+fun result_type (CombType (_, [_, tp2])) = tp2
| result_type _ = raise Fail "non-function type"
fun type_of_combterm (CombConst (_, tp, _)) = tp
@@ -387,11 +385,11 @@
fun type_of (Type (a, Ts)) =
let val (folTypes,ts) = types_of Ts in
- (TyConstr (`make_fixed_type_const a, folTypes), ts)
+ (CombType (`make_fixed_type_const a, folTypes), ts)
end
- | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+ | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
| type_of (tp as TVar (x, _)) =
- (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
+ (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
and types_of Ts =
let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
(folTyps, union_all ts)
@@ -399,10 +397,10 @@
(* same as above, but no gathering of sort information *)
fun simp_type_of (Type (a, Ts)) =
- TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
- | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+ CombType (`make_fixed_type_const a, map simp_type_of Ts)
+ | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
| simp_type_of (TVar (x, _)) =
- TyVar (make_schematic_type_var x, string_of_indexname x)
+ CombTVar (make_schematic_type_var x, string_of_indexname x)
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
fun combterm_of thy (Const (c, T)) =
@@ -439,7 +437,7 @@
literals_of_term1 (literals_of_term1 args thy P) thy Q
| literals_of_term1 (lits, ts) thy P =
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
- (Literal (pol, pred) :: lits, union (op =) ts ts')
+ (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
end
val literals_of_term = literals_of_term1 ([], [])
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jul 22 08:37:46 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 (TyVar (x, _)) = Metis.Term.Var x
- | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
- | hol_type_to_fol (TyConstr ((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, _)) =
@@ -103,21 +102,21 @@
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
type_of_combterm tm);
-fun hol_literal_to_fol FO (Literal (pol, tm)) =
+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 pol (fn_isa_to_met p) (tylits @ lits) end
- | hol_literal_to_fol HO (Literal (pol, tm)) =
+ in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+ | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
- metis_lit pol "=" (map hol_term_to_fol_HO tms)
- | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
- | hol_literal_to_fol FT (Literal (pol, tm)) =
+ metis_lit pos "=" (map hol_term_to_fol_HO tms)
+ | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
+ | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
- metis_lit pol "=" (map hol_term_to_fol_FT tms)
- | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
+ metis_lit pos "=" (map hol_term_to_fol_FT tms)
+ | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
fun literals_of_hol_term thy mode t =
let val (lits, types_sorts) = literals_of_term thy t
@@ -170,11 +169,11 @@
(* CLASSREL CLAUSE *)
-fun m_classrel_cls (subclass, _) (superclass, _) =
+fun m_class_rel_cls (subclass, _) (superclass, _) =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
-fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
- (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
+fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
+ (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass)));
(* ------------------------------------------------------------------------- *)
(* FOL to HOL (Metis to Isabelle) *)
@@ -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,15 +599,15 @@
(* ------------------------------------------------------------------------- *)
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
val supers = tvar_classes_of_terms tms
and tycons = type_consts_of_terms thy tms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val classrel_clauses = make_classrel_clauses thy subs supers'
- in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
end;
(* ------------------------------------------------------------------------- *)
@@ -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) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 22 08:37:46 2010 +0200
@@ -18,7 +18,6 @@
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
struct
-open Clausifier
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Proof_Reconstruct
@@ -56,7 +55,7 @@
val _ = priority ("Testing " ^ string_of_int num_theorems ^
" theorem" ^ plural_s num_theorems ^ "...")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = cnf_rules_pairs thy true name_thm_pairs
+ val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jul 22 08:37:46 2010 +0200
@@ -17,7 +17,6 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
-open Clausifier
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open ATP_Manager
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 22 08:37:46 2010 +0200
@@ -8,18 +8,17 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Sledgehammer_TPTP_Format.name_pool
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
-> string * string list
val isar_proof_text:
- name_pool option * bool * int * Proof.context * int list list
+ string Symtab.table * bool * int * Proof.context * int list list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
val proof_text:
- bool -> name_pool option * bool * int * Proof.context * int list list
+ bool -> string Symtab.table * bool * int * Proof.context * int list list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
end;
@@ -27,7 +26,6 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
-open Clausifier
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
@@ -44,12 +42,6 @@
fun is_conjecture_clause_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
-fun ugly_name NONE s = s
- | ugly_name (SOME the_pool) s =
- case Symtab.lookup (snd the_pool) s of
- SOME s' => s'
- | NONE => s
-
fun smart_lambda v t =
Abs (case v of
Const (s, _) =>
@@ -104,7 +96,7 @@
| repair_name _ "$false" = "c_False"
| repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
| repair_name _ "equal" = "c_equal" (* probably not needed *)
- | repair_name pool s = ugly_name pool s
+ | repair_name pool s = Symtab.lookup pool s |> the_default s
(* Generalized first-order terms, which include file names, numbers, etc. *)
(* The "x" argument is not strictly necessary, but without it Poly/ML loops
forever at compile time. *)
@@ -144,12 +136,12 @@
fun ints_of_node (IntLeaf n) = cons n
| ints_of_node (StrNode (_, us)) = fold ints_of_node us
val parse_tstp_annotations =
- Scan.optional ($$ "," |-- parse_term NONE
- --| Scan.option ($$ "," |-- parse_terms NONE)
+ Scan.optional ($$ "," |-- parse_term Symtab.empty
+ --| Scan.option ($$ "," |-- parse_terms Symtab.empty)
>> (fn source => ints_of_node source [])) []
fun parse_definition pool =
- $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
+ $$ "(" |-- parse_literal pool --| Scan.this_string "<=>"
-- parse_clause pool --| $$ ")"
(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Thu Jul 22 08:37:46 2010 +0200
@@ -7,16 +7,15 @@
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
- type classrel_clause = Metis_Clauses.classrel_clause
+ type class_rel_clause = Metis_Clauses.class_rel_clause
type arity_clause = Metis_Clauses.arity_clause
- type hol_clause = Metis_Clauses.hol_clause
- type name_pool = string Symtab.table * string Symtab.table
+ type fol_clause = Metis_Clauses.fol_clause
val write_tptp_file :
theory -> bool -> bool -> bool -> Path.T
- -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
- * classrel_clause list * arity_clause list
- -> name_pool option * int
+ -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
+ * class_rel_clause list * arity_clause list
+ -> string Symtab.table * int
end;
structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
@@ -56,8 +55,6 @@
(** Nice names **)
-type name_pool = string Symtab.table * string Symtab.table
-
fun empty_name_pool readable_names =
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
@@ -120,9 +117,9 @@
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
- | atp_term_for_combtyp (TyFree name) = ATerm (name, [])
- | atp_term_for_combtyp (TyConstr (name, tys)) =
+fun atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
+ | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
+ | atp_term_for_combtyp (CombType (name, tys)) =
ATerm (name, map atp_term_for_combtyp tys)
fun atp_term_for_combterm full_types top_level u =
@@ -145,7 +142,7 @@
else t
end
-fun atp_literal_for_literal full_types (Literal (pos, t)) =
+fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
(pos, atp_term_for_combterm full_types true t)
fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
@@ -154,18 +151,18 @@
(pos, ATerm (class, [ATerm (name, [])]))
fun atp_literals_for_axiom full_types
- (HOLClause {literals, ctypes_sorts, ...}) =
+ (FOLClause {literals, ctypes_sorts, ...}) =
map (atp_literal_for_literal full_types) literals @
map (atp_literal_for_type_literal false)
(type_literals_for_types ctypes_sorts)
fun problem_line_for_axiom full_types
- (clause as HOLClause {axiom_name, clause_id, kind, ...}) =
+ (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
Cnf (hol_ident axiom_name clause_id, kind,
atp_literals_for_axiom full_types clause)
-fun problem_line_for_classrel
- (ClassrelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel_clause
+ (ClassRelClause {axiom_name, subclass, superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
(true, ATerm (superclass, [ty_arg]))])
@@ -176,16 +173,17 @@
| atp_literal_for_arity_literal (TVarLit (c, sort)) =
(false, ATerm (c, [ATerm (sort, [])]))
-fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
+fun problem_line_for_arity_clause
+ (ArityClause {axiom_name, conclLit, premLits, ...}) =
Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
map atp_literal_for_arity_literal (conclLit :: premLits))
fun problem_line_for_conjecture full_types
- (clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
+ (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
Cnf (hol_ident axiom_name clause_id, kind,
map (atp_literal_for_literal full_types) literals)
-fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
+fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
@@ -303,17 +301,18 @@
fun write_tptp_file thy readable_names full_types explicit_apply file
(conjectures, axiom_clauses, extra_clauses, helper_clauses,
- classrel_clauses, arity_clauses) =
+ class_rel_clauses, arity_clauses) =
let
val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
- val classrel_lines = map problem_line_for_classrel classrel_clauses
- val arity_lines = map problem_line_for_arity arity_clauses
+ val class_rel_lines =
+ map problem_line_for_class_rel_clause class_rel_clauses
+ val arity_lines = map problem_line_for_arity_clause arity_clauses
val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
val conjecture_lines =
map (problem_line_for_conjecture full_types) conjectures
val tfree_lines = problem_lines_for_free_types conjectures
val problem = [("Relevant facts", axiom_lines),
- ("Class relationships", classrel_lines),
+ ("Class relationships", class_rel_lines),
("Arity declarations", arity_lines),
("Helper facts", helper_lines),
("Conjectures", conjecture_lines),
@@ -321,9 +320,12 @@
|> repair_problem thy full_types explicit_apply
val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
val conjecture_offset =
- length axiom_lines + length classrel_lines + length arity_lines
+ length axiom_lines + length class_rel_lines + length arity_lines
+ length helper_lines
val _ = File.write_list file (strings_for_problem problem)
- in (pool, conjecture_offset) end
+ in
+ (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+ conjecture_offset)
+ end
end;
--- a/src/HOL/Tools/meson.ML Wed Jul 21 19:21:07 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jul 22 08:37:46 2010 +0200
@@ -584,8 +584,7 @@
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
fun skolemize_prems_tac ctxt prems =
- cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
- REPEAT o (etac exE);
+ cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)