author  wenzelm 
Mon, 06 Apr 2015 16:00:19 +0200  
changeset 59934  b65c4370f831 
parent 59083  88b0b1f28adc 
child 59936  b8ffc3dc9e24 
permissions  rwrr 
30143  1 
(* Title: Pure/Tools/find_consts.ML 
29884  2 
Author: Timothy Bourke and Gerwin Klein, NICTA 
3 

30143  4 
Hooglelike (http://wwwusers.cs.york.ac.uk/~ndm/hoogle) searching by 
5 
type over constants, but matching is not fuzzy. 

29884  6 
*) 
7 

8 
signature FIND_CONSTS = 

9 
sig 

30143  10 
datatype criterion = 
11 
Strict of string 

12 
 Loose of string 

13 
 Name of string 

56758  14 
val read_query: Position.T > string > (bool * criterion) list 
29884  15 
val find_consts : Proof.context > (bool * criterion) list > unit 
16 
end; 

17 

33301  18 
structure Find_Consts : FIND_CONSTS = 
29884  19 
struct 
20 

30143  21 
(* search criteria *) 
22 

23 
datatype criterion = 

24 
Strict of string 

25 
 Loose of string 

26 
 Name of string; 

29884  27 

31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

28 

30143  29 
(* matching types/consts *) 
29884  30 

30143  31 
fun matches_subtype thy typat = 
38335  32 
Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat)); 
29884  33 

38335  34 
fun check_const pred (nm, (ty, _)) = 
35 
if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE; 

29884  36 

30143  37 
fun opt_not f (c as (_, (ty, _))) = 
38335  38 
if is_some (f c) then NONE else SOME (Term.size_of_typ ty); 
29884  39 

46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset

40 
fun filter_const _ _ NONE = NONE 
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset

41 
 filter_const c f (SOME rank) = 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

42 
(case f c of 
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

43 
NONE => NONE 
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset

44 
 SOME i => SOME (Int.min (rank, i))); 
30143  45 

46 

47 
(* pretty results *) 

29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

48 

0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

49 
fun pretty_criterion (b, c) = 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

50 
let 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

51 
fun prfx s = if b then s else "" ^ s; 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

52 
in 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

53 
(case c of 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

54 
Strict pat => Pretty.str (prfx "strict: " ^ quote pat) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

55 
 Loose pat => Pretty.str (prfx (quote pat)) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

56 
 Name name => Pretty.str (prfx "name: " ^ quote name)) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

57 
end; 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

58 

49886  59 
fun pretty_const ctxt (c, ty) = 
30143  60 
let 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
33301
diff
changeset

61 
val ty' = Logic.unvarifyT_global ty; 
56025  62 
val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt)); 
63 
val markup = Name_Space.markup const_space c; 

29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

64 
in 
30143  65 
Pretty.block 
49886  66 
[Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1, 
30143  67 
Pretty.quote (Syntax.pretty_typ ctxt ty')] 
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

68 
end; 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

69 

31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

70 

30143  71 
(* find_consts *) 
72 

56758  73 
fun pretty_consts ctxt raw_criteria = 
30143  74 
let 
42360  75 
val thy = Proof_Context.theory_of ctxt; 
29884  76 
val low_ranking = 10000; 
77 

33158  78 
fun user_visible consts (nm, _) = 
79 
if Consts.is_concealed consts nm then NONE else SOME low_ranking; 

30206
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

80 

30207
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

81 
fun make_pattern crit = 
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

82 
let 
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

83 
val raw_T = Syntax.parse_typ ctxt crit; 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

84 
val t = 
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

85 
Syntax.check_term 
42360  86 
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt) 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

87 
(Term.dummy_pattern raw_T); 
30207
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

88 
in Term.type_of t end; 
29884  89 

90 
fun make_match (Strict arg) = 

91 
let val qty = make_pattern arg; in 

30143  92 
fn (_, (ty, _)) => 
93 
let 

29884  94 
val tye = Sign.typ_match thy (qty, ty) Vartab.empty; 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

95 
val sub_size = 
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

96 
Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0; 
32790
a7b92f98180b
handle Type.TYPE_MATCH, not arbitrary exceptions;
wenzelm
parents:
31687
diff
changeset

97 
in SOME sub_size end handle Type.TYPE_MATCH => NONE 
29884  98 
end 
99 
 make_match (Loose arg) = 

100 
check_const (matches_subtype thy (make_pattern arg) o snd) 

101 
 make_match (Name arg) = check_const (match_string arg o fst); 

102 

103 
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit); 

30206
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

104 
val criteria = map make_criterion raw_criteria; 
29884  105 

30206
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

106 
val consts = Sign.consts_of thy; 
56025  107 
val {constants, ...} = Consts.dest consts; 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset

108 
fun eval_entry c = 
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset

109 
fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking); 
29884  110 

30143  111 
val matches = 
56062  112 
fold (fn c => (case eval_entry c of NONE => I  SOME rank => cons (rank, c))) constants [] 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

113 
> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst)) 
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset

114 
> map (apsnd fst o snd); 
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

115 

293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

116 
val position_markup = Position.markup (Position.thread_data ()) Markup.position; 
29884  117 
in 
56891
48899c43b07d
tuned message  more context for detached window etc.;
wenzelm
parents:
56763
diff
changeset

118 
Pretty.block 
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

119 
(Pretty.fbreaks 
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

120 
(Pretty.mark position_markup (Pretty.keyword1 "find_consts") :: 
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset

121 
map pretty_criterion raw_criteria)) :: 
38335  122 
Pretty.str "" :: 
56908
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

123 
(if null matches then [Pretty.str "found nothing"] 
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

124 
else 
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

125 
Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") :: 
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset

126 
grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches) 
56758  127 
end > Pretty.fbreaks > curry Pretty.blk 0; 
128 

129 
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args); 

29884  130 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

131 

30143  132 
(* command syntax *) 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

133 

38334  134 
local 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

135 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

136 
val criterion = 
36950  137 
Parse.reserved "strict"  Parse.!!! (Parse.$$$ ":"  Parse.xname) >> Strict  
138 
Parse.reserved "name"  Parse.!!! (Parse.$$$ ":"  Parse.xname) >> Name  

139 
Parse.xname >> Loose; 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

140 

56758  141 
val query = Scan.repeat ((Scan.option Parse.minus >> is_none)  criterion); 
142 

59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59083
diff
changeset

143 
val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords; 
58905  144 

38334  145 
in 
146 

56758  147 
fun read_query pos str = 
59083  148 
Token.explode query_keywords pos str 
56758  149 
> filter Token.is_proper 
150 
> Scan.error (Scan.finite Token.stopper (Parse.!!! (query  Scan.ahead Parse.eof))) 

151 
> #1; 

152 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

153 
val _ = 
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
57918
diff
changeset

154 
Outer_Syntax.command @{command_spec "find_consts"} 
56758  155 
"find constants by name / type patterns" 
156 
(query >> (fn spec => 

157 
Toplevel.keep (fn st => 

158 
Pretty.writeln (pretty_consts (Toplevel.context_of st) spec)))); 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

159 

29884  160 
end; 
161 

56758  162 

163 
(* PIDE query operation *) 

164 

165 
val _ = 

166 
Query_Operation.register "find_consts" (fn {state, args, output_result} => 

167 
(case try Toplevel.context_of state of 

168 
SOME ctxt => 

169 
let 

170 
val [query_arg] = args; 

171 
val query = read_query Position.none query_arg; 

172 
in output_result (Pretty.string_of (pretty_consts ctxt query)) end 

173 
 NONE => error "Unknown context")); 

174 

38334  175 
end; 
176 