# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 46d485f8d144de331f48ff0d84e0b85664a03d92
# Parent  7a506b0b644f667cb5a36015116a1848518b4e55
added room for types in ATP quantifiers

diff -r 7a506b0b644f -r 46d485f8d144 src/HOL/Tools/ATP/atp_problem.ML
--- 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 list * ('a, 'b) formula |
+    AQuant of quantifier * ('a * 'a 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 list * ('a, 'b) formula |
+  AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
   AConn of connective * ('a, 'b) formula list |
   AAtom of 'b
 type 'a uniform_formula = ('a, 'a fo_term) formula
@@ -79,8 +79,11 @@
   | string_for_connective AIf = "<="
   | 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
 fun string_for_formula (AQuant (q, xs, phi)) =
-    "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+    "(" ^ string_for_quantifier q ^
+    "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
     string_for_formula phi ^ ")"
   | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
     space_implode " != " (map string_for_term ts)
@@ -179,8 +182,11 @@
 fun nice_term (ATerm (name, ts)) =
   nice_name name ##>> pool_map nice_term ts #>> ATerm
 fun nice_formula (AQuant (q, xs, phi)) =
-    pool_map nice_name xs ##>> nice_formula phi
-    #>> (fn (xs, phi) => 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)
+    ##>> 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
diff -r 7a506b0b644f -r 46d485f8d144 src/HOL/Tools/ATP/atp_proof.ML
--- 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
@@ -258,7 +258,9 @@
   (($$ "(" |-- parse_formula --| $$ ")"
     || ($$ "!" >> K AForall || $$ "?" >> K AExists)
        --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
-       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
+       >> (fn ((q, ts), phi) =>
+              (* FIXME: TFF *)
+              AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
     || $$ "~" |-- parse_formula >> mk_anot
     || parse_atom)
    -- Scan.option ((Scan.this_string "=>" >> K AImplies
diff -r 7a506b0b644f -r 46d485f8d144 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -441,12 +441,13 @@
     fun do_formula pos phi =
       case phi of
         AQuant (_, [], phi) => do_formula pos phi
-      | AQuant (q, x :: xs, phi') =>
+      | AQuant (q, (s, _) :: xs, phi') =>
         do_formula pos (AQuant (q, xs, phi'))
+        (* FIXME: TFF *)
         #>> quantify_over_var (case q of
                                  AForall => forall_of
                                | AExists => exists_of)
-                              (repair_atp_variable_name Char.toLower x)
+                              (repair_atp_variable_name Char.toLower s)
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1
diff -r 7a506b0b644f -r 46d485f8d144 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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
@@ -114,19 +114,22 @@
 fun close_universally atom_vars phi =
   let
     fun formula_vars bounds (AQuant (_, xs, phi)) =
-        formula_vars (xs @ bounds) phi
+        formula_vars (map fst xs @ bounds) phi
       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
       | formula_vars bounds (AAtom tm) =
-        union (op =) (atom_vars tm [] |> subtract (op =) bounds)
+        union (op =) (atom_vars tm []
+                      |> filter_out (member (op =) bounds o fst))
   in mk_aquant AForall (formula_vars [] phi []) phi end
 
 fun combterm_vars (CombApp (ct, cu)) = fold combterm_vars [ct, cu]
   | combterm_vars (CombConst _) = I
-  | combterm_vars (CombVar (name, _)) = insert (op =) name
+  | combterm_vars (CombVar (name, _)) =
+    insert (op =) (name, NONE) (* FIXME: TFF *)
 val close_combformula_universally = close_universally combterm_vars
 
 fun term_vars (ATerm (name as (s, _), tms)) =
-  is_atp_variable s ? insert (op =) name #> fold term_vars tms
+  is_atp_variable s ? insert (op =) (name, NONE) (* FIXME: TFF *)
+  #> fold term_vars tms
 val close_formula_universally = close_universally term_vars
 
 fun combformula_for_prop thy eq_as_iff =
@@ -137,7 +140,8 @@
     fun do_quant bs q s T t' =
       let val s = Name.variant (map fst bs) s in
         do_formula ((s, T) :: bs) t'
-        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+        (* FIXME: TFF *)
+        #>> (fn phi => AQuant (q, [(`make_bound_var s, NONE)], phi))
       end
     and do_conn bs c t1 t2 =
       do_formula bs t1 ##>> do_formula bs t2