1 (* Title: HOL/Tools/ATP/atp_util.ML
2 Author: Jasmin Blanchette, TU Muenchen
4 General-purpose functions used by the ATP module.
9 val timestamp : unit -> string
10 val hashw : word * word -> word
11 val hashw_string : string * word -> word
12 val strip_spaces : bool -> (char -> bool) -> string -> string
13 val nat_subscript : int -> string
14 val unyxml : string -> string
15 val maybe_quote : string -> string
16 val string_from_ext_time : bool * Time.time -> string
17 val string_from_time : Time.time -> string
18 val varify_type : Proof.context -> typ -> typ
19 val instantiate_type : theory -> typ -> typ -> typ -> typ
20 val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
22 Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
24 val is_type_surely_finite : Proof.context -> bool -> typ -> bool
25 val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
26 val monomorphic_term : Type.tyenv -> term -> term
27 val eta_expand : typ list -> term -> int -> term
28 val transform_elim_prop : term -> term
29 val specialize_type : theory -> (string * typ) -> term -> term
31 Proof.context -> thm -> int -> (string * typ) list * term list * term
34 structure ATP_Util : ATP_UTIL =
37 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
39 (* This hash function is recommended in "Compilers: Principles, Techniques, and
40 Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
41 particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
42 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
43 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
44 fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
46 fun strip_c_style_comment _ [] = []
47 | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
48 strip_spaces_in_list true is_evil cs
49 | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
50 and strip_spaces_in_list _ _ [] = []
51 | strip_spaces_in_list true is_evil (#"%" :: cs) =
52 strip_spaces_in_list true is_evil
53 (cs |> chop_while (not_equal #"\n") |> snd)
54 | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
55 strip_c_style_comment is_evil cs
56 | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
57 | strip_spaces_in_list skip_comments is_evil [c1, c2] =
58 strip_spaces_in_list skip_comments is_evil [c1] @
59 strip_spaces_in_list skip_comments is_evil [c2]
60 | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
61 if Char.isSpace c1 then
62 strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
63 else if Char.isSpace c2 then
64 if Char.isSpace c3 then
65 strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
67 str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
68 strip_spaces_in_list skip_comments is_evil (c3 :: cs)
70 str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
71 fun strip_spaces skip_comments is_evil =
72 implode o strip_spaces_in_list skip_comments is_evil o String.explode
74 val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
76 n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
78 val unyxml = XML.content_of o YXML.parse_body
80 val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
82 let val s = unyxml y in
83 y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
84 not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
85 Keyword.is_keyword s) ? quote
88 fun string_from_ext_time (plus, time) =
89 let val ms = Time.toMilliseconds time in
90 (if plus then "> " else "") ^
91 (if plus andalso ms mod 1000 = 0 then
92 signed_string_of_int (ms div 1000) ^ " s"
93 else if ms < 1000 then
94 signed_string_of_int ms ^ " ms"
96 string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
99 val string_from_time = string_from_ext_time o pair false
101 fun varify_type ctxt T =
102 Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
103 |> snd |> the_single |> dest_Const |> snd
105 (* TODO: use "Term_Subst.instantiateT" instead? *)
106 fun instantiate_type thy T1 T1' T2 =
107 Same.commit (Envir.subst_type_same
108 (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
109 handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
111 fun varify_and_instantiate_type ctxt T1 T1' T2 =
112 let val thy = Proof_Context.theory_of ctxt in
113 instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
116 fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
117 the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
118 | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
119 Type (s, map (typ_of_dtyp descr typ_assoc) Us)
120 | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
121 let val (s, ds, _) = the (AList.lookup (op =) descr i) in
122 Type (s, map (typ_of_dtyp descr typ_assoc) ds)
125 fun datatype_constrs thy (T as Type (s, Ts)) =
126 (case Datatype.get_info thy s of
127 SOME {index, descr, ...} =>
128 let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
129 map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
133 | datatype_constrs _ _ = []
135 (* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
136 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
137 cardinality 2 or more. The specified default cardinality is returned if the
138 cardinality of the type can't be determined. *)
139 fun tiny_card_of_type ctxt sound default_card T =
141 val thy = Proof_Context.theory_of ctxt
142 val max = 2 (* 1 would be too small for the "fun" case *)
143 fun aux slack avoid T =
144 if member (op =) avoid T then
147 Type (@{type_name fun}, [T1, T2]) =>
148 (case (aux slack avoid T1, aux slack avoid T2) of
149 (k, 1) => if slack andalso k = 0 then 0 else 1
153 if k1 >= max orelse k2 >= max then max
154 else Int.min (max, Integer.pow k2 k1))
156 | @{typ bool} => 2 (* optimization *)
157 | @{typ nat} => 0 (* optimization *)
158 | Type ("Int.int", []) => 0 (* optimization *)
160 (case datatype_constrs thy T of
164 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
167 if exists (curry (op =) 0) constr_cards then 0
168 else Int.min (max, Integer.sum constr_cards)
171 case Typedef.get_info ctxt s of
172 ({abs_type, rep_type, ...}, _) :: _ =>
173 (* We cheat here by assuming that typedef types are infinite if
174 their underlying type is infinite. This is unsound in general
175 but it's hard to think of a realistic example where this would
176 not be the case. We are also slack with representation types:
177 If a representation type has the form "sigma => tau", we
178 consider it enough to check "sigma" for infiniteness. (Look
179 for "slack" in this function.) *)
180 (case varify_and_instantiate_type ctxt
181 (Logic.varifyT_global abs_type) T
182 (Logic.varifyT_global rep_type)
184 0 => if sound then default_card else 0
187 | [] => default_card)
188 (* Very slightly unsound: Type variables are assumed not to be
189 constrained to cardinality 1. (In practice, the user would most
190 likely have used "unit" directly anyway.) *)
192 if default_card = 1 andalso not sound then 2 else default_card
193 | TVar _ => default_card
194 in Int.min (max, aux false [] T) end
196 fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
197 fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
199 fun monomorphic_term subst =
200 map_types (map_type_tvar (fn v =>
201 case Type.lookup subst v of
205 fun eta_expand _ t 0 = t
206 | eta_expand Ts (Abs (s, T, t')) n =
207 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
208 | eta_expand Ts t n =
209 fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
210 (List.take (binder_types (fastype_of1 (Ts, t)), n))
211 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
213 (* Converts an elim-rule into an equivalent theorem that does not have the
214 predicate variable. Leaves other theorems unchanged. We simply instantiate
215 the conclusion variable to False. (Cf. "transform_elim_theorem" in
216 "Meson_Clausify".) *)
217 fun transform_elim_prop t =
218 case Logic.strip_imp_concl t of
219 @{const Trueprop} $ Var (z, @{typ bool}) =>
220 subst_Vars [(z, @{const False})] t
221 | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
224 fun specialize_type thy (s, T) t =
226 fun subst_for (Const (s', T')) =
228 SOME (Sign.typ_match thy (T', T) Vartab.empty)
229 handle Type.TYPE_MATCH => NONE
232 | subst_for (t1 $ t2) =
233 (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
234 | subst_for (Abs (_, _, t')) = subst_for t'
238 SOME subst => monomorphic_term subst t
239 | NONE => raise Type.TYPE_MATCH
242 fun strip_subgoal ctxt goal i =
244 val (t, (frees, params)) =
245 Logic.goal_params (prop_of goal) i
246 ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
247 val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
248 val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
249 in (rev params, hyp_ts, concl_t) end