src/Pure/Isar/find_consts.ML
changeset 29895 0e70a29d3e02
parent 29884 74c183927054
     1.1 --- a/src/Pure/Isar/find_consts.ML	Fri Feb 13 14:57:25 2009 +1100
     1.2 +++ b/src/Pure/Isar/find_consts.ML	Fri Feb 13 16:00:45 2009 +1100
     1.3 @@ -44,7 +44,31 @@
     1.4  fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
     1.5                                      then NONE else SOME (size_of_typ ty);
     1.6  
     1.7 +fun filter_const (_, NONE) = NONE
     1.8 +  | filter_const (f, (SOME (c, r))) = Option.map
     1.9 +                                        (pair c o ((curry Int.min) r)) (f c);
    1.10 +
    1.11 +fun pretty_criterion (b, c) =
    1.12 +  let
    1.13 +    fun prfx s = if b then s else "-" ^ s;
    1.14 +  in
    1.15 +    (case c of
    1.16 +      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    1.17 +    | Loose pat => Pretty.str (prfx (quote pat))
    1.18 +    | Name name => Pretty.str (prfx "name: " ^ quote name))
    1.19 +  end;
    1.20 +
    1.21 +fun pretty_const ctxt (nm, ty) = let
    1.22 +    val ty' = Logic.unvarifyT ty;
    1.23 +  in
    1.24 +    Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    1.25 +                  Pretty.str "::", Pretty.brk 1,
    1.26 +                  Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.27 +  end;
    1.28 +
    1.29  fun find_consts ctxt raw_criteria = let
    1.30 +    val start = start_timing ();
    1.31 +
    1.32      val thy = ProofContext.theory_of ctxt;
    1.33      val low_ranking = 10000;
    1.34  
    1.35 @@ -68,28 +92,27 @@
    1.36      val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
    1.37  
    1.38      val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    1.39 -
    1.40 -    fun filter_const (_, NONE) = NONE
    1.41 -      | filter_const (f, (SOME (c, r))) = Option.map
    1.42 -                                            (pair c o ((curry Int.min) r))
    1.43 -                                            (f c);
    1.44 -
    1.45      fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
    1.46  
    1.47 -    fun show (nm, ty) = let
    1.48 -        val ty' = Logic.unvarifyT ty;
    1.49 -      in
    1.50 -        (Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    1.51 -                       Pretty.str "::", Pretty.brk 1,
    1.52 -                       Pretty.quote (Syntax.pretty_typ ctxt ty')])
    1.53 -      end;
    1.54 +    val matches = Symtab.fold (cons o eval_entry) consts []
    1.55 +                  |> map_filter I
    1.56 +                  |> sort (rev_order o int_ord o pairself snd)
    1.57 +                  |> map ((apsnd fst) o fst);
    1.58 +
    1.59 +    val end_msg = " in " ^
    1.60 +                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
    1.61 +                  ^ " secs"
    1.62    in
    1.63 -    Symtab.fold (cons o eval_entry) consts []
    1.64 -    |> map_filter I
    1.65 -    |> sort (rev_order o int_ord o pairself snd)
    1.66 -    |> map ((apsnd fst) o fst)
    1.67 -    |> map show
    1.68 -    |> Pretty.big_list "results:"
    1.69 +    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    1.70 +      :: Pretty.str ""
    1.71 +      :: (Pretty.str o concat)
    1.72 +           (if null matches
    1.73 +            then ["nothing found", end_msg]
    1.74 +            else ["found ", (string_of_int o length) matches,
    1.75 +                  " constants", end_msg, ":"])
    1.76 +      :: Pretty.str ""
    1.77 +      :: map (pretty_const ctxt) matches
    1.78 +    |> Pretty.chunks
    1.79      |> Pretty.writeln
    1.80    end handle ERROR s => Output.error_msg s
    1.81