# HG changeset patch
# User blanchet
# Date 1274084294 -7200
# Node ID adc11fb3f3aa727355b9dd1d4f2f959cc7e65872
# Parent  67ae217c6b5c6eae783710c24f8adf1426c1dbcf
generate proper arity declarations for TFrees for SPASS's DFG format;
and renamed a confusing function in the process

diff -r 67ae217c6b5c -r adc11fb3f3aa src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon May 17 10:16:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon May 17 10:18:14 2010 +0200
@@ -141,9 +141,10 @@
   in
       if is_conjecture then
           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
-           add_type_literals types_sorts)
+           type_literals_for_types types_sorts)
       else
-        let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
+        let val tylits = filter_out (default_sort ctxt) types_sorts
+                         |> type_literals_for_types
             val mtylits = if Config.get ctxt type_lits
                           then map (metis_of_type_literals false) tylits else []
         in
@@ -599,9 +600,9 @@
 
 (*Extract TFree constraints from context to include as conjecture clauses*)
 fun init_tfrees ctxt =
-  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
-  in
-    add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
+  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
+    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
+    |> type_literals_for_types
   end;
 
 (*transform isabelle type / arity clause to metis clause *)
diff -r 67ae217c6b5c -r adc11fb3f3aa src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon May 17 10:16:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon May 17 10:18:14 2010 +0200
@@ -48,7 +48,7 @@
     TyLitVar of string * name |
     TyLitFree of string * name
   exception CLAUSE of string * term
-  val add_type_literals : typ list -> type_literal list
+  val type_literals_for_types : typ list -> type_literal list
   val get_tvar_strs: typ list -> string list
   datatype arLit =
       TConsLit of class * string * string list
@@ -331,7 +331,8 @@
   | pred_of_sort (TyLitFree (s, _)) = (s, 1)
 
 (*Given a list of sorted type variables, return a list of type literals.*)
-fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
+fun type_literals_for_types Ts =
+  fold (union (op =)) (map sorts_on_typs Ts) []
 
 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -520,7 +521,7 @@
       dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
       string_of_clausename (cls_id,ax_name) ^  ").\n\n";
 
-fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
+fun string_of_arity (name, arity) =  "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
 
 fun string_of_preds [] = ""
   | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
diff -r 67ae217c6b5c -r adc11fb3f3aa src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon May 17 10:16:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon May 17 10:18:14 2010 +0200
@@ -300,7 +300,7 @@
   let
     val (lits, pool) = pool_map (tptp_literal params) literals pool
     val (tylits, pool) = pool_map (tptp_of_type_literal pos)
-                                  (add_type_literals ctypes_sorts) pool
+                                  (type_literals_for_types ctypes_sorts) pool
   in ((lits, tylits), pool) end
 
 fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
@@ -320,7 +320,8 @@
 
 fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   pool_map (dfg_literal params) literals
-  #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
+  #>> rpair (map (dfg_of_type_literal pos)
+                 (type_literals_for_types ctypes_sorts))
 
 fun get_uvars (CombConst _) vars pool = (vars, pool)
   | get_uvars (CombVar (name, _)) vars pool =
@@ -531,6 +532,8 @@
 
 (* DFG format *)
 
+fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
+
 fun write_dfg_file full_types explicit_apply file clauses =
   let
     (* Some of the helper functions below are not name-pool-aware. However,
@@ -543,13 +546,16 @@
     val params = (full_types, explicit_apply, cma, cnh)
     val ((conjecture_clss, tfree_litss), pool) =
       pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
-    and problem_name = Path.implode (Path.base file)
+    val tfree_lits = union_all tfree_litss
+    val problem_name = Path.implode (Path.base file)
     val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
-    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
+    val tfree_clss = map dfg_tfree_clause tfree_lits
+    val tfree_preds = map dfg_tfree_predicate tfree_lits
     val (helper_clauses_strs, pool) =
       pool_map (apfst fst oo dfg_clause params) helper_clauses pool
     val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
-    and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+    val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+    val preds = tfree_preds @ cl_preds @ ty_preds
     val conjecture_offset =
       length axclauses + length classrel_clauses + length arity_clauses
       + length helper_clauses
@@ -559,7 +565,7 @@
            string_of_start problem_name ::
            string_of_descrip problem_name ::
            string_of_symbols (string_of_funcs funcs)
-                             (string_of_preds (cl_preds @ ty_preds)) ::
+                             (string_of_preds preds) ::
            "list_of_clauses(axioms, cnf).\n" ::
            axstrs @
            map dfg_classrel_clause classrel_clauses @