renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
authorblanchet
Fri Jun 25 17:08:39 2010 +0200 (2010-06-25)
changeset 375789367cb36b1c4
parent 37577 5379f41a1322
child 37579 61a01843a028
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/meson_tactic.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 25 16:42:06 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 25 17:08:39 2010 +0200
     1.3 @@ -315,10 +315,10 @@
     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_tactics.ML \
     1.9    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
    1.10    Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
    1.11 -  Tools/Sledgehammer/sledgehammer_fol_clause.ML \
    1.12    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.13    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
    1.14    Tools/Sledgehammer/sledgehammer_tptp_format.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 25 16:42:06 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 25 17:08:39 2010 +0200
     2.3 @@ -325,7 +325,7 @@
     2.4        NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     2.5      | SOME _ => (message, SH_FAIL (time_isa, time_atp))
     2.6    end
     2.7 -  handle Sledgehammer_FOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     2.8 +  handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
     2.9         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    2.10         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    2.11  
    2.12 @@ -382,7 +382,7 @@
    2.13  
    2.14  fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
    2.15    let
    2.16 -    open Sledgehammer_Fact_Minimizer
    2.17 +    open Metis_Clauses
    2.18      open Sledgehammer_Isar
    2.19      val thy = Proof.theory_of st
    2.20      val n0 = length (these (!named_thms))
     3.1 --- a/src/HOL/Sledgehammer.thy	Fri Jun 25 16:42:06 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 17:08:39 2010 +0200
     3.3 @@ -13,8 +13,9 @@
     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_tactics.ML")
     3.9    ("Tools/Sledgehammer/sledgehammer_util.ML")
    3.10 -  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    3.11    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    3.12    ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
    3.13    ("Tools/ATP_Manager/atp_manager.ML")
    3.14 @@ -22,7 +23,6 @@
    3.15    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    3.16    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    3.17    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    3.18 -  ("Tools/Sledgehammer/metis_tactics.ML")
    3.19  begin
    3.20  
    3.21  definition skolem_id :: "'a \<Rightarrow> 'a" where
    3.22 @@ -86,11 +86,14 @@
    3.23  
    3.24  use "Tools/Sledgehammer/clausifier.ML"
    3.25  setup Clausifier.setup
    3.26 +
    3.27  use "Tools/Sledgehammer/meson_tactic.ML"
    3.28  setup Meson_Tactic.setup
    3.29  
    3.30 +use "Tools/Sledgehammer/metis_clauses.ML"
    3.31 +use "Tools/Sledgehammer/metis_tactics.ML"
    3.32 +
    3.33  use "Tools/Sledgehammer/sledgehammer_util.ML"
    3.34 -use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    3.35  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    3.36  use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    3.37  use "Tools/ATP_Manager/atp_manager.ML"
    3.38 @@ -99,7 +102,6 @@
    3.39  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    3.40  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    3.41  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.42 -use "Tools/Sledgehammer/metis_tactics.ML"
    3.43  setup Metis_Tactics.setup
    3.44  
    3.45  end
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 16:42:06 2010 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Jun 25 17:08:39 2010 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  signature ATP_MANAGER =
     4.5  sig
     4.6    type cnf_thm = Clausifier.cnf_thm
     4.7 -  type name_pool = Sledgehammer_FOL_Clause.name_pool
     4.8 +  type name_pool = Metis_Clauses.name_pool
     4.9    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    4.10    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    4.11    type params =
    4.12 @@ -65,9 +65,8 @@
    4.13  structure ATP_Manager : ATP_MANAGER =
    4.14  struct
    4.15  
    4.16 -open Sledgehammer_Util
    4.17 +open Metis_Clauses
    4.18  open Sledgehammer_Fact_Filter
    4.19 -open Sledgehammer_FOL_Clause
    4.20  open Sledgehammer_Proof_Reconstruct
    4.21  
    4.22  (** problems, results, provers, etc. **)
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 16:42:06 2010 +0200
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 17:08:39 2010 +0200
     5.3 @@ -23,11 +23,11 @@
     5.4  struct
     5.5  
     5.6  open Clausifier
     5.7 +open Metis_Clauses
     5.8  open Sledgehammer_Util
     5.9 -open Sledgehammer_FOL_Clause
    5.10  open Sledgehammer_Fact_Filter
    5.11 +open Sledgehammer_TPTP_Format
    5.12  open Sledgehammer_Proof_Reconstruct
    5.13 -open Sledgehammer_TPTP_Format
    5.14  open ATP_Manager
    5.15  
    5.16  (** generic ATP **)
     6.1 --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Fri Jun 25 16:42:06 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Fri Jun 25 17:08:39 2010 +0200
     6.3 @@ -14,11 +14,9 @@
     6.4  structure Meson_Tactic : MESON_TACTIC =
     6.5  struct
     6.6  
     6.7 -open Clausifier
     6.8 -
     6.9  (*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
    6.10  fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
    6.11 -    String.isPrefix skolem_prefix a
    6.12 +    String.isPrefix Clausifier.skolem_prefix a
    6.13    | is_absko _ = false;
    6.14  
    6.15  fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) =   (*Definition of Free, not in certain terms*)
    6.16 @@ -43,7 +41,10 @@
    6.17    let
    6.18      val thy = ProofContext.theory_of ctxt
    6.19      val ctxt0 = Classical.put_claset HOL_cs ctxt
    6.20 -  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
    6.21 +  in
    6.22 +    (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
    6.23 +     THEN expand_defs_tac st0) st0
    6.24 +  end
    6.25  
    6.26  val setup =
    6.27    Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Jun 25 17:08:39 2010 +0200
     7.3 @@ -0,0 +1,685 @@
     7.4 +(*  Title:      HOL/Tools/Sledgehammer/metis_clauses.ML
     7.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory
     7.6 +    Author:     Jasmin Blanchette, TU Muenchen
     7.7 +
     7.8 +Storing/printing FOL clauses and arity clauses.  Typed equality is
     7.9 +treated differently.
    7.10 +*)
    7.11 +
    7.12 +signature METIS_CLAUSES =
    7.13 +sig
    7.14 +  type cnf_thm = Clausifier.cnf_thm
    7.15 +  type name = string * string
    7.16 +  type name_pool = string Symtab.table * string Symtab.table
    7.17 +  datatype kind = Axiom | Conjecture
    7.18 +  datatype type_literal =
    7.19 +    TyLitVar of string * name |
    7.20 +    TyLitFree of string * name
    7.21 +  datatype arLit =
    7.22 +      TConsLit of class * string * string list
    7.23 +    | TVarLit of class * string
    7.24 +  datatype arity_clause = ArityClause of
    7.25 +   {axiom_name: string, conclLit: arLit, premLits: arLit list}
    7.26 +  datatype classrel_clause = ClassrelClause of
    7.27 +   {axiom_name: string, subclass: class, superclass: class}
    7.28 +  datatype combtyp =
    7.29 +    TyVar of name |
    7.30 +    TyFree of name |
    7.31 +    TyConstr of name * combtyp list
    7.32 +  datatype combterm =
    7.33 +    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    7.34 +    CombVar of name * combtyp |
    7.35 +    CombApp of combterm * combterm
    7.36 +  datatype literal = Literal of bool * combterm
    7.37 +  datatype hol_clause =
    7.38 +    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    7.39 +                  literals: literal list, ctypes_sorts: typ list}
    7.40 +  exception TRIVIAL of unit
    7.41 +
    7.42 +  val type_wrapper_name : string
    7.43 +  val schematic_var_prefix: string
    7.44 +  val fixed_var_prefix: string
    7.45 +  val tvar_prefix: string
    7.46 +  val tfree_prefix: string
    7.47 +  val const_prefix: string
    7.48 +  val tconst_prefix: string
    7.49 +  val class_prefix: string
    7.50 +  val union_all: ''a list list -> ''a list
    7.51 +  val invert_const: string -> string
    7.52 +  val ascii_of: string -> string
    7.53 +  val undo_ascii_of: string -> string
    7.54 +  val strip_prefix: string -> string -> string option
    7.55 +  val make_schematic_var : string * int -> string
    7.56 +  val make_fixed_var : string -> string
    7.57 +  val make_schematic_type_var : string * int -> string
    7.58 +  val make_fixed_type_var : string -> string
    7.59 +  val make_fixed_const : string -> string
    7.60 +  val make_fixed_type_const : string -> string
    7.61 +  val make_type_class : string -> string
    7.62 +  val empty_name_pool : bool -> name_pool option
    7.63 +  val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    7.64 +  val nice_name : name -> name_pool option -> string * name_pool option
    7.65 +  val type_literals_for_types : typ list -> type_literal list
    7.66 +  val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    7.67 +  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    7.68 +  val type_of_combterm : combterm -> combtyp
    7.69 +  val strip_combterm_comb : combterm -> combterm * combterm list
    7.70 +  val literals_of_term : theory -> term -> literal list * typ list
    7.71 +  val conceal_skolem_somes :
    7.72 +    int -> (string * term) list -> term -> (string * term) list * term
    7.73 +  val is_quasi_fol_theorem : theory -> thm -> bool
    7.74 +  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
    7.75 +  val tfree_classes_of_terms : term list -> string list
    7.76 +  val tvar_classes_of_terms : term list -> string list
    7.77 +  val type_consts_of_terms : theory -> term list -> string list
    7.78 +  val prepare_clauses :
    7.79 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    7.80 +    -> string vector
    7.81 +       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
    7.82 +          * classrel_clause list * arity_clause list)
    7.83 +end
    7.84 +
    7.85 +structure Metis_Clauses : METIS_CLAUSES =
    7.86 +struct
    7.87 +
    7.88 +open Clausifier
    7.89 +
    7.90 +val type_wrapper_name = "ti"
    7.91 +
    7.92 +val schematic_var_prefix = "V_";
    7.93 +val fixed_var_prefix = "v_";
    7.94 +
    7.95 +val tvar_prefix = "T_";
    7.96 +val tfree_prefix = "t_";
    7.97 +
    7.98 +val classrel_clause_prefix = "clsrel_";
    7.99 +
   7.100 +val const_prefix = "c_";
   7.101 +val tconst_prefix = "tc_";
   7.102 +val class_prefix = "class_";
   7.103 +
   7.104 +fun union_all xss = fold (union (op =)) xss []
   7.105 +
   7.106 +(* Readable names for the more common symbolic functions. Do not mess with the
   7.107 +   last nine entries of the table unless you know what you are doing. *)
   7.108 +val const_trans_table =
   7.109 +  Symtab.make [(@{const_name "op ="}, "equal"),
   7.110 +               (@{const_name "op &"}, "and"),
   7.111 +               (@{const_name "op |"}, "or"),
   7.112 +               (@{const_name "op -->"}, "implies"),
   7.113 +               (@{const_name "op :"}, "in"),
   7.114 +               (@{const_name fequal}, "fequal"),
   7.115 +               (@{const_name COMBI}, "COMBI"),
   7.116 +               (@{const_name COMBK}, "COMBK"),
   7.117 +               (@{const_name COMBB}, "COMBB"),
   7.118 +               (@{const_name COMBC}, "COMBC"),
   7.119 +               (@{const_name COMBS}, "COMBS"),
   7.120 +               (@{const_name True}, "True"),
   7.121 +               (@{const_name False}, "False"),
   7.122 +               (@{const_name If}, "If"),
   7.123 +               (@{type_name "*"}, "prod"),
   7.124 +               (@{type_name "+"}, "sum")]
   7.125 +
   7.126 +(* Invert the table of translations between Isabelle and ATPs. *)
   7.127 +val const_trans_table_inv =
   7.128 +  Symtab.update ("fequal", @{const_name "op ="})
   7.129 +                (Symtab.make (map swap (Symtab.dest const_trans_table)))
   7.130 +
   7.131 +val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   7.132 +
   7.133 +(*Escaping of special characters.
   7.134 +  Alphanumeric characters are left unchanged.
   7.135 +  The character _ goes to __
   7.136 +  Characters in the range ASCII space to / go to _A to _P, respectively.
   7.137 +  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
   7.138 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
   7.139 +
   7.140 +fun stringN_of_int 0 _ = ""
   7.141 +  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   7.142 +
   7.143 +fun ascii_of_c c =
   7.144 +  if Char.isAlphaNum c then String.str c
   7.145 +  else if c = #"_" then "__"
   7.146 +  else if #" " <= c andalso c <= #"/"
   7.147 +       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   7.148 +  else if Char.isPrint c
   7.149 +       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   7.150 +  else ""
   7.151 +
   7.152 +val ascii_of = String.translate ascii_of_c;
   7.153 +
   7.154 +(** Remove ASCII armouring from names in proof files **)
   7.155 +
   7.156 +(*We don't raise error exceptions because this code can run inside the watcher.
   7.157 +  Also, the errors are "impossible" (hah!)*)
   7.158 +fun undo_ascii_aux rcs [] = String.implode(rev rcs)
   7.159 +  | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
   7.160 +      (*Three types of _ escapes: __, _A to _P, _nnn*)
   7.161 +  | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
   7.162 +  | undo_ascii_aux rcs (#"_" :: c :: cs) =
   7.163 +      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   7.164 +      then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   7.165 +      else
   7.166 +        let val digits = List.take (c::cs, 3) handle Subscript => []
   7.167 +        in
   7.168 +            case Int.fromString (String.implode digits) of
   7.169 +                NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   7.170 +              | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   7.171 +        end
   7.172 +  | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
   7.173 +
   7.174 +val undo_ascii_of = undo_ascii_aux [] o String.explode;
   7.175 +
   7.176 +(* If string s has the prefix s1, return the result of deleting it,
   7.177 +   un-ASCII'd. *)
   7.178 +fun strip_prefix s1 s =
   7.179 +  if String.isPrefix s1 s then
   7.180 +    SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   7.181 +  else
   7.182 +    NONE
   7.183 +
   7.184 +(*Remove the initial ' character from a type variable, if it is present*)
   7.185 +fun trim_type_var s =
   7.186 +  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   7.187 +  else error ("trim_type: Malformed type variable encountered: " ^ s);
   7.188 +
   7.189 +fun ascii_of_indexname (v,0) = ascii_of v
   7.190 +  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   7.191 +
   7.192 +fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   7.193 +fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   7.194 +
   7.195 +fun make_schematic_type_var (x,i) =
   7.196 +      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   7.197 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   7.198 +
   7.199 +fun lookup_const c =
   7.200 +  case Symtab.lookup const_trans_table c of
   7.201 +    SOME c' => c'
   7.202 +  | NONE => ascii_of c
   7.203 +
   7.204 +(* "op =" MUST BE "equal" because it's built into ATPs. *)
   7.205 +fun make_fixed_const @{const_name "op ="} = "equal"
   7.206 +  | make_fixed_const c = const_prefix ^ lookup_const c
   7.207 +
   7.208 +fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
   7.209 +
   7.210 +fun make_type_class clas = class_prefix ^ ascii_of clas;
   7.211 +
   7.212 +
   7.213 +(**** name pool ****)
   7.214 + 
   7.215 +type name = string * string
   7.216 +type name_pool = string Symtab.table * string Symtab.table
   7.217 +
   7.218 +fun empty_name_pool readable_names =
   7.219 +  if readable_names then SOME (`I Symtab.empty) else NONE
   7.220 +
   7.221 +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
   7.222 +fun pool_map f xs =
   7.223 +  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
   7.224 +
   7.225 +fun add_nice_name full_name nice_prefix j the_pool =
   7.226 +  let
   7.227 +    val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
   7.228 +  in
   7.229 +    case Symtab.lookup (snd the_pool) nice_name of
   7.230 +      SOME full_name' =>
   7.231 +      if full_name = full_name' then (nice_name, the_pool)
   7.232 +      else add_nice_name full_name nice_prefix (j + 1) the_pool
   7.233 +    | NONE =>
   7.234 +      (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
   7.235 +                   Symtab.update_new (nice_name, full_name) (snd the_pool)))
   7.236 +  end
   7.237 +
   7.238 +fun translate_first_char f s =
   7.239 +  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
   7.240 +
   7.241 +fun readable_name full_name s =
   7.242 +  let
   7.243 +    val s = s |> Long_Name.base_name |> Name.desymbolize false
   7.244 +    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
   7.245 +    val s' =
   7.246 +      (s' |> rev
   7.247 +          |> implode
   7.248 +          |> String.translate
   7.249 +                 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
   7.250 +                          else ""))
   7.251 +      ^ replicate_string (String.size s - length s') "_"
   7.252 +    val s' =
   7.253 +      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
   7.254 +      else s'
   7.255 +    (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
   7.256 +       ("op &", "op |", etc.). *)
   7.257 +    val s' = if s' = "equal" orelse s' = "op" then full_name else s'
   7.258 +  in
   7.259 +    case (Char.isLower (String.sub (full_name, 0)),
   7.260 +          Char.isLower (String.sub (s', 0))) of
   7.261 +      (true, false) => translate_first_char Char.toLower s'
   7.262 +    | (false, true) => translate_first_char Char.toUpper s'
   7.263 +    | _ => s'
   7.264 +  end
   7.265 +
   7.266 +fun nice_name (full_name, _) NONE = (full_name, NONE)
   7.267 +  | nice_name (full_name, desired_name) (SOME the_pool) =
   7.268 +    case Symtab.lookup (fst the_pool) full_name of
   7.269 +      SOME nice_name => (nice_name, SOME the_pool)
   7.270 +    | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
   7.271 +                            the_pool
   7.272 +              |> apsnd SOME
   7.273 +
   7.274 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
   7.275 +
   7.276 +datatype kind = Axiom | Conjecture
   7.277 +
   7.278 +(**** Isabelle FOL clauses ****)
   7.279 +
   7.280 +(* The first component is the type class; the second is a TVar or TFree. *)
   7.281 +datatype type_literal =
   7.282 +  TyLitVar of string * name |
   7.283 +  TyLitFree of string * name
   7.284 +
   7.285 +exception CLAUSE of string * term;
   7.286 +
   7.287 +(*Make literals for sorted type variables*)
   7.288 +fun sorts_on_typs_aux (_, [])   = []
   7.289 +  | sorts_on_typs_aux ((x,i),  s::ss) =
   7.290 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
   7.291 +      in
   7.292 +          if s = "HOL.type" then sorts
   7.293 +          else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
   7.294 +          else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
   7.295 +      end;
   7.296 +
   7.297 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   7.298 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   7.299 +
   7.300 +(*Given a list of sorted type variables, return a list of type literals.*)
   7.301 +fun type_literals_for_types Ts =
   7.302 +  fold (union (op =)) (map sorts_on_typs Ts) []
   7.303 +
   7.304 +(** make axiom and conjecture clauses. **)
   7.305 +
   7.306 +(**** Isabelle arities ****)
   7.307 +
   7.308 +datatype arLit = TConsLit of class * string * string list
   7.309 +               | TVarLit of class * string;
   7.310 +
   7.311 +datatype arity_clause =
   7.312 +  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
   7.313 +
   7.314 +
   7.315 +fun gen_TVars 0 = []
   7.316 +  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   7.317 +
   7.318 +fun pack_sort(_,[])  = []
   7.319 +  | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
   7.320 +  | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
   7.321 +
   7.322 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
   7.323 +fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
   7.324 +   let val tvars = gen_TVars (length args)
   7.325 +       val tvars_srts = ListPair.zip (tvars,args)
   7.326 +   in
   7.327 +     ArityClause {axiom_name = axiom_name, 
   7.328 +                  conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   7.329 +                  premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   7.330 +   end;
   7.331 +
   7.332 +
   7.333 +(**** Isabelle class relations ****)
   7.334 +
   7.335 +datatype classrel_clause =
   7.336 +  ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
   7.337 +
   7.338 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   7.339 +fun class_pairs _ [] _ = []
   7.340 +  | class_pairs thy subs supers =
   7.341 +      let
   7.342 +        val class_less = Sorts.class_less (Sign.classes_of thy)
   7.343 +        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   7.344 +        fun add_supers sub = fold (add_super sub) supers
   7.345 +      in fold add_supers subs [] end
   7.346 +
   7.347 +fun make_classrel_clause (sub,super) =
   7.348 +  ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
   7.349 +                               ascii_of super,
   7.350 +                  subclass = make_type_class sub,
   7.351 +                  superclass = make_type_class super};
   7.352 +
   7.353 +fun make_classrel_clauses thy subs supers =
   7.354 +  map make_classrel_clause (class_pairs thy subs supers);
   7.355 +
   7.356 +
   7.357 +(** Isabelle arities **)
   7.358 +
   7.359 +fun arity_clause _ _ (_, []) = []
   7.360 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   7.361 +      arity_clause seen n (tcons,ars)
   7.362 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   7.363 +      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   7.364 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   7.365 +          arity_clause seen (n+1) (tcons,ars)
   7.366 +      else
   7.367 +          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
   7.368 +          arity_clause (class::seen) n (tcons,ars)
   7.369 +
   7.370 +fun multi_arity_clause [] = []
   7.371 +  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   7.372 +      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   7.373 +
   7.374 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   7.375 +  provided its arguments have the corresponding sorts.*)
   7.376 +fun type_class_pairs thy tycons classes =
   7.377 +  let val alg = Sign.classes_of thy
   7.378 +      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   7.379 +      fun add_class tycon class =
   7.380 +        cons (class, domain_sorts tycon class)
   7.381 +        handle Sorts.CLASS_ERROR _ => I
   7.382 +      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   7.383 +  in  map try_classes tycons  end;
   7.384 +
   7.385 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
   7.386 +fun iter_type_class_pairs _ _ [] = ([], [])
   7.387 +  | iter_type_class_pairs thy tycons classes =
   7.388 +      let val cpairs = type_class_pairs thy tycons classes
   7.389 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   7.390 +            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   7.391 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   7.392 +      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   7.393 +
   7.394 +fun make_arity_clauses thy tycons classes =
   7.395 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   7.396 +  in  (classes', multi_arity_clause cpairs)  end;
   7.397 +
   7.398 +datatype combtyp =
   7.399 +  TyVar of name |
   7.400 +  TyFree of name |
   7.401 +  TyConstr of name * combtyp list
   7.402 +
   7.403 +datatype combterm =
   7.404 +  CombConst of name * combtyp * combtyp list (* Const and Free *) |
   7.405 +  CombVar of name * combtyp |
   7.406 +  CombApp of combterm * combterm
   7.407 +
   7.408 +datatype literal = Literal of bool * combterm
   7.409 +
   7.410 +datatype hol_clause =
   7.411 +  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
   7.412 +                literals: literal list, ctypes_sorts: typ list}
   7.413 +
   7.414 +(*********************************************************************)
   7.415 +(* convert a clause with type Term.term to a clause with type clause *)
   7.416 +(*********************************************************************)
   7.417 +
   7.418 +(*Result of a function type; no need to check that the argument type matches.*)
   7.419 +fun result_type (TyConstr (_, [_, tp2])) = tp2
   7.420 +  | result_type _ = raise Fail "non-function type"
   7.421 +
   7.422 +fun type_of_combterm (CombConst (_, tp, _)) = tp
   7.423 +  | type_of_combterm (CombVar (_, tp)) = tp
   7.424 +  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
   7.425 +
   7.426 +(*gets the head of a combinator application, along with the list of arguments*)
   7.427 +fun strip_combterm_comb u =
   7.428 +    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   7.429 +        |   stripc  x =  x
   7.430 +    in stripc(u,[]) end
   7.431 +
   7.432 +fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
   7.433 +      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
   7.434 +  | isFalse _ = false;
   7.435 +
   7.436 +fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
   7.437 +      (pol andalso c = "c_True") orelse
   7.438 +      (not pol andalso c = "c_False")
   7.439 +  | isTrue _ = false;
   7.440 +
   7.441 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
   7.442 +
   7.443 +fun type_of (Type (a, Ts)) =
   7.444 +    let val (folTypes,ts) = types_of Ts in
   7.445 +      (TyConstr (`make_fixed_type_const a, folTypes), ts)
   7.446 +    end
   7.447 +  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
   7.448 +  | type_of (tp as TVar (x, _)) =
   7.449 +    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
   7.450 +and types_of Ts =
   7.451 +    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   7.452 +      (folTyps, union_all ts)
   7.453 +    end
   7.454 +
   7.455 +(* same as above, but no gathering of sort information *)
   7.456 +fun simp_type_of (Type (a, Ts)) =
   7.457 +      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
   7.458 +  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
   7.459 +  | simp_type_of (TVar (x, _)) =
   7.460 +    TyVar (make_schematic_type_var x, string_of_indexname x)
   7.461 +
   7.462 +(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   7.463 +fun combterm_of thy (Const (c, T)) =
   7.464 +      let
   7.465 +        val (tp, ts) = type_of T
   7.466 +        val tvar_list =
   7.467 +          (if String.isPrefix skolem_theory_name c then
   7.468 +             [] |> Term.add_tvarsT T |> map TVar
   7.469 +           else
   7.470 +             (c, T) |> Sign.const_typargs thy)
   7.471 +          |> map simp_type_of
   7.472 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   7.473 +      in  (c',ts)  end
   7.474 +  | combterm_of _ (Free(v, T)) =
   7.475 +      let val (tp,ts) = type_of T
   7.476 +          val v' = CombConst (`make_fixed_var v, tp, [])
   7.477 +      in  (v',ts)  end
   7.478 +  | combterm_of _ (Var(v, T)) =
   7.479 +      let val (tp,ts) = type_of T
   7.480 +          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   7.481 +      in  (v',ts)  end
   7.482 +  | combterm_of thy (P $ Q) =
   7.483 +      let val (P', tsP) = combterm_of thy P
   7.484 +          val (Q', tsQ) = combterm_of thy Q
   7.485 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   7.486 +  | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
   7.487 +
   7.488 +fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   7.489 +  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
   7.490 +
   7.491 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   7.492 +    literals_of_term1 args thy P
   7.493 +  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   7.494 +    literals_of_term1 (literals_of_term1 args thy P) thy Q
   7.495 +  | literals_of_term1 (lits, ts) thy P =
   7.496 +    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   7.497 +      (Literal (pol, pred) :: lits, union (op =) ts ts')
   7.498 +    end
   7.499 +val literals_of_term = literals_of_term1 ([], [])
   7.500 +
   7.501 +fun skolem_name i j num_T_args =
   7.502 +  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   7.503 +  skolem_infix ^ "g"
   7.504 +
   7.505 +fun conceal_skolem_somes i skolem_somes t =
   7.506 +  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
   7.507 +    let
   7.508 +      fun aux skolem_somes
   7.509 +              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
   7.510 +          let
   7.511 +            val (skolem_somes, s) =
   7.512 +              if i = ~1 then
   7.513 +                (skolem_somes, @{const_name undefined})
   7.514 +              else case AList.find (op aconv) skolem_somes t of
   7.515 +                s :: _ => (skolem_somes, s)
   7.516 +              | [] =>
   7.517 +                let
   7.518 +                  val s = skolem_theory_name ^ "." ^
   7.519 +                          skolem_name i (length skolem_somes)
   7.520 +                                        (length (Term.add_tvarsT T []))
   7.521 +                in ((s, t) :: skolem_somes, s) end
   7.522 +          in (skolem_somes, Const (s, T)) end
   7.523 +        | aux skolem_somes (t1 $ t2) =
   7.524 +          let
   7.525 +            val (skolem_somes, t1) = aux skolem_somes t1
   7.526 +            val (skolem_somes, t2) = aux skolem_somes t2
   7.527 +          in (skolem_somes, t1 $ t2) end
   7.528 +        | aux skolem_somes (Abs (s, T, t')) =
   7.529 +          let val (skolem_somes, t') = aux skolem_somes t' in
   7.530 +            (skolem_somes, Abs (s, T, t'))
   7.531 +          end
   7.532 +        | aux skolem_somes t = (skolem_somes, t)
   7.533 +    in aux skolem_somes t end
   7.534 +  else
   7.535 +    (skolem_somes, t)
   7.536 +
   7.537 +fun is_quasi_fol_theorem thy =
   7.538 +  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
   7.539 +
   7.540 +(* Trivial problem, which resolution cannot handle (empty clause) *)
   7.541 +exception TRIVIAL of unit
   7.542 +
   7.543 +(* making axiom and conjecture clauses *)
   7.544 +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
   7.545 +  let
   7.546 +    val (skolem_somes, t) =
   7.547 +      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
   7.548 +    val (lits, ctypes_sorts) = literals_of_term thy t
   7.549 +  in
   7.550 +    if forall isFalse lits then
   7.551 +      raise TRIVIAL ()
   7.552 +    else
   7.553 +      (skolem_somes,
   7.554 +       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   7.555 +                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   7.556 +  end
   7.557 +
   7.558 +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
   7.559 +  let
   7.560 +    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   7.561 +  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   7.562 +
   7.563 +fun make_axiom_clauses thy clauses =
   7.564 +  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
   7.565 +
   7.566 +fun make_conjecture_clauses thy =
   7.567 +  let
   7.568 +    fun aux _ _ [] = []
   7.569 +      | aux n skolem_somes (th :: ths) =
   7.570 +        let
   7.571 +          val (skolem_somes, cls) =
   7.572 +            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
   7.573 +        in cls :: aux (n + 1) skolem_somes ths end
   7.574 +  in aux 0 [] end
   7.575 +
   7.576 +(** Helper clauses **)
   7.577 +
   7.578 +fun count_combterm (CombConst ((c, _), _, _)) =
   7.579 +    Symtab.map_entry c (Integer.add 1)
   7.580 +  | count_combterm (CombVar _) = I
   7.581 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   7.582 +fun count_literal (Literal (_, t)) = count_combterm t
   7.583 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   7.584 +
   7.585 +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
   7.586 +fun cnf_helper_thms thy raw =
   7.587 +  map (`Thm.get_name_hint)
   7.588 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   7.589 +
   7.590 +val optional_helpers =
   7.591 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   7.592 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   7.593 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
   7.594 +val optional_typed_helpers =
   7.595 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
   7.596 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   7.597 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   7.598 +
   7.599 +val init_counters =
   7.600 +  Symtab.make (maps (maps (map (rpair 0) o fst))
   7.601 +                    [optional_helpers, optional_typed_helpers])
   7.602 +
   7.603 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
   7.604 +  let
   7.605 +    val axclauses = map snd (make_axiom_clauses thy axcls)
   7.606 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   7.607 +    fun is_needed c = the (Symtab.lookup ct c) > 0
   7.608 +    val cnfs =
   7.609 +      (optional_helpers
   7.610 +       |> full_types ? append optional_typed_helpers
   7.611 +       |> maps (fn (ss, (raw, ths)) =>
   7.612 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
   7.613 +                   else []))
   7.614 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   7.615 +  in map snd (make_axiom_clauses thy cnfs) end
   7.616 +
   7.617 +fun make_clause_table xs =
   7.618 +  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
   7.619 +
   7.620 +
   7.621 +(***************************************************************)
   7.622 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
   7.623 +(***************************************************************)
   7.624 +
   7.625 +fun set_insert (x, s) = Symtab.update (x, ()) s
   7.626 +
   7.627 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   7.628 +
   7.629 +(*Remove this trivial type class*)
   7.630 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   7.631 +
   7.632 +fun tfree_classes_of_terms ts =
   7.633 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   7.634 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   7.635 +
   7.636 +fun tvar_classes_of_terms ts =
   7.637 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   7.638 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   7.639 +
   7.640 +(*fold type constructors*)
   7.641 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   7.642 +  | fold_type_consts _ _ x = x;
   7.643 +
   7.644 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   7.645 +fun add_type_consts_in_term thy =
   7.646 +  let
   7.647 +    val const_typargs = Sign.const_typargs thy
   7.648 +    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   7.649 +      | aux (Abs (_, _, u)) = aux u
   7.650 +      | aux (Const (@{const_name skolem_id}, _) $ _) = I
   7.651 +      | aux (t $ u) = aux t #> aux u
   7.652 +      | aux _ = I
   7.653 +  in aux end
   7.654 +
   7.655 +fun type_consts_of_terms thy ts =
   7.656 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   7.657 +
   7.658 +(* Remove existing axiom clauses from the conjecture clauses, as this can
   7.659 +   dramatically boost an ATP's performance (for some reason). *)
   7.660 +fun subtract_cls ax_clauses =
   7.661 +  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   7.662 +
   7.663 +(* prepare for passing to writer,
   7.664 +   create additional clauses based on the information from extra_cls *)
   7.665 +fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   7.666 +  let
   7.667 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   7.668 +    val ccls = subtract_cls extra_cls goal_cls
   7.669 +    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   7.670 +    val ccltms = map prop_of ccls
   7.671 +    and axtms = map (prop_of o #1) extra_cls
   7.672 +    val subs = tfree_classes_of_terms ccltms
   7.673 +    and supers = tvar_classes_of_terms axtms
   7.674 +    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   7.675 +    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   7.676 +    val conjectures = make_conjecture_clauses thy ccls
   7.677 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   7.678 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   7.679 +    val helper_clauses =
   7.680 +      get_helper_clauses thy is_FO full_types conjectures extra_cls
   7.681 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   7.682 +    val classrel_clauses = make_classrel_clauses thy subs supers'
   7.683 +  in
   7.684 +    (Vector.fromList clnames,
   7.685 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   7.686 +  end
   7.687 +
   7.688 +end;
     8.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:42:06 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 17:08:39 2010 +0200
     8.3 @@ -19,8 +19,7 @@
     8.4  struct
     8.5  
     8.6  open Clausifier
     8.7 -open Sledgehammer_Util
     8.8 -open Sledgehammer_FOL_Clause
     8.9 +open Metis_Clauses
    8.10  
    8.11  exception METIS of string * string
    8.12  
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 16:42:06 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 17:08:39 2010 +0200
     9.3 @@ -22,7 +22,7 @@
     9.4  struct
     9.5  
     9.6  open Clausifier
     9.7 -open Sledgehammer_FOL_Clause
     9.8 +open Metis_Clauses
     9.9  
    9.10  (* Experimental feature: Filter theorems in natural form or in CNF? *)
    9.11  val use_natural_form = Unsynchronized.ref false
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:42:06 2010 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 17:08:39 2010 +0200
    10.3 @@ -19,8 +19,8 @@
    10.4  struct
    10.5  
    10.6  open Clausifier
    10.7 +open Metis_Clauses
    10.8  open Sledgehammer_Util
    10.9 -open Sledgehammer_FOL_Clause
   10.10  open Sledgehammer_Proof_Reconstruct
   10.11  open ATP_Manager
   10.12  
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Jun 25 16:42:06 2010 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,685 +0,0 @@
    11.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
    11.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory
    11.6 -    Author:     Jasmin Blanchette, TU Muenchen
    11.7 -
    11.8 -Storing/printing FOL clauses and arity clauses.  Typed equality is
    11.9 -treated differently.
   11.10 -*)
   11.11 -
   11.12 -signature SLEDGEHAMMER_FOL_CLAUSE =
   11.13 -sig
   11.14 -  type cnf_thm = Clausifier.cnf_thm
   11.15 -  type name = string * string
   11.16 -  type name_pool = string Symtab.table * string Symtab.table
   11.17 -  datatype kind = Axiom | Conjecture
   11.18 -  datatype type_literal =
   11.19 -    TyLitVar of string * name |
   11.20 -    TyLitFree of string * name
   11.21 -  datatype arLit =
   11.22 -      TConsLit of class * string * string list
   11.23 -    | TVarLit of class * string
   11.24 -  datatype arity_clause = ArityClause of
   11.25 -   {axiom_name: string, conclLit: arLit, premLits: arLit list}
   11.26 -  datatype classrel_clause = ClassrelClause of
   11.27 -   {axiom_name: string, subclass: class, superclass: class}
   11.28 -  datatype combtyp =
   11.29 -    TyVar of name |
   11.30 -    TyFree of name |
   11.31 -    TyConstr of name * combtyp list
   11.32 -  datatype combterm =
   11.33 -    CombConst of name * combtyp * combtyp list (* Const and Free *) |
   11.34 -    CombVar of name * combtyp |
   11.35 -    CombApp of combterm * combterm
   11.36 -  datatype literal = Literal of bool * combterm
   11.37 -  datatype hol_clause =
   11.38 -    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
   11.39 -                  literals: literal list, ctypes_sorts: typ list}
   11.40 -  exception TRIVIAL of unit
   11.41 -
   11.42 -  val type_wrapper_name : string
   11.43 -  val schematic_var_prefix: string
   11.44 -  val fixed_var_prefix: string
   11.45 -  val tvar_prefix: string
   11.46 -  val tfree_prefix: string
   11.47 -  val const_prefix: string
   11.48 -  val tconst_prefix: string
   11.49 -  val class_prefix: string
   11.50 -  val union_all: ''a list list -> ''a list
   11.51 -  val invert_const: string -> string
   11.52 -  val ascii_of: string -> string
   11.53 -  val undo_ascii_of: string -> string
   11.54 -  val strip_prefix: string -> string -> string option
   11.55 -  val make_schematic_var : string * int -> string
   11.56 -  val make_fixed_var : string -> string
   11.57 -  val make_schematic_type_var : string * int -> string
   11.58 -  val make_fixed_type_var : string -> string
   11.59 -  val make_fixed_const : string -> string
   11.60 -  val make_fixed_type_const : string -> string
   11.61 -  val make_type_class : string -> string
   11.62 -  val empty_name_pool : bool -> name_pool option
   11.63 -  val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   11.64 -  val nice_name : name -> name_pool option -> string * name_pool option
   11.65 -  val type_literals_for_types : typ list -> type_literal list
   11.66 -  val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
   11.67 -  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   11.68 -  val type_of_combterm : combterm -> combtyp
   11.69 -  val strip_combterm_comb : combterm -> combterm * combterm list
   11.70 -  val literals_of_term : theory -> term -> literal list * typ list
   11.71 -  val conceal_skolem_somes :
   11.72 -    int -> (string * term) list -> term -> (string * term) list * term
   11.73 -  val is_quasi_fol_theorem : theory -> thm -> bool
   11.74 -  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
   11.75 -  val tfree_classes_of_terms : term list -> string list
   11.76 -  val tvar_classes_of_terms : term list -> string list
   11.77 -  val type_consts_of_terms : theory -> term list -> string list
   11.78 -  val prepare_clauses :
   11.79 -    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
   11.80 -    -> string vector
   11.81 -       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
   11.82 -          * classrel_clause list * arity_clause list)
   11.83 -end
   11.84 -
   11.85 -structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
   11.86 -struct
   11.87 -
   11.88 -open Clausifier
   11.89 -
   11.90 -val type_wrapper_name = "ti"
   11.91 -
   11.92 -val schematic_var_prefix = "V_";
   11.93 -val fixed_var_prefix = "v_";
   11.94 -
   11.95 -val tvar_prefix = "T_";
   11.96 -val tfree_prefix = "t_";
   11.97 -
   11.98 -val classrel_clause_prefix = "clsrel_";
   11.99 -
  11.100 -val const_prefix = "c_";
  11.101 -val tconst_prefix = "tc_";
  11.102 -val class_prefix = "class_";
  11.103 -
  11.104 -fun union_all xss = fold (union (op =)) xss []
  11.105 -
  11.106 -(* Readable names for the more common symbolic functions. Do not mess with the
  11.107 -   last nine entries of the table unless you know what you are doing. *)
  11.108 -val const_trans_table =
  11.109 -  Symtab.make [(@{const_name "op ="}, "equal"),
  11.110 -               (@{const_name "op &"}, "and"),
  11.111 -               (@{const_name "op |"}, "or"),
  11.112 -               (@{const_name "op -->"}, "implies"),
  11.113 -               (@{const_name "op :"}, "in"),
  11.114 -               (@{const_name fequal}, "fequal"),
  11.115 -               (@{const_name COMBI}, "COMBI"),
  11.116 -               (@{const_name COMBK}, "COMBK"),
  11.117 -               (@{const_name COMBB}, "COMBB"),
  11.118 -               (@{const_name COMBC}, "COMBC"),
  11.119 -               (@{const_name COMBS}, "COMBS"),
  11.120 -               (@{const_name True}, "True"),
  11.121 -               (@{const_name False}, "False"),
  11.122 -               (@{const_name If}, "If"),
  11.123 -               (@{type_name "*"}, "prod"),
  11.124 -               (@{type_name "+"}, "sum")]
  11.125 -
  11.126 -(* Invert the table of translations between Isabelle and ATPs. *)
  11.127 -val const_trans_table_inv =
  11.128 -  Symtab.update ("fequal", @{const_name "op ="})
  11.129 -                (Symtab.make (map swap (Symtab.dest const_trans_table)))
  11.130 -
  11.131 -val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
  11.132 -
  11.133 -(*Escaping of special characters.
  11.134 -  Alphanumeric characters are left unchanged.
  11.135 -  The character _ goes to __
  11.136 -  Characters in the range ASCII space to / go to _A to _P, respectively.
  11.137 -  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
  11.138 -val A_minus_space = Char.ord #"A" - Char.ord #" ";
  11.139 -
  11.140 -fun stringN_of_int 0 _ = ""
  11.141 -  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
  11.142 -
  11.143 -fun ascii_of_c c =
  11.144 -  if Char.isAlphaNum c then String.str c
  11.145 -  else if c = #"_" then "__"
  11.146 -  else if #" " <= c andalso c <= #"/"
  11.147 -       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
  11.148 -  else if Char.isPrint c
  11.149 -       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
  11.150 -  else ""
  11.151 -
  11.152 -val ascii_of = String.translate ascii_of_c;
  11.153 -
  11.154 -(** Remove ASCII armouring from names in proof files **)
  11.155 -
  11.156 -(*We don't raise error exceptions because this code can run inside the watcher.
  11.157 -  Also, the errors are "impossible" (hah!)*)
  11.158 -fun undo_ascii_aux rcs [] = String.implode(rev rcs)
  11.159 -  | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
  11.160 -      (*Three types of _ escapes: __, _A to _P, _nnn*)
  11.161 -  | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
  11.162 -  | undo_ascii_aux rcs (#"_" :: c :: cs) =
  11.163 -      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
  11.164 -      then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
  11.165 -      else
  11.166 -        let val digits = List.take (c::cs, 3) handle Subscript => []
  11.167 -        in
  11.168 -            case Int.fromString (String.implode digits) of
  11.169 -                NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
  11.170 -              | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
  11.171 -        end
  11.172 -  | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
  11.173 -
  11.174 -val undo_ascii_of = undo_ascii_aux [] o String.explode;
  11.175 -
  11.176 -(* If string s has the prefix s1, return the result of deleting it,
  11.177 -   un-ASCII'd. *)
  11.178 -fun strip_prefix s1 s =
  11.179 -  if String.isPrefix s1 s then
  11.180 -    SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
  11.181 -  else
  11.182 -    NONE
  11.183 -
  11.184 -(*Remove the initial ' character from a type variable, if it is present*)
  11.185 -fun trim_type_var s =
  11.186 -  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
  11.187 -  else error ("trim_type: Malformed type variable encountered: " ^ s);
  11.188 -
  11.189 -fun ascii_of_indexname (v,0) = ascii_of v
  11.190 -  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
  11.191 -
  11.192 -fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
  11.193 -fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
  11.194 -
  11.195 -fun make_schematic_type_var (x,i) =
  11.196 -      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
  11.197 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
  11.198 -
  11.199 -fun lookup_const c =
  11.200 -  case Symtab.lookup const_trans_table c of
  11.201 -    SOME c' => c'
  11.202 -  | NONE => ascii_of c
  11.203 -
  11.204 -(* "op =" MUST BE "equal" because it's built into ATPs. *)
  11.205 -fun make_fixed_const @{const_name "op ="} = "equal"
  11.206 -  | make_fixed_const c = const_prefix ^ lookup_const c
  11.207 -
  11.208 -fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
  11.209 -
  11.210 -fun make_type_class clas = class_prefix ^ ascii_of clas;
  11.211 -
  11.212 -
  11.213 -(**** name pool ****)
  11.214 - 
  11.215 -type name = string * string
  11.216 -type name_pool = string Symtab.table * string Symtab.table
  11.217 -
  11.218 -fun empty_name_pool readable_names =
  11.219 -  if readable_names then SOME (`I Symtab.empty) else NONE
  11.220 -
  11.221 -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
  11.222 -fun pool_map f xs =
  11.223 -  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
  11.224 -
  11.225 -fun add_nice_name full_name nice_prefix j the_pool =
  11.226 -  let
  11.227 -    val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
  11.228 -  in
  11.229 -    case Symtab.lookup (snd the_pool) nice_name of
  11.230 -      SOME full_name' =>
  11.231 -      if full_name = full_name' then (nice_name, the_pool)
  11.232 -      else add_nice_name full_name nice_prefix (j + 1) the_pool
  11.233 -    | NONE =>
  11.234 -      (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
  11.235 -                   Symtab.update_new (nice_name, full_name) (snd the_pool)))
  11.236 -  end
  11.237 -
  11.238 -fun translate_first_char f s =
  11.239 -  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
  11.240 -
  11.241 -fun readable_name full_name s =
  11.242 -  let
  11.243 -    val s = s |> Long_Name.base_name |> Name.desymbolize false
  11.244 -    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
  11.245 -    val s' =
  11.246 -      (s' |> rev
  11.247 -          |> implode
  11.248 -          |> String.translate
  11.249 -                 (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
  11.250 -                          else ""))
  11.251 -      ^ replicate_string (String.size s - length s') "_"
  11.252 -    val s' =
  11.253 -      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
  11.254 -      else s'
  11.255 -    (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
  11.256 -       ("op &", "op |", etc.). *)
  11.257 -    val s' = if s' = "equal" orelse s' = "op" then full_name else s'
  11.258 -  in
  11.259 -    case (Char.isLower (String.sub (full_name, 0)),
  11.260 -          Char.isLower (String.sub (s', 0))) of
  11.261 -      (true, false) => translate_first_char Char.toLower s'
  11.262 -    | (false, true) => translate_first_char Char.toUpper s'
  11.263 -    | _ => s'
  11.264 -  end
  11.265 -
  11.266 -fun nice_name (full_name, _) NONE = (full_name, NONE)
  11.267 -  | nice_name (full_name, desired_name) (SOME the_pool) =
  11.268 -    case Symtab.lookup (fst the_pool) full_name of
  11.269 -      SOME nice_name => (nice_name, SOME the_pool)
  11.270 -    | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
  11.271 -                            the_pool
  11.272 -              |> apsnd SOME
  11.273 -
  11.274 -(**** Definitions and functions for FOL clauses for TPTP format output ****)
  11.275 -
  11.276 -datatype kind = Axiom | Conjecture
  11.277 -
  11.278 -(**** Isabelle FOL clauses ****)
  11.279 -
  11.280 -(* The first component is the type class; the second is a TVar or TFree. *)
  11.281 -datatype type_literal =
  11.282 -  TyLitVar of string * name |
  11.283 -  TyLitFree of string * name
  11.284 -
  11.285 -exception CLAUSE of string * term;
  11.286 -
  11.287 -(*Make literals for sorted type variables*)
  11.288 -fun sorts_on_typs_aux (_, [])   = []
  11.289 -  | sorts_on_typs_aux ((x,i),  s::ss) =
  11.290 -      let val sorts = sorts_on_typs_aux ((x,i), ss)
  11.291 -      in
  11.292 -          if s = "HOL.type" then sorts
  11.293 -          else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
  11.294 -          else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
  11.295 -      end;
  11.296 -
  11.297 -fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
  11.298 -  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
  11.299 -
  11.300 -(*Given a list of sorted type variables, return a list of type literals.*)
  11.301 -fun type_literals_for_types Ts =
  11.302 -  fold (union (op =)) (map sorts_on_typs Ts) []
  11.303 -
  11.304 -(** make axiom and conjecture clauses. **)
  11.305 -
  11.306 -(**** Isabelle arities ****)
  11.307 -
  11.308 -datatype arLit = TConsLit of class * string * string list
  11.309 -               | TVarLit of class * string;
  11.310 -
  11.311 -datatype arity_clause =
  11.312 -  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
  11.313 -
  11.314 -
  11.315 -fun gen_TVars 0 = []
  11.316 -  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
  11.317 -
  11.318 -fun pack_sort(_,[])  = []
  11.319 -  | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
  11.320 -  | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
  11.321 -
  11.322 -(*Arity of type constructor tcon :: (arg1,...,argN)res*)
  11.323 -fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
  11.324 -   let val tvars = gen_TVars (length args)
  11.325 -       val tvars_srts = ListPair.zip (tvars,args)
  11.326 -   in
  11.327 -     ArityClause {axiom_name = axiom_name, 
  11.328 -                  conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
  11.329 -                  premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
  11.330 -   end;
  11.331 -
  11.332 -
  11.333 -(**** Isabelle class relations ****)
  11.334 -
  11.335 -datatype classrel_clause =
  11.336 -  ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
  11.337 -
  11.338 -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
  11.339 -fun class_pairs _ [] _ = []
  11.340 -  | class_pairs thy subs supers =
  11.341 -      let
  11.342 -        val class_less = Sorts.class_less (Sign.classes_of thy)
  11.343 -        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
  11.344 -        fun add_supers sub = fold (add_super sub) supers
  11.345 -      in fold add_supers subs [] end
  11.346 -
  11.347 -fun make_classrel_clause (sub,super) =
  11.348 -  ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
  11.349 -                               ascii_of super,
  11.350 -                  subclass = make_type_class sub,
  11.351 -                  superclass = make_type_class super};
  11.352 -
  11.353 -fun make_classrel_clauses thy subs supers =
  11.354 -  map make_classrel_clause (class_pairs thy subs supers);
  11.355 -
  11.356 -
  11.357 -(** Isabelle arities **)
  11.358 -
  11.359 -fun arity_clause _ _ (_, []) = []
  11.360 -  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
  11.361 -      arity_clause seen n (tcons,ars)
  11.362 -  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
  11.363 -      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
  11.364 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
  11.365 -          arity_clause seen (n+1) (tcons,ars)
  11.366 -      else
  11.367 -          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
  11.368 -          arity_clause (class::seen) n (tcons,ars)
  11.369 -
  11.370 -fun multi_arity_clause [] = []
  11.371 -  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
  11.372 -      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
  11.373 -
  11.374 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
  11.375 -  provided its arguments have the corresponding sorts.*)
  11.376 -fun type_class_pairs thy tycons classes =
  11.377 -  let val alg = Sign.classes_of thy
  11.378 -      fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
  11.379 -      fun add_class tycon class =
  11.380 -        cons (class, domain_sorts tycon class)
  11.381 -        handle Sorts.CLASS_ERROR _ => I
  11.382 -      fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
  11.383 -  in  map try_classes tycons  end;
  11.384 -
  11.385 -(*Proving one (tycon, class) membership may require proving others, so iterate.*)
  11.386 -fun iter_type_class_pairs _ _ [] = ([], [])
  11.387 -  | iter_type_class_pairs thy tycons classes =
  11.388 -      let val cpairs = type_class_pairs thy tycons classes
  11.389 -          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
  11.390 -            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
  11.391 -          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
  11.392 -      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
  11.393 -
  11.394 -fun make_arity_clauses thy tycons classes =
  11.395 -  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
  11.396 -  in  (classes', multi_arity_clause cpairs)  end;
  11.397 -
  11.398 -datatype combtyp =
  11.399 -  TyVar of name |
  11.400 -  TyFree of name |
  11.401 -  TyConstr of name * combtyp list
  11.402 -
  11.403 -datatype combterm =
  11.404 -  CombConst of name * combtyp * combtyp list (* Const and Free *) |
  11.405 -  CombVar of name * combtyp |
  11.406 -  CombApp of combterm * combterm
  11.407 -
  11.408 -datatype literal = Literal of bool * combterm
  11.409 -
  11.410 -datatype hol_clause =
  11.411 -  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
  11.412 -                literals: literal list, ctypes_sorts: typ list}
  11.413 -
  11.414 -(*********************************************************************)
  11.415 -(* convert a clause with type Term.term to a clause with type clause *)
  11.416 -(*********************************************************************)
  11.417 -
  11.418 -(*Result of a function type; no need to check that the argument type matches.*)
  11.419 -fun result_type (TyConstr (_, [_, tp2])) = tp2
  11.420 -  | result_type _ = raise Fail "non-function type"
  11.421 -
  11.422 -fun type_of_combterm (CombConst (_, tp, _)) = tp
  11.423 -  | type_of_combterm (CombVar (_, tp)) = tp
  11.424 -  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
  11.425 -
  11.426 -(*gets the head of a combinator application, along with the list of arguments*)
  11.427 -fun strip_combterm_comb u =
  11.428 -    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
  11.429 -        |   stripc  x =  x
  11.430 -    in stripc(u,[]) end
  11.431 -
  11.432 -fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
  11.433 -      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
  11.434 -  | isFalse _ = false;
  11.435 -
  11.436 -fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
  11.437 -      (pol andalso c = "c_True") orelse
  11.438 -      (not pol andalso c = "c_False")
  11.439 -  | isTrue _ = false;
  11.440 -
  11.441 -fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
  11.442 -
  11.443 -fun type_of (Type (a, Ts)) =
  11.444 -    let val (folTypes,ts) = types_of Ts in
  11.445 -      (TyConstr (`make_fixed_type_const a, folTypes), ts)
  11.446 -    end
  11.447 -  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
  11.448 -  | type_of (tp as TVar (x, _)) =
  11.449 -    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
  11.450 -and types_of Ts =
  11.451 -    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
  11.452 -      (folTyps, union_all ts)
  11.453 -    end
  11.454 -
  11.455 -(* same as above, but no gathering of sort information *)
  11.456 -fun simp_type_of (Type (a, Ts)) =
  11.457 -      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
  11.458 -  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
  11.459 -  | simp_type_of (TVar (x, _)) =
  11.460 -    TyVar (make_schematic_type_var x, string_of_indexname x)
  11.461 -
  11.462 -(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
  11.463 -fun combterm_of thy (Const (c, T)) =
  11.464 -      let
  11.465 -        val (tp, ts) = type_of T
  11.466 -        val tvar_list =
  11.467 -          (if String.isPrefix skolem_theory_name c then
  11.468 -             [] |> Term.add_tvarsT T |> map TVar
  11.469 -           else
  11.470 -             (c, T) |> Sign.const_typargs thy)
  11.471 -          |> map simp_type_of
  11.472 -        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
  11.473 -      in  (c',ts)  end
  11.474 -  | combterm_of _ (Free(v, T)) =
  11.475 -      let val (tp,ts) = type_of T
  11.476 -          val v' = CombConst (`make_fixed_var v, tp, [])
  11.477 -      in  (v',ts)  end
  11.478 -  | combterm_of _ (Var(v, T)) =
  11.479 -      let val (tp,ts) = type_of T
  11.480 -          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
  11.481 -      in  (v',ts)  end
  11.482 -  | combterm_of thy (P $ Q) =
  11.483 -      let val (P', tsP) = combterm_of thy P
  11.484 -          val (Q', tsQ) = combterm_of thy Q
  11.485 -      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
  11.486 -  | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
  11.487 -
  11.488 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
  11.489 -  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
  11.490 -
  11.491 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
  11.492 -    literals_of_term1 args thy P
  11.493 -  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
  11.494 -    literals_of_term1 (literals_of_term1 args thy P) thy Q
  11.495 -  | literals_of_term1 (lits, ts) thy P =
  11.496 -    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
  11.497 -      (Literal (pol, pred) :: lits, union (op =) ts ts')
  11.498 -    end
  11.499 -val literals_of_term = literals_of_term1 ([], [])
  11.500 -
  11.501 -fun skolem_name i j num_T_args =
  11.502 -  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
  11.503 -  skolem_infix ^ "g"
  11.504 -
  11.505 -fun conceal_skolem_somes i skolem_somes t =
  11.506 -  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
  11.507 -    let
  11.508 -      fun aux skolem_somes
  11.509 -              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
  11.510 -          let
  11.511 -            val (skolem_somes, s) =
  11.512 -              if i = ~1 then
  11.513 -                (skolem_somes, @{const_name undefined})
  11.514 -              else case AList.find (op aconv) skolem_somes t of
  11.515 -                s :: _ => (skolem_somes, s)
  11.516 -              | [] =>
  11.517 -                let
  11.518 -                  val s = skolem_theory_name ^ "." ^
  11.519 -                          skolem_name i (length skolem_somes)
  11.520 -                                        (length (Term.add_tvarsT T []))
  11.521 -                in ((s, t) :: skolem_somes, s) end
  11.522 -          in (skolem_somes, Const (s, T)) end
  11.523 -        | aux skolem_somes (t1 $ t2) =
  11.524 -          let
  11.525 -            val (skolem_somes, t1) = aux skolem_somes t1
  11.526 -            val (skolem_somes, t2) = aux skolem_somes t2
  11.527 -          in (skolem_somes, t1 $ t2) end
  11.528 -        | aux skolem_somes (Abs (s, T, t')) =
  11.529 -          let val (skolem_somes, t') = aux skolem_somes t' in
  11.530 -            (skolem_somes, Abs (s, T, t'))
  11.531 -          end
  11.532 -        | aux skolem_somes t = (skolem_somes, t)
  11.533 -    in aux skolem_somes t end
  11.534 -  else
  11.535 -    (skolem_somes, t)
  11.536 -
  11.537 -fun is_quasi_fol_theorem thy =
  11.538 -  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
  11.539 -
  11.540 -(* Trivial problem, which resolution cannot handle (empty clause) *)
  11.541 -exception TRIVIAL of unit
  11.542 -
  11.543 -(* making axiom and conjecture clauses *)
  11.544 -fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
  11.545 -  let
  11.546 -    val (skolem_somes, t) =
  11.547 -      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
  11.548 -    val (lits, ctypes_sorts) = literals_of_term thy t
  11.549 -  in
  11.550 -    if forall isFalse lits then
  11.551 -      raise TRIVIAL ()
  11.552 -    else
  11.553 -      (skolem_somes,
  11.554 -       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
  11.555 -                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
  11.556 -  end
  11.557 -
  11.558 -fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
  11.559 -  let
  11.560 -    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
  11.561 -  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
  11.562 -
  11.563 -fun make_axiom_clauses thy clauses =
  11.564 -  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
  11.565 -
  11.566 -fun make_conjecture_clauses thy =
  11.567 -  let
  11.568 -    fun aux _ _ [] = []
  11.569 -      | aux n skolem_somes (th :: ths) =
  11.570 -        let
  11.571 -          val (skolem_somes, cls) =
  11.572 -            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
  11.573 -        in cls :: aux (n + 1) skolem_somes ths end
  11.574 -  in aux 0 [] end
  11.575 -
  11.576 -(** Helper clauses **)
  11.577 -
  11.578 -fun count_combterm (CombConst ((c, _), _, _)) =
  11.579 -    Symtab.map_entry c (Integer.add 1)
  11.580 -  | count_combterm (CombVar _) = I
  11.581 -  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
  11.582 -fun count_literal (Literal (_, t)) = count_combterm t
  11.583 -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
  11.584 -
  11.585 -fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
  11.586 -fun cnf_helper_thms thy raw =
  11.587 -  map (`Thm.get_name_hint)
  11.588 -  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
  11.589 -
  11.590 -val optional_helpers =
  11.591 -  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
  11.592 -   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
  11.593 -   (["c_COMBS"], (false, @{thms COMBS_def}))]
  11.594 -val optional_typed_helpers =
  11.595 -  [(["c_True", "c_False"], (true, @{thms True_or_False})),
  11.596 -   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
  11.597 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
  11.598 -
  11.599 -val init_counters =
  11.600 -  Symtab.make (maps (maps (map (rpair 0) o fst))
  11.601 -                    [optional_helpers, optional_typed_helpers])
  11.602 -
  11.603 -fun get_helper_clauses thy is_FO full_types conjectures axcls =
  11.604 -  let
  11.605 -    val axclauses = map snd (make_axiom_clauses thy axcls)
  11.606 -    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
  11.607 -    fun is_needed c = the (Symtab.lookup ct c) > 0
  11.608 -    val cnfs =
  11.609 -      (optional_helpers
  11.610 -       |> full_types ? append optional_typed_helpers
  11.611 -       |> maps (fn (ss, (raw, ths)) =>
  11.612 -                   if exists is_needed ss then cnf_helper_thms thy raw ths
  11.613 -                   else []))
  11.614 -      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
  11.615 -  in map snd (make_axiom_clauses thy cnfs) end
  11.616 -
  11.617 -fun make_clause_table xs =
  11.618 -  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
  11.619 -
  11.620 -
  11.621 -(***************************************************************)
  11.622 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
  11.623 -(***************************************************************)
  11.624 -
  11.625 -fun set_insert (x, s) = Symtab.update (x, ()) s
  11.626 -
  11.627 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  11.628 -
  11.629 -(*Remove this trivial type class*)
  11.630 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
  11.631 -
  11.632 -fun tfree_classes_of_terms ts =
  11.633 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
  11.634 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  11.635 -
  11.636 -fun tvar_classes_of_terms ts =
  11.637 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
  11.638 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
  11.639 -
  11.640 -(*fold type constructors*)
  11.641 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
  11.642 -  | fold_type_consts _ _ x = x;
  11.643 -
  11.644 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
  11.645 -fun add_type_consts_in_term thy =
  11.646 -  let
  11.647 -    val const_typargs = Sign.const_typargs thy
  11.648 -    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
  11.649 -      | aux (Abs (_, _, u)) = aux u
  11.650 -      | aux (Const (@{const_name skolem_id}, _) $ _) = I
  11.651 -      | aux (t $ u) = aux t #> aux u
  11.652 -      | aux _ = I
  11.653 -  in aux end
  11.654 -
  11.655 -fun type_consts_of_terms thy ts =
  11.656 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
  11.657 -
  11.658 -(* Remove existing axiom clauses from the conjecture clauses, as this can
  11.659 -   dramatically boost an ATP's performance (for some reason). *)
  11.660 -fun subtract_cls ax_clauses =
  11.661 -  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
  11.662 -
  11.663 -(* prepare for passing to writer,
  11.664 -   create additional clauses based on the information from extra_cls *)
  11.665 -fun prepare_clauses full_types goal_cls axcls extra_cls thy =
  11.666 -  let
  11.667 -    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
  11.668 -    val ccls = subtract_cls extra_cls goal_cls
  11.669 -    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
  11.670 -    val ccltms = map prop_of ccls
  11.671 -    and axtms = map (prop_of o #1) extra_cls
  11.672 -    val subs = tfree_classes_of_terms ccltms
  11.673 -    and supers = tvar_classes_of_terms axtms
  11.674 -    and tycons = type_consts_of_terms thy (ccltms @ axtms)
  11.675 -    (*TFrees in conjecture clauses; TVars in axiom clauses*)
  11.676 -    val conjectures = make_conjecture_clauses thy ccls
  11.677 -    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
  11.678 -    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
  11.679 -    val helper_clauses =
  11.680 -      get_helper_clauses thy is_FO full_types conjectures extra_cls
  11.681 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  11.682 -    val classrel_clauses = make_classrel_clauses thy subs supers'
  11.683 -  in
  11.684 -    (Vector.fromList clnames,
  11.685 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
  11.686 -  end
  11.687 -
  11.688 -end;
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 16:42:06 2010 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 25 17:08:39 2010 +0200
    12.3 @@ -8,7 +8,7 @@
    12.4  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
    12.5  sig
    12.6    type minimize_command = string list -> string
    12.7 -  type name_pool = Sledgehammer_FOL_Clause.name_pool
    12.8 +  type name_pool = Metis_Clauses.name_pool
    12.9  
   12.10    val metis_line: bool -> int -> int -> string list -> string
   12.11    val metis_proof_text:
   12.12 @@ -28,8 +28,8 @@
   12.13  struct
   12.14  
   12.15  open Clausifier
   12.16 +open Metis_Clauses
   12.17  open Sledgehammer_Util
   12.18 -open Sledgehammer_FOL_Clause
   12.19  
   12.20  type minimize_command = string list -> string
   12.21  
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jun 25 16:42:06 2010 +0200
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jun 25 17:08:39 2010 +0200
    13.3 @@ -7,11 +7,11 @@
    13.4  
    13.5  signature SLEDGEHAMMER_TPTP_FORMAT =
    13.6  sig
    13.7 -  type name_pool = Sledgehammer_FOL_Clause.name_pool
    13.8 -  type type_literal = Sledgehammer_FOL_Clause.type_literal
    13.9 -  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   13.10 -  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
   13.11 -  type hol_clause = Sledgehammer_FOL_Clause.hol_clause
   13.12 +  type name_pool = Metis_Clauses.name_pool
   13.13 +  type type_literal = Metis_Clauses.type_literal
   13.14 +  type classrel_clause = Metis_Clauses.classrel_clause
   13.15 +  type arity_clause = Metis_Clauses.arity_clause
   13.16 +  type hol_clause = Metis_Clauses.hol_clause
   13.17  
   13.18    val tptp_of_type_literal :
   13.19      bool -> type_literal -> name_pool option -> string * name_pool option
   13.20 @@ -25,8 +25,8 @@
   13.21  structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
   13.22  struct
   13.23  
   13.24 +open Metis_Clauses
   13.25  open Sledgehammer_Util
   13.26 -open Sledgehammer_FOL_Clause
   13.27  
   13.28  type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   13.29