src/Pure/Tools/find_consts.ML
author wenzelm
Thu Jul 18 22:32:00 2013 +0200 (2013-07-18)
changeset 52703 d68fd63bf082
parent 51658 21c10672633b
child 56025 d74fed45fa8b
permissions -rw-r--r--
tuned messages -- avoid text folds stemming from Pretty.chunks;
     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   Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
    32 
    33 fun check_const pred (nm, (ty, _)) =
    34   if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
    35 
    36 fun opt_not f (c as (_, (ty, _))) =
    37   if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
    38 
    39 fun filter_const _ _ NONE = NONE
    40   | filter_const c f (SOME rank) =
    41       (case f c of
    42         NONE => NONE
    43       | SOME i => SOME (Int.min (rank, i)));
    44 
    45 
    46 (* pretty results *)
    47 
    48 fun pretty_criterion (b, c) =
    49   let
    50     fun prfx s = if b then s else "-" ^ s;
    51   in
    52     (case c of
    53       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
    54     | Loose pat => Pretty.str (prfx (quote pat))
    55     | Name name => Pretty.str (prfx "name: " ^ quote name))
    56   end;
    57 
    58 fun pretty_const ctxt (c, ty) =
    59   let
    60     val ty' = Logic.unvarifyT_global ty;
    61     val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
    62     val markup = Name_Space.markup consts_space c;
    63   in
    64     Pretty.block
    65      [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
    66       Pretty.quote (Syntax.pretty_typ ctxt ty')]
    67   end;
    68 
    69 
    70 (* find_consts *)
    71 
    72 fun find_consts ctxt raw_criteria =
    73   let
    74     val thy = Proof_Context.theory_of ctxt;
    75     val low_ranking = 10000;
    76 
    77     fun user_visible consts (nm, _) =
    78       if Consts.is_concealed consts nm then NONE else SOME low_ranking;
    79 
    80     fun make_pattern crit =
    81       let
    82         val raw_T = Syntax.parse_typ ctxt crit;
    83         val t =
    84           Syntax.check_term
    85             (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    86             (Term.dummy_pattern raw_T);
    87       in Term.type_of t end;
    88 
    89     fun make_match (Strict arg) =
    90           let val qty = make_pattern arg; in
    91             fn (_, (ty, _)) =>
    92               let
    93                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
    94                 val sub_size =
    95                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
    96               in SOME sub_size end handle Type.TYPE_MATCH => NONE
    97           end
    98       | make_match (Loose arg) =
    99           check_const (matches_subtype thy (make_pattern arg) o snd)
   100       | make_match (Name arg) = check_const (match_string arg o fst);
   101 
   102     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
   103     val criteria = map make_criterion raw_criteria;
   104 
   105     val consts = Sign.consts_of thy;
   106     val (_, consts_tab) = #constants (Consts.dest consts);
   107     fun eval_entry c =
   108       fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
   109 
   110     val matches =
   111       Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
   112         consts_tab []
   113       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
   114       |> map (apsnd fst o snd);
   115   in
   116     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
   117     Pretty.str "" ::
   118     Pretty.str
   119      (if null matches
   120       then "nothing found"
   121       else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
   122     Pretty.str "" ::
   123     map (pretty_const ctxt) matches
   124   end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
   125 
   126 
   127 (* command syntax *)
   128 
   129 local
   130 
   131 val criterion =
   132   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
   133   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   134   Parse.xname >> Loose;
   135 
   136 in
   137 
   138 val _ =
   139   Outer_Syntax.improper_command @{command_spec "find_consts"}
   140     "find constants by name/type patterns"
   141     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   142       >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
   143 
   144 end;
   145 
   146 end;
   147