author blanchet Sun, 01 May 2011 18:37:24 +0200 changeset 42530 f64c546efe8c parent 42529 747736d8b47e child 42531 a462dbaa584f
fixed type of ATP quantifier types (sic)
```--- 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
@@ -11,7 +11,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype ('a, 'b) formula =
-    AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
+    AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -42,7 +42,7 @@
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
datatype ('a, 'b) formula =
-  AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
+  AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -80,7 +80,7 @@
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
fun string_for_bound_var (s, NONE) = s
-  | string_for_bound_var (s, SOME t) = s ^ " : " ^ t
+  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ string_for_term ty
fun string_for_formula (AQuant (q, xs, phi)) =
"(" ^ string_for_quantifier q ^
"[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
@@ -201,7 +201,7 @@
fun nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
-                    | SOME s => nice_name s #>> SOME) (map snd xs)
+                    | SOME ty => nice_term ty #>> SOME) (map snd xs)
##>> nice_formula phi
#>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
| nice_formula (AConn (c, phis)) =```
```--- 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
@@ -447,9 +447,9 @@
(hd ss, map unmangled_type (tl ss))
end

-fun fo_term_for_combterm ctxt type_sys =
+fun formula_for_combformula ctxt type_sys =
let
-    fun aux top_level u =
+    fun do_term top_level u =
let
val (head, args) = strip_combterm_comb u
val (x, ty_args) =
@@ -478,23 +478,20 @@
end)
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
-        val t =
-          ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args)
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @
+                          map (do_term false) args)
val ty = combtyp_of u
-    in
-      t |> (if should_tag_with_type ctxt type_sys ty then
-              tag_with_type (fo_term_for_combtyp ty)
-            else
-              I)
-    end
-  in aux true end
-
-fun formula_for_combformula ctxt type_sys =
-  let
-    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
-      | aux (AConn (c, phis)) = AConn (c, map aux phis)
-      | aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm)
-  in aux end
+      in
+        t |> (if should_tag_with_type ctxt type_sys ty then
+                tag_with_type (fo_term_for_combtyp ty)
+              else
+                I)
+      end
+    fun do_formula (AQuant (q, xs, phi)) =
+        AQuant (q, map (apsnd (Option.map (do_term true))) xs, do_formula phi)
+      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
+      | do_formula (AAtom tm) = AAtom (do_term true tm)
+  in do_formula end

fun formula_for_fact ctxt type_sys
({combformula, ctypes_sorts, ...} : translated_formula) =```