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