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

2 3 4 5 6 7
(*

  small helpers

 *)

8
let get_opt o = Js.Opt.get o (fun () -> assert false)
9

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

12 13 14 15 16 17
(*

  module for generating HTML elements

*)

MARCHE Claude's avatar
MARCHE Claude committed
18 19
module Html = struct

20
let d = Dom_html.document
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23

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

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

MARCHE Claude's avatar
MARCHE Claude committed
26 27 28 29
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
30

MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35 36 37 38 39 40 41
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
42

43
(*
44

45
  Interface to Why3 and Alt-Ergo
46

47
*)
MARCHE Claude's avatar
MARCHE Claude committed
48

49
let why3_conf_file = "/trywhy3.conf"
50

MARCHE Claude's avatar
MARCHE Claude committed
51
open Why3
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 81 82 83 84 85
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
86 87
  let lb = Lexing.from_string text in
(* from Alt-Ergo *)
88
  let _a = Why_parser.file Why_lexer.token lb in
89 90
(* TODO ! *)
(*
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
  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)
*)
110 111 112
  text

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

114 115 116 117 118 119 120 121 122 123 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 151 152 153 154 155 156 157
let why3_prove theories =
  let theories =
    Stdlib.Mstr.fold
      (fun thname th acc ->
        let tasks = Task.split_theory th None None in
        let tasks = List.map
          (fun t ->
            let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
            let expl = match expl with
              | Some s -> s
              | None -> id.Ident.id_string
            in
            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

let why3_execute (modules,_theories) =
  let mods =
    Stdlib.Mstr.fold
      (fun _k m acc ->
        let th = m.Mlw_module.mod_theory in
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
        let modname = th.Theory.th_name.Ident.id_string in
        try
          let ps =
            Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
          in
          let moduleans = Html.of_string ("Module " ^ modname ^ ": ") in
          let ans =
            match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
            | None ->
              [moduleans;
               Html.ul
                 [[Html.of_string "function main has no definition"]]]
            | Some d ->
              try
                [moduleans;
                 Html.ul
                   [[Html.of_string
175
                        (Pp.sprintf "Execution of main () returns:@\n%a"
176 177 178 179 180 181 182 183 184 185 186
                           (Mlw_interp.eval_global_symbol env m) d)]]]
              with e ->
                [moduleans;
                 Html.ul
                   [[Html.of_string
                        (Pp.sprintf
                           "exception during execution of function main : %a (%s)"
                         Exn_printer.exn_printer e
                           (Printexc.to_string e))]]]
          in ans :: acc
        with Not_found -> acc)
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
      modules []
  in
  Html.ul mods

(* from ../tools/why3execute.ml

  let do_exec (mid,name) =
    let m = try Mstr.find mid mm with Not_found ->
      eprintf "Module '%s' not found.@." mid;
      exit 1 in
    let ps =
      try Mlw_module.ns_find_ps m.Mlw_module.mod_export [name]
      with Not_found ->
        eprintf "Function '%s' not found in module '%s'.@." name mid;
        exit 1 in
    match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
    | None ->
      eprintf "Function '%s.%s' has no definition.@." mid name;
      exit 1
    | Some d ->
      try
        printf "@[<hov 2>Execution of %s.%s ():@\n" mid name;
        Mlw_interp.eval_global_symbol env m d;
      with e when Debug.test_noflag Debug.stack_trace ->
        printf "@\n@]@.";
        raise e in
  Queue.iter do_exec opt_exec

*)

217 218 219 220 221 222 223 224 225 226 227 228

(*

   Connecting why3 calls to the interface

 *)

let temp_file_name = "/input.mlw"

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

229
let run_why3 f lang global text =
230 231 232
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
233 234
  try
    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
235 236
    let theories = Env.read_file lang env temp_file_name in
    f theories
237 238 239
  with
  | Loc.Located(loc,e') ->
    let (_,l,b,e) = Loc.get loc in
240 241
    ignore (Js.Unsafe.meth_call global "highlightError"
	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
242 243 244 245 246 247 248 249 250 251 252
    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))]
253 254

let add_why3_cmd buttonname f lang =
255 256 257 258 259 260
  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
261
      let answer = run_why3 f lang global code in
262 263 264 265 266 267 268
      (* 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;
269
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
270
      Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
271
  in
272
  let button =
273
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
274 275
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
276

277 278 279 280
let () =
  add_why3_cmd "prove" why3_prove Env.base_language;
  add_why3_cmd "run" why3_execute Mlw_module.mlw_language

281 282 283 284 285 286 287

(*

  Predefined examples

*)

288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
let add_file_example buttonname file =
  let handler = Dom.handler
    (fun _ev ->
      let text = Sysutil.file_contents file in
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
      Js.Unsafe.set global (Js.string "loadedBuffer") (Js.string text);
      let loaded = Filename.basename file in
      Js.Unsafe.set global (Js.string "loadedFilename") (Js.string loaded);
      ignore (Js.Unsafe.meth_call global "replaceWithLoaded" [| |]);
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
      Js._false)
  in
  let button =
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
  in
  button ## onclick <- handler

let () =
  add_file_example "drinkers" "/drinkers.why";
  add_file_example "simplearith" "/simplearith.why";
  add_file_example "isqrt" "/isqrt.mlw"

MARCHE Claude's avatar
MARCHE Claude committed
311 312 313 314 315 316

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