src/Pure/Isar/find_consts.ML
author kleing
Fri Feb 13 16:00:45 2009 +1100 (2009-02-13)
changeset 29895 0e70a29d3e02
parent 29884 74c183927054
permissions -rw-r--r--
find_consts: display the search criteria. (by Timothy Bourke)
     1 (*  Title:      find_consts.ML
     2     Author:     Timothy Bourke and Gerwin Klein, NICTA
     3 
     4   Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
     5   over constants, but matching is not fuzzy
     6 *)
     7 
     8 signature FIND_CONSTS =
     9 sig
    10   datatype criterion = Strict of string
    11                      | Loose of string
    12                      | Name of string
    13 
    14   val default_criteria : (bool * criterion) list ref
    15 
    16   val find_consts : Proof.context -> (bool * criterion) list -> unit
    17 end;
    18 
    19 structure FindConsts : FIND_CONSTS =
    20 struct
    21 
    22 datatype criterion = Strict of string
    23                    | Loose of string
    24                    | Name of string;
    25 
    26 val default_criteria = ref [(false, Name ".sko_")];
    27 
    28 fun add_tye (_, (_, t)) n = size_of_typ t + n;
    29 
    30 fun matches_subtype thy typat = let
    31     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    32 
    33     fun fs [] = false
    34       | fs (t::ts) = f t orelse fs ts
    35 
    36     and f (t as Type (_, ars)) = p t orelse fs ars
    37       | f t = p t;
    38   in f end;
    39 
    40 fun check_const p (nm, (ty, _)) = if p (nm, ty)
    41                                   then SOME (size_of_typ ty)
    42                                   else NONE;
    43 
    44 fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
    45                                     then NONE else SOME (size_of_typ ty);
    46 
    47 fun filter_const (_, NONE) = NONE
    48   | filter_const (f, (SOME (c, r))) = Option.map
    49                                         (pair c o ((curry Int.min) r)) (f c);
    50 
    51 fun pretty_criterion (b, c) =
    52   let
    53     fun prfx s = if b then s else "-" ^ s;
    54   in
    55     (case c of
    56       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    57     | Loose pat => Pretty.str (prfx (quote pat))
    58     | Name name => Pretty.str (prfx "name: " ^ quote name))
    59   end;
    60 
    61 fun pretty_const ctxt (nm, ty) = let
    62     val ty' = Logic.unvarifyT ty;
    63   in
    64     Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    65                   Pretty.str "::", Pretty.brk 1,
    66                   Pretty.quote (Syntax.pretty_typ ctxt ty')]
    67   end;
    68 
    69 fun find_consts ctxt raw_criteria = let
    70     val start = start_timing ();
    71 
    72     val thy = ProofContext.theory_of ctxt;
    73     val low_ranking = 10000;
    74 
    75     fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
    76                             |> type_of;
    77 
    78     fun make_match (Strict arg) =
    79           let val qty = make_pattern arg; in
    80             fn (_, (ty, _)) => let
    81                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    82                 val sub_size = Vartab.fold add_tye tye 0;
    83               in SOME sub_size end handle MATCH => NONE
    84           end
    85 
    86       | make_match (Loose arg) =
    87           check_const (matches_subtype thy (make_pattern arg) o snd)
    88       
    89       | make_match (Name arg) = check_const (match_string arg o fst);
    90 
    91     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
    92     val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
    93 
    94     val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    95     fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
    96 
    97     val matches = Symtab.fold (cons o eval_entry) consts []
    98                   |> map_filter I
    99                   |> sort (rev_order o int_ord o pairself snd)
   100                   |> map ((apsnd fst) o fst);
   101 
   102     val end_msg = " in " ^
   103                   (List.nth (String.tokens Char.isSpace (end_timing start), 3))
   104                   ^ " secs"
   105   in
   106     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   107       :: Pretty.str ""
   108       :: (Pretty.str o concat)
   109            (if null matches
   110             then ["nothing found", end_msg]
   111             else ["found ", (string_of_int o length) matches,
   112                   " constants", end_msg, ":"])
   113       :: Pretty.str ""
   114       :: map (pretty_const ctxt) matches
   115     |> Pretty.chunks
   116     |> Pretty.writeln
   117   end handle ERROR s => Output.error_msg s
   118 
   119 end;
   120