# HG changeset patch # User bulwahn # Date 1279780666 -7200 # Node ID 38e71ffc8fe8dc8bdcd62e4f30e39dd4098c3b4a # Parent 22e0797857e6072c18287fe88df8860e1db9525c# Parent 24785fa2416cf2a33d8ee45b31738198e56eafda merged diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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, diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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 diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Nitpick/nitpick.ML --- 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"), diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 = diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- 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 ([], []) diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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) => diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- 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)), diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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(, , ). diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- 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; diff -r 22e0797857e6 -r 38e71ffc8fe8 src/HOL/Tools/meson.ML --- 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.*)