src/Pure/Tools/find_consts.ML
author wenzelm
Wed Jun 17 15:14:48 2009 +0200 (2009-06-17)
changeset 31684 d5d830979a54
parent 30207 c56d27155041
child 31687 0d2f700fe5e7
permissions -rw-r--r--
minor tuning according to Isabelle/ML conventions;
slightly less combinators;
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
kleing@29884
    15
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    16
end;
kleing@29884
    17
kleing@29884
    18
structure FindConsts : 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@30143
    32
  let
kleing@29884
    33
    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
kleing@29884
    34
kleing@29884
    35
    fun fs [] = false
wenzelm@30143
    36
      | fs (t :: ts) = f t orelse fs ts
kleing@29884
    37
kleing@29884
    38
    and f (t as Type (_, ars)) = p t orelse fs ars
kleing@29884
    39
      | f t = p t;
kleing@29884
    40
  in f end;
kleing@29884
    41
wenzelm@30143
    42
fun check_const p (nm, (ty, _)) =
wenzelm@30143
    43
  if p (nm, ty)
wenzelm@30143
    44
  then SOME (Term.size_of_typ ty)
wenzelm@30143
    45
  else NONE;
kleing@29884
    46
wenzelm@30143
    47
fun opt_not f (c as (_, (ty, _))) =
wenzelm@30143
    48
  if is_some (f c)
wenzelm@30143
    49
  then NONE else SOME (Term.size_of_typ ty);
kleing@29884
    50
Timothy@30206
    51
fun filter_const _ NONE = NONE
Timothy@30206
    52
  | filter_const f (SOME (c, r)) =
wenzelm@31684
    53
      (case f c of
wenzelm@31684
    54
        NONE => NONE
wenzelm@31684
    55
      | SOME i => SOME (c, Int.min (r, i)));
wenzelm@30143
    56
wenzelm@30143
    57
wenzelm@30143
    58
(* pretty results *)
kleing@29895
    59
kleing@29895
    60
fun pretty_criterion (b, c) =
kleing@29895
    61
  let
kleing@29895
    62
    fun prfx s = if b then s else "-" ^ s;
kleing@29895
    63
  in
kleing@29895
    64
    (case c of
kleing@29895
    65
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
kleing@29895
    66
    | Loose pat => Pretty.str (prfx (quote pat))
kleing@29895
    67
    | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895
    68
  end;
kleing@29895
    69
wenzelm@30143
    70
fun pretty_const ctxt (nm, ty) =
wenzelm@30143
    71
  let
kleing@29895
    72
    val ty' = Logic.unvarifyT ty;
kleing@29895
    73
  in
wenzelm@30143
    74
    Pretty.block
wenzelm@30143
    75
     [Pretty.quote (Pretty.str nm), Pretty.fbrk,
wenzelm@30143
    76
      Pretty.str "::", Pretty.brk 1,
wenzelm@30143
    77
      Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895
    78
  end;
kleing@29895
    79
wenzelm@31684
    80
wenzelm@30143
    81
(* find_consts *)
wenzelm@30143
    82
wenzelm@30143
    83
fun find_consts ctxt raw_criteria =
wenzelm@30143
    84
  let
kleing@29895
    85
    val start = start_timing ();
kleing@29895
    86
kleing@29884
    87
    val thy = ProofContext.theory_of ctxt;
kleing@29884
    88
    val low_ranking = 10000;
kleing@29884
    89
wenzelm@31684
    90
    fun not_internal consts (nm, _) =
Timothy@30206
    91
      if member (op =) (Consts.the_tags consts nm) Markup.property_internal
Timothy@30206
    92
      then NONE else SOME low_ranking;
Timothy@30206
    93
Timothy@30207
    94
    fun make_pattern crit =
Timothy@30207
    95
      let
Timothy@30207
    96
        val raw_T = Syntax.parse_typ ctxt crit;
wenzelm@31684
    97
        val t =
wenzelm@31684
    98
          Syntax.check_term
wenzelm@31684
    99
            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
wenzelm@31684
   100
            (Term.dummy_pattern raw_T);
Timothy@30207
   101
      in Term.type_of t end;
kleing@29884
   102
kleing@29884
   103
    fun make_match (Strict arg) =
kleing@29884
   104
          let val qty = make_pattern arg; in
wenzelm@30143
   105
            fn (_, (ty, _)) =>
wenzelm@30143
   106
              let
kleing@29884
   107
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
wenzelm@31684
   108
                val sub_size =
wenzelm@31684
   109
                  Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
kleing@29884
   110
              in SOME sub_size end handle MATCH => NONE
kleing@29884
   111
          end
kleing@29884
   112
      | make_match (Loose arg) =
kleing@29884
   113
          check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884
   114
      | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884
   115
kleing@29884
   116
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
Timothy@30206
   117
    val criteria = map make_criterion raw_criteria;
kleing@29884
   118
Timothy@30206
   119
    val consts = Sign.consts_of thy;
wenzelm@31684
   120
    val (_, consts_tab) = #constants (Consts.dest consts);
wenzelm@31684
   121
    fun eval_entry c =
wenzelm@31684
   122
      fold filter_const (not_internal consts :: criteria)
wenzelm@31684
   123
        (SOME (c, low_ranking));
kleing@29884
   124
wenzelm@30143
   125
    val matches =
Timothy@30206
   126
      Symtab.fold (cons o eval_entry) consts_tab []
wenzelm@30143
   127
      |> map_filter I
wenzelm@30143
   128
      |> sort (rev_order o int_ord o pairself snd)
wenzelm@31684
   129
      |> map (apsnd fst o fst);
kleing@29895
   130
wenzelm@30188
   131
    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
kleing@29884
   132
  in
kleing@29895
   133
    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
kleing@29895
   134
      :: Pretty.str ""
wenzelm@31684
   135
      :: (Pretty.str o implode)
kleing@29895
   136
           (if null matches
kleing@29895
   137
            then ["nothing found", end_msg]
kleing@29895
   138
            else ["found ", (string_of_int o length) matches,
kleing@29895
   139
                  " constants", end_msg, ":"])
kleing@29895
   140
      :: Pretty.str ""
kleing@29895
   141
      :: map (pretty_const ctxt) matches
kleing@29895
   142
    |> Pretty.chunks
kleing@29884
   143
    |> Pretty.writeln
Timothy@30206
   144
  end;
kleing@29884
   145
wenzelm@30142
   146
wenzelm@30143
   147
(* command syntax *)
wenzelm@30142
   148
wenzelm@30142
   149
fun find_consts_cmd spec =
wenzelm@30142
   150
  Toplevel.unknown_theory o Toplevel.keep (fn state =>
wenzelm@30142
   151
    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
wenzelm@30142
   152
wenzelm@30142
   153
local
wenzelm@30142
   154
wenzelm@30142
   155
structure P = OuterParse and K = OuterKeyword;
wenzelm@30142
   156
wenzelm@30142
   157
val criterion =
wenzelm@30142
   158
  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
wenzelm@30142
   159
  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
wenzelm@30142
   160
  P.xname >> Loose;
wenzelm@30142
   161
wenzelm@30142
   162
in
wenzelm@30142
   163
wenzelm@30142
   164
val _ =
wenzelm@30142
   165
  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
wenzelm@30142
   166
    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
wenzelm@30142
   167
      >> (Toplevel.no_timing oo find_consts_cmd));
wenzelm@30142
   168
kleing@29884
   169
end;
kleing@29884
   170
wenzelm@30142
   171
end;
wenzelm@30142
   172