src/Pure/Tools/find_theorems.ML
 changeset 30785 15f64e05e703 parent 30693 c672c8162f4b child 30822 8aac4b974280
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 29 19:48:35 2009 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Mar 30 12:25:52 2009 +1100
1.3 @@ -11,8 +11,8 @@
1.4      Pattern of 'term
1.5    val tac_limit: int ref
1.6    val limit: int ref
1.7 -  val find_theorems: Proof.context -> thm option -> bool ->
1.8 -    (bool * string criterion) list -> (Facts.ref * thm) list
1.9 +  val find_theorems: Proof.context -> thm option -> int option -> bool ->
1.10 +    (bool * string criterion) list -> int option * (Facts.ref * thm) list
1.11    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
1.12    val print_theorems: Proof.context -> thm option -> int option -> bool ->
1.13      (bool * string criterion) list -> unit
1.14 @@ -254,12 +254,13 @@
1.15            in app (opt_add r r', consts', fs) end;
1.16    in app end;
1.17
1.18 +
1.19  in
1.20
1.21  fun filter_criterion ctxt opt_goal (b, c) =
1.22    (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
1.23
1.24 -fun all_filters filters thms =
1.25 +fun sorted_filter filters thms =
1.26    let
1.27      fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters);
1.28
1.29 @@ -270,6 +271,15 @@
1.30        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
1.31    in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
1.32
1.33 +fun lazy_filter filters = let
1.34 +    fun lazy_match thms = Seq.make (fn () => first_match thms)
1.35 +
1.36 +    and first_match [] = NONE
1.37 +      | first_match (thm::thms) =
1.38 +          case app_filters thm (SOME (0, 0), NONE, filters) of
1.39 +            NONE => first_match thms
1.40 +          | SOME (_, t) => SOME (t, lazy_match thms);
1.41 +  in lazy_match end;
1.42  end;
1.43
1.44
1.45 @@ -334,7 +344,7 @@
1.46
1.47  val limit = ref 40;
1.48
1.49 -fun find_theorems ctxt opt_goal rem_dups raw_criteria =
1.50 +fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.51    let
1.52      val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
1.53                  handle ERROR _ => [];
1.54 @@ -344,13 +354,25 @@
1.55      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.56      val filters = map (filter_criterion ctxt opt_goal') criteria;
1.57
1.58 -    val raw_matches = all_filters filters (all_facts_of ctxt);
1.59 +    fun find_all facts =
1.60 +      let
1.61 +        val raw_matches = sorted_filter filters facts;
1.62 +
1.63 +        val matches =
1.64 +          if rem_dups
1.65 +          then rem_thm_dups (nicer_shortest ctxt) raw_matches
1.66 +          else raw_matches;
1.67
1.68 -    val matches =
1.69 -      if rem_dups
1.70 -      then rem_thm_dups (nicer_shortest ctxt) raw_matches
1.71 -      else raw_matches;
1.72 -  in matches end;
1.73 +        val len = length matches;
1.74 +        val lim = the_default (! limit) opt_limit;
1.75 +      in (SOME len, Library.drop (len - lim, matches)) end;
1.76 +
1.77 +    val find =
1.78 +      if rem_dups orelse is_none opt_limit
1.79 +      then find_all
1.80 +      else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
1.81 +
1.82 +  in find (all_facts_of ctxt) end;
1.83
1.84
1.85  fun pretty_thm ctxt (thmref, thm) = Pretty.block
1.86 @@ -362,11 +384,16 @@
1.87      val start = start_timing ();
1.88
1.89      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.90 -    val matches = find_theorems ctxt opt_goal rem_dups raw_criteria;
1.91 -
1.92 -    val len = length matches;
1.93 -    val lim = the_default (! limit) opt_limit;
1.94 -    val thms = Library.drop (len - lim, matches);
1.95 +    val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
1.96 +    val returned = length thms;
1.97 +
1.98 +    val tally_msg =
1.99 +      case foundo of
1.100 +        NONE => "displaying " ^ string_of_int returned ^ " theorems"
1.101 +      | SOME found => "found " ^ string_of_int found ^ " theorems" ^
1.102 +                      (if returned < found
1.103 +                       then " (" ^ string_of_int returned ^ " displayed)"
1.104 +                       else "");
1.105
1.106      val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
1.107    in
1.108 @@ -374,16 +401,12 @@
1.109          :: Pretty.str "" ::
1.110       (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
1.111        else
1.112 -        [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
1.113 -          (if len <= lim then ""
1.114 -           else " (" ^ string_of_int lim ^ " displayed)")
1.115 -           ^ end_msg ^ ":"), Pretty.str ""] @
1.116 +        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
1.117          map (pretty_thm ctxt) thms)
1.118      |> Pretty.chunks |> Pretty.writeln
1.119    end;
1.120
1.121
1.122 -
1.123  (** command syntax **)
1.124
1.125  fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
```