66 (*** constants with types ***) |
66 (*** constants with types ***) |
67 |
67 |
68 (*An abstraction of Isabelle types*) |
68 (*An abstraction of Isabelle types*) |
69 datatype pseudotype = PVar | PType of string * pseudotype list |
69 datatype pseudotype = PVar | PType of string * pseudotype list |
70 |
70 |
71 fun string_for_pseudotype PVar = "?" |
71 fun string_for_pseudotype PVar = "_" |
72 | string_for_pseudotype (PType (s, Ts)) = |
72 | string_for_pseudotype (PType (s, Ts)) = |
73 (case Ts of |
73 (case Ts of |
74 [] => "" |
74 [] => "" |
75 | [T] => string_for_pseudotype T |
75 | [T] => string_for_pseudotype T ^ " " |
76 | Ts => string_for_pseudotypes Ts ^ " ") ^ s |
76 | Ts => string_for_pseudotypes Ts ^ " ") ^ s |
77 and string_for_pseudotypes Ts = |
77 and string_for_pseudotypes Ts = |
78 "(" ^ commas (map string_for_pseudotype Ts) ^ ")" |
78 "(" ^ commas (map string_for_pseudotype Ts) ^ ")" |
79 |
79 |
80 (*Is the second type an instance of the first one?*) |
80 (*Is the second type an instance of the first one?*) |
316 chop max_imperfect imperfect |>> append perfect |>> chop remaining_max |
316 chop max_imperfect imperfect |>> append perfect |>> chop remaining_max |
317 in |
317 in |
318 trace_msg (fn () => "Number of candidates: " ^ |
318 trace_msg (fn () => "Number of candidates: " ^ |
319 string_of_int (length candidates)); |
319 string_of_int (length candidates)); |
320 trace_msg (fn () => "Effective threshold: " ^ |
320 trace_msg (fn () => "Effective threshold: " ^ |
321 Real.toString (#2 (hd accepts))); |
321 Real.toString (#2 (List.last accepts))); |
322 trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ |
322 trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ |
323 "): " ^ (accepts |
323 "): " ^ (accepts |
324 |> map (fn ((((name, _), _), _), weight) => |
324 |> map (fn ((((name, _), _), _), weight) => |
325 name () ^ " [" ^ Real.toString weight ^ "]") |
325 name () ^ " [" ^ Real.toString weight ^ "]") |
326 |> commas)); |
326 |> commas)); |
595 val named_locals = local_facts |> Facts.dest_static [] |
595 val named_locals = local_facts |> Facts.dest_static [] |
596 val is_chained = member Thm.eq_thm chained_ths |
596 val is_chained = member Thm.eq_thm chained_ths |
597 (* Unnamed nonchained formulas with schematic variables are omitted, because |
597 (* Unnamed nonchained formulas with schematic variables are omitted, because |
598 they are rejected by the backticks (`...`) parser for some reason. *) |
598 they are rejected by the backticks (`...`) parser for some reason. *) |
599 fun is_good_unnamed_local th = |
599 fun is_good_unnamed_local th = |
|
600 not (Thm.has_name_hint th) andalso |
|
601 (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso |
600 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
602 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
601 andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) |
|
602 val unnamed_locals = |
603 val unnamed_locals = |
603 local_facts |> Facts.props |> filter is_good_unnamed_local |
604 union Thm.eq_thm (Facts.props local_facts) chained_ths |
604 |> map (pair "" o single) |
605 |> filter is_good_unnamed_local |> map (pair "" o single) |
605 val full_space = |
606 val full_space = |
606 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) |
607 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) |
607 fun add_facts global foldx facts = |
608 fun add_facts global foldx facts = |
608 foldx (fn (name0, ths) => |
609 foldx (fn (name0, ths) => |
609 if name0 <> "" andalso |
610 if name0 <> "" andalso |