src/HOL/Tools/Sledgehammer/sledgehammer.ML

 
 
 (* Clause preparation *)
 
 datatype fol_formula =
-  FOLFormula of {formula_name: string,
+  FOLFormula of {name: string,
                  kind: kind,
                  combformula: (name, combterm) formula,
                  ctypes_sorts: typ list}
 
 fun mk_anot phi = AConn (ANot, [phi])

         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
       | aux t = t
   in t |> exists_subterm is_Var t ? aux end
 
 (* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (formula_name, kind, t) =
+fun make_formula ctxt presimp (name, kind, t) =
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> transform_elim_term
               |> Object_Logic.atomize_term thy
     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop

               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
               |> kind = Conjecture ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    FOLFormula {formula_name = formula_name, combformula = combformula,
-                kind = kind, ctypes_sorts = ctypes_sorts}
+    FOLFormula {name = name, combformula = combformula, kind = kind,
+                ctypes_sorts = ctypes_sorts}
   end
 
 fun make_axiom ctxt presimp (name, th) =
   (name, make_formula ctxt presimp (name, Axiom, prop_of th))
 fun make_conjectures ctxt ts =

 fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
                 (type_literals_for_types ctypes_sorts))
            (formula_for_combformula full_types combformula)
 
-fun problem_line_for_axiom full_types
-        (formula as FOLFormula {formula_name, kind, ...}) =
-  Fof (axiom_prefix ^ ascii_of formula_name, kind,
-       formula_for_axiom full_types formula)
-
-fun problem_line_for_class_rel_clause
-        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_fact prefix full_types
+                          (formula as FOLFormula {name, kind, ...}) =
+  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
+
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+                                                       superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
-    Fof (ascii_of axiom_name, Axiom,
+    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
                            AAtom (ATerm (superclass, [ty_arg]))]))
   end
 
 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun problem_line_for_arity_clause
-        (ArityClause {axiom_name, conclLit, premLits, ...}) =
-  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+                                                ...}) =
+  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
        mk_ahorn (map (formula_for_fo_literal o apfst not
                       o fo_literal_for_arity_literal) premLits)
                 (formula_for_fo_literal
                      (fo_literal_for_arity_literal conclLit)))
 
 fun problem_line_for_conjecture full_types
-        (FOLFormula {formula_name, kind, combformula, ...}) =
-  Fof (conjecture_prefix ^ formula_name, kind,
+                                (FOLFormula {name, kind, combformula, ...}) =
+  Fof (conjecture_prefix ^ name, kind,
        formula_for_combformula full_types combformula)
 
 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
 

 
 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
                     file (conjectures, axioms, helper_facts, class_rel_clauses,
                           arity_clauses) =
   let
-    val axiom_lines = map (problem_line_for_axiom full_types) axioms
+    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+    val helper_lines =
+      map (problem_line_for_fact helper_prefix full_types) helper_facts
+    val conjecture_lines =
+      map (problem_line_for_conjecture full_types) conjectures
+    val tfree_lines = problem_lines_for_free_types conjectures
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses
     val arity_lines = map problem_line_for_arity_clause arity_clauses
-    val helper_lines = map (problem_line_for_axiom full_types) helper_facts
-    val conjecture_lines =
-      map (problem_line_for_conjecture full_types) conjectures
-    val tfree_lines = problem_lines_for_free_types conjectures
     (* Reordering these might or might not confuse the proof reconstruction
        code or the SPASS Flotter hack. *)
     val problem =
       [("Relevant facts", axiom_lines),
        ("Class relationships", class_rel_lines),

   in output |> split_lines |> map_filter (extract_num o tokens_of) end
 
 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
 
 val parse_clause_formula_pair =
-  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
+  --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
   --| Scan.option ($$ ",")
 val parse_clause_formula_relation =
   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   |-- Scan.repeat parse_clause_formula_pair
 val extract_clause_formula_relation =

       fun renumber_conjecture j =
         AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
         |> map (fn s => find_index (curry (op =) s) seq + 1)
     in
       (conjecture_shape |> map (maps renumber_conjecture),
-       seq |> map (the o AList.lookup (op =) name_map)
-           |> map (fn s => case try (unprefix axiom_prefix) s of
+       seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
+                                  |> try (unprefix axiom_prefix) of
                              SOME s' => undo_ascii_of s'
                            | NONE => "")
            |> Vector.fromList)
     end
   else