author blanchet Sun, 01 May 2011 18:37:24 +0200 changeset 42543 f9d402d144d4 parent 42542 024920b65ce2 child 42544 75cb06eee990
declare TFF types so that SNARK can be used with types
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
@@ -18,7 +18,7 @@
datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
-    Type_Decl of string * 'a * 'a list * 'a |
+    Decl of string * 'a * 'a list * 'a |
Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -49,7 +49,7 @@
datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
-  Type_Decl of string * 'a * 'a list * 'a |
+  Decl of string * 'a * 'a list * 'a |
Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -99,7 +99,7 @@
| string_for_symbol_type arg_tys res_ty =
string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty

-fun string_for_problem_line _ (Type_Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
"tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
string_for_symbol_type arg_tys res_ty ^ ").\n"
| string_for_problem_line use_conjecture_for_hypotheses
@@ -201,11 +201,11 @@
| 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 (Type_Decl (ident, sym, arg_tys, res_ty)) =
+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) => Type_Decl (ident, sym, arg_tys, res_ty))
+    #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
| nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
nice_formula phi
#>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))```
```--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -237,6 +237,7 @@

fun parse_term x =
(scan_general_id
+     --| Scan.option (\$\$ ":" -- scan_general_id) (* ignore TFF types for now *)
-- Scan.optional (\$\$ "(" |-- (parse_vampire_detritus || parse_terms)
--| \$\$ ")") []
--| Scan.optional (\$\$ "(" |-- parse_vampire_detritus --| \$\$ ")") []```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -45,11 +45,12 @@
open Metis_Translate
open Sledgehammer_Util

+val type_decl_prefix = "type_"
+val sym_decl_prefix = "sym_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
-val type_decl_prefix = "type_"
-val class_rel_clause_prefix = "clrel_";
+val class_rel_clause_prefix = "crel_";
val arity_clause_prefix = "arity_"
val tfree_prefix = "tfree_"

@@ -61,6 +62,7 @@
fun make_type ty = type_prefix ^ ascii_of ty

(* official TPTP TFF syntax *)
+val tff_type_of_types = "\$tType"
val tff_bool_type = "\$o"

(* Freshness almost guaranteed! *)
@@ -778,14 +780,14 @@
| _ => ([], f ty))
| strip_and_map_combtyp f ty = ([], f ty)

-fun type_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
+fun sym_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
if type_sys = Many_Typed then
let
val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty
val (s, s') = (s, s') |> mangled_const_name ty_args
in
-      Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
-                 if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
+      Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
+            if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
end
else
let
@@ -796,7 +798,7 @@
val bound_tms =
map (fn (name, ty) => CombConst (name, the ty, [])) bounds
in
-      Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom,
+      Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
CombConst ((s, s'), ty, ty_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom type_sys res_ty
@@ -804,13 +806,31 @@
|> formula_for_combformula ctxt type_sys,
NONE, NONE)
end
-fun type_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
-  map (type_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+fun sym_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
+  map (sym_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+
+fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
+    union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
+  | add_tff_types_in_formula (AConn (_, phis)) =
+    fold add_tff_types_in_formula phis
+  | add_tff_types_in_formula (AAtom _) = I

-val type_declsN = "Type declarations"
+fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) =
+    union (op =) (res_ty :: arg_tys)
+  | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
+
+fun tff_types_in_problem problem =
+  fold (fold add_tff_types_in_problem_line o snd) problem []
+
+fun problem_line_for_tff_type (s, s') =
+  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
+
+val type_declsN = "Types"
+val sym_declsN = "Symbols"
val factsN = "Relevant facts"
val class_relsN = "Class relationships"
-val aritiesN = "Arity declarations"
+val aritiesN = "Arities"
val helpersN = "Helper facts"
val conjsN = "Conjectures"
val free_typesN = "Type variables"
@@ -832,6 +852,7 @@
Flotter hack. *)
val problem =
[(type_declsN, []),
+       (sym_declsN, []),
(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
@@ -845,17 +866,24 @@
|> get_helper_facts ctxt type_sys
|>> map (hrepair_fact type_sys hrepairs)
val const_tab = const_table_for_facts type_sys hrepairs (conjs @ facts)
-    val type_decl_lines =
-      Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys
-                                                          hrepairs)
+    val sym_decl_lines =
+      Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys hrepairs)
const_tab []
val helper_lines =
helper_facts
|>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys)
|> op @
-    val (problem, pool) =
+    val problem =
problem |> fold (AList.update (op =))
-                      [(type_declsN, type_decl_lines), (helpersN, helper_lines)]
+                      [(sym_declsN, sym_decl_lines),
+                       (helpersN, helper_lines)]
+    val type_decl_lines =
+      if type_sys = Many_Typed then
+        problem |> tff_types_in_problem |> map problem_line_for_tff_type
+      else
+        []
+    val (problem, pool) =
+      problem |> AList.update (op =) (type_declsN, type_decl_lines)