miz3/miz3.ml

   1 needs "Examples/holby.ml";;
   2
   3 let horizon = ref 1;;
   4 let timeout = ref 1;;
   5 let default_prover = ref ("HOL_BY", CONV_TAC o HOL_BY);;
   6 let renumber_labels = ref true;;
   7 let extra_labels = ref 0;;
   8 let start_label = ref 1;;
   9 let growth_mode = ref true;;
  10 let proof_indent = ref "  ";;
  11 let proof_width = ref 72;;
  12 let grow_haves = ref true;;
  13 let grow_duplicates = ref 0;;
  14 let indent_continued = ref false;;
  15 let sketch_mode = ref false;;
  16 let silent_server = ref 1;;
  17 let explain_errors = ref 1;;
  18 let miz3_pid = ref "/tmp/miz3_pid";;
  19 let miz3_filename = ref "/tmp/miz3_filename";;
  20
  21 let ERRORS =
  22   ["1: inference error";
  23    "2: inference time-out";
  24    "3: skeleton error";
  25    "4: unknown label";
  26    "5: error ocaml (or justification)";
  27    "6: underspecified types hol";
  28    "7: unbound free variables hol";
  29    "8: syntax or type error hol";
  30    "9: syntax error mizar"];;
  31
  32 let mizar_step_words =
  33   ["assume"; "cases"; "case"; "consider"; "end"; "let"; "now"; "proof";
  34    "qed"; "set"; "suppose"; "take"; "thus"];;
  35
  36 let mizar_step_words = mizar_step_words @
  37   ["exec"];;
  38
  39 let mizar_words = mizar_step_words @
  40   ["be"; "being"; "by"; "from"; "such"; "that"];;
  41
  42 let mizar_skip_bracketed =
  43   [","; ";"; "["];;
  44
  45 reserve_words (subtract mizar_words (reserved_words()));;
  46
  47 type by_item =
  48 | Label of string
  49 | Thm of string * thm
  50 | Tactic of string * (thm list -> tactic)
  51 | Grow of string * (thm list -> tactic)
  52 | Hole;;
  53
  54 type step =
  55   int * (string * lexcode * string) list list * substep
  56
  57 and substep =
  58 | Have of term * string list * just
  59 | Now of string list * just
  60 | Let of term list
  61 | Assume of term * string list
  62 | Thus of term * string list * just
  63 | Qed of just
  64 | Bracket_proof
  65 | Bracket_end
  66 | Take of term
  67 | Consider of term list * term * string list * just
  68 | Set of term * string list
  69 | Cases of just * just list
  70 | Bracket_case
  71 | Suppose of term * string list
  72 | Exec of string * tactic
  73 | Error of string * just
  74 | Error_point
  75 | Empty_step
  76
  77 and just =
  78 | By of by_item list * by_item list * bool
  79 | Proof of step option * step list * step option
  80 | Proof_expected of bool
  81 | No_steps;;
  82
  83 unset_jrh_lexer;;
  84
  85 let system_ok = Unix.WEXITED 0;;
  86 let wronly = Unix.O_WRONLY;;
  87 let usr2_handler = ref (fun () -> print_string "usr2_handler\n");;
  88 Sys.signal Sys.sigusr2 (Sys.Signal_handle (fun _ -> !usr2_handler ()));;
  89
  90 set_jrh_lexer;;
  91
  92 let rawtoken =
  93   let collect (h,t) = end_itlist (^) (h::t) in
  94   let stringof p = atleast 1 p >> end_itlist (^) in
  95   let simple_ident = stringof(some isalnum) || stringof(some issymb) in
  96   let undertail = stringof (a "_") ++ possibly simple_ident >> collect in
  97   let ident = (undertail || simple_ident) ++ many undertail >> collect in
  98   let septok = stringof(some issep) in
  99   let stringchar =
 100       some (fun i -> i <> "\\" & i <> "\"")
 101   || (a "\\" ++ some (fun _ -> true) >> fun (_,x) -> "\\"^x) in
 102   let string = a "\"" ++ many stringchar ++ ((a "\"" >> K 0) || finished) >>
 103         (fun ((_,s),_) -> "\""^implode s^"\"") in
 104   (string || some isbra || septok || ident || a "`");;
 105
 106 let rec whitespace e i =
 107   let non_newline i =
 108     if i <> [] & hd i <> "\n" then hd i,tl i else raise Noparse in
 109   let rest_of_line = many non_newline ++ (a "\n" || (finished >> K "")) >>
 110     fun x,y -> itlist (^) x y in
 111   let comment_string =
 112     match !comment_token with
 113     | Resword t -> t
 114     | Ident t -> t in
 115   match i with
 116   | [] -> if e then "",i else raise Noparse
 117   | (" " as c)::rst | ("\t" as c)::rst | ("\r" as c)::rst ->
 118       let s,rst1 = whitespace true rst in c^s,rst1
 119   | ("\n" as c)::rst -> c,rst
 120   | _ ->
 121       let t,rst = rawtoken i in
 122       if t = comment_string then (rest_of_line >> fun x -> t^x) rst
 123       else if String.length t >= 2 && String.sub t 0 2 = "::" then
 124         (rest_of_line >> fun x -> if e then t^x else "") rst
 125       else if e then "",i else raise Noparse;;
 126
 127 let lex1 =
 128   let reserve1 n =
 129     if is_reserved_word n then Resword n else Ident n in
 130   let rec tokens i =
 131     try (many (whitespace false) ++ rawtoken ++ whitespace true
 132         ++ tokens >>
 133       fun (((x,y),z),w) -> (implode x,reserve1 y,z)::w) i
 134     with Noparse -> [],i in
 135   fun l ->
 136     let (toks,rst) = tokens l in
 137     let rst',rst'' = many (whitespace false) rst in
 138     if rst'' <> [] then failwith "lex1" else
 139     if toks = [] then toks else
 140     let (x,y,z) = last toks in
 141     butlast toks@[x,y,z^implode rst'];;
 142
 143 let lex2 = lex1 o explode;;
 144
 145 let middle (_,x,_) = x;;
 146
 147 let a' t toks =
 148   match toks with
 149   | ((_,Resword t',_) as tok)::rst when t = t' -> tok,rst
 150   | ((_,Ident t',_) as tok)::rst when t = t' -> tok,rst
 151   | _ -> raise Noparse;;
 152
 153 let a_semi = a' ";";;
 154
 155 let ident' toks =
 156   match toks with
 157   | (_,Ident s,_)::rst -> s,rst
 158   | (_,Resword "(",_)::(_,Ident s,_)::(_,Resword ")",_)::rst -> s,rst
 159   | _ -> raise Noparse;;
 160
 161 let unident' s =
 162   if parses_as_binder s or can get_infix_status s or is_prefix s
 163     then ["",Resword "(",""; "",Ident s,""; "",Resword ")",""]
 164     else ["",Ident s,""];;
 165
 166 let rec cut_to b n c l toks =
 167   match toks with
 168   | [] -> if b then [],[] else raise Noparse
 169   | tok::rst ->
 170      (match tok with
 171       | _,Resword s,_ | _,Ident s,_ ->
 172           let x = not (n > 0 & mem s mizar_skip_bracketed) in
 173           if mem s c & x then [tok],rst else
 174           if b & mem s l & x then [],toks else
 175           let stp1,rst1 =
 176            (match s with
 177             | "(" | "[" -> cut_to true (n + 1) c l rst
 178             | ")" | "]" -> cut_to true (if n > 0 then n - 1 else 0) c l rst
 179             | _ -> cut_to true n c l rst) in
 180           (tok::stp1),rst1);;
 181
 182 let cut_step toks =
 183   match toks with
 184   | (_,Resword "proof",_ as tok)::rst -> [tok],rst
 185   | (_,Resword "now",_)::rst ->
 186       (a' "now" ++
 187         (many (a' "[" ++ cut_to false 0 ["]"] mizar_step_words >>
 188           fun x,y -> x::y)) >> fun x,y -> x::(itlist (@) y [])) toks
 189   | _ -> cut_to false 0 [";"] mizar_step_words toks;;
 190
 191 let rec cut_steps toks =
 192   let steps,rst = many cut_step toks in
 193   if rst = [] then steps else steps@[rst];;
 194
 195 let strings_of_toks toks =
 196   let rec string_of_toks1 toks =
 197     match toks with
 198     | [] -> "",""
 199     | [x,Ident y,z] | [x,Resword y,z] -> x^y,z
 200     | (x,Ident y,z)::rst | (x,Resword y,z)::rst  ->
 201         let u,v = string_of_toks1 rst in x^y^z^u,v in
 202   match toks with
 203   | [] -> "","",""
 204   | [x,Ident y,z] | [x,Resword y,z] -> x,y,z
 205   | (x,Ident y,z)::rst | (x,Resword y,z)::rst ->
 206       let u,v = string_of_toks1 rst in x,y^z^u,v;;
 207
 208 let string_of_toks = middle o strings_of_toks;;
 209
 210 let split_string = map string_of_toks o cut_steps o lex2;;
 211
 212 let tok_of_toks toks =
 213   let x,y,z = strings_of_toks toks in
 214   x,Ident y,z;;
 215
 216 let exec_phrase b s =
 217   let lexbuf = Lexing.from_string s in
 218   let ok = Toploop.execute_phrase b Format.std_formatter
 219     (!Toploop.parse_toplevel_phrase lexbuf) in
 220   Format.pp_print_flush Format.std_formatter ();
 221   (ok,
 222    let i = lexbuf.Lexing.lex_curr_pos in
 223    String.sub lexbuf.Lexing.lex_buffer
 224      i (lexbuf.Lexing.lex_buffer_len - i));;
 225
 226 let exec_thm_out = ref TRUTH;;
 227
 228 let exec_thm s =
 229   try
 230     let ok,rst = exec_phrase false
 231       ("exec_thm_out := (("^s^") : thm);;") in
 232     if not ok or rst <> "" then raise Noparse;
 233     !exec_thm_out
 234   with _ -> raise Noparse;;
 235
 236 let exec_thmlist_tactic_out = ref REWRITE_TAC;;
 237
 238 let exec_thmlist_tactic s =
 239   try
 240     let ok,rst = exec_phrase false
 241       ("exec_thmlist_tactic_out := (("^s^") : thm list -> tactic);;") in
 242     if not ok or rst <> "" then raise Noparse;
 243     !exec_thmlist_tactic_out
 244   with _ -> raise Noparse;;
 245
 246 let exec_thmtactic_out = ref MATCH_MP_TAC;;
 247
 248 let exec_thmtactic s =
 249   try
 250     let ok,rst = exec_phrase false
 251       ("exec_thmtactic_out := (("^s^") : thm -> tactic);;") in
 252     if not ok or rst <> "" then raise Noparse;
 253     !exec_thmtactic_out
 254   with _ -> raise Noparse;;
 255
 256 let exec_tactic_out = ref ALL_TAC;;
 257
 258 let exec_tactic s =
 259   try
 260     let ok,rst = exec_phrase false
 261       ("exec_tactic_out := (("^s^") : tactic);;") in
 262     if not ok or rst <> "" then raise Noparse;
 263     !exec_tactic_out
 264   with _ -> raise Noparse;;
 265
 266 let exec_conv_out = ref NUM_REDUCE_CONV;;
 267
 268 let exec_conv s =
 269   try
 270     let ok,rst = exec_phrase false
 271       ("exec_conv_out := (("^s^") : conv);;") in
 272     if not ok or rst <> "" then raise Noparse;
 273     !exec_conv_out
 274   with _ -> raise Noparse;;
 275
 276 let (MP_ALL : tactic -> thm list -> tactic) =
 277   fun tac ths ->
 278     MAP_EVERY MP_TAC ths THEN tac;;
 279
 280 let use_thms tac =
 281   fun ths -> tac ORELSE MP_ALL tac ths;;
 282
 283 let by_item_cache = ref undefined;;
 284
 285 let rec by_item_of_toks toks =
 286   match toks with
 287   | [_,Ident "#",_] -> Hole
 288   | (_,Ident "#",_)::toks' ->
 289      (match by_item_of_toks toks' with
 290       | Tactic(s,tac) -> Grow(s,tac)
 291       | _ -> failwith "by_item_of_toks")
 292   | [_,Ident "*",_] -> Label "*"
 293   | _ ->
 294   let s = string_of_toks toks in
 295   try apply (!by_item_cache) s with _ ->
 296   let i =
 297     try Thm (s, exec_thm s) with _ ->
 298     try Tactic (s, exec_thmlist_tactic s) with _ ->
 299     try Tactic (s, (exec_thmtactic s) o hd) with _ ->
 300     try Tactic (s, use_thms (exec_tactic s)) with _ ->
 301     try Tactic (s, use_thms (CONV_TAC (exec_conv s))) with _ ->
 302     match toks with
 303     | [_,Ident s,_] -> Label s
 304     | _ -> failwith "by_item_of_toks" in
 305   by_item_cache := (s |-> i) !by_item_cache;
 306   i;;
 307
 308 let parse_by =
 309   let parse_by_item toks =
 310     match toks with
 311     | (_,Ident "#",_ as tok1)::(_,Ident s,_ as tok2)::toks when s <> "," ->
 312         [tok1;tok2],toks
 313     | (_,Ident _,_ as tok)::toks -> [tok],toks
 314     | _ -> raise Noparse in
 315   let parse_by_part =
 316      ((a' "by" ++ many (parse_by_item ++ a' "," >> fst) >> snd) ++
 317        parse_by_item) >>
 318           (fun (x,y) -> x@[y])
 319   || (nothing >> K [])
 320   and parse_from_part =
 321      ((a' "from" ++ many (parse_by_item ++ a' "," >> fst) >> snd) ++
 322        parse_by_item) >>
 323           (fun (x,y) -> (x@[y]),true)
 324   || (nothing >> K ([],false)) in
 325   let rec will_grow l =
 326     match l with
 327     | [] -> false
 328     | Tactic _::_ -> false
 329     | Grow _::_ -> true
 330     | _::l' -> will_grow l'
 331   in
 332      ((parse_by_part ++ parse_from_part) ++ a_semi ++ finished >>
 333         fun (((x,(y,z)),_),_) ->
 334           let x' = map by_item_of_toks x in
 335           let y' = map by_item_of_toks y in
 336           By(x',y',z or will_grow (x'@y')))
 337   || (finished >> K (Proof_expected true));;
 338
 339 let rec parse_labels toks =
 340   match toks with
 341   | [] -> []
 342   | (_,Resword "[",_)::(_,Ident s,_)::(_,Resword "]",_)::rst ->
 343       s::(parse_labels rst)
 344   | _ -> raise Noparse;;
 345
 346 let rec type_of_pretype1 ty =
 347   match ty with
 348     Stv n -> failwith "type_of_pretype1"
 349   | Utv(v) -> mk_vartype(v)
 350   | Ptycon(con,args) -> mk_type(con,map type_of_pretype1 args);;
 351
 352 let term_of_preterm1 =
 353   let rec term_of_preterm1 ptm =
 354     match ptm with
 355       Varp(s,pty) -> mk_var(s,type_of_pretype1 pty)
 356     | Constp(s,pty) -> mk_mconst(s,type_of_pretype1 pty)
 357     | Combp(l,r) -> mk_comb(term_of_preterm1 l,term_of_preterm1 r)
 358     | Absp(v,bod) -> mk_gabs(term_of_preterm1 v,term_of_preterm1 bod)
 359     | Typing(ptm,pty) -> term_of_preterm1 ptm in
 360   fun ptm -> term_of_preterm1 ptm;;
 361
 362 let term_of_hol b =
 363   let error = mk_var("error",`:error`) in
 364   let term_of_hol1 env toks =
 365     let env' = ("thesis",Ptycon("bool",[]))::
 366       (map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var) env) in
 367     try
 368       let ptm,l = (parse_preterm o map middle) toks in
 369       if l <> [] then (8,error) else
 370       try
 371         let tm = (term_of_preterm1 o retypecheck env') ptm in
 372         if not (subset
 373            (filter
 374              (fun v -> not (mem (fst (dest_var v)) ["..."; "thesis"]))
 375              (frees tm)) env)
 376           then (7,error) else
 377         if b && type_of tm <> bool_ty then (8,error) else
 378         (0,tm)
 379       with _ ->
 380         let tiw = !type_invention_warning in
 381         type_invention_warning := false;
 382         let tm =
 383           try (term_of_preterm o retypecheck env') ptm
 384           with e -> type_invention_warning := tiw; raise e in
 385         type_invention_warning := tiw;
 386         if not (subset (frees tm) env) then (7,error) else (6,error)
 387     with _ -> (8,error) in
 388   fun env toks ->
 389     match toks with
 390     | (x,Ident ".=",y)::rest ->
 391         term_of_hol1 env ((x,Ident "..."," ")::("",Ident "=",y)::rest)
 392     | _ -> term_of_hol1 env toks;;
 393
 394 let type_of_hol =
 395   let error = `:error` in
 396   fun toks ->
 397     try (0,(parse_type o middle o strings_of_toks) toks)
 398     with _ -> (8,error);;
 399
 400 let split_step toks =
 401   let cut_semi toks =
 402     match toks with
 403     | (_,Resword ";",_ as tok)::rst -> rev rst,[tok]
 404     | _ -> rev toks,[] in
 405   let rec cut_by_part rev_front toks =
 406     match toks with
 407     | [] | (_,Resword "by",_)::_ | (_,Resword "from",_)::_ -> rev_front,toks
 408     | tok::rst -> cut_by_part (tok::rev_front) rst in
 409   let rec group_by_items toks =
 410     match toks with
 411     | [] -> []
 412     | (_,Resword "by",_ as tok)::rst
 413     |   (_,Resword "from",_ as tok)::rst
 414     |   (_,Ident ",",_ as tok)::rst
 415     |   (_,Resword ";",_ as tok)::rst -> tok::group_by_items rst
 416     | (_,Ident "#",_ as tok)::toks' ->
 417         let toks1,toks2 =
 418           if toks' = [] then [],[]
 419             else cut_to false 0 [] ([","; ";"]@mizar_words) toks' in
 420         tok::(if toks1 = [] then [] else [tok_of_toks toks1])@
 421           group_by_items toks2
 422     | tok::rst ->
 423         let toks1,toks2 = cut_to false 0 [] ([","; ";"]@mizar_words) toks in
 424         if toks1 = [] then tok::group_by_items rst else
 425         (tok_of_toks toks1)::group_by_items toks2 in
 426   let rec cut_labs toks labs =
 427     match toks with
 428     | (_,Resword "]",_ as tok1)::(_,Ident _,_ as tok2)::
 429       (_,Resword "[",_ as tok3)::rst ->
 430         cut_labs rst (tok3::tok2::tok1::labs)
 431     | _ -> toks,labs in
 432   let rec cut_front toks tail =
 433     match toks with
 434     | [] -> [],tail
 435     | (_,Resword s,_)::rst when mem s mizar_words -> rev toks,tail
 436     | tok::rst -> cut_front rst (tok::tail) in
 437   let toks1,semi_part = cut_semi (rev toks) in
 438   let toks2,by_part = cut_by_part [] toks1 in
 439   let toks3,labs_part = cut_labs toks2 [] in
 440   let front_part,hol_part = cut_front toks3 [] in
 441   if front_part <> [] & middle (hd front_part) = Resword "exec" then
 442     let ml_tok = tok_of_toks ((tl front_part)@hol_part@labs_part@by_part) in
 443     [[hd front_part]; [ml_tok]; []; []; semi_part]
 444   else
 445     [front_part; hol_part; labs_part; group_by_items by_part; semi_part];;
 446
 447 let parse_step env toks =
 448   let src = split_step toks in
 449   try
 450     match src with
 451     | [front_part; hol_part; labs_part; by_part; semi_part] ->
 452         let labs = parse_labels labs_part in
 453         let just,_ = parse_by (by_part@semi_part) in
 454        (match front_part with
 455         | [] ->
 456            (match toks with
 457             | [_,Resword ";",_] ->
 458                 -1,src,Empty_step
 459             | _ ->
 460                 let n,t = term_of_hol true env hol_part in
 461                 if n <> 0 then n,src,Error(string_of_toks toks,just) else
 462                 -1,src,Have(t,labs,just))
 463         | (_,Resword key,_)::_ ->
 464            (match key,(tl front_part),(string_of_toks semi_part) with
 465             | "now",[],"" ->
 466                 if hol_part <> [] or by_part <> [] then raise Noparse else
 467                 -1,src,Now(labs,Proof_expected false)
 468             | "let",rst,";" ->
 469                 if labs_part <> [] or by_part <> [] then raise Noparse else
 470                 let x = (fst o fst o fst o
 471                   many ident' ++ a' "be" ++ finished) rst in
 472                 let n,t = type_of_hol hol_part in
 473                 if n <> 0 then n,src,Error(string_of_toks toks,No_steps) else
 474                 -1,src,Let(map (fun s -> mk_var(s,t)) x)
 475             | "assume",[],";" ->
 476                 if by_part <> [] then raise Noparse else
 477                 let n,t = term_of_hol true env hol_part in
 478                 if n <> 0 then n,src,Error(string_of_toks toks,No_steps) else
 479                 -1,src,Assume(t,labs)
 480             | "thus",[],_ ->
 481                 let n,t = term_of_hol true env hol_part in
 482                 if n <> 0 then n,src,Error(string_of_toks toks,just) else
 483                 -1,src,Thus(t,labs,just)
 484             | "qed",[],_ ->
 485                 if hol_part <> [] or labs_part <> [] then raise Noparse else
 486                 -1,src,Qed just
 487             | "proof",[],"" ->
 488                 if hol_part <> [] or labs_part <> [] or by_part <> [] then
 489                   raise Noparse else
 490                 -1,src,Bracket_proof
 491             | "end",[],";" ->
 492                 if hol_part <> [] or labs_part <> [] or by_part <> [] then
 493                   raise Noparse else
 494                 -1,src,Bracket_end
 495             | "take",[],";" ->
 496                 if labs_part <> [] or by_part <> [] then raise Noparse else
 497                 let n,t = term_of_hol false env hol_part in
 498                 if n <> 0 then n,src,Error(string_of_toks toks,No_steps) else
 499                 -1,src,Take t
 500             | "consider",rst,_ ->
 501                 let cut_suchthat toks =
 502                   match toks with
 503                   | (_,Resword "that",_)::(_,Resword "such",_)::rst -> rst
 504                   | _ -> raise Not_found in
 505                 let rec cut_being toks tail =
 506                   match toks with
 507                   | [] -> raise Not_found
 508                   | (_,Resword "being",_)::rst -> (rev rst),(rev tail)
 509                   | tok::rst -> cut_being rst (tok::tail) in
 510                (try
 511                   let rst1,rst2 = cut_being (cut_suchthat (rev rst)) [] in
 512                   let n,t = type_of_hol rst2 in
 513                   if n <> 0 then n,src,Error(string_of_toks toks,just) else
 514                   let x = (fst o fst o many ident' ++ finished) rst1 in
 515                   let vars = map (fun s -> mk_var(s,t)) x in
 516                   let n,tm' = term_of_hol true (vars@env) hol_part in
 517                   if n <> 0 then n,src,Error(string_of_toks toks,just) else
 518                   -1,src,Consider(vars,tm',labs,just)
 519                 with Not_found ->
 520                   let x = (fst o fst o fst o fst o
 521                     many ident' ++ a' "such" ++ a' "that" ++ finished) rst in
 522                   let xy = (("",Ident "?","")::((flat (map unident' x))@
 523                     (("",Resword ".","")::hol_part))) in
 524                   let n,tm = term_of_hol true env xy in
 525                   if n <> 0 then n,src,Error(string_of_toks toks,just) else
 526                   let vars,tm' = nsplit dest_exists x tm in
 527                   -1,src,Consider(vars,tm',labs,just))
 528             | "set",[],";" ->
 529                 if by_part <> [] then raise Noparse else
 530                 let (w,_),rst = (ident' ++ a' "=") hol_part in
 531                 let n,t = term_of_hol false env rst in
 532                 if n <> 0 then n,src,Error(string_of_toks toks,No_steps) else
 533                 -1,src,Set(mk_eq(mk_var(w,type_of t),t),labs)
 534             | "cases",[],_ ->
 535                 if hol_part <> [] or labs_part <> [] then raise Noparse else
 536                 -1,src,Cases(just,[])
 537             | "case",[],";" ->
 538                 if hol_part <> [] or labs_part <> [] or by_part <> [] then
 539                   raise Noparse else
 540                 -1,src,Bracket_case
 541             | "suppose",[],";" ->
 542                 if by_part <> [] then raise Noparse else
 543                 let n,t = term_of_hol true env hol_part in
 544                 if n <> 0 then
 545                   n,src,Error(string_of_toks toks,Proof_expected false) else
 546                 -1,src,Suppose(t,labs)
 547             | "exec",[],";" ->
 548                 let s = string_of_toks hol_part in
 549                 -1,src,Exec(s,exec_tactic s)
 550             | _ -> raise Noparse)
 551         | _ -> raise Noparse)
 552     | _ -> raise Noparse
 553   with
 554   | Failure "by_item_of_toks" -> 5,src,Error(string_of_toks toks,No_steps)
 555   | _ -> 9,src,Error(string_of_toks toks,No_steps);;
 556
 557 let rec steps_of_toks1 q e env toks =
 558   let prefix x (y,w,z) = (x@y),w,z in
 559   if toks = [] then
 560     if e then [9,[],Error_point],None,[] else [],None,[]
 561   else
 562     let stoks,rst = cut_step toks in
 563     let (status,src,substep as step) = parse_step env stoks in
 564     match substep with
 565     | Have (tm, labs, Proof_expected _) ->
 566         let just,rst1 = just_of_toks env rst in
 567         let step,rst2 =
 568          (match just with
 569           | Proof(_, _, _) -> (status,src,Have (tm, labs, just)),rst1
 570           | _ -> (9,src,Error(string_of_toks stoks, No_steps)),rst) in
 571         prefix [step] (steps_of_toks1 q e env rst2)
 572     | Thus (tm, labs, Proof_expected _) ->
 573         let just,rst1 = just_of_toks env rst in
 574         let step,rst2 =
 575          (match just with
 576           | Proof(_, _, _) -> (status,src,Thus (tm, labs, just)),rst1
 577           | _ -> (9,src,Error(string_of_toks stoks, No_steps)),rst) in
 578         prefix [step] (steps_of_toks1 q e env rst2)
 579     | Let vars -> prefix [step] (steps_of_toks1 q e ((rev vars)@env) rst)
 580     | Now (labs, Proof_expected _) ->
 581         let just,rst1 = now_of_toks env rst in
 582         prefix [status,src,Now (labs, just)] (steps_of_toks1 q e env rst1)
 583     | Consider (vars, _, _, By _) ->
 584         prefix [step] (steps_of_toks1 q e ((rev vars)@env) rst)
 585     | Consider (vars, tm, labs, Proof_expected _) ->
 586         let just,rst1 = just_of_toks env rst in
 587         let step,rst2 =
 588          (match just with
 589           | Proof(_, _, _) -> (status,src,Consider(vars, tm, labs, just)),rst1
 590           | _ -> (9,src,Error(string_of_toks stoks, No_steps)),rst) in
 591         prefix [step] (steps_of_toks1 q e ((rev vars)@env) rst2)
 592     | Set (tm, _) ->
 593         prefix [step] (steps_of_toks1 q e ((fst (dest_eq tm))::env) rst)
 594     | Cases ((By _ as just), []) ->
 595        (try
 596           let justs,rst1 = many (case_of_toks env q) rst in
 597           let final,step1,rst2 = steps_of_toks1 false e env rst1 in
 598           let cases = status,src,Cases(just, justs) in
 599           if final <> [] then
 600             prefix [cases; 9,[],Error_point]
 601               (steps_of_toks1 q e env rst1)
 602           else [cases],step1,rst2
 603         with Noparse ->
 604           prefix [9,src,Error(string_of_toks stoks, No_steps)]
 605             (steps_of_toks1 q e env rst))
 606     | Qed just ->
 607         if q then [step],None,rst else
 608         prefix [(if e then 3 else 9),src,Error(string_of_toks stoks, No_steps)]
 609           (steps_of_toks1 q e env rst)
 610     | Bracket_end ->
 611         if e then [],Some step,rst else
 612         prefix [9,src,Error(string_of_toks stoks, No_steps)]
 613           (steps_of_toks1 q e env rst)
 614     | Bracket_proof | Cases (_, _) | Bracket_case | Suppose (_, _) ->
 615         prefix [9,src,Error(string_of_toks stoks, No_steps)]
 616           (steps_of_toks1 q e env rst)
 617     | Error (s, Proof_expected true) ->
 618         let just,rst1 = just_of_toks env rst in
 619        (match just with
 620         | Proof(_, _, _) ->
 621             prefix [status,src,Error(s, just)] (steps_of_toks1 q e env rst1)
 622         | _ ->
 623             prefix [status,src,Error(string_of_toks stoks, No_steps)]
 624               (steps_of_toks1 q e env rst))
 625     | Error (s, Proof_expected false) ->
 626         let steps,step1,rst1 = steps_of_toks1 true true env rst in
 627         prefix [status,src,Error(s, Proof(None,steps,step1))]
 628           (steps_of_toks1 q e env rst)
 629     | Error (_, By _) ->
 630         prefix [status,src,Error(string_of_toks stoks, No_steps)]
 631           (steps_of_toks1 q e env rst)
 632     | _ -> prefix [step] (steps_of_toks1 q e env rst)
 633
 634 and just_of_toks env toks =
 635   try
 636     let stoks,rst = cut_step toks in
 637     let (_,_,substep as step) = parse_step env stoks in
 638     if substep = Bracket_proof then
 639       let steps,step1,rst1 = steps_of_toks1 true true env rst in
 640       (Proof(Some step,steps,step1)),rst1
 641     else (No_steps),toks
 642   with Noparse -> (No_steps),toks
 643
 644 and now_of_toks env toks =
 645   let steps,step1,rst = steps_of_toks1 false true env toks in
 646   (Proof(None,steps,step1)),rst
 647
 648 and case_of_toks env q toks =
 649   let stoks,rst = cut_step toks in
 650   let (_,_,substep as step) = parse_step env stoks in
 651   match substep with
 652   | Bracket_case ->
 653       let steps,step1,rst1 = steps_of_toks1 q true env rst in
 654       (Proof(Some step,steps,step1)),rst1
 655   | Suppose (_, _) ->
 656       let steps,step1,rst1 = steps_of_toks1 q true env rst in
 657       (Proof(None,step::steps,step1)),rst1
 658   | _ -> raise Noparse;;
 659
 660 let steps_of_toks toks =
 661   let proof,_,rst = steps_of_toks1 false false [] toks in
 662   if rst = [] then proof else
 663     proof@[9,[rst],Error (string_of_toks rst, No_steps)];;
 664
 665 let fix_semi toks =
 666   if toks = [] then toks else
 667   match last toks with
 668   | _,Resword ";",_ -> toks
 669   | _ -> toks@["\n",Resword ";",""];;
 670
 671 let parse_proof = steps_of_toks o fix_semi o lex2;;
 672
 673 exception Timeout;;
 674
 675 Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Timeout));;
 676
 677 let TIMED_TAC n tac g =
 678   let _ = Unix.alarm n in
 679   try
 680     let gs = tac g in
 681     let _ = Unix.alarm 0 in
 682     gs
 683   with x ->
 684     let _ = Unix.alarm 0 in
 685     raise x;;
 686
 687 let FAKE_TAC : bool -> thm list -> tactic =
 688   fun fake thl (asl,w as g) ->
 689     if fake then
 690       let tm' = itlist (curry mk_imp) (map concl thl) w in
 691       let vl = frees tm' in
 692       let tm = itlist (curry mk_forall) vl tm' in
 693       let th = itlist (C MP) (rev thl) (itlist SPEC (rev vl) (ASSUME tm)) in
 694       null_meta,[],(fun i _ -> INSTANTIATE_ALL i th)
 695     else NO_TAC g;;
 696
 697 let MIZAR_NEXT : (goal -> step * goalstate) -> (goal -> step * goalstate) =
 698   let t = `T` in
 699   fun tac (asl,_ as g) ->
 700     let e,((mvs,insts),gls,just as gs) = tac g in
 701     match gls with
 702     | [] -> e,((mvs,insts),[asl,t],(fun _ _ -> just null_inst []))
 703     | [gl] -> e,gs
 704     | _ -> failwith "MIZAR_NEXT";;
 705
 706 let MIZAR_NEXT' : tactic -> tactic =
 707   let t = `T` in
 708   fun tac (asl,_ as g) ->
 709     let ((mvs,insts),gls,just as gs) = tac g in
 710     match gls with
 711     | [] ->
 712         ((mvs,insts),[asl,t],(fun _ _ -> just null_inst []))
 713     | [gl] -> gs
 714     | _ -> failwith "MIZAR_NEXT'";;
 715
 716 let fix_dots prevs tm =
 717   try
 718     let lhs,_ = dest_eq (hd prevs) in
 719     vsubst [lhs, mk_var("...",type_of lhs)] tm
 720   with _ -> tm;;
 721
 722 let fix_dots' asl tm =
 723   try
 724     let th = snd (hd asl) in
 725     let lhs,_ = dest_eq (concl th) in
 726     let dots = mk_var("...",type_of lhs) in
 727     let rec fix_dots1 tm =
 728      (match tm with
 729       | Var _ when tm = dots -> th
 730       | Comb(t1,t2) -> MK_COMB(fix_dots1 t1,fix_dots1 t2)
 731       | Abs(x,t) -> ABS x (fix_dots1 t)
 732       | _ -> REFL tm) in
 733     if vfree_in dots tm then fix_dots1 tm else REFL tm
 734   with _ -> REFL tm;;
 735
 736 let rec terms_of_step prevs (_,_,substep) =
 737   match substep with
 738   | Have (tm, _, _) -> [fix_dots prevs tm]
 739   | Now (_, just) -> [term_of_now just]
 740   | Assume (tm, _) -> [fix_dots prevs tm]
 741   | Thus (tm, _, _) -> [fix_dots prevs tm]
 742   | Consider (_, tm, _, _) -> [fix_dots prevs tm]
 743   | Set (tm, _) -> [fix_dots prevs tm]
 744   | Suppose (tm, _) -> [fix_dots prevs tm]
 745   | _ -> []
 746
 747 and term_of_now =
 748   let t = `T` in
 749   let rec term_of_steps prevs steps =
 750     match steps with
 751     | [] -> t
 752     | (_,_,substep as step)::rst ->
 753         let tm' = term_of_steps ((terms_of_step prevs step)@prevs) rst in
 754        (match substep with
 755         | Let vars -> list_mk_forall(vars,tm')
 756         | Assume (tm, _) -> mk_imp(fix_dots prevs tm,tm')
 757         | Thus (tm, _, _) -> mk_conj(fix_dots prevs tm,tm')
 758         | Take tm ->
 759             let var = genvar (type_of tm) in mk_exists(var,subst [var,tm] tm')
 760         | Consider (vars, _, _, _) ->
 761             if intersect (frees tm') vars <> [] then failwith "term_of_now"
 762             else tm'
 763         | Cases (_, _) -> failwith "term_of_now"
 764         | _ -> tm') in
 765   fun just ->
 766     match just with
 767     | Proof(_, steps, _) ->
 768         (rand o concl o PURE_REWRITE_CONV[AND_CLAUSES])
 769           (term_of_steps [] steps)
 770     | _ -> failwith "term_of_now";;
 771
 772 let terms_of_cases =
 773   let f = `F` in
 774   let rec terms_of_cases cases =
 775     match cases with
 776     | [] -> [],f
 777     | case::rst ->
 778       let l',tm' = terms_of_cases rst in
 779      (match case with
 780       | (_,_,Suppose (tm, _))::_ -> (()::l'),mk_disj(tm,tm')
 781       | _ -> failwith "terms_of_cases") in
 782   terms_of_cases o (map
 783     (fun just ->
 784        match just with
 785        | Proof(_, case, _) -> case
 786        | _ -> failwith "terms_of_cases"));;
 787
 788 let print_to_string1 printer =
 789   let sbuff = ref "" in
 790   let output s m n = sbuff := (!sbuff)^(String.sub s m n) and flush() = () in
 791   let fmt = make_formatter output flush in
 792   ignore(pp_set_max_boxes fmt 100);
 793   fun prefix' n i ->
 794     let prefix = prefix'^(implode (replicate " " n)) in
 795     let m = String.length prefix in
 796     pp_set_margin fmt ((!proof_width) - m);
 797     ignore(printer fmt i);
 798     ignore(pp_print_flush fmt ());
 799     let s = !sbuff in sbuff := "";
 800     implode (map (fun x -> if x = "\n" then "\n"^prefix else x) (explode s));;
 801
 802 let string_of_term1 = print_to_string1 pp_print_term;;
 803 let string_of_type1 = print_to_string1 pp_print_type;;
 804
 805 let string_of_substep prefix substep =
 806   let string_of_vars tl = implode (map (fun v -> " "^fst (dest_var v)) tl) in
 807   let string_of_labs l = implode (map (fun s -> " ["^s^"]") l) in
 808   let rec string_of_by_items x l =
 809     match l with
 810     | [] -> ""
 811     | i::l' -> x^(match i with
 812         | Label s | Thm(s,_) | Tactic(s,_) | Grow(s,_) -> s
 813         | Hole -> "#")^string_of_by_items "," l' in
 814   let string_of_just just =
 815     match just with
 816     | By(l,l',_) ->
 817         (if l = [] then "" else " by"^string_of_by_items " " l)^
 818         (if l' = [] then "" else " from"^string_of_by_items " " l')^";"
 819     | _ -> "" in
 820   prefix^
 821  (match substep with
 822   | Have(tm,l,just) ->
 823       string_of_term1 prefix
 824         (if !indent_continued then String.length !proof_indent else 0) tm^
 825       string_of_labs l^string_of_just just
 826   | Now(l,just) -> "now"^string_of_labs l
 827   | Let(tl) ->
 828       let s = "let"^string_of_vars tl^" be " in
 829       s^string_of_type1 prefix (String.length s) (type_of (hd tl))^";"
 830   | Assume(tm,l) ->
 831       let s = "assume " in
 832       s^string_of_term1 prefix (String.length s) tm^string_of_labs l^";"
 833   | Thus(tm,l,just) ->
 834       let s = "thus " in
 835       s^string_of_term1 prefix (String.length s) tm^string_of_labs l^
 836       string_of_just just
 837   | Qed(just) -> "qed"^string_of_just just
 838   | Bracket_proof -> "proof"
 839   | Bracket_end -> "end;"
 840   | Take(tm) ->
 841       let s = "take " in
 842       s^string_of_term1 prefix (String.length s) tm^";"
 843   | Consider(tl,tm,l,just) ->
 844       let s = "consider"^string_of_vars tl^" such that " in
 845       s^string_of_term1 prefix (String.length s) tm^
 846       string_of_labs l^string_of_just just
 847   | Set(tm,l) ->
 848       let s = "set " in
 849       s^string_of_term1 prefix (String.length s) tm^string_of_labs l^";"
 850   | Cases(just,_) -> "cases"^string_of_just just
 851   | Bracket_case -> "case;"
 852   | Suppose(tm,l) ->
 853       let s = "suppose " in
 854       s^string_of_term1 prefix (String.length s) tm^string_of_labs l^";"
 855   | Exec(s,_) -> "exec "^s^";"
 856   | Error(s,_) -> s
 857   | Empty_step -> ""
 858   | Error_point -> "")^
 859   "\n";;
 860
 861 let step_of_substep prefix substep =
 862   (-1,split_step (lex2 (string_of_substep prefix substep)),substep :step);;
 863
 864 let step_of_obligation prefix lab tl ass tm =
 865   let hole = By([Hole],[],false) in
 866   let prefix' = prefix^ !proof_indent in
 867   let rec lets l =
 868     match l with
 869     | [] -> []
 870     | t::_ -> let l',l'' = partition ((=) (type_of t) o type_of) l in
 871         step_of_substep prefix' (Let l')::lets l'' in
 872   step_of_substep prefix
 873     (if tl = [] & ass = [] then Have(tm,[lab],hole) else
 874     let ll = lets tl in
 875     let intros = ll@(map (fun a ->
 876          step_of_substep prefix' (Assume(a,[]))) ass) in
 877       if !grow_haves then
 878         Have(list_mk_forall(flat
 879             (map (function (_,_,Let l) -> l | _ -> []) ll),
 880           itlist (curry mk_imp) ass tm), [lab],
 881         Proof (Some (step_of_substep prefix Bracket_proof),
 882           intros@
 883         [step_of_substep prefix (Qed(hole))], None))
 884       else
 885         Now([lab], Proof (None,
 886           intros@
 887           [step_of_substep prefix' (Thus(tm,[],hole))],
 888         Some (step_of_substep prefix Bracket_end))));;
 889
 890 let steps_of_goals (asl,w :goal) (_,gl,_ :goalstate) prefix n =
 891   let ass = map (concl o snd) asl in
 892   let fv = union (flat (map frees ass)) (frees w) in
 893   let rec extra_ass l l' =
 894     if subset l ass then l' else extra_ass (tl l) ((hd l)::l') in
 895   let rec steps_of_goals1 n gl =
 896     match gl with
 897     | [] -> [],[],n
 898     | (asl',w')::gl' ->
 899         let ass' = map (concl o snd) asl' in
 900         let steps',labs',n' = steps_of_goals1 (n + 1) gl' in
 901         let lab = string_of_int n in
 902         ((step_of_obligation prefix lab
 903           (subtract (union (flat (map frees ass')) (frees w')) fv)
 904           (extra_ass ass' []) w')::steps'),lab::labs',n' in
 905   steps_of_goals1 n gl;;
 906
 907 let next_growth_label = ref 0;;
 908
 909 let connect_step (step:step) labs =
 910   let comma = "",Ident ",","" in
 911   let from_key = " ",Resword "from"," " in
 912   let rec ungrow_by src l =
 913     match l with
 914     | [] -> src,[]
 915     | Grow(name,tac)::l' ->
 916        (match src with
 917         | tok1::(_,Ident "#",_)::tok2::src' ->
 918             let src'',l'' = ungrow_by src' l' in
 919             (tok1::tok2::src''),(Tactic(name,tac)::l')
 920         | _ -> failwith "ungrow_by")
 921     | x::l' -> let toks,src' = chop_list 2 src in
 922         let src'',l'' = ungrow_by src' l' in
 923         (toks@src''),(x::l'') in
 924   let rec extra_from sep labs =
 925     match labs with
 926     | [] -> []
 927     | lab::labs' -> sep::("",Ident lab,"")::extra_from comma labs' in
 928   let connect_just src4 just =
 929     match just with
 930     | By(l,l',b) ->
 931         let src4',l'' = ungrow_by src4 l in
 932         let src4'',l''' = ungrow_by src4' l' in
 933         (src4''@if labs = [] then [] else
 934           extra_from (if l' = [] then from_key else comma) labs),
 935         By(l'',(l'''@map (fun s -> Label s) labs),b)
 936     | _ -> src4,just in
 937   match step with
 938   | (e,[src1; src2; src3; src4; src5],substep) ->
 939      (match substep with
 940       | Have(x,y,just) ->
 941           let src4',just' = connect_just src4 just in
 942           (e,[src1; src2; src3; src4'; src5],Have(x,y,just'))
 943       | Thus(x,y,just) ->
 944           let src4',just' = connect_just src4 just in
 945           (e,[src1; src2; src3; src4'; src5],Thus(x,y,just'))
 946       | Qed just ->
 947           let src4',just' = connect_just src4 just in
 948           (e,[src1; src2; src3; src4'; src5],Qed just')
 949       | Consider(x,y,z,just) ->
 950           let src4',just' = connect_just src4 just in
 951           (e,[src1; src2; src3; src4'; src5],Consider(x,y,z,just'))
 952       | Cases(just,x) ->
 953           let src4',just' = connect_just src4 just in
 954           (e,[src1; src2; src3; src4'; src5],Cases(just',x))
 955       | _ -> failwith "connect_step" :step)
 956   | _ -> failwith "connect_step";;
 957
 958 let add_width n s =
 959   let rec add_width1 n s =
 960     match s with
 961     | [] -> n
 962     | "\t"::s' -> add_width1 ((n/8 + 1)*8) s'
 963     | "\n"::s' -> add_width1 0 s'
 964     | _::s' -> add_width1 (n + 1) s' in
 965   add_width1 n (explode s);;
 966
 967 let rewrap_step (e,src,substep as step:step) =
 968   let rec rewrap_from x1 src4a src4b =
 969     match src4b with
 970     | [] -> rev src4a
 971     | (x,y,z)::(x',(Resword "from" as y'),z')::rst ->
 972         (rev src4a)@(x,y,"\n")::(x1,y',z')::rst
 973     | tok::rst -> rewrap_from x1 (tok::src4a) rst in
 974   match src with
 975   | [src1; src2; src3; src4; src5] ->
 976       if src4 = [] then step else
 977       let src123 = src1@src2@src3 in
 978       let x,y,z = strings_of_toks src123 in
 979       let x',y',_ = strings_of_toks src4 in
 980       if add_width 0 (x^y^z^x'^y') > !proof_width then
 981         let a,b,_ = last src123 in
 982         let src123' = (butlast src123)@[a,b,"\n"] in
 983         let src1',src23' = chop_list (length src1) src123' in
 984         let src2',src3' = chop_list (length src2) src23' in
 985         let _,b',c' = hd src4 in
 986         let x1 = x^ !proof_indent in
 987         let src4' = (x1,b',c')::tl src4 in
 988         let src4'' =
 989           if add_width 0 (x1^y') > !proof_width then
 990             rewrap_from x1 [] src4' else src4' in
 991         (e,[src1'; src2'; src3'; src4''; src5],substep)
 992       else (step:step)
 993   | _ -> failwith "rewrap_step";;
 994
 995 let rec pp_step prefix step =
 996   let (e,_,substep) = step in
 997   let (_,src,substep') =
 998     rewrap_step (step_of_substep prefix substep) in
 999   let substep'' =
1000    (match substep' with
1001     | Have(x,y,just) -> Have(x,y,pp_just prefix just)
1002     | Now(x,just) -> Now(x,pp_just prefix just)
1003     | Thus(x,y,just) -> Thus(x,y,pp_just prefix just)
1004     | Qed(just) -> Qed(pp_just prefix just)
1005     | Consider(x,y,z,just) -> Consider(x,y,z,pp_just prefix just)
1006     | Cases(just,justl) ->
1007         Cases(pp_just prefix just,map (pp_just prefix) justl)
1008     | Error(x,just) -> Error(x,pp_just prefix just)
1009     | _ -> substep') in
1010   (e,src,substep'')
1011 and pp_just prefix just =
1012   let pp_step' step' =
1013     match step' with
1014     | Some step -> Some (pp_step prefix step)
1015     | None -> None in
1016   let prefix' = (!proof_indent)^prefix in
1017   let pp_step'' step =
1018     match step with
1019     | (_,_,Qed _) -> pp_step prefix step
1020     | (_,_,Suppose _) -> pp_step prefix step
1021     | _ -> pp_step prefix' step in
1022   match just with
1023   | Proof(step',stepl,step'') ->
1024       Proof(pp_step' step',map (pp_step'') stepl,pp_step' step'')
1025   | _ -> just;;
1026
1027 let outdent n step =
1028   let (_,src,_) = step in
1029   match flat src with
1030   | (x,_,_)::_ ->
1031       let x' = explode x in
1032       if length x' < n then step else
1033       let _,x'' = chop_list n x' in
1034       pp_step (implode x'') step
1035   | _ -> step;;
1036
1037 let replacement_steps (asl,w) f step =
1038   let n = String.length !proof_indent in
1039   let indent_of (_,src,substep) =
1040     let x,_,_ = hd (flat src) in
1041     match substep with
1042     | Qed _ -> x^ !proof_indent
1043     | _ -> x in
1044   let shift src2 src3 just =
1045     match just with
1046     | Proof _ ->
1047         if src3 <> [] then
1048           let (x,y,z) = last src3 in
1049           src2,((butlast src3)@[x,y,"\n"])
1050         else if src2 <> [] then
1051           let (x,y,z) = last src2 in
1052           ((butlast src2)@[x,y,"\n"]),src3
1053         else src2,src3
1054     | _ -> src2,src3 in
1055   let steps,labs,n = f (indent_of step) (!next_growth_label) in
1056   next_growth_label := n;
1057   if !grow_duplicates > 1 then
1058     steps@[rewrap_step (connect_step step labs)]
1059   else
1060   match steps,step with
1061   | [e,[src1'; src2'; src3'; src4'; src5'],Have(tm',_,just')],
1062     (_,[src1; src2; src3; src4; src5],Have(tm,labs,_)) when tm' = tm ->
1063       let src2'',src3'' = shift src2 src3 just' in
1064       [e,[src1; src2''; src3''; src4'; src5'],Have(tm,labs,just')]
1065   | [e,[src1'; src2'; src3'; src4'; src5'],Have(tm',_,just')],
1066     (_,[src1; src2; src3; src4; src5],Thus(tm,labs,_)) when tm' = tm ->
1067       let src2'',src3'' = shift src2 src3 just' in
1068       [e,[src1; src2''; src3''; src4'; src5'],Thus(tm,labs,just')]
1069   | [e,_,Have(tm',_,Proof(_,y,_))],
1070     (_,_,Qed(_)) when tm' = w ->
1071       map (outdent n) y
1072   | [e,[src1'; src2'; src3'; src4'; src5'],Have(tm',_,(By _ as just'))],
1073     (_,[src1; src2; src3; src4; src5],Qed(_)) when tm' = w ->
1074       [e,[src1; src2; src3; src4'; src5'],Qed(just')]
1075   | _ ->
1076   if !grow_duplicates > 0 then
1077     steps@[rewrap_step (connect_step step labs)]
1078   else
1079     let al = map (fun x,y -> concl y,x) asl in
1080     let rec filter_growth steps labs steps' labs' =
1081       match steps with
1082       | [] -> (rev steps'),(rev labs')
1083       | ((_,_,Have(tm,_,_)) as step')::rst ->
1084          (try let lab' = assoc tm al in
1085             if lab' <> "" then
1086               filter_growth rst (tl labs) steps' (lab'::labs')
1087             else
1088               filter_growth rst (tl labs) (step'::steps') ((hd labs)::labs')
1089           with _ ->
1090             filter_growth rst (tl labs) (step'::steps') ((hd labs)::labs'))
1091       | step'::rst ->
1092           filter_growth rst (tl labs) (step'::steps') ((hd labs)::labs') in
1093     let steps',labs' = filter_growth steps labs [] [] in
1094     steps'@[rewrap_step (connect_step step labs')];;
1095
1096 exception Grown of (string -> int -> step list * string list * int);;
1097
1098 let (FILTER_ASSUMS : (int * (string * thm) -> bool) -> tactic) =
1099   let rec filter' f n l =
1100     match l with
1101     | [] -> []
1102     | h::t ->
1103         let t' = filter' f (n + 1) t in
1104         if f (n,h) then h::t' else t' in
1105   fun f (asl,w) ->
1106     null_meta,[filter' f 0 asl,w],(fun i ths -> hd ths);;
1107
1108 let (MAP_ASSUMS : (string * thm -> string * thm) -> tactic) =
1109   let FIRST_ASSUM' ttac' (asl,w as g) =
1110     tryfind (fun lth -> ttac' lth g) asl in
1111   fun f ->
1112     let rec recurse g =
1113      (FIRST_ASSUM' (fun (l,th as lth) ->
1114        UNDISCH_THEN (concl th) (fun th ->
1115          recurse THEN uncurry LABEL_TAC (f lth))) ORELSE ALL_TAC) g in
1116     recurse ORELSE FAIL_TAC "MAP_ASSUMS";;
1117
1118 let (thenl':
1119     tactic -> (goal -> 'a * goalstate) list -> goal -> 'a list * goalstate) =
1120   let propagate_empty i _ = [] in
1121   let propagate_thm th i _ = INSTANTIATE_ALL i th in
1122   let compose_justs n just1 just2 i ths =
1123     let ths1,ths2 = chop_list n ths in
1124     (just1 i ths1)::(just2 i ths2) in
1125   let rec seqapply l1 l2 =
1126     match (l1,l2) with
1127     | ([],[]) -> [],(null_meta,[],propagate_empty)
1128     | (tac::tacs),(goal::goals) ->
1129             let a,((mvs1,insts1),gls1,just1) = tac goal in
1130             let goals' = map (inst_goal insts1) goals in
1131             let aa',((mvs2,insts2),gls2,just2) = seqapply tacs goals' in
1132             (a::aa'),((union mvs1 mvs2,compose_insts insts1 insts2),
1133               gls1@gls2,compose_justs (length gls1) just1 just2)
1134     | _,_ -> failwith "seqapply: Length mismatch" in
1135   let justsequence just1 just2 insts2 i ths =
1136     just1 (compose_insts insts2 i) (just2 i ths) in
1137   let tacsequence ((mvs1,insts1),gls1,just1) tacl =
1138     let aa,((mvs2,insts2),gls2,just2) = seqapply tacl gls1 in
1139     let jst = justsequence just1 just2 insts2 in
1140     let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
1141     aa,((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
1142   fun tac1 tac2l g ->
1143     let _,gls,_ as gstate = tac1 g in
1144     if gls = [] then tacsequence gstate [] else tacsequence gstate tac2l;;
1145
1146 let just_cache = ref undefined;;
1147
1148 let tactic_of_by fake l l' b =
1149  (fun (asl,_ as g) ->
1150   let hor = if b then 0 else !horizon in
1151   let rec find_tactic l =
1152     match l with
1153     | [] -> !default_prover,false
1154     | (Tactic (name, tac))::l' -> (name,tac),false
1155     | (Grow (name, tac))::l' -> (name,tac),true
1156     | _::l' -> find_tactic l' in
1157   let sets = BETA_THM::map snd (filter (fun x,_ -> x = "=") asl) in
1158   let asl' = filter (fun x,_ -> x <> "=") asl in
1159   let rec find_thms l b =
1160     match l with
1161     | [] ->
1162         if b then [] else
1163         map (PURE_REWRITE_RULE sets o snd)
1164           (try fst (chop_list hor asl') with _ -> asl')
1165     | (Thm (_, th))::l' -> th::(find_thms l' b)
1166     | (Label "*")::l' ->
1167         (map (PURE_REWRITE_RULE sets o snd) asl')@(find_thms l' b)
1168     | (Label s)::l' ->
1169         (PURE_REWRITE_RULE sets
1170           (if s = "-" then snd (hd asl') else assoc s asl'))::(find_thms l' b)
1171     | _::l' -> find_thms l' b in
1172   let rec find_labs l =
1173     match l with
1174     | [] -> []
1175     | (Label s)::l' -> s::(find_labs l')
1176     | _::l' -> find_labs l' in
1177   try
1178     let thms = find_thms l b in
1179     let thms' = find_thms l' true in
1180     let thms'' = thms@thms' in
1181     let (name,tac),grow = find_tactic (l@l') in
1182     if fake & (mem Hole l or mem Hole l') or not (!growth_mode) & grow then
1183       -2,FAKE_TAC fake thms'' g else
1184     let labs = find_labs l in
1185     let full_asl = hor < 0 or mem "*" labs in
1186    (try
1187       0,((FILTER_ASSUMS (fun _,(x,_) -> x <> "=") THEN
1188         FILTER_ASSUMS
1189          (fun n,(x,_) ->
1190             mem x labs or n < hor or (n = 0 & mem "-" labs) or full_asl) THEN
1191         MAP_ASSUMS (fun l,th -> l,PURE_REWRITE_RULE sets th) THEN
1192         MIZAR_NEXT' (PURE_REWRITE_TAC sets) THEN
1193        (fun (asl',w' as g') ->
1194           let key = name,(map concl thms,map concl thms'),w' in
1195           try
1196             if grow then failwith "apply";
1197             let e,th = apply (!just_cache) key in
1198             if e = 0 then (ACCEPT_TAC th THEN NO_TAC) g' else
1199             if e = 2 then raise Timeout else failwith "cached by"
1200           with
1201           | Failure "apply" ->
1202               try
1203                 let (_,_,just as gs) =
1204                  ((fun g'' ->
1205                     let gs' = TIMED_TAC (!timeout) (tac thms) g'' in
1206                     if grow then raise (Grown (steps_of_goals g gs'))
1207                             else gs') THEN
1208                   REPEAT (fun (asl'',_ as g'') ->
1209                     if subset asl'' asl' then NO_TAC g''
1210                     else FIRST_ASSUM (UNDISCH_TAC o concl) g'') THEN
1211                   TRY (FIRST (map ACCEPT_TAC thms'')) THEN
1212                   REWRITE_TAC thms'' THEN NO_TAC) g' in
1213                 let th = just null_inst [] in
1214                 just_cache := (key |-> (0,th)) !just_cache;
1215                 gs
1216               with
1217               | Grown _ as x -> raise x
1218               | x -> if name <> "GOAL_TAC" then just_cache :=
1219                     (key |-> ((if x = Timeout then 2 else 1),TRUTH))
1220                       !just_cache;
1221                   raise x
1222         )) g)
1223     with
1224     | Grown _ as x -> raise x
1225     | x -> (if x = Timeout then 2 else 1),(FAKE_TAC fake thms'' g))
1226   with Failure "find" | Failure "hd" -> 4,(FAKE_TAC fake [] g)
1227   : goal -> int * goalstate);;
1228
1229 let LABELS_TAC ls th =
1230   if ls = [] then ASSUME_TAC th else
1231   EVERY (map (fun l -> LABEL_TAC l th) ls);;
1232
1233 let PURE_EXACTLY_ONCE_REWRITE_TAC =
1234   let ONCE_COMB_QCONV conv tm =
1235     let l,r = dest_comb tm in
1236     try let th1 = conv l in AP_THM th1 r
1237     with Failure _ -> AP_TERM l (conv r) in
1238   let ONCE_SUB_QCONV conv tm =
1239     if is_abs tm then ABS_CONV conv tm
1240     else ONCE_COMB_QCONV conv tm in
1241   let rec EXACTLY_ONCE_DEPTH_QCONV conv tm =
1242       (conv ORELSEC (ONCE_SUB_QCONV (EXACTLY_ONCE_DEPTH_QCONV conv))) tm in
1243   let PURE_EXACTLY_ONCE_REWRITE_CONV thl =
1244     GENERAL_REWRITE_CONV false EXACTLY_ONCE_DEPTH_QCONV empty_net thl in
1245   fun thl ->
1246     CONV_TAC(PURE_EXACTLY_ONCE_REWRITE_CONV thl);;
1247
1248 let EQTF_INTRO =
1249   let lemma = TAUT `(~t <=> T) <=> (t <=> F)` in
1250   fun th ->
1251     PURE_ONCE_REWRITE_RULE[lemma] (EQT_INTRO th);;
1252
1253 let REWRITE_THESIS_TAC =
1254   let PROP_REWRITE_TAC =
1255     PURE_REWRITE_TAC[AND_CLAUSES; IMP_CLAUSES; NOT_CLAUSES; OR_CLAUSES;
1256       prop_2; TAUT `!t. (t <=> t) <=> T`] in
1257   fun th ->
1258     PURE_EXACTLY_ONCE_REWRITE_TAC[EQTF_INTRO th] THEN PROP_REWRITE_TAC;;
1259
1260 let thesis_var = `thesis:bool`;;
1261
1262 let rec tactic_of_step fake step (asl,w as g) =
1263   let justify tac just g =
1264     let (mvs,inst),gls,jst = tac g in
1265    (match gls with
1266     | [g1; g2] ->
1267         let (e,just'),((mvs',inst'),gls',jst') =
1268           tactic_of_just fake just g1 in
1269         let mvs'' = union mvs' mvs in
1270         let inst'' = compose_insts inst' inst in
1271         let gls'' = gls'@[g2] in
1272         let jst'' i ths =
1273           jst (compose_insts inst'' i) [jst' i (butlast ths); last ths] in
1274         (e,just'),((mvs'',inst''),gls'',jst'')
1275     | _ -> failwith "justify") in
1276   let SUBGOAL_THEN' tm tac =
1277     let th = fix_dots' asl tm in
1278     let lhs,_ = dest_eq (concl th) in
1279     SUBGOAL_THEN lhs tac THENL [MIZAR_NEXT' (CONV_TAC (K th)); ALL_TAC] in
1280   let fix_thesis tm = vsubst [w,thesis_var] tm in
1281   let e,src,substep = step in
1282     match substep with
1283     | Let tl ->
1284        (try (0,src,substep),(MAP_EVERY X_GEN_TAC tl g)
1285         with x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1286     | Assume (tm, l) | Suppose (tm, l) ->
1287        (try (0,src,substep),(DISJ_CASES_THEN2
1288          (fun th -> MIZAR_NEXT' (REWRITE_THESIS_TAC th) THEN
1289             LABELS_TAC l th)
1290          (fun th ->
1291             let th' = PURE_REWRITE_RULE[NOT_CLAUSES; IMP_CLAUSES] th in
1292             REWRITE_TAC[th'] THEN CONTR_TAC th' THEN NO_TAC)
1293           (SPEC (fix_thesis tm) EXCLUDED_MIDDLE) g)
1294         with x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1295     | Have (tm, l, just) ->
1296        (try let (e,just'),gs =
1297             justify (SUBGOAL_THEN' (fix_thesis tm) (LABELS_TAC l)) just g in
1298          (e,src,Have(tm, l, just')),gs
1299         with x -> raise x)
1300     | Now (l, just) ->
1301        (try let (e,just'),gs =
1302             justify (SUBGOAL_THEN (term_of_now just) (LABELS_TAC l)) just g in
1303          (e,src,Now(l, just')),gs
1304         with x -> raise x)
1305     | Thus (tm, l, just) ->
1306        (try let (e,just'),gs =
1307             justify (SUBGOAL_THEN' (fix_thesis tm) (LABELS_TAC l) THENL
1308               [ALL_TAC; MIZAR_NEXT'
1309                  (FIRST_ASSUM (fun th ->
1310                     EVERY (map (fun th' -> REWRITE_THESIS_TAC th')
1311                       (CONJUNCTS th))))])
1312               just g in
1313          (e,src,Thus(tm, l, just')),gs
1314         with x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1315     | Qed just ->
1316        (try let (e,just'),gs = tactic_of_just fake just g in
1317          (e,src,substep),gs
1318         with x -> raise x)
1319     | Take tm ->
1320        (try (0,src,substep),(EXISTS_TAC tm g)
1321         with x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1322     | Consider (tl, tm, l, just) ->
1323         let tm' = itlist (curry mk_exists) tl (fix_thesis tm) in
1324        (try let (e,just'),gs =
1325             justify (SUBGOAL_THEN tm'
1326             ((EVERY_TCL (map X_CHOOSE_THEN tl)) (LABELS_TAC l))) just g in
1327           (e,src,Consider(tl, tm, l, just')),gs
1328         with x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1329     | Set (tm, l) ->
1330        (try
1331           let v,_ = dest_eq tm in
1332           let tm' = mk_exists(v,tm) in
1333           let l' = if l = [] then ["="] else l in
1334          (0,src,substep),
1335          ((SUBGOAL_THEN tm' (X_CHOOSE_THEN v (LABELS_TAC l')) THENL
1336            [REWRITE_TAC[EXISTS_REFL] ORELSE FAKE_TAC fake []; ALL_TAC]) g)
1337         with x -> raise x)
1338     | Cases (just, cases) ->
1339        (try
1340           let l,tm = terms_of_cases cases in
1341           let steps,gs =
1342            (thenl' (SUBGOAL_THEN tm
1343              (EVERY_TCL
1344                (map (K (DISJ_CASES_THEN2
1345                  (fun th -> ASSUME_TAC th THEN
1346                     FIRST_ASSUM (UNDISCH_TAC o concl)))) l) CONTR_TAC))
1347          ((tactic_of_just fake just)::
1348            (map (fun just -> tactic_of_just fake just) cases)) g) in
1349          (match steps with
1350           | (e,just')::ecases' -> (e,src,Cases(just',map snd ecases')),gs
1351           | _ -> failwith "tactic_of_step")
1352         with x -> raise x)
1353     | Bracket_proof | Bracket_end | Bracket_case ->
1354        (3,src,substep),(ALL_TAC g)
1355     | Exec(_,tac) ->
1356        (try (0,src,substep),(TIMED_TAC (!timeout) tac THENL [ALL_TAC]) g
1357         with
1358         | Timeout as x -> if fake then (2,src,substep),(ALL_TAC g) else raise x
1359         | x -> if fake then (3,src,substep),(ALL_TAC g) else raise x)
1360     | Error (_,_) | Error_point ->
1361         if fake then (e,src,substep),(ALL_TAC g) else failwith "tactic_of_step"
1362     | Empty_step ->
1363        (0,src,substep),(ALL_TAC g)
1364
1365 and tactic_of_just fake just g =
1366   let bracket_step step e =
1367     match step with
1368     | None -> if e = 0 then None else Some (e, [], Error_point)
1369     | Some (_, src, substep) -> Some (e, src, substep) in
1370   let rec tactic_of_just1 l (_,w as g) =
1371     match l with
1372     | [] ->
1373         if is_const w && fst (dest_const w) = "T"
1374           then [],0,ACCEPT_TAC TRUTH g
1375           else [],3,FAKE_TAC fake (map snd (fst g)) g
1376     | step::l' ->
1377        (try
1378           let step',((mvs,inst),gls,just) =
1379             MIZAR_NEXT (tactic_of_step fake step) g in
1380          (match gls with
1381           | [g'] ->
1382               let l'',e,((mvs',inst'),gls',just') = tactic_of_just1 l' g' in
1383               let mvs'' = union mvs' mvs in
1384               let inst'' = compose_insts inst' inst in
1385               let gls'' = gls' in
1386               let just'' i ths = just (compose_insts inst'' i) [just' i ths] in
1387               step'::l'',e,((mvs'',inst''),gls'',just'')
1388           | _ -> failwith "tactic_of_just")
1389         with Grown f ->
1390           tactic_of_just1 (replacement_steps g f step@l') g) in
1391   match just with
1392   | By(l,l',b) -> let e,gs = tactic_of_by fake l l' b g in (e,just),gs
1393   | Proof(step1, l, step2) ->
1394       let l',e,gs = tactic_of_just1 l g in
1395       (0,Proof(bracket_step step1 0, l', bracket_step step2 e)),gs
1396   | _ -> failwith "tactic_of_just";;
1397
1398 let parse_qproof s = steps_of_toks (fix_semi (tl (lex2 s)));;
1399
1400 let rec src_of_step (e,src,substep) =
1401   [e,strings_of_toks (flat src)]@
1402   match substep with
1403   | Have(_, _, just) -> src_of_just just
1404   | Now(_, just) -> src_of_just just
1405   | Thus(_, _, just) -> src_of_just just
1406   | Qed just -> src_of_just just
1407   | Consider(_, _, _, just) -> src_of_just just
1408   | Cases(just, cases) ->
1409       (src_of_just just)@(itlist (@) (map src_of_just cases) [])
1410   | Error(_, just) -> src_of_just just
1411   | _ -> []
1412
1413 and src_of_just just =
1414   let unpack step1 =
1415     match step1 with
1416     | Some step -> src_of_step step
1417     | _ -> [] in
1418   match just with
1419   | Proof(step1, steps, step2) ->
1420       (unpack step1)@(itlist (@) (map src_of_step steps) [])@(unpack step2)
1421   | _ -> [];;
1422
1423 let src_of_steps steps = itlist (@) (map src_of_step steps) [];;
1424
1425 let count_errors src =
1426   let rec count_errors1 src (n1,n2,n3) =
1427     match src with
1428     | [] -> n1,n2,n3
1429     | (e,_)::src' -> count_errors1 src'
1430        (if e > 2 then (n1 + 1,n2,n3) else
1431         if e > 0 then (n1,n2 + 1,n3) else
1432         if e = -2 then (n1,n2,n3 + 1) else
1433           (n1,n2,n3)) in
1434   count_errors1 src (0,0,0);;
1435
1436 let error_line l ee =
1437   let rec error_line1 s1 s2 n l ee =
1438     match l with
1439     | [] -> (s1^"\n"),s2,ee
1440     | (m,e)::l' ->
1441         let d = m - n - 1 in
1442         let d' = if d > 0 then d else 0 in
1443         let s' = "#"^string_of_int e in
1444         error_line1 (s1^(implode (replicate " " d'))^s')
1445          (if !explain_errors > 0 then
1446             if mem e ee then s2 else s2^":: "^(el (e - 1) ERRORS)^"\n"
1447           else s2)
1448          (add_width (n + d') s') l' (union ee [e]) in
1449   let s1,s2,ee' =
1450     error_line1 "::" "" 2 l (if !explain_errors > 1 then [] else ee) in
1451   (s1^s2),ee';;
1452
1453 let insert_errors n s l ee =
1454   let rec insert_errors1 n s l ee =
1455     match s with
1456     | [] -> [],n,l,ee
1457     | ("\n" as c)::s' ->
1458         let s1,ee' = if l = [] then "",ee else error_line l ee in
1459         let s2,n1,l1,ee' = insert_errors1 0 s' [] ee' in
1460         (c::s1::s2),n1,l1,ee'
1461     | c::s' ->
1462         let s1,n1,l1,ee' = insert_errors1 (add_width n c) s' l ee in
1463           (c::s1),n1,l1,ee' in
1464   let s1,n1,l1,ee' = insert_errors1 n (explode s) l ee in
1465   (implode s1),n1,l1,ee';;
1466
1467 let string_of_src m steps =
1468   let add_error l n e =
1469     if e > (if !sketch_mode then 2 else 0) then l@[n,e] else l in
1470   let rec string_of_src1 s n l s3' steps ee =
1471     match steps with
1472     | [] ->
1473         let s',n',l',ee' = insert_errors n s3' l ee in
1474         if l' = [] then s^s' else
1475           let s'',_,_,_ = insert_errors n' "\n" l' ee' in
1476           s^s'^s''
1477     | (e,(s1,"",s3))::steps' ->
1478         string_of_src1 s n (add_error l n e) (s3'^s1^s3) steps' ee
1479     | (e,(s1,s2,s3))::steps' ->
1480         let s',n',l',ee' = insert_errors n (s3'^s1) l ee in
1481         let n'' = add_width n' s2 in
1482         string_of_src1 (s^s'^s2) n'' (add_error l' n'' e) s3 steps' ee' in
1483   string_of_src1 "" m [] "" steps [];;
1484
1485 let print_boxed f s =
1486   let print_boxed_char c =
1487     if c = "\n"
1488       then Format.pp_print_cut f ()
1489       else Format.pp_print_string f c in
1490   Format.pp_open_vbox f 0;
1491   do_list print_boxed_char (explode s);
1492   Format.pp_close_box f ();;
1493
1494 let print_step f x =
1495   print_boxed f (string_of_src 0 (src_of_step x));;
1496
1497 let print_qsteps f x =
1498   print_boxed f ("`;\n"^(string_of_src 0 (src_of_steps x))^"`");;
1499
1500 #install_printer print_step;;
1501 #install_printer print_qsteps;;
1502
1503 let GOAL_TAC g =
1504   current_goalstack := (mk_goalstate g)::!current_goalstack;
1505   ALL_TAC g;;
1506
1507 let GOAL_FROM x = fun y -> x y THEN GOAL_TAC;;
1508
1509 let ee s =
1510   let toks = lex2 s in
1511   let l,t = top_goal() in
1512   let env = itlist union (map frees l) (frees t) in
1513   let proof,step1,rst = steps_of_toks1 true false env toks in
1514   if rst <> [] or step1 <> None then failwith "ee" else
1515   (e o EVERY o map (fun step -> snd o tactic_of_step false step)) proof;;
1516
1517 let check_proof steps =
1518   let step =
1519     match steps with
1520     | [_,_,Have (_, _, _) as step] -> step
1521     | [_,_,Now (_, _) as step] -> step
1522     | _ ->
1523         -1,[],Now([], Proof(None,steps,
1524             Some(-1,[],Bracket_end))) in
1525   let step',gs = tactic_of_step true step ([],thesis_var) in
1526   let steps' =
1527     match step' with
1528     | _,[],Now(_, Proof(_,steps',_)) -> steps'
1529     | step' -> [step'] in
1530   let _,gl,j = gs in
1531   if length gl <> 1 then failwith "thm" else
1532   let (asl,w) = hd gl in
1533   if length asl <> 1 or w <> thesis_var then failwith "thm" else
1534   let a = (concl o snd o hd) asl in
1535   let src' = src_of_steps steps' in
1536   steps',count_errors src',j ([],[a,thesis_var],[]) [ASSUME a];;
1537
1538 exception Mizar_error of step list * (int * int * int);;
1539
1540 let thm steps =
1541   let steps',(n1,n2,n3 as n),th = check_proof steps in
1542   if n1 + n2 + n3 = 0 then th else raise (Mizar_error(steps',n));;
1543
1544 let thm_of_string = thm o parse_proof;;
1545
1546 let rec labels_of_steps labels context steps =
1547   match steps with
1548   | [] -> labels
1549   | (_,_,substep)::rst ->
1550      (match substep with
1551       | Assume(_,labs) | Suppose(_,labs) | Set(_,(_::_ as labs)) ->
1552           let label = (labs,ref 0) in
1553           labels_of_steps (label::labels) (label::context) rst
1554       | Have(_,labs,just) | Thus(_,labs,just) | Consider(_,_,labs,just)
1555       | Now(labs,just) ->
1556           let label = (labs,ref 0) in
1557           let labels1 = labels_of_just (label::labels) context just in
1558           labels_of_steps labels1 (label::context) rst
1559       | Qed(just) ->
1560           let labels1 = labels_of_just labels context just in
1561           labels_of_steps labels1 context rst
1562       | Cases(just,justl) ->
1563           itlist
1564             (fun just' labels' -> labels_of_just labels' context just')
1565             (rev justl) (labels_of_just labels context just)
1566       | Error(_,_) -> raise Noparse
1567       | _ -> labels_of_steps labels context rst)
1568
1569 and labels_of_just labels context just =
1570   let rec collect_strings l =
1571     match l with
1572     | [] -> []
1573     | Label(s)::l' -> s::collect_strings l'
1574     | _::l' -> collect_strings l' in
1575   match just with
1576   | Proof(_,steps,_) -> labels_of_steps labels context steps
1577   | By(x,y,_) ->
1578       do_list (fun s ->
1579           do_list (fun _,n -> n := !n + 1) (filter (mem s o fst) context))
1580         (subtract (collect_strings (x@y)) ["-"; "*"]);
1581       labels
1582   | _ -> labels;;
1583
1584 let isnumber = forall isnum o explode;;
1585
1586 let max_label labels = itlist max
1587   (map int_of_string (filter isnumber (flat (map fst labels)))) (-1);;
1588
1589 let rec number_labels n labels =
1590   match labels with
1591   | [] -> []
1592   | (oldlabs,count)::rst ->
1593       let newlabs,n' =
1594        (if !extra_labels > 1 or !count > 0 or
1595           (!extra_labels > 0 & exists isnumber oldlabs)
1596         then [string_of_int n],(n + 1) else [],n) in
1597       (oldlabs,newlabs)::(number_labels n' rst);;
1598
1599 let rec renumber_steps labels context steps =
1600   let make_lab x1 y1 x2 y2 x3 y3 s =
1601     ([x1,Resword "[",y1; x2,Ident s,y2; x3,Resword "]",y3],[s]) in
1602   let rec renumber_labs b w src labs label =
1603     match labs with
1604     | [] ->
1605         if b then (make_lab "" "" "" "" "" w (hd (snd label)))," "
1606           else ([],[]),w
1607     | lab::rst when isnumber lab ->
1608        (match src with
1609         | (x1,Resword "[",y1)::(x2,Ident s',y2)::(x3,Resword "]",y3)::rstsrc ->
1610             let (src',labs'),w' = renumber_labs false y3 rstsrc rst label in
1611             let newsrc,newlabs =
1612               if b then make_lab x1 y1 x2 y2 x3 w' (hd (snd label))
1613               else [],[] in
1614             ((newsrc@src'),(newlabs@labs')),if b then w else y3
1615         | _ -> failwith "renumber_labs")
1616     | lab::rst ->
1617        (match src with
1618         | tok1::tok2::(x3,y3,z3)::rstsrc ->
1619             let (src',labs'),w' = renumber_labs b z3 rstsrc rst label in
1620             ((tok1::tok2::(x3,y3,w')::src'),(lab::labs')),w
1621         | _ -> failwith "renumber_labs") in
1622   let renumber_labs1 b src1 src labs label =
1623     let (x,y,w) = last src1 in
1624     let (src',labs'),w' = renumber_labs b w src labs label in
1625     let src1' = if w' <> w then (butlast src1)@[x,y,w'] else src1 in
1626     src1',src',labs' in
1627   match steps with
1628   | [] -> labels,[]
1629   | (e,src,substep)::rst ->
1630      (match src with
1631       | [src1; src2; src3; src4; src5] ->
1632          (match substep with
1633           | Assume(x,labs) ->
1634               let label = hd labels in
1635               let src2',src3',labs' =
1636                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1637               let labels',rst' =
1638                 renumber_steps (tl labels) (label::context) rst in
1639               labels',
1640               (e,[src1; src2'; src3'; src4; src5],Assume(x,labs'))::rst'
1641           | Suppose(x,labs) ->
1642               let label = hd labels in
1643               let src2',src3',labs' =
1644                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1645               let labels',rst' =
1646                 renumber_steps (tl labels) (label::context) rst in
1647               labels',
1648               (e,[src1; src2'; src3'; src4; src5],Suppose(x,labs'))::rst'
1649           | Set(x,(_::_ as labs)) ->
1650               let label = hd labels in
1651               let src2',src3',labs' =
1652                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1653               let labels',rst' =
1654                 renumber_steps (tl labels) (label::context) rst in
1655               labels',
1656               (e,[src1; src2'; src3'; src4; src5],Set(x,labs'))::rst'
1657           | Have(x,labs,just) ->
1658               let label = hd labels in
1659               let src2',src3',labs' =
1660                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1661               let labels',src4',just' =
1662                 renumber_just (tl labels) context src4 just in
1663               let labels'',rst' =
1664                 renumber_steps labels' (label::context) rst in
1665               labels'',
1666                 ((e,[src1; src2'; src3'; src4'; src5],Have(x,labs',just'))::
1667                  rst')
1668           | Thus(x,labs,just) ->
1669               let label = hd labels in
1670               let src2',src3',labs' =
1671                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1672               let labels',src4',just' =
1673                 renumber_just (tl labels) context src4 just in
1674               let labels'',rst' =
1675                 renumber_steps labels' (label::context) rst in
1676               labels'',
1677                 ((e,[src1; src2'; src3'; src4'; src5],Thus(x,labs',just'))::
1678                  rst')
1679           | Qed(just) ->
1680               let labels',src4',just' =
1681                 renumber_just labels context src4 just in
1682               let labels'',rst' =
1683                 renumber_steps labels' context rst in
1684               labels'',
1685                 ((e,[src1; src2; src3; src4'; src5],Qed(just'))::
1686                  rst')
1687           | Consider(x,y,labs,just) ->
1688               let label = hd labels in
1689               let src2',src3',labs' =
1690                 renumber_labs1 (snd label <> []) src2 src3 labs label in
1691               let labels',src4',just' =
1692                 renumber_just (tl labels) context src4 just in
1693               let labels'',rst' =
1694                 renumber_steps labels' (label::context) rst in
1695               labels'',
1696                 ((e,[src1; src2'; src3'; src4'; src5],
1697                   Consider(x,y,labs',just'))::
1698                  rst')
1699           | Now(labs,just) ->
1700               let label = hd labels in
1701               let src1',src3',labs' =
1702                 renumber_labs1 (snd label <> []) src1 src3 labs label in
1703               let labels',src4',just' =
1704                 renumber_just (tl labels) context src4 just in
1705               let labels'',rst' =
1706                 renumber_steps labels' (label::context) rst in
1707               labels'',
1708                 ((e,[src1'; src2; src3'; src4'; src5],Now(labs',just'))::
1709                  rst')
1710           | Cases(just,justl) ->
1711               let labels',src4',just' =
1712                 renumber_just labels context src4 just in
1713               let labels'',justl'' =
1714                 itlist
1715                   (fun just' (labels',justl') ->
1716                     let labels'',_,just'' =
1717                       renumber_just labels' context [] just' in
1718                     labels'',(just''::justl'))
1719                   (rev justl) (labels',[]) in
1720               let labels''',rst' =
1721                 renumber_steps labels'' context rst in
1722               labels''',
1723                 ((e,[src1; src2; src3; src4'; src5],Cases(just',rev justl''))::
1724                  rst')
1725           | Error(_,_) -> raise Noparse
1726           | _ ->
1727               let labels',rst' = renumber_steps labels context rst in
1728               labels',((e,src,substep)::rst'))
1729       | _ -> failwith "renumber_steps")
1730
1731 and renumber_just labels context src just =
1732   let rec renumber_by src l =
1733     match l with
1734     | [] -> [],src,[]
1735     | (Label s as x)::l' when isnumber s ->
1736        (match src with
1737         | tok::(x1,Ident _,x2 as tok')::src23 ->
1738             let labs = flat (map snd (filter (mem s o fst) context)) in
1739             let src2,src3,l'' = renumber_by src23 l' in
1740             if labs = [] then (tok::tok'::src2),src3,(x::l'') else
1741             let items = map (fun s -> Label s) labs in
1742             let labs' = tl labs in
1743             let src1 = flat (map
1744               (fun s -> ["",Ident ",",""; "",Ident s,x2]) labs') in
1745             (tok::(x1,Ident (hd labs),
1746                    if labs' = [] then x2 else "")::src1@src2),src3,(items@l'')
1747         | _ -> failwith "renumber_by")
1748     | x::l' ->
1749         let src1,src23 =
1750          (match src with
1751           | tok::(_,Ident "#",_ as tok1)::(_,Ident s,_ as tok2)::src23
1752               when s <> "," -> [tok;tok1;tok2],src23
1753           | tok::(_,Ident _,_ as tok')::src23 -> [tok;tok'],src23
1754           | _ -> failwith "renumber_by") in
1755         let src2,src3,l'' = renumber_by src23 l' in
1756         (src1@src2),src3,(x::l'') in
1757   match just with
1758   | Proof(x,steps,z) ->
1759       let labels',steps' = renumber_steps labels context steps in
1760       labels',src,Proof(x,steps',z)
1761   | By(x,y,z) ->
1762       let src1',src2,x' = renumber_by src x in
1763       let src2',_,y' = renumber_by src2 y in
1764       labels,(src1'@src2'),By(x',y',z)
1765   | _ -> labels,src,just;;
1766
1767 let renumber_steps1 steps =
1768   let labels = rev (labels_of_steps [] [] steps) in
1769   let labels' = number_labels (!start_label) labels in
1770   snd (renumber_steps labels' [] steps);;
1771
1772 let VERBOSE_TAC : bool -> tactic -> tactic =
1773   fun v tac g  ->
1774     let call f x =
1775       let v' = !verbose in verbose := v;
1776       let y = (try f x with e -> verbose := v'; raise e) in
1777       verbose := v'; y in
1778     let (mvs,insts),gls,just = call tac g in
1779     (mvs,insts),gls,(call just);;
1780
1781 let last_thm_internal = ref None;;
1782 let last_thm_internal' = ref None;;
1783
1784 let last_thm () =
1785   match !last_thm_internal with
1786   | Some th -> last_thm_internal := None; th
1787   | None -> failwith "last_thm";;
1788
1789 let check_file_verbose name lemma =
1790   let l = String.length name in
1791   if l >= 3 & String.sub name (l - 3) 3 = ".ml" then
1792    (let _ = exec_phrase false ("loadt \""^name^"\";;") in
1793     (0,0,0),TRUTH)
1794   else
1795  (last_thm_internal := None;
1796   let file = Pervasives.open_in name in
1797   let n = in_channel_length file in
1798   let s = String.create n in
1799   really_input file s 0 n;
1800   close_in file;
1801   let t,x,y = try
1802     let steps = parse_proof s in
1803    (if !growth_mode then
1804       try next_growth_label := 1 + max_label (labels_of_steps [] [] steps)
1805       with _ -> ());
1806     let steps',((n1,n2,n3) as x),y = if !silent_server > 0 then
1807         let oldstdout = Unix.dup Unix.stdout in
1808         let cleanup () = Unix.dup2 oldstdout Unix.stdout in
1809         let newstdout = Unix.openfile "/dev/null" [wronly] 0 in
1810         Unix.dup2 newstdout Unix.stdout;
1811         try
1812           let x = check_proof steps in cleanup(); x
1813         with e -> cleanup(); raise e
1814       else check_proof steps in
1815     let steps'' = if !renumber_labels then
1816       try renumber_steps1 steps' with Noparse -> steps' else steps' in
1817     let y' = if n1 + n2 + n3 = 0 then y else ASSUME (concl y) in
1818     last_thm_internal := Some y;
1819     last_thm_internal' := Some y';
1820    (match lemma with
1821     | Some s ->
1822         let _ = exec_phrase (!silent_server < 2 & n1 + n2 + n3 = 0)
1823          ("let "^s^" = "^
1824           "match !last_thm_internal' with Some y -> y | None -> TRUTH;;") in
1825         by_item_cache := undefined;
1826     | None -> ());
1827     string_of_src 0 (src_of_steps steps''),x,y
1828   with _ -> ("::#"^"10\n:: 10: MIZ3 EXCEPTION\n"^s),(1,0,0),TRUTH in
1829   let file = open_out name in
1830   output_string file t;
1831   close_out file;
1832   x,y);;
1833
1834 let check_file name =
1835   let (n1,n2,n3),th = check_file_verbose name None in
1836   if n1 + n2 + n3 = 0 then th else
1837     failwith (string_of_int n1^"+"^string_of_int n2^"+"^string_of_int n3^
1838       " errors");;
1839
1840 usr2_handler :=
1841   fun () ->
1842     let cleanup () = let _ = Unix.system ("rm -f "^(!miz3_filename)) in () in
1843     try
1844       let namefile = Pervasives.open_in !miz3_filename in
1845       let name = input_line namefile in
1846       let lemma = try Some (input_line namefile) with End_of_file -> None in
1847       close_in namefile;
1848       let _ = check_file_verbose name lemma in cleanup()
1849     with _ -> cleanup();;
1850
1851 let exit_proc = ref (fun () -> ());;
1852
1853 let server_up () =
1854   if Unix.fork() = 0 then
1855    (exit_proc := (fun () -> ());
1856    (try
1857       let pidfile = open_out !miz3_pid in
1858       output_string pidfile ((string_of_int (Unix.getppid()))^"\n");
1859       close_out pidfile
1860     with _ -> print_string "server_up failed\n");
1861     exit 0)
1862   else let _ = Unix.wait() in ();;
1863
1864 let server_down () =
1865   if Unix.fork() = 0 then
1866    (exit_proc := (fun () -> ());
1867    (try
1868       let pidfile = Pervasives.open_in !miz3_pid in
1869       let pid_string = input_line pidfile in
1870       close_in pidfile;
1871       if pid_string <> string_of_int (Unix.getppid())
1872         then failwith "server_down" else
1873       let _ = Unix.system ("rm -f "^(!miz3_pid)) in ()
1874     with _ -> print_string "server_down failed\n");
1875     exit 0)
1876   else let _ = Unix.wait() in ();;
1877
1878 server_up();;
1879 exit_proc := server_down;;
1880 at_exit (fun _ -> !exit_proc ());;
1881
1882 let reset_miz3 h =
1883   horizon := h;
1884   timeout := 1;
1885   default_prover := ("HOL_BY", CONV_TAC o HOL_BY);
1886   sketch_mode := false;
1887   just_cache := undefined;
1888   by_item_cache := undefined;
1889   current_goalstack := [];
1890   server_up();;