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) =