Remove duplicates from printed theorems in find_theorems
authorkleing
Tue Feb 20 00:14:33 2007 +0100 (2007-02-20 ago)
changeset 22340275802767bf3
parent 22339 0dc6b45e5662
child 22341 306488144b4a
Remove duplicates from printed theorems in find_theorems
(still pretty slow, needs optimising).
Added syntax "find_theorems (..) with_dups .." to switch off removal.
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/find_theorems.ML	Mon Feb 19 16:44:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/find_theorems.ML	Tue Feb 20 00:14:33 2007 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  sig
     1.5    datatype 'term criterion =
     1.6      Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
     1.7 -  val print_theorems: Proof.context -> term option -> int option ->
     1.8 +  val print_theorems: Proof.context -> term option -> int option -> bool ->
     1.9      (bool * string criterion) list -> unit
    1.10  end;
    1.11  
    1.12 @@ -227,12 +227,43 @@
    1.13    in
    1.14      map (`(eval_filters filters)) thms
    1.15      |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
    1.16 -    |> sort thm_ord |> map #2
    1.17 +    |> sort thm_ord |> map #2 
    1.18    end;
    1.19  
    1.20  end;
    1.21  
    1.22  
    1.23 +(* removing duplicates, preferring nicer names *)
    1.24 +
    1.25 +fun rem_thm_dups xs =
    1.26 +    let 
    1.27 +      fun nicer (Fact x) (Fact y) = size x <= size y
    1.28 +        | nicer (Fact _) _        = true
    1.29 +        | nicer (PureThy.Name x) (PureThy.Name y) = size x <= size y
    1.30 +        | nicer (PureThy.Name _) (Fact _) = false
    1.31 +        | nicer (PureThy.Name _) _ = true
    1.32 +        | nicer (NameSelection (x,_)) (NameSelection (y,_)) = size x <= size y
    1.33 +        | nicer (NameSelection _) _ = false;
    1.34 +
    1.35 +      fun is_in [] _ = NONE
    1.36 +        | is_in ((n,t) :: xs) t' = if eq_thm (t, t') 
    1.37 +                                   then SOME (n,t) 
    1.38 +                                   else is_in xs t';
    1.39 +
    1.40 +      fun eq ((_,t1),(_,t2)) = eq_thm (t1,t2)
    1.41 +
    1.42 +      fun rem_d (rev_seen, []) = rev rev_seen
    1.43 +        | rem_d (rev_seen, (x as (n',t')) :: xs) = 
    1.44 +          case is_in rev_seen t' of 
    1.45 +            NONE => rem_d (x::rev_seen, xs)
    1.46 +          | SOME (n,t) => if nicer n n' 
    1.47 +                          then rem_d (rev_seen, xs) 
    1.48 +                          else rem_d (x::remove eq (n,t) rev_seen,xs)
    1.49 +
    1.50 +    in rem_d ([], xs) end;
    1.51 +
    1.52 +
    1.53 +
    1.54  (* print_theorems *)
    1.55  
    1.56  fun find_thms ctxt spec =
    1.57 @@ -243,25 +274,28 @@
    1.58      |> distinct (fn ((r1, th1), (r2, th2)) =>
    1.59          r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
    1.60  
    1.61 -fun print_theorems ctxt opt_goal opt_limit raw_criteria =
    1.62 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.63    let
    1.64      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.65      val filters = map (filter_criterion ctxt opt_goal) criteria;
    1.66  
    1.67 -    val matches = all_filters filters (find_thms ctxt ([], []));
    1.68 +    val raw_matches = all_filters filters (find_thms ctxt ([], []));
    1.69 +    val matches = if rem_dups then rem_thm_dups raw_matches else raw_matches;
    1.70 +
    1.71      val len = length matches;
    1.72      val limit = the_default (! thms_containing_limit) opt_limit;
    1.73 +    val thms = Library.drop (len - limit, matches);
    1.74  
    1.75      fun prt_fact (thmref, thm) =
    1.76        ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
    1.77    in
    1.78      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
    1.79 -     (if null matches then [Pretty.str "nothing found"]
    1.80 +     (if null thms then [Pretty.str "nothing found"]
    1.81        else
    1.82          [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
    1.83            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"),
    1.84           Pretty.str ""] @
    1.85 -        map prt_fact (Library.drop (len - limit, matches)))
    1.86 +        map prt_fact thms)
    1.87      |> Pretty.chunks |> Pretty.writeln
    1.88    end;
    1.89  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Feb 19 16:44:08 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Feb 20 00:14:33 2007 +0100
     2.3 @@ -94,7 +94,7 @@
     2.4    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     2.5    val class_deps: Toplevel.transition -> Toplevel.transition
     2.6    val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
     2.7 -  val find_theorems: int option * (bool * string FindTheorems.criterion) list
     2.8 +  val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     2.9      -> Toplevel.transition -> Toplevel.transition
    2.10    val print_binds: Toplevel.transition -> Toplevel.transition
    2.11    val print_cases: Toplevel.transition -> Toplevel.transition
    2.12 @@ -509,12 +509,13 @@
    2.13  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    2.14    ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
    2.15  
    2.16 -fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    2.17 +fun find_theorems ((opt_lim, rem_dups), spec) = 
    2.18 +  Toplevel.unknown_theory o Toplevel.keep (fn state =>
    2.19    let
    2.20      val proof_state = Toplevel.enter_proof_body state;
    2.21      val ctxt = Proof.context_of proof_state;
    2.22      val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
    2.23 -  in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
    2.24 +  in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    2.25  
    2.26  
    2.27  (* print proof context contents *)
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 19 16:44:08 2007 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 20 00:14:33 2007 +0100
     3.3 @@ -810,6 +810,7 @@
     3.4    OuterSyntax.improper_command "find_theorems"
     3.5      "print theorems meeting specified criteria" K.diag
     3.6      (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
     3.7 +     Scan.optional (P.reserved "with_dups" >> K false) true -- 
     3.8       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
     3.9        >> (Toplevel.no_timing oo IsarCmd.find_theorems));
    3.10