1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
1.3 @@ -119,7 +119,6 @@
1.4 val is_type_sys_virtually_sound : type_sys -> bool
1.5 val is_type_sys_fairly_sound : type_sys -> bool
1.6 val choose_format : format list -> type_sys -> format * type_sys
1.7 - val raw_type_literals_for_types : typ list -> type_literal list
1.8 val mk_aconns :
1.9 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.10 val unmangled_const_name : string -> string
1.11 @@ -145,9 +144,6 @@
1.12
1.13 type name = string * string
1.14
1.15 -(* FIXME: avoid *)
1.16 -fun union_all xss = fold (union (op =)) xss []
1.17 -
1.18 (* experimental *)
1.19 val generate_useful_info = false
1.20
1.21 @@ -393,11 +389,10 @@
1.22 fun gen_TVars 0 = []
1.23 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
1.24
1.25 -fun pack_sort (_,[]) = []
1.26 - | pack_sort (tvar, "HOL.type" :: srt) =
1.27 - pack_sort (tvar, srt) (* IGNORE sort "type" *)
1.28 - | pack_sort (tvar, cls :: srt) =
1.29 - (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
1.30 +val type_class = the_single @{sort type}
1.31 +
1.32 +fun add_packed_sort tvar =
1.33 + fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
1.34
1.35 type arity_clause =
1.36 {name: string,
1.37 @@ -411,7 +406,7 @@
1.38 val tvars_srts = ListPair.zip (tvars, args)
1.39 in
1.40 {name = name,
1.41 - prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
1.42 + prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
1.43 concl_lits = TConsLit (`make_type_class cls,
1.44 `make_fixed_type_const tcons,
1.45 tvars ~~ tvars)}
1.46 @@ -447,10 +442,14 @@
1.47 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
1.48 fun iter_type_class_pairs _ _ [] = ([], [])
1.49 | iter_type_class_pairs thy tycons classes =
1.50 - let val cpairs = type_class_pairs thy tycons classes
1.51 - val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
1.52 - |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
1.53 - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
1.54 + let
1.55 + fun maybe_insert_class s =
1.56 + (s <> type_class andalso not (member (op =) classes s))
1.57 + ? insert (op =) s
1.58 + val cpairs = type_class_pairs thy tycons classes
1.59 + val newclasses =
1.60 + [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
1.61 + val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
1.62 in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
1.63
1.64 fun make_arity_clauses thy tycons =
1.65 @@ -684,28 +683,23 @@
1.66 general_type_arg_policy type_sys
1.67
1.68 (*Make literals for sorted type variables*)
1.69 -fun generic_sorts_on_type (_, []) = []
1.70 - | generic_sorts_on_type ((x, i), s :: ss) =
1.71 - generic_sorts_on_type ((x, i), ss)
1.72 - |> (if s = the_single @{sort HOL.type} then
1.73 +fun generic_add_sorts_on_type (_, []) = I
1.74 + | generic_add_sorts_on_type ((x, i), s :: ss) =
1.75 + generic_add_sorts_on_type ((x, i), ss)
1.76 + #> (if s = the_single @{sort HOL.type} then
1.77 I
1.78 else if i = ~1 then
1.79 - cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
1.80 + insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
1.81 else
1.82 - cons (TyLitVar (`make_type_class s,
1.83 - (make_schematic_type_var (x, i), x))))
1.84 -fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
1.85 - | sorts_on_tfree _ = []
1.86 -fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
1.87 - | sorts_on_tvar _ = []
1.88 + insert (op =) (TyLitVar (`make_type_class s,
1.89 + (make_schematic_type_var (x, i), x))))
1.90 +fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
1.91 + | add_sorts_on_tfree _ = I
1.92 +fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
1.93 + | add_sorts_on_tvar _ = I
1.94
1.95 -(* Given a list of sorted type variables, return a list of type literals. *)
1.96 -fun raw_type_literals_for_types Ts =
1.97 - union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
1.98 -
1.99 -fun type_literals_for_types type_sys sorts_on_typ Ts =
1.100 - if level_of_type_sys type_sys = No_Types then []
1.101 - else union_all (map sorts_on_typ Ts)
1.102 +fun type_literals_for_types type_sys add_sorts_on_typ Ts =
1.103 + [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
1.104
1.105 fun mk_aconns c phis =
1.106 let val (phis', phi') = split_last phis in
1.107 @@ -1529,7 +1523,7 @@
1.108
1.109 fun bound_tvars type_sys Ts =
1.110 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1.111 - (type_literals_for_types type_sys sorts_on_tvar Ts))
1.112 + (type_literals_for_types type_sys add_sorts_on_tvar Ts))
1.113
1.114 fun formula_for_fact ctxt format nonmono_Ts type_sys
1.115 ({combformula, atomic_types, ...} : translated_formula) =
1.116 @@ -1591,7 +1585,7 @@
1.117 |> close_formula_universally, NONE, NONE)
1.118
1.119 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
1.120 - atomic_types |> type_literals_for_types type_sys sorts_on_tfree
1.121 + atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
1.122 |> map fo_literal_from_type_literal
1.123
1.124 fun formula_line_for_free_type j lit =