src/Pure/Tools/find_consts.ML
author wenzelm
Mon Jul 06 16:10:00 2015 +0200 (2015-07-06)
changeset 60667 d86c449d30ba
parent 60664 263a8f15faf3
child 61223 dfccf6c06201
permissions -rw-r--r--
plain string output, without funny control chars;
     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   val read_query: Position.T -> string -> (bool * criterion) list
    15   val find_consts : Proof.context -> (bool * criterion) list -> unit
    16 end;
    17 
    18 structure Find_Consts : 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   Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
    33 
    34 fun check_const pred (nm, (ty, _)) =
    35   if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
    36 
    37 fun opt_not f (c as (_, (ty, _))) =
    38   if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
    39 
    40 fun filter_const _ _ NONE = NONE
    41   | filter_const c f (SOME rank) =
    42       (case f c of
    43         NONE => NONE
    44       | SOME i => SOME (Int.min (rank, i)));
    45 
    46 
    47 (* pretty results *)
    48 
    49 fun pretty_criterion (b, c) =
    50   let
    51     fun prfx s = if b then s else "-" ^ s;
    52     val show_pat = quote o Input.source_content o Syntax.read_input;
    53   in
    54     (case c of
    55       Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat)
    56     | Loose pat => Pretty.str (prfx (show_pat pat))
    57     | Name name => Pretty.str (prfx "name: " ^ quote name))
    58   end;
    59 
    60 fun pretty_const ctxt (c, ty) =
    61   let
    62     val ty' = Logic.unvarifyT_global ty;
    63     val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
    64     val markup = Name_Space.markup const_space c;
    65   in
    66     Pretty.block
    67      [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
    68       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    69   end;
    70 
    71 
    72 (* find_consts *)
    73 
    74 fun pretty_consts ctxt raw_criteria =
    75   let
    76     val thy = Proof_Context.theory_of ctxt;
    77     val low_ranking = 10000;
    78 
    79     fun user_visible consts (nm, _) =
    80       if Consts.is_concealed consts nm then NONE else SOME low_ranking;
    81 
    82     fun make_pattern crit =
    83       let
    84         val raw_T = Syntax.parse_typ ctxt crit;
    85         val t =
    86           Syntax.check_term
    87             (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    88             (Term.dummy_pattern raw_T);
    89       in Term.type_of t end;
    90 
    91     fun make_match (Strict arg) =
    92           let val qty = make_pattern arg; in
    93             fn (_, (ty, _)) =>
    94               let
    95                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    96                 val sub_size =
    97                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
    98               in SOME sub_size end handle Type.TYPE_MATCH => NONE
    99           end
   100       | make_match (Loose arg) =
   101           check_const (matches_subtype thy (make_pattern arg) o snd)
   102       | make_match (Name arg) = check_const (match_string arg o fst);
   103 
   104     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   105     val criteria = map make_criterion raw_criteria;
   106 
   107     val consts = Sign.consts_of thy;
   108     val {constants, ...} = Consts.dest consts;
   109     fun eval_entry c =
   110       fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
   111 
   112     val matches =
   113       fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
   114       |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
   115       |> map (apsnd fst o snd);
   116 
   117     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   118   in
   119     Pretty.block
   120       (Pretty.fbreaks
   121         (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
   122           map pretty_criterion raw_criteria)) ::
   123     Pretty.str "" ::
   124     (if null matches then [Pretty.str "found nothing"]
   125      else
   126        Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
   127        grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
   128   end |> Pretty.fbreaks |> curry Pretty.blk 0;
   129 
   130 fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
   131 
   132 
   133 (* command syntax *)
   134 
   135 local
   136 
   137 val criterion =
   138   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   139   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
   140   Parse.typ >> Loose;
   141 
   142 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   143 
   144 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
   145 
   146 in
   147 
   148 fun read_query pos str =
   149   Token.explode query_keywords pos str
   150   |> filter Token.is_proper
   151   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   152   |> #1;
   153 
   154 val _ =
   155   Outer_Syntax.command @{command_keyword find_consts}
   156     "find constants by name / type patterns"
   157     (query >> (fn spec =>
   158       Toplevel.keep (fn st =>
   159         Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
   160 
   161 end;
   162 
   163 
   164 (* PIDE query operation *)
   165 
   166 val _ =
   167   Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
   168     (fn {state, args, output_result} =>
   169       (case try Toplevel.context_of state of
   170         SOME ctxt =>
   171           let
   172             val [query_arg] = args;
   173             val query = read_query Position.none query_arg;
   174           in output_result (Pretty.string_of (pretty_consts ctxt query)) end
   175       | NONE => error "Unknown context"));
   176 
   177 end;
   178