added room for types in ATP quantifiers
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 4252646d485f8d144
parent 42525 7a506b0b644f
child 42527 6a9458524f01
added room for types in ATP quantifiers
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    datatype quantifier = AForall | AExists
     1.5    datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
     1.6    datatype ('a, 'b) formula =
     1.7 -    AQuant of quantifier * 'a list * ('a, 'b) formula |
     1.8 +    AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
     1.9      AConn of connective * ('a, 'b) formula list |
    1.10      AAtom of 'b
    1.11    type 'a uniform_formula = ('a, 'a fo_term) formula
    1.12 @@ -42,7 +42,7 @@
    1.13  datatype quantifier = AForall | AExists
    1.14  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
    1.15  datatype ('a, 'b) formula =
    1.16 -  AQuant of quantifier * 'a list * ('a, 'b) formula |
    1.17 +  AQuant of quantifier * ('a * 'a option) list * ('a, 'b) formula |
    1.18    AConn of connective * ('a, 'b) formula list |
    1.19    AAtom of 'b
    1.20  type 'a uniform_formula = ('a, 'a fo_term) formula
    1.21 @@ -79,8 +79,11 @@
    1.22    | string_for_connective AIf = "<="
    1.23    | string_for_connective AIff = "<=>"
    1.24    | string_for_connective ANotIff = "<~>"
    1.25 +fun string_for_bound_var (s, NONE) = s
    1.26 +  | string_for_bound_var (s, SOME t) = s ^ " : " ^ t
    1.27  fun string_for_formula (AQuant (q, xs, phi)) =
    1.28 -    "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
    1.29 +    "(" ^ string_for_quantifier q ^
    1.30 +    "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
    1.31      string_for_formula phi ^ ")"
    1.32    | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
    1.33      space_implode " != " (map string_for_term ts)
    1.34 @@ -179,8 +182,11 @@
    1.35  fun nice_term (ATerm (name, ts)) =
    1.36    nice_name name ##>> pool_map nice_term ts #>> ATerm
    1.37  fun nice_formula (AQuant (q, xs, phi)) =
    1.38 -    pool_map nice_name xs ##>> nice_formula phi
    1.39 -    #>> (fn (xs, phi) => AQuant (q, xs, phi))
    1.40 +    pool_map nice_name (map fst xs)
    1.41 +    ##>> pool_map (fn NONE => pair NONE
    1.42 +                    | SOME s => nice_name s #>> SOME) (map snd xs)
    1.43 +    ##>> nice_formula phi
    1.44 +    #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
    1.45    | nice_formula (AConn (c, phis)) =
    1.46      pool_map nice_formula phis #>> curry AConn c
    1.47    | nice_formula (AAtom tm) = nice_term tm #>> AAtom
     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -258,7 +258,9 @@
     2.4    (($$ "(" |-- parse_formula --| $$ ")"
     2.5      || ($$ "!" >> K AForall || $$ "?" >> K AExists)
     2.6         --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
     2.7 -       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
     2.8 +       >> (fn ((q, ts), phi) =>
     2.9 +              (* FIXME: TFF *)
    2.10 +              AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
    2.11      || $$ "~" |-- parse_formula >> mk_anot
    2.12      || parse_atom)
    2.13     -- Scan.option ((Scan.this_string "=>" >> K AImplies
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     3.3 @@ -441,12 +441,13 @@
     3.4      fun do_formula pos phi =
     3.5        case phi of
     3.6          AQuant (_, [], phi) => do_formula pos phi
     3.7 -      | AQuant (q, x :: xs, phi') =>
     3.8 +      | AQuant (q, (s, _) :: xs, phi') =>
     3.9          do_formula pos (AQuant (q, xs, phi'))
    3.10 +        (* FIXME: TFF *)
    3.11          #>> quantify_over_var (case q of
    3.12                                   AForall => forall_of
    3.13                                 | AExists => exists_of)
    3.14 -                              (repair_atp_variable_name Char.toLower x)
    3.15 +                              (repair_atp_variable_name Char.toLower s)
    3.16        | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
    3.17        | AConn (c, [phi1, phi2]) =>
    3.18          do_formula (pos |> c = AImplies ? not) phi1
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     4.3 @@ -114,19 +114,22 @@
     4.4  fun close_universally atom_vars phi =
     4.5    let
     4.6      fun formula_vars bounds (AQuant (_, xs, phi)) =
     4.7 -        formula_vars (xs @ bounds) phi
     4.8 +        formula_vars (map fst xs @ bounds) phi
     4.9        | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
    4.10        | formula_vars bounds (AAtom tm) =
    4.11 -        union (op =) (atom_vars tm [] |> subtract (op =) bounds)
    4.12 +        union (op =) (atom_vars tm []
    4.13 +                      |> filter_out (member (op =) bounds o fst))
    4.14    in mk_aquant AForall (formula_vars [] phi []) phi end
    4.15  
    4.16  fun combterm_vars (CombApp (ct, cu)) = fold combterm_vars [ct, cu]
    4.17    | combterm_vars (CombConst _) = I
    4.18 -  | combterm_vars (CombVar (name, _)) = insert (op =) name
    4.19 +  | combterm_vars (CombVar (name, _)) =
    4.20 +    insert (op =) (name, NONE) (* FIXME: TFF *)
    4.21  val close_combformula_universally = close_universally combterm_vars
    4.22  
    4.23  fun term_vars (ATerm (name as (s, _), tms)) =
    4.24 -  is_atp_variable s ? insert (op =) name #> fold term_vars tms
    4.25 +  is_atp_variable s ? insert (op =) (name, NONE) (* FIXME: TFF *)
    4.26 +  #> fold term_vars tms
    4.27  val close_formula_universally = close_universally term_vars
    4.28  
    4.29  fun combformula_for_prop thy eq_as_iff =
    4.30 @@ -137,7 +140,8 @@
    4.31      fun do_quant bs q s T t' =
    4.32        let val s = Name.variant (map fst bs) s in
    4.33          do_formula ((s, T) :: bs) t'
    4.34 -        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    4.35 +        (* FIXME: TFF *)
    4.36 +        #>> (fn phi => AQuant (q, [(`make_bound_var s, NONE)], phi))
    4.37        end
    4.38      and do_conn bs c t1 t2 =
    4.39        do_formula bs t1 ##>> do_formula bs t2