help.ml

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