# HG changeset patch # User blanchet # Date 1271422114 -7200 # Node ID 27b1cc58715e574d752143267b2932bbe2d54134 # Parent 0a6ed065683d4033d0d5d7199b1106764a37077c store nonmangled names along with mangled type names in Sledgehammer for debugging purposes diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Apr 15 13:57:17 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 16 14:48:34 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,7 +127,7 @@ 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 ^ "."); diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 15 13:57:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Apr 16 14:48:34 2010 +0200 @@ -69,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 x) = Metis.Term.Fn (x, []) - | hol_type_to_fol (TyConstr (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.*) diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 15 13:57:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Apr 16 14:48:34 2010 +0200 @@ -30,12 +30,17 @@ 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 = - TyVar of string | - TyFree of string | - TyConstr of string * fol_type list + TyVar of name | + TyFree of name | + TyConstr of name * fol_type list val string_of_fol_type : fol_type -> string datatype type_literal = LTVar of string * string | LTFree of string * string exception CLAUSE of string * term @@ -207,7 +212,65 @@ 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 (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; @@ -216,13 +279,13 @@ (**** Isabelle FOL clauses ****) datatype fol_type = - TyVar of string | - TyFree of string | - TyConstr of string * fol_type list + TyVar of name | + TyFree of name | + TyConstr of name * fol_type list -fun string_of_fol_type (TyVar s) = s - | string_of_fol_type (TyFree s) = s - | string_of_fol_type (TyConstr (tcon, tps)) = +fun string_of_fol_type (TyVar (s, _)) = s + | string_of_fol_type (TyFree (s, _)) = s + | string_of_fol_type (TyConstr ((tcon, _), tps)) = tcon ^ (paren_pack (map string_of_fol_type tps)); (*First string is the type class; the second is a TVar or TFfree*) @@ -230,19 +293,9 @@ exception CLAUSE of string * term; -fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a) - | atomic_type (TVar (v,_)) = TyVar(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 (TyConstr (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; +fun atomic_type (TFree (a,_)) = TyFree (`make_fixed_type_var a) + | atomic_type (TVar (x, _)) = + TyVar (make_schematic_type_var x, string_of_indexname x) (*Make literals for sorted type variables*) fun sorts_on_typs_aux (_, []) = [] @@ -402,9 +455,9 @@ (*** Find occurrences of functions in clauses ***) fun add_foltype_funcs (TyVar _, funcs) = funcs - | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs - | add_foltype_funcs (TyConstr (a, tys), funcs) = - List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; + | 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 diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 15 13:57:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 16 14:48:34 2010 +0200 @@ -33,11 +33,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 @@ -102,19 +102,22 @@ fun isTaut (HOLClause {literals,...}) = exists isTrue literals; fun type_of dfg (Type (a, Ts)) = - 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 (v, _)) = (TyVar (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)) = - 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 (v, _)) = TyVar (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) = @@ -193,7 +196,7 @@ (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) -fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2 +fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2 | result_type _ = raise Fail "Non-function type" fun type_of_combterm (CombConst (_, tp, _)) = tp @@ -452,7 +455,7 @@ (* 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 @@ -480,7 +483,7 @@ (* DFG format *) -fun write_dfg_file full_types file clauses = +fun write_dfg_file debug full_types file clauses = let val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 15 13:57:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 14:48:34 2010 +0200 @@ -8,6 +8,8 @@ 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 parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val hashw : word * word -> word @@ -26,6 +28,18 @@ | 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 "" + fun parse_bool_option option name s = (case s of "smart" => if option then NONE else raise Option