src/Pure/Tools/find_consts.ML
author wenzelm
Wed Sep 30 22:31:16 2009 +0200 (2009-09-30)
changeset 32790 a7b92f98180b
parent 31687 0d2f700fe5e7
child 33158 6e3dc0ba2b06
permissions -rw-r--r--
handle Type.TYPE_MATCH, not arbitrary exceptions;
     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 
    29 (* matching types/consts *)
    30 
    31 fun matches_subtype thy typat =
    32   let
    33     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    34 
    35     fun fs [] = false
    36       | fs (t :: ts) = f t orelse fs ts
    37 
    38     and f (t as Type (_, ars)) = p t orelse fs ars
    39       | f t = p t;
    40   in f end;
    41 
    42 fun check_const p (nm, (ty, _)) =
    43   if p (nm, ty)
    44   then SOME (Term.size_of_typ ty)
    45   else NONE;
    46 
    47 fun opt_not f (c as (_, (ty, _))) =
    48   if is_some (f c)
    49   then NONE else SOME (Term.size_of_typ ty);
    50 
    51 fun filter_const _ NONE = NONE
    52   | filter_const f (SOME (c, r)) =
    53       (case f c of
    54         NONE => NONE
    55       | SOME i => SOME (c, Int.min (r, i)));
    56 
    57 
    58 (* pretty results *)
    59 
    60 fun pretty_criterion (b, c) =
    61   let
    62     fun prfx s = if b then s else "-" ^ s;
    63   in
    64     (case c of
    65       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    66     | Loose pat => Pretty.str (prfx (quote pat))
    67     | Name name => Pretty.str (prfx "name: " ^ quote name))
    68   end;
    69 
    70 fun pretty_const ctxt (nm, ty) =
    71   let
    72     val ty' = Logic.unvarifyT ty;
    73   in
    74     Pretty.block
    75      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    76       Pretty.str "::", Pretty.brk 1,
    77       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    78   end;
    79 
    80 
    81 (* find_consts *)
    82 
    83 fun find_consts ctxt raw_criteria =
    84   let
    85     val start = start_timing ();
    86 
    87     val thy = ProofContext.theory_of ctxt;
    88     val low_ranking = 10000;
    89 
    90     fun not_internal consts (nm, _) =
    91       if member (op =) (Consts.the_tags consts nm) Markup.property_internal
    92       then NONE else SOME low_ranking;
    93 
    94     fun make_pattern crit =
    95       let
    96         val raw_T = Syntax.parse_typ ctxt crit;
    97         val t =
    98           Syntax.check_term
    99             (ProofContext.set_mode ProofContext.mode_pattern ctxt)
   100             (Term.dummy_pattern raw_T);
   101       in Term.type_of t end;
   102 
   103     fun make_match (Strict arg) =
   104           let val qty = make_pattern arg; in
   105             fn (_, (ty, _)) =>
   106               let
   107                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
   108                 val sub_size =
   109                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
   110               in SOME sub_size end handle Type.TYPE_MATCH => NONE
   111           end
   112       | make_match (Loose arg) =
   113           check_const (matches_subtype thy (make_pattern arg) o snd)
   114       | make_match (Name arg) = check_const (match_string arg o fst);
   115 
   116     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   117     val criteria = map make_criterion raw_criteria;
   118 
   119     val consts = Sign.consts_of thy;
   120     val (_, consts_tab) = #constants (Consts.dest consts);
   121     fun eval_entry c =
   122       fold filter_const (not_internal consts :: criteria)
   123         (SOME (c, low_ranking));
   124 
   125     val matches =
   126       Symtab.fold (cons o eval_entry) consts_tab []
   127       |> map_filter I
   128       |> sort (rev_order o int_ord o pairself snd)
   129       |> map (apsnd fst o fst);
   130 
   131     val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   132   in
   133     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   134       :: Pretty.str ""
   135       :: (Pretty.str o implode)
   136            (if null matches
   137             then ["nothing found", end_msg]
   138             else ["found ", (string_of_int o length) matches,
   139                   " constants", end_msg, ":"])
   140       :: Pretty.str ""
   141       :: map (pretty_const ctxt) matches
   142     |> Pretty.chunks
   143     |> Pretty.writeln
   144   end;
   145 
   146 
   147 (* command syntax *)
   148 
   149 fun find_consts_cmd spec =
   150   Toplevel.unknown_theory o Toplevel.keep (fn state =>
   151     find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
   152 
   153 local
   154 
   155 structure P = OuterParse and K = OuterKeyword;
   156 
   157 val criterion =
   158   P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   159   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   160   P.xname >> Loose;
   161 
   162 in
   163 
   164 val _ =
   165   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   166     (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   167       >> (Toplevel.no_timing oo find_consts_cmd));
   168 
   169 end;
   170 
   171 end;
   172