src/Pure/Tools/find_consts.ML
author wenzelm
Sun Oct 25 13:18:35 2009 +0100 (2009-10-25)
changeset 33158 6e3dc0ba2b06
parent 32790 a7b92f98180b
child 33301 1fe9fc908ec3
permissions -rw-r--r--
conceal consts via name space, not tags;
     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 user_visible consts (nm, _) =
    91       if Consts.is_concealed consts nm then NONE else SOME low_ranking;
    92 
    93     fun make_pattern crit =
    94       let
    95         val raw_T = Syntax.parse_typ ctxt crit;
    96         val t =
    97           Syntax.check_term
    98             (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    99             (Term.dummy_pattern raw_T);
   100       in Term.type_of t end;
   101 
   102     fun make_match (Strict arg) =
   103           let val qty = make_pattern arg; in
   104             fn (_, (ty, _)) =>
   105               let
   106                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
   107                 val sub_size =
   108                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
   109               in SOME sub_size end handle Type.TYPE_MATCH => NONE
   110           end
   111       | make_match (Loose arg) =
   112           check_const (matches_subtype thy (make_pattern arg) o snd)
   113       | make_match (Name arg) = check_const (match_string arg o fst);
   114 
   115     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   116     val criteria = map make_criterion raw_criteria;
   117 
   118     val consts = Sign.consts_of thy;
   119     val (_, consts_tab) = #constants (Consts.dest consts);
   120     fun eval_entry c =
   121       fold filter_const (user_visible consts :: criteria)
   122         (SOME (c, low_ranking));
   123 
   124     val matches =
   125       Symtab.fold (cons o eval_entry) consts_tab []
   126       |> map_filter I
   127       |> sort (rev_order o int_ord o pairself snd)
   128       |> map (apsnd fst o fst);
   129 
   130     val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   131   in
   132     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   133       :: Pretty.str ""
   134       :: (Pretty.str o implode)
   135            (if null matches
   136             then ["nothing found", end_msg]
   137             else ["found ", (string_of_int o length) matches,
   138                   " constants", end_msg, ":"])
   139       :: Pretty.str ""
   140       :: map (pretty_const ctxt) matches
   141     |> Pretty.chunks
   142     |> Pretty.writeln
   143   end;
   144 
   145 
   146 (* command syntax *)
   147 
   148 fun find_consts_cmd spec =
   149   Toplevel.unknown_theory o Toplevel.keep (fn state =>
   150     find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
   151 
   152 local
   153 
   154 structure P = OuterParse and K = OuterKeyword;
   155 
   156 val criterion =
   157   P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   158   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   159   P.xname >> Loose;
   160 
   161 in
   162 
   163 val _ =
   164   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   165     (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   166       >> (Toplevel.no_timing oo find_consts_cmd));
   167 
   168 end;
   169 
   170 end;
   171