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 wenzelm@56758: val read_query: Position.T -> string -> (bool * criterion) list 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; wenzelm@60667: val show_pat = quote o Input.source_content o Syntax.read_input; kleing@29895: in kleing@29895: (case c of wenzelm@60667: Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat) wenzelm@60667: | Loose pat => Pretty.str (prfx (show_pat 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@56025: val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt)); wenzelm@56025: val markup = Name_Space.markup const_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@56758: fun pretty_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@56025: val {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@56062: fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants [] wenzelm@59058: |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst)) wenzelm@46979: |> map (apsnd fst o snd); wenzelm@56912: wenzelm@56912: val position_markup = Position.markup (Position.thread_data ()) Markup.position; kleing@29884: in wenzelm@56891: Pretty.block wenzelm@56912: (Pretty.fbreaks wenzelm@56912: (Pretty.mark position_markup (Pretty.keyword1 "find_consts") :: wenzelm@56912: map pretty_criterion raw_criteria)) :: wenzelm@38335: Pretty.str "" :: wenzelm@56908: (if null matches then [Pretty.str "found nothing"] wenzelm@56908: else wenzelm@56908: Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") :: wenzelm@56908: grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches) wenzelm@56758: end |> Pretty.fbreaks |> curry Pretty.blk 0; wenzelm@56758: wenzelm@56758: fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args); kleing@29884: wenzelm@30142: wenzelm@30143: (* command syntax *) wenzelm@30142: wenzelm@38334: local wenzelm@30142: wenzelm@30142: val criterion = wenzelm@36950: Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || wenzelm@60664: Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict || wenzelm@60664: Parse.typ >> Loose; wenzelm@30142: wenzelm@56758: val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); wenzelm@56758: wenzelm@59934: val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords; wenzelm@58905: wenzelm@38334: in wenzelm@38334: wenzelm@56758: fun read_query pos str = wenzelm@59083: Token.explode query_keywords pos str wenzelm@56758: |> filter Token.is_proper wenzelm@56758: |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof))) wenzelm@56758: |> #1; wenzelm@56758: wenzelm@30142: val _ = wenzelm@59936: Outer_Syntax.command @{command_keyword find_consts} wenzelm@56758: "find constants by name / type patterns" wenzelm@56758: (query >> (fn spec => wenzelm@56758: Toplevel.keep (fn st => wenzelm@56758: Pretty.writeln (pretty_consts (Toplevel.context_of st) spec)))); wenzelm@30142: kleing@29884: end; kleing@29884: wenzelm@56758: wenzelm@56758: (* PIDE query operation *) wenzelm@56758: wenzelm@56758: val _ = wenzelm@60610: Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri} wenzelm@61223: (fn {state, args, writeln_result, ...} => wenzelm@60610: (case try Toplevel.context_of state of wenzelm@60610: SOME ctxt => wenzelm@60610: let wenzelm@60610: val [query_arg] = args; wenzelm@60610: val query = read_query Position.none query_arg; wenzelm@61223: in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end wenzelm@60610: | NONE => error "Unknown context")); wenzelm@56758: wenzelm@38334: end; wenzelm@38334: