more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 15:30:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 15:59:13 2010 +0200
@@ -22,7 +22,6 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
-open Sledgehammer_Proof_Reconstruct
open Sledgehammer_TPTP_Format
exception METIS of string * string
@@ -233,7 +232,7 @@
| NONE => make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix tconst_prefix x of
- SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
@@ -294,7 +293,7 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix tconst_prefix a of
SOME b =>
- Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 15:30:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 15:59:13 2010 +0200
@@ -19,6 +19,7 @@
val skolem_prefix: string
val skolem_infix: string
val is_skolem_const_name: string -> bool
+ val num_type_args: theory -> string -> int
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
val is_theorem_bad_for_atps: thm -> bool
@@ -98,6 +99,17 @@
Long_Name.base_name
#> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
fun rhs_extra_types lhsT rhs =
let val lhs_vars = Term.add_tfreesT lhsT []
fun add_new_TFrees (TFree v) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Jun 25 15:30:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Jun 25 15:59:13 2010 +0200
@@ -19,10 +19,10 @@
val tconst_prefix: string
val class_prefix: string
val union_all: ''a list list -> ''a list
- val const_trans_table: string Symtab.table
- val type_const_trans_table: string Symtab.table
+ val invert_const: string -> string
val ascii_of: string -> string
val undo_ascii_of: string -> string
+ val strip_prefix: string -> string -> string option
val make_schematic_var : string * int -> string
val make_fixed_var : string -> string
val make_schematic_type_var : string * int -> string
@@ -88,11 +88,16 @@
(@{const_name COMBS}, "COMBS"),
(@{const_name True}, "True"),
(@{const_name False}, "False"),
- (@{const_name If}, "If")]
+ (@{const_name If}, "If"),
+ (@{type_name "*"}, "prod"),
+ (@{type_name "+"}, "sum")]
-val type_const_trans_table =
- Symtab.make [(@{type_name "*"}, "prod"),
- (@{type_name "+"}, "sum")]
+(* Invert the table of translations between Isabelle and ATPs. *)
+val const_trans_table_inv =
+ Symtab.update ("fequal", @{const_name "op ="})
+ (Symtab.make (map swap (Symtab.dest const_trans_table)))
+
+val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
@@ -137,6 +142,14 @@
val undo_ascii_of = undo_ascii_aux [] o String.explode;
+(* If string s has the prefix s1, return the result of deleting it,
+ un-ASCII'd. *)
+fun strip_prefix s1 s =
+ if String.isPrefix s1 s then
+ SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
+ else
+ NONE
+
(*Remove the initial ' character from a type variable, if it is present*)
fun trim_type_var s =
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
@@ -157,16 +170,11 @@
SOME c' => c'
| NONE => ascii_of c
-fun lookup_type_const c =
- case Symtab.lookup type_const_trans_table c of
- SOME c' => c'
- | NONE => ascii_of c
-
(* "op =" MUST BE "equal" because it's built into ATPs. *)
fun make_fixed_const @{const_name "op ="} = "equal"
| make_fixed_const c = const_prefix ^ lookup_const c
-fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
+fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
fun make_type_class clas = class_prefix ^ ascii_of clas;
@@ -323,10 +331,10 @@
arity_clause seen n (tcons,ars)
| arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
arity_clause seen (n+1) (tcons,ars)
else
- make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
+ make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
arity_clause (class::seen) n (tcons,ars)
fun multi_arity_clause [] = []
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 25 15:30:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 25 15:59:13 2010 +0200
@@ -10,10 +10,6 @@
type minimize_command = string list -> string
type name_pool = Sledgehammer_FOL_Clause.name_pool
- val invert_const: string -> string
- val invert_type_const: string -> string
- val num_type_args: theory -> string -> int
- val strip_prefix: string -> string -> string option
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
@@ -212,28 +208,13 @@
exception NODE of node list
-(*If string s has the prefix s1, return the result of deleting it.*)
-fun strip_prefix s1 s =
- if String.isPrefix s1 s
- then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
- else NONE;
-
-(*Invert the table of translations between Isabelle and ATPs*)
-val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest type_const_trans_table));
-
-fun invert_type_const c =
- case Symtab.lookup type_const_trans_table_inv c of
- SOME c' => c'
- | NONE => c;
-
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
| type_from_node tfrees (u as StrNode (a, us)) =
let val Ts = map (type_from_node tfrees) us in
case strip_prefix tconst_prefix a of
- SOME b => Type (invert_type_const b, Ts)
+ SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise NODE [u] (* only "tconst"s have type arguments *)
@@ -250,24 +231,6 @@
Type_Infer.param 0 (a, HOLogic.typeS)
end
-(*Invert the table of translations between Isabelle and ATPs*)
-val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name "op ="})
- (Symtab.make (map swap (Symtab.dest const_trans_table)))
-
-fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_theory_name s then
- s |> unprefix skolem_theory_name
- |> space_explode skolem_infix |> hd
- |> space_explode "_" |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
fun fix_atp_variable_name s =
let
fun subscript_name s n = s ^ nat_subscript n