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