author blanchet Tue, 24 May 2011 00:01:33 +0200 changeset 42963 5725deb11ae7 parent 42962 3b50fdeb6cfc child 42964 bf45fd2488a2
identify HOL functions with THF functions
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 00:01:33 2011 +0200
@@ -15,11 +15,13 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

+  datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+
datatype format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
-    Decl of string * 'a * 'a list * 'a |
-    Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+    Decl of string * 'a * 'a ho_type |
+    Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

@@ -30,6 +32,7 @@
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
+  val tptp_fun_type : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -61,11 +64,13 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

+datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
+
datatype format = CNF_UEQ | FOF | TFF | THF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
-  Decl of string * 'a * 'a list * 'a |
-  Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+  Decl of string * 'a * 'a ho_type |
+  Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

@@ -76,6 +81,7 @@
val tptp_type_of_types = "\$tType"
val tptp_bool_type = "\$o"
val tptp_individual_type = "\$i"
+val tptp_fun_type = ">"

fun is_atp_variable s = Char.isUpper (String.sub (s, 0))

@@ -102,6 +108,25 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"

+fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s
+  | strip_tff_type (AFun (AFun _, _)) =
+    raise Fail "unexpected higher-order type in first-order format"
+  | strip_tff_type (AType s) = ([], s)
+
+fun string_for_type THF ty =
+    let
+      fun aux _ (AType s) = s
+        | aux rhs (AFun (ty1, ty2)) =
+          aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
+          |> not rhs ? enclose "(" ")"
+    in aux true ty end
+  | string_for_type TFF ty =
+    (case strip_tff_type ty of
+       ([], s) => s
+     | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
+     | (ss, s) => "(" ^ space_implode " * " ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
+  | string_for_type _ _ = raise Fail "unexpected type in untyped format"
+
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm ("equal", ts)) =
space_implode " = " (map (string_for_term format) ts)
@@ -114,8 +139,10 @@
if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")"
else s ^ "(" ^ commas ss ^ ")"
end
+
fun string_for_quantifier AForall = "!"
| string_for_quantifier AExists = "?"
+
fun string_for_connective ANot = "~"
| string_for_connective AAnd = "&"
| string_for_connective AOr = "|"
@@ -123,17 +150,21 @@
| string_for_connective AIf = "<="
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
+
fun string_for_bound_var format (s, ty) =
-    s ^ (if format = TFF orelse format = THF then
-           " : " ^ (ty |> the_default tptp_individual_type)
-         else
-           "")
+  s ^ (if format = TFF orelse format = THF then
+         " : " ^
+         string_for_type format (ty |> the_default (AType tptp_individual_type))
+       else
+         "")
+
fun string_for_formula format (AQuant (q, xs, phi)) =
"(" ^ string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
string_for_formula format phi ^ ")"
| string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
space_implode " != " (map (string_for_term format) ts)
+    |> format = THF ? enclose "(" ")"
| string_for_formula format (AConn (c, [phi])) =
"(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
| string_for_formula format (AConn (c, phis)) =
@@ -141,14 +172,6 @@
(map (string_for_formula format) phis) ^ ")"
| string_for_formula format (AAtom tm) = string_for_term format tm

-fun string_for_symbol_type THF arg_tys res_ty =
-    space_implode " > " (arg_tys @ [res_ty])
-  | string_for_symbol_type _ [] res_ty = res_ty
-  | string_for_symbol_type _ [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
-  | string_for_symbol_type format arg_tys res_ty =
-    string_for_symbol_type format ["(" ^ space_implode " * " arg_tys ^ ")"]
-                           res_ty
-
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))

@@ -157,9 +180,9 @@
| string_for_format TFF = "tff"
| string_for_format THF = "thf"

-fun string_for_problem_line format (Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
-    string_for_symbol_type format arg_tys res_ty ^ ").\n"
+    string_for_type format ty ^ ").\n"
| string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
",\n    (" ^ string_for_formula format phi ^ ")" ^
@@ -285,20 +308,20 @@

fun nice_term (ATerm (name, ts)) =
nice_name name ##>> pool_map nice_term ts #>> ATerm
+fun nice_type (AType name) = nice_name name #>> AType
+  | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
fun nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
-                    | SOME ty => nice_name ty #>> SOME) (map snd xs)
+                    | SOME ty => nice_type ty #>> SOME) (map snd xs)
##>> nice_formula phi
#>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Decl (ident, sym, arg_tys, res_ty)) =
-    nice_name sym
-    ##>> pool_map nice_name arg_tys
-    ##>> nice_name res_ty
-    #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
+fun nice_problem_line (Decl (ident, sym, ty)) =
+    nice_name sym ##>> nice_type ty
+    #>> (fn (sym, ty) => Decl (ident, sym, ty))
| nice_problem_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =```
```--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
@@ -462,7 +462,8 @@

val atps =
[e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
-   remote_leo2, remote_sine_e, remote_snark, remote_tofof_e, remote_waldmeister]
+   remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
+   remote_waldmeister]
val setup = fold add_atp atps

end;```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 24 00:01:33 2011 +0200
@@ -99,7 +99,8 @@
val simple_type_prefix = "ty_"

fun make_simple_type s =
-  if s = tptp_bool_type then s else simple_type_prefix ^ ascii_of s
+  if s = tptp_bool_type orelse s = tptp_fun_type then s
+  else simple_type_prefix ^ ascii_of s

(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
@@ -281,8 +282,10 @@
fun close_formula_universally phi = close_universally term_vars phi

fun fo_term_from_typ format (Type (s, Ts)) =
-    ATerm (if format = THF andalso s = @{type_name bool} then `I tptp_bool_type
-           else `make_fixed_type_const s,
+    ATerm (case (format, s) of
+             (THF, @{type_name bool}) => `I tptp_bool_type
+           | (THF, @{type_name fun}) => `I tptp_fun_type
+           | _ => `make_fixed_type_const s,
map (fo_term_from_typ format) Ts)
| fo_term_from_typ _ (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
| fo_term_from_typ _ (TVar ((x as (s, _)), _)) =
@@ -295,19 +298,30 @@
| generic_mangled_type_name f (ATerm (name, tys)) =
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
-fun mangled_type_name format =
-  fo_term_from_typ format
-  #> (fn ty => (make_simple_type (generic_mangled_type_name fst ty),
-                generic_mangled_type_name snd ty))

-fun generic_mangled_type_suffix f g Ts =
-  fold_rev (curry (op ^) o g o prefix mangled_type_sep
-            o generic_mangled_type_name f) Ts ""
+fun ho_type_from_fo_term format pred_sym ary =
+  let
+    fun to_atype ty =
+      AType ((make_simple_type (generic_mangled_type_name fst ty),
+              generic_mangled_type_name snd ty))
+    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+    fun to_tff 0 ty =
+        if pred_sym then AType (`I tptp_bool_type) else to_atype ty
+      | to_tff ary (ATerm (_, tys)) = to_afun to_atype (to_tff (ary - 1)) tys
+    fun to_thf (ty as ATerm ((s, _), tys)) =
+      if s = tptp_fun_type then to_afun to_thf to_thf tys else to_atype ty
+  in if format = THF then to_thf else to_tff ary end
+
+fun mangled_type format pred_sym ary =
+  ho_type_from_fo_term format pred_sym ary o fo_term_from_typ format
+
fun mangled_const_name format T_args (s, s') =
-  let val ty_args = map (fo_term_from_typ format) T_args in
-    (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
-     s' ^ generic_mangled_type_suffix snd I ty_args)
-  end
+  let
+    val ty_args = map (fo_term_from_typ format) T_args
+    fun type_suffix f g =
+      fold_rev (curry (op ^) o g o prefix mangled_type_sep
+                o generic_mangled_type_name f) ty_args ""
+  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

val parse_mangled_ident =
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
@@ -334,12 +348,15 @@

fun introduce_proxies format tm =
let
-    fun aux top_level (CombApp (tm1, tm2)) =
-        CombApp (aux top_level tm1, aux false tm2)
-      | aux top_level (CombConst (name as (s, s'), T, T_args)) =
+    fun aux ary top_level (CombApp (tm1, tm2)) =
+        CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
+      | aux ary top_level (CombConst (name as (s, s'), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
-           if top_level orelse format = THF then
+           (* Proxies are not needed in THF, except for partially applied
+              equality since THF does not provide any syntax for it. *)
+           if top_level orelse
+              (format = THF andalso (s <> "equal" orelse ary = 2)) then
(case s of
"c_False" => (tptp_false, s')
| "c_True" => (tptp_true, s')
@@ -348,8 +365,8 @@
(proxy_base |>> prefix const_prefix, T_args)
| NONE => (name, T_args))
|> (fn (name, T_args) => CombConst (name, T, T_args))
-      | aux _ tm = tm
-  in aux true tm end
+      | aux _ _ tm = tm
+  in aux 0 true tm end

fun combformula_from_prop thy format eq_as_iff =
let
@@ -863,7 +880,8 @@
val do_bound_type =
case type_sys of
Simple_Types level =>
-        SOME o mangled_type_name format o homogenized_type ctxt nonmono_Ts level
+        homogenized_type ctxt nonmono_Ts level
+        #> mangled_type format false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
if should_predicate_on_type ctxt nonmono_Ts type_sys
@@ -1041,15 +1059,9 @@

fun decl_line_for_sym ctxt format nonmono_Ts level s
(s', _, T, pred_sym, ary, _) =
-  let
-    val translate_type =
-      mangled_type_name format o homogenized_type ctxt nonmono_Ts level
-    val (arg_tys, res_ty) =
-      T |> chop_fun ary |>> map translate_type ||> translate_type
-  in
-    Decl (sym_decl_prefix ^ s, (s, s'), arg_tys,
-          if pred_sym then `I tptp_bool_type else res_ty)
-  end
+  Decl (sym_decl_prefix ^ s, (s, s'),
+        T |> homogenized_type ctxt nonmono_Ts level
+          |> mangled_type format pred_sym ary)

fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false

@@ -1073,8 +1085,7 @@
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
|> type_pred_combterm ctxt format nonmono_Ts type_sys res_T
-             |> AAtom
-             |> mk_aquant AForall (bound_names ~~ bound_Ts)
+             |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
|> formula_from_combformula ctxt format nonmono_Ts type_sys
(K (K (K (K true)))) true
|> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
@@ -1179,14 +1190,19 @@
type_sys)
sym_decl_tab []

+fun add_simple_types_in_type (AFun (ty1, ty2)) =
+  | add_simple_types_in_type (AType name) = insert (op =) name
+
fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
-    union (op =) (map_filter snd xs) #> add_simple_types_in_formula phi
+    fold add_simple_types_in_type (map_filter snd xs)
| add_simple_types_in_formula (AConn (_, phis)) =
| add_simple_types_in_formula (AAtom _) = I

-fun add_simple_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
-    union (op =) (res_T :: arg_Ts)
+fun add_simple_types_in_problem_line (Decl (_, _, ty)) =
| add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =

@@ -1195,7 +1211,7 @@
|> filter_out (String.isPrefix tptp_special_prefix o fst)

fun decl_line_for_simple_type (s, s') =
-  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_type_of_types)
+  Decl (type_decl_prefix ^ s, (s, s'), AType (`I tptp_type_of_types))

fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
level = Nonmonotonic_Types orelse level = Finite_Types```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 00:01:33 2011 +0200
@@ -439,23 +439,24 @@
[Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]

fun adjust_dumb_type_sys formats (Simple_Types level) =
-    (case inter (op =) formats [TFF, THF] of
-       format :: _ => (format, Simple_Types level)
-     | [] => adjust_dumb_type_sys formats
-                                  (Preds (Mangled_Monomorphic, level, Heavy)))
+    if member (op =) formats THF then
+      (THF, Simple_Types level)
+    else if member (op =) formats TFF then
+      (TFF, Simple_Types level)
+    else
+      adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
-    if member (op =) formats CNF_UEQ then
+    if member (op =) formats FOF then
+      (FOF, type_sys)
+    else if member (op =) formats CNF_UEQ then
(CNF_UEQ, case type_sys of
Tags _ => type_sys
| _ => Preds (polymorphism_of_type_sys type_sys,
Const_Arg_Types, Light))
-    else if member (op =) formats FOF then
-      (FOF, type_sys)
else
-      (* We could return "type_sys" in all cases but this would require the
-         TFF and THF provers to accept problems in which constants are
-         implicitly declared. Today neither SNARK nor ToFoF-E satisfy this
-         criterion. (FIXME: what about LEO-II?) *)
+      (* We could return "type_sys" unchanged for TFF but this would require the
+         TFF provers to accept problems in which constants are implicitly
+         declared. Today neither SNARK nor ToFoF-E meet this criterion. *)
(hd formats, Simple_Types All_Types)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =