wenzelm@30143: (*  Title:      Pure/Tools/find_consts.ML
kleing@29884:     Author:     Timothy Bourke and Gerwin Klein, NICTA
kleing@29884: 
wenzelm@30143: Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
wenzelm@30143: type over constants, but matching is not fuzzy.
kleing@29884: *)
kleing@29884: 
kleing@29884: signature FIND_CONSTS =
kleing@29884: sig
wenzelm@30143:   datatype criterion =
wenzelm@30143:       Strict of string
wenzelm@30143:     | Loose of string
wenzelm@30143:     | Name of string
kleing@29884:   val find_consts : Proof.context -> (bool * criterion) list -> unit
kleing@29884: end;
kleing@29884: 
wenzelm@33301: structure Find_Consts : FIND_CONSTS =
kleing@29884: struct
kleing@29884: 
wenzelm@30143: (* search criteria *)
wenzelm@30143: 
wenzelm@30143: datatype criterion =
wenzelm@30143:     Strict of string
wenzelm@30143:   | Loose of string
wenzelm@30143:   | Name of string;
kleing@29884: 
wenzelm@31684: 
wenzelm@30143: (* matching types/consts *)
kleing@29884: 
wenzelm@30143: fun matches_subtype thy typat =
wenzelm@38335:   Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
kleing@29884: 
wenzelm@38335: fun check_const pred (nm, (ty, _)) =
wenzelm@38335:   if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
kleing@29884: 
wenzelm@30143: fun opt_not f (c as (_, (ty, _))) =
wenzelm@38335:   if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
kleing@29884: 
wenzelm@46979: fun filter_const _ _ NONE = NONE
wenzelm@46979:   | filter_const c f (SOME rank) =
wenzelm@31684:       (case f c of
wenzelm@31684:         NONE => NONE
wenzelm@46979:       | SOME i => SOME (Int.min (rank, i)));
wenzelm@30143: 
wenzelm@30143: 
wenzelm@30143: (* pretty results *)
kleing@29895: 
kleing@29895: fun pretty_criterion (b, c) =
kleing@29895:   let
kleing@29895:     fun prfx s = if b then s else "-" ^ s;
kleing@29895:   in
kleing@29895:     (case c of
kleing@29895:       Strict pat => Pretty.str (prfx "strict: " ^ quote pat)
kleing@29895:     | Loose pat => Pretty.str (prfx (quote pat))
kleing@29895:     | Name name => Pretty.str (prfx "name: " ^ quote name))
kleing@29895:   end;
kleing@29895: 
wenzelm@49886: fun pretty_const ctxt (c, ty) =
wenzelm@30143:   let
wenzelm@35845:     val ty' = Logic.unvarifyT_global ty;
wenzelm@49886:     val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
wenzelm@49886:     val markup = Name_Space.markup consts_space c;
kleing@29895:   in
wenzelm@30143:     Pretty.block
wenzelm@49886:      [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
wenzelm@30143:       Pretty.quote (Syntax.pretty_typ ctxt ty')]
kleing@29895:   end;
kleing@29895: 
wenzelm@31684: 
wenzelm@30143: (* find_consts *)
wenzelm@30143: 
wenzelm@30143: fun find_consts ctxt raw_criteria =
wenzelm@30143:   let
wenzelm@42360:     val thy = Proof_Context.theory_of ctxt;
kleing@29884:     val low_ranking = 10000;
kleing@29884: 
wenzelm@33158:     fun user_visible consts (nm, _) =
wenzelm@33158:       if Consts.is_concealed consts nm then NONE else SOME low_ranking;
Timothy@30206: 
Timothy@30207:     fun make_pattern crit =
Timothy@30207:       let
Timothy@30207:         val raw_T = Syntax.parse_typ ctxt crit;
wenzelm@31684:         val t =
wenzelm@31684:           Syntax.check_term
wenzelm@42360:             (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
wenzelm@31684:             (Term.dummy_pattern raw_T);
Timothy@30207:       in Term.type_of t end;
kleing@29884: 
kleing@29884:     fun make_match (Strict arg) =
kleing@29884:           let val qty = make_pattern arg; in
wenzelm@30143:             fn (_, (ty, _)) =>
wenzelm@30143:               let
kleing@29884:                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
wenzelm@31684:                 val sub_size =
wenzelm@31684:                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
wenzelm@32790:               in SOME sub_size end handle Type.TYPE_MATCH => NONE
kleing@29884:           end
kleing@29884:       | make_match (Loose arg) =
kleing@29884:           check_const (matches_subtype thy (make_pattern arg) o snd)
kleing@29884:       | make_match (Name arg) = check_const (match_string arg o fst);
kleing@29884: 
kleing@29884:     fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
Timothy@30206:     val criteria = map make_criterion raw_criteria;
kleing@29884: 
Timothy@30206:     val consts = Sign.consts_of thy;
wenzelm@31684:     val (_, consts_tab) = #constants (Consts.dest consts);
wenzelm@31684:     fun eval_entry c =
wenzelm@46979:       fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
kleing@29884: 
wenzelm@30143:     val matches =
wenzelm@46979:       Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
wenzelm@46979:         consts_tab []
wenzelm@46979:       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
wenzelm@46979:       |> map (apsnd fst o snd);
kleing@29884:   in
wenzelm@38335:     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
wenzelm@38335:     Pretty.str "" ::
wenzelm@38335:     Pretty.str
wenzelm@38335:      (if null matches
wenzelm@46716:       then "nothing found"
wenzelm@46716:       else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
wenzelm@38335:     Pretty.str "" ::
wenzelm@38335:     map (pretty_const ctxt) matches
wenzelm@38335:   end |> Pretty.chunks |> Pretty.writeln;
kleing@29884: 
wenzelm@30142: 
wenzelm@30143: (* command syntax *)
wenzelm@30142: 
wenzelm@38334: local
wenzelm@30142: 
wenzelm@30142: val criterion =
wenzelm@36950:   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
wenzelm@36950:   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
wenzelm@36950:   Parse.xname >> Loose;
wenzelm@30142: 
wenzelm@38334: in
wenzelm@38334: 
wenzelm@30142: val _ =
wenzelm@50214:   Outer_Syntax.improper_command @{command_spec "find_consts"}
wenzelm@50214:     "find constants by name/type patterns"
wenzelm@36950:     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
wenzelm@51658:       >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
wenzelm@30142: 
kleing@29884: end;
kleing@29884: 
wenzelm@38334: end;
wenzelm@38334: