generate properly typed TFF1 (PFF) problems in the presence of type class predicates
authorblanchet
Tue Aug 30 16:07:46 2011 +0200 (2011-08-30)
changeset 44595444d111bde7d
parent 44594 ae82943481e9
child 44596 2621046c550a
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:46 2011 +0200
     1.3 @@ -74,6 +74,9 @@
     1.4    val is_built_in_tptp_symbol : string -> bool
     1.5    val is_tptp_variable : string -> bool
     1.6    val is_tptp_user_symbol : string -> bool
     1.7 +  val atype_of_types : (string * string) ho_type
     1.8 +  val bool_atype : (string * string) ho_type
     1.9 +  val individual_atype : (string * string) ho_type
    1.10    val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
    1.11    val mk_aconn :
    1.12      connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:46 2011 +0200
     2.3 @@ -311,7 +311,7 @@
     2.4  fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
     2.5  
     2.6  fun make_schematic_type_var (x, i) =
     2.7 -      tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
     2.8 +  tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
     2.9  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
    2.10  
    2.11  (* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
    2.12 @@ -372,9 +372,6 @@
    2.13    TConsLit of name * name * name list |
    2.14    TVarLit of name * name
    2.15  
    2.16 -fun gen_TVars 0 = []
    2.17 -  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
    2.18 -
    2.19  val type_class = the_single @{sort type}
    2.20  
    2.21  fun add_packed_sort tvar =
    2.22 @@ -388,13 +385,12 @@
    2.23  (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
    2.24  fun make_axiom_arity_clause (tcons, name, (cls, args)) =
    2.25    let
    2.26 -    val tvars = gen_TVars (length args)
    2.27 +    val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
    2.28      val tvars_srts = ListPair.zip (tvars, args)
    2.29    in
    2.30      {name = name,
    2.31       prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
    2.32 -     concl_lits = TConsLit (`make_type_class cls,
    2.33 -                            `make_fixed_type_const tcons,
    2.34 +     concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons,
    2.35                              tvars ~~ tvars)}
    2.36    end
    2.37  
    2.38 @@ -774,10 +770,8 @@
    2.39          (if is_tptp_variable s andalso not (member (op =) bounds name) then
    2.40             (case type_enc of
    2.41                Simple_Types (_, Polymorphic, _) =>
    2.42 -              if String.isPrefix tvar_prefix s then
    2.43 -                SOME (AType (`I tptp_type_of_types, []))
    2.44 -              else
    2.45 -                NONE
    2.46 +              if String.isPrefix tvar_prefix s then SOME atype_of_types
    2.47 +              else NONE
    2.48              | _ => NONE)
    2.49             |> pair name |> insert (op =)
    2.50           else
    2.51 @@ -824,8 +818,6 @@
    2.52  fun mangled_type format type_enc =
    2.53    generic_mangled_type_name fst o ho_term_from_typ format type_enc
    2.54  
    2.55 -val bool_atype = AType (`I tptp_bool_type, [])
    2.56 -
    2.57  fun make_simple_type s =
    2.58    if s = tptp_bool_type orelse s = tptp_fun_type orelse
    2.59       s = tptp_individual_type then
    2.60 @@ -1618,8 +1610,8 @@
    2.61        else make_arity_clauses thy tycons supers
    2.62      val class_rel_clauses = make_class_rel_clauses thy subs supers
    2.63    in
    2.64 -    (fact_names |> map single,
    2.65 -     (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
    2.66 +    (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
    2.67 +     class_rel_clauses, arity_clauses)
    2.68    end
    2.69  
    2.70  val type_guard = `(make_fixed_const NONE) type_guard_name
    2.71 @@ -1746,7 +1738,7 @@
    2.72  
    2.73  fun formula_line_for_class_rel_clause type_enc
    2.74          ({name, subclass, superclass, ...} : class_rel_clause) =
    2.75 -  let val ty_arg = ATerm (`I "T", []) in
    2.76 +  let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in
    2.77      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
    2.78               AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
    2.79                                 AAtom (ATerm (superclass, [ty_arg]))])
    2.80 @@ -1791,6 +1783,16 @@
    2.81  
    2.82  (** Symbol declarations **)
    2.83  
    2.84 +fun decl_line_for_class s =
    2.85 +  let val name as (s, _) = `make_type_class s in
    2.86 +    Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype))
    2.87 +  end
    2.88 +
    2.89 +fun decl_lines_for_classes type_enc classes =
    2.90 +  case type_enc of
    2.91 +    Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
    2.92 +  | _ => []
    2.93 +
    2.94  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    2.95                               (conjs, facts) =
    2.96    let
    2.97 @@ -2170,7 +2172,7 @@
    2.98        else
    2.99          error ("Unknown lambda translation method: " ^
   2.100                 quote lambda_trans ^ ".")
   2.101 -    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   2.102 +    val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
   2.103        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   2.104                           hyp_ts concl_t facts
   2.105      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   2.106 @@ -2185,6 +2187,7 @@
   2.107      val mono_Ts =
   2.108        helpers @ conjs @ facts
   2.109        |> monotonic_types_for_facts ctxt mono type_enc
   2.110 +    val class_decl_lines = decl_lines_for_classes type_enc classes
   2.111      val sym_decl_lines =
   2.112        (conjs, helpers @ facts)
   2.113        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   2.114 @@ -2201,11 +2204,10 @@
   2.115      (* Reordering these might confuse the proof reconstruction code or the SPASS
   2.116         FLOTTER hack. *)
   2.117      val problem =
   2.118 -      [(explicit_declsN, sym_decl_lines),
   2.119 +      [(explicit_declsN, class_decl_lines @ sym_decl_lines),
   2.120         (factsN,
   2.121          map (formula_line_for_fact ctxt format fact_prefix ascii_of
   2.122 -                                   (not exporter) (not exporter) mono
   2.123 -                                   type_enc)
   2.124 +                                   (not exporter) (not exporter) mono type_enc)
   2.125              (0 upto length facts - 1 ~~ facts)),
   2.126         (class_relsN,
   2.127          map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),