misc tuning and simplification;
authorwenzelm
Wed Aug 11 18:03:02 2010 +0200 (2010-08-11)
changeset 38335630f379f2660
parent 38334 c677c2c1d333
child 38336 fd53ae1d4c47
misc tuning and simplification;
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Aug 11 17:50:29 2010 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Aug 11 18:03:02 2010 +0200
     1.3 @@ -28,24 +28,13 @@
     1.4  (* matching types/consts *)
     1.5  
     1.6  fun matches_subtype thy typat =
     1.7 -  let
     1.8 -    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
     1.9 -
    1.10 -    fun fs [] = false
    1.11 -      | fs (t :: ts) = f t orelse fs ts
    1.12 +  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
    1.13  
    1.14 -    and f (t as Type (_, ars)) = p t orelse fs ars
    1.15 -      | f t = p t;
    1.16 -  in f end;
    1.17 -
    1.18 -fun check_const p (nm, (ty, _)) =
    1.19 -  if p (nm, ty)
    1.20 -  then SOME (Term.size_of_typ ty)
    1.21 -  else NONE;
    1.22 +fun check_const pred (nm, (ty, _)) =
    1.23 +  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
    1.24  
    1.25  fun opt_not f (c as (_, (ty, _))) =
    1.26 -  if is_some (f c)
    1.27 -  then NONE else SOME (Term.size_of_typ ty);
    1.28 +  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
    1.29  
    1.30  fun filter_const _ NONE = NONE
    1.31    | filter_const f (SOME (c, r)) =
    1.32 @@ -128,18 +117,15 @@
    1.33  
    1.34      val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
    1.35    in
    1.36 -    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    1.37 -      :: Pretty.str ""
    1.38 -      :: (Pretty.str o implode)
    1.39 -           (if null matches
    1.40 -            then ["nothing found", end_msg]
    1.41 -            else ["found ", (string_of_int o length) matches,
    1.42 -                  " constants", end_msg, ":"])
    1.43 -      :: Pretty.str ""
    1.44 -      :: map (pretty_const ctxt) matches
    1.45 -    |> Pretty.chunks
    1.46 -    |> Pretty.writeln
    1.47 -  end;
    1.48 +    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    1.49 +    Pretty.str "" ::
    1.50 +    Pretty.str
    1.51 +     (if null matches
    1.52 +      then "nothing found" ^ end_msg
    1.53 +      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
    1.54 +    Pretty.str "" ::
    1.55 +    map (pretty_const ctxt) matches
    1.56 +  end |> Pretty.chunks |> Pretty.writeln;
    1.57  
    1.58  
    1.59  (* command syntax *)
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Aug 11 17:50:29 2010 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Aug 11 18:03:02 2010 +0200
     2.3 @@ -433,23 +433,22 @@
     2.4  
     2.5      val tally_msg =
     2.6        (case foundo of
     2.7 -        NONE => "displaying " ^ string_of_int returned ^ " theorems"
     2.8 +        NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
     2.9        | SOME found =>
    2.10 -          "found " ^ string_of_int found ^ " theorems" ^
    2.11 +          "found " ^ string_of_int found ^ " theorem(s)" ^
    2.12              (if returned < found
    2.13               then " (" ^ string_of_int returned ^ " displayed)"
    2.14               else ""));
    2.15  
    2.16      val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
    2.17    in
    2.18 -    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
    2.19 -        :: Pretty.str "" ::
    2.20 -     (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
    2.21 -      else
    2.22 -        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
    2.23 +    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    2.24 +    Pretty.str "" ::
    2.25 +    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
    2.26 +     else
    2.27 +      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
    2.28          map (pretty_thm ctxt) thms)
    2.29 -    |> Pretty.chunks |> Pretty.writeln
    2.30 -  end;
    2.31 +  end |> Pretty.chunks |> Pretty.writeln;
    2.32  
    2.33  
    2.34