1structure writerLib :> writerLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5 6val writer_prints = ref true; 7 8local 9 val filename_base = ref "output_"; 10 val filename_current = ref ""; 11 val current_graph_file = ref (NONE:TextIO.outstream option) 12 val last_line_is_blank = ref false; 13 fun remove_trailing_underscores s = let 14 fun aux (#"_"::cs) = aux cs | aux xs = String.implode (rev xs) 15 in aux (rev (String.explode s)) end 16 fun graph_filename () = remove_trailing_underscores (!filename_base) ^ "_mc_graph.txt" 17 fun print_fail str = (print (str ^ "\n"); failwith str); 18in 19 fun reset_graph_file () = 20 TextIO.closeOut (TextIO.openOut (graph_filename ())) 21 handle Io _ => () 22 fun close_current () = 23 ((case !current_graph_file of NONE => () | SOME f => TextIO.closeOut f); 24 (current_graph_file := NONE)) 25 fun write_graph str = 26 case !current_graph_file of 27 NONE => print_fail "Attempt to write to graph file, but no graph file open." 28 | SOME f => TextIO.output (f,str) 29 fun open_current sec_name = 30 (close_current (); 31 filename_current := sec_name; last_line_is_blank := false; 32 current_graph_file := SOME (TextIO.openAppend (graph_filename ())); 33 write_graph "\n") 34 fun set_base filename = 35 (close_current (); 36 filename_base := filename; 37 reset_graph_file ()) 38 fun write_txt_and_print str = 39 (if !writer_prints then print str else ()) 40 fun write_blank_line () = 41 if !last_line_is_blank then () else 42 (write_txt_and_print "\n"; last_line_is_blank := true) 43 fun write_line str = 44 (write_txt_and_print (str ^ "\n"); 45 last_line_is_blank := (size str = 0)) 46 fun write_section str = 47 (write_blank_line (); 48 write_line str; 49 write_line (String.translate (fn c => "=") str); 50 write_blank_line ()) 51 fun write_subsection str = 52 (write_blank_line (); 53 write_line str; 54 write_line (String.translate (fn c => "-") str); 55 write_blank_line ()) 56 fun write_indented_block str = let 57 val lines = String.tokens (fn c => c = #"\n") str 58 in (write_blank_line (); 59 map (fn l => if l = "" then () else write_line (" " ^ l)) lines; 60 write_blank_line ()) end 61 fun write_term th = let 62 val _ = set_trace "PPBackEnd use annotations" 0 63 val _ = write_indented_block (term_to_string th) 64 val _ = set_trace "PPBackEnd use annotations" 1 65 in () end 66 fun write_thm th = let 67 val _ = set_trace "PPBackEnd use annotations" 0 68 val a = !Globals.show_assums 69 val _ = Globals.show_assums := false 70 val _ = write_indented_block (thm_to_string th) 71 val _ = set_trace "PPBackEnd use annotations" 1 72 in Globals.show_assums := a end 73end 74 75end 76