src/Pure/Tools/find_consts.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 30188 82144a95f9ec
child 30206 48507466d9d2
permissions -rw-r--r--
use long names for old-style fold combinators;
     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 default_criteria : (bool * criterion) list ref
    16 
    17   val find_consts : Proof.context -> (bool * criterion) list -> unit
    18 end;
    19 
    20 structure FindConsts : FIND_CONSTS =
    21 struct
    22 
    23 (* search criteria *)
    24 
    25 datatype criterion =
    26     Strict of string
    27   | Loose of string
    28   | Name of string;
    29 
    30 val default_criteria = ref [(false, Name ".sko_")];
    31 
    32 
    33 (* matching types/consts *)
    34 
    35 fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
    36 
    37 fun matches_subtype thy typat =
    38   let
    39     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    40 
    41     fun fs [] = false
    42       | fs (t :: ts) = f t orelse fs ts
    43 
    44     and f (t as Type (_, ars)) = p t orelse fs ars
    45       | f t = p t;
    46   in f end;
    47 
    48 fun check_const p (nm, (ty, _)) =
    49   if p (nm, ty)
    50   then SOME (Term.size_of_typ ty)
    51   else NONE;
    52 
    53 fun opt_not f (c as (_, (ty, _))) =
    54   if is_some (f c)
    55   then NONE else SOME (Term.size_of_typ ty);
    56 
    57 fun filter_const (_, NONE) = NONE
    58   | filter_const (f, (SOME (c, r))) =
    59       Option.map (pair c o (curry Int.min r)) (f c);
    60 
    61 
    62 (* pretty results *)
    63 
    64 fun pretty_criterion (b, c) =
    65   let
    66     fun prfx s = if b then s else "-" ^ s;
    67   in
    68     (case c of
    69       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    70     | Loose pat => Pretty.str (prfx (quote pat))
    71     | Name name => Pretty.str (prfx "name: " ^ quote name))
    72   end;
    73 
    74 fun pretty_const ctxt (nm, ty) =
    75   let
    76     val ty' = Logic.unvarifyT ty;
    77   in
    78     Pretty.block
    79      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    80       Pretty.str "::", Pretty.brk 1,
    81       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    82   end;
    83 
    84 
    85 (* find_consts *)
    86 
    87 fun find_consts ctxt raw_criteria =
    88   let
    89     val start = start_timing ();
    90 
    91     val thy = ProofContext.theory_of ctxt;
    92     val low_ranking = 10000;
    93 
    94     fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |> Term.type_of;
    95 
    96     fun make_match (Strict arg) =
    97           let val qty = make_pattern arg; in
    98             fn (_, (ty, _)) =>
    99               let
   100                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
   101                 val sub_size = Vartab.fold add_tye tye 0;
   102               in SOME sub_size end handle MATCH => NONE
   103           end
   104 
   105       | make_match (Loose arg) =
   106           check_const (matches_subtype thy (make_pattern arg) o snd)
   107       
   108       | make_match (Name arg) = check_const (match_string arg o fst);
   109 
   110     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   111     val criteria = map make_criterion (! default_criteria @ raw_criteria);
   112 
   113     val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
   114     fun eval_entry c = List.foldl filter_const (SOME (c, low_ranking)) criteria;
   115 
   116     val matches =
   117       Symtab.fold (cons o eval_entry) consts []
   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 handle ERROR s => Output.error_msg s;
   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