src/Pure/Tools/find_consts.ML
author wenzelm
Wed Aug 11 18:10:39 2010 +0200 (2010-08-11)
changeset 38336 fd53ae1d4c47
parent 38335 630f379f2660
child 42012 2c3fe3cbebae
permissions -rw-r--r--
standardized pretty printing of consts (e.g. see find_theorems, print_theory);
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
kleing@29884
    14
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    15
end;
kleing@29884
    16
wenzelm@33301
    17
structure Find_Consts : FIND_CONSTS =
kleing@29884
    18
struct
kleing@29884
    19
wenzelm@30143
    20
(* search criteria *)
wenzelm@30143
    21
wenzelm@30143
    22
datatype criterion =
wenzelm@30143
    23
    Strict of string
wenzelm@30143
    24
  | Loose of string
wenzelm@30143
    25
  | Name of string;
kleing@29884
    26
wenzelm@31684
    27
wenzelm@30143
    28
(* matching types/consts *)
kleing@29884
    29
wenzelm@30143
    30
fun matches_subtype thy typat =
wenzelm@38335
    31
  Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
kleing@29884
    32
wenzelm@38335
    33
fun check_const pred (nm, (ty, _)) =
wenzelm@38335
    34
  if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
kleing@29884
    35
wenzelm@30143
    36
fun opt_not f (c as (_, (ty, _))) =
wenzelm@38335
    37
  if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
kleing@29884
    38
Timothy@30206
    39
fun filter_const _ NONE = NONE
Timothy@30206
    40
  | filter_const f (SOME (c, r)) =
wenzelm@31684
    41
      (case f c of
wenzelm@31684
    42
        NONE => NONE
wenzelm@31684
    43
      | SOME i => SOME (c, Int.min (r, i)));
wenzelm@30143
    44
wenzelm@30143
    45
wenzelm@30143
    46
(* pretty results *)
kleing@29895
    47
kleing@29895
    48
fun pretty_criterion (b, c) =
kleing@29895
    49
  let
kleing@29895
    50
    fun prfx s = if b then s else "-" ^ s;
kleing@29895
    51
  in
kleing@29895
    52
    (case c of
kleing@29895
    53
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
kleing@29895
    54
    | Loose pat => Pretty.str (prfx (quote pat))
kleing@29895
    55
    | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895
    56
  end;
kleing@29895
    57
wenzelm@30143
    58
fun pretty_const ctxt (nm, ty) =
wenzelm@30143
    59
  let
wenzelm@35845
    60
    val ty' = Logic.unvarifyT_global ty;
kleing@29895
    61
  in
wenzelm@30143
    62
    Pretty.block
wenzelm@38336
    63
     [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
wenzelm@30143
    64
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895
    65
  end;
kleing@29895
    66
wenzelm@31684
    67
wenzelm@30143
    68
(* find_consts *)
wenzelm@30143
    69
wenzelm@30143
    70
fun find_consts ctxt raw_criteria =
wenzelm@30143
    71
  let
kleing@29895
    72
    val start = start_timing ();
kleing@29895
    73
kleing@29884
    74
    val thy = ProofContext.theory_of ctxt;
kleing@29884
    75
    val low_ranking = 10000;
kleing@29884
    76
wenzelm@33158
    77
    fun user_visible consts (nm, _) =
wenzelm@33158
    78
      if Consts.is_concealed consts nm then NONE else SOME low_ranking;
Timothy@30206
    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@31684
    85
            (ProofContext.set_mode ProofContext.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
Timothy@30206
   105
    val consts = Sign.consts_of thy;
wenzelm@31684
   106
    val (_, consts_tab) = #constants (Consts.dest consts);
wenzelm@31684
   107
    fun eval_entry c =
wenzelm@33158
   108
      fold filter_const (user_visible consts :: criteria)
wenzelm@31684
   109
        (SOME (c, low_ranking));
kleing@29884
   110
wenzelm@30143
   111
    val matches =
Timothy@30206
   112
      Symtab.fold (cons o eval_entry) consts_tab []
wenzelm@30143
   113
      |> map_filter I
wenzelm@30143
   114
      |> sort (rev_order o int_ord o pairself snd)
wenzelm@31684
   115
      |> map (apsnd fst o fst);
kleing@29895
   116
wenzelm@31687
   117
    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
kleing@29884
   118
  in
wenzelm@38335
   119
    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
wenzelm@38335
   120
    Pretty.str "" ::
wenzelm@38335
   121
    Pretty.str
wenzelm@38335
   122
     (if null matches
wenzelm@38335
   123
      then "nothing found" ^ end_msg
wenzelm@38335
   124
      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
wenzelm@38335
   125
    Pretty.str "" ::
wenzelm@38335
   126
    map (pretty_const ctxt) matches
wenzelm@38335
   127
  end |> Pretty.chunks |> Pretty.writeln;
kleing@29884
   128
wenzelm@30142
   129
wenzelm@30143
   130
(* command syntax *)
wenzelm@30142
   131
wenzelm@38334
   132
local
wenzelm@30142
   133
wenzelm@30142
   134
val criterion =
wenzelm@36950
   135
  Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
wenzelm@36950
   136
  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
wenzelm@36950
   137
  Parse.xname >> Loose;
wenzelm@30142
   138
wenzelm@38334
   139
in
wenzelm@38334
   140
wenzelm@30142
   141
val _ =
wenzelm@36953
   142
  Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
wenzelm@36950
   143
    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
wenzelm@38334
   144
      >> (fn spec => Toplevel.no_timing o
wenzelm@38334
   145
        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
wenzelm@30142
   146
kleing@29884
   147
end;
kleing@29884
   148
wenzelm@38334
   149
end;
wenzelm@38334
   150