1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(* ========================================================================= *)
(* Simple online help system, based on old HOL88 one. *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
needs "define.ml";;
(* ------------------------------------------------------------------------- *)
(* Help system. *)
(* ------------------------------------------------------------------------- *)
let help_path = ref ["$/Help"];;
let help s =
let funny_filenames =
["++", ".joinparsers";
"|||", ".orparser";
">>", ".pipeparser";
"|=>", ".singlefun";
"--", ".upto";
"|->", ".valmod";
"insert'", "insert_prime";
"mem'", "mem_prime";
"subtract'", "subtract_prime";
"union'", "union_prime";
"unions'", "unions_prime";
"ALPHA", "ALPHA_UPPERCASE";
"CHOOSE", "CHOOSE_UPPERCASE";
"CONJUNCTS", "CONJUNCTS_UPPERCASE";
"EXISTS", "EXISTS_UPPERCASE";
"HYP", "HYP_UPPERCASE";
"INSTANTIATE", "INSTANTIATE_UPPERCASE";
"INST", "INST_UPPERCASE";
"MK_BINOP", "MK_BINOP_UPPERCASE";
"MK_COMB", "MK_COMB_UPPERCASE";
"MK_CONJ", "MK_CONJ_UPPERCASE";
"MK_DISJ", "MK_DISJ_UPPERCASE";
"MK_EXISTS", "MK_EXISTS_UPPERCASE";
"MK_FORALL", "MK_FORALL_UPPERCASE";
"REPEAT", "REPEAT_UPPERCASE"] in
let true_path = map hol_expand_directory (!help_path) in
let raw_listing =
map (fun s -> String.sub s 0 (String.length s - 4))
(itlist (fun a l -> Array.to_list (Sys.readdir a) @ l) true_path []) in
let mod_listing =
map fst funny_filenames @
subtract raw_listing (map snd funny_filenames) in
let edit_distance s1 s2 =
let l1 = String.length s1 and l2 = String.length s2 in
let a = Array.make_matrix (l1 + 1) (l2 + 1) 0 in
for i = 1 to l1 do a.(i).(0) <- i done;
for j = 1 to l2 do a.(0).(j) <- j done;
for i = 1 to l1 do
for j = 1 to l2 do
let cost = if String.get s1 (i-1) = String.get s2 (j-1) then 0 else 1 in
a.(i).(j) <- min (min a.(i-1).(j) a.(i).(j-1) + 1)
(a.(i-1).(j-1) + cost)
done
done;
a.(l1).(l2) in
let closeness s s' =
s',2.0 *. float_of_int
(edit_distance (String.uppercase s) (String.uppercase s')) /.
float_of_int(String.length s + String.length s') in
let guess s =
let guesses = mergesort(increasing snd) (map (closeness s) mod_listing) in
map fst (fst(chop_list 3 guesses)) in
Format.print_string
"-------------------------------------------------------------------\n";
Format.print_flush();
(if mem s mod_listing then
let fn = assocd s funny_filenames s ^".doc" in
let file = file_on_path true_path fn
and script = file_on_path [!hol_dir] "doc-to-help.sed" in
ignore(Sys.command("sed -f "^script^" "^file))
else
let guesses = map
(fun s -> "help \""^String.escaped s^"\";;\n") (guess s) in
(Format.print_string o end_itlist(^))
(["No help found for \""; String.escaped s; "\"; did you mean:\n\n"] @
guesses @ ["\n?\n"]));
Format.print_string
"--------------------------------------------------------------------\n";
Format.print_flush();;
(* ------------------------------------------------------------------------- *)
(* Set up a theorem database, but leave contents clear for now. *)
(* ------------------------------------------------------------------------- *)
let theorems = ref([]:(string*thm)list);;
(* ------------------------------------------------------------------------- *)
(* Some hacky term modifiers to encode searches. *)
(* ------------------------------------------------------------------------- *)
let omit t = mk_comb(mk_var("<omit this pattern>",W mk_fun_ty (type_of t)),t);;
let exactly t = mk_comb(mk_var("<match aconv>",W mk_fun_ty (type_of t)),t);;
let name s = mk_comb(mk_var("<match theorem name>",W mk_fun_ty aty),
mk_var(s,aty));;
(* ------------------------------------------------------------------------- *)
(* The main search function. *)
(* ------------------------------------------------------------------------- *)
let search =
let rec immediatesublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> h1 = h2 && immediatesublist t1 t2 in
let rec sublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> immediatesublist l1 l2 || sublist l1 t2 in
let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
and name_contains s (n,th) = sublist (explode s) (explode n) in
let rec filterpred tm =
match tm with
Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
| Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
| Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
| pat -> exists_subterm_satisfying (can (term_match [] pat)) in
fun pats ->
let triv,nontriv = partition is_var pats in
(if triv <> [] then
warn true
("Ignoring plain variables in search: "^
end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
else ());
(if nontriv = [] && triv <> [] then []
else itlist (filter o filterpred) pats (!theorems));;
|
