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