author blanchet Sat, 29 Oct 2011 13:15:58 +0200 changeset 45303 bd03b08161ac parent 45302 04c87dec70b8 child 45304 e6901aa86a9e
added DFG unsorted support (like in the old days)
 src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -25,6 +25,7 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
+  datatype dfg_flavor = DFG_Unsorted | DFG_Sorted

datatype atp_format =
CNF |
@@ -32,7 +33,7 @@
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
-    DFG_Sorted
+    DFG of dfg_flavor

datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -99,7 +100,7 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
-  val is_format_thf : atp_format -> bool
+  val is_format_higher_order : atp_format -> bool
val is_format_typed : atp_format -> bool
val lines_for_atp_problem : atp_format -> string problem -> string list
val ensure_cnf_problem :
@@ -140,6 +141,7 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
+datatype dfg_flavor = DFG_Unsorted | DFG_Sorted

datatype atp_format =
CNF |
@@ -147,7 +149,7 @@
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
-  DFG_Sorted
+  DFG of dfg_flavor

datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -158,8 +160,9 @@

val isabelle_info_prefix = "isabelle_"

-(* Currently, only SPASS supports Isabelle metainformation. *)
-fun isabelle_info DFG_Sorted s =
+(* Currently, only newer versions of SPASS, with sorted DFG format support, can
+   process Isabelle metainformation. *)
+fun isabelle_info (DFG DFG_Sorted) s =
SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))
| isabelle_info _ _ = NONE

@@ -251,11 +254,11 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)

-fun is_format_thf (THF _) = true
-  | is_format_thf _ = false
+fun is_format_higher_order (THF _) = true
+  | is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
-  | is_format_typed (DFG_Sorted) = true
+  | is_format_typed (DFG DFG_Sorted) = true
| is_format_typed _ = false

fun tptp_string_for_kind Axiom = "axiom"
@@ -265,7 +268,7 @@
| tptp_string_for_kind Conjecture = "conjecture"

fun tptp_string_for_app format func args =
-  if is_format_thf format then
+  if is_format_higher_order format then
"(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
else
func ^ "(" ^ commas args ^ ")"
@@ -283,7 +286,7 @@

fun str_for_type format ty =
let
-    val dfg = (format = DFG_Sorted)
+    val dfg = (format = DFG DFG_Sorted)
fun str _ (AType (s, [])) =
if dfg andalso s = tptp_individual_type then "Top" else s
| str _ (AType (s, tys)) =
@@ -337,7 +340,7 @@
else if is_tptp_equal s then
space_implode (" " ^ tptp_equal ^ " ")
(map (tptp_string_for_term format) ts)
-       |> is_format_thf format ? enclose "(" ")"
+       |> is_format_higher_order format ? enclose "(" ")"
else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
s = tptp_choice andalso is_format_with_choice format, ts) of
(true, _, [AAbs ((s', ty), tm)]) =>
@@ -367,11 +370,11 @@
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
(map (tptp_string_for_term format) ts)
-    |> is_format_thf format ? enclose "(" ")"
+    |> is_format_higher_order format ? enclose "(" ")"
| tptp_string_for_formula format (AConn (c, [phi])) =
tptp_string_for_connective c ^ " " ^
(tptp_string_for_formula format phi
-     |> is_format_thf format ? enclose "(" ")")
+     |> is_format_higher_order format ? enclose "(" ")")
|> enclose "(" ")"
| tptp_string_for_formula format (AConn (c, phis)) =
space_implode (" " ^ tptp_string_for_connective c ^ " ")
@@ -389,7 +392,7 @@
| tptp_string_for_format FOF = tptp_fof
| tptp_string_for_format (TFF _) = tptp_tff
| tptp_string_for_format (THF _) = tptp_thf
-  | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format"
+  | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"

fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
@@ -427,7 +430,7 @@
| is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
| is_predicate_type _ = false

-fun dfg_string_for_formula info =
+fun dfg_string_for_formula flavor info =
let
fun str_for_term simp (ATerm (s, tms)) =
(if is_tptp_equal s then "equal" |> simp ? suffix ":lr"
@@ -446,7 +449,7 @@
| str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr"
fun str_for_formula simp (AQuant (q, xs, phi)) =
str_for_quant q ^ "(" ^ "[" ^
-        commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^
+        commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^
str_for_formula simp phi ^ ")"
| str_for_formula simp (AConn (c, phis)) =
str_for_conn simp c ^ "(" ^
@@ -454,19 +457,20 @@
| str_for_formula simp (AAtom tm) = str_for_term simp tm
in str_for_formula (is_isabelle_info simpN info) end

-fun dfg_lines problem =
+fun dfg_lines flavor problem =
let
+    val format = DFG flavor
fun ary sym ty =
"(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
fun fun_typ sym ty =
-      "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")."
+      "function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."
fun pred_typ sym ty =
"predicate(" ^
-      commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")."
+      commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
-          SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^
-                ").")
+          SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^
+                ident ^ ").")
else
NONE
| formula _ _ = NONE
@@ -515,7 +519,9 @@
fun lines_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
-  (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem
+  (case format of
+     DFG flavor => dfg_lines flavor
+   | _ => tptp_lines format) problem

(** CNF (Metis) and CNF UEQ (Waldmeister) **)```
```--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -341,9 +341,9 @@
prem_kind = #prem_kind spass_config,
best_slices = fn ctxt =>
(* FUDGE *)
-     [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*,
-      (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))),
-      (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)]
+     [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*,
+      (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))),
+      (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
```
```--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -640,7 +640,7 @@
| adjust_type_enc (THF _) type_enc = type_enc
| adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
Simple_Types (First_Order, Mangled_Monomorphic, level)
-  | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) =
+  | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
Simple_Types (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
Simple_Types (First_Order, poly, level)
@@ -2365,6 +2365,7 @@
| FOF => I
| TFF (_, TPTP_Implicit) => I
| THF (_, TPTP_Implicit, _) => I
+          | DFG DFG_Unsorted => I
| _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
implicit_declsN)
val (problem, pool) = problem |> nice_atp_problem readable_names```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -160,7 +160,7 @@
end

val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
-val is_ho_atp = is_atp_for_format is_format_thf
+val is_ho_atp = is_atp_for_format is_format_higher_order

fun is_prover_supported ctxt name =
let val thy = Proof_Context.theory_of ctxt in```