# HG changeset patch # User blanchet # Date 1277795956 -7200 # Node ID 3ee5683348137931cb200538fcaa176a8fec8fef # Parent 295f3a9b44b6cd682b76d81d319c219e26dce46c move "nice names" from Metis to TPTP format diff -r 295f3a9b44b6 -r 3ee568334813 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 09:05:37 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 09:19:16 2010 +0200 @@ -8,8 +8,8 @@ signature ATP_MANAGER = sig - type name_pool = Metis_Clauses.name_pool 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, diff -r 295f3a9b44b6 -r 3ee568334813 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 09:05:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 09:19:16 2010 +0200 @@ -9,7 +9,6 @@ signature METIS_CLAUSES = sig type name = string * string - type name_pool = string Symtab.table * string Symtab.table datatype kind = Axiom | Conjecture datatype type_literal = TyLitVar of string * name | @@ -59,9 +58,6 @@ val skolem_infix: string val is_skolem_const_name: string -> bool val num_type_args: theory -> string -> int - 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 val type_literals_for_types : typ list -> type_literal list val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list @@ -223,68 +219,9 @@ else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length -(**** name pool ****) - -type name = string * string -type name_pool = string Symtab.table * string Symtab.table - -fun empty_name_pool readable_names = - if readable_names then SOME (`I Symtab.empty) else NONE - -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs -fun pool_map f xs = - pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] - -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) +(**** Definitions and functions for FOL clauses for TPTP format output ****) -fun readable_name full_name s = - let - val s = s |> Long_Name.base_name |> Name.desymbolize false - val s' = s |> explode |> rev |> dropwhile (curry (op =) "'") - val s' = - (s' |> rev - |> implode - |> String.translate - (fn c => if Char.isAlphaNum c orelse 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' - (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous - ("op &", "op |", etc.). *) - val s' = if s' = "equal" orelse 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 (readable_name full_name desired_name) 0 - the_pool - |> apsnd SOME - -(**** Definitions and functions for FOL clauses for TPTP format output ****) +type name = string * string datatype kind = Axiom | Conjecture diff -r 295f3a9b44b6 -r 3ee568334813 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 09:05:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 09:19:16 2010 +0200 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig type minimize_command = string list -> string - type name_pool = Metis_Clauses.name_pool + type name_pool = Sledgehammer_TPTP_Format.name_pool val metis_line: bool -> int -> int -> string list -> string val metis_proof_text: @@ -31,6 +31,7 @@ open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter +open Sledgehammer_TPTP_Format type minimize_command = string list -> string diff -r 295f3a9b44b6 -r 3ee568334813 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 09:05:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 09:19:16 2010 +0200 @@ -7,14 +7,11 @@ signature SLEDGEHAMMER_TPTP_FORMAT = sig - type name_pool = Metis_Clauses.name_pool - type type_literal = Metis_Clauses.type_literal type classrel_clause = Metis_Clauses.classrel_clause type arity_clause = Metis_Clauses.arity_clause type hol_clause = Metis_Clauses.hol_clause + type name_pool = string Symtab.table * string Symtab.table - val tptp_of_type_literal : - bool -> type_literal -> name_pool option -> string * name_pool option val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list @@ -28,6 +25,65 @@ open Metis_Clauses open Sledgehammer_Util +type name_pool = string Symtab.table * string Symtab.table + +fun empty_name_pool readable_names = + if readable_names then SOME (`I Symtab.empty) else NONE + +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs +fun pool_map f xs = + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] + +fun translate_first_char f s = + String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE) +fun readable_name full_name s = + let + val s = s |> Long_Name.base_name |> Name.desymbolize false + val s' = s |> explode |> rev |> dropwhile (curry (op =) "'") + val s' = + (s' |> rev + |> implode + |> String.translate + (fn c => if Char.isAlphaNum c orelse 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' + (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous + ("op &", "op |", etc.). *) + val s' = if s' = "equal" orelse 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 => + let + val nice_prefix = readable_name full_name desired_name + fun add j = + 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 (j + 1) + | NONE => + (nice_name, + (Symtab.update_new (full_name, nice_name) (fst the_pool), + Symtab.update_new (nice_name, full_name) (snd the_pool))) + end + in add 0 |> apsnd SOME end + type const_info = {min_arity: int, max_arity: int, sub_level: bool} val clause_prefix = "cls_"