trywhy3.ml 5.73 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2

MARCHE Claude's avatar
MARCHE Claude committed
3 4
module D = Dom_html

MARCHE Claude's avatar
MARCHE Claude committed
5 6
module Html = struct

MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10
let d = D.document

let node x = (x : #Dom.node Js.t :> Dom.node Js.t)

MARCHE Claude's avatar
MARCHE Claude committed
11
let of_string s = node (d##createTextNode (Js.string s))
MARCHE Claude's avatar
MARCHE Claude committed
12

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16
let par nl =
  let x = d##createElement (Js.string "p") in
  List.iter (Dom.appendChild x) nl;
  node x
MARCHE Claude's avatar
MARCHE Claude committed
17

MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21 22 23 24 25 26 27 28
let ul nl =
  let x = d##createElement (Js.string "ul") in
  List.iter
    (fun n ->
      let y =  d##createElement (Js.string "li") in
      List.iter (Dom.appendChild y) n;
      Dom.appendChild x (node y))
    nl;
  node x

end
MARCHE Claude's avatar
MARCHE Claude committed
29

30 31 32 33 34 35 36
let get_opt o =
  Js.Opt.get o (fun () -> assert false)

let log s =
  Firebug.console ## log (Js.string s)


MARCHE Claude's avatar
MARCHE Claude committed
37
let temp_file_name = "/input.mlw"
38
let why3_conf_file = "/why3.conf"
MARCHE Claude's avatar
MARCHE Claude committed
39

40
let () =
41
  Sys_js.register_file ~name:temp_file_name ~content:""
42

MARCHE Claude's avatar
MARCHE Claude committed
43
open Why3
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
open Format

(* reads the config file *)
let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
  if Whyconf.Mprover.is_empty provers then begin
    eprintf "Prover Alt-Ergo not installed or not configured@.";
    exit 0
  end else snd (Whyconf.Mprover.choose provers)

(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)


let alt_ergo_driver : Driver.driver =
  try
    Printexc.record_backtrace true;
    Driver.load_driver env alt_ergo.Whyconf.driver []
  with e ->
    let s = Printexc.get_backtrace () in
    eprintf "Failed to load driver for alt-ergo: %a@.%s@."
      Exn_printer.exn_printer e s;
  exit 1


let run_alt_ergo_on_task t =
  (* printing the task in a string *)
  Driver.print_task alt_ergo_driver str_formatter t;
  let text = flush_str_formatter () in
  (* TODO ! *)
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
(* from Alt-Ergo:
  let a = Why_parser.file Why_lexer.token lb in
  let ltd, typ_env = Why_typing.file false Why_typing.empty_env a in
  let declss = Why_typing.split_goals ltd in
  SAT.start ();
  let declss = List.map (List.map fst) declss in
  let report = FE.print_status in
  let pruning =
    List.map
      (fun d ->
        if select () > 0 then Pruning.split_and_prune (select ()) d
        else [List.map (fun f -> f,true) d])
  in
  List.iter
    (List.iter
       (fun dcl ->
	 let cnf = Cnf.make dcl in
	 ignore (Queue.fold (FE.process_decl report)
		   (SAT.empty (), true, Explanation.empty) cnf)
       )) (pruning declss)
*)
102 103 104
  text

let split_trans = Trans.lookup_transform_l "split_goal_wp" env
MARCHE Claude's avatar
MARCHE Claude committed
105

106
let prove global text =
107 108 109
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
110 111 112 113 114 115
  try
    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
    let theories = Env.read_file Env.base_language env temp_file_name in
    let theories =
      Stdlib.Mstr.fold
        (fun thname th acc ->
116
          let tasks = Task.split_theory th None None in
117 118 119
          let tasks = List.map
            (fun t ->
              let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
120 121 122 123
              let expl = match expl with
                | Some s -> s
                | None -> id.Ident.id_string
              in
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
              let tl = Trans.apply split_trans t in
              let tasks =
                List.map
                  (fun task ->
                    let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
                    let expl = match expl with
                      | Some s -> s
                      | None -> id.Ident.id_string
                    in
                    let result = run_alt_ergo_on_task task in
                    let result =
                      if String.length result > 80 then
                        "..." ^ String.sub result (String.length result - 80) 80
                      else result
                    in
                    [Html.of_string (expl ^" : " ^ result)])
                  tl
              in
              [Html.of_string expl; Html.ul tasks])
            tasks
          in
          [ Html.of_string ("Theory " ^ thname); Html.ul tasks]
          :: acc)
        theories []
    in
    Html.ul theories
  with
151
(*
152 153 154 155 156
  | Loc.Located(loc,Parser.Error) ->
    let (_,l,b,e) = Loc.get loc in
    Html.par
      [Html.of_string
          (Pp.sprintf "syntax error line %d, columns %d-%d" l b e)]
157
*)
158 159
  | Loc.Located(loc,e') ->
    let (_,l,b,e) = Loc.get loc in
160 161
    ignore (Js.Unsafe.meth_call global "highlightError"
	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
    Html.par
      [Html.of_string
          (Pp.sprintf
             "error line %d, columns %d-%d: %a" l b e
             Exn_printer.exn_printer e')]
  | e ->
    Html.par
      [Html.of_string
          (Pp.sprintf
             "unexpected exception: %a (%s)" Exn_printer.exn_printer e
             (Printexc.to_string e))]
let () =
  let handler = Dom.handler
    (fun _ev ->
      log "why3 prove is running";
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
      let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
180
      let answer = prove global code in
181 182 183 184 185 186 187
      (* remove the previous answer if any *)
      let console =
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
      in
      Js.Opt.iter (console##lastChild) (Dom.removeChild console);
      (* put the new answer *)
      Dom.appendChild console answer;
188
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
189
      Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
190
  in
191 192 193 194
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string "prove"))
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
195 196 197 198 199 200 201


(*
Local Variables:
compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
End:
*)