# HG changeset patch # User blanchet # Date 1271425786 -7200 # Node ID 2c787345c0831f4aeace6c3ce5eb990b62220e70 # Parent da7b40aa221598cf6e701fa384851d0ea3212f5e# Parent 0cdb76723c88023bed5a2f4f8c032be78cebca05 merged diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 16 15:49:46 2010 +0200 @@ -223,7 +223,7 @@ do (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action |> these - |> List.app (unregister "Interrupted (reached timeout)"); + |> List.app (unregister "Timed out."); print_new_messages (); (*give threads some time to respond to interrupt*) OS.Process.sleep min_wait_time) @@ -325,7 +325,7 @@ fun start_prover (params as {timeout, ...}) birth_time death_time i relevance_override proof_state name = (case get_prover (Proof.theory_of proof_state) name of - NONE => warning ("Unknown ATP: " ^ quote name) + NONE => warning ("Unknown ATP: " ^ quote name ^ ".") | SOME prover => let val {context = ctxt, facts, goal} = Proof.goal proof_state; @@ -357,7 +357,10 @@ let val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) - val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *) + val _ = + (* RACE w.r.t. other invocations of Sledgehammer *) + if null (#active (Synchronized.value global_state)) then () + else (kill_atps (); priority "Killed active Sledgehammer threads.") val _ = priority "Sledgehammering..." val _ = List.app (start_prover params birth_time death_time i relevance_override proof_state) atps diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 16 15:49:46 2010 +0200 @@ -65,8 +65,8 @@ else SOME "Ill-formed ATP output" | (failure :: _) => SOME failure -fun generic_prover overlord get_facts prepare write cmd args failure_strs - produce_answer name ({full_types, ...} : params) +fun generic_prover overlord get_facts prepare write_file cmd args failure_strs + produce_answer name ({debug, full_types, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -100,7 +100,7 @@ if destdir' = "" then File.tmp_path probfile else if File.exists (Path.explode destdir') then Path.append (Path.explode destdir') probfile - else error ("No such directory: " ^ destdir') + else error ("No such directory: " ^ destdir' ^ ".") end; (* write out problem file and call prover *) @@ -127,11 +127,12 @@ if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists cmd then - write full_types probfile clauses + write_file debug full_types probfile clauses |> pair (apfst split_time' (bash_output (cmd_line probfile))) - else error ("Bad executable: " ^ Path.implode cmd); + else error ("Bad executable: " ^ Path.implode cmd ^ "."); - (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) + (* If the problem file has not been exported, remove it; otherwise, export + the proof file too. *) fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE; fun export probfile (((proof, _), _), _) = if destdir' = "" then () @@ -140,12 +141,12 @@ val (((proof, atp_run_time_in_msecs), rc), conj_pos) = with_path cleanup export run_on (prob_pathname subgoal); - (* check for success and print out some information on failure *) + (* Check for success and print out some information on failure. *) val failure = find_failure failure_strs proof; val success = rc = 0 andalso is_none failure; val (message, relevant_thm_names) = - if is_some failure then ("External prover failed.", []) - else if rc <> 0 then ("External prover failed: " ^ proof, []) + if is_some failure then ("ATP failed to find a proof.", []) + else if rc <> 0 then ("ATP error: " ^ proof ^ ".", []) else (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, subgoal)); diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Apr 16 15:49:46 2010 +0200 @@ -69,25 +69,25 @@ fun metis_lit b c args = (b, (c, args)); -fun hol_type_to_fol (AtomV x) = Metis.Term.Var x - | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, []) - | hol_type_to_fol (Comp (tc, tps)) = - Metis.Term.Fn (tc, map hol_type_to_fol tps); +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); (*These two functions insert type literals before the real literals. That is the opposite order from TPTP linkup, but maybe OK.*) fun hol_term_to_fol_FO tm = case strip_combterm_comb tm of - (CombConst(c,_,tys), tms) => + (CombConst ((c, _), _, tys), tms) => let val tyargs = map hol_type_to_fol tys val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end - | (CombVar(v,_), []) => Metis.Term.Var v + | (CombVar ((v, _), _), []) => Metis.Term.Var v | _ => error "hol_term_to_fol_FO"; -fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a - | hol_term_to_fol_HO (CombConst (a, _, tylist)) = +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) | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); @@ -95,26 +95,26 @@ (*The fully-typed translation, to avoid type errors*) fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); -fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty) - | hol_term_to_fol_FT (CombConst(a, 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, _)) = wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = 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)) = - let val (CombConst(p,_,tys), tms) = strip_combterm_comb 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 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)) = (case strip_combterm_comb tm of - (CombConst("equal",_,_), tms) => + (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)) = (case strip_combterm_comb tm of - (CombConst("equal",_,_), tms) => + (CombConst(("equal", _), _, _), tms) => metis_lit pol "=" (map hol_term_to_fol_FT tms) | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 16 15:49:46 2010 +0200 @@ -30,13 +30,19 @@ val make_fixed_const : bool -> string -> string val make_fixed_type_const : bool -> string -> string val make_type_class : string -> string + type name = string * string + type name_pool = string Symtab.table * string Symtab.table + val empty_name_pool : bool -> name_pool option + val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b + val nice_name : name -> name_pool option -> string * name_pool option datatype kind = Axiom | Conjecture type axiom_name = string datatype fol_type = - AtomV of string - | AtomF of string - | Comp of string * fol_type list - val string_of_fol_type : fol_type -> string + TyVar of name | + TyFree of name | + TyConstr of name * fol_type list + val string_of_fol_type : + fol_type -> name_pool option -> string * name_pool option datatype type_literal = LTVar of string * string | LTFree of string * string exception CLAUSE of string * term val add_typs : typ list -> type_literal list @@ -207,7 +213,66 @@ fun make_type_class clas = class_prefix ^ ascii_of clas; -(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****) +(**** name pool ****) + +type name = string * string +type name_pool = string Symtab.table * string Symtab.table + +fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE + +fun pool_map f xs = + fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs + o pair [] + +fun add_nice_name full_name nice_prefix j the_pool = + let + val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j) + in + case Symtab.lookup (snd the_pool) nice_name of + SOME full_name' => + if full_name = full_name' then (nice_name, the_pool) + else add_nice_name full_name nice_prefix (j + 1) the_pool + | NONE => + (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool), + Symtab.update_new (nice_name, full_name) (snd the_pool))) + end + +fun translate_first_char f s = + String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE) + +fun clean_short_name full_name s = + let + val s = s |> Long_Name.base_name + |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"] + val s' = s |> explode |> rev |> dropwhile (curry (op =) "'") + val s' = + (s' |> rev + |> implode + |> String.translate + (fn c => if Char.isAlphaNum c then String.str c else "")) + ^ replicate_string (String.size s - length s') "_" + val s' = + if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s' + else s' + val s' = if s' = "op" then full_name else s' + in + case (Char.isLower (String.sub (full_name, 0)), + Char.isLower (String.sub (s', 0))) of + (true, false) => translate_first_char Char.toLower s' + | (false, true) => translate_first_char Char.toUpper s' + | _ => s' + end + +fun nice_name (full_name, _) NONE = (full_name, NONE) + | nice_name (full_name, desired_name) (SOME the_pool) = + case Symtab.lookup (fst the_pool) full_name of + SOME nice_name => (nice_name, SOME the_pool) + | NONE => add_nice_name full_name (clean_short_name full_name desired_name) + 0 the_pool + |> apsnd SOME + +(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG + format ****) datatype kind = Axiom | Conjecture; @@ -215,35 +280,24 @@ (**** Isabelle FOL clauses ****) -(*FIXME: give the constructors more sensible names*) -datatype fol_type = AtomV of string - | AtomF of string - | Comp of string * fol_type list; +datatype fol_type = + TyVar of name | + TyFree of name | + TyConstr of name * fol_type list -fun string_of_fol_type (AtomV x) = x - | string_of_fol_type (AtomF x) = x - | string_of_fol_type (Comp(tcon,tps)) = - tcon ^ (paren_pack (map string_of_fol_type tps)); +fun string_of_fol_type (TyVar sp) pool = nice_name sp pool + | string_of_fol_type (TyFree sp) pool = nice_name sp pool + | string_of_fol_type (TyConstr (sp, tys)) pool = + let + val (s, pool) = nice_name sp pool + val (ss, pool) = pool_map string_of_fol_type tys pool + in (s ^ paren_pack ss, pool) end (*First string is the type class; the second is a TVar or TFfree*) datatype type_literal = LTVar of string * string | LTFree of string * string; exception CLAUSE of string * term; -fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a) - | atomic_type (TVar (v,_)) = AtomV(make_schematic_type_var v); - -(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and - TVars it contains.*) -fun type_of dfg (Type (a, Ts)) = - let val (folTyps, ts) = types_of dfg Ts - val t = make_fixed_type_const dfg a - in (Comp(t,folTyps), ts) end - | type_of dfg T = (atomic_type T, [T]) -and types_of dfg Ts = - let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) - in (folTyps, union_all ts) end; - (*Make literals for sorted type variables*) fun sorts_on_typs_aux (_, []) = [] | sorts_on_typs_aux ((x,i), s::ss) = @@ -282,8 +336,6 @@ (**** Isabelle arities ****) -exception ARCLAUSE of string; - datatype arLit = TConsLit of class * string * string list | TVarLit of class * string; @@ -401,10 +453,10 @@ (*** Find occurrences of functions in clauses ***) -fun add_foltype_funcs (AtomV _, funcs) = funcs - | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs - | add_foltype_funcs (Comp(a,tys), funcs) = - List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; +fun add_foltype_funcs (TyVar _, funcs) = funcs + | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs + | add_foltype_funcs (TyConstr ((s, _), tys), funcs) = + List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys; (*TFrees are recorded as constants*) fun add_type_sort_funcs (TVar _, funcs) = funcs @@ -495,22 +547,24 @@ (**** Produce TPTP files ****) -(*Attach sign in TPTP syntax: false means negate.*) fun tptp_sign true s = s | tptp_sign false s = "~ " ^ s -fun tptp_of_typeLit pos (LTVar (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")") - | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")"); +fun tptp_of_typeLit pos (LTVar (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")") + | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")") + +fun tptp_cnf name kind formula = + "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n" -fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) = - "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ - tptp_pack (tylits@lits) ^ ").\n" - | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) = - "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ - tptp_pack lits ^ ").\n"; +fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) = + tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom" + (tptp_pack (tylits @ lits)) + | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) = + tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture" + (tptp_pack lits) fun tptp_tfree_clause tfree_lit = - "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n"; + tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit]) fun tptp_of_arLit (TConsLit (c,t,args)) = tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") @@ -518,14 +572,14 @@ tptp_sign false (make_type_class c ^ "(" ^ str ^ ")") fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = - "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^ - tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n"; + tptp_cnf (string_of_ar axiom_name) "axiom" + (tptp_pack (map tptp_of_arLit (conclLit :: premLits))) fun tptp_classrelLits sub sup = let val tvar = "(T)" in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = - "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" + tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) end; diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 16 15:49:46 2010 +0200 @@ -6,6 +6,7 @@ signature SLEDGEHAMMER_HOL_CLAUSE = sig + type name = Sledgehammer_FOL_Clause.name type kind = Sledgehammer_FOL_Clause.kind type fol_type = Sledgehammer_FOL_Clause.fol_type type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause @@ -15,8 +16,8 @@ type hol_clause_id = int datatype combterm = - CombConst of string * fol_type * fol_type list (* Const and Free *) | - CombVar of string * fol_type | + CombConst of name * fol_type * fol_type list (* Const and Free *) | + CombVar of name * fol_type | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm datatype hol_clause = @@ -33,11 +34,11 @@ val get_helper_clauses : bool -> theory -> bool -> hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> hol_clause list - val write_tptp_file : bool -> Path.T -> + val write_tptp_file : bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> int * int - val write_dfg_file : bool -> Path.T -> + val write_dfg_file : bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> int * int end @@ -45,6 +46,7 @@ structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = struct +open Sledgehammer_Util open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor @@ -74,8 +76,8 @@ type hol_clause_id = int; datatype combterm = - CombConst of string * fol_type * fol_type list (* Const and Free *) | - CombVar of string * fol_type | + CombConst of name * fol_type * fol_type list (* Const and Free *) | + CombVar of name * fol_type | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm; @@ -89,11 +91,11 @@ (* convert a clause with type Term.term to a clause with type clause *) (*********************************************************************) -fun isFalse (Literal(pol, CombConst(c,_,_))) = +fun isFalse (Literal (pol, CombConst ((c, _), _, _))) = (pol andalso c = "c_False") orelse (not pol andalso c = "c_True") | isFalse _ = false; -fun isTrue (Literal (pol, CombConst(c,_,_))) = +fun isTrue (Literal (pol, CombConst ((c, _), _, _))) = (pol andalso c = "c_True") orelse (not pol andalso c = "c_False") | isTrue _ = false; @@ -101,19 +103,22 @@ fun isTaut (HOLClause {literals,...}) = exists isTrue literals; fun type_of dfg (Type (a, Ts)) = - let val (folTypes,ts) = types_of dfg Ts - in (Comp(make_fixed_type_const dfg a, folTypes), ts) end - | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp]) - | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp]) + let val (folTypes,ts) = types_of dfg Ts in + (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts) + end + | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) + | type_of _ (tp as TVar (x, _)) = + (TyVar (make_schematic_type_var x, string_of_indexname x), [tp]) and types_of dfg Ts = let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) in (folTyps, union_all ts) end; (* same as above, but no gathering of sort information *) fun simp_type_of dfg (Type (a, Ts)) = - Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) - | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a) - | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v); + TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts) + | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a) + | simp_type_of _ (TVar (x, _)) = + TyVar (make_schematic_type_var x, string_of_indexname x); fun const_type_of dfg thy (c,t) = @@ -123,15 +128,15 @@ (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) fun combterm_of dfg thy (Const(c,t)) = let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) - val c' = CombConst(make_fixed_const dfg c, tp, tvar_list) + val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list) in (c',ts) end | combterm_of dfg _ (Free(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombConst(make_fixed_var v, tp, []) + val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end | combterm_of dfg _ (Var(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombVar(make_schematic_var v,tp) + val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v',ts) end | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P @@ -192,8 +197,8 @@ (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) -fun result_type (Comp ("tc_fun", [_, tp2])) = tp2 - | result_type _ = error "result_type" +fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2 + | result_type _ = raise Fail "Non-function type" fun type_of_combterm (CombConst (_, tp, _)) = tp | type_of_combterm (CombVar (_, tp)) = tp @@ -207,11 +212,20 @@ val type_wrapper = "ti"; -fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c +fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) = + needs_hBOOL const_needs_hBOOL c | head_needs_hBOOL _ _ = true; -fun wrap_type full_types (s, tp) = - if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s; +fun wrap_type full_types (s, ty) pool = + if full_types then + let val (s', pool) = string_of_fol_type ty pool in + (type_wrapper ^ paren_pack [s, s'], pool) + end + else + (s, pool) + +fun wrap_type_if full_types cnh (head, s, tp) = + if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s fun apply ss = "hAPP" ^ paren_pack ss; @@ -220,105 +234,118 @@ fun string_apply (v, args) = rev_apply (v, rev args); -(*Apply an operator to the argument strings, using either the "apply" operator or - direct function application.*) -fun string_of_applic full_types cma (CombConst (c, _, tvars), args) = - let val c = if c = "equal" then "c_fequal" else c - val nargs = min_arity_of cma c - val args1 = List.take(args, nargs) - handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^ - Int.toString nargs ^ " but is applied to " ^ - space_implode ", " args) - val args2 = List.drop(args, nargs) - val targs = if full_types then [] else map string_of_fol_type tvars - in - string_apply (c ^ paren_pack (args1@targs), args2) - end - | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) - | string_of_applic _ _ _ = error "string_of_applic"; +(* Apply an operator to the argument strings, using either the "apply" operator + or direct function application. *) +fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args) + pool = + let + val s = if s = "equal" then "c_fequal" else s + val nargs = min_arity_of cma s + val args1 = List.take (args, nargs) + handle Subscript => + raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^ + " but is applied to " ^ commas (map quote args)) + val args2 = List.drop (args, nargs) + val (targs, pool) = if full_types then ([], pool) + else pool_map string_of_fol_type tvars pool + val (s, pool) = nice_name (s, s') pool + in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end + | string_of_application _ _ (CombVar (name, _), args) pool = + nice_name name pool |>> (fn s => string_apply (s, args)) -fun wrap_type_if full_types cnh (head, s, tp) = - if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s; - -fun string_of_combterm (params as (full_types, cma, cnh)) t = - let val (head, args) = strip_combterm_comb t - in wrap_type_if full_types cnh (head, - string_of_applic full_types cma - (head, map (string_of_combterm (params)) args), - type_of_combterm t) - end; +fun string_of_combterm (params as (full_types, cma, cnh)) t pool = + let + val (head, args) = strip_combterm_comb t + val (ss, pool) = pool_map (string_of_combterm params) args pool + val (s, pool) = string_of_application full_types cma (head, ss) pool + in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end (*Boolean-valued terms are here converted to literals.*) -fun boolify params t = - "hBOOL" ^ paren_pack [string_of_combterm params t]; +fun boolify params c = + string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single -fun string_of_predicate (params as (_,_,cnh)) t = +fun string_of_predicate (params as (_, _, cnh)) t = case t of - (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => - (*DFG only: new TPTP prefers infix equality*) - ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2]) - | _ => - case #1 (strip_combterm_comb t) of - CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t - | _ => boolify params t; + (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) => + (* DFG only: new TPTP prefers infix equality *) + pool_map (string_of_combterm params) [t1, t2] + #>> prefix "equal" o paren_pack + | _ => + case #1 (strip_combterm_comb t) of + CombConst ((s, _), _, _) => + (if needs_hBOOL cnh s then boolify else string_of_combterm) params t + | _ => boolify params t -(*** tptp format ***) +(*** TPTP format ***) -fun tptp_of_equality params pol (t1,t2) = - let val eqop = if pol then " = " else " != " - in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end; - -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) = - tptp_of_equality params pol (t1,t2) - | tptp_literal params (Literal(pol,pred)) = - tptp_sign pol (string_of_predicate params pred); +fun tptp_of_equality params pos (t1, t2) = + pool_map (string_of_combterm params) [t1, t2] + #>> space_implode (if pos then " = " else " != ") -(*Given a clause, returns its literals paired with a list of literals concerning TFrees; - the latter should only occur in conjecture clauses.*) -fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = - (map (tptp_literal params) literals, - map (tptp_of_typeLit pos) (add_typs ctypes_sorts)); +fun tptp_literal params + (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1), + t2))) = + tptp_of_equality params pos (t1, t2) + | tptp_literal params (Literal (pos, pred)) = + string_of_predicate params pred #>> tptp_sign pos + +(* Given a clause, returns its literals paired with a list of literals + concerning TFrees; the latter should only occur in conjecture clauses. *) +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = + pool_map (tptp_literal params) literals + #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts)) -fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) = - let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls +fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) + pool = +let + val ((lits, tylits), pool) = + tptp_type_literals params (kind = Conjecture) cls pool in - (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits) - end; + ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool) + end -(*** dfg format ***) +(*** DFG format ***) -fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred); +fun dfg_literal params (Literal (pos, pred)) = + string_of_predicate params pred #>> dfg_sign pos -fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) = - (map (dfg_literal params) literals, - map (dfg_of_typeLit pos) (add_typs ctypes_sorts)); +fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = + pool_map (dfg_literal params) literals + #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts)) -fun get_uvars (CombConst _) vars = vars - | get_uvars (CombVar(v,_)) vars = (v::vars) - | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars); +fun get_uvars (CombConst _) vars pool = (vars, pool) + | get_uvars (CombVar (name, _)) vars pool = + nice_name name pool |>> (fn var => var :: vars) + | get_uvars (CombApp (P, Q)) vars pool = + let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end -fun get_uvars_l (Literal(_,c)) = get_uvars c []; +fun get_uvars_l (Literal (_, c)) = get_uvars c []; -fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals); +fun dfg_vars (HOLClause {literals, ...}) = + pool_map get_uvars_l literals #>> union_all -fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind, - ctypes_sorts, ...}) = - let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls - val vars = dfg_vars cls - val tvars = get_tvar_strs ctypes_sorts +fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind, + ctypes_sorts, ...}) pool = + let + val ((lits, tylits), pool) = + dfg_type_literals params (kind = Conjecture) cls pool + val (vars, pool) = dfg_vars cls pool + val tvars = get_tvar_strs ctypes_sorts in - (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) - end; + ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars), + tylits), pool) + end (** For DFG format: accumulate function and predicate declarations **) fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; -fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = - if c = "equal" then (addtypes tvars funcs, preds) +fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) = + if c = "equal" then + (addtypes tvars funcs, preds) else let val arity = min_arity_of cma c val ntys = if not full_types then length tvars else 0 @@ -327,7 +354,7 @@ if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) else (addtypes tvars funcs, addit preds) end - | add_decls _ (CombVar(_,ctp), (funcs,preds)) = + | add_decls _ (CombVar (_,ctp), (funcs, preds)) = (add_foltype_funcs (ctp,funcs), preds) | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); @@ -368,7 +395,7 @@ Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), ("c_COMBS", 0)]; -fun count_combterm (CombConst (c, _, _), ct) = +fun count_combterm (CombConst ((c, _), _, _), ct) = (case Symtab.lookup ct c of NONE => ct (*no counter*) | SOME n => Symtab.update (c,n+1) ct) | count_combterm (CombVar _, ct) = ct @@ -416,7 +443,7 @@ val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL) in case head of - CombConst (a,_,_) => (*predicate or function version of "equal"?*) + CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*) let val a = if a="equal" andalso not toplev then "c_fequal" else a val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity in @@ -451,39 +478,54 @@ (* TPTP format *) -fun write_tptp_file full_types file clauses = +fun write_tptp_file debug full_types file clauses = let + fun section _ [] = [] + | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss + val pool = empty_name_pool debug val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (full_types, cma, cnh) - val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) + val ((conjecture_clss, tfree_litss), pool) = + pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) + val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses + pool + val classrel_clss = map tptp_classrel_clause classrel_clauses + val arity_clss = map tptp_arity_clause arity_clauses + val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) + helper_clauses pool val _ = File.write_list file ( - map (#1 o (clause2tptp params)) axclauses @ - tfree_clss @ - tptp_clss @ - map tptp_classrel_clause classrel_clauses @ - map tptp_arity_clause arity_clauses @ - map (#1 o (clause2tptp params)) helper_clauses) - in (length axclauses + 1, length tfree_clss + length tptp_clss) + "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ + "% " ^ timestamp () ^ "\n" :: + section "Relevant fact" ax_clss @ + section "Type variable" tfree_clss @ + section "Class relationship" classrel_clss @ + section "Arity declaration" arity_clss @ + section "Helper fact" helper_clss @ + section "Conjecture" conjecture_clss) + in (length axclauses + 1, length tfree_clss + length conjecture_clss) end; (* DFG format *) -fun write_dfg_file full_types file clauses = +fun write_dfg_file debug full_types file clauses = let + val pool = empty_name_pool debug val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses val params = (full_types, cma, cnh) - val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) + val ((conjecture_clss, tfree_litss), pool) = + pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip and probname = Path.implode (Path.base file) - val axstrs = map (#1 o (clause2dfg params)) axclauses + val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) - val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses + val (helper_clauses_strs, pool) = + pool_map (apfst fst oo dfg_clause params) helper_clauses pool val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses val _ = @@ -492,21 +534,22 @@ string_of_descrip probname :: string_of_symbols (string_of_funcs funcs) (string_of_preds (cl_preds @ ty_preds)) :: - "list_of_clauses(axioms,cnf).\n" :: + "list_of_clauses(axioms, cnf).\n" :: axstrs @ map dfg_classrel_clause classrel_clauses @ map dfg_arity_clause arity_clauses @ helper_clauses_strs @ - ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ + ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ tfree_clss @ - dfg_clss @ + conjecture_clss @ ["end_of_list.\n\n", (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) - "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n", + "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n", "end_problem.\n"]) - in (length axclauses + length classrel_clauses + length arity_clauses + - length helper_clauses + 1, length tfree_clss + length dfg_clss) - end; + in + (length axclauses + length classrel_clauses + length arity_clauses + + length helper_clauses + 1, length tfree_clss + length conjecture_clss) + end end; diff -r da7b40aa2215 -r 2c787345c083 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 12:51:57 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 15:49:46 2010 +0200 @@ -8,13 +8,16 @@ sig val plural_s : int -> string val serial_commas : string -> string list -> string list + val replace_all : string -> string -> string -> string + val remove_all : string -> string -> string + val timestamp : unit -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val hashw : word * word -> word val hashw_char : Char.char * word -> word val hashw_string : string * word -> word end; - + structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct @@ -26,6 +29,20 @@ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss +fun replace_all bef aft = + let + fun aux seen "" = String.implode (rev seen) + | aux seen s = + if String.isPrefix bef s then + aux seen "" ^ aft ^ aux [] (unprefix bef s) + else + aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) + in aux [] end + +fun remove_all bef = replace_all bef "" + +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now + fun parse_bool_option option name s = (case s of "smart" => if option then NONE else raise Option