holyhammer/legacy/hh_write.ml

42 let os = output_string;;
46   | h :: t -> fn oc h; os oc sep; oiter oc fn sep t;;
146       0 -> os oc (Hashtbl.find ts ty)
149         os oc "("; oty_mono ts 0 oc t1; os oc " > "; oty_mono ts 0 oc t2; os oc ")"
152         os oc "("; oiter oc (oty_mono ts (order - 1)) " > " args; os oc " > ";
153         oty_mono ts (order - 1) oc res; os oc ")"
154   else os oc (Hashtbl.find ts ty);;
158   if is_vartype ty then os oc (try Hashtbl.find ts (dest_vartype ty) with Not_found -> print_vartype ty) else
162       if tys <> [] then os oc "(";
163       os oc (Hashtbl.find ts s);
164       List.iter (fun ty -> os oc " @ "; oty_poly ts order oc ty) tys;
165       if tys <> [] then os oc ")";
167       os oc (Hashtbl.find ts s);
168       if tys = [] then () else (os oc "("; oiter oc (oty_poly ts 0) "," tys; os oc ")")
176           [a] -> oty_poly ts 0 oc a; os oc " > "; oty_poly ts 0 oc res
177         | _ -> os oc "("; oiter oc (oty_poly ts 0) " * " args; os oc " > "; oty_poly ts 0 oc res)
180         os oc "("; oiter oc (oty_poly ts (order - 1)) " > " args; os oc " > ";
181         oty_poly ts (order - 1) oc res; os oc ")")
196     os oc (try Tmm.find tm bnd with Not_found -> Hashtbl.find cs ("`" ^ (o fst dest_var) tm))
199     os oc (Hashtbl.find cs (fst (dest_const f)));
202       os oc "(";
204       (if args <> [] && insts <> [] then os oc "," else ());
206       os oc ")"
218   (os oc "["; oiter oc (fun oc v -> os oc (Tmm.find v bnd); os oc ":"; oty_poly ts order oc (type_of v)) "," bs;
219    os oc "]:");;
225     os oc "!"; pr_bs_poly oc 0 bnd ts bs; tff_pred oc (bnd, used) cs ts bod
229     os oc "?"; pr_bs_poly oc 0 bnd ts bs; tff_pred oc (bnd, used) cs ts bod
231     (os oc "("; oiter oc (fun oc e -> tff_pred oc (bnd, used) cs ts e) " & " (conjuncts tm); os oc ")")
233     (os oc "("; oiter oc (fun oc e -> tff_pred oc (bnd, used) cs ts e) " | " (disjuncts tm); os oc ")")
235     (os oc "("; tff_pred oc (bnd, used) cs ts l; os oc " => ";
236                tff_pred oc (bnd, used) cs ts r; os oc ")")
238     let t = dest_neg tm in (os oc "~ ("; tff_pred oc (bnd,used) cs ts t; os oc ")")
241       (os oc "("; tff_pred oc (bnd, used) cs ts l; os oc " <=> ";
242       tff_pred oc (bnd, used) cs ts r; os oc ")")
244       (tff_tm oc (bnd, used) cs ts l; os oc " = "; tff_tm oc (bnd, used) cs ts r)
246     (os oc "p("; tff_tm oc (bnd, used) cs ts tm; os oc ")");;
252   (if tvs <> [] then (os oc "!["; oiter oc (fun oc e -> oty_poly ts 0 oc e; os oc " : $tType") "," tvs; os oc "]: "));
257   (os oc "["; oiter oc (fun oc v -> os oc (Tmm.find v bnd); os oc ":"; oty_mono ts order oc (type_of v)) "," bs;
258    os oc "]:");;
264     os oc "!"; pr_bs_mono oc (-1) bnd ts bs; thf_tm oc (bnd, used) cs ts bod
268     os oc "?"; pr_bs_mono oc (-1) bnd ts bs; thf_tm oc (bnd, used) cs ts bod
272     os oc "^"; pr_bs_mono oc (-1) bnd ts bs; thf_tm oc (bnd, used) cs ts bod
274     (os oc "("; oiter oc (fun oc e -> thf_tm oc (bnd, used) cs ts e) " & " (conjuncts tm); os oc ")")
276     (os oc "("; oiter oc (fun oc e -> thf_tm oc (bnd, used) cs ts e) " | " (disjuncts tm); os oc ")")
278     (os oc "("; thf_tm oc (bnd, used) cs ts l; os oc " => ";
279                thf_tm oc (bnd, used) cs ts r; os oc ")")
281     let t = dest_neg tm in (os oc "~ ("; thf_tm oc (bnd,used) cs ts t; os oc ")")
283     (os oc "("; thf_tm oc (bnd, used) cs ts l;
284     os oc (if type_of l = bool_ty then " <=> " else " = ");
285     thf_tm oc (bnd, used) cs ts r; os oc ")")
287     (os oc "("; oiter oc (fun oc e -> thf_tm oc (bnd, used) cs ts e) " @ " (hop :: args); os oc ")")
288   else if is_const tm then os oc (Hashtbl.find cs tm)
289   else os oc (try Tmm.find tm bnd with Not_found -> failwith "thf_tm");;
292   let iter (s, thm) = os oc "% Assm ["; os oc s; os oc "]: "; os oc (lstring_of_term (concl thm)); os oc "\n" in
294   os oc "% Goal: "; os oc (lstring_of_term gl); os oc "\n";;
296 let oi oc i = os oc (string_of_int i);;
302   let ohdr s1 s2 = os oc "thf("; os oc s1; os oc ", "; os oc s2; os oc ", " in
303   let otl () = os oc ").\n" in
304   os oc "%  TYPES\n";
306   Hashtbl.iter (fun _ ty -> ohdr ty "type"; os oc ty; os oc " : $tType"; otl ()) ts;
308   os oc "%  CONSTS\n";
310   Hashtbl.iter (fun t s -> ohdr s "type"; os oc s; os oc " : "; oty_mono ts (-1) oc (type_of t); otl ()) cs;
312   os oc "%  AXIOMS\n";
321     os oc "!"; pr_bs_poly oc (-1) bnd ts bs; thff_tm oc (bnd, used) cs ts bod
325     os oc "?"; pr_bs_poly oc (-1) bnd ts bs; thff_tm oc (bnd, used) cs ts bod
329     os oc "^"; pr_bs_poly oc (-1) bnd ts bs; thff_tm oc (bnd, used) cs ts bod
331     (os oc "("; oiter oc (fun oc e -> thff_tm oc (bnd, used) cs ts e) " & " (conjuncts tm); os oc ")")
333     (os oc "("; oiter oc (fun oc e -> thff_tm oc (bnd, used) cs ts e) " | " (disjuncts tm); os oc ")")
335     (os oc "("; thff_tm oc (bnd, used) cs ts l; os oc " => ";
336                 thff_tm oc (bnd, used) cs ts r; os oc ")")
338     let t = dest_neg tm in (os oc "~ ("; thff_tm oc (bnd,used) cs ts t; os oc ")")
340     (os oc "("; thff_tm oc (bnd, used) cs ts l;
341     os oc (if type_of l = bool_ty then " <=> " else " = ");
342     thff_tm oc (bnd, used) cs ts r; os oc ")")
344     (os oc "("; oiter oc (fun oc e -> thff_tm oc (bnd, used) cs ts e) " @ " (hop :: args); os oc ")")
347     if insts <> [] then os oc "(";
348     os oc (Hashtbl.find cs (fst (dest_const tm)));
349     if insts <> [] then (List.iter (fun ty -> os oc " @ "; oty_poly ts (-1) oc ty) insts; os oc ")");
351   else os oc (try Tmm.find tm bnd with Not_found -> failwith "thff_tm");;
356   (if tvs <> [] then (os oc "!["; oiter oc (fun oc e -> oty_poly ts (-1) oc e; os oc ":$tType") "," tvs; os oc "]: "));
364     os oc "!>["; oiter oc (fun oc t -> os oc (print_vartype t); os oc ":$tType")
365       "," tys; os oc "]: " end;;
370   let ohdr s1 s2 = os oc "thf("; os oc s1; os oc ", "; os oc s2; os oc ", " in
371   let otl () = os oc ").\n" in
372   os oc "%  TYPES\n";
378       ohdr t "type"; os oc s; os oc ":";
379       let rec prty n = if n = 0 then os oc "$tType" else (os oc "$tType > "; prty (n - 1)) in
383   os oc "%  CONSTS\n";
386   Hashtbl.iter (fun t s -> if t.[0] <> '`' then (ohdr s "type"; os oc s; os oc " : ";
392   os oc "%  AXIOMS\n";
401   if is_vartype ty then (os oc "'"; os oc (try Hashtbl.find ts (dest_vartype ty)
404   (if tys = [] then () else (os oc "("; oiter oc (oty_isa ts) "," tys; os oc ")"));
405   os oc (Hashtbl.find ts s);;
408   os oc "(";
409   oiter oc (fun oc v -> os oc (Tmm.find v bnd); os oc "::"; oty_isa ts oc (type_of v)) ") (" bs;
410   os oc ").";;
416     os oc "(ALL"; pr_bs_isa oc bnd ts bs; otm_isa oc (bnd, used) cs ts bod; os oc ")"
420     os oc "(EX"; pr_bs_isa oc bnd ts bs; otm_isa oc (bnd, used) cs ts bod; os oc ")"
424     os oc "(%"; pr_bs_isa oc bnd ts bs; otm_isa oc (bnd, used) cs ts bod; os oc ")"
426     (os oc "("; oiter oc (fun oc e -> otm_isa oc (bnd, used) cs ts e) " & " (conjuncts tm); os oc ")")
428     (os oc "("; oiter oc (fun oc e -> otm_isa oc (bnd, used) cs ts e) " | " (disjuncts tm); os oc ")")
430     (os oc "("; otm_isa oc (bnd, used) cs ts l; os oc " --> ";
431                otm_isa oc (bnd, used) cs ts r; os oc ")")
433     let t = dest_neg tm in (os oc "(~"; otm_isa oc (bnd,used) cs ts t; os oc ")")
435     (os oc "("; otm_isa oc (bnd, used) cs ts l; os oc " = ";
436     otm_isa oc (bnd, used) cs ts r; os oc ")")
438     (os oc "("; oiter oc (fun oc e -> otm_isa oc (bnd, used) cs ts e) " " (hop :: args); os oc ")")
439   else if is_const tm then os oc (Hashtbl.find cs (fst (dest_const tm)))
440   else os oc (try Tmm.find tm bnd with Not_found -> failwith ("tm_isa:" ^ (fst (dest_var tm))));;
454   os oc "theory Bla imports \"~~/src/HOL/TPTP/ATP_Problem_Import\" begin\n";
466       os oc "typedecl ";
467       (if a > 0 then (os oc "("; os oc
468                         (String.concat "," (Array.to_list (Array.init a (fun i -> "'" ^ (String.make 1 (Char.chr (65 + i))))))); os oc ") ") else ());
469       os oc sty; os oc "\n"
473   os oc "axiomatization\n";
474   oiter oc (fun oc (t, s) -> os oc s; os oc " :: \""; oty_isa ts oc (get_const_type t); os oc "\"\n") "and " (hash_to_list cs);
476   os oc "axiomatization where\n";
477   oiter oc (fun oc (n, t) -> os oc n; os oc ": \""; otm_isa oc (Tmm.empty, Sm.empty) cs ts t; os oc "\"\n") "and " (zip (rev names) asms);
478   os oc "lemma conjecture:\n  \"";
479   otm_isa oc (Tmm.empty, Sm.empty) cs ts gl; os oc "\"\n"
495   os oc "("; (if List.length tys1 > 1 then os oc "(" else ());
497   (if List.length tys1 > 1 then os oc ")" else ());
498   os oc " > "; oty_poly ts 0 oc ty2; os oc ")"
522   let ohdr s1 s2 = os oc "tff("; os oc s1; os oc ", "; os oc s2; os oc ", " in
523   let otl () = os oc ").\n" in
524   os oc "%   TYPES\n";
527     ohdr t "type"; os oc s; os oc ":";
529       0 -> os oc "$tType"
530     | 1 -> os oc "$tType > $tType"
531     | n -> os oc "("; oiter oc (fun oc _ -> os oc "$tType") " * " (Array.to_list (Array.make n ()));
532         os oc ") > $tType" end; otl ()) (funtys_of_tms (gl::asms));
533   os oc "%   CONSTS\n";
534   ohdr "cp" "type"; os oc "p : (bool > $o)"; otl ();
537     ohdr c "type"; os oc (Hashtbl.find cs c); os oc ":";
541   os oc "%   AXIOMS\n";
562     os oc "s("; oty_poly ts 0 oc (type_of tm); os oc ","; os oc (
564     os oc ")"
567     os oc "s("; oty_poly ts 0 oc (type_of tm); os oc ","; os oc (
570       (os oc "("; oiter oc (fun oc e -> fof_tm oc (bnd, used) cs ts e) "," args; os oc ")"));
571     os oc ")"
576   if is_var tm then os oc (Tmm.find tm bnd)
579     os oc (Hashtbl.find cs (fst (dest_const f)));
581       (os oc "("; oiter oc (fun oc e -> fof_tm_unsafe oc (bnd, used) cs ts e) "," args; os oc ")"));;
587     os oc "![";oiter oc (fun oc v -> os oc (Tmm.find v bnd)) ", " vs;os oc "]: ";fof_pred oc (bnd, used) cs ts bod
591     os oc "?[";oiter oc (fun oc v -> os oc (Tmm.find v bnd)) ", " vs;os oc "]: ";fof_pred oc (bnd, used) cs ts bod
593     (os oc "("; fof_pred oc (bnd, used) cs ts l; os oc " & "; fof_pred oc (bnd, used) cs ts r; os oc ")")
595     (os oc "("; fof_pred oc (bnd, used) cs ts l; os oc " | "; fof_pred oc (bnd, used) cs ts r; os oc ")")
597     (os oc "("; fof_pred oc (bnd, used) cs ts l; os oc " => "; fof_pred oc (bnd, used) cs ts r; os oc ")")
599     let t = dest_neg tm in (os oc "~ ("; fof_pred oc (bnd,used) cs ts t; os oc ")")
602       (os oc "("; fof_pred oc (bnd, used) cs ts l; os oc " <=> ";
603       fof_pred oc (bnd, used) cs ts r; os oc ")")
605       (fof_tm oc (bnd, used) cs ts l; os oc " = "; fof_tm oc (bnd, used) cs ts r)
607     (os oc "p("; fof_tm oc (bnd, used) cs ts tm; os oc ")");;
611   (if tvs <> [] then (os oc "!["; oiter oc (fun oc e -> oty_poly ts 0 oc e) "," tvs; os oc "]: "));
616   let ohdr s1 s2 = os oc "fof("; os oc s1; os oc ", "; os oc s2; os oc ", " in
617   let otl () = os oc ").\n" in