diff -r bce3de79c8ce -r 6ca79a354c51 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Jul 20 08:46:17 2011 +0200 +++ b/src/HOL/Import/proof_kernel.ML Wed Jul 20 10:11:08 2011 +0200 @@ -129,7 +129,7 @@ fun to_hol_thm th = HOLThm ([], th) val replay_add_dump = add_dump -fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy) +fun add_dump s thy = replay_add_dump s thy datatype proof_info = Info of {disk_info: (string * string) option Unsynchronized.ref} @@ -303,85 +303,14 @@ handle PK _ => thyname) val get_name : (string * string) list -> string = Lib.assoc "n" -local - open LazyScan - infix 7 |-- --| - infix 5 :-- -- ^^ - infix 3 >> - infix 0 || -in exception XML of string datatype xml = Elem of string * (string * string) list * xml list datatype XMLtype = XMLty of xml | FullType of hol_type datatype XMLterm = XMLtm of xml | FullTerm of term -fun pair x y = (x,y) - -fun scan_id toks = - let - val (x,toks2) = one Char.isAlpha toks - val (xs,toks3) = any Char.isAlphaNum toks2 - in - (String.implode (x::xs),toks3) - end - -fun scan_string str c = - let - fun F [] toks = (c,toks) - | F (c::cs) toks = - case LazySeq.getItem toks of - SOME(c',toks') => - if c = c' - then F cs toks' - else raise SyntaxError - | NONE => raise SyntaxError - in - F (String.explode str) - end - -local - val scan_entity = - (scan_string "amp;" #"&") - || scan_string "quot;" #"\"" - || scan_string "gt;" #">" - || scan_string "lt;" #"<" - || scan_string "apos;" #"'" -in -fun scan_nonquote toks = - case LazySeq.getItem toks of - SOME (c,toks') => - (case c of - #"\"" => raise SyntaxError - | #"&" => scan_entity toks' - | c => (c,toks')) - | NONE => raise SyntaxError -end - -val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >> - String.implode - -val scan_attribute = scan_id -- $$ #"=" |-- scan_string - -val scan_start_of_tag = $$ #"<" |-- scan_id -- - repeat ($$ #" " |-- scan_attribute) - -fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks - -val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">" - -fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >> - (fn (chldr,id') => if id = id' - then chldr - else raise XML "Tag mismatch") -and scan_tag toks = - let - val ((id,atts),toks2) = scan_start_of_tag toks - val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2 - in - (Elem (id,atts,chldr),toks3) - end -end +fun xml_to_import_xml (XML.Elem ((n, l), ts)) = Elem (n, l, map xml_to_import_xml ts) + | xml_to_import_xml (XML.Text _) = raise XML "Incorrect proof file: text"; val type_of = Term.type_of @@ -473,7 +402,6 @@ let val _ = Unsynchronized.inc invented_isavar val t = "u_" ^ string_of_int (!invented_isavar) - val _ = ImportRecorder.protect_varname s t val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) in t @@ -927,7 +855,7 @@ fun import_proof_concl thyname thmname thy = let val is = TextIO.openIn(proof_file_name thyname thmname thy) - val (proof_xml,_) = scan_tag (LazySeq.of_instream is) + val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is)) val _ = TextIO.closeIn is in case proof_xml of @@ -948,7 +876,7 @@ fun import_proof thyname thmname thy = let val is = TextIO.openIn(proof_file_name thyname thmname thy) - val (proof_xml,_) = scan_tag (LazySeq.of_instream is) + val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is)) val _ = TextIO.closeIn is in case proof_xml of @@ -1292,8 +1220,6 @@ val hth as HOLThm args = mk_res th val thy' = thy |> add_hol4_theorem thyname thmname args |> add_hol4_mapping thyname thmname isaname - val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args) - val _ = ImportRecorder.add_hol_mapping thyname thmname isaname in (thy',SOME hth) end @@ -1364,7 +1290,6 @@ val rew = rewrite_hol4_term (concl_of th) thy val th = Thm.equal_elim rew th val thy' = add_hol4_pending thyname thmname args thy - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val th = disambiguate_frees th val th = Object_Logic.rulify th val thy2 = @@ -1920,17 +1845,14 @@ val csyn = mk_syn thy constname val thy1 = case HOL4DefThy.get thy of Replaying _ => thy - | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; - Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy) + | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy val eq = mk_defeq constname rhs' thy1 val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1 - val _ = ImportRecorder.add_defs thmname eq val def_thm = hd thms val thm' = def_thm RS meta_eq_to_obj_eq_thm val (thy',th) = (thy2, thm') val fullcname = Sign.intern_const thy' constname val thy'' = add_hol4_const_mapping thyname constname true fullcname thy' - val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'') val rew = rewrite_hol4_term eq thy'' val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) @@ -1958,13 +1880,10 @@ | NONE => raise ERR "new_definition" "Bad conclusion" val fullname = Sign.full_bname thy22 thmname val thy22' = case opt_get_output_thy thy22 of - "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; - add_hol4_mapping thyname thmname fullname thy22) + "" => add_hol4_mapping thyname thmname fullname thy22 | output_thy => let val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname - val _ = ImportRecorder.add_hol_move fullname moved_thmname - val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname in thy22 |> add_hol4_move fullname moved_thmname |> add_hol4_mapping thyname thmname moved_thmname @@ -2012,7 +1931,6 @@ acc ^ "\n " ^ quotename c ^ " :: \"" ^ Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts) val thy' = add_dump str thy - val _ = ImportRecorder.add_consts consts in Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy' end @@ -2024,7 +1942,6 @@ val (thy',res) = Choice_Specification.add_specification NONE names' (thy1,th) - val _ = ImportRecorder.add_specification names' th val res' = Thm.unvarify_global res val hth = HOLThm(rens,res') val rew = rewrite_hol4_term (concl_of res') thy' @@ -2092,19 +2009,16 @@ val ((_, typedef_info), thy') = Typedef.add_typedef_global false (SOME (Binding.name thmname)) (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy - val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4 val fulltyname = Sign.intern_type thy' tycname val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3)) val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") else () val thy4 = add_hol4_pending thyname thmname args thy'' - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val rew = rewrite_hol4_term (concl_of td_th) thy4 val th = Thm.equal_elim rew (Thm.transfer thy4 td_th) @@ -2169,7 +2083,6 @@ Typedef.add_typedef_global false NONE (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy - val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) val abs_ty = tT --> aty @@ -2186,11 +2099,9 @@ raise ERR "type_introduction" "no term variables expected any more" val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname val _ = message "step 4" val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) val thy4 = add_hol4_pending thyname thmname args thy'' - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *) val c =