src/Pure/Tools/find_consts.ML
author wenzelm
Thu Oct 29 11:56:02 2009 +0100 (2009-10-29)
changeset 33301 1fe9fc908ec3
parent 33158 6e3dc0ba2b06
child 35845 e5980f0ad025
permissions -rw-r--r--
less hermetic ML;
parse_pattern: apply Consts.intern only once (Why is this done anyway?);
modernized structure names;
     1 (*  Title:      Pure/Tools/find_consts.ML
     2     Author:     Timothy Bourke and Gerwin Klein, NICTA
     3 
     4 Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
     5 type over constants, but matching is not fuzzy.
     6 *)
     7 
     8 signature FIND_CONSTS =
     9 sig
    10   datatype criterion =
    11       Strict of string
    12     | Loose of string
    13     | Name of string
    14   val find_consts : Proof.context -> (bool * criterion) list -> unit
    15 end;
    16 
    17 structure Find_Consts : FIND_CONSTS =
    18 struct
    19 
    20 (* search criteria *)
    21 
    22 datatype criterion =
    23     Strict of string
    24   | Loose of string
    25   | Name of string;
    26 
    27 
    28 (* matching types/consts *)
    29 
    30 fun matches_subtype thy typat =
    31   let
    32     val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
    33 
    34     fun fs [] = false
    35       | fs (t :: ts) = f t orelse fs ts
    36 
    37     and f (t as Type (_, ars)) = p t orelse fs ars
    38       | f t = p t;
    39   in f end;
    40 
    41 fun check_const p (nm, (ty, _)) =
    42   if p (nm, ty)
    43   then SOME (Term.size_of_typ ty)
    44   else NONE;
    45 
    46 fun opt_not f (c as (_, (ty, _))) =
    47   if is_some (f c)
    48   then NONE else SOME (Term.size_of_typ ty);
    49 
    50 fun filter_const _ NONE = NONE
    51   | filter_const f (SOME (c, r)) =
    52       (case f c of
    53         NONE => NONE
    54       | SOME i => SOME (c, Int.min (r, i)));
    55 
    56 
    57 (* pretty results *)
    58 
    59 fun pretty_criterion (b, c) =
    60   let
    61     fun prfx s = if b then s else "-" ^ s;
    62   in
    63     (case c of
    64       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    65     | Loose pat => Pretty.str (prfx (quote pat))
    66     | Name name => Pretty.str (prfx "name: " ^ quote name))
    67   end;
    68 
    69 fun pretty_const ctxt (nm, ty) =
    70   let
    71     val ty' = Logic.unvarifyT ty;
    72   in
    73     Pretty.block
    74      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
    75       Pretty.str "::", Pretty.brk 1,
    76       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    77   end;
    78 
    79 
    80 (* find_consts *)
    81 
    82 fun find_consts ctxt raw_criteria =
    83   let
    84     val start = start_timing ();
    85 
    86     val thy = ProofContext.theory_of ctxt;
    87     val low_ranking = 10000;
    88 
    89     fun user_visible consts (nm, _) =
    90       if Consts.is_concealed consts nm then NONE else SOME low_ranking;
    91 
    92     fun make_pattern crit =
    93       let
    94         val raw_T = Syntax.parse_typ ctxt crit;
    95         val t =
    96           Syntax.check_term
    97             (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    98             (Term.dummy_pattern raw_T);
    99       in Term.type_of t end;
   100 
   101     fun make_match (Strict arg) =
   102           let val qty = make_pattern arg; in
   103             fn (_, (ty, _)) =>
   104               let
   105                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
   106                 val sub_size =
   107                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
   108               in SOME sub_size end handle Type.TYPE_MATCH => NONE
   109           end
   110       | make_match (Loose arg) =
   111           check_const (matches_subtype thy (make_pattern arg) o snd)
   112       | make_match (Name arg) = check_const (match_string arg o fst);
   113 
   114     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   115     val criteria = map make_criterion raw_criteria;
   116 
   117     val consts = Sign.consts_of thy;
   118     val (_, consts_tab) = #constants (Consts.dest consts);
   119     fun eval_entry c =
   120       fold filter_const (user_visible consts :: criteria)
   121         (SOME (c, low_ranking));
   122 
   123     val matches =
   124       Symtab.fold (cons o eval_entry) consts_tab []
   125       |> map_filter I
   126       |> sort (rev_order o int_ord o pairself snd)
   127       |> map (apsnd fst o fst);
   128 
   129     val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   130   in
   131     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
   132       :: Pretty.str ""
   133       :: (Pretty.str o implode)
   134            (if null matches
   135             then ["nothing found", end_msg]
   136             else ["found ", (string_of_int o length) matches,
   137                   " constants", end_msg, ":"])
   138       :: Pretty.str ""
   139       :: map (pretty_const ctxt) matches
   140     |> Pretty.chunks
   141     |> Pretty.writeln
   142   end;
   143 
   144 
   145 (* command syntax *)
   146 
   147 fun find_consts_cmd spec =
   148   Toplevel.unknown_theory o Toplevel.keep (fn state =>
   149     find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
   150 
   151 local
   152 
   153 structure P = OuterParse and K = OuterKeyword;
   154 
   155 val criterion =
   156   P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
   157   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
   158   P.xname >> Loose;
   159 
   160 in
   161 
   162 val _ =
   163   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
   164     (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
   165       >> (Toplevel.no_timing oo find_consts_cmd));
   166 
   167 end;
   168 
   169 end;
   170