src/Pure/Tools/find_consts.ML
author Timothy Bourke
Mon Mar 02 18:11:39 2009 +1100 (2009-03-02)
changeset 30206 48507466d9d2
parent 30190 479806475f3c
child 30207 c56d27155041
permissions -rw-r--r--
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
     1 (*  Title:      Pure/Tools/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
     5 type over constants, but matching is not fuzzy.
     6 *)
     7 
     8 signature FIND_CONSTS =
     9 sig
    10   datatype criterion =
    11       Strict of string
    12     | Loose of string
    13     | Name of string
    14 
    15   val find_consts : Proof.context -> (bool * criterion) list -> unit
    16 end;
    17 
    18 structure FindConsts : FIND_CONSTS =
    19 struct
    20 
    21 (* search criteria *)
    22 
    23 datatype criterion =
    24     Strict of string
    25   | Loose of string
    26   | Name of string;
    27 
    28 (* matching types/consts *)
    29 
    30 fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
    31 
    32 fun matches_subtype thy typat =
    33   let
    34     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    35 
    36     fun fs [] = false
    37       | fs (t :: ts) = f t orelse fs ts
    38 
    39     and f (t as Type (_, ars)) = p t orelse fs ars
    40       | f t = p t;
    41   in f end;
    42 
    43 fun check_const p (nm, (ty, _)) =
    44   if p (nm, ty)
    45   then SOME (Term.size_of_typ ty)
    46   else NONE;
    47 
    48 fun opt_not f (c as (_, (ty, _))) =
    49   if is_some (f c)
    50   then NONE else SOME (Term.size_of_typ ty);
    51 
    52 fun filter_const _ NONE = NONE
    53   | filter_const f (SOME (c, r)) =
    54       Option.map (pair c o (curry Int.min r)) (f c);
    55 
    56 
    57 (* pretty results *)
    58 
    59 fun pretty_criterion (b, c) =
    60   let
    61     fun prfx s = if b then s else "-" ^ s;
    62   in
    63     (case c of
    64       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    65     | Loose pat => Pretty.str (prfx (quote pat))
    66     | Name name => Pretty.str (prfx "name: " ^ quote name))
    67   end;
    68 
    69 fun pretty_const ctxt (nm, ty) =
    70   let
    71     val ty' = Logic.unvarifyT ty;
    72   in
    73     Pretty.block
    74      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    75       Pretty.str "::", Pretty.brk 1,
    76       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    77   end;
    78 
    79 (* find_consts *)
    80 
    81 fun find_consts ctxt raw_criteria =
    82   let
    83     val start = start_timing ();
    84 
    85     val thy = ProofContext.theory_of ctxt;
    86     val low_ranking = 10000;
    87 
    88     fun not_internal consts (nm, _) = 
    89       if member (op =) (Consts.the_tags consts nm) Markup.property_internal
    90       then NONE else SOME low_ranking;
    91 
    92     fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> type_of;
    93 
    94     fun make_match (Strict arg) =
    95           let val qty = make_pattern arg; in
    96             fn (_, (ty, _)) =>
    97               let
    98                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    99                 val sub_size = Vartab.fold add_tye tye 0;
   100               in SOME sub_size end handle MATCH => NONE
   101           end
   102 
   103       | make_match (Loose arg) =
   104           check_const (matches_subtype thy (make_pattern arg) o snd)
   105       
   106       | make_match (Name arg) = check_const (match_string arg o fst);
   107 
   108     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   109     val criteria = map make_criterion raw_criteria;
   110 
   111     val consts = Sign.consts_of thy;
   112     val (_, consts_tab) = (#constants o Consts.dest) consts;
   113     fun eval_entry c = fold filter_const (not_internal consts::criteria)
   114                                          (SOME (c, low_ranking));
   115 
   116     val matches =
   117       Symtab.fold (cons o eval_entry) consts_tab []
   118       |> map_filter I
   119       |> sort (rev_order o int_ord o pairself snd)
   120       |> map ((apsnd fst) o fst);
   121 
   122     val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
   123   in
   124     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   125       :: Pretty.str ""
   126       :: (Pretty.str o concat)
   127            (if null matches
   128             then ["nothing found", end_msg]
   129             else ["found ", (string_of_int o length) matches,
   130                   " constants", end_msg, ":"])
   131       :: Pretty.str ""
   132       :: map (pretty_const ctxt) matches
   133     |> Pretty.chunks
   134     |> Pretty.writeln
   135   end;
   136 
   137 
   138 (* command syntax *)
   139 
   140 fun find_consts_cmd spec =
   141   Toplevel.unknown_theory o Toplevel.keep (fn state =>
   142     find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
   143 
   144 local
   145 
   146 structure P = OuterParse and K = OuterKeyword;
   147 
   148 val criterion =
   149   P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   150   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   151   P.xname >> Loose;
   152 
   153 in
   154 
   155 val _ =
   156   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   157     (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   158       >> (Toplevel.no_timing oo find_consts_cmd));
   159 
   160 end;
   161 
   162 end;
   163