src/HOL/Tools/ATP/atp_translate.ML
changeset 44595 444d111bde7d
parent 44594 ae82943481e9
child 44622 779f79ed0ddc
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:46 2011 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4  fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
     1.5  
     1.6  fun make_schematic_type_var (x, i) =
     1.7 -      tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
     1.8 +  tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
     1.9  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
    1.10  
    1.11  (* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
    1.12 @@ -372,9 +372,6 @@
    1.13    TConsLit of name * name * name list |
    1.14    TVarLit of name * name
    1.15  
    1.16 -fun gen_TVars 0 = []
    1.17 -  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
    1.18 -
    1.19  val type_class = the_single @{sort type}
    1.20  
    1.21  fun add_packed_sort tvar =
    1.22 @@ -388,13 +385,12 @@
    1.23  (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
    1.24  fun make_axiom_arity_clause (tcons, name, (cls, args)) =
    1.25    let
    1.26 -    val tvars = gen_TVars (length args)
    1.27 +    val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
    1.28      val tvars_srts = ListPair.zip (tvars, args)
    1.29    in
    1.30      {name = name,
    1.31       prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
    1.32 -     concl_lits = TConsLit (`make_type_class cls,
    1.33 -                            `make_fixed_type_const tcons,
    1.34 +     concl_lits = TConsLit (`make_type_class cls, `make_fixed_type_const tcons,
    1.35                              tvars ~~ tvars)}
    1.36    end
    1.37  
    1.38 @@ -774,10 +770,8 @@
    1.39          (if is_tptp_variable s andalso not (member (op =) bounds name) then
    1.40             (case type_enc of
    1.41                Simple_Types (_, Polymorphic, _) =>
    1.42 -              if String.isPrefix tvar_prefix s then
    1.43 -                SOME (AType (`I tptp_type_of_types, []))
    1.44 -              else
    1.45 -                NONE
    1.46 +              if String.isPrefix tvar_prefix s then SOME atype_of_types
    1.47 +              else NONE
    1.48              | _ => NONE)
    1.49             |> pair name |> insert (op =)
    1.50           else
    1.51 @@ -824,8 +818,6 @@
    1.52  fun mangled_type format type_enc =
    1.53    generic_mangled_type_name fst o ho_term_from_typ format type_enc
    1.54  
    1.55 -val bool_atype = AType (`I tptp_bool_type, [])
    1.56 -
    1.57  fun make_simple_type s =
    1.58    if s = tptp_bool_type orelse s = tptp_fun_type orelse
    1.59       s = tptp_individual_type then
    1.60 @@ -1618,8 +1610,8 @@
    1.61        else make_arity_clauses thy tycons supers
    1.62      val class_rel_clauses = make_class_rel_clauses thy subs supers
    1.63    in
    1.64 -    (fact_names |> map single,
    1.65 -     (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
    1.66 +    (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
    1.67 +     class_rel_clauses, arity_clauses)
    1.68    end
    1.69  
    1.70  val type_guard = `(make_fixed_const NONE) type_guard_name
    1.71 @@ -1746,7 +1738,7 @@
    1.72  
    1.73  fun formula_line_for_class_rel_clause type_enc
    1.74          ({name, subclass, superclass, ...} : class_rel_clause) =
    1.75 -  let val ty_arg = ATerm (`I "T", []) in
    1.76 +  let val ty_arg = ATerm ((make_schematic_type_var ("'a", 0), "'a"), []) in
    1.77      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
    1.78               AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
    1.79                                 AAtom (ATerm (superclass, [ty_arg]))])
    1.80 @@ -1791,6 +1783,16 @@
    1.81  
    1.82  (** Symbol declarations **)
    1.83  
    1.84 +fun decl_line_for_class s =
    1.85 +  let val name as (s, _) = `make_type_class s in
    1.86 +    Decl (sym_decl_prefix ^ s, name, AFun (atype_of_types, bool_atype))
    1.87 +  end
    1.88 +
    1.89 +fun decl_lines_for_classes type_enc classes =
    1.90 +  case type_enc of
    1.91 +    Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
    1.92 +  | _ => []
    1.93 +
    1.94  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    1.95                               (conjs, facts) =
    1.96    let
    1.97 @@ -2170,7 +2172,7 @@
    1.98        else
    1.99          error ("Unknown lambda translation method: " ^
   1.100                 quote lambda_trans ^ ".")
   1.101 -    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   1.102 +    val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
   1.103        translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   1.104                           hyp_ts concl_t facts
   1.105      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   1.106 @@ -2185,6 +2187,7 @@
   1.107      val mono_Ts =
   1.108        helpers @ conjs @ facts
   1.109        |> monotonic_types_for_facts ctxt mono type_enc
   1.110 +    val class_decl_lines = decl_lines_for_classes type_enc classes
   1.111      val sym_decl_lines =
   1.112        (conjs, helpers @ facts)
   1.113        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   1.114 @@ -2201,11 +2204,10 @@
   1.115      (* Reordering these might confuse the proof reconstruction code or the SPASS
   1.116         FLOTTER hack. *)
   1.117      val problem =
   1.118 -      [(explicit_declsN, sym_decl_lines),
   1.119 +      [(explicit_declsN, class_decl_lines @ sym_decl_lines),
   1.120         (factsN,
   1.121          map (formula_line_for_fact ctxt format fact_prefix ascii_of
   1.122 -                                   (not exporter) (not exporter) mono
   1.123 -                                   type_enc)
   1.124 +                                   (not exporter) (not exporter) mono type_enc)
   1.125              (0 upto length facts - 1 ~~ facts)),
   1.126         (class_relsN,
   1.127          map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),