1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
1.3 @@ -15,11 +15,13 @@
1.4 AConn of connective * ('a, 'b, 'c) formula list |
1.5 AAtom of 'c
1.6
1.7 + datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.8 +
1.9 datatype format = CNF_UEQ | FOF | TFF | THF
1.10 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.11 datatype 'a problem_line =
1.12 - Decl of string * 'a * 'a list * 'a |
1.13 - Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.14 + Decl of string * 'a * 'a ho_type |
1.15 + Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
1.16 * string fo_term option * string fo_term option
1.17 type 'a problem = (string * 'a problem_line list) list
1.18
1.19 @@ -30,6 +32,7 @@
1.20 val tptp_type_of_types : string
1.21 val tptp_bool_type : string
1.22 val tptp_individual_type : string
1.23 + val tptp_fun_type : string
1.24 val is_atp_variable : string -> bool
1.25 val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
1.26 val mk_aconn :
1.27 @@ -61,11 +64,13 @@
1.28 AConn of connective * ('a, 'b, 'c) formula list |
1.29 AAtom of 'c
1.30
1.31 +datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
1.32 +
1.33 datatype format = CNF_UEQ | FOF | TFF | THF
1.34 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.35 datatype 'a problem_line =
1.36 - Decl of string * 'a * 'a list * 'a |
1.37 - Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.38 + Decl of string * 'a * 'a ho_type |
1.39 + Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
1.40 * string fo_term option * string fo_term option
1.41 type 'a problem = (string * 'a problem_line list) list
1.42
1.43 @@ -76,6 +81,7 @@
1.44 val tptp_type_of_types = "$tType"
1.45 val tptp_bool_type = "$o"
1.46 val tptp_individual_type = "$i"
1.47 +val tptp_fun_type = ">"
1.48
1.49 fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
1.50
1.51 @@ -102,6 +108,25 @@
1.52 | string_for_kind Hypothesis = "hypothesis"
1.53 | string_for_kind Conjecture = "conjecture"
1.54
1.55 +fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s
1.56 + | strip_tff_type (AFun (AFun _, _)) =
1.57 + raise Fail "unexpected higher-order type in first-order format"
1.58 + | strip_tff_type (AType s) = ([], s)
1.59 +
1.60 +fun string_for_type THF ty =
1.61 + let
1.62 + fun aux _ (AType s) = s
1.63 + | aux rhs (AFun (ty1, ty2)) =
1.64 + aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
1.65 + |> not rhs ? enclose "(" ")"
1.66 + in aux true ty end
1.67 + | string_for_type TFF ty =
1.68 + (case strip_tff_type ty of
1.69 + ([], s) => s
1.70 + | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
1.71 + | (ss, s) => "(" ^ space_implode " * " ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
1.72 + | string_for_type _ _ = raise Fail "unexpected type in untyped format"
1.73 +
1.74 fun string_for_term _ (ATerm (s, [])) = s
1.75 | string_for_term format (ATerm ("equal", ts)) =
1.76 space_implode " = " (map (string_for_term format) ts)
1.77 @@ -114,8 +139,10 @@
1.78 if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")"
1.79 else s ^ "(" ^ commas ss ^ ")"
1.80 end
1.81 +
1.82 fun string_for_quantifier AForall = "!"
1.83 | string_for_quantifier AExists = "?"
1.84 +
1.85 fun string_for_connective ANot = "~"
1.86 | string_for_connective AAnd = "&"
1.87 | string_for_connective AOr = "|"
1.88 @@ -123,17 +150,21 @@
1.89 | string_for_connective AIf = "<="
1.90 | string_for_connective AIff = "<=>"
1.91 | string_for_connective ANotIff = "<~>"
1.92 +
1.93 fun string_for_bound_var format (s, ty) =
1.94 - s ^ (if format = TFF orelse format = THF then
1.95 - " : " ^ (ty |> the_default tptp_individual_type)
1.96 - else
1.97 - "")
1.98 + s ^ (if format = TFF orelse format = THF then
1.99 + " : " ^
1.100 + string_for_type format (ty |> the_default (AType tptp_individual_type))
1.101 + else
1.102 + "")
1.103 +
1.104 fun string_for_formula format (AQuant (q, xs, phi)) =
1.105 "(" ^ string_for_quantifier q ^
1.106 "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
1.107 string_for_formula format phi ^ ")"
1.108 | string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
1.109 space_implode " != " (map (string_for_term format) ts)
1.110 + |> format = THF ? enclose "(" ")"
1.111 | string_for_formula format (AConn (c, [phi])) =
1.112 "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
1.113 | string_for_formula format (AConn (c, phis)) =
1.114 @@ -141,14 +172,6 @@
1.115 (map (string_for_formula format) phis) ^ ")"
1.116 | string_for_formula format (AAtom tm) = string_for_term format tm
1.117
1.118 -fun string_for_symbol_type THF arg_tys res_ty =
1.119 - space_implode " > " (arg_tys @ [res_ty])
1.120 - | string_for_symbol_type _ [] res_ty = res_ty
1.121 - | string_for_symbol_type _ [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
1.122 - | string_for_symbol_type format arg_tys res_ty =
1.123 - string_for_symbol_type format ["(" ^ space_implode " * " arg_tys ^ ")"]
1.124 - res_ty
1.125 -
1.126 val default_source =
1.127 ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
1.128
1.129 @@ -157,9 +180,9 @@
1.130 | string_for_format TFF = "tff"
1.131 | string_for_format THF = "thf"
1.132
1.133 -fun string_for_problem_line format (Decl (ident, sym, arg_tys, res_ty)) =
1.134 +fun string_for_problem_line format (Decl (ident, sym, ty)) =
1.135 string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
1.136 - string_for_symbol_type format arg_tys res_ty ^ ").\n"
1.137 + string_for_type format ty ^ ").\n"
1.138 | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
1.139 string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
1.140 ",\n (" ^ string_for_formula format phi ^ ")" ^
1.141 @@ -285,20 +308,20 @@
1.142
1.143 fun nice_term (ATerm (name, ts)) =
1.144 nice_name name ##>> pool_map nice_term ts #>> ATerm
1.145 +fun nice_type (AType name) = nice_name name #>> AType
1.146 + | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
1.147 fun nice_formula (AQuant (q, xs, phi)) =
1.148 pool_map nice_name (map fst xs)
1.149 ##>> pool_map (fn NONE => pair NONE
1.150 - | SOME ty => nice_name ty #>> SOME) (map snd xs)
1.151 + | SOME ty => nice_type ty #>> SOME) (map snd xs)
1.152 ##>> nice_formula phi
1.153 #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
1.154 | nice_formula (AConn (c, phis)) =
1.155 pool_map nice_formula phis #>> curry AConn c
1.156 | nice_formula (AAtom tm) = nice_term tm #>> AAtom
1.157 -fun nice_problem_line (Decl (ident, sym, arg_tys, res_ty)) =
1.158 - nice_name sym
1.159 - ##>> pool_map nice_name arg_tys
1.160 - ##>> nice_name res_ty
1.161 - #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
1.162 +fun nice_problem_line (Decl (ident, sym, ty)) =
1.163 + nice_name sym ##>> nice_type ty
1.164 + #>> (fn (sym, ty) => Decl (ident, sym, ty))
1.165 | nice_problem_line (Formula (ident, kind, phi, source, info)) =
1.166 nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
1.167 fun nice_problem problem =