text_formalization/usr/thales/searching.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Author: Thomas C. Hales                                                    *)
   4 (* Date: 2011-06-18                                                           *)
   5 (* ========================================================================== *)
   6
   7
   8
   9 #load "str.cma";;
  10
  11 flyspeck_needs "usr/thales/hales_tactic.hl";;
  12
  13 module Searching = struct
  14
  15   open Hales_tactic;;
  16
  17
  18 (*
  19
  20 ? forces interpretation as a theorem.
  21 ?-n follows suggestion n.
  22 %`x` performs type matching
  23 %%[`x`;`y`] performs type matching.
  24
  25 *)
  26
  27 (*
  28 TODO:
  29  -Combine different search mechanisms with the same return type.
  30  -Make a log of all searches, all bookmarked items, with context, for data mining purposes.
  31  -integrate suggest.
  32 *)
  33
  34
  35 (* quicksilver style search for name matching.
  36     ignore case and look for nonconsecutive letters. *)
  37
  38 let unsplit d f = function
  39   | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  40   | [] -> "";;
  41
  42 let match_sparse s u =
  43   let re = Str.regexp_case_fold (".*"^(unsplit ".*" I (   explode s))) in
  44     Str.string_match re u 0;;
  45
  46 let maxl0 xs = try (end_itlist max xs) with _ -> 0;;
  47
  48 (*
  49 let ignore = Pervasives.ignore;;
  50 *)
  51
  52 (* ========================================================================== *)
  53 (* TYPES *)
  54
  55
  56 let types_of = Print_types.print_term_types;;
  57 let type_of_thm = Print_types.print_thm_types;;
  58 let type_of_goal = Print_types.print_goal_types;;
  59 let goal_types = Print_types.print_goal_types;;
  60
  61
  62 (* ========================================================================== *)
  63 (* HELP                                              *)
  64
  65
  66 let hollight_dir =
  67   (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
  68
  69 (* let local_help_dir =   Filename.concat flyspeck_dir "../help";; *)
  70
  71 let local_help_dir = ".";;
  72
  73 let helpdirs = ref [
  74   local_help_dir;
  75   Filename.concat hollight_dir "Help"
  76  ];;
  77
  78 help_path := !helpdirs @ (!help_path);; (* hol-light help *)
  79
  80 let help_grep pat =
  81   let split =   Str.split (Str.regexp "\n") in
  82   let cmd s = process_to_string ("(cd "  ^s^  "; ls | grep -v '~' | sed 's/.doc$//g' | grep '" ^pat^ "')") in
  83   List.flatten (map ( split o cmd ) (!helpdirs));;
  84
  85 (*
  86 todo: if pat starts with regexp "-[a-z]+ " then it should be taken as a flags command.
  87 Also make help_grep_local a flag, say -l for local.
  88 *)
  89
  90 let help_flag flag pat  =
  91   let constant_of_regexp ss =
  92     let re = Str.regexp_case_fold (".*"^ss) in
  93     let c = map fst (constants()) in
  94       filter (fun s -> Str.string_match re s 0) c in
  95   let help_grep_local pat =
  96     let backup = !helpdirs in
  97     let _ = helpdirs := [local_help_dir] in
  98     let out = help_grep pat in
  99     let _ = helpdirs := backup in
 100       out in
 101   let split =   Str.split (Str.regexp "\n") in
 102   let grep_s s = Printf.sprintf "(cd %s; ls | sed 's/.doc$//g' | grep -i '%s')" s pat in
 103   let cmd s = process_to_string (grep_s s) in
 104     match flag with
 105       | 'i' ->  List.flatten (map ( split o cmd ) (!helpdirs))
 106       | 'd' -> constant_of_regexp pat
 107       | 'l' -> help_grep_local pat
 108       | 'g' -> help_grep pat
 109       | _ -> [" 'd' search constants";"'g' help_grep"; "'i' ignore case"; "'l' help_grep local dir"];;
 110
 111
 112 (*
 113 Example:
 114 help_grep "ASM.*REWRITE";;
 115 help_grep "^ASM_";;
 116 help_grep "help";;
 117 help_grep "RULE";;
 118 help_grep "ARITH";;
 119 help_grep "_TAC$";;
 120 List.length (help_grep ".*");;
 121
 122 help_flag '?' "";;
 123
 124 help_flag 'd'  ".*contin";;
 125 help_flag 'd'  ".*integr";;
 126 help_flag 'd'  ".*auchy";;
 127 help_flag 'd'  "at.*[ng]$";;
 128 help_flag 'd' "cos" ;;
 129
 130 *)
 131
 132
 133
 134 (* ========================================================================== *)
 135 (* SEARCH *)
 136
 137 let def s = mk_comb(mk_var("<match constant def>",W mk_fun_ty aty),
 138                      mk_var(s,aty));;
 139
 140 let searches = ref[];;
 141
 142 let searcht n pat =
 143   let _ = searches := (n,pat)::!searches in
 144   let def_of_regexp ss =
 145     let c = help_flag 'd'  ss in
 146     let strip d =   (fst o dest_const o fst o dest_eq o concl) d in
 147     let def_assoc = map (fun t -> (strip t,t)) (definitions()) in
 148       map (fun s -> (s,assoc s def_assoc)) c in
 149   let raw = match pat with
 150     | Comb(Var("<match constant def>",_),Var(ss,_))::_ -> def_of_regexp ss
 151     | _ -> search pat in
 152   let m = min n (List.length raw) in
 153   let s = sortlength_thml raw in
 154   let r = fst (chop_list m s) in
 155   let z = zip (0--(List.length r - 1)) r in
 156     z;;
 157
 158 let searchl ls pat = search_thml (term_match [])  pat ls;;
 159
 160 (* added Oct 2012 *)
 161
 162 let save_searc  = ref [];;
 163
 164 let searc c n tl =
 165   let u = snd(List.nth (searcht (n+1) tl) n) in
 166   let _ = (save_searc := (c,u)::!save_searc) in
 167      u;;
 168
 169 (* tactics that search assumption list for match.
 170    Deprecated. Replaced with FIRST_X_ASSUM_ST *)
 171
 172 (*
 173 let SEARCH_THEN pat ttac (asl,w) =
 174   let thl = map snd (searchl asl pat) in
 175     ttac thl (asl,w);;
 176
 177 let FIRST_SEARCH_THEN pat ttac (asl,w) =
 178   let thl = map snd (searchl asl pat) in
 179     ttac (hd thl) (asl,w);;
 180 *)
 181
 182 let searchn n f s = snd(List.nth (searcht (n+1) f) n);;  (* used for write-up of search results *)
 183
 184 (*
 185 Example: searcht 5 [def "cos"];;
 186 searcht 5 [def "mul"];;
 187 *)
 188
 189 let research m =
 190   let (n,pat) = hd (!searches) in
 191     searcht (m) pat;;
 192
 193 let search_results = ref [];;
 194
 195 (* add stored searches to list *)
 196 let augment_search_results ss =
 197   let get s = try (Lib.assoc s !theorems) with _ -> failwith s in
 198   let cs = map (fun (_,s,_,_) -> s) !search_results in
 199   let ss = Lib.subtract ss cs in
 200   let ns = List.length cs in
 201   let ss = Lib.zip (ns -- (ns+List.length ss - 1)) ss in
 202   let ss =   map (fun (i,s) -> (i,s,get s,[])) ss in
 203     !search_results @ ss;;
 204
 205 let mark m =
 206   let (n,pat) = hd (!searches) in
 207   let (s,th) =   snd(List.nth (searcht (1 + min n m) pat) m)  in
 208   let v = (List.length !search_results,s,th,pat) in
 209   let _ = search_results := v::(!search_results) in
 210     v;;
 211
 212 let result n pat =
 213   let ls = map (fun (_,s,th,_) -> (s,th)) !search_results in
 214   let a = zip ls !search_results in
 215   let sl = if pat = [] then ls else searchl ls pat in
 216   let n' = min n (List.length sl) in
 217   let ts =   fst(chop_list n' (sl)) in
 218     map (fun t -> assoc t a) ts;;
 219
 220 let results pat =
 221   let n = List.length (!search_results) in
 222     result n pat;;
 223
 224 let retrieve_search_number n =
 225   let (_,s,_,_) = Lib.find (fun (c,_,_,_) -> (c=n)) !search_results in
 226     s;;
 227
 228 (*
 229
 230
 231 let (srch,more,less,retrieve_search)  =
 232   let allsearch = ref [] in
 233
 234   let tags = explode "abcdefghijklmnopqrstuvwxyz" in
 235   let tag_num = ref 0 in
 236
 237   let update () = (tag_num := (!tag_num + 1) mod (List.length tags)) in
 238
 239   let current_search = ref [] in
 240   let nextdisplayed = ref 0 in
 241
 242   let ziptg tg a xs =
 243     let z = zip (a--(List.length xs - 1 + a)) xs in
 244       map (fun (i,x) -> (tg^(string_of_int i),x)) z  in
 245
 246   let sub_range tg a b xs =
 247     let b' = min b (List.length xs - 1) in
 248     let _ = (a <= b') or failwith "bad range" in
 249     let _ = (0 <= a) or failwith "bad neg index" in
 250     let bs = fst (chop_list (b'+1) xs) in
 251      ziptg tg a (snd (chop_list a bs)) in
 252
 253   let more () =
 254     let tg = List.nth tags (!tag_num) in
 255     let sr = sub_range tg (!nextdisplayed) (!nextdisplayed + 5) (!current_search) in
 256     let _ = (nextdisplayed := 5 + !nextdisplayed) in
 257       sr  in
 258
 259   let less () =
 260     let _ = (nextdisplayed := max 0 (!nextdisplayed - 10)) in
 261       more()  in
 262
 263   let srch pat =
 264     let raw = search pat in
 265     let _ = update() in
 266     let _ = (nextdisplayed := 0) in
 267     let _ = current_search := sortlength_thml raw in
 268     let tg = List.nth tags (!tag_num) in
 269     let _ = (allsearch := (tg,!current_search)   :: !allsearch) in
 270       more() in
 271
 272   let retrieve_search tag item =
 273     fst ( List.nth (Hol_pervasives.assoc tag !allsearch)  item) in
 274
 275     (srch,more,less,retrieve_search);;
 276 *)
 277
 278 (* ========================================================================== *)
 279 (* STATS of WORD COUNTS, indexing all words in  HOL LIGHT and FLYSPECK  *)
 280
 281
 282 let wc_tmpfile = Filename.temp_file "tmp_" ".txt";;
 283
 284 let int_tmpfile =
 285   let ss1 = process_to_string ("ls "^flyspeck_dir^"/*/*.hl") in
 286   let ss2 = Str.split (Str.regexp "\n") ss1 in
 287   let ss1 = process_to_string ("ls "^hollight_dir^"/*/*.ml") in
 288   let ss2 =  Str.split (Str.regexp "\n") ss1 @ ss2 in
 289   let tmpfile =  wc_tmpfile in
 290   let _ =     Sys.command("touch "^tmpfile) in
 291   let _ =     map (fun s -> Sys.command("cat "^ s^ " >> " ^ tmpfile)) ss2 in
 292     ();;
 293
 294 let word_counts() =
 295   let sout = Str.split (Str.regexp "\n")
 296     (process_to_string("cat "^wc_tmpfile^" | tr -C 'A-Z:a-z0-9_' '\n' | sort | uniq -c | sed 's/^ *//'")) in
 297   let sout1 = map (Str.split (Str.regexp " ")) sout in
 298   let sout2 = filter (fun t -> List.length t = 2) sout1 in
 299   let sout3 = map (function | [a;b]-> (b,int_of_string a) | _ -> ("?",0)) sout2 in
 300     sout3;;
 301
 302 let word_count_list = word_counts();;
 303
 304 (* stats of the word immediately following another word.
 305    This can be useful in determining, for example, which theorems are used
 306    with MATCH_MP_TAC.  Or which tactics are used with REPEAT. *)
 307
 308 let word_successor_counts word_successor =
 309   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/^ *//'"
 310     word_successor wc_tmpfile word_successor in
 311   let sout = Str.split (Str.regexp "\n")
 312     (process_to_string(sed_pipe )) in
 313   let sout1 = map (Str.split (Str.regexp " ")) sout in
 314   let sout2 = filter (fun t -> List.length t = 2) sout1 in
 315   let sout3 = map (function | [a;b]-> (b,int_of_string a) | _ -> ("?",0)) sout2 in
 316     sort (fun (_,a) (_,b) -> (a > b)) sout3;;
 317
 318 (* inaccurate because constants and theorems with the same name are overcounted *)
 319
 320 let thm_counts =
 321   let alpha_thm = sort (<) (map fst !theorems) in
 322   let rec build buff ats bts = match (ats,bts) with
 323     | ([],_) -> buff
 324     | (_,[]) -> buff
 325     | (a::atss,(b,n)::btss) -> if (a=b) then build ((b,n)::buff) atss btss
 326       else if (a>b) then build buff ats btss else build buff atss bts in
 327   sort (fun (_,a) (_,b) -> (a > b)) (build [] (alpha_thm) word_count_list);;
 328
 329 let quasi_tactic_list =
 330   let tactic_wordlist =
 331     ["REPEAT";"POP_ASSUM";
 332      "FIRST_X_ASSUM";"FIRST_ASSUM";
 333      "fun";"REAL_ARITH";"ARITH_RULE";"TAUT"] in
 334   let tactic_list =  (help_grep "TAC$") in
 335   let then_list =  (help_grep "THEN") in
 336     tactic_wordlist @ tactic_list @ then_list;;
 337
 338 let tactic_counts = sort (fun (_,a) (_,b) -> (a > b))
 339   (filter (fun (a,_) -> mem a  (quasi_tactic_list)) word_count_list);;
 340
 341
 342 (* ========================================================================== *)
 343 (* DEPTH FUNCTIONS *)
 344 (* each constant is defined in terms of other constants.
 345    The depth of a constant is the length of its longest chain down to the primitives *)
 346
 347 (* SLOW BUT POTENTIALLY USEFUL. START HERE.
 348
 349
 350 let nub = Parse_ineq.nub;;
 351
 352 let rec c_of buf = function
 353   | Const _ as t  -> nub (t:: buf)
 354   | Comb (r,s)  -> c_of (c_of buf r) s
 355   | Abs (x,t) -> c_of buf t
 356   | _ -> nub buf;;
 357
 358 let def_assoc =
 359   let r =  (map (dest_eq o concl) (definitions())) in
 360   let s = fst o dest_const in
 361     map (fun (x,y) -> ( s x,nub (map s (c_of [] y)))) r;;
 362
 363 let stm_depth =
 364   let cache = ref [] in
 365   let rec s_depth t =
 366     try (assoc t !cache)
 367     with _ ->
 368       let rs = try (assoc t def_assoc)
 369       with _ -> [] in
 370       let _ = not(mem t rs) or failwith t in
 371       let u = 1 + maxl0 (map s_depth rs) in
 372       let _ = cache:= (t,u)::!cache in
 373         u in
 374     s_depth;;
 375
 376 let sdef_assoc = map (fun (t,ul) -> ((t,stm_depth t),(map (fun u -> (u,stm_depth u)) ul)))
 377   def_assoc;;
 378
 379 let tm_depth t =
 380   let c = map (fst o dest_const )(c_of [] t) in
 381   let u = map (fun x -> (x,stm_depth x)) c in
 382   let s = nub (sort (fun (_,a) (_,b) -> a > b) u) in
 383     s;;
 384
 385 (* ball park distance of goal *)
 386
 387 let rec rec_hash n acc = function
 388   |  [] -> acc
 389   |  (a,_)::b -> if (n<=0) then acc else rec_hash (n-1) (Hashtbl.hash a ::acc) b;;
 390
 391 let hash_depths = sort (<) o (rec_hash 3 []);;
 392
 393 let rec sorted_meet k al bl = if (k<1) then true else  (* look for at least k matches *)
 394   (match bl with
 395   | [] -> false
 396   | b::bl' -> match al with
 397       | [] -> false
 398       | a::al' -> if (a = b) then
 399           (sorted_meet (k-1) al' bl')
 400         else
 401           (if (a<b) then sorted_meet k al' bl else sorted_meet k al bl'));;
 402
 403 let strip_imp = striplist dest_imp;;
 404
 405 let preprocess_theorems thml =
 406   let get_tm_depth = (tm_depth o last o strip_imp o snd o strip_forall o concl ) in
 407   let de = function | [] -> 0 | ((_,d)::_) -> d in
 408   let data r = (de r,hash_depths r) in
 409   let thl = map (fun (s,t) -> ((data o get_tm_depth) t,s,t) ) thml in
 410     thl;;
 411
 412 let depth_encoded_theorems = preprocess_theorems (!theorems);;
 413
 414 let rec ballpark i j  thml (d,hd) =
 415   if (List.length thml < 80) then thml else
 416     let k = max i j in
 417     let (thml',i',j') =
 418       if (k=i) then (filter (fun ((d',_),_,_)-> abs(d-d') < 1+k) thml,i-1,j) else
 419         (filter (fun ((_,hd'),_,_) -> (sorted_meet (3-k) hd hd')) thml,i,j-1) in
 420       if (List.length thml' < 20) then thml else ballpark i' j' thml' (d,hd);;
 421
 422 let  ballpark_theorems (_,w) =
 423   let thml = depth_encoded_theorems in
 424   let get_tm_depth = (tm_depth o last o strip_imp o snd o strip_forall ) in
 425   let de = function | [] -> 0 | ((_,d)::_) -> d in
 426   let data r = (de r,hash_depths r) in
 427     map (fun (_,s,t)->(s,t))  (ballpark 3 3 thml (data (get_tm_depth w)));;
 428
 429
 430 (* fails on depth 0 *)
 431
 432 let drop_depth_once ul =
 433   List.flatten (map  (fun u -> assoc u sdef_assoc) ul);;
 434
 435 let rec drop_depth_to d ul =
 436   let (hi,lo) = partition (fun (_,h) -> (h>d)) ul in
 437     if hi = [] then ul else
 438       let hi' = drop_depth_once hi in
 439         (nub ((drop_depth_to d hi') @ lo));;
 440
 441 (* metric symbol distance, an estimate of the distance between two lists of symbols.
 442     dsofar = distance so far.
 443     common = list of symbols and their shallowings that the two lists have already in common.
 444     depth_weight is a heuristic weighting: matches should increase distance less than mismatches.
 445 *)
 446
 447 let rec msd dsofar common  al bl =
 448   if (al=[]) && (bl=[]) then dsofar else
 449     let depth_weight = 10 in
 450     let d = maxl0 (map snd (al @ bl)) in
 451     let c =  ( drop_depth_to d common) @ (intersect al  bl) in
 452     let al' = subtract al c in
 453     let bl' = subtract bl c in
 454     let dsofar' = dsofar +.  float_of_int( List.length ((intersect al  c) @ (intersect bl  c)) +
 455                                              depth_weight *  List.length (al' @ bl')) in
 456       if (d <=1) then dsofar'  else
 457         let al'' = drop_depth_to (d-1) al' in
 458         let bl'' = drop_depth_to (d-1) bl' in
 459           msd dsofar' c al'' bl'';;
 460
 461 let metric_symbol_distance bl cl =
 462   let tt tl = List.flatten (map tm_depth tl) in
 463   if (List.length bl = 1)&&(List.length cl=1)&& (aconv (hd bl) (hd cl)) then 0.0
 464   else msd 10.0 [] (tt bl) (tt cl);;
 465
 466 let nearest_thm_to_goal (asl,w) =
 467   let tt tl = List.flatten (map (tm_depth o concl) tl) in
 468   let common = tt (map snd asl) in
 469   let thl = map (fun (s,t) -> ((tm_depth o snd o strip_forall o concl )t,s,t) ) (!theorems) in
 470   let r = map (fun (tl,s,t) -> (tl,s,t,msd 0.0 common (tm_depth w) tl)) thl in
 471     (sort (<) r);;
 472
 473
 474 let thm_depth = tm_depth o concl;;
 475
 476 let search_depth  =
 477   let dthm = map (fun (s,t) -> (maxl0 (map snd(thm_depth t)),(s,t))) !theorems in
 478   let m tml = maxl0 (map snd (List.flatten (map (tm_depth) tml))) in
 479   let fthm tml = map snd (filter (fun (x,(_,_)) -> (x <=m tml)) dthm) in
 480     fun tml -> searchl (fthm tml) tml;;
 481
 482 END SLOW BUT POTENTIALLY USEFUL
 483 *)
 484
 485 (* ========================================================================== *)
 486 (* EVAL AND PROOF STACK *)
 487
 488 (*
 489 eval_command comes from
 490
 491 http://solaria.dimino.org/cgi-bin/darcsweb.cgi?r=peps;a=headblob;f=/src/core/peps_top.ml
 492 License: BSD3
 493
 494 If the expression is syntactically correct
 495 and the evaluation raises an exception, then the return value is true.
 496 *)
 497
 498
 499 let eval_command ?(silent=false) command =
 500    let buffer = Buffer.create 512 in
 501    let pp = Format.formatter_of_buffer buffer in
 502    Format.pp_set_margin pp max_int;
 503    try
 504      let _ =
 505        Toploop.execute_phrase (not silent) pp
 506          (!Toploop.parse_toplevel_phrase (Lexing.from_string (command ^ ";;")))
 507      in
 508      (true, Buffer.contents buffer)
 509    with exn ->
 510      let save = !Toploop.parse_use_file in
 511      Toploop.parse_use_file := (fun _ -> raise exn);
 512      Pervasives.ignore (Toploop.use_silently pp "/dev/null");
 513      Toploop.parse_use_file := save;
 514      (false,  Buffer.contents buffer);;
 515
 516 (* eval_command ~silent:false "g `x=y`";; *)
 517
 518 type proof_record = Tax of string*int*tactic | Bax | Gax of term*string;;
 519
 520 let proof_record  =ref [];;
 521 let tactic_cache = ref (fun () -> ALL_TAC);;
 522
 523 (* we evaluate the tactic outside eval_command, so that we can catch exceptions *)
 524
 525 let eval_tactic  =
 526   fun s ->
 527     let (b,r) = eval_command ~silent:false
 528       ("tactic_cache := (fun () -> ("^s^"));;") in
 529     let _ = b or (print_string (r^"\n"^s^"\n"); failwith "bad input string") in
 530     let t= (!tactic_cache)() in
 531     let (_,gs,_) ::_ = !current_goalstack in
 532     let i = List.length gs in
 533     let v = Hol_pervasives.e(t) in
 534     let _ = proof_record := Tax (s,i,t)::!proof_record in
 535       v;;
 536
 537 (*
 538 let string_of_frees t =
 539   let u =  (map (fst o dest_var) o frees) t in
 540     (unsplit " " I) u;;
 541 *)
 542
 543 let eval_goal t =
 544   let _ = print_goalstack (Hol_pervasives.g(t));
 545     proof_record := Gax (t,process_to_string "date")::!proof_record;
 546     warn (has_stv t)  "?type in goal" in
 547     ();;
 548
 549 let eval_back () =
 550   let _ = proof_record := Bax::!proof_record in Hol_pervasives.b();;
 551
 552 (*
 553 eval_goal `1 + 1 = 2`;;
 554 eval_tactic "REPEAT STRIP_TAC";;
 555 eval_back();;
 556 eval_tactic "ARITH_TAC";;
 557 eval_tactic "REWRITE_TAC[TRUTH]";;
 558 *)
 559
 560 let string_starts_with u s =
 561   (String.length u <= String.length s) && (u = String.sub s 0 (String.length u));;
 562
 563 let rec strs_of_proof_records ind skip buf  =
 564   let by t s = if t && (not (string_starts_with "BY" s)) then "BY("^s^")" else s in
 565     function
 566         [] -> buf
 567       | Gax _ :: xs -> buf
 568       | Tax (s,i,_) :: xs ->
 569           let indent = String.make (2*i) ' ' in
 570             if (skip=0) then strs_of_proof_records i skip ((indent^(by (i>ind) s))::buf) xs
 571             else strs_of_proof_records ind (skip-1) buf xs
 572       | Bax :: xs -> strs_of_proof_records ind (skip+1) buf xs;;
 573
 574 let string_of_proof () =
 575   let ss = strs_of_proof_records 0 0 [] !proof_record in
 576     "\n[\n"^unsplit ";\n" I (ss) ^"\n]\n";;
 577
 578 let print_proof () =
 579   print_string (string_of_proof());;
 580
 581 let string_of_proof_k k () =
 582   let ss = strs_of_proof_records 0 0 [] !proof_record in
 583   let k' = min k (List.length ss) in
 584   let ss' = (fst(chop_list k' (List.rev ss))) in
 585     if (List.length ss' = 0) then ""
 586     else if (List.length ss' = 1) then hd(ss')
 587     else "\n[ ... most recent steps ...\n"^unsplit ";\n" I (List.rev ss') ^"\n]\n";;
 588
 589 let rec split_proof_record acc cur = function
 590   | [] -> if (List.length cur > 0) then acc @[cur] else acc
 591   | Gax (_,_) as a :: xs ->
 592       let acc' =  acc @ [cur @ [a]]  in
 593         split_proof_record acc' [] xs
 594   | a :: xs -> split_proof_record acc (cur @ [a]) xs;;
 595
 596 let gax() =
 597   let u = split_proof_record [] [] (!proof_record) in
 598   let j = zip u (0-- (List.length u - 1)) in
 599   let k = map (fun (u,z) -> (z,List.length u,last u)) j in
 600      k;;
 601
 602
 603 split_proof_record [] [] (!proof_record);;
 604
 605 (*
 606 print_string (string_of_proof());;
 607 *)
 608
 609
 610 (* ========================================================================== *)
 611 (* SUGGEST TACTIC                                              *)
 612
 613
 614
 615 (* term matching without higher order matches *)
 616
 617
 618 let term_match_no_ho pat u =
 619   let (_,b,c) = (term_match[] pat u) in
 620   let v = instantiate ([],b,c) pat in
 621     aconv v u  or failwith "no match";;
 622
 623 let match_g_no_ho pat (_,w) = not(search_thml term_match_no_ho pat [("", ASSUME w)] = []);;
 624
 625 let match_g pat (_,w) = not(search_thml (term_match[]) pat [("", ASSUME w)] = []);;
 626
 627 let match_asm pat (asl,_) = not(search_thml term_match_no_ho pat asl = []);;
 628
 629 (* new version, july 2012 *)
 630
 631 let noses = ref [];;
 632
 633 let add_your_nose x = (noses := x::!noses);;
 634
 635 let follow_your_nose_string() =
 636   let aslw = top_realgoal() in
 637   let n =
 638     try
 639       let (_,_,a) = find (fun (p,_,_) -> p aslw) !noses
 640       in a
 641     with Failure _ -> "" in
 642     n;;
 643
 644 let fyn () =
 645   let aslw = top_realgoal() in
 646   let (_,t,_) = find (fun (p,_,_) -> p aslw)  !noses in
 647     t;;
 648
 649 let follow_your_nose_string_list() =
 650   let aslw = top_realgoal() in
 651   let m = filter (fun (p,_,_) -> p aslw) !noses in
 652   let m2 = map (fun ((_,_,a),b) -> ("{"^string_of_int b ^":"^a^"}")) (zip m (0--((List.length m) -1))) in
 653     Flyspeck_lib.join_comma m2;;
 654
 655 let fynlist k =
 656   let aslw = top_realgoal() in
 657   let m = filter (fun (p,_,_) -> p aslw) !noses in
 658   let l = List.length m in
 659   let _ = k < l or failwith ("fyn length = "^string_of_int k ^ " "^string_of_int l) in
 660   let (_,t,_) = List.nth m k in
 661    t;;
 662
 663
 664 (* new version, march 2012 *)
 665
 666 let nub = Parse_ineq.nub;;
 667
 668
 669 let rec c_of buf = function
 670   | Const _ as t  -> nub (t:: buf)
 671   | Comb (r,s)  -> c_of (c_of buf r) s
 672   | Abs (x,t) -> c_of buf t
 673   | _ -> nub buf;;
 674
 675 let rewrite_tags = ref [];;
 676 let remove_rewrite_tag s =
 677   rewrite_tags:= filter (fun (_,_,s',_) -> not (s =s')) !rewrite_tags;;
 678
 679 let st_of tm = map (fst o dest_const) (c_of [] tm);;
 680 let add_rewrite_tag (s,th) =
 681   let thl = mk_rewrites true th [] in
 682   let tml = map concl thl in
 683   let wd tm = if (is_imp ( tm)) then (snd(dest_imp( tm))) else tm in
 684   let tml = map (fst o dest_eq  o wd) tml in
 685   let stl = map st_of tml in
 686   let zl = map (fun (a,b)-> (a,b,s,th)) (zip tml stl) in
 687   let _ =     rewrite_tags := zl @ !rewrite_tags in
 688     ();;
 689
 690 let add_rewrite_stag s =
 691   let _ = (can (assoc s) !theorems) or failwith (s ^ " not found ") in
 692   add_rewrite_tag (s,assoc s !theorems);;
 693
 694 let refresh_rewrite_stag s =
 695   let _ = remove_rewrite_tag s in
 696     add_rewrite_stag s;;
 697
 698 let refresh() =
 699   let _ = map (fun (_,s,_,_) -> refresh_rewrite_stag s) !search_results in
 700     ();;
 701
 702 let write m =
 703   let u = mark m in
 704   let (_,s,_,_) = u in
 705   let _ =     refresh_rewrite_stag s in
 706     u;;
 707
 708 let lookup_rewrite_tags (asl,w) =
 709   let sw = st_of w in
 710   let f1 = filter (fun (_,sl,_,_) -> (subset sl sw)) !rewrite_tags in
 711   let ml = filter (fun (pat,_,_,_) -> match_g [pat] (asl,w)) f1 in
 712     ml;;
 713
 714 let rewrite_suggest() =
 715   let rawl =  lookup_rewrite_tags (top_realgoal()) in
 716     zip (0--(List.length rawl - 1)) (map (fun (_,_,s,th) -> (s,th)) rawl);;
 717
 718 let suggest = rewrite_suggest;;
 719
 720 (* let assum t = mk_comb(mk_var("<assum>",W mk_fun_ty (type_of t)),t);; *)
 721
 722 (*
 723
 724 trigger pattern;
 725 English text;
 726 prompt;
 727 tactic;
 728
 729 *)
 730
 731 let tactic_patterns = ref [];;
 732
 733 let add_tactic_pattern t = (tactic_patterns := t::!tactic_patterns);;
 734
 735 let tactic_suggest _ =
 736   let s = filter (fun (a,_,_,_) -> a (top_realgoal())) !tactic_patterns in
 737   zip (0-- (List.length s  -1) ) s;;
 738
 739 let print_suggest sg =
 740   let print_one (i,(_,_,s,_)) = (print_int i; print_string (": "^s)) in
 741   map (print_one) sg;;
 742
 743 (*
 744 let s () = let sg = suggest() in Pervasives.ignore(print_suggest sg);;
 745 *)
 746
 747 let expand_suggest s =
 748   let sg = tactic_suggest() in
 749   let n = (int_of_string s) in
 750   let r = Lib.assoc n sg in
 751     (fun (_,s,_,_) -> s) r;;
 752
 753 (*
 754 let eh n = let (_,(_,_,_,tac)) = List.nth (suggest()) n in e(tac());;
 755 *)
 756
 757 (* let follow n = let (_,(_,_,_,tac)) = List.nth (suggest()) n in tac();; *)
 758
 759 (*
 760 let rewrite_suggest = [
 761  ([`x IN {y}`],"IN_SING",IN_SING);
 762 ];;
 763
 764 let rewrites _ =
 765   let s = filter (fun (a,_,_) -> match_g a (top_realgoal())) rewrite_suggest in
 766     zip (0-- (List.length s  -1) ) s;;
 767 *)
 768
 769 (* ========================================================================== *)
 770 (* ABBREVIATIONS                                              *)
 771
 772 let matching_tactics  s =
 773   filter (match_sparse s) (map fst tactic_counts);;
 774
 775 let tactic_abbreviations = ref [];;
 776
 777 let abbrev u = (tactic_abbreviations:= (u::!tactic_abbreviations));;
 778
 779 let unabbrev s = (tactic_abbreviations:= (filter (fun (s',_) ->  (s <> s')) !tactic_abbreviations));;
 780
 781 let thm_abbreviations = ref[("elim","IN_ELIM_THM");("morgan","DE_MORGAN_THM")];;
 782
 783 let thm_abbrev s = (let _ = thm_abbreviations:= s::!thm_abbreviations in s);;
 784
 785 thm_abbrev ("empty","EMPTY");;
 786
 787 let expansive_thms   =
 788   let  full =  (map fst thm_counts) in
 789     fun op s ->
 790       let searches = map (fun (_,s,_,_) -> s) !search_results in
 791         op (match_sparse s) (searches @ full);;
 792
 793 (*
 794 ?n to get marked theorem n.
 795 ?abbrev to abbreviate.
 796 *)
 797
 798 let expand_thm  =
 799   let charset = (explode "abcdefghijklmnopqrstuvwxyz0123456789'_.") in
 800   let number s =
 801     let n = int_of_string s in
 802       retrieve_search_number n in
 803   let search_thm s =
 804     let c = s.[0] in
 805       fst(Hol_pervasives.assoc c (!save_searc)) in
 806   let abbreviable s = (subset (explode s) charset) in
 807   let unabbrev s =
 808     let _ = not(abbreviable s) or failwith "abbrev" in s in
 809   let exact_thm s = (Pervasives.ignore (Hol_pervasives.assoc s !theorems); s) in
 810   let assoct s = Hol_pervasives.assoc s !thm_abbreviations in
 811   let match_t = expansive_thms Lib.find in
 812    fun s->  tryfind (fun f -> f s) [unabbrev;search_thm;number;exact_thm;assoct;match_t;I];;
 813
 814 (*
 815 %`x` to expand types of term
 816 %%[`x`;`y`] to expand types of term list.
 817 *)
 818
 819 (* deprecated HASH: *)
 820
 821 (*
 822 let el_to_hash s i =
 823   let el_assoc = [
 824     ("u","HASH_UNDISCH_TAC");
 825     ("r","HASH_RULE_TAC");
 826     ("k","HASH_KILL_TAC");
 827     ("p","HASH_COPY_TAC");
 828     ("c","HASH_CHOOSE_TAC");
 829     ("x","HASH_X_CHOOSE_TAC");
 830     ("a","HASH_ASM_REWRITE_TAC")] in
 831   let tac = assoc s el_assoc in
 832   let h = el_hash i (top_realgoal()) in
 833     tac ^ " " ^ (string_of_int h);;
 834 *)
 835
 836 let el_to_hash s i = failwith "el_to_hash has been deprecated";;
 837
 838 let break_init init s =
 839   let l_init = String.length init  in
 840   let _ = (l_init <= String.length s) or failwith "length mismatch break_init" in
 841   let _ = (String.sub s 0 l_init = init) or failwith "mismatch break_init" in
 842     String.sub s (l_init) (String.length s - l_init);;
 843
 844 let unabbrev_string  =
 845   let charset = (explode "abcdefghijklmnopqrstuvwxyz0123456789'_/\\!?@") in
 846   let abbreviable s = (subset (explode s) charset) in
 847   let unabbrev s =
 848     let _ = not(abbreviable s) or failwith "abbrev" in s in
 849   let assoc_thm s = (Pervasives.ignore (Hol_pervasives.assoc s !theorems); s) in
 850   let assoct s = Hol_pervasives.assoc s !tactic_abbreviations in
 851   let assoc_sans_t s =
 852     let len = String.length s in
 853     let _ = (len > 1) or failwith "too short" in
 854     let _ = (s.[len-1]= 't') or failwith "final char t" in
 855       assoct (String.sub s 0 (len -1)) in
 856   let hash s =
 857     let rest = break_init "el" s in
 858     let c = String.sub rest 0 1 in
 859     let n = int_of_string (String.sub rest 1 (String.length rest - 1)) in
 860       el_to_hash c n in
 861   let tac s =
 862     let v = matching_tactics s in
 863       if (List.length v > 0) then hd v else s in
 864   let fynose s =
 865     if (s = "fyn") then fyn ()
 866     else
 867       let _ = String.length s = 4 or failwith "fynose" in
 868       let _ = "fyn" = String.sub s 0 3 or failwith "fynose2" in
 869       let k = int_of_string (String.sub s 3 1) in
 870         fynlist k in
 871   let deprecated_fynose s =
 872     let _ = (s = "fyn") or failwith "fynose" in fyn () in
 873    fun s->  tryfind (fun f -> f s) [unabbrev;assoc_thm;fynose;assoct;assoc_sans_t;hash;hash;tac;];;
 874
 875
 876
 877 (* ========================================================================== *)
 878 (* PARSING INPUT *)
 879
 880 type mtoken =
 881        | M_comment
 882        | M_string of string
 883        | M_hol_term of string
 884         | M_semicolon
 885         | M_white of string
 886         | M_text of string
 887         | M_query of string
 888         | M_lparen
 889         | M_rparen
 890         | M_lbracket
 891         | M_rbracket
 892        | M_env of int
 893             (* not implemented : *)
 894       | M_local of string
 895        | M_asm of int ;;
 896
 897 let some_look p =
 898   function
 899       [] -> raise Noparse
 900     | [_] -> raise Noparse
 901     | (h1::h2::t) -> if p (h1,h2) then (h1,h2::t) else raise Noparse;;
 902
 903 let rec m_lex  =
 904   let stringchar =
 905       some (fun i -> i <> "\"") in
 906   let string = a "\"" ++ many stringchar ++ a "\"" >>
 907         (fun ((_,s),_) -> M_string (implode s)) in
 908   let hol_term_char =
 909       some (fun i -> i <> "`") in
 910   let hol_term = a "`" ++ many hol_term_char ++ a "`" >>
 911         (fun ((_,s),_) -> M_hol_term (implode s)) in
 912   let nonendcomment = (some_look (fun (h1,h2) -> h1 <> "*" or h2 <> ")")) in  (* comment nesting unrecognized *)
 913   let comment = a "(" ++ (a "*") ++ many nonendcomment ++ a "*" ++ a ")"
 914     >> (fun _ -> M_comment) in
 915   let semi = a ";" >> (fun _ -> M_semicolon) in
 916   let textchar = some (fun i -> not (mem i (explode " %\t\n;()[]`\""))) in
 917   let text = atleast 1 (textchar) >> (fun s -> M_text (implode s)) in
 918   let numerical =  (some (fun i -> (mem i (explode "0123456789")))) in
 919   let asm = a "_" ++ atleast 1 numerical >> (fun (_,s) -> M_asm (int_of_string (implode s))) in
 920   let local = a "_" ++ atleast 1 (textchar) >> (fun (_,s) -> M_local (implode s)) in
 921   let query = a "?" ++ atleast 1 (textchar) >> (fun (_,s) -> M_query (implode s)) in
 922   let lparen = a "(" >> (fun _ -> M_lparen) in
 923   let rparen = a ")" >> (fun _ -> M_rparen) in
 924   let lbracket = a "[" >> (fun _ -> M_lbracket) in
 925   let rbracket = a "]" >> (fun _ -> M_rbracket) in
 926   let menv = atleast 1 (a "%") >> (fun s -> M_env (List.length s)) in
 927   let white = atleast 1 (some isspace) >> (fun s -> M_white (implode s)) in
 928     many (some isspace) ++
 929     many(comment || string || hol_term || semi || menv || lparen || rparen ||
 930            lbracket || rbracket || asm || query || local || text || white) ;;
 931
 932 let rec strip_space = function
 933   | M_comment :: xs -> strip_space xs
 934   | M_white _ :: xs -> strip_space xs
 935   | M_semicolon :: xs -> strip_space xs
 936   | xs -> xs;;
 937
 938 let end_strip_space = List.rev o strip_space o List.rev o strip_space;;
 939
 940 (*
 941
 942 let test1 = " (* note *) _t _44 __33 `1 /\\ [3] (* 42` (* hi *) ; [lade] da(%% (\"quote\";))  then (* c *) \t\n ";;
 943 let test2 = " (* hi *) (*  (* hi again *)  *) \"quote\" `&1 + &1`;; (* there *) ;; ";;
 944 (end_strip_space o snd o fst o m_lex o explode) test1;;
 945 implode;;
 946 many (some isspace);;
 947 test1;;
 948 unabbrev test1;;
 949
 950 *)
 951
 952
 953
 954
 955 (*
 956 let unabbrev_thm s =
 957   let tg = String.sub s 0 1 in
 958   let item = int_of_string (String.sub s 1 (String.length s - 1)) in
 959     retrieve_search tg item;;
 960 *)
 961
 962 let unabbrev_token = function
 963   | M_comment -> ""
 964   | M_string s -> "\""^s^"\""
 965   | M_hol_term s -> "`"^s^"`"
 966   | M_semicolon -> ";"
 967   | M_white s -> " "
 968   | M_text s -> unabbrev_string s
 969   | M_lparen -> "("
 970   | M_rparen -> ")"
 971   | M_lbracket -> "["
 972   | M_rbracket -> "]"
 973   | M_query s -> if (s.[0]='-') then expand_suggest (String.sub s 1 (String.length s - 1))
 974     else expand_thm s
 975   | M_env level -> if (level <=1) then " env w" else " envl w"
 976   | M_local s -> ("loc_"^s)
 977   | M_asm i -> ("asm_"^(string_of_int i));;
 978
 979 let which_asms  = mapfilter (function | M_asm i -> i | _ -> failwith "");;
 980
 981 let has_env = can (Lib.find (function M_env _ -> true | _ -> false));;
 982
 983
 984 let really_expand s  =
 985   let ((_,r),rest) = m_lex (explode s) in
 986   let _ = (rest=[]) or (failwith ("unparsed data : " ^ (implode rest))) in
 987   let r = end_strip_space r in
 988   let rs = map unabbrev_token r in
 989   let u =   unsplit "" I rs in
 990   let which = setify( which_asms r) in
 991   let gets = map (fun i ->Printf.sprintf " let asm_%d = snd(List.nth (List.rev asl) %d ) in " i i) which in
 992   let v = unsplit "" I gets in
 993   let envA,envB = if (has_env r) or (List.length which > 0) then
 994     "GOAL_TERM (fun w -> (","))" else "","" in
 995     (envA^v^u^envB);;
 996
 997
 998 (*
 999 let escape s =
1000   let ss = Str.split (Str.regexp "\"") s in
1001   let s = unsplit "\\\"" I ss in
1002   let ss = Str.split (Str.regexp "\\ ") s in
1003   let s = unsplit "\\\\ " I ss in
1004     s;;
1005 *)
1006
1007 let p() =
1008   let history = 5 in
1009   let _ = print_string (string_of_proof_k history ()) in
1010   if ((!current_goalstack=[])) then print_string "There is no current goal."
1011   else
1012     let (_,gl,_) = hd !current_goalstack in
1013     let ns = follow_your_nose_string_list() in
1014       if (gl = []) then print_string "\nNo subgoal"
1015       else
1016         (Print_types.print_goal_var_overload() ;
1017          print_goalstack (!current_goalstack);
1018          print_string ("\n >>>last step: "^ (string_of_proof_k 1 ()) ^ "\n");
1019          print_string (" >>>total: "^(string_of_int (length gl)) ^ "\n");
1020          if not(ns="") then print_string ("Follow your nose: "^ns)
1021         );;
1022
1023 (*
1024 let eval_tactic_abbrev s =
1025     try(
1026       let i = String.index s ',' in
1027       let pre = String.sub s 0 i in
1028       let post = String.sub s (i+1) (String.length s - (i+1)) in
1029         ((unabbrev_tactic pre)^" "^post)
1030     )
1031     with _ -> s in
1032  (* let _ = print_string (String.escaped expand_s) in *)
1033   let _ = eval_tactic (expand_s) in
1034     p();;
1035 *)
1036
1037 let eval_tactic_abbrev2 s =
1038   let sexp = really_expand s in
1039   let _ = report sexp in
1040   let _ = eval_tactic (sexp) in
1041    p();;
1042
1043 let blank_line = Str.regexp ("^ *$");;
1044
1045 let eval_tactic_lines s =
1046   let ss = Str.split (Str.regexp "\n") s in
1047   let one_line s1 =
1048     let sepx = try (really_expand s1) with _ -> (failwith "expansion error : "^s1) in
1049       if (Str.string_match blank_line sepx 0) then ()
1050       else
1051         try (Pervasives.ignore(eval_tactic sepx))
1052         with _ -> failwith ("tactic failure : "^s1^" >>> "^sepx) in
1053   let _ = do_list one_line ss in
1054     p();;
1055 (* emacs: hol-light-tactic-replay  "\C-c\C-r" *)
1056
1057 let e_abbrev = eval_tactic_abbrev2;;
1058
1059 let g = eval_goal;;
1060
1061 let b() =
1062   let _ = eval_back() in p();;
1063
1064 let bb k =
1065   let _ = map eval_back (replicate () k) in p();;
1066
1067 let back_to s =
1068   let r = List.rev (strs_of_proof_records 0 0 [] !proof_record) in
1069   let re = Str.regexp_case_fold (".*"^s) in
1070   let searcher a = Str.string_match re a 0 in
1071   let z = find searcher r in
1072   let _ = report z in
1073   let i = index z r in
1074    bb i;;
1075
1076 (*
1077 let directive_abbreviations= ref[
1078   ("-b",eval_back);
1079   ("-?",fun () ->
1080      let s = map snd tactic_counts in
1081      let s1 = unsplit ": "
1082 ];;
1083 *)
1084
1085 (* EMACS BINDINGS:
1086 see hol-light-mode.el
1087
1088 eval_tactic_lines -> hol-light-tactic-replay  "\C-c\C-r"
1089 (local-set-key "\C-ct" 'hol-light-goal-types)
1090 (local-set-key "\C-c\C-y" 'hol-light-type-region)
1091  (local-set-key "\C-cr" 'hol-light-eval-region)
1092
1093 *)
1094
1095
1096
1097 end;;