src/Pure/Tools/find_consts.ML
author wenzelm
Sun Apr 27 13:35:18 2014 +0200 (2014-04-27)
changeset 56763 70371621fdb6
parent 56760 ef5df088e022
child 56891 48899c43b07d
permissions -rw-r--r--
tuned;
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@56758
    14
  val read_query: Position.T -> string -> (bool * criterion) list
kleing@29884
    15
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    16
end;
kleing@29884
    17
wenzelm@33301
    18
structure Find_Consts : FIND_CONSTS =
kleing@29884
    19
struct
kleing@29884
    20
wenzelm@30143
    21
(* search criteria *)
wenzelm@30143
    22
wenzelm@30143
    23
datatype criterion =
wenzelm@30143
    24
    Strict of string
wenzelm@30143
    25
  | Loose of string
wenzelm@30143
    26
  | Name of string;
kleing@29884
    27
wenzelm@31684
    28
wenzelm@30143
    29
(* matching types/consts *)
kleing@29884
    30
wenzelm@30143
    31
fun matches_subtype thy typat =
wenzelm@38335
    32
  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
kleing@29884
    33
wenzelm@38335
    34
fun check_const pred (nm, (ty, _)) =
wenzelm@38335
    35
  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
kleing@29884
    36
wenzelm@30143
    37
fun opt_not f (c as (_, (ty, _))) =
wenzelm@38335
    38
  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
kleing@29884
    39
wenzelm@46979
    40
fun filter_const _ _ NONE = NONE
wenzelm@46979
    41
  | filter_const c f (SOME rank) =
wenzelm@31684
    42
      (case f c of
wenzelm@31684
    43
        NONE => NONE
wenzelm@46979
    44
      | SOME i => SOME (Int.min (rank, i)));
wenzelm@30143
    45
wenzelm@30143
    46
wenzelm@30143
    47
(* pretty results *)
kleing@29895
    48
kleing@29895
    49
fun pretty_criterion (b, c) =
kleing@29895
    50
  let
kleing@29895
    51
    fun prfx s = if b then s else "-" ^ s;
kleing@29895
    52
  in
kleing@29895
    53
    (case c of
kleing@29895
    54
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
kleing@29895
    55
    | Loose pat => Pretty.str (prfx (quote pat))
kleing@29895
    56
    | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895
    57
  end;
kleing@29895
    58
wenzelm@49886
    59
fun pretty_const ctxt (c, ty) =
wenzelm@30143
    60
  let
wenzelm@35845
    61
    val ty' = Logic.unvarifyT_global ty;
wenzelm@56025
    62
    val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
wenzelm@56025
    63
    val markup = Name_Space.markup const_space c;
kleing@29895
    64
  in
wenzelm@30143
    65
    Pretty.block
wenzelm@49886
    66
     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
wenzelm@30143
    67
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895
    68
  end;
kleing@29895
    69
wenzelm@31684
    70
wenzelm@30143
    71
(* find_consts *)
wenzelm@30143
    72
wenzelm@56758
    73
fun pretty_consts ctxt raw_criteria =
wenzelm@30143
    74
  let
wenzelm@42360
    75
    val thy = Proof_Context.theory_of ctxt;
kleing@29884
    76
    val low_ranking = 10000;
kleing@29884
    77
wenzelm@33158
    78
    fun user_visible consts (nm, _) =
wenzelm@33158
    79
      if Consts.is_concealed consts nm then NONE else SOME low_ranking;
Timothy@30206
    80
Timothy@30207
    81
    fun make_pattern crit =
Timothy@30207
    82
      let
Timothy@30207
    83
        val raw_T = Syntax.parse_typ ctxt crit;
wenzelm@31684
    84
        val t =
wenzelm@31684
    85
          Syntax.check_term
wenzelm@42360
    86
            (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
wenzelm@31684
    87
            (Term.dummy_pattern raw_T);
Timothy@30207
    88
      in Term.type_of t end;
kleing@29884
    89
kleing@29884
    90
    fun make_match (Strict arg) =
kleing@29884
    91
          let val qty = make_pattern arg; in
wenzelm@30143
    92
            fn (_, (ty, _)) =>
wenzelm@30143
    93
              let
kleing@29884
    94
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
wenzelm@31684
    95
                val sub_size =
wenzelm@31684
    96
                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
wenzelm@32790
    97
              in SOME sub_size end handle Type.TYPE_MATCH => NONE
kleing@29884
    98
          end
kleing@29884
    99
      | make_match (Loose arg) =
kleing@29884
   100
          check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884
   101
      | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884
   102
kleing@29884
   103
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
Timothy@30206
   104
    val criteria = map make_criterion raw_criteria;
kleing@29884
   105
Timothy@30206
   106
    val consts = Sign.consts_of thy;
wenzelm@56025
   107
    val {constants, ...} = Consts.dest consts;
wenzelm@31684
   108
    fun eval_entry c =
wenzelm@46979
   109
      fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
kleing@29884
   110
wenzelm@30143
   111
    val matches =
wenzelm@56062
   112
      fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
wenzelm@46979
   113
      |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
wenzelm@46979
   114
      |> map (apsnd fst o snd);
kleing@29884
   115
  in
wenzelm@38335
   116
    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
wenzelm@38335
   117
    Pretty.str "" ::
wenzelm@38335
   118
    Pretty.str
wenzelm@38335
   119
     (if null matches
wenzelm@46716
   120
      then "nothing found"
wenzelm@46716
   121
      else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
wenzelm@38335
   122
    Pretty.str "" ::
wenzelm@56763
   123
    grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches
wenzelm@56758
   124
  end |> Pretty.fbreaks |> curry Pretty.blk 0;
wenzelm@56758
   125
wenzelm@56758
   126
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
kleing@29884
   127
wenzelm@30142
   128
wenzelm@30143
   129
(* command syntax *)
wenzelm@30142
   130
wenzelm@38334
   131
local
wenzelm@30142
   132
wenzelm@30142
   133
val criterion =
wenzelm@36950
   134
  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
wenzelm@36950
   135
  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
wenzelm@36950
   136
  Parse.xname >> Loose;
wenzelm@30142
   137
wenzelm@56758
   138
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
wenzelm@56758
   139
wenzelm@38334
   140
in
wenzelm@38334
   141
wenzelm@56758
   142
fun read_query pos str =
wenzelm@56758
   143
  Outer_Syntax.scan pos str
wenzelm@56758
   144
  |> filter Token.is_proper
wenzelm@56758
   145
  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
wenzelm@56758
   146
  |> #1;
wenzelm@56758
   147
wenzelm@30142
   148
val _ =
wenzelm@50214
   149
  Outer_Syntax.improper_command @{command_spec "find_consts"}
wenzelm@56758
   150
    "find constants by name / type patterns"
wenzelm@56758
   151
    (query >> (fn spec =>
wenzelm@56758
   152
      Toplevel.keep (fn st =>
wenzelm@56758
   153
        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
wenzelm@30142
   154
kleing@29884
   155
end;
kleing@29884
   156
wenzelm@56758
   157
wenzelm@56758
   158
(* PIDE query operation *)
wenzelm@56758
   159
wenzelm@56758
   160
val _ =
wenzelm@56758
   161
  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
wenzelm@56758
   162
    (case try Toplevel.context_of state of
wenzelm@56758
   163
      SOME ctxt =>
wenzelm@56758
   164
        let
wenzelm@56758
   165
          val [query_arg] = args;
wenzelm@56758
   166
          val query = read_query Position.none query_arg;
wenzelm@56758
   167
        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
wenzelm@56758
   168
    | NONE => error "Unknown context"));
wenzelm@56758
   169
wenzelm@38334
   170
end;
wenzelm@38334
   171