author  Timothy Bourke 
Tue, 03 Mar 2009 12:14:52 +1100  
changeset 30207  c56d27155041 
parent 30206  48507466d9d2 
child 31684  d5d830979a54 
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 

29884  14 

15 
val find_consts : Proof.context > (bool * criterion) list > unit 

16 
end; 

17 

18 
structure FindConsts : FIND_CONSTS = 

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 

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

30143  30 
fun add_tye (_, (_, t)) n = Term.size_of_typ t + n; 
31 

32 
fun matches_subtype thy typat = 

33 
let 

29884  34 
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty); 
35 

36 
fun fs [] = false 

30143  37 
 fs (t :: ts) = f t orelse fs ts 
29884  38 

39 
and f (t as Type (_, ars)) = p t orelse fs ars 

40 
 f t = p t; 

41 
in f end; 

42 

30143  43 
fun check_const p (nm, (ty, _)) = 
44 
if p (nm, ty) 

45 
then SOME (Term.size_of_typ ty) 

46 
else NONE; 

29884  47 

30143  48 
fun opt_not f (c as (_, (ty, _))) = 
49 
if is_some (f c) 

50 
then NONE else SOME (Term.size_of_typ ty); 

29884  51 

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

52 
fun filter_const _ NONE = NONE 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

53 
 filter_const f (SOME (c, r)) = 
30143  54 
Option.map (pair c o (curry Int.min r)) (f c); 
55 

56 

57 
(* pretty results *) 

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

58 

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

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

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

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

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

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

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

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

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

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

68 

30143  69 
fun pretty_const ctxt (nm, ty) = 
70 
let 

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

71 
val ty' = Logic.unvarifyT ty; 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

72 
in 
30143  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')] 

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

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

78 

30143  79 
(* find_consts *) 
80 

81 
fun find_consts ctxt raw_criteria = 

82 
let 

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

83 
val start = start_timing (); 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

84 

29884  85 
val thy = ProofContext.theory_of ctxt; 
86 
val low_ranking = 10000; 

87 

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

88 
fun not_internal consts (nm, _) = 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

89 
if member (op =) (Consts.the_tags consts nm) Markup.property_internal 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

90 
then NONE else SOME low_ranking; 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

91 

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

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

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

94 
val raw_T = Syntax.parse_typ ctxt crit; 
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

95 
val t = Syntax.check_term 
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

96 
(ProofContext.set_mode ProofContext.mode_pattern ctxt) 
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset

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

98 
in Term.type_of t end; 
29884  99 

100 
fun make_match (Strict arg) = 

101 
let val qty = make_pattern arg; in 

30143  102 
fn (_, (ty, _)) => 
103 
let 

29884  104 
val tye = Sign.typ_match thy (qty, ty) Vartab.empty; 
105 
val sub_size = Vartab.fold add_tye tye 0; 

106 
in SOME sub_size end handle MATCH => NONE 

107 
end 

108 

109 
 make_match (Loose arg) = 

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

111 

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); 

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

115 
val criteria = map make_criterion raw_criteria; 
29884  116 

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

117 
val consts = Sign.consts_of thy; 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

118 
val (_, consts_tab) = (#constants o Consts.dest) consts; 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

119 
fun eval_entry c = fold filter_const (not_internal consts::criteria) 
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

120 
(SOME (c, low_ranking)); 
29884  121 

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

123 
Symtab.fold (cons o eval_entry) consts_tab [] 
30143  124 
> map_filter I 
125 
> sort (rev_order o int_ord o pairself snd) 

126 
> map ((apsnd fst) o fst); 

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

127 

30188
82144a95f9ec
avoid fragile parsing of end_timing result  would have produced GC time on MosML, for example;
wenzelm
parents:
30143
diff
changeset

128 
val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; 
29884  129 
in 
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

130 
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

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

132 
:: (Pretty.str o concat) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

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

134 
then ["nothing found", end_msg] 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

135 
else ["found ", (string_of_int o length) matches, 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

136 
" constants", end_msg, ":"]) 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

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

138 
:: map (pretty_const ctxt) matches 
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset

139 
> Pretty.chunks 
29884  140 
> Pretty.writeln 
30206
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset

141 
end; 
29884  142 

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

143 

30143  144 
(* 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

145 

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

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

147 
Toplevel.unknown_theory o Toplevel.keep (fn state => 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

148 
find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec); 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

149 

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

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

151 

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

152 
structure P = OuterParse and K = OuterKeyword; 
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 

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

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

155 
P.reserved "strict"  P.!!! (P.$$$ ":"  P.xname) >> Strict  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

156 
P.reserved "name"  P.!!! (P.$$$ ":"  P.xname) >> Name  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

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

158 

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 
in 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

160 

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

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

162 
OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

163 
(Scan.repeat (((Scan.option P.minus >> is_none)  criterion)) 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

164 
>> (Toplevel.no_timing oo find_consts_cmd)); 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset

165 

29884  166 
end; 
167 

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

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

169 