1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4  
     1.5    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
     1.6    datatype 'a problem_line =
     1.7 +    Type_Decl of string * 'a * 'a list * 'a |
     1.8      Formula of string * formula_kind * ('a, 'a fo_term) formula
     1.9                 * string fo_term option
    1.10    type 'a problem = (string * 'a problem_line list) list
    1.11 @@ -48,6 +49,7 @@
    1.12  
    1.13  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.14  datatype 'a problem_line =
    1.15 +  Type_Decl of string * 'a * 'a list * 'a |
    1.16    Formula of string * formula_kind * ('a, 'a fo_term) formula
    1.17               * string fo_term option
    1.18  type 'a problem = (string * 'a problem_line list) list
    1.19 @@ -98,22 +100,30 @@
    1.20      exists formula_needs_typed_logic phis
    1.21    | formula_needs_typed_logic (AAtom _) = false
    1.22  
    1.23 -fun string_for_problem_line use_conjecture_for_hypotheses
    1.24 +fun string_for_symbol_type [] res_ty = res_ty
    1.25 +  | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
    1.26 +  | string_for_symbol_type arg_tys res_ty =
    1.27 +    string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
    1.28 +
    1.29 +fun string_for_problem_line _ (Type_Decl (ident, sym, arg_tys, res_ty)) =
    1.30 +    "tff(" ^ ident ^ ", type, " ^ sym ^ " : " ^
    1.31 +    string_for_symbol_type arg_tys res_ty ^ ").\n"
    1.32 +  | string_for_problem_line use_conjecture_for_hypotheses
    1.33                              (Formula (ident, kind, phi, source)) =
    1.34 -  let
    1.35 -    val (kind, phi) =
    1.36 -      if kind = Hypothesis andalso use_conjecture_for_hypotheses then
    1.37 -        (Conjecture, AConn (ANot, [phi]))
    1.38 -      else
    1.39 -        (kind, phi)
    1.40 -  in
    1.41 -    (if formula_needs_typed_logic phi then "tff" else "fof") ^
    1.42 -    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
    1.43 -    string_for_formula phi ^ ")" ^
    1.44 -    (case source of
    1.45 -       SOME tm => ", " ^ string_for_term tm
    1.46 -     | NONE => "") ^ ").\n"
    1.47 -  end
    1.48 +    let
    1.49 +      val (kind, phi) =
    1.50 +        if kind = Hypothesis andalso use_conjecture_for_hypotheses then
    1.51 +          (Conjecture, AConn (ANot, [phi]))
    1.52 +        else
    1.53 +          (kind, phi)
    1.54 +    in
    1.55 +      (if formula_needs_typed_logic phi then "tff" else "fof") ^
    1.56 +      "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
    1.57 +      string_for_formula phi ^ ")" ^
    1.58 +      (case source of
    1.59 +         SOME tm => ", " ^ string_for_term tm
    1.60 +       | NONE => "") ^ ").\n"
    1.61 +    end
    1.62  fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
    1.63    "% This file was generated by Isabelle (most likely Sledgehammer)\n\
    1.64    \% " ^ timestamp () ^ "\n" ::
    1.65 @@ -194,8 +204,13 @@
    1.66    | nice_formula (AConn (c, phis)) =
    1.67      pool_map nice_formula phis #>> curry AConn c
    1.68    | nice_formula (AAtom tm) = nice_term tm #>> AAtom
    1.69 -fun nice_problem_line (Formula (ident, kind, phi, source)) =
    1.70 -  nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
    1.71 +fun nice_problem_line (Type_Decl (ident, sym, arg_tys, res_ty)) =
    1.72 +    nice_name sym
    1.73 +    ##>> pool_map nice_name arg_tys
    1.74 +    ##>> nice_name res_ty
    1.75 +    #>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
    1.76 +  | nice_problem_line (Formula (ident, kind, phi, source)) =
    1.77 +    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
    1.78  fun nice_problem problem =
    1.79    pool_map (fn (heading, lines) =>
    1.80                 pool_map nice_problem_line lines #>> pair heading) problem