why3session_html.ml 13.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
21
open Why3
22
module C = Whyconf
23 24 25 26 27 28

let files = Queue.create ()
let opt_version = ref false
let output_dir = ref ""
let allow_obsolete = ref true
let opt_config = ref None
29
let opt_context = ref false
30

31 32 33 34 35 36 37 38 39 40
type style =
  | Simple
  | Jstree

let opt_style = ref Jstree

let set_opt_style = function
  | "simple" -> opt_style := Simple
  | "jstree" -> opt_style := Jstree
  | _ -> assert false
41

42 43 44 45 46 47 48 49 50
let opt_pp = ref []

let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
  let suf = ref "" in
  let cmd = ref "" in
  (fun s -> suf := s),
  (fun s -> cmd := s),
  (fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)

51 52 53
let spec = Arg.align [
  ("-v",
   Arg.Set opt_version,
54
   " Print version information") ;
55 56
  ("-o",
   Arg.Set_string output_dir,
57
   " The directory to output the files ('-' for stdout)");
58 59
  ("--strict",
   Arg.Clear allow_obsolete,
60
   " Forbid obsolete session");
61 62 63
  "-C", Arg.String (fun s -> opt_config := Some s),
      "<file> Read configuration from <file>";
  "--config", Arg.String (fun s -> opt_config := Some s),
64 65 66 67 68
      " Same as -C";
  "--context", Arg.Set opt_context,
  " Add context around the generated code in order to allow direct \
    visualisation (header, css, ...). It also add in the directory \
    all the needed external file. It can't be set with stdout output";
69 70
  "--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
  " Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
71 72 73 74 75 76 77 78 79 80 81 82
    the 'jstree' plugin of the javascript library 'jquery'.";
  "--add_pp", Arg.Tuple
    [Arg.String set_opt_pp_in;
     Arg.String set_opt_pp_cmd;
     Arg.String set_opt_pp_out],
  "<suffix> <cmd> <out_suffix> \
Add for the given prefix the given pretty-printer, \
the new file as the given out_suffix. cmd must contain '%i' which will be \
replace by the input file and '%o' which will be replaced by the output file.";
    "--coqdoc",
  Arg.Unit (fun ()->
    opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
83 84 85 86
  " same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'";
    Debug.Opt.desc_debug_list;
    Debug.Opt.desc_debug_all;
    Debug.Opt.desc_debug;
87 88 89
]


90
(*
91
let version_msg = sprintf
92 93 94
  "Why3 html session output, version %s (build date: %s)"
  Config.version Config.builddate

95
let usage_str = sprintf
96 97 98 99 100 101 102 103 104
  "Usage: %s [options] [<file.why>|<project directory>] ... "
  (Filename.basename Sys.argv.(0))

let set_file f = Queue.push f files

let () = Arg.parse spec set_file usage_str

let () =
  if !opt_version then begin
105
    printf "%s@." version_msg;
106 107
    exit 0
  end
108
*)
109

110 111 112 113
(* let () = *)
(*   List.iter (fun (in_,(cmd,out)) -> *)
(*     printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)

114
(*
115 116 117
let () =
  Debug.Opt.set_flags_selected ();
  if  Debug.Opt.option_list () then exit 0
118
*)
119

120
let output_dir =
121
  match !output_dir with
122 123 124
 (*
   | "" -> 
      printf "Error: output_dir must be set@.";
125 126 127 128 129
      exit 1
    | "-" when !opt_context ->
      printf
        "Error: context and stdout output can't be set at the same time@.";
      exit 1
130
 *)
131
    | _ -> !output_dir
132

133 134
let edited_dst = Filename.concat output_dir "edited"

François Bobot's avatar
François Bobot committed
135 136 137
let whyconf = Whyconf.read_config !opt_config

open Session
138 139
open Util

140
type context =
141
    (string ->
François Bobot's avatar
François Bobot committed
142
     (formatter -> notask session -> unit) -> notask session
143 144 145 146 147
     -> unit, formatter, unit) format

let run_file (context : context) print_session f =
  let session_path = get_project_dir f in
  let basename = Filename.basename session_path in
François Bobot's avatar
François Bobot committed
148
  let session = read_session session_path in
149 150 151 152 153 154 155 156 157 158 159 160 161
  let cout = if output_dir = "-" then stdout else
      open_out (Filename.concat output_dir (basename^".html")) in
  let fmt = formatter_of_out_channel cout in
  if !opt_context
  then fprintf fmt context basename (print_session basename) session
  else print_session basename fmt session;
  pp_print_flush fmt ();
  if output_dir <> "-" then close_out cout


module Simple =
struct

162
  let print_prover = Whyconf.print_prover
163 164

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
165
    | Undone _ -> fprintf fmt "Undone"
166 167 168
    | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
    | InternalFailure exn ->
      fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
169

170 171
  let print_proof_attempt fmt pa =
    fprintf fmt "<li>%a : %a</li>"
François Bobot's avatar
François Bobot committed
172
      print_prover pa.proof_prover
173 174 175 176 177
      print_proof_status pa.proof_state

  let rec print_transf fmt tr =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      tr.transf_name
François Bobot's avatar
François Bobot committed
178
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
179 180 181

  and print_goal fmt g =
    fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
François Bobot's avatar
François Bobot committed
182 183
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
184
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
185 186
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
187
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
188
      g.goal_transformations
189 190 191

  let print_theory fmt th =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
François Bobot's avatar
François Bobot committed
192 193
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
194 195 196 197

  let print_file fmt f =
    fprintf fmt "<li>%s : <ul>%a</ul></li>"
      f.file_name
François Bobot's avatar
François Bobot committed
198
      (Pp.print_list Pp.newline print_theory) f.file_theories
199 200 201

  let print_session _name fmt s =
    fprintf fmt "<ul>%a</ul>"
François Bobot's avatar
François Bobot committed
202 203
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
         print_file) s.session_files
204 205 206


  let context : context = "<!DOCTYPE html
207 208 209 210
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
211
<title>Why3 session of %s</title>
212 213 214 215 216 217
</head>
<body>
%a
</body>
</html>
"
218

219 220
  let run_files () =
  Queue.iter (run_file context print_session) files
221

222
end
223

224 225 226
module Jstree =
struct

227 228 229 230 231
  let print_verified fmt b =
    if b
    then fprintf fmt "class='verified'"
    else fprintf fmt "class='notverified'"

232
  let print_prover = Whyconf.print_prover
233 234

  let print_proof_status fmt = function
François Bobot's avatar
François Bobot committed
235
    | Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
236 237
    | Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
      Call_provers.print_prover_result pr
238
    | InternalFailure exn ->
239 240
      fprintf fmt "<span class='notverified'>Failure : %a</span>"
        Exn_printer.exn_printer exn
241

242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
  let cmd_regexp = Str.regexp "%\\(.\\)"

  let pp_run input cmd output =
    let replace s = match Str.matched_group 1 s with
      | "%" -> "%"
      | "i" -> input
      | "o" -> output
      | _ -> failwith "unknown format specifier, use %%i, %%o"
    in
    let cmd = Str.global_substitute cmd_regexp replace cmd in
    let c = Sys.command cmd in
    if c <> 0 then
      eprintf "[Error] '%s' stopped abnormaly : code %i" cmd c

  let find_pp edited =
    let basename = Filename.basename edited in
    try
      let suff,(cmd,suff_out) =
        List.find (fun (s,_) -> ends_with basename s) !opt_pp in
      let base =
        String.sub basename 0 (String.length basename - String.length suff) in
      let base_dst = (base^suff_out) in
      if !opt_context then
        pp_run edited cmd (Filename.concat edited_dst base_dst);
      base_dst
    with Not_found ->
      eprintf "Default %s@." basename;
      (** default printer *)
      let base = try Filename.chop_extension basename with _ -> basename in
      let base_dst = base^".txt" in
      if !opt_context then
        Sysutil.copy_file edited (Filename.concat edited_dst base_dst);
      base_dst

276
  let print_proof_attempt fmt pa =
François Bobot's avatar
François Bobot committed
277
    match pa.proof_edited_as with
278 279
      | None ->
        fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
François Bobot's avatar
François Bobot committed
280
          print_prover pa.proof_prover
281 282 283 284 285 286
          print_proof_status pa.proof_state
      | Some f ->
        let output = find_pp f in
        fprintf fmt "@[<hov><li rel='prover' ><a href='#' \
onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
          output
François Bobot's avatar
François Bobot committed
287
          print_prover pa.proof_prover
288
          print_proof_status pa.proof_state
289 290 291

  let rec print_transf fmt tr =
    fprintf fmt
292 293 294
      "@[<hov><li rel='transf'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified tr.transf_verified
295
      tr.transf_name
François Bobot's avatar
François Bobot committed
296
      (Pp.print_list Pp.newline print_goal) tr.transf_goals
297 298 299

  and print_goal fmt g =
    fprintf fmt
300 301 302
      "@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
      print_verified g.goal_verified
François Bobot's avatar
François Bobot committed
303 304
      g.goal_name.Ident.id_string
      (Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
305
         Pp.nothing print_proof_attempt)
François Bobot's avatar
François Bobot committed
306 307
      g.goal_external_proofs
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
308
         Pp.nothing print_transf)
François Bobot's avatar
François Bobot committed
309
      g.goal_transformations
310 311 312

  let print_theory fmt th =
    fprintf fmt
313 314 315
      "@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified th.theory_verified
François Bobot's avatar
François Bobot committed
316 317
      th.theory_name.Ident.id_string
      (Pp.print_list Pp.newline print_goal) th.theory_goals
318 319

  let print_file fmt f =
320 321 322 323
    fprintf fmt
      "@[<hov><li rel='file'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
      print_verified f.file_verified
324
      f.file_name
François Bobot's avatar
François Bobot committed
325
      (Pp.print_list Pp.newline print_theory) f.file_theories
326 327 328 329

  let print_session_aux name fmt s =
    fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
      name
François Bobot's avatar
François Bobot committed
330 331
      (Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
      s.session_files
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380


  let print_session name fmt s =
    fprintf fmt
      "<a href='#' onclick=\"$('#%s_session').jstree('open_all');\">
expand all
</a> <a href='#' onclick=\"$('#%s_session').jstree('close_all');\">
close all
</a>
<div id=\"%s_session\" class=\"session\">
%a
</div>
<script type=\"text/javascript\" class=\"source\">
$(function () {
  $(\"#%s_session\").jstree({ 
      \"types\" : {
	   \"types\" : {
	   \"file\" : {
		\"icon\" : { \"image\" : \"images/folder16.png\"},
		      },
	   \"theory\" : {
		\"icon\" : { \"image\" : \"images/folder16.png\"},
		      },
	   \"goal\" : {
		\"icon\" : { \"image\" : \"images/file16.png\"},
		      },
	   \"prover\" : {
		\"icon\" : { \"image\" : \"images/wizard16.png\"},
		      },
	   \"transf\" : {
		\"icon\" : { \"image\" : \"images/configure16.png\"},
		      },
                        }
                },
      \"plugins\" : [\"themes\",\"html_data\",\"types\"]
        });
});
</script>
"
  name name name (print_session_aux name) s name


  let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
    <meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\" />
    <title>Why3 session of %s</title>
381 382
    <link rel=\"stylesheet\" type=\"text/css\"
     href=\"javascript/session.css\" />
383
    <script type=\"text/javascript\" src=\"javascript/jquery.js\"></script>
384 385 386 387
    <script type=\"text/javascript\" src=\"javascript/jquery.jstree.js\">\
</script>
    <script type=\"text/javascript\" src=\"javascript/session.js\">\
</script>
388 389 390
</head>
<body>
%a
391 392 393 394 395 396 397 398
<iframe src=\"\"  id='edited'>
<p>Your browser does not support iframes.</p>
</iframe>
<script type=\"text/javascript\" class=\"source\">
$(function () {
  $('#edited').hide()
})
</script>
399 400 401 402 403
</body>
</html>
"

  let run_files () =
404 405
    if !opt_context then
      if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
406 407
    Queue.iter (run_file context print_session) files;
    if !opt_context then
François Bobot's avatar
François Bobot committed
408
      let data_dir = Whyconf.datadir (Whyconf.get_main whyconf) in
409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425
      (** copy images *)
      let img_dir_src = Filename.concat data_dir "images" in
      let img_dir_dst = Filename.concat output_dir "images" in
      if not (Sys.file_exists img_dir_dst) then Unix.mkdir img_dir_dst 0o755;
      List.iter (fun img_name ->
        let from = Filename.concat img_dir_src img_name in
        let to_  = Filename.concat img_dir_dst img_name in
        Sysutil.copy_file from to_)
        ["folder16.png";"file16.png";"wizard16.png";"configure16.png"];
      (** copy javascript *)
      let js_dir_src = Filename.concat data_dir "javascript" in
      let js_dir_dst = Filename.concat output_dir "javascript" in
      Sysutil.copy_dir js_dir_src js_dir_dst

end


426
(*
427 428 429 430
let () =
  match !opt_style with
    | Simple -> Simple.run_files ()
    | Jstree -> Jstree.run_files ()
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
*)

let run_one _fname = ()

open Why3session_lib

let run () =
  let should_exit1 = read_simple_spec () in
  if should_exit1 then exit 1;
  iter_files run_one


let cmd =
  { cmd_spec = spec;
    cmd_desc = "output session in HTML format.";
    cmd_name = "html";
    cmd_run  = run;
  }