src/Pure/Tools/find_consts.ML
author wenzelm
Fri Feb 27 15:46:22 2009 +0100 (2009-02-27)
changeset 30142 8d6145694bb5
parent 29895 src/Pure/Isar/find_consts.ML@0e70a29d3e02
child 30143 98a986b02022
permissions -rw-r--r--
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
kleing@29884
     1
(*  Title:      find_consts.ML
kleing@29884
     2
    Author:     Timothy Bourke and Gerwin Klein, NICTA
kleing@29884
     3
kleing@29884
     4
  Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type
kleing@29884
     5
  over constants, but matching is not fuzzy
kleing@29884
     6
*)
kleing@29884
     7
kleing@29884
     8
signature FIND_CONSTS =
kleing@29884
     9
sig
kleing@29884
    10
  datatype criterion = Strict of string
kleing@29884
    11
                     | Loose of string
kleing@29884
    12
                     | Name of string
kleing@29884
    13
kleing@29884
    14
  val default_criteria : (bool * criterion) list ref
kleing@29884
    15
kleing@29884
    16
  val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884
    17
end;
kleing@29884
    18
kleing@29884
    19
structure FindConsts : FIND_CONSTS =
kleing@29884
    20
struct
kleing@29884
    21
kleing@29884
    22
datatype criterion = Strict of string
kleing@29884
    23
                   | Loose of string
kleing@29884
    24
                   | Name of string;
kleing@29884
    25
kleing@29884
    26
val default_criteria = ref [(false, Name ".sko_")];
kleing@29884
    27
kleing@29884
    28
fun add_tye (_, (_, t)) n = size_of_typ t + n;
kleing@29884
    29
kleing@29884
    30
fun matches_subtype thy typat = let
kleing@29884
    31
    val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
kleing@29884
    32
kleing@29884
    33
    fun fs [] = false
kleing@29884
    34
      | fs (t::ts) = f t orelse fs ts
kleing@29884
    35
kleing@29884
    36
    and f (t as Type (_, ars)) = p t orelse fs ars
kleing@29884
    37
      | f t = p t;
kleing@29884
    38
  in f end;
kleing@29884
    39
kleing@29884
    40
fun check_const p (nm, (ty, _)) = if p (nm, ty)
kleing@29884
    41
                                  then SOME (size_of_typ ty)
kleing@29884
    42
                                  else NONE;
kleing@29884
    43
kleing@29884
    44
fun opt_not f (c as (_, (ty, _))) = if is_some (f c)
kleing@29884
    45
                                    then NONE else SOME (size_of_typ ty);
kleing@29884
    46
kleing@29895
    47
fun filter_const (_, NONE) = NONE
kleing@29895
    48
  | filter_const (f, (SOME (c, r))) = Option.map
kleing@29895
    49
                                        (pair c o ((curry Int.min) r)) (f c);
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;
kleing@29895
    54
  in
kleing@29895
    55
    (case c of
kleing@29895
    56
      Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
kleing@29895
    57
    | Loose pat => Pretty.str (prfx (quote pat))
kleing@29895
    58
    | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895
    59
  end;
kleing@29895
    60
kleing@29895
    61
fun pretty_const ctxt (nm, ty) = let
kleing@29895
    62
    val ty' = Logic.unvarifyT ty;
kleing@29895
    63
  in
kleing@29895
    64
    Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk,
kleing@29895
    65
                  Pretty.str "::", Pretty.brk 1,
kleing@29895
    66
                  Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895
    67
  end;
kleing@29895
    68
kleing@29884
    69
fun find_consts ctxt raw_criteria = let
kleing@29895
    70
    val start = start_timing ();
kleing@29895
    71
kleing@29884
    72
    val thy = ProofContext.theory_of ctxt;
kleing@29884
    73
    val low_ranking = 10000;
kleing@29884
    74
kleing@29884
    75
    fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit)
kleing@29884
    76
                            |> type_of;
kleing@29884
    77
kleing@29884
    78
    fun make_match (Strict arg) =
kleing@29884
    79
          let val qty = make_pattern arg; in
kleing@29884
    80
            fn (_, (ty, _)) => let
kleing@29884
    81
                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
kleing@29884
    82
                val sub_size = Vartab.fold add_tye tye 0;
kleing@29884
    83
              in SOME sub_size end handle MATCH => NONE
kleing@29884
    84
          end
kleing@29884
    85
kleing@29884
    86
      | make_match (Loose arg) =
kleing@29884
    87
          check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884
    88
      
kleing@29884
    89
      | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884
    90
kleing@29884
    91
    fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
kleing@29884
    92
    val criteria = map make_criterion ((!default_criteria) @ raw_criteria);
kleing@29884
    93
kleing@29884
    94
    val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
kleing@29884
    95
    fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
kleing@29884
    96
kleing@29895
    97
    val matches = Symtab.fold (cons o eval_entry) consts []
kleing@29895
    98
                  |> map_filter I
kleing@29895
    99
                  |> sort (rev_order o int_ord o pairself snd)
kleing@29895
   100
                  |> map ((apsnd fst) o fst);
kleing@29895
   101
kleing@29895
   102
    val end_msg = " in " ^
kleing@29895
   103
                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
kleing@29895
   104
                  ^ " secs"
kleing@29884
   105
  in
kleing@29895
   106
    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
kleing@29895
   107
      :: Pretty.str ""
kleing@29895
   108
      :: (Pretty.str o concat)
kleing@29895
   109
           (if null matches
kleing@29895
   110
            then ["nothing found", end_msg]
kleing@29895
   111
            else ["found ", (string_of_int o length) matches,
kleing@29895
   112
                  " constants", end_msg, ":"])
kleing@29895
   113
      :: Pretty.str ""
kleing@29895
   114
      :: map (pretty_const ctxt) matches
kleing@29895
   115
    |> Pretty.chunks
kleing@29884
   116
    |> Pretty.writeln
kleing@29884
   117
  end handle ERROR s => Output.error_msg s
kleing@29884
   118
wenzelm@30142
   119
wenzelm@30142
   120
wenzelm@30142
   121
(** command syntax **)
wenzelm@30142
   122
wenzelm@30142
   123
fun find_consts_cmd spec =
wenzelm@30142
   124
  Toplevel.unknown_theory o Toplevel.keep (fn state =>
wenzelm@30142
   125
    find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
wenzelm@30142
   126
wenzelm@30142
   127
local
wenzelm@30142
   128
wenzelm@30142
   129
structure P = OuterParse and K = OuterKeyword;
wenzelm@30142
   130
wenzelm@30142
   131
val criterion =
wenzelm@30142
   132
  P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
wenzelm@30142
   133
  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
wenzelm@30142
   134
  P.xname >> Loose;
wenzelm@30142
   135
wenzelm@30142
   136
in
wenzelm@30142
   137
wenzelm@30142
   138
val _ =
wenzelm@30142
   139
  OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
wenzelm@30142
   140
    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
wenzelm@30142
   141
      >> (Toplevel.no_timing oo find_consts_cmd));
wenzelm@30142
   142
kleing@29884
   143
end;
kleing@29884
   144
wenzelm@30142
   145
end;
wenzelm@30142
   146