Proofrecording/diffs/proofobjects_trt.ml

   1 (* ========================================================================= *)
   2 (*                 Proof-objects for HOL-light                               *)
   3 (*                                                                           *)
   4 (*       Steven Obua, TU München, December 2004                              *)
   5 (*                                                                           *)
   6 (*       based on Sebastian Skalberg's HOL4 proof-objects                    *)
   7 (* ========================================================================= *)
   8
   9 #load "unix.cma";;
  10
  11 module type Proofobject_primitives =
  12   sig
  13
  14     type proof
  15
  16     val proof_REFL : term -> proof
  17     val proof_TRANS : proof * proof -> proof
  18     val proof_MK_COMB : proof * proof -> proof
  19     val proof_ASSUME : term -> proof
  20     val proof_EQ_MP : proof -> proof -> proof
  21     val proof_IMPAS : proof -> proof -> proof
  22     val proof_DISCH : proof -> term -> proof
  23     val proof_DEDUCT_ANTISYM_RULE : proof * term -> proof * term -> proof
  24     val proof_BETA : term -> proof
  25     val proof_ABS : term -> proof -> proof
  26     val proof_INST_TYPE : (hol_type * hol_type) list -> proof -> proof
  27     val proof_INST : (term * term) list -> proof -> proof
  28     val proof_new_definition : string -> hol_type -> term -> proof
  29     val proof_CONJ : proof -> proof -> proof
  30     val proof_CONJUNCT1 : proof -> proof
  31     val proof_CONJUNCT2 : proof -> proof
  32     val proof_new_basic_type_definition :
  33         string -> string * string -> term * term -> proof -> proof
  34     val proof_SPEC : term -> proof -> proof
  35     val proof_SYM : proof -> proof
  36     val proof_GEN : proof -> term -> proof
  37     val proof_DISJ1 : proof -> term -> proof
  38     val proof_DISJ2 : proof -> term -> proof
  39     val proof_NOTI : proof -> proof
  40     val proof_NOTE : proof -> proof
  41     val proof_CONTR : proof -> term -> proof
  42     val proof_DISJCASES : proof -> proof -> proof -> proof
  43     val proof_CHOOSE : term -> proof -> proof -> proof
  44     val proof_EXISTS : term -> term -> proof -> proof
  45
  46     val new_axiom_name : string -> string
  47     val proof_new_axiom : string -> term -> proof
  48
  49     val save_proof : string -> proof -> (term option) -> unit
  50     val proof_database : unit -> ((string * proof * (term option)) list)
  51
  52     val export_proofs : string option -> (string * proof * (term option)) list -> unit
  53     val export_saved_proofs : string option -> unit
  54 end;;
  55
  56 module Proofobjects : Proofobject_primitives = struct
  57
  58   let writeln s p = p;;
  59 (*    let q = s^"\n" in
  60     (output stdout q 0 (String.length q); p);;*)
  61
  62   type tag = string
  63
  64   type proof_info_rec =
  65       {disk_info: (string * string) option ref;
  66        status: int ref;
  67        references: int ref;
  68        queued: bool ref}
  69
  70   type proof_info = Info of proof_info_rec
  71
  72   type ('a, 'b) libsubst_rec = {redex:'a; residue:'b}
  73   type ('a, 'b) libsubst = (('a,'b) libsubst_rec) list
  74
  75   let pair2libsubstrec =
  76     fun (a,b) -> {redex=b;residue=a}
  77
  78 (* note: not all of the proof_content constructors are actually used, some are just legacy from the HOL4 proof objects *)
  79   type proof =
  80       Proof of (proof_info * proof_content * (unit -> unit))
  81   and proof_content =
  82       Prefl of term
  83     | Pinstt of proof * ((hol_type,hol_type) libsubst)
  84     | Psubst of proof list * term * proof
  85     | Pabs of proof * term
  86     | Pdisch of proof * term
  87     | Pmp of proof * proof
  88     | Phyp of term
  89     | Paxm of string * term
  90     | Pdef of string * string * term
  91     | Ptmspec of string * string list * proof
  92     | Ptydef of string * string * proof
  93     | Ptyintro of string * string * string * string * term * term * proof
  94     | Poracle of tag * term list * term
  95     | Pdisk
  96     | Pspec of proof * term
  97     | Pinst of proof * (term,term) libsubst
  98     | Pgen of proof * term
  99     | Pgenabs of proof * term option * term list
 100     | Psym of proof
 101     | Ptrans of proof * proof
 102     | Pcomb of proof * proof
 103     | Peqmp of proof * proof
 104     | Peqimp of proof
 105     | Pexists of proof * term * term
 106     | Pchoose of term * proof * proof
 107     | Pconj of proof * proof
 108     | Pconjunct1 of proof
 109     | Pconjunct2 of proof
 110     | Pdisj1 of proof * term
 111     | Pdisj2 of proof * term
 112     | Pdisjcases of proof * proof * proof
 113     | Pnoti of proof
 114     | Pnote of proof
 115     | Pcontr of proof * term
 116     | Pimpas of proof * proof
 117
 118   let THEORY_NAME = "hollight"
 119
 120   let content_of (Proof (_,p,_)) = p
 121
 122   let inc_references (Proof(Info{references=r},_,_) as p) = (
 123     let
 124         old = !r
 125     in
 126     r := old + 1;
 127     p)
 128
 129   let concat = String.concat ""
 130
 131   let dummy_fun () = ()
 132
 133   let mk_proof p = Proof(Info {disk_info = ref None; status = ref 0; references = ref 0; queued = ref false},p, dummy_fun)
 134
 135   let global_ax_counter = let counter = ref 1 in let f = fun () -> (let x = !counter in counter := !counter+1; x) in f
 136
 137   let new_axiom_name n = concat["ax_"; n; "_"; string_of_int(global_ax_counter())]
 138
 139   let proof_REFL t = writeln "REFL" (mk_proof (Prefl t))
 140
 141   let proof_TRANS (p,q) = writeln "TRANS" (
 142     match (content_of p, content_of q) with
 143       (Prefl _,_) -> q
 144     | (_, Prefl _) -> p
 145     | _ -> mk_proof (Ptrans (inc_references p, inc_references q)))
 146
 147   let proof_MK_COMB (p1,p2) = writeln "MK_COMB" (
 148     (match (content_of p1, content_of p2) with
 149       (Prefl tm1, Prefl tm2) -> proof_REFL (mk_comb (tm1, tm2))
 150     | _ ->  mk_proof (Pcomb (inc_references p1, inc_references p2))))
 151
 152   let proof_ASSUME t = writeln "ASSUME "(mk_proof (Phyp t))
 153
 154   let proof_EQ_MP p q = writeln "EQ_MP" (
 155     (match content_of p with
 156       Prefl _ -> q
 157     | _ -> mk_proof (Peqmp(inc_references p, inc_references q))))
 158
 159   let proof_IMPAS p1 p2 = writeln "IMPAS" (
 160     mk_proof (Pimpas (inc_references p1, inc_references p2)))
 161
 162   let proof_DISCH p t = writeln "DISCH" (mk_proof (Pdisch(inc_references p,t)))
 163
 164   let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) = writeln "DEDUCT_ANTISYM_RULE" (
 165     proof_IMPAS (proof_DISCH p1 t2) (proof_DISCH p2 t1))
 166
 167   let proof_BETA t = writeln "BETA" (mk_proof (Prefl t))
 168
 169   let proof_ABS x p = writeln "ABS" (
 170     (match (content_of p) with
 171       Prefl tm -> proof_REFL (mk_abs(x,tm))
 172     | _ -> mk_proof (Pabs(inc_references p,x))))
 173
 174   let proof_INST_TYPE s p = writeln "INST_TYPE" (mk_proof (Pinstt(inc_references p, map pair2libsubstrec s)))
 175
 176   let proof_INST s p = writeln "INST" (mk_proof (Pinst(inc_references p, map pair2libsubstrec s)))
 177
 178   let proof_new_definition cname _ t = writeln "new_definition" (mk_proof (Pdef (THEORY_NAME, cname, t)))
 179
 180   let proof_new_axiom axname t = writeln "new_axiom" (mk_proof (Paxm (axname, t)))
 181
 182   let proof_CONJ p1 p2 = writeln "CONJ" (mk_proof (Pconj (inc_references p1, inc_references p2)))
 183
 184   let proof_CONJUNCT1 p = writeln "CONJUNCT1" (mk_proof (Pconjunct1 (inc_references p)))
 185
 186   let proof_CONJUNCT2 p = writeln "CONJUNCT2" (mk_proof (Pconjunct2 (inc_references p)))
 187
 188   let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) p = writeln "new_basic_type_definition" (
 189     mk_proof(Ptyintro (THEORY_NAME, tyname, absname, repname, pt, tt,inc_references p)))
 190
 191 (* ---- used only in substitute_proof calls ---- *)
 192
 193   let proof_SPEC s p = writeln "SPEC" (mk_proof (Pspec(inc_references p, s)))
 194
 195   let proof_SYM p = writeln "SYM" (mk_proof (Psym(inc_references p)))
 196
 197   let proof_GEN p a = writeln "GEN" (mk_proof (Pgen(inc_references p, a)))
 198
 199   let proof_DISJ1 p a = writeln "DISJ1" (mk_proof (Pdisj1 (inc_references p, a)))
 200
 201   let proof_DISJ2 p a = writeln "DISJ2" (mk_proof (Pdisj2 (inc_references p, a)))
 202
 203   let proof_NOTI p = writeln "NOTI" (mk_proof (Pnoti (inc_references p)))
 204
 205   let proof_NOTE p = writeln "NOTE" (mk_proof (Pnote (inc_references p)))
 206
 207   let proof_CONTR p a = writeln "CONTR" (mk_proof (Pcontr (inc_references p, a)))
 208
 209   let proof_DISJCASES p q r = writeln "DISJCASES" (mk_proof (Pdisjcases (inc_references p, inc_references q, inc_references r)))
 210
 211   let proof_CHOOSE a p q = writeln "CHOOSE" (mk_proof (Pchoose (a, inc_references p, inc_references q)))
 212
 213   let proof_EXISTS x y p  = writeln "EXISTS" (mk_proof (Pexists (inc_references p, x, y)))
 214
 215 (* ---- formerly known as proofio.ml ---- *)
 216
 217 let ensure_export_directory thyname =
 218   let dir = Sys.getenv "HOLPROOFEXPORTDIR" in
 219   let dirsub = Filename.concat dir "hollight" in
 220   let dirsubsub = Filename.concat dirsub thyname in
 221   let mk d = if Sys.file_exists d then () else Unix.mkdir d 509
 222   in
 223     (mk dir;
 224      mk dirsub;
 225      mk dirsubsub;
 226      dirsubsub);;
 227
 228 (* ---- Useful functions on terms ---- *)
 229 let rec types_of tm =
 230     if is_var tm
 231     then [type_of tm]
 232     else if is_const tm
 233     then [type_of tm]
 234     else if is_comb tm
 235     then
 236         let
 237             (f,a) = dest_comb tm
 238         in
 239             union (types_of f) (types_of a)
 240     else
 241         let
 242             (x,a) = dest_abs tm
 243         in
 244             insert (type_of x) (types_of a);;
 245
 246 let beta_conv tm =
 247   try let (f,arg) = dest_comb tm in
 248       let (v,bod) = dest_abs f in
 249       vsubst [(arg,v)] bod
 250   with Failure _ -> failwith "beta_conv: Not a beta-redex";;
 251
 252 let eta_conv tm =
 253   try
 254     (let (v, bod) = dest_abs tm in
 255     let (f, arg) = dest_comb bod in
 256       if (arg = v && (not(vfree_in v f))) then
 257         f
 258       else failwith "")
 259   with
 260     Failure _ -> failwith "eta_conv: Not an eta-redex";;
 261
 262 let rec be_contract tm =
 263     let rec bec tm = try try Some (beta_conv tm)
 264             with Failure _ ->
 265                    Some (eta_conv tm)
 266             with Failure _ ->
 267                    if is_comb tm
 268                    then
 269                        (let
 270                            (f,x) = dest_comb tm
 271                        in
 272                            match bec f with
 273                                Some f' -> Some (mk_comb(f',x))
 274                              | None -> (match bec x with
 275                                             Some x' -> Some (mk_comb(f,x'))
 276                                           | None -> None))
 277                    else if is_abs tm
 278                    then
 279                        (let
 280                          (x,body) = dest_abs tm
 281                        in
 282                            (match bec body with
 283                                Some body' -> Some (mk_abs(x,body'))
 284                              | None -> None))
 285                    else None
 286     in
 287         (match bec tm with
 288             Some tm' -> be_contract tm'
 289           | None -> tm);;
 290
 291 let rec polymorphic x =
 292   if is_vartype x then true else exists polymorphic (snd (dest_type x))
 293
 294 (* ---- From Lib etc. ---- *)
 295
 296
 297 let rec append = fun xlist l ->
 298   (match xlist with
 299     [] -> l
 300   | (x::xs) -> x::(append xs l));;
 301
 302 let assoc1 item =
 303   let rec assc =
 304     (function (((key,_) as e)::rst) -> if item=key then Some e else assc rst
 305       | [] -> None)
 306   in
 307     assc;;
 308
 309
 310 let rec listconcat =
 311   function [] -> []
 312     | (l::ls) -> append l (listconcat ls);;
 313
 314 let listnull =
 315   function [] -> true | _ -> false;;
 316
 317 (* ---- exported ---- *)
 318 let encodeXMLEntities m = m;;let encodeXMLEntities s =
 319   let len = String.length s in
 320   let encodeChar  = function '<' -> "&lt;" | '>' -> "&gt;" | '&' -> "&amp;" | '\'' -> "&apos;" | '"' -> "&quot;" | c -> String.make 1 c in
 321   let rec encodeStr i =  if (i<len) then (encodeChar (String.get s i))::(encodeStr (i+1)) else [] in
 322   String.concat "" (encodeStr 0);;
 323
 324 let encodeXMLEntitiesOut out = function x -> out (encodeXMLEntities x);;
 325
 326
 327 let content_of (Proof (_,x,_)) = x;;
 328
 329 let rec explode_subst =
 330   function [] -> []
 331     | ({redex=x;residue=y}::rest) -> x::y::(explode_subst rest);;
 332
 333 let rec app f =
 334   function [] -> ()
 335     | (x::l) -> (f x; app f l);;
 336
 337 let disk_info_of (Proof(Info {disk_info=di},_,_)) = !di;;
 338
 339 let set_disk_info_of (Proof(Info {disk_info=di},_,_)) thyname thmname =
 340     di := Some (thyname,thmname);;
 341
 342 let references (Proof (Info info,_,_)) = !(info.references);;
 343
 344 let wrap b e s = b^s^e;;
 345
 346 let xml_empty_tag = wrap "<" "/>";;
 347 let xml_start_tag = wrap "<" ">";;
 348 let xml_end_tag = wrap "</" ">";;
 349 let xml_attr attr =
 350     itlist (function (tag,v) ->
 351             function s ->
 352                concat[" ";tag;"=\"";v;"\"";s]
 353            )
 354            attr "";;
 355 let xml_element tag attr children =
 356     let
 357         header = tag ^ (xml_attr attr)
 358     in
 359         (if listnull children
 360          then xml_empty_tag header
 361          else wrap (xml_start_tag header) (xml_end_tag tag) (concat children));;
 362
 363 let id_to_atts curthy id = [("n", encodeXMLEntities id)];; (* There is only one theory in Hol-Light, therefore id_to_atts is superfluous *)
 364
 365 let glob_counter = ref 1;;
 366
 367 let get_counter () =
 368   let
 369       res = !glob_counter
 370   in
 371     glob_counter := res + 1;
 372     res;;
 373
 374 let get_iname =  string_of_int o get_counter;;
 375
 376 let next_counter () = !glob_counter;;
 377
 378 let trivial p =
 379       match (content_of p) with
 380         Prefl _ -> true
 381       | Paxm _ -> true
 382       | Pdisk -> true
 383       | Phyp _ -> true
 384       | Poracle _ -> true
 385       | _ -> false;;
 386
 387 let do_share p = references p > 1 & not (trivial p);;
 388
 389 exception Err of string*string;;
 390
 391 (* ---- The General List Formerly Known As Net ---- *)
 392
 393 type 'a exprnet = (('a list) ref) * ('a -> ('a list))
 394
 395 let empty_net f () = (ref [], f);;
 396
 397 let rec lookup'_net net x =
 398   match net with
 399     [] -> raise Not_found
 400   | (a::l) -> if (a = x) then 0 else 1+(lookup'_net l x);;
 401
 402 let lookup_net (net,f) x = lookup'_net (!net) x;;
 403
 404 let insert'_net (net,f) x =
 405   try lookup'_net !net x; () with Not_found -> ((net := (!net)@[x]);());;
 406
 407 let rec insert_net ((net,f) as n) x =
 408   (app (insert_net n) (f x); insert'_net n x);;
 409
 410 let to_list_net (net,f) = !net;;
 411
 412 (* ---- The Type Net (it's not a net any more!) ---- *)
 413
 414 type yy_net = hol_type exprnet;;
 415
 416 let yy_empty = empty_net (function x -> if is_type x then snd (dest_type x) else []);;
 417
 418 let yy_lookup = lookup_net;;
 419
 420 let yy_output_types out thyname net =
 421     let
 422         all_types = to_list_net net in let rec
 423         xml_index ty = xml_element "tyi" [("i",string_of_int (yy_lookup net ty))] []
 424         and xml_const id = xml_element "tyc" (id_to_atts thyname id) []
 425         and out_type ty =
 426           if is_vartype ty then out (xml_element "tyv" [("n",encodeXMLEntities (dest_vartype ty))] [])
 427           else (
 428             match dest_type ty with
 429               (id, []) -> out (xml_const id)
 430             | (id, tl) -> out (xml_element "tya" [] ((xml_const id)::(map xml_index tl)))
 431           )
 432     in
 433         out "<tylist i=\"";
 434         out (string_of_int (length all_types));
 435         out "\">";
 436         app out_type all_types;
 437         out "</tylist>";;
 438
 439 let yy_insert = insert_net;;
 440
 441 (* ---- The Term Net (it's not a net anymore!) ---- *)
 442
 443 type mm_net = term exprnet;;
 444
 445 let mm_empty = empty_net (
 446   function tm ->
 447     if is_abs tm then
 448       (let (x,b) = dest_abs tm in [x; b])
 449     else if is_comb tm then
 450       (let (s,t) = dest_comb tm in [s; t])
 451     else
 452       [])
 453
 454 let mm_lookup net x = lookup_net net (be_contract x);;
 455
 456 let mm_insert net x = insert_net net (be_contract x);;
 457
 458 let mm_output_terms out thyname types net =
 459     let all_terms = to_list_net net in
 460     let xml_type ty = xml_element "tyi" [("i",string_of_int (yy_lookup types ty))] [] in
 461     let xml_index tm = xml_element "tmi" [("i",string_of_int (mm_lookup net tm))] [] in
 462     let out_term tm =
 463             if is_var tm
 464             then
 465                 let
 466                     (name,ty) = dest_var tm
 467                 in
 468                     out (xml_element "tmv" [("n",encodeXMLEntities name);("t", string_of_int (yy_lookup types ty))] [])
 469             else if is_const tm
 470             then
 471                 let (name, ty) = (dest_const tm) in
 472                 let general_ty = get_const_type name in
 473                 let atts = [("n",encodeXMLEntities name)]
 474                 in
 475                     if polymorphic general_ty then
 476                       out (xml_element "tmc" (atts@[("t",string_of_int (yy_lookup types ty))]) [])
 477                     else out (xml_element "tmc" atts [])
 478             else if is_comb tm
 479             then
 480                 let
 481                     (f,a) = dest_comb tm
 482                 in
 483                     out (xml_element "tma" [("f", string_of_int (mm_lookup net f));("a",string_of_int (mm_lookup net a))] [])
 484             else
 485                 let
 486                     (x,a) = dest_abs tm
 487                 in
 488                     out (xml_element "tml" [("x", string_of_int (mm_lookup net x));("a",string_of_int (mm_lookup net a))] [])
 489     in
 490         out "<tmlist i=\"";
 491         out (string_of_int(length all_terms));
 492         out "\">";
 493         app out_term all_terms;
 494         out "</tmlist>";;
 495
 496
 497 (* ---- collect_types_terms ---- *)
 498
 499 let collect_types_terms thyname out prf c_opt =
 500     let
 501         will_be_shared prf = (
 502             match disk_info_of prf with
 503                 Some _ -> true
 504               | None -> do_share prf) in let
 505
 506         types = yy_empty () in let
 507         terms = mm_empty () in let
 508
 509         insert_type ty = yy_insert types ty in let
 510
 511         insert_term tm = (mm_insert terms tm;
 512                           app (yy_insert types) (types_of tm)) in let rec
 513
 514         ct' prf =
 515             (match content_of prf with
 516                 Pinstt(prf,tsubst) -> (app (function {redex=x;residue=u}->(insert_type x; insert_type u))
 517                                            tsubst;
 518                                        ct prf)
 519               | Psubst(prfs,tm,prf) -> (insert_term tm;
 520                                         ct prf;
 521                                         app ct prfs)
 522               | Pabs(prf,tm) -> (insert_term tm;
 523                                  ct prf)
 524               | Pdisch(prf,tm) -> (insert_term tm;
 525                                    ct prf)
 526               | Pmp(prf1,prf2) -> (ct prf1; ct prf2)
 527               | Poracle(_,tms,tm) -> (insert_term tm;
 528                                       app insert_term tms)
 529               | Pdef(_,_,tm) -> insert_term tm
 530               | Ptmspec(_,_,prf) -> ct prf
 531               | Ptydef(_,_,prf) -> ct prf
 532               | Ptyintro(_,_,_,_,pt,tt,prf) -> (insert_term pt; insert_term tt;ct prf)
 533               | Pspec(prf,tm) -> (insert_term tm; ct prf)
 534               | Pinst(prf,subst) -> (app (fun{redex=x;residue=u}->(insert_term x;
 535                                                               insert_term u))
 536                                          subst;
 537                                      ct prf)
 538               | Pgen(prf,tm) -> (insert_term tm; ct prf)
 539               | Pgenabs(prf,tm_opt,tms) -> (match tm_opt with
 540                                                 Some tm -> insert_term tm
 541                                               | None -> ();
 542                                             app insert_term tms;
 543                                             ct prf)
 544               | Psym prf -> ct prf
 545               | Ptrans(prf1,prf2) -> (ct prf1; ct prf2)
 546               | Pcomb(prf1,prf2) -> (ct prf1; ct prf2)
 547               | Peqmp(prf1,prf2) -> (ct prf1; ct prf2)
 548               | Peqimp prf -> ct prf
 549               | Pexists(prf,ex,w) -> (insert_term ex;
 550                                       insert_term w;
 551                                       ct prf)
 552               | Pchoose(v,prf1,prf2) -> (insert_term v; ct prf1; ct prf2)
 553               | Pconj(prf1,prf2) -> (ct prf1; ct prf2)
 554               | Pconjunct1 prf -> ct prf
 555               | Pconjunct2 prf -> ct prf
 556               | Pdisj1(prf,tm) -> (insert_term tm;
 557                                    ct prf)
 558               | Pdisj2(prf,tm) -> (insert_term tm;
 559                                    ct prf)
 560               | Pdisjcases(prf1,prf2,prf3) -> (ct prf1; ct prf2; ct prf3)
 561               | Pnoti prf -> ct prf
 562               | Pnote prf -> ct prf
 563               | Pcontr(prf,tm) -> (insert_term tm;
 564                                    ct prf)
 565               | Prefl tm -> insert_term tm
 566               | Phyp tm -> insert_term tm
 567               | Pdisk -> ()
 568               | Paxm (_,tm) -> insert_term tm
 569               | Pimpas (prf1,prf2) -> (ct prf1; ct prf2))
 570         and ct prf =
 571             if will_be_shared prf
 572             then ()
 573             else ct' prf in let
 574
 575         _ = ct' prf in let
 576         _ = (match c_opt with
 577                     Some c -> insert_term c
 578                   | None -> ()) in let
 579         _ = yy_output_types out thyname types in let
 580         _ = mm_output_terms out thyname types terms
 581     in
 582         (types,terms);;
 583
 584 let rec export_proof path thyname thmname p c_opt il  =
 585   let outchannel = open_out (Filename.concat path (thmname^".prf")) in
 586   let out = output_string outchannel in
 587   let nout = encodeXMLEntitiesOut out in
 588   let
 589       _ = out "<proof>" in let
 590
 591       (types,terms) = collect_types_terms thyname out p c_opt in let
 592
 593       wti att tm =
 594         (out " ";
 595          out att;
 596          out "=\"";
 597          out (string_of_int (mm_lookup terms tm));
 598          out "\"") in let
 599
 600       wt tm = try (out "<tmi"; wti "i" tm; out "/>") with Not_found -> raise (Err("export_proof","Term not found!")) in let
 601
 602       wty ty =
 603         try (out "<tyi i=\"";
 604              out (string_of_int (yy_lookup types ty));
 605              out "\"/>") with Not_found -> raise (Err("export_proof","Type not found!")) in let
 606
 607       wdi thy thm =
 608         (out "<pfact ";
 609          if not (thy = thyname)
 610          then (out "s=\"";
 611                out thy;
 612                out "\" ")
 613          else ();
 614          out "n=\"";
 615          nout thm;
 616          out "\"/>") in let
 617
 618       write_proof p il =
 619        (let rec
 620           share_info_of p il =
 621             (match (disk_info_of p) with
 622               Some (thyname,thmname) -> Some(thyname,thmname,il)
 623             | None ->
 624                 if do_share p then
 625                   let name = get_iname() in set_disk_info_of p thyname name; Some(thyname,name,(name,p,None)::il)
 626                 else
 627                   None
 628             )
 629           and
 630           dump str il prfs =
 631                     (let
 632                         _ = out (xml_start_tag str) in let
 633                         res = rev_itlist (function p -> function il -> wp il p) prfs il in let
 634                         _ = out (xml_end_tag str)
 635                     in
 636                         res)
 637           and
 638           wp' il =
 639             (function
 640               (Prefl tm) -> (out "<prefl"; wti "i" tm; out "/>"; il)
 641             |  (Pinstt(p,lambda)) ->
 642                    (let
 643                         _ = out "<pinstt>" in let
 644                         res = wp il p in let
 645                         _ = app wty (explode_subst lambda) in let
 646                         _ = out "</pinstt>"
 647                     in
 648                         res)
 649             |  (Psubst(ps,t,p)) ->
 650                    (let
 651                         _ = (out "<psubst"; wti "i" t; out ">") in let
 652                         il' = wp il p in let
 653                         res = rev_itlist (function p -> function il -> wp il p) ps il' in let
 654                         _ = out "</psubst>"
 655                     in
 656                         res)
 657             |  (Pabs(p,t)) ->
 658                    (let
 659                         _ = (out "<pabs"; wti "i" t; out ">") in let
 660                         res = wp il p in let
 661                         _ = out "</pabs>"
 662                     in
 663                         res)
 664             |  (Pdisch(p,tm)) ->
 665                     (let
 666                         _ = (out "<pdisch"; wti "i" tm; out ">") in let
 667                         res = wp il p in let
 668                         _ = out "</pdisch>"
 669                     in
 670                         res)
 671             |  (Pmp(p1,p2)) -> dump "pmp" il [p1;p2]
 672             |  (Phyp tm) -> (out "<phyp"; wti "i" tm; out "/>"; il)
 673             |  (Paxm(name,tm)) ->
 674                     (out "<paxiom n=\"";
 675                      nout name;
 676                      out "\"";
 677                      wti "i" tm;
 678                      out "/>";
 679                      il)
 680             |  (Pdef(seg,name,tm)) ->
 681                     (out "<pdef s=\"";
 682                      out seg;
 683                      out "\" n=\"";
 684                      nout name;
 685                      out "\"";
 686                      wti "i" tm;
 687                      out "/>";
 688                      il)
 689             |  (Ptmspec(seg,names,p)) ->
 690                     (let
 691                         _ = (out "<ptmspec s=\""; out seg; out "\">") in let
 692                         res = wp il p in let
 693                         _ = app (function s -> (out "<name n=\""; nout s; out "\"/>")) names in let
 694                         _ = out "</ptmspec>"
 695                     in
 696                         res)
 697             |  (Ptydef(seg,name,p)) ->
 698                     (let
 699                         _ = (out "<ptydef s=\""; out seg; out "\" n=\""; nout name; out "\">") in let
 700                         res = wp il p in let
 701                         _ = out "</ptydef>"
 702                     in
 703                         res)
 704             |  (Ptyintro(seg,name,abs,rep,pt,tt,p)) ->
 705                     (let
 706                         _ = (out "<ptyintro s=\""; out seg; out "\" n=\""; nout name;
 707                              out "\" a=\""; out abs; out "\" r=\""; out rep; out "\">") in let
 708
 709                         _ = wt pt in let
 710                         _ = wt tt in let
 711                         res = wp il p in let
 712                         _ = out "</ptyintro>"
 713                     in
 714                         res)
 715             |  (Poracle(tg,asl,c)) -> raise (Err("export_proof", "sorry, oracle export is not implemented!"))
 716 (*                  (out "<poracle>";
 717                      app (function s -> (out "<oracle n=\""; nout s; out "\"/>")) (Tag.oracles_of tg);
 718                      wt c;
 719                      app wt asl;
 720                      out "</poracle>";
 721                      il)*)
 722             |  (Pspec(p,t)) ->
 723                     (let
 724                         _ = (out "<pspec"; wti "i" t; out ">") in let
 725                         res = wp il p in let
 726                         _ = out "</pspec>"
 727                     in
 728                         res)
 729             |  (Pinst(p,theta)) ->
 730                     (let
 731                         _ = out "<pinst>" in let
 732                         res = wp il p in let
 733                         _ = app wt (explode_subst theta) in let
 734                         _ = out "</pinst>"
 735                     in
 736                         res)
 737             |  (Pgen(p,x)) ->
 738                     (let
 739                         _ = (out "<pgen"; wti "i" x; out ">") in let
 740                         res = wp il p in let
 741                         _ = out "</pgen>"
 742                     in
 743                         res)
 744             |  (Pgenabs(p,opt,vl)) ->
 745                     (let
 746                         _ = out "<pgenabs" in let
 747                         _ = (match opt with
 748                                     Some c -> wti "i" c
 749                                   | None -> ()) in let
 750                         _ = out ">" in let
 751                         res = wp il p in let
 752                         _ = app wt vl in let
 753                         _ = out "</pgenabs>"
 754                     in
 755                         res)
 756                   |  (Psym p) -> dump "psym" il [p]
 757                   |  (Ptrans(p1,p2)) -> dump "ptrans" il [p1;p2]
 758                   |  (Pcomb(p1,p2)) -> dump "pcomb" il [p1;p2]
 759                   |  (Peqmp(p1,p2)) -> dump "peqmp" il [p1;p2]
 760                   |  (Peqimp p) -> dump "peqimp" il [p]
 761                   |  (Pexists(p,ex,w)) ->
 762                     (let
 763                         _ = (out "<pexists"; wti "e" ex; wti "w" w; out ">") in let
 764                         res = wp il p in let
 765                         _ = out "</pexists>"
 766                     in
 767                         res)
 768                   |  (Pchoose(v,p1,p2)) ->
 769                     (let
 770                         _ = (out "<pchoose"; wti "i" v; out ">") in let
 771                         il' = wp il p1 in let
 772                         res = wp il' p2 in let
 773                         _ = out "</pchoose>"
 774                     in
 775                         res)
 776                   |  (Pconj(p1,p2)) -> dump "pconj" il [p1;p2]
 777                   |  (Pimpas(p1,p2)) -> dump "pimpas" il [p1;p2]
 778                   |  (Pconjunct1 p) -> dump "pconjunct1" il [p]
 779                   |  (Pconjunct2 p) -> dump "pconjunct2" il [p]
 780                   |  (Pdisj1(p,tm)) ->
 781                     (let
 782                         _ = (out "<pdisj1"; wti "i" tm; out ">") in let
 783                         res = wp il p in let
 784                         _ = out "</pdisj1>"
 785                     in
 786                         res)
 787                   |  (Pdisj2(p,tm)) ->
 788                     (let
 789                         _ = (out "<pdisj2"; wti "i" tm; out ">") in let
 790                         res = wp il p in let
 791                         _ = out "</pdisj2>"
 792                     in
 793                         res)
 794                   |  (Pdisjcases(p1,p2,p3)) -> dump "pdisjcases" il [p1;p2;p3]
 795                   |  (Pnoti p) -> dump "pnoti" il [p]
 796                   |  (Pnote p) -> dump "pnote" il [p]
 797                   |  (Pcontr(p,tm)) ->
 798                     (let
 799                         _ = (out "<pcontr"; wti "i" tm; out ">") in let
 800                         res = wp il p in let
 801                         _ = out "</pcontr>"
 802                     in
 803                         res)
 804                   |  Pdisk -> raise (Err("wp'","shouldn't try to write pdisk"))
 805             )
 806           and wp il p =
 807                (let
 808                     res = match (share_info_of p il) with
 809                             Some(thyname',thmname,il') -> (wdi thyname' thmname; il')
 810                           | None -> wp' il (content_of p)
 811                 in res) in let
 812
 813           res = (match disk_info_of p with
 814                               Some(thyname',thmname') ->
 815                               if thyname' = thyname &
 816                                  thmname' = thmname
 817                               then
 818                                   wp' il (content_of p)
 819                               else
 820                                   (wdi thyname' thmname';
 821                                    il)
 822                             | None -> wp' il (content_of p))
 823          in res) in let
 824
 825         il = write_proof p il in let
 826         _ = (match c_opt with
 827                     Some c -> wt c
 828                   | None -> ()) in let
 829         _ = (out "</proof>\n";(close_out outchannel))  in let
 830         _ = set_disk_info_of p thyname thmname
 831         in
 832            match il with
 833              [] -> () (* everything has been written *)
 834            | ((thmname',prf,c_opt)::rest) -> export_proof path thyname thmname' prf c_opt rest;;
 835
 836 let export_proofs theory_name l' =
 837   let theory_name = match theory_name with None -> THEORY_NAME | Some n -> n in
 838   let path = ensure_export_directory theory_name in
 839   let ostrm = open_out (Filename.concat path "facts.lst") in
 840   let out = output_string ostrm in
 841   let _ = app (function (s,_,_) -> out (s^"\n")) l' in
 842   let _ = flush ostrm in
 843   let _ =
 844     (match l' with
 845       [] -> ()
 846     | ((thmname,p,c_opt)::rest) -> export_proof path theory_name thmname p c_opt rest) in
 847   let num_int_thms = next_counter() - 1 in
 848   let _ = out ((string_of_int num_int_thms)^"\n");(close_out ostrm) in
 849   ();;
 850
 851 let the_proof_database = ref ([]:(string*proof*(term option)) list);;
 852
 853 exception Duplicate_proof_name;;
 854
 855 let rec search_proof_name n db =
 856   match db with [] -> () | ((m, a, b)::db') -> if n=m then (raise Duplicate_proof_name) else search_proof_name n db'
 857
 858 let save_proof name p c_opt =
 859   let _ = search_proof_name name (!the_proof_database)
 860   in
 861   (the_proof_database :=
 862     (name, p, c_opt)::(!the_proof_database));;
 863
 864 let proof_database () = !the_proof_database;;
 865
 866 (* this is a little bit dangerous, because the function is not injective,
 867    but I guess one can live with that *)
 868 let make_filesystem_compatible s =
 869   let modify = function
 870     | "/" -> "_slash_"
 871     | "\\" -> "_backslash_"
 872     | "=" -> "_equal_"
 873     | ">" -> "_greaterthan_"
 874     | "<" -> "_lessthan_"
 875     | "?" -> "_questionmark_"
 876     | "!" -> "_exclamationmark_"
 877     | "*" -> "_star_"
 878     | s -> s
 879   in
 880   implode (map modify (explode s));;
 881
 882 let export_saved_proofs thy =
 883   let context = rev (proof_database ()) in
 884   export_proofs thy (map (function (s,p,c) -> (make_filesystem_compatible s,p,c)) context);;
 885
 886 end;;
 887
 888 include Proofobjects;;