# HG changeset patch
# User blanchet
# Date 1277474353 -7200
# Node ID a899f9506f39b66b8176c2f44a209a42b5c17b93
# Parent  76e23303c7ffa4b7058caa3ca33bac2ce0191e25
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe

diff -r 76e23303c7ff -r a899f9506f39 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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)
diff -r 76e23303c7ff -r a899f9506f39 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- 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) =
diff -r 76e23303c7ff -r a899f9506f39 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- 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 [] = []
diff -r 76e23303c7ff -r a899f9506f39 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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