https://github.com/JacquesCarette/hol-light
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
help.ml
(* ========================================================================= *)
(* 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));;