--- 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,
--- 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
--- 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
--- 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_"