(* ========================================================================== *) (* 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("",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("",_),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 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("",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;;