--- 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) =