author | kleing |
Fri, 13 Feb 2009 16:00:45 +1100 | |
changeset 29895 | 0e70a29d3e02 |
parent 29884 | 74c183927054 |
permissions | -rw-r--r-- |
29884 | 1 |
(* Title: 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 type |
|
5 |
over constants, but matching is not fuzzy |
|
6 |
*) |
|
7 |
||
8 |
signature FIND_CONSTS = |
|
9 |
sig |
|
10 |
datatype criterion = Strict of string |
|
11 |
| Loose of string |
|
12 |
| Name of string |
|
13 |
||
14 |
val default_criteria : (bool * criterion) list ref |
|
15 |
||
16 |
val find_consts : Proof.context -> (bool * criterion) list -> unit |
|
17 |
end; |
|
18 |
||
19 |
structure FindConsts : FIND_CONSTS = |
|
20 |
struct |
|
21 |
||
22 |
datatype criterion = Strict of string |
|
23 |
| Loose of string |
|
24 |
| Name of string; |
|
25 |
||
26 |
val default_criteria = ref [(false, Name ".sko_")]; |
|
27 |
||
28 |
fun add_tye (_, (_, t)) n = size_of_typ t + n; |
|
29 |
||
30 |
fun matches_subtype thy typat = let |
|
31 |
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty); |
|
32 |
||
33 |
fun fs [] = false |
|
34 |
| fs (t::ts) = f t orelse fs ts |
|
35 |
||
36 |
and f (t as Type (_, ars)) = p t orelse fs ars |
|
37 |
| f t = p t; |
|
38 |
in f end; |
|
39 |
||
40 |
fun check_const p (nm, (ty, _)) = if p (nm, ty) |
|
41 |
then SOME (size_of_typ ty) |
|
42 |
else NONE; |
|
43 |
||
44 |
fun opt_not f (c as (_, (ty, _))) = if is_some (f c) |
|
45 |
then NONE else SOME (size_of_typ ty); |
|
46 |
||
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
47 |
fun filter_const (_, NONE) = NONE |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
48 |
| filter_const (f, (SOME (c, r))) = Option.map |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
49 |
(pair c o ((curry Int.min) r)) (f c); |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
50 |
|
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
51 |
fun pretty_criterion (b, c) = |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
52 |
let |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
53 |
fun prfx s = if b then s else "-" ^ s; |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
54 |
in |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
55 |
(case c of |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
56 |
Strict pat => Pretty.str (prfx "strict: " ^ quote pat) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
57 |
| Loose pat => Pretty.str (prfx (quote pat)) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
58 |
| Name name => Pretty.str (prfx "name: " ^ quote name)) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
59 |
end; |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
60 |
|
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
61 |
fun pretty_const ctxt (nm, ty) = let |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
62 |
val ty' = Logic.unvarifyT ty; |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
63 |
in |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
64 |
Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk, |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
65 |
Pretty.str "::", Pretty.brk 1, |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
66 |
Pretty.quote (Syntax.pretty_typ ctxt ty')] |
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 |
|
29884 | 69 |
fun find_consts ctxt raw_criteria = let |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
70 |
val start = start_timing (); |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
71 |
|
29884 | 72 |
val thy = ProofContext.theory_of ctxt; |
73 |
val low_ranking = 10000; |
|
74 |
||
75 |
fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) |
|
76 |
|> type_of; |
|
77 |
||
78 |
fun make_match (Strict arg) = |
|
79 |
let val qty = make_pattern arg; in |
|
80 |
fn (_, (ty, _)) => let |
|
81 |
val tye = Sign.typ_match thy (qty, ty) Vartab.empty; |
|
82 |
val sub_size = Vartab.fold add_tye tye 0; |
|
83 |
in SOME sub_size end handle MATCH => NONE |
|
84 |
end |
|
85 |
||
86 |
| make_match (Loose arg) = |
|
87 |
check_const (matches_subtype thy (make_pattern arg) o snd) |
|
88 |
||
89 |
| make_match (Name arg) = check_const (match_string arg o fst); |
|
90 |
||
91 |
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit); |
|
92 |
val criteria = map make_criterion ((!default_criteria) @ raw_criteria); |
|
93 |
||
94 |
val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy; |
|
95 |
fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria; |
|
96 |
||
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
97 |
val matches = Symtab.fold (cons o eval_entry) consts [] |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
98 |
|> map_filter I |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
99 |
|> sort (rev_order o int_ord o pairself snd) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
100 |
|> map ((apsnd fst) o fst); |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
101 |
|
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
102 |
val end_msg = " in " ^ |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
103 |
(List.nth (String.tokens Char.isSpace (end_timing start), 3)) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
104 |
^ " secs" |
29884 | 105 |
in |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
106 |
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
|
107 |
:: Pretty.str "" |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
108 |
:: (Pretty.str o concat) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
109 |
(if null matches |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
110 |
then ["nothing found", end_msg] |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
111 |
else ["found ", (string_of_int o length) matches, |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
112 |
" constants", end_msg, ":"]) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
113 |
:: Pretty.str "" |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
114 |
:: map (pretty_const ctxt) matches |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
115 |
|> Pretty.chunks |
29884 | 116 |
|> Pretty.writeln |
117 |
end handle ERROR s => Output.error_msg s |
|
118 |
||
119 |
end; |
|
120 |