(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2011-06-18                                                           *)
(* ========================================================================== *)



#load "str.cma";;

flyspeck_needs "usr/thales/hales_tactic.hl";;

module Searching = struct

  open Hales_tactic;;


(*

? forces interpretation as a theorem.
?-n follows suggestion n.
%`x` performs type matching
%%[`x`;`y`] performs type matching.

*)

(* 
TODO: 
 -Combine different search mechanisms with the same return type.
 -Make a log of all searches, all bookmarked items, with context, for data mining purposes.
 -integrate suggest.
*)


(* quicksilver style search for name matching.
    ignore case and look for nonconsecutive letters. *)

let unsplit d f = function
  | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  | [] -> "";;

let match_sparse s u = 
  let re = Str.regexp_case_fold (".*"^(unsplit ".*" I (   explode s))) in
    Str.string_match re u 0;;

let maxl0 xs = try (end_itlist max xs) with _ -> 0;;

(*
let ignore = Pervasives.ignore;;
*)

(* ========================================================================== *)
(* TYPES *)


let types_of = Print_types.print_term_types;;
let type_of_thm = Print_types.print_thm_types;;
let type_of_goal = Print_types.print_goal_types;;
let goal_types = Print_types.print_goal_types;;


(* ========================================================================== *)
(* HELP                                              *)


let hollight_dir = 
  (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;

(* let local_help_dir =   Filename.concat flyspeck_dir "../help";; *)

let local_help_dir = ".";;

let helpdirs = ref [
  local_help_dir; 
  Filename.concat hollight_dir "Help"
 ];;

help_path := !helpdirs @ (!help_path);; (* hol-light help *)

let help_grep pat = 
  let split =   Str.split (Str.regexp "\n") in
  let cmd s = process_to_string ("(cd "  ^s^  "; ls | grep -v '~' | sed 's/.doc$//g' | grep '" ^pat^ "')") in
  List.flatten (map ( split o cmd ) (!helpdirs));;

(*
todo: if pat starts with regexp "-[a-z]+ " then it should be taken as a flags command.
Also make help_grep_local a flag, say -l for local.
*)

let help_flag flag pat  = 
  let constant_of_regexp ss = 
    let re = Str.regexp_case_fold (".*"^ss) in
    let c = map fst (constants()) in
      filter (fun s -> Str.string_match re s 0) c in
  let help_grep_local pat =
    let backup = !helpdirs in
    let _ = helpdirs := [local_help_dir] in 
    let out = help_grep pat in
    let _ = helpdirs := backup in
      out in
  let split =   Str.split (Str.regexp "\n") in
  let grep_s s = Printf.sprintf "(cd %s; ls | sed 's/.doc$//g' | grep -i '%s')" s pat in 
  let cmd s = process_to_string (grep_s s) in
    match flag with
      | 'i' ->  List.flatten (map ( split o cmd ) (!helpdirs))
      | 'd' -> constant_of_regexp pat
      | 'l' -> help_grep_local pat
      | 'g' -> help_grep pat
      | _ -> [" 'd' search constants";"'g' help_grep"; "'i' ignore case"; "'l' help_grep local dir"];;


(*  
Example:
help_grep "ASM.*REWRITE";;
help_grep "^ASM_";;
help_grep "help";;
help_grep "RULE";;
help_grep "ARITH";;
help_grep "_TAC$";;
List.length (help_grep ".*");;

help_flag '?' "";;

help_flag 'd'  ".*contin";;
help_flag 'd'  ".*integr";;
help_flag 'd'  ".*auchy";;
help_flag 'd'  "at.*[ng]$";;
help_flag 'd' "cos" ;;

*)



(* ========================================================================== *)
(* SEARCH *)

let def s = mk_comb(mk_var("<match constant def>",W mk_fun_ty aty),
                     mk_var(s,aty));;

let searches = ref[];;

let searcht n pat = 
  let _ = searches := (n,pat)::!searches in
  let def_of_regexp ss = 
    let c = help_flag 'd'  ss in
    let strip d =   (fst o dest_const o fst o dest_eq o concl) d in
    let def_assoc = map (fun t -> (strip t,t)) (definitions()) in
      map (fun s -> (s,assoc s def_assoc)) c in
  let raw = match pat with
    | Comb(Var("<match constant def>",_),Var(ss,_))::_ -> def_of_regexp ss
    | _ -> search pat in
  let m = min n (List.length raw) in
  let s = sortlength_thml raw in
  let r = fst (chop_list m s) in
  let z = zip (0--(List.length r - 1)) r in
    z;;

let searchl ls pat = search_thml (term_match [])  pat ls;;

(* added Oct 2012 *)

let save_searc  = ref [];;

let searc c n tl =
  let u = snd(List.nth (searcht (n+1) tl) n) in
  let _ = (save_searc := (c,u)::!save_searc) in
     u;;

(* tactics that search assumption list for match.
   Deprecated. Replaced with FIRST_X_ASSUM_ST *)

(*
let SEARCH_THEN pat ttac (asl,w) =
  let thl = map snd (searchl asl pat) in
    ttac thl (asl,w);;

let FIRST_SEARCH_THEN pat ttac (asl,w) =
  let thl = map snd (searchl asl pat) in
    ttac (hd thl) (asl,w);;
*)

let searchn n f s = snd(List.nth (searcht (n+1) f) n);;  (* used for write-up of search results *)

(* 
Example: searcht 5 [def "cos"];;
searcht 5 [def "mul"];;
*)

let research m = 
  let (n,pat) = hd (!searches) in
    searcht (m) pat;;

let search_results = ref [];;

(* add stored searches to list *)
let augment_search_results ss = 
  let get s = try (Lib.assoc s !theorems) with _ -> failwith s in
  let cs = map (fun (_,s,_,_) -> s) !search_results in
  let ss = Lib.subtract ss cs in
  let ns = List.length cs in
  let ss = Lib.zip (ns -- (ns+List.length ss - 1)) ss in
  let ss =   map (fun (i,s) -> (i,s,get s,[])) ss in
    !search_results @ ss;;

let mark m = 
  let (n,pat) = hd (!searches) in
  let (s,th) =   snd(List.nth (searcht (1 + min n m) pat) m)  in
  let v = (List.length !search_results,s,th,pat) in
  let _ = search_results := v::(!search_results) in
    v;;

let result n pat = 
  let ls = map (fun (_,s,th,_) -> (s,th)) !search_results in
  let a = zip ls !search_results in
  let sl = if pat = [] then ls else searchl ls pat in
  let n' = min n (List.length sl) in
  let ts =   fst(chop_list n' (sl)) in
    map (fun t -> assoc t a) ts;;

let results pat = 
  let n = List.length (!search_results) in 
    result n pat;;

let retrieve_search_number n = 
  let (_,s,_,_) = Lib.find (fun (c,_,_,_) -> (c=n)) !search_results in
    s;;

(*


let (srch,more,less,retrieve_search)  =
  let allsearch = ref [] in

  let tags = explode "abcdefghijklmnopqrstuvwxyz" in
  let tag_num = ref 0 in

  let update () = (tag_num := (!tag_num + 1) mod (List.length tags)) in

  let current_search = ref [] in
  let nextdisplayed = ref 0 in

  let ziptg tg a xs = 
    let z = zip (a--(List.length xs - 1 + a)) xs in
      map (fun (i,x) -> (tg^(string_of_int i),x)) z  in

  let sub_range tg a b xs = 
    let b' = min b (List.length xs - 1) in
    let _ = (a <= b') or failwith "bad range" in
    let _ = (0 <= a) or failwith "bad neg index" in
    let bs = fst (chop_list (b'+1) xs) in
     ziptg tg a (snd (chop_list a bs)) in 
    
  let more () = 
    let tg = List.nth tags (!tag_num) in
    let sr = sub_range tg (!nextdisplayed) (!nextdisplayed + 5) (!current_search) in
    let _ = (nextdisplayed := 5 + !nextdisplayed) in
      sr  in

  let less () =
    let _ = (nextdisplayed := max 0 (!nextdisplayed - 10)) in
      more()  in

  let srch pat = 
    let raw = search pat in
    let _ = update() in
    let _ = (nextdisplayed := 0) in
    let _ = current_search := sortlength_thml raw in
    let tg = List.nth tags (!tag_num) in
    let _ = (allsearch := (tg,!current_search)   :: !allsearch) in
      more() in

  let retrieve_search tag item = 
    fst ( List.nth (Hol_pervasives.assoc tag !allsearch)  item) in

    (srch,more,less,retrieve_search);;
*)

(* ========================================================================== *)
(* STATS of WORD COUNTS, indexing all words in  HOL LIGHT and FLYSPECK  *)


let wc_tmpfile = Filename.temp_file "tmp_" ".txt";;

let int_tmpfile = 
  let ss1 = process_to_string ("ls "^flyspeck_dir^"/*/*.hl") in
  let ss2 = Str.split (Str.regexp "\n") ss1 in
  let ss1 = process_to_string ("ls "^hollight_dir^"/*/*.ml") in
  let ss2 =  Str.split (Str.regexp "\n") ss1 @ ss2 in
  let tmpfile =  wc_tmpfile in
  let _ =     Sys.command("touch "^tmpfile) in
  let _ =     map (fun s -> Sys.command("cat "^ s^ " >> " ^ tmpfile)) ss2 in
    ();;

let word_counts() = 
  let sout = Str.split (Str.regexp "\n") 
    (process_to_string("cat "^wc_tmpfile^" | tr -C 'A-Z:a-z0-9_' '\n' | sort | uniq -c | sed 's/^ *//'")) in
  let sout1 = map (Str.split (Str.regexp " ")) sout in
  let sout2 = filter (fun t -> List.length t = 2) sout1 in
  let sout3 = map (function | [a;b]-> (b,int_of_string a) | _ -> ("?",0)) sout2 in
    sout3;;

let word_count_list = word_counts();;

(* stats of the word immediately following another word.
   This can be useful in determining, for example, which theorems are used
   with MATCH_MP_TAC.  Or which tactics are used with REPEAT. *)

let word_successor_counts word_successor = 
  let sed_pipe = Printf.sprintf "grep '%s ' %s | sed 's/^.*%s *//'  | sed 's/^[^a-z.A-Z]*//g' | sed 's/ .*$//g' | tr -C 'A-Z.a-z_0-9' '\n' | sed 's/ //g' | sort | uniq -c | sed 's/^ *//'" 
    word_successor wc_tmpfile word_successor in 
  let sout = Str.split (Str.regexp "\n") 
    (process_to_string(sed_pipe )) in
  let sout1 = map (Str.split (Str.regexp " ")) sout in
  let sout2 = filter (fun t -> List.length t = 2) sout1 in
  let sout3 = map (function | [a;b]-> (b,int_of_string a) | _ -> ("?",0)) sout2 in
    sort (fun (_,a) (_,b) -> (a > b)) sout3;;

(* inaccurate because constants and theorems with the same name are overcounted *)

let thm_counts = 
  let alpha_thm = sort (<) (map fst !theorems) in
  let rec build buff ats bts = match (ats,bts) with
    | ([],_) -> buff
    | (_,[]) -> buff
    | (a::atss,(b,n)::btss) -> if (a=b) then build ((b,n)::buff) atss btss
      else if (a>b) then build buff ats btss else build buff atss bts in
  sort (fun (_,a) (_,b) -> (a > b)) (build [] (alpha_thm) word_count_list);;

let quasi_tactic_list = 
  let tactic_wordlist =  
    ["REPEAT";"POP_ASSUM";
     "FIRST_X_ASSUM";"FIRST_ASSUM";
     "fun";"REAL_ARITH";"ARITH_RULE";"TAUT"] in
  let tactic_list =  (help_grep "TAC$") in
  let then_list =  (help_grep "THEN") in
    tactic_wordlist @ tactic_list @ then_list;;

let tactic_counts = sort (fun (_,a) (_,b) -> (a > b)) 
  (filter (fun (a,_) -> mem a  (quasi_tactic_list)) word_count_list);;


(* ========================================================================== *)
(* DEPTH FUNCTIONS *)
(* each constant is defined in terms of other constants.
   The depth of a constant is the length of its longest chain down to the primitives *)

(* SLOW BUT POTENTIALLY USEFUL. START HERE.


let nub = Parse_ineq.nub;;

let rec c_of buf = function
  | Const _ as t  -> nub (t:: buf)
  | Comb (r,s)  -> c_of (c_of buf r) s
  | Abs (x,t) -> c_of buf t
  | _ -> nub buf;;

let def_assoc = 
  let r =  (map (dest_eq o concl) (definitions())) in
  let s = fst o dest_const in 
    map (fun (x,y) -> ( s x,nub (map s (c_of [] y)))) r;;

let stm_depth = 
  let cache = ref [] in
  let rec s_depth t = 
    try (assoc t !cache)
    with _ -> 
      let rs = try (assoc t def_assoc)
      with _ -> [] in
      let _ = not(mem t rs) or failwith t in
      let u = 1 + maxl0 (map s_depth rs) in
      let _ = cache:= (t,u)::!cache in
	u in
    s_depth;;

let sdef_assoc = map (fun (t,ul) -> ((t,stm_depth t),(map (fun u -> (u,stm_depth u)) ul)))
  def_assoc;;

let tm_depth t =
  let c = map (fst o dest_const )(c_of [] t) in
  let u = map (fun x -> (x,stm_depth x)) c in
  let s = nub (sort (fun (_,a) (_,b) -> a > b) u) in
    s;;

(* ball park distance of goal *)

let rec rec_hash n acc = function
  |  [] -> acc
  |  (a,_)::b -> if (n<=0) then acc else rec_hash (n-1) (Hashtbl.hash a ::acc) b;;

let hash_depths = sort (<) o (rec_hash 3 []);;

let rec sorted_meet k al bl = if (k<1) then true else  (* look for at least k matches *)
  (match bl with
  | [] -> false
  | b::bl' -> match al with
      | [] -> false
      | a::al' -> if (a = b) then 
	  (sorted_meet (k-1) al' bl')
	else 
	  (if (a<b) then sorted_meet k al' bl else sorted_meet k al bl'));;

let strip_imp = striplist dest_imp;;

let preprocess_theorems thml = 
  let get_tm_depth = (tm_depth o last o strip_imp o snd o strip_forall o concl ) in
  let de = function | [] -> 0 | ((_,d)::_) -> d in
  let data r = (de r,hash_depths r) in
  let thl = map (fun (s,t) -> ((data o get_tm_depth) t,s,t) ) thml in
    thl;;

let depth_encoded_theorems = preprocess_theorems (!theorems);;

let rec ballpark i j  thml (d,hd) = 
  if (List.length thml < 80) then thml else
    let k = max i j in
    let (thml',i',j') = 
      if (k=i) then (filter (fun ((d',_),_,_)-> abs(d-d') < 1+k) thml,i-1,j) else
	(filter (fun ((_,hd'),_,_) -> (sorted_meet (3-k) hd hd')) thml,i,j-1) in
      if (List.length thml' < 20) then thml else ballpark i' j' thml' (d,hd);;

let  ballpark_theorems (_,w) = 
  let thml = depth_encoded_theorems in
  let get_tm_depth = (tm_depth o last o strip_imp o snd o strip_forall ) in
  let de = function | [] -> 0 | ((_,d)::_) -> d in
  let data r = (de r,hash_depths r) in
    map (fun (_,s,t)->(s,t))  (ballpark 3 3 thml (data (get_tm_depth w)));;


(* fails on depth 0 *)

let drop_depth_once ul = 
  List.flatten (map  (fun u -> assoc u sdef_assoc) ul);;

let rec drop_depth_to d ul =
  let (hi,lo) = partition (fun (_,h) -> (h>d)) ul in
    if hi = [] then ul else
      let hi' = drop_depth_once hi in
	(nub ((drop_depth_to d hi') @ lo));;

(* metric symbol distance, an estimate of the distance between two lists of symbols.
    dsofar = distance so far.
    common = list of symbols and their shallowings that the two lists have already in common.
    depth_weight is a heuristic weighting: matches should increase distance less than mismatches.
*)

let rec msd dsofar common  al bl = 
  if (al=[]) && (bl=[]) then dsofar else
    let depth_weight = 10 in
    let d = maxl0 (map snd (al @ bl)) in 
    let c =  ( drop_depth_to d common) @ (intersect al  bl) in
    let al' = subtract al c in
    let bl' = subtract bl c in
    let dsofar' = dsofar +.  float_of_int( List.length ((intersect al  c) @ (intersect bl  c)) +
					     depth_weight *  List.length (al' @ bl')) in
      if (d <=1) then dsofar'  else
	let al'' = drop_depth_to (d-1) al' in
	let bl'' = drop_depth_to (d-1) bl' in
	  msd dsofar' c al'' bl'';;

let metric_symbol_distance bl cl = 
  let tt tl = List.flatten (map tm_depth tl) in
  if (List.length bl = 1)&&(List.length cl=1)&& (aconv (hd bl) (hd cl)) then 0.0
  else msd 10.0 [] (tt bl) (tt cl);;

let nearest_thm_to_goal (asl,w) = 
  let tt tl = List.flatten (map (tm_depth o concl) tl) in
  let common = tt (map snd asl) in
  let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) (!theorems) in
  let r = map (fun (tl,s,t) -> (tl,s,t,msd 0.0 common (tm_depth w) tl)) thl in
    (sort (<) r);;


let thm_depth = tm_depth o concl;;

let search_depth  = 
  let dthm = map (fun (s,t) -> (maxl0 (map snd(thm_depth t)),(s,t))) !theorems in
  let m tml = maxl0 (map snd (List.flatten (map (tm_depth) tml))) in
  let fthm tml = map snd (filter (fun (x,(_,_)) -> (x <=m tml)) dthm) in    
    fun tml -> searchl (fthm tml) tml;;

END SLOW BUT POTENTIALLY USEFUL
*)

(* ========================================================================== *)
(* EVAL AND PROOF STACK *)

(*
eval_command comes from

http://solaria.dimino.org/cgi-bin/darcsweb.cgi?r=peps;a=headblob;f=/src/core/peps_top.ml
License: BSD3

If the expression is syntactically correct 
and the evaluation raises an exception, then the return value is true.
*)


let eval_command ?(silent=false) command =
   let buffer = Buffer.create 512 in
   let pp = Format.formatter_of_buffer buffer in
   Format.pp_set_margin pp max_int;
   try
     let _ =
       Toploop.execute_phrase (not silent) pp
         (!Toploop.parse_toplevel_phrase (Lexing.from_string (command ^ ";;")))
     in
     (true, Buffer.contents buffer)
   with exn ->
     let save = !Toploop.parse_use_file in
     Toploop.parse_use_file := (fun _ -> raise exn);
     Pervasives.ignore (Toploop.use_silently pp "/dev/null");
     Toploop.parse_use_file := save;
     (false,  Buffer.contents buffer);;

(* eval_command ~silent:false "g `x=y`";; *)

type proof_record = Tax of string*int*tactic | Bax | Gax of term*string;;

let proof_record  =ref [];;
let tactic_cache = ref (fun () -> ALL_TAC);;

(* we evaluate the tactic outside eval_command, so that we can catch exceptions *)

let eval_tactic  = 
  fun s ->
    let (b,r) = eval_command ~silent:false 
      ("tactic_cache := (fun () -> ("^s^"));;") in
    let _ = b or (print_string (r^"\n"^s^"\n"); failwith "bad input string") in
    let t= (!tactic_cache)() in
    let (_,gs,_) ::_ = !current_goalstack in
    let i = List.length gs in
    let v = Hol_pervasives.e(t) in
    let _ = proof_record := Tax (s,i,t)::!proof_record in
      v;;

(*
let string_of_frees t = 
  let u =  (map (fst o dest_var) o frees) t in
    (unsplit " " I) u;;
*)

let eval_goal t = 
  let _ = print_goalstack (Hol_pervasives.g(t));
    proof_record := Gax (t,process_to_string "date")::!proof_record;
    warn (has_stv t)  "?type in goal" in
    ();;

let eval_back () = 
  let _ = proof_record := Bax::!proof_record in Hol_pervasives.b();;

(*
eval_goal `1 + 1 = 2`;;
eval_tactic "REPEAT STRIP_TAC";;
eval_back();;
eval_tactic "ARITH_TAC";;
eval_tactic "REWRITE_TAC[TRUTH]";;
*)

let string_starts_with u s = 
  (String.length u <= String.length s) && (u = String.sub s 0 (String.length u));;

let rec strs_of_proof_records ind skip buf  =   
  let by t s = if t && (not (string_starts_with "BY" s)) then "BY("^s^")" else s in
    function
	[] -> buf
      | Gax _ :: xs -> buf
      | Tax (s,i,_) :: xs -> 
	  let indent = String.make (2*i) ' ' in
	    if (skip=0) then strs_of_proof_records i skip ((indent^(by (i>ind) s))::buf) xs
	    else strs_of_proof_records ind (skip-1) buf xs
      | Bax :: xs -> strs_of_proof_records ind (skip+1) buf xs;;

let string_of_proof () = 
  let ss = strs_of_proof_records 0 0 [] !proof_record in
    "\n[\n"^unsplit ";\n" I (ss) ^"\n]\n";;

let print_proof () = 
  print_string (string_of_proof());;

let string_of_proof_k k () = 
  let ss = strs_of_proof_records 0 0 [] !proof_record in
  let k' = min k (List.length ss) in
  let ss' = (fst(chop_list k' (List.rev ss))) in
    if (List.length ss' = 0) then "" 
    else if (List.length ss' = 1) then hd(ss')
    else "\n[ ... most recent steps ...\n"^unsplit ";\n" I (List.rev ss') ^"\n]\n";;

let rec split_proof_record acc cur = function
  | [] -> if (List.length cur > 0) then acc @[cur] else acc
  | Gax (_,_) as a :: xs -> 
      let acc' =  acc @ [cur @ [a]]  in
	split_proof_record acc' [] xs
  | a :: xs -> split_proof_record acc (cur @ [a]) xs;;

let gax() =
  let u = split_proof_record [] [] (!proof_record) in
  let j = zip u (0-- (List.length u - 1)) in
  let k = map (fun (u,z) -> (z,List.length u,last u)) j in
     k;;


split_proof_record [] [] (!proof_record);;

(*
print_string (string_of_proof());;
*)   


(* ========================================================================== *)
(* SUGGEST TACTIC                                              *)



(* term matching without higher order matches *)


let term_match_no_ho pat u = 
  let (_,b,c) = (term_match[] pat u) in
  let v = instantiate ([],b,c) pat in 
    aconv v u  or failwith "no match";;

let match_g_no_ho pat (_,w) = not(search_thml term_match_no_ho pat [("", ASSUME w)] = []);;

let match_g pat (_,w) = not(search_thml (term_match[]) pat [("", ASSUME w)] = []);;

let match_asm pat (asl,_) = not(search_thml term_match_no_ho pat asl = []);;

(* new version, july 2012 *)

let noses = ref [];;

let add_your_nose x = (noses := x::!noses);;

let follow_your_nose_string() = 
  let aslw = top_realgoal() in
  let n = 
    try
      let (_,_,a) = find (fun (p,_,_) -> p aslw) !noses 
      in a 
    with Failure _ -> "" in 
    n;;

let fyn () = 
  let aslw = top_realgoal() in
  let (_,t,_) = find (fun (p,_,_) -> p aslw)  !noses in
    t;;

let follow_your_nose_string_list() = 
  let aslw = top_realgoal() in
  let m = filter (fun (p,_,_) -> p aslw) !noses in
  let m2 = map (fun ((_,_,a),b) -> ("{"^string_of_int b ^":"^a^"}")) (zip m (0--((List.length m) -1))) in
    Flyspeck_lib.join_comma m2;;

let fynlist k = 
  let aslw = top_realgoal() in
  let m = filter (fun (p,_,_) -> p aslw) !noses in
  let l = List.length m in
  let _ = k < l or failwith ("fyn length = "^string_of_int k ^ " "^string_of_int l) in
  let (_,t,_) = List.nth m k in
   t;;


(* new version, march 2012 *)

let nub = Parse_ineq.nub;;


let rec c_of buf = function
  | Const _ as t  -> nub (t:: buf)
  | Comb (r,s)  -> c_of (c_of buf r) s
  | Abs (x,t) -> c_of buf t
  | _ -> nub buf;;

let rewrite_tags = ref [];;
let remove_rewrite_tag s =
  rewrite_tags:= filter (fun (_,_,s',_) -> not (s =s')) !rewrite_tags;;

let st_of tm = map (fst o dest_const) (c_of [] tm);;
let add_rewrite_tag (s,th) = 
  let thl = mk_rewrites true th [] in
  let tml = map concl thl in
  let wd tm = if (is_imp ( tm)) then (snd(dest_imp( tm))) else tm in
  let tml = map (fst o dest_eq  o wd) tml in
  let stl = map st_of tml in
  let zl = map (fun (a,b)-> (a,b,s,th)) (zip tml stl) in
  let _ =     rewrite_tags := zl @ !rewrite_tags in
    ();;

let add_rewrite_stag s = 
  let _ = (can (assoc s) !theorems) or failwith (s ^ " not found ") in
  add_rewrite_tag (s,assoc s !theorems);;

let refresh_rewrite_stag s = 
  let _ = remove_rewrite_tag s in
    add_rewrite_stag s;;

let refresh() = 
  let _ = map (fun (_,s,_,_) -> refresh_rewrite_stag s) !search_results in
    ();;

let write m = 
  let u = mark m in
  let (_,s,_,_) = u in
  let _ =     refresh_rewrite_stag s in
    u;;
  
let lookup_rewrite_tags (asl,w) = 
  let sw = st_of w in
  let f1 = filter (fun (_,sl,_,_) -> (subset sl sw)) !rewrite_tags in
  let ml = filter (fun (pat,_,_,_) -> match_g [pat] (asl,w)) f1 in
    ml;;

let rewrite_suggest() = 
  let rawl =  lookup_rewrite_tags (top_realgoal()) in
    zip (0--(List.length rawl - 1)) (map (fun (_,_,s,th) -> (s,th)) rawl);;

let suggest = rewrite_suggest;;

(* let assum t = mk_comb(mk_var("<assum>",W mk_fun_ty (type_of t)),t);; *)

(* 

trigger pattern;
English text;
prompt;
tactic;

*)

let tactic_patterns = ref [];;

let add_tactic_pattern t = (tactic_patterns := t::!tactic_patterns);;

let tactic_suggest _ = 
  let s = filter (fun (a,_,_,_) -> a (top_realgoal())) !tactic_patterns in
  zip (0-- (List.length s  -1) ) s;;

let print_suggest sg = 
  let print_one (i,(_,_,s,_)) = (print_int i; print_string (": "^s)) in
  map (print_one) sg;;

(*
let s () = let sg = suggest() in Pervasives.ignore(print_suggest sg);;
*)

let expand_suggest s = 
  let sg = tactic_suggest() in
  let n = (int_of_string s) in
  let r = Lib.assoc n sg in
    (fun (_,s,_,_) -> s) r;;

(*
let eh n = let (_,(_,_,_,tac)) = List.nth (suggest()) n in e(tac());;
*)

(* let follow n = let (_,(_,_,_,tac)) = List.nth (suggest()) n in tac();; *)

(*
let rewrite_suggest = [
 ([`x IN {y}`],"IN_SING",IN_SING);
];;

let rewrites _ =
  let s = filter (fun (a,_,_) -> match_g a (top_realgoal())) rewrite_suggest in
    zip (0-- (List.length s  -1) ) s;;
*)

(* ========================================================================== *)
(* ABBREVIATIONS                                              *)

let matching_tactics  s = 
  filter (match_sparse s) (map fst tactic_counts);;

let tactic_abbreviations = ref [];;

let abbrev u = (tactic_abbreviations:= (u::!tactic_abbreviations));;

let unabbrev s = (tactic_abbreviations:= (filter (fun (s',_) ->  (s <> s')) !tactic_abbreviations));;

let thm_abbreviations = ref[("elim","IN_ELIM_THM");("morgan","DE_MORGAN_THM")];;

let thm_abbrev s = (let _ = thm_abbreviations:= s::!thm_abbreviations in s);;

thm_abbrev ("empty","EMPTY");;

let expansive_thms   = 
  let  full =  (map fst thm_counts) in
    fun op s ->
      let searches = map (fun (_,s,_,_) -> s) !search_results in
	op (match_sparse s) (searches @ full);;

(*
?n to get marked theorem n.
?abbrev to abbreviate.
*)

let expand_thm  =
  let charset = (explode "abcdefghijklmnopqrstuvwxyz0123456789'_.") in
  let number s = 
    let n = int_of_string s in
      retrieve_search_number n in
  let search_thm s = 
    let c = s.[0] in
      fst(Hol_pervasives.assoc c (!save_searc)) in
  let abbreviable s = (subset (explode s) charset) in 
  let unabbrev s = 
    let _ = not(abbreviable s) or failwith "abbrev" in s in
  let exact_thm s = (Pervasives.ignore (Hol_pervasives.assoc s !theorems); s) in
  let assoct s = Hol_pervasives.assoc s !thm_abbreviations in
  let match_t = expansive_thms Lib.find in
   fun s->  tryfind (fun f -> f s) [unabbrev;search_thm;number;exact_thm;assoct;match_t;I];; 

(*
%`x` to expand types of term
%%[`x`;`y`] to expand types of term list.
*)

(* deprecated HASH: *)

(*
let el_to_hash s i = 
  let el_assoc = [
    ("u","HASH_UNDISCH_TAC");
    ("r","HASH_RULE_TAC");
    ("k","HASH_KILL_TAC");
    ("p","HASH_COPY_TAC");
    ("c","HASH_CHOOSE_TAC");
    ("x","HASH_X_CHOOSE_TAC");
    ("a","HASH_ASM_REWRITE_TAC")] in
  let tac = assoc s el_assoc in
  let h = el_hash i (top_realgoal()) in
    tac ^ " " ^ (string_of_int h);;
*)

let el_to_hash s i = failwith "el_to_hash has been deprecated";;

let break_init init s = 
  let l_init = String.length init  in
  let _ = (l_init <= String.length s) or failwith "length mismatch break_init" in
  let _ = (String.sub s 0 l_init = init) or failwith "mismatch break_init" in
    String.sub s (l_init) (String.length s - l_init);;

let unabbrev_string  =
  let charset = (explode "abcdefghijklmnopqrstuvwxyz0123456789'_/\\!?@") in
  let abbreviable s = (subset (explode s) charset) in 
  let unabbrev s = 
    let _ = not(abbreviable s) or failwith "abbrev" in s in
  let assoc_thm s = (Pervasives.ignore (Hol_pervasives.assoc s !theorems); s) in
  let assoct s = Hol_pervasives.assoc s !tactic_abbreviations in
  let assoc_sans_t s = 
    let len = String.length s in
    let _ = (len > 1) or failwith "too short" in
    let _ = (s.[len-1]= 't') or failwith "final char t" in
      assoct (String.sub s 0 (len -1)) in
  let hash s = 
    let rest = break_init "el" s in
    let c = String.sub rest 0 1 in
    let n = int_of_string (String.sub rest 1 (String.length rest - 1)) in
      el_to_hash c n in
  let tac s = 
    let v = matching_tactics s in
      if (List.length v > 0) then hd v else s in
  let fynose s = 
    if (s = "fyn") then fyn ()
    else 
      let _ = String.length s = 4 or failwith "fynose" in
      let _ = "fyn" = String.sub s 0 3 or failwith "fynose2" in
      let k = int_of_string (String.sub s 3 1) in
	fynlist k in
  let deprecated_fynose s = 
    let _ = (s = "fyn") or failwith "fynose" in fyn () in
   fun s->  tryfind (fun f -> f s) [unabbrev;assoc_thm;fynose;assoct;assoc_sans_t;hash;hash;tac;];; 



(* ========================================================================== *)
(* PARSING INPUT *)

type mtoken =
       | M_comment
       | M_string of string
       | M_hol_term of string
        | M_semicolon
	| M_white of string
	| M_text of string
	| M_query of string
	| M_lparen
	| M_rparen
	| M_lbracket
	| M_rbracket
       | M_env of int
	    (* not implemented : *)
      | M_local of string
       | M_asm of int ;; 

let some_look p =
  function
      [] -> raise Noparse
    | [_] -> raise Noparse
    | (h1::h2::t) -> if p (h1,h2) then (h1,h2::t) else raise Noparse;;

let rec m_lex  = 
  let stringchar =
      some (fun i -> i <> "\"") in
  let string = a "\"" ++ many stringchar ++ a "\"" >>
        (fun ((_,s),_) -> M_string (implode s)) in
  let hol_term_char =
      some (fun i -> i <> "`") in
  let hol_term = a "`" ++ many hol_term_char ++ a "`" >>
        (fun ((_,s),_) -> M_hol_term (implode s)) in
  let nonendcomment = (some_look (fun (h1,h2) -> h1 <> "*" or h2 <> ")")) in  (* comment nesting unrecognized *)
  let comment = a "(" ++ (a "*") ++ many nonendcomment ++ a "*" ++ a ")" 
    >> (fun _ -> M_comment) in
  let semi = a ";" >> (fun _ -> M_semicolon) in
  let textchar = some (fun i -> not (mem i (explode " %\t\n;()[]`\""))) in
  let text = atleast 1 (textchar) >> (fun s -> M_text (implode s)) in
  let numerical =  (some (fun i -> (mem i (explode "0123456789")))) in
  let asm = a "_" ++ atleast 1 numerical >> (fun (_,s) -> M_asm (int_of_string (implode s))) in
  let local = a "_" ++ atleast 1 (textchar) >> (fun (_,s) -> M_local (implode s)) in
  let query = a "?" ++ atleast 1 (textchar) >> (fun (_,s) -> M_query (implode s)) in
  let lparen = a "(" >> (fun _ -> M_lparen) in
  let rparen = a ")" >> (fun _ -> M_rparen) in
  let lbracket = a "[" >> (fun _ -> M_lbracket) in
  let rbracket = a "]" >> (fun _ -> M_rbracket) in
  let menv = atleast 1 (a "%") >> (fun s -> M_env (List.length s)) in
  let white = atleast 1 (some isspace) >> (fun s -> M_white (implode s)) in
    many (some isspace) ++ 
    many(comment || string || hol_term || semi || menv || lparen || rparen ||
	   lbracket || rbracket || asm || query || local || text || white) ;;

let rec strip_space = function
  | M_comment :: xs -> strip_space xs
  | M_white _ :: xs -> strip_space xs
  | M_semicolon :: xs -> strip_space xs
  | xs -> xs;;
  
let end_strip_space = List.rev o strip_space o List.rev o strip_space;; 

(*

let test1 = " (* note *) _t _44 __33 `1 /\\ [3] (* 42` (* hi *) ; [lade] da(%% (\"quote\";))  then (* c *) \t\n ";;
let test2 = " (* hi *) (*  (* hi again *)  *) \"quote\" `&1 + &1`;; (* there *) ;; ";;
(end_strip_space o snd o fst o m_lex o explode) test1;;
implode;;
many (some isspace);;
test1;;
unabbrev test1;;

*)




(*
let unabbrev_thm s = 
  let tg = String.sub s 0 1 in
  let item = int_of_string (String.sub s 1 (String.length s - 1)) in
    retrieve_search tg item;;
*)

let unabbrev_token = function
  | M_comment -> ""
  | M_string s -> "\""^s^"\""
  | M_hol_term s -> "`"^s^"`"
  | M_semicolon -> ";"
  | M_white s -> " "
  | M_text s -> unabbrev_string s
  | M_lparen -> "("
  | M_rparen -> ")"
  | M_lbracket -> "["
  | M_rbracket -> "]"
  | M_query s -> if (s.[0]='-') then expand_suggest (String.sub s 1 (String.length s - 1)) 
    else expand_thm s
  | M_env level -> if (level <=1) then " env w" else " envl w"
  | M_local s -> ("loc_"^s)
  | M_asm i -> ("asm_"^(string_of_int i));;

let which_asms  = mapfilter (function | M_asm i -> i | _ -> failwith "");;

let has_env = can (Lib.find (function M_env _ -> true | _ -> false));;


let really_expand s  = 
  let ((_,r),rest) = m_lex (explode s) in
  let _ = (rest=[]) or (failwith ("unparsed data : " ^ (implode rest))) in
  let r = end_strip_space r in
  let rs = map unabbrev_token r in
  let u =   unsplit "" I rs in
  let which = setify( which_asms r) in
  let gets = map (fun i ->Printf.sprintf " let asm_%d = snd(List.nth (List.rev asl) %d ) in " i i) which in
  let v = unsplit "" I gets in
  let envA,envB = if (has_env r) or (List.length which > 0) then 
    "GOAL_TERM (fun w -> (","))" else "","" in
    (envA^v^u^envB);;


(*
let escape s = 
  let ss = Str.split (Str.regexp "\"") s in
  let s = unsplit "\\\"" I ss in
  let ss = Str.split (Str.regexp "\\ ") s in
  let s = unsplit "\\\\ " I ss in
    s;;
*)

let p() = 
  let history = 5 in
  let _ = print_string (string_of_proof_k history ()) in
  if ((!current_goalstack=[])) then print_string "There is no current goal." 
  else 
    let (_,gl,_) = hd !current_goalstack in
    let ns = follow_your_nose_string_list() in
      if (gl = []) then print_string "\nNo subgoal"
      else  
	(Print_types.print_goal_var_overload() ; 
	 print_goalstack (!current_goalstack);
	 print_string ("\n >>>last step: "^ (string_of_proof_k 1 ()) ^ "\n");
	 print_string (" >>>total: "^(string_of_int (length gl)) ^ "\n");
	 if not(ns="") then print_string ("Follow your nose: "^ns)
	);;

(*
let eval_tactic_abbrev s = 
    try(
      let i = String.index s ',' in
      let pre = String.sub s 0 i in
      let post = String.sub s (i+1) (String.length s - (i+1)) in
	((unabbrev_tactic pre)^" "^post) 
    )
    with _ -> s in
 (* let _ = print_string (String.escaped expand_s) in *)
  let _ = eval_tactic (expand_s) in
    p();;
*)

let eval_tactic_abbrev2 s = 
  let sexp = really_expand s in
  let _ = report sexp in
  let _ = eval_tactic (sexp) in
   p();;

let blank_line = Str.regexp ("^ *$");;

let eval_tactic_lines s = 
  let ss = Str.split (Str.regexp "\n") s in
  let one_line s1 = 
    let sepx = try (really_expand s1) with _ -> (failwith "expansion error : "^s1) in
      if (Str.string_match blank_line sepx 0) then ()
      else 
	try (Pervasives.ignore(eval_tactic sepx)) 
	with _ -> failwith ("tactic failure : "^s1^" >>> "^sepx) in
  let _ = do_list one_line ss in
    p();;
(* emacs: hol-light-tactic-replay  "\C-c\C-r" *)

let e_abbrev = eval_tactic_abbrev2;;

let g = eval_goal;;

let b() = 
  let _ = eval_back() in p();;

let bb k = 
  let _ = map eval_back (replicate () k) in p();;

let back_to s = 
  let r = List.rev (strs_of_proof_records 0 0 [] !proof_record) in
  let re = Str.regexp_case_fold (".*"^s) in
  let searcher a = Str.string_match re a 0 in
  let z = find searcher r in 
  let _ = report z in
  let i = index z r in
   bb i;;

(*
let directive_abbreviations= ref[
  ("-b",eval_back);
  ("-?",fun () ->
     let s = map snd tactic_counts in
     let s1 = unsplit ": " 
];;
*)

(* EMACS BINDINGS:
see hol-light-mode.el

eval_tactic_lines -> hol-light-tactic-replay  "\C-c\C-r" 
(local-set-key "\C-ct" 'hol-light-goal-types)
(local-set-key "\C-c\C-y" 'hol-light-type-region)
 (local-set-key "\C-cr" 'hol-light-eval-region)

*)



end;;