src/Pure/Tools/find_consts.ML
changeset 31684 d5d830979a54
parent 30207 c56d27155041
child 31687 0d2f700fe5e7
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Jun 17 15:00:19 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Jun 17 15:14:48 2009 +0200
     1.3 @@ -25,10 +25,9 @@
     1.4    | Loose of string
     1.5    | Name of string;
     1.6  
     1.7 +
     1.8  (* matching types/consts *)
     1.9  
    1.10 -fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
    1.11 -
    1.12  fun matches_subtype thy typat =
    1.13    let
    1.14      val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    1.15 @@ -51,7 +50,9 @@
    1.16  
    1.17  fun filter_const _ NONE = NONE
    1.18    | filter_const f (SOME (c, r)) =
    1.19 -      Option.map (pair c o (curry Int.min r)) (f c);
    1.20 +      (case f c of
    1.21 +        NONE => NONE
    1.22 +      | SOME i => SOME (c, Int.min (r, i)));
    1.23  
    1.24  
    1.25  (* pretty results *)
    1.26 @@ -76,6 +77,7 @@
    1.27        Pretty.quote (Syntax.pretty_typ ctxt ty')]
    1.28    end;
    1.29  
    1.30 +
    1.31  (* find_consts *)
    1.32  
    1.33  fun find_consts ctxt raw_criteria =
    1.34 @@ -85,16 +87,17 @@
    1.35      val thy = ProofContext.theory_of ctxt;
    1.36      val low_ranking = 10000;
    1.37  
    1.38 -    fun not_internal consts (nm, _) = 
    1.39 +    fun not_internal consts (nm, _) =
    1.40        if member (op =) (Consts.the_tags consts nm) Markup.property_internal
    1.41        then NONE else SOME low_ranking;
    1.42  
    1.43      fun make_pattern crit =
    1.44        let
    1.45          val raw_T = Syntax.parse_typ ctxt crit;
    1.46 -        val t = Syntax.check_term
    1.47 -                  (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    1.48 -                  (Term.dummy_pattern raw_T);
    1.49 +        val t =
    1.50 +          Syntax.check_term
    1.51 +            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    1.52 +            (Term.dummy_pattern raw_T);
    1.53        in Term.type_of t end;
    1.54  
    1.55      fun make_match (Strict arg) =
    1.56 @@ -102,34 +105,34 @@
    1.57              fn (_, (ty, _)) =>
    1.58                let
    1.59                  val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    1.60 -                val sub_size = Vartab.fold add_tye tye 0;
    1.61 +                val sub_size =
    1.62 +                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
    1.63                in SOME sub_size end handle MATCH => NONE
    1.64            end
    1.65 -
    1.66        | make_match (Loose arg) =
    1.67            check_const (matches_subtype thy (make_pattern arg) o snd)
    1.68 -      
    1.69        | make_match (Name arg) = check_const (match_string arg o fst);
    1.70  
    1.71      fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
    1.72      val criteria = map make_criterion raw_criteria;
    1.73  
    1.74      val consts = Sign.consts_of thy;
    1.75 -    val (_, consts_tab) = (#constants o Consts.dest) consts;
    1.76 -    fun eval_entry c = fold filter_const (not_internal consts::criteria)
    1.77 -                                         (SOME (c, low_ranking));
    1.78 +    val (_, consts_tab) = #constants (Consts.dest consts);
    1.79 +    fun eval_entry c =
    1.80 +      fold filter_const (not_internal consts :: criteria)
    1.81 +        (SOME (c, low_ranking));
    1.82  
    1.83      val matches =
    1.84        Symtab.fold (cons o eval_entry) consts_tab []
    1.85        |> map_filter I
    1.86        |> sort (rev_order o int_ord o pairself snd)
    1.87 -      |> map ((apsnd fst) o fst);
    1.88 +      |> map (apsnd fst o fst);
    1.89  
    1.90      val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
    1.91    in
    1.92      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
    1.93        :: Pretty.str ""
    1.94 -      :: (Pretty.str o concat)
    1.95 +      :: (Pretty.str o implode)
    1.96             (if null matches
    1.97              then ["nothing found", end_msg]
    1.98              else ["found ", (string_of_int o length) matches,