rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
authorblanchet
Thu Sep 16 16:12:02 2010 +0200 (2010-09-16)
changeset 39494bf7dd4902321
parent 39493 cb2208f2c07d
child 39495 bb4fb9ffe2d1
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 16 15:38:46 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 16 16:12:02 2010 +0200
     1.3 @@ -316,7 +316,7 @@
     1.4    Tools/semiring_normalizer.ML \
     1.5    Tools/Sledgehammer/clausifier.ML \
     1.6    Tools/Sledgehammer/meson_tactic.ML \
     1.7 -  Tools/Sledgehammer/metis_clauses.ML \
     1.8 +  Tools/Sledgehammer/metis_translate.ML \
     1.9    Tools/Sledgehammer/metis_tactics.ML \
    1.10    Tools/Sledgehammer/sledgehammer.ML \
    1.11    Tools/Sledgehammer/sledgehammer_filter.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 16 15:38:46 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 16 16:12:02 2010 +0200
     2.3 @@ -434,7 +434,7 @@
     2.4  
     2.5  fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
     2.6    let
     2.7 -    open Metis_Clauses
     2.8 +    open Metis_Translate
     2.9      val thy = Proof.theory_of st
    2.10      val n0 = length (these (!named_thms))
    2.11      val (prover_name, _) = get_atp thy args
     3.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 16 15:38:46 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 16:12:02 2010 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4    ("~~/src/Tools/Metis/metis.ML")
     3.5    ("Tools/Sledgehammer/clausifier.ML")
     3.6    ("Tools/Sledgehammer/meson_tactic.ML")
     3.7 -  ("Tools/Sledgehammer/metis_clauses.ML")
     3.8 +  ("Tools/Sledgehammer/metis_translate.ML")
     3.9    ("Tools/Sledgehammer/metis_tactics.ML")
    3.10    ("Tools/Sledgehammer/sledgehammer_util.ML")
    3.11    ("Tools/Sledgehammer/sledgehammer_filter.ML")
    3.12 @@ -102,7 +102,7 @@
    3.13  use "Tools/Sledgehammer/meson_tactic.ML"
    3.14  setup Meson_Tactic.setup
    3.15  
    3.16 -use "Tools/Sledgehammer/metis_clauses.ML"
    3.17 +use "Tools/Sledgehammer/metis_translate.ML"
    3.18  use "Tools/Sledgehammer/metis_tactics.ML"
    3.19  setup Metis_Tactics.setup
    3.20  
     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Sep 16 15:38:46 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,524 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/metis_clauses.ML
     4.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.6 -    Author:     Jasmin Blanchette, TU Muenchen
     4.7 -
     4.8 -Storing/printing FOL clauses and arity clauses.  Typed equality is
     4.9 -treated differently.
    4.10 -*)
    4.11 -
    4.12 -signature METIS_CLAUSES =
    4.13 -sig
    4.14 -  type name = string * string
    4.15 -  datatype type_literal =
    4.16 -    TyLitVar of name * name |
    4.17 -    TyLitFree of name * name
    4.18 -  datatype arLit =
    4.19 -    TConsLit of name * name * name list |
    4.20 -    TVarLit of name * name
    4.21 -  datatype arity_clause =
    4.22 -    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
    4.23 -  datatype class_rel_clause =
    4.24 -    ClassRelClause of {name: string, subclass: name, superclass: name}
    4.25 -  datatype combtyp =
    4.26 -    CombTVar of name |
    4.27 -    CombTFree of name |
    4.28 -    CombType of name * combtyp list
    4.29 -  datatype combterm =
    4.30 -    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    4.31 -    CombVar of name * combtyp |
    4.32 -    CombApp of combterm * combterm
    4.33 -  datatype fol_literal = FOLLiteral of bool * combterm
    4.34 -
    4.35 -  val type_wrapper_name : string
    4.36 -  val bound_var_prefix : string
    4.37 -  val schematic_var_prefix: string
    4.38 -  val fixed_var_prefix: string
    4.39 -  val tvar_prefix: string
    4.40 -  val tfree_prefix: string
    4.41 -  val const_prefix: string
    4.42 -  val type_const_prefix: string
    4.43 -  val class_prefix: string
    4.44 -  val invert_const: string -> string
    4.45 -  val ascii_of: string -> string
    4.46 -  val unascii_of: string -> string
    4.47 -  val strip_prefix_and_unascii: string -> string -> string option
    4.48 -  val make_bound_var : string -> string
    4.49 -  val make_schematic_var : string * int -> string
    4.50 -  val make_fixed_var : string -> string
    4.51 -  val make_schematic_type_var : string * int -> string
    4.52 -  val make_fixed_type_var : string -> string
    4.53 -  val make_fixed_const : string -> string
    4.54 -  val make_fixed_type_const : string -> string
    4.55 -  val make_type_class : string -> string
    4.56 -  val skolem_theory_name: string
    4.57 -  val skolem_prefix: string
    4.58 -  val skolem_infix: string
    4.59 -  val is_skolem_const_name: string -> bool
    4.60 -  val num_type_args: theory -> string -> int
    4.61 -  val type_literals_for_types : typ list -> type_literal list
    4.62 -  val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
    4.63 -  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    4.64 -  val combtyp_of : combterm -> combtyp
    4.65 -  val strip_combterm_comb : combterm -> combterm * combterm list
    4.66 -  val combterm_from_term :
    4.67 -    theory -> (string * typ) list -> term -> combterm * typ list
    4.68 -  val literals_of_term : theory -> term -> fol_literal list * typ list
    4.69 -  val conceal_skolem_terms :
    4.70 -    int -> (string * term) list -> term -> (string * term) list * term
    4.71 -  val reveal_skolem_terms : (string * term) list -> term -> term
    4.72 -  val tfree_classes_of_terms : term list -> string list
    4.73 -  val tvar_classes_of_terms : term list -> string list
    4.74 -  val type_consts_of_terms : theory -> term list -> string list
    4.75 -end
    4.76 -
    4.77 -structure Metis_Clauses : METIS_CLAUSES =
    4.78 -struct
    4.79 -
    4.80 -val type_wrapper_name = "ti"
    4.81 -
    4.82 -val bound_var_prefix = "B_"
    4.83 -val schematic_var_prefix = "V_"
    4.84 -val fixed_var_prefix = "v_"
    4.85 -
    4.86 -val tvar_prefix = "T_";
    4.87 -val tfree_prefix = "t_";
    4.88 -
    4.89 -val const_prefix = "c_";
    4.90 -val type_const_prefix = "tc_";
    4.91 -val class_prefix = "class_";
    4.92 -
    4.93 -fun union_all xss = fold (union (op =)) xss []
    4.94 -
    4.95 -(* Readable names for the more common symbolic functions. Do not mess with the
    4.96 -   last nine entries of the table unless you know what you are doing. *)
    4.97 -val const_trans_table =
    4.98 -  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
    4.99 -               (@{type_name Sum_Type.sum}, "sum"),
   4.100 -               (@{const_name HOL.eq}, "equal"),
   4.101 -               (@{const_name HOL.conj}, "and"),
   4.102 -               (@{const_name HOL.disj}, "or"),
   4.103 -               (@{const_name HOL.implies}, "implies"),
   4.104 -               (@{const_name Set.member}, "member"),
   4.105 -               (@{const_name fequal}, "fequal"),
   4.106 -               (@{const_name COMBI}, "COMBI"),
   4.107 -               (@{const_name COMBK}, "COMBK"),
   4.108 -               (@{const_name COMBB}, "COMBB"),
   4.109 -               (@{const_name COMBC}, "COMBC"),
   4.110 -               (@{const_name COMBS}, "COMBS"),
   4.111 -               (@{const_name True}, "True"),
   4.112 -               (@{const_name False}, "False"),
   4.113 -               (@{const_name If}, "If")]
   4.114 -
   4.115 -(* Invert the table of translations between Isabelle and ATPs. *)
   4.116 -val const_trans_table_inv =
   4.117 -  Symtab.update ("fequal", @{const_name HOL.eq})
   4.118 -                (Symtab.make (map swap (Symtab.dest const_trans_table)))
   4.119 -
   4.120 -val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   4.121 -
   4.122 -(*Escaping of special characters.
   4.123 -  Alphanumeric characters are left unchanged.
   4.124 -  The character _ goes to __
   4.125 -  Characters in the range ASCII space to / go to _A to _P, respectively.
   4.126 -  Other characters go to _nnn where nnn is the decimal ASCII code.*)
   4.127 -val A_minus_space = Char.ord #"A" - Char.ord #" ";
   4.128 -
   4.129 -fun stringN_of_int 0 _ = ""
   4.130 -  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   4.131 -
   4.132 -fun ascii_of_c c =
   4.133 -  if Char.isAlphaNum c then String.str c
   4.134 -  else if c = #"_" then "__"
   4.135 -  else if #" " <= c andalso c <= #"/"
   4.136 -       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   4.137 -  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   4.138 -
   4.139 -val ascii_of = String.translate ascii_of_c;
   4.140 -
   4.141 -(** Remove ASCII armouring from names in proof files **)
   4.142 -
   4.143 -(*We don't raise error exceptions because this code can run inside the watcher.
   4.144 -  Also, the errors are "impossible" (hah!)*)
   4.145 -fun unascii_aux rcs [] = String.implode(rev rcs)
   4.146 -  | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) []  (*ERROR*)
   4.147 -      (*Three types of _ escapes: __, _A to _P, _nnn*)
   4.148 -  | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
   4.149 -  | unascii_aux rcs (#"_" :: c :: cs) =
   4.150 -      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   4.151 -      then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   4.152 -      else
   4.153 -        let val digits = List.take (c::cs, 3) handle Subscript => []
   4.154 -        in
   4.155 -            case Int.fromString (String.implode digits) of
   4.156 -                NONE => unascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   4.157 -              | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   4.158 -        end
   4.159 -  | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
   4.160 -val unascii_of = unascii_aux [] o String.explode
   4.161 -
   4.162 -(* If string s has the prefix s1, return the result of deleting it,
   4.163 -   un-ASCII'd. *)
   4.164 -fun strip_prefix_and_unascii s1 s =
   4.165 -  if String.isPrefix s1 s then
   4.166 -    SOME (unascii_of (String.extract (s, size s1, NONE)))
   4.167 -  else
   4.168 -    NONE
   4.169 -
   4.170 -(*Remove the initial ' character from a type variable, if it is present*)
   4.171 -fun trim_type_var s =
   4.172 -  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   4.173 -  else error ("trim_type: Malformed type variable encountered: " ^ s);
   4.174 -
   4.175 -fun ascii_of_indexname (v,0) = ascii_of v
   4.176 -  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   4.177 -
   4.178 -fun make_bound_var x = bound_var_prefix ^ ascii_of x
   4.179 -fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   4.180 -fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   4.181 -
   4.182 -fun make_schematic_type_var (x,i) =
   4.183 -      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   4.184 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   4.185 -
   4.186 -fun lookup_const c =
   4.187 -  case Symtab.lookup const_trans_table c of
   4.188 -    SOME c' => c'
   4.189 -  | NONE => ascii_of c
   4.190 -
   4.191 -(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
   4.192 -fun make_fixed_const @{const_name HOL.eq} = "equal"
   4.193 -  | make_fixed_const c = const_prefix ^ lookup_const c
   4.194 -
   4.195 -fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   4.196 -
   4.197 -fun make_type_class clas = class_prefix ^ ascii_of clas;
   4.198 -
   4.199 -val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
   4.200 -val skolem_prefix = "sko_"
   4.201 -val skolem_infix = "$"
   4.202 -
   4.203 -(* Hack: Could return false positives (e.g., a user happens to declare a
   4.204 -   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
   4.205 -val is_skolem_const_name =
   4.206 -  Long_Name.base_name
   4.207 -  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
   4.208 -
   4.209 -(* The number of type arguments of a constant, zero if it's monomorphic. For
   4.210 -   (instances of) Skolem pseudoconstants, this information is encoded in the
   4.211 -   constant name. *)
   4.212 -fun num_type_args thy s =
   4.213 -  if String.isPrefix skolem_theory_name s then
   4.214 -    s |> unprefix skolem_theory_name
   4.215 -      |> space_explode skolem_infix |> hd
   4.216 -      |> space_explode "_" |> List.last |> Int.fromString |> the
   4.217 -  else
   4.218 -    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   4.219 -
   4.220 -(**** Definitions and functions for FOL clauses for TPTP format output ****)
   4.221 -
   4.222 -type name = string * string
   4.223 -
   4.224 -(**** Isabelle FOL clauses ****)
   4.225 -
   4.226 -(* The first component is the type class; the second is a TVar or TFree. *)
   4.227 -datatype type_literal =
   4.228 -  TyLitVar of name * name |
   4.229 -  TyLitFree of name * name
   4.230 -
   4.231 -exception CLAUSE of string * term;
   4.232 -
   4.233 -(*Make literals for sorted type variables*)
   4.234 -fun sorts_on_typs_aux (_, [])   = []
   4.235 -  | sorts_on_typs_aux ((x,i),  s::ss) =
   4.236 -      let val sorts = sorts_on_typs_aux ((x,i), ss)
   4.237 -      in
   4.238 -          if s = "HOL.type" then sorts
   4.239 -          else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
   4.240 -          else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
   4.241 -      end;
   4.242 -
   4.243 -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   4.244 -  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   4.245 -
   4.246 -(*Given a list of sorted type variables, return a list of type literals.*)
   4.247 -fun type_literals_for_types Ts =
   4.248 -  fold (union (op =)) (map sorts_on_typs Ts) []
   4.249 -
   4.250 -(** make axiom and conjecture clauses. **)
   4.251 -
   4.252 -(**** Isabelle arities ****)
   4.253 -
   4.254 -datatype arLit =
   4.255 -  TConsLit of name * name * name list |
   4.256 -  TVarLit of name * name
   4.257 -
   4.258 -datatype arity_clause =
   4.259 -  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   4.260 -
   4.261 -
   4.262 -fun gen_TVars 0 = []
   4.263 -  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   4.264 -
   4.265 -fun pack_sort(_,[])  = []
   4.266 -  | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
   4.267 -  | pack_sort(tvar, cls::srt) =
   4.268 -    (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
   4.269 -
   4.270 -(*Arity of type constructor tcon :: (arg1,...,argN)res*)
   4.271 -fun make_axiom_arity_clause (tcons, name, (cls,args)) =
   4.272 -  let
   4.273 -    val tvars = gen_TVars (length args)
   4.274 -    val tvars_srts = ListPair.zip (tvars, args)
   4.275 -  in
   4.276 -    ArityClause {name = name,
   4.277 -                 conclLit = TConsLit (`make_type_class cls,
   4.278 -                                      `make_fixed_type_const tcons,
   4.279 -                                      tvars ~~ tvars),
   4.280 -                 premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
   4.281 -  end
   4.282 -
   4.283 -
   4.284 -(**** Isabelle class relations ****)
   4.285 -
   4.286 -datatype class_rel_clause =
   4.287 -  ClassRelClause of {name: string, subclass: name, superclass: name}
   4.288 -
   4.289 -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   4.290 -fun class_pairs _ [] _ = []
   4.291 -  | class_pairs thy subs supers =
   4.292 -      let
   4.293 -        val class_less = Sorts.class_less (Sign.classes_of thy)
   4.294 -        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   4.295 -        fun add_supers sub = fold (add_super sub) supers
   4.296 -      in fold add_supers subs [] end
   4.297 -
   4.298 -fun make_class_rel_clause (sub,super) =
   4.299 -  ClassRelClause {name = sub ^ "_" ^ super,
   4.300 -                  subclass = `make_type_class sub,
   4.301 -                  superclass = `make_type_class super}
   4.302 -
   4.303 -fun make_class_rel_clauses thy subs supers =
   4.304 -  map make_class_rel_clause (class_pairs thy subs supers);
   4.305 -
   4.306 -
   4.307 -(** Isabelle arities **)
   4.308 -
   4.309 -fun arity_clause _ _ (_, []) = []
   4.310 -  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   4.311 -      arity_clause seen n (tcons,ars)
   4.312 -  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   4.313 -      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   4.314 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   4.315 -          arity_clause seen (n+1) (tcons,ars)
   4.316 -      else
   4.317 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
   4.318 -          arity_clause (class::seen) n (tcons,ars)
   4.319 -
   4.320 -fun multi_arity_clause [] = []
   4.321 -  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   4.322 -      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   4.323 -
   4.324 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   4.325 -  provided its arguments have the corresponding sorts.*)
   4.326 -fun type_class_pairs thy tycons classes =
   4.327 -  let val alg = Sign.classes_of thy
   4.328 -      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   4.329 -      fun add_class tycon class =
   4.330 -        cons (class, domain_sorts tycon class)
   4.331 -        handle Sorts.CLASS_ERROR _ => I
   4.332 -      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   4.333 -  in  map try_classes tycons  end;
   4.334 -
   4.335 -(*Proving one (tycon, class) membership may require proving others, so iterate.*)
   4.336 -fun iter_type_class_pairs _ _ [] = ([], [])
   4.337 -  | iter_type_class_pairs thy tycons classes =
   4.338 -      let val cpairs = type_class_pairs thy tycons classes
   4.339 -          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   4.340 -            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   4.341 -          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   4.342 -      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   4.343 -
   4.344 -fun make_arity_clauses thy tycons classes =
   4.345 -  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   4.346 -  in  (classes', multi_arity_clause cpairs)  end;
   4.347 -
   4.348 -datatype combtyp =
   4.349 -  CombTVar of name |
   4.350 -  CombTFree of name |
   4.351 -  CombType of name * combtyp list
   4.352 -
   4.353 -datatype combterm =
   4.354 -  CombConst of name * combtyp * combtyp list (* Const and Free *) |
   4.355 -  CombVar of name * combtyp |
   4.356 -  CombApp of combterm * combterm
   4.357 -
   4.358 -datatype fol_literal = FOLLiteral of bool * combterm
   4.359 -
   4.360 -(*********************************************************************)
   4.361 -(* convert a clause with type Term.term to a clause with type clause *)
   4.362 -(*********************************************************************)
   4.363 -
   4.364 -(*Result of a function type; no need to check that the argument type matches.*)
   4.365 -fun result_type (CombType (_, [_, tp2])) = tp2
   4.366 -  | result_type _ = raise Fail "non-function type"
   4.367 -
   4.368 -fun combtyp_of (CombConst (_, tp, _)) = tp
   4.369 -  | combtyp_of (CombVar (_, tp)) = tp
   4.370 -  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
   4.371 -
   4.372 -(*gets the head of a combinator application, along with the list of arguments*)
   4.373 -fun strip_combterm_comb u =
   4.374 -    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   4.375 -        |   stripc  x =  x
   4.376 -    in stripc(u,[]) end
   4.377 -
   4.378 -fun type_of (Type (a, Ts)) =
   4.379 -    let val (folTypes,ts) = types_of Ts in
   4.380 -      (CombType (`make_fixed_type_const a, folTypes), ts)
   4.381 -    end
   4.382 -  | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
   4.383 -  | type_of (tp as TVar (x, _)) =
   4.384 -    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
   4.385 -and types_of Ts =
   4.386 -    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   4.387 -      (folTyps, union_all ts)
   4.388 -    end
   4.389 -
   4.390 -(* same as above, but no gathering of sort information *)
   4.391 -fun simp_type_of (Type (a, Ts)) =
   4.392 -      CombType (`make_fixed_type_const a, map simp_type_of Ts)
   4.393 -  | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
   4.394 -  | simp_type_of (TVar (x, _)) =
   4.395 -    CombTVar (make_schematic_type_var x, string_of_indexname x)
   4.396 -
   4.397 -(* Converts a term (with combinators) into a combterm. Also accummulates sort
   4.398 -   infomation. *)
   4.399 -fun combterm_from_term thy bs (P $ Q) =
   4.400 -      let val (P', tsP) = combterm_from_term thy bs P
   4.401 -          val (Q', tsQ) = combterm_from_term thy bs Q
   4.402 -      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   4.403 -  | combterm_from_term thy _ (Const (c, T)) =
   4.404 -      let
   4.405 -        val (tp, ts) = type_of T
   4.406 -        val tvar_list =
   4.407 -          (if String.isPrefix skolem_theory_name c then
   4.408 -             [] |> Term.add_tvarsT T |> map TVar
   4.409 -           else
   4.410 -             (c, T) |> Sign.const_typargs thy)
   4.411 -          |> map simp_type_of
   4.412 -        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   4.413 -      in  (c',ts)  end
   4.414 -  | combterm_from_term _ _ (Free (v, T)) =
   4.415 -      let val (tp,ts) = type_of T
   4.416 -          val v' = CombConst (`make_fixed_var v, tp, [])
   4.417 -      in  (v',ts)  end
   4.418 -  | combterm_from_term _ _ (Var (v, T)) =
   4.419 -      let val (tp,ts) = type_of T
   4.420 -          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   4.421 -      in  (v',ts)  end
   4.422 -  | combterm_from_term _ bs (Bound j) =
   4.423 -      let
   4.424 -        val (s, T) = nth bs j
   4.425 -        val (tp, ts) = type_of T
   4.426 -        val v' = CombConst (`make_bound_var s, tp, [])
   4.427 -      in (v', ts) end
   4.428 -  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   4.429 -
   4.430 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   4.431 -  | predicate_of thy (t, pos) =
   4.432 -    (combterm_from_term thy [] (Envir.eta_contract t), pos)
   4.433 -
   4.434 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   4.435 -    literals_of_term1 args thy P
   4.436 -  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
   4.437 -    literals_of_term1 (literals_of_term1 args thy P) thy Q
   4.438 -  | literals_of_term1 (lits, ts) thy P =
   4.439 -    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   4.440 -      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
   4.441 -    end
   4.442 -val literals_of_term = literals_of_term1 ([], [])
   4.443 -
   4.444 -fun skolem_name i j num_T_args =
   4.445 -  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   4.446 -  skolem_infix ^ "g"
   4.447 -
   4.448 -fun conceal_skolem_terms i skolems t =
   4.449 -  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
   4.450 -    let
   4.451 -      fun aux skolems
   4.452 -              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
   4.453 -          let
   4.454 -            val (skolems, s) =
   4.455 -              if i = ~1 then
   4.456 -                (skolems, @{const_name undefined})
   4.457 -              else case AList.find (op aconv) skolems t of
   4.458 -                s :: _ => (skolems, s)
   4.459 -              | [] =>
   4.460 -                let
   4.461 -                  val s = skolem_theory_name ^ "." ^
   4.462 -                          skolem_name i (length skolems)
   4.463 -                                        (length (Term.add_tvarsT T []))
   4.464 -                in ((s, t) :: skolems, s) end
   4.465 -          in (skolems, Const (s, T)) end
   4.466 -        | aux skolems (t1 $ t2) =
   4.467 -          let
   4.468 -            val (skolems, t1) = aux skolems t1
   4.469 -            val (skolems, t2) = aux skolems t2
   4.470 -          in (skolems, t1 $ t2) end
   4.471 -        | aux skolems (Abs (s, T, t')) =
   4.472 -          let val (skolems, t') = aux skolems t' in
   4.473 -            (skolems, Abs (s, T, t'))
   4.474 -          end
   4.475 -        | aux skolems t = (skolems, t)
   4.476 -    in aux skolems t end
   4.477 -  else
   4.478 -    (skolems, t)
   4.479 -
   4.480 -fun reveal_skolem_terms skolems =
   4.481 -  map_aterms (fn t as Const (s, _) =>
   4.482 -                 if String.isPrefix skolem_theory_name s then
   4.483 -                   AList.lookup (op =) skolems s |> the
   4.484 -                   |> map_types Type_Infer.paramify_vars
   4.485 -                 else
   4.486 -                   t
   4.487 -               | t => t)
   4.488 -
   4.489 -
   4.490 -(***************************************************************)
   4.491 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
   4.492 -(***************************************************************)
   4.493 -
   4.494 -fun set_insert (x, s) = Symtab.update (x, ()) s
   4.495 -
   4.496 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   4.497 -
   4.498 -(*Remove this trivial type class*)
   4.499 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   4.500 -
   4.501 -fun tfree_classes_of_terms ts =
   4.502 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   4.503 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   4.504 -
   4.505 -fun tvar_classes_of_terms ts =
   4.506 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   4.507 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   4.508 -
   4.509 -(*fold type constructors*)
   4.510 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   4.511 -  | fold_type_consts _ _ x = x;
   4.512 -
   4.513 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   4.514 -fun add_type_consts_in_term thy =
   4.515 -  let
   4.516 -    fun aux (Const x) =
   4.517 -        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
   4.518 -      | aux (Abs (_, _, u)) = aux u
   4.519 -      | aux (Const (@{const_name skolem}, _) $ _) = I
   4.520 -      | aux (t $ u) = aux t #> aux u
   4.521 -      | aux _ = I
   4.522 -  in aux end
   4.523 -
   4.524 -fun type_consts_of_terms thy ts =
   4.525 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   4.526 -
   4.527 -end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 16 15:38:46 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 16 16:12:02 2010 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  structure Metis_Tactics : METIS_TACTICS =
     5.5  struct
     5.6  
     5.7 -open Metis_Clauses
     5.8 +open Metis_Translate
     5.9  
    5.10  val trace = Unsynchronized.ref false;
    5.11  fun trace_msg msg = if !trace then tracing (msg ()) else ();
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Thu Sep 16 16:12:02 2010 +0200
     6.3 @@ -0,0 +1,521 @@
     6.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_translate.ML
     6.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     6.6 +    Author:     Jasmin Blanchette, TU Muenchen
     6.7 +
     6.8 +Translation of HOL to FOL for Metis.
     6.9 +*)
    6.10 +
    6.11 +signature METIS_TRANSLATE =
    6.12 +sig
    6.13 +  type name = string * string
    6.14 +  datatype type_literal =
    6.15 +    TyLitVar of name * name |
    6.16 +    TyLitFree of name * name
    6.17 +  datatype arLit =
    6.18 +    TConsLit of name * name * name list |
    6.19 +    TVarLit of name * name
    6.20 +  datatype arity_clause =
    6.21 +    ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
    6.22 +  datatype class_rel_clause =
    6.23 +    ClassRelClause of {name: string, subclass: name, superclass: name}
    6.24 +  datatype combtyp =
    6.25 +    CombTVar of name |
    6.26 +    CombTFree of name |
    6.27 +    CombType of name * combtyp list
    6.28 +  datatype combterm =
    6.29 +    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    6.30 +    CombVar of name * combtyp |
    6.31 +    CombApp of combterm * combterm
    6.32 +  datatype fol_literal = FOLLiteral of bool * combterm
    6.33 +
    6.34 +  val type_wrapper_name : string
    6.35 +  val bound_var_prefix : string
    6.36 +  val schematic_var_prefix: string
    6.37 +  val fixed_var_prefix: string
    6.38 +  val tvar_prefix: string
    6.39 +  val tfree_prefix: string
    6.40 +  val const_prefix: string
    6.41 +  val type_const_prefix: string
    6.42 +  val class_prefix: string
    6.43 +  val invert_const: string -> string
    6.44 +  val ascii_of: string -> string
    6.45 +  val unascii_of: string -> string
    6.46 +  val strip_prefix_and_unascii: string -> string -> string option
    6.47 +  val make_bound_var : string -> string
    6.48 +  val make_schematic_var : string * int -> string
    6.49 +  val make_fixed_var : string -> string
    6.50 +  val make_schematic_type_var : string * int -> string
    6.51 +  val make_fixed_type_var : string -> string
    6.52 +  val make_fixed_const : string -> string
    6.53 +  val make_fixed_type_const : string -> string
    6.54 +  val make_type_class : string -> string
    6.55 +  val skolem_theory_name: string
    6.56 +  val skolem_prefix: string
    6.57 +  val skolem_infix: string
    6.58 +  val is_skolem_const_name: string -> bool
    6.59 +  val num_type_args: theory -> string -> int
    6.60 +  val type_literals_for_types : typ list -> type_literal list
    6.61 +  val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
    6.62 +  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    6.63 +  val combtyp_of : combterm -> combtyp
    6.64 +  val strip_combterm_comb : combterm -> combterm * combterm list
    6.65 +  val combterm_from_term :
    6.66 +    theory -> (string * typ) list -> term -> combterm * typ list
    6.67 +  val literals_of_term : theory -> term -> fol_literal list * typ list
    6.68 +  val conceal_skolem_terms :
    6.69 +    int -> (string * term) list -> term -> (string * term) list * term
    6.70 +  val reveal_skolem_terms : (string * term) list -> term -> term
    6.71 +  val tfree_classes_of_terms : term list -> string list
    6.72 +  val tvar_classes_of_terms : term list -> string list
    6.73 +  val type_consts_of_terms : theory -> term list -> string list
    6.74 +end
    6.75 +
    6.76 +structure Metis_Translate : METIS_TRANSLATE =
    6.77 +struct
    6.78 +
    6.79 +val type_wrapper_name = "ti"
    6.80 +
    6.81 +val bound_var_prefix = "B_"
    6.82 +val schematic_var_prefix = "V_"
    6.83 +val fixed_var_prefix = "v_"
    6.84 +
    6.85 +val tvar_prefix = "T_";
    6.86 +val tfree_prefix = "t_";
    6.87 +
    6.88 +val const_prefix = "c_";
    6.89 +val type_const_prefix = "tc_";
    6.90 +val class_prefix = "class_";
    6.91 +
    6.92 +fun union_all xss = fold (union (op =)) xss []
    6.93 +
    6.94 +(* Readable names for the more common symbolic functions. Do not mess with the
    6.95 +   last nine entries of the table unless you know what you are doing. *)
    6.96 +val const_trans_table =
    6.97 +  Symtab.make [(@{type_name Product_Type.prod}, "prod"),
    6.98 +               (@{type_name Sum_Type.sum}, "sum"),
    6.99 +               (@{const_name HOL.eq}, "equal"),
   6.100 +               (@{const_name HOL.conj}, "and"),
   6.101 +               (@{const_name HOL.disj}, "or"),
   6.102 +               (@{const_name HOL.implies}, "implies"),
   6.103 +               (@{const_name Set.member}, "member"),
   6.104 +               (@{const_name fequal}, "fequal"),
   6.105 +               (@{const_name COMBI}, "COMBI"),
   6.106 +               (@{const_name COMBK}, "COMBK"),
   6.107 +               (@{const_name COMBB}, "COMBB"),
   6.108 +               (@{const_name COMBC}, "COMBC"),
   6.109 +               (@{const_name COMBS}, "COMBS"),
   6.110 +               (@{const_name True}, "True"),
   6.111 +               (@{const_name False}, "False"),
   6.112 +               (@{const_name If}, "If")]
   6.113 +
   6.114 +(* Invert the table of translations between Isabelle and ATPs. *)
   6.115 +val const_trans_table_inv =
   6.116 +  Symtab.update ("fequal", @{const_name HOL.eq})
   6.117 +                (Symtab.make (map swap (Symtab.dest const_trans_table)))
   6.118 +
   6.119 +val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   6.120 +
   6.121 +(*Escaping of special characters.
   6.122 +  Alphanumeric characters are left unchanged.
   6.123 +  The character _ goes to __
   6.124 +  Characters in the range ASCII space to / go to _A to _P, respectively.
   6.125 +  Other characters go to _nnn where nnn is the decimal ASCII code.*)
   6.126 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
   6.127 +
   6.128 +fun stringN_of_int 0 _ = ""
   6.129 +  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   6.130 +
   6.131 +fun ascii_of_c c =
   6.132 +  if Char.isAlphaNum c then String.str c
   6.133 +  else if c = #"_" then "__"
   6.134 +  else if #" " <= c andalso c <= #"/"
   6.135 +       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   6.136 +  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   6.137 +
   6.138 +val ascii_of = String.translate ascii_of_c;
   6.139 +
   6.140 +(** Remove ASCII armouring from names in proof files **)
   6.141 +
   6.142 +(*We don't raise error exceptions because this code can run inside the watcher.
   6.143 +  Also, the errors are "impossible" (hah!)*)
   6.144 +fun unascii_aux rcs [] = String.implode(rev rcs)
   6.145 +  | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) []  (*ERROR*)
   6.146 +      (*Three types of _ escapes: __, _A to _P, _nnn*)
   6.147 +  | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
   6.148 +  | unascii_aux rcs (#"_" :: c :: cs) =
   6.149 +      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   6.150 +      then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   6.151 +      else
   6.152 +        let val digits = List.take (c::cs, 3) handle Subscript => []
   6.153 +        in
   6.154 +            case Int.fromString (String.implode digits) of
   6.155 +                NONE => unascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   6.156 +              | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   6.157 +        end
   6.158 +  | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
   6.159 +val unascii_of = unascii_aux [] o String.explode
   6.160 +
   6.161 +(* If string s has the prefix s1, return the result of deleting it,
   6.162 +   un-ASCII'd. *)
   6.163 +fun strip_prefix_and_unascii s1 s =
   6.164 +  if String.isPrefix s1 s then
   6.165 +    SOME (unascii_of (String.extract (s, size s1, NONE)))
   6.166 +  else
   6.167 +    NONE
   6.168 +
   6.169 +(*Remove the initial ' character from a type variable, if it is present*)
   6.170 +fun trim_type_var s =
   6.171 +  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   6.172 +  else error ("trim_type: Malformed type variable encountered: " ^ s);
   6.173 +
   6.174 +fun ascii_of_indexname (v,0) = ascii_of v
   6.175 +  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   6.176 +
   6.177 +fun make_bound_var x = bound_var_prefix ^ ascii_of x
   6.178 +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   6.179 +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   6.180 +
   6.181 +fun make_schematic_type_var (x,i) =
   6.182 +      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   6.183 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   6.184 +
   6.185 +fun lookup_const c =
   6.186 +  case Symtab.lookup const_trans_table c of
   6.187 +    SOME c' => c'
   6.188 +  | NONE => ascii_of c
   6.189 +
   6.190 +(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
   6.191 +fun make_fixed_const @{const_name HOL.eq} = "equal"
   6.192 +  | make_fixed_const c = const_prefix ^ lookup_const c
   6.193 +
   6.194 +fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   6.195 +
   6.196 +fun make_type_class clas = class_prefix ^ ascii_of clas;
   6.197 +
   6.198 +val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
   6.199 +val skolem_prefix = "sko_"
   6.200 +val skolem_infix = "$"
   6.201 +
   6.202 +(* Hack: Could return false positives (e.g., a user happens to declare a
   6.203 +   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
   6.204 +val is_skolem_const_name =
   6.205 +  Long_Name.base_name
   6.206 +  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
   6.207 +
   6.208 +(* The number of type arguments of a constant, zero if it's monomorphic. For
   6.209 +   (instances of) Skolem pseudoconstants, this information is encoded in the
   6.210 +   constant name. *)
   6.211 +fun num_type_args thy s =
   6.212 +  if String.isPrefix skolem_theory_name s then
   6.213 +    s |> unprefix skolem_theory_name
   6.214 +      |> space_explode skolem_infix |> hd
   6.215 +      |> space_explode "_" |> List.last |> Int.fromString |> the
   6.216 +  else
   6.217 +    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   6.218 +
   6.219 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
   6.220 +
   6.221 +type name = string * string
   6.222 +
   6.223 +(**** Isabelle FOL clauses ****)
   6.224 +
   6.225 +(* The first component is the type class; the second is a TVar or TFree. *)
   6.226 +datatype type_literal =
   6.227 +  TyLitVar of name * name |
   6.228 +  TyLitFree of name * name
   6.229 +
   6.230 +(*Make literals for sorted type variables*)
   6.231 +fun sorts_on_typs_aux (_, [])   = []
   6.232 +  | sorts_on_typs_aux ((x,i),  s::ss) =
   6.233 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
   6.234 +      in
   6.235 +          if s = "HOL.type" then sorts
   6.236 +          else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
   6.237 +          else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
   6.238 +      end;
   6.239 +
   6.240 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   6.241 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   6.242 +
   6.243 +(*Given a list of sorted type variables, return a list of type literals.*)
   6.244 +fun type_literals_for_types Ts =
   6.245 +  fold (union (op =)) (map sorts_on_typs Ts) []
   6.246 +
   6.247 +(** make axiom and conjecture clauses. **)
   6.248 +
   6.249 +(**** Isabelle arities ****)
   6.250 +
   6.251 +datatype arLit =
   6.252 +  TConsLit of name * name * name list |
   6.253 +  TVarLit of name * name
   6.254 +
   6.255 +datatype arity_clause =
   6.256 +  ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   6.257 +
   6.258 +
   6.259 +fun gen_TVars 0 = []
   6.260 +  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   6.261 +
   6.262 +fun pack_sort(_,[])  = []
   6.263 +  | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
   6.264 +  | pack_sort(tvar, cls::srt) =
   6.265 +    (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
   6.266 +
   6.267 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
   6.268 +fun make_axiom_arity_clause (tcons, name, (cls,args)) =
   6.269 +  let
   6.270 +    val tvars = gen_TVars (length args)
   6.271 +    val tvars_srts = ListPair.zip (tvars, args)
   6.272 +  in
   6.273 +    ArityClause {name = name,
   6.274 +                 conclLit = TConsLit (`make_type_class cls,
   6.275 +                                      `make_fixed_type_const tcons,
   6.276 +                                      tvars ~~ tvars),
   6.277 +                 premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
   6.278 +  end
   6.279 +
   6.280 +
   6.281 +(**** Isabelle class relations ****)
   6.282 +
   6.283 +datatype class_rel_clause =
   6.284 +  ClassRelClause of {name: string, subclass: name, superclass: name}
   6.285 +
   6.286 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   6.287 +fun class_pairs _ [] _ = []
   6.288 +  | class_pairs thy subs supers =
   6.289 +      let
   6.290 +        val class_less = Sorts.class_less (Sign.classes_of thy)
   6.291 +        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   6.292 +        fun add_supers sub = fold (add_super sub) supers
   6.293 +      in fold add_supers subs [] end
   6.294 +
   6.295 +fun make_class_rel_clause (sub,super) =
   6.296 +  ClassRelClause {name = sub ^ "_" ^ super,
   6.297 +                  subclass = `make_type_class sub,
   6.298 +                  superclass = `make_type_class super}
   6.299 +
   6.300 +fun make_class_rel_clauses thy subs supers =
   6.301 +  map make_class_rel_clause (class_pairs thy subs supers);
   6.302 +
   6.303 +
   6.304 +(** Isabelle arities **)
   6.305 +
   6.306 +fun arity_clause _ _ (_, []) = []
   6.307 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   6.308 +      arity_clause seen n (tcons,ars)
   6.309 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   6.310 +      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   6.311 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   6.312 +          arity_clause seen (n+1) (tcons,ars)
   6.313 +      else
   6.314 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
   6.315 +          arity_clause (class::seen) n (tcons,ars)
   6.316 +
   6.317 +fun multi_arity_clause [] = []
   6.318 +  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   6.319 +      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   6.320 +
   6.321 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   6.322 +  provided its arguments have the corresponding sorts.*)
   6.323 +fun type_class_pairs thy tycons classes =
   6.324 +  let val alg = Sign.classes_of thy
   6.325 +      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   6.326 +      fun add_class tycon class =
   6.327 +        cons (class, domain_sorts tycon class)
   6.328 +        handle Sorts.CLASS_ERROR _ => I
   6.329 +      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   6.330 +  in  map try_classes tycons  end;
   6.331 +
   6.332 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
   6.333 +fun iter_type_class_pairs _ _ [] = ([], [])
   6.334 +  | iter_type_class_pairs thy tycons classes =
   6.335 +      let val cpairs = type_class_pairs thy tycons classes
   6.336 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   6.337 +            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   6.338 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   6.339 +      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   6.340 +
   6.341 +fun make_arity_clauses thy tycons classes =
   6.342 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   6.343 +  in  (classes', multi_arity_clause cpairs)  end;
   6.344 +
   6.345 +datatype combtyp =
   6.346 +  CombTVar of name |
   6.347 +  CombTFree of name |
   6.348 +  CombType of name * combtyp list
   6.349 +
   6.350 +datatype combterm =
   6.351 +  CombConst of name * combtyp * combtyp list (* Const and Free *) |
   6.352 +  CombVar of name * combtyp |
   6.353 +  CombApp of combterm * combterm
   6.354 +
   6.355 +datatype fol_literal = FOLLiteral of bool * combterm
   6.356 +
   6.357 +(*********************************************************************)
   6.358 +(* convert a clause with type Term.term to a clause with type clause *)
   6.359 +(*********************************************************************)
   6.360 +
   6.361 +(*Result of a function type; no need to check that the argument type matches.*)
   6.362 +fun result_type (CombType (_, [_, tp2])) = tp2
   6.363 +  | result_type _ = raise Fail "non-function type"
   6.364 +
   6.365 +fun combtyp_of (CombConst (_, tp, _)) = tp
   6.366 +  | combtyp_of (CombVar (_, tp)) = tp
   6.367 +  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
   6.368 +
   6.369 +(*gets the head of a combinator application, along with the list of arguments*)
   6.370 +fun strip_combterm_comb u =
   6.371 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   6.372 +        |   stripc  x =  x
   6.373 +    in stripc(u,[]) end
   6.374 +
   6.375 +fun type_of (Type (a, Ts)) =
   6.376 +    let val (folTypes,ts) = types_of Ts in
   6.377 +      (CombType (`make_fixed_type_const a, folTypes), ts)
   6.378 +    end
   6.379 +  | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
   6.380 +  | type_of (tp as TVar (x, _)) =
   6.381 +    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
   6.382 +and types_of Ts =
   6.383 +    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   6.384 +      (folTyps, union_all ts)
   6.385 +    end
   6.386 +
   6.387 +(* same as above, but no gathering of sort information *)
   6.388 +fun simp_type_of (Type (a, Ts)) =
   6.389 +      CombType (`make_fixed_type_const a, map simp_type_of Ts)
   6.390 +  | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
   6.391 +  | simp_type_of (TVar (x, _)) =
   6.392 +    CombTVar (make_schematic_type_var x, string_of_indexname x)
   6.393 +
   6.394 +(* Converts a term (with combinators) into a combterm. Also accummulates sort
   6.395 +   infomation. *)
   6.396 +fun combterm_from_term thy bs (P $ Q) =
   6.397 +      let val (P', tsP) = combterm_from_term thy bs P
   6.398 +          val (Q', tsQ) = combterm_from_term thy bs Q
   6.399 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   6.400 +  | combterm_from_term thy _ (Const (c, T)) =
   6.401 +      let
   6.402 +        val (tp, ts) = type_of T
   6.403 +        val tvar_list =
   6.404 +          (if String.isPrefix skolem_theory_name c then
   6.405 +             [] |> Term.add_tvarsT T |> map TVar
   6.406 +           else
   6.407 +             (c, T) |> Sign.const_typargs thy)
   6.408 +          |> map simp_type_of
   6.409 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   6.410 +      in  (c',ts)  end
   6.411 +  | combterm_from_term _ _ (Free (v, T)) =
   6.412 +      let val (tp,ts) = type_of T
   6.413 +          val v' = CombConst (`make_fixed_var v, tp, [])
   6.414 +      in  (v',ts)  end
   6.415 +  | combterm_from_term _ _ (Var (v, T)) =
   6.416 +      let val (tp,ts) = type_of T
   6.417 +          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   6.418 +      in  (v',ts)  end
   6.419 +  | combterm_from_term _ bs (Bound j) =
   6.420 +      let
   6.421 +        val (s, T) = nth bs j
   6.422 +        val (tp, ts) = type_of T
   6.423 +        val v' = CombConst (`make_bound_var s, tp, [])
   6.424 +      in (v', ts) end
   6.425 +  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   6.426 +
   6.427 +fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   6.428 +  | predicate_of thy (t, pos) =
   6.429 +    (combterm_from_term thy [] (Envir.eta_contract t), pos)
   6.430 +
   6.431 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   6.432 +    literals_of_term1 args thy P
   6.433 +  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
   6.434 +    literals_of_term1 (literals_of_term1 args thy P) thy Q
   6.435 +  | literals_of_term1 (lits, ts) thy P =
   6.436 +    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   6.437 +      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
   6.438 +    end
   6.439 +val literals_of_term = literals_of_term1 ([], [])
   6.440 +
   6.441 +fun skolem_name i j num_T_args =
   6.442 +  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   6.443 +  skolem_infix ^ "g"
   6.444 +
   6.445 +fun conceal_skolem_terms i skolems t =
   6.446 +  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
   6.447 +    let
   6.448 +      fun aux skolems
   6.449 +              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
   6.450 +          let
   6.451 +            val (skolems, s) =
   6.452 +              if i = ~1 then
   6.453 +                (skolems, @{const_name undefined})
   6.454 +              else case AList.find (op aconv) skolems t of
   6.455 +                s :: _ => (skolems, s)
   6.456 +              | [] =>
   6.457 +                let
   6.458 +                  val s = skolem_theory_name ^ "." ^
   6.459 +                          skolem_name i (length skolems)
   6.460 +                                        (length (Term.add_tvarsT T []))
   6.461 +                in ((s, t) :: skolems, s) end
   6.462 +          in (skolems, Const (s, T)) end
   6.463 +        | aux skolems (t1 $ t2) =
   6.464 +          let
   6.465 +            val (skolems, t1) = aux skolems t1
   6.466 +            val (skolems, t2) = aux skolems t2
   6.467 +          in (skolems, t1 $ t2) end
   6.468 +        | aux skolems (Abs (s, T, t')) =
   6.469 +          let val (skolems, t') = aux skolems t' in
   6.470 +            (skolems, Abs (s, T, t'))
   6.471 +          end
   6.472 +        | aux skolems t = (skolems, t)
   6.473 +    in aux skolems t end
   6.474 +  else
   6.475 +    (skolems, t)
   6.476 +
   6.477 +fun reveal_skolem_terms skolems =
   6.478 +  map_aterms (fn t as Const (s, _) =>
   6.479 +                 if String.isPrefix skolem_theory_name s then
   6.480 +                   AList.lookup (op =) skolems s |> the
   6.481 +                   |> map_types Type_Infer.paramify_vars
   6.482 +                 else
   6.483 +                   t
   6.484 +               | t => t)
   6.485 +
   6.486 +
   6.487 +(***************************************************************)
   6.488 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
   6.489 +(***************************************************************)
   6.490 +
   6.491 +fun set_insert (x, s) = Symtab.update (x, ()) s
   6.492 +
   6.493 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   6.494 +
   6.495 +(*Remove this trivial type class*)
   6.496 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   6.497 +
   6.498 +fun tfree_classes_of_terms ts =
   6.499 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   6.500 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   6.501 +
   6.502 +fun tvar_classes_of_terms ts =
   6.503 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   6.504 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   6.505 +
   6.506 +(*fold type constructors*)
   6.507 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   6.508 +  | fold_type_consts _ _ x = x;
   6.509 +
   6.510 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   6.511 +fun add_type_consts_in_term thy =
   6.512 +  let
   6.513 +    fun aux (Const x) =
   6.514 +        fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
   6.515 +      | aux (Abs (_, _, u)) = aux u
   6.516 +      | aux (Const (@{const_name skolem}, _) $ _) = I
   6.517 +      | aux (t $ u) = aux t #> aux u
   6.518 +      | aux _ = I
   6.519 +  in aux end
   6.520 +
   6.521 +fun type_consts_of_terms thy ts =
   6.522 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   6.523 +
   6.524 +end;
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 15:38:46 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 16:12:02 2010 +0200
     7.3 @@ -68,7 +68,7 @@
     7.4  open ATP_Problem
     7.5  open ATP_Proof
     7.6  open ATP_Systems
     7.7 -open Metis_Clauses
     7.8 +open Metis_Translate
     7.9  open Sledgehammer_Util
    7.10  open Sledgehammer_Filter
    7.11  open Sledgehammer_Translate
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 15:38:46 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 16:12:02 2010 +0200
     8.3 @@ -30,7 +30,7 @@
     8.4  
     8.5  open ATP_Problem
     8.6  open ATP_Proof
     8.7 -open Metis_Clauses
     8.8 +open Metis_Translate
     8.9  open Sledgehammer_Util
    8.10  open Sledgehammer_Filter
    8.11  open Sledgehammer_Translate
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 15:38:46 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 16:12:02 2010 +0200
     9.3 @@ -3,7 +3,7 @@
     9.4      Author:     Makarius
     9.5      Author:     Jasmin Blanchette, TU Muenchen
     9.6  
     9.7 -Translation of HOL to FOL.
     9.8 +Translation of HOL to FOL for Sledgehammer.
     9.9  *)
    9.10  
    9.11  signature SLEDGEHAMMER_TRANSLATE =
    9.12 @@ -30,7 +30,7 @@
    9.13  struct
    9.14  
    9.15  open ATP_Problem
    9.16 -open Metis_Clauses
    9.17 +open Metis_Translate
    9.18  open Sledgehammer_Util
    9.19  
    9.20  val axiom_prefix = "ax_"