src/Pure/Tools/find_consts.ML
author wenzelm
Sun Jul 10 11:18:35 2016 +0200 (2016-07-10)
changeset 63429 baedd4724f08
parent 62969 9f394a16c557
child 64556 851ae0e7b09c
permissions -rw-r--r--
tuned signature: more uniform Keyword.spec;
wenzelm@30143
     1
(*  Title:      Pure/Tools/find_consts.ML
kleing@29884
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
kleing@29884
     3
wenzelm@30143
     4
Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
wenzelm@30143
     5
type over constants, but matching is not fuzzy.
kleing@29884
     6
*)
kleing@29884
     7
kleing@29884
     8
signature FIND_CONSTS =
kleing@29884
     9
sig
wenzelm@30143
    10
  datatype criterion =
wenzelm@30143
    11
      Strict of string
wenzelm@30143
    12
    | Loose of string
wenzelm@30143
    13
    | Name of string
wenzelm@62848
    14
  val pretty_consts: Proof.context -> (bool * criterion) list -> Pretty.T
wenzelm@62848
    15
  val query_parser: (bool * criterion) list parser
wenzelm@56758
    16
  val read_query: Position.T -> string -> (bool * criterion) list
kleing@29884
    17
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    18
end;
kleing@29884
    19
wenzelm@33301
    20
structure Find_Consts : FIND_CONSTS =
kleing@29884
    21
struct
kleing@29884
    22
wenzelm@30143
    23
(* search criteria *)
wenzelm@30143
    24
wenzelm@30143
    25
datatype criterion =
wenzelm@30143
    26
    Strict of string
wenzelm@30143
    27
  | Loose of string
wenzelm@30143
    28
  | Name of string;
kleing@29884
    29
wenzelm@31684
    30
wenzelm@30143
    31
(* matching types/consts *)
kleing@29884
    32
wenzelm@30143
    33
fun matches_subtype thy typat =
wenzelm@38335
    34
  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
kleing@29884
    35
wenzelm@61335
    36
fun check_const pred (c, (ty, _)) =
wenzelm@61335
    37
  if pred (c, ty) then SOME (Term.size_of_typ ty) else NONE;
kleing@29884
    38
wenzelm@30143
    39
fun opt_not f (c as (_, (ty, _))) =
wenzelm@38335
    40
  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
kleing@29884
    41
wenzelm@46979
    42
fun filter_const _ _ NONE = NONE
wenzelm@46979
    43
  | filter_const c f (SOME rank) =
wenzelm@31684
    44
      (case f c of
wenzelm@31684
    45
        NONE => NONE
wenzelm@46979
    46
      | SOME i => SOME (Int.min (rank, i)));
wenzelm@30143
    47
wenzelm@30143
    48
wenzelm@30143
    49
(* pretty results *)
kleing@29895
    50
kleing@29895
    51
fun pretty_criterion (b, c) =
kleing@29895
    52
  let
kleing@29895
    53
    fun prfx s = if b then s else "-" ^ s;
wenzelm@60667
    54
    val show_pat = quote o Input.source_content o Syntax.read_input;
kleing@29895
    55
  in
kleing@29895
    56
    (case c of
wenzelm@60667
    57
      Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat)
wenzelm@60667
    58
    | Loose pat => Pretty.str (prfx (show_pat pat))
kleing@29895
    59
    | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895
    60
  end;
kleing@29895
    61
wenzelm@49886
    62
fun pretty_const ctxt (c, ty) =
wenzelm@30143
    63
  let
wenzelm@35845
    64
    val ty' = Logic.unvarifyT_global ty;
wenzelm@61335
    65
    val markup = Name_Space.markup (Proof_Context.const_space ctxt) c;
kleing@29895
    66
  in
wenzelm@30143
    67
    Pretty.block
wenzelm@49886
    68
     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
wenzelm@30143
    69
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895
    70
  end;
kleing@29895
    71
wenzelm@31684
    72
wenzelm@30143
    73
(* find_consts *)
wenzelm@30143
    74
wenzelm@56758
    75
fun pretty_consts ctxt raw_criteria =
wenzelm@30143
    76
  let
wenzelm@42360
    77
    val thy = Proof_Context.theory_of ctxt;
kleing@29884
    78
    val low_ranking = 10000;
kleing@29884
    79
Timothy@30207
    80
    fun make_pattern crit =
Timothy@30207
    81
      let
Timothy@30207
    82
        val raw_T = Syntax.parse_typ ctxt crit;
wenzelm@31684
    83
        val t =
wenzelm@31684
    84
          Syntax.check_term
wenzelm@42360
    85
            (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
wenzelm@31684
    86
            (Term.dummy_pattern raw_T);
Timothy@30207
    87
      in Term.type_of t end;
kleing@29884
    88
kleing@29884
    89
    fun make_match (Strict arg) =
kleing@29884
    90
          let val qty = make_pattern arg; in
wenzelm@30143
    91
            fn (_, (ty, _)) =>
wenzelm@30143
    92
              let
kleing@29884
    93
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
wenzelm@31684
    94
                val sub_size =
wenzelm@31684
    95
                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
wenzelm@32790
    96
              in SOME sub_size end handle Type.TYPE_MATCH => NONE
kleing@29884
    97
          end
kleing@29884
    98
      | make_match (Loose arg) =
kleing@29884
    99
          check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884
   100
      | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884
   101
kleing@29884
   102
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
Timothy@30206
   103
    val criteria = map make_criterion raw_criteria;
kleing@29884
   104
wenzelm@61335
   105
    fun user_visible (c, _) =
wenzelm@61335
   106
      if Consts.is_concealed (Proof_Context.consts_of ctxt) c
wenzelm@61335
   107
      then NONE else SOME low_ranking;
wenzelm@61335
   108
wenzelm@31684
   109
    fun eval_entry c =
wenzelm@61335
   110
      fold (filter_const c) (user_visible :: criteria) (SOME low_ranking);
kleing@29884
   111
wenzelm@61335
   112
    val {constants, ...} = Consts.dest (Sign.consts_of thy);
wenzelm@30143
   113
    val matches =
wenzelm@56062
   114
      fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
wenzelm@59058
   115
      |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
wenzelm@46979
   116
      |> map (apsnd fst o snd);
wenzelm@56912
   117
wenzelm@56912
   118
    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
kleing@29884
   119
  in
wenzelm@56891
   120
    Pretty.block
wenzelm@56912
   121
      (Pretty.fbreaks
wenzelm@56912
   122
        (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
wenzelm@56912
   123
          map pretty_criterion raw_criteria)) ::
wenzelm@38335
   124
    Pretty.str "" ::
wenzelm@56908
   125
    (if null matches then [Pretty.str "found nothing"]
wenzelm@56908
   126
     else
wenzelm@56908
   127
       Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") ::
wenzelm@56908
   128
       grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches)
wenzelm@61335
   129
  end |> Pretty.chunks;
wenzelm@56758
   130
wenzelm@56758
   131
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
kleing@29884
   132
wenzelm@30142
   133
wenzelm@30143
   134
(* command syntax *)
wenzelm@30142
   135
wenzelm@38334
   136
local
wenzelm@30142
   137
wenzelm@30142
   138
val criterion =
wenzelm@62969
   139
  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.name) >> Name ||
wenzelm@60664
   140
  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
wenzelm@60664
   141
  Parse.typ >> Loose;
wenzelm@30142
   142
wenzelm@63429
   143
val query_keywords =
wenzelm@63429
   144
  Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
wenzelm@58905
   145
wenzelm@38334
   146
in
wenzelm@38334
   147
wenzelm@62848
   148
val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
wenzelm@62848
   149
wenzelm@56758
   150
fun read_query pos str =
wenzelm@59083
   151
  Token.explode query_keywords pos str
wenzelm@56758
   152
  |> filter Token.is_proper
wenzelm@62848
   153
  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
wenzelm@56758
   154
  |> #1;
wenzelm@56758
   155
kleing@29884
   156
end;
kleing@29884
   157
wenzelm@56758
   158
wenzelm@56758
   159
(* PIDE query operation *)
wenzelm@56758
   160
wenzelm@56758
   161
val _ =
wenzelm@60610
   162
  Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
wenzelm@61223
   163
    (fn {state, args, writeln_result, ...} =>
wenzelm@60610
   164
      (case try Toplevel.context_of state of
wenzelm@60610
   165
        SOME ctxt =>
wenzelm@60610
   166
          let
wenzelm@60610
   167
            val [query_arg] = args;
wenzelm@60610
   168
            val query = read_query Position.none query_arg;
wenzelm@61223
   169
          in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end
wenzelm@60610
   170
      | NONE => error "Unknown context"));
wenzelm@56758
   171
wenzelm@38334
   172
end;