1(* this is an -*- sml -*- file *) 2 3(* ====================================================================== 4 Automatic generation of clickable image maps of the 5 HOL theory hierarchy. 6 ---------------------------------------------------------------------- 7 8 The algorithm works as follows: 9 10 1. Generate the dependencies from the current theory hierarchy 11 2. Write them to a file ready for processing by "dot" 12 3. Invoke dot to generate the SVG image 13 4. Generate a HTML file to hold the reference to the image 14 5. Generate the html files for each segment in the current 15 theory hierarchy. 16 17 Before loading this file, you might need to tell "dot" where the 18 TrueType fonts that it needs are. On my Linux system, this used to 19 be: 20 21 DOTFONTPATH=/dosc/windows/fonts; export DOTFONTPATH 22 23 Run the file by 24 25 hol < DOT 26 27 ====================================================================== *) 28 29val _ = HOL_Interactive.toggle_quietdec(); 30 31fun die s = 32 (TextIO.output(TextIO.stdErr, s ^ "\n"); 33 TextIO.flushOut TextIO.stdErr; 34 OS.Process.exit OS.Process.failure) 35 36val HTML_DIR = Path.toString(Path.fromString(Path.concat 37 (Globals.HOLDIR,"help/theorygraph"))); 38val SIGOBJ_DIR = Path.toString(Path.fromString(Path.concat 39 (Globals.HOLDIR,"sigobj"))); 40 41val DOTPATH = 42 case Systeml.DOT_PATH of 43 NONE => die "No DOT_PATH in Systeml" 44 | SOME s => s 45 46(*--------------------------------------------------------------------------- 47 Extract dot-friendly digraph from HOL theory graph. 48 ---------------------------------------------------------------------------*) 49 50fun node thy = map (fn p => (p,thy)) (parents thy); 51 52local fun leq (s:string,_) (t,_) = s <= t 53in 54fun ancestor_nodes thy = 55 let val thys = ancestry thy 56 val pairs = sort leq (flatten (map node thys)) 57 in (thys, pairs) 58 end 59end; 60 61(*---------------------------------------------------------------------------*) 62(* There are lots of parameters that can be played with here. See the dot *) 63(* manual for tweakables. *) 64(*---------------------------------------------------------------------------*) 65 66fun pp_dot_file {size,ranksep,nodesep} (dom,pairs) = 67 let open Portable PP 68 fun pp_thy s = 69 block CONSISTENT 2 [ 70 add_string s, add_break (1,0), 71 add_string "[URL =", add_break(1,0), 72 add_string (quote (s^"Theory.html")), 73 add_string "]" 74 ] 75 fun pp_pair (x,y) = 76 block CONSISTENT 0 [add_string x, add_string " -> ", add_string y] 77 in 78 block CONSISTENT 0 [ 79 block CONSISTENT 5 [ 80 add_string "digraph G {", 81 add_break (1,0), 82 add_string "bgcolor = transparent", add_break(1,0), 83 add_string "ratio = compress", add_break(1,0), 84 add_string "size = ", add_string (quote size), add_break(1,0), 85 add_string "ranksep = ", add_string ranksep, add_break(1,0), 86 add_string "nodesep = ", add_string nodesep, add_break(1,0), 87 add_string "node [target=_parent style=filled fillcolor=white fontcolor=darkgreen fontsize=30 fontname=Arial]", 88 add_break(1,0), 89 add_newline, 90 block CONSISTENT 0 (pr_list pp_thy [add_newline] dom), 91 add_newline, add_newline, 92 block CONSISTENT 0 (pr_list pp_pair [add_newline] pairs) 93 ], 94 add_newline, add_string "}", add_newline 95 ] 96 end; 97 98fun gen_dotfile file node_info = 99 let open TextIO 100 val ostrm = openOut file 101 in 102 PP.prettyPrint(curry output ostrm, 75) 103 (pp_dot_file {size="16,16",ranksep="1.0",nodesep="0.30"} 104 node_info); 105 closeOut ostrm 106 end; 107 108(* ---------------------------------------------------------------------- 109 cat filename out 110 111 push contents of filename into outstream out 112 ---------------------------------------------------------------------- *) 113 114fun cat fname outstr = let 115 val instr = TextIO.openIn fname 116 val infile = TextIO.inputAll instr 117in 118 TextIO.output(outstr, infile) 119end 120 121(*--------------------------------------------------------------------------- 122 Parse theory coordinates generated by dot -Timap. Note that 123 these come (i,j) (p,q), but it seems that they should be 124 transformed to (i,q) (p,j) ... and so that's what we do! 125 ---------------------------------------------------------------------------*) 126 127fun gen_map_file dot node_info name = let 128 open TextIO 129 val dotfile = name^".dot" 130 val svgfile = name^".svg" 131 val mapfile = name^".html" 132 val _ = gen_dotfile dotfile node_info 133 val cmdstatus = Systeml.systeml [dot, 134 "-Tsvg", "-o"^svgfile, 135 dotfile] 136in 137 if OS.Process.isSuccess cmdstatus then let 138 val _ = print "Called dot successfully.\n" 139 val ostrm = openOut mapfile 140 fun out s = output(ostrm, s^"\n") 141 in 142 out "<!DOCTYPE html>"; 143 out "<HTML>"; 144 out "<META CHARSET=\"utf-8\">"; 145 out "<HEAD><TITLE>HOL Theory Hierarchy</TITLE></HEAD>"; 146 out "<BODY bgcolor=linen>"; 147 out "<H1>HOL Theory Hierarchy (clickable)</H1>"; 148 out (String.concat 149 ["<object data=\"",OS.Path.file svgfile,"\" type=\"image/svg+xml\">HOL Theory Map</object>"]); 150 out "</BODY>"; 151 out "</HTML>"; 152 closeOut ostrm 153 end 154 else raise Fail "gen_map_file: failed " 155end; 156 157fun dir_theories dir = let 158 open Substring FileSys 159 val dstrm = openDir dir 160 fun thys () = 161 case readDir dstrm of 162 NONE => [] 163 | SOME file => let 164 val (ss1,ss2) = position "Theory.sig" (full file) 165 in 166 if isEmpty ss1 orelse isEmpty ss2 orelse string ss1 = "Final" then 167 thys() 168 else string ss1 :: thys() 169 end 170in 171 thys() 172end; 173 174 175val load_theories = let 176 fun loadi i s = (if i mod 5 = 0 then print "." else () ; 177 load (s^"Theory")) 178in 179 appi loadi 180end 181 182fun pappi f (l1,l2) = let 183 fun recurse i (l1,l2) = 184 case (l1,l2) of 185 ([], _) => () 186 | (_, []) => () 187 | (h1::t1,h2::t2) => (f i (h1,h2) ; recurse (i + 1) (t1, t2)) 188in 189 recurse 0 (l1,l2) 190end 191 192(* ---------------------------------------------------------------------- 193 Up to this point, no work is done - the above just sets up 194 functions to do the work. What follows actually figures out what 195 the graph is and causes lots of stuff to be written to disk 196 ---------------------------------------------------------------------- *) 197 198val sys_theories = List.filter (not o String.isSuffix "_emit") 199 (dir_theories SIGOBJ_DIR); 200(* trailing spaces make this line up with HTML printing message later *) 201val _ = print "\n\nLoading system theories "; 202load_theories sys_theories; 203val _ = print " done\n" 204val ancs = ancestor_nodes "-"; 205 206val all_theories = "min"::sys_theories; 207val paths = map(fn s => Path.concat (HTML_DIR,s^"Theory.html")) all_theories; 208val _ = print "Printing HTML theories to disk "; 209fun appthis i (thy,path) = 210 (if i mod 5 = 0 then print "." else (); 211 print_theory_as_html thy path 212 handle Fail s => print (">>> PP failure on "^thy^": "^s^"\n")) 213val _ = pappi appthis (all_theories, paths); 214val _ = print " done\n"; 215 216(* The following works on Unix with dot version 1.10.2003xxxxxxx *) 217 218gen_map_file DOTPATH ancs (Path.concat(HTML_DIR, "theories")) 219 handle _ => 220 die ("Failed to call gen_map_file on dot="^DOTPATH^" targeting "^ 221 Path.concat(HTML_DIR, "theories")) 222; 223