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

2
(* simple helpers *)
3

4
let get_opt o = Js.Opt.get o (fun () -> assert false)
5

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

8

9
(* module for generating HTML elements *)
10

MARCHE Claude's avatar
MARCHE Claude committed
11 12
module Html = struct

13
let d = Dom_html.document
MARCHE Claude's avatar
MARCHE Claude committed
14 15 16

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

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

19 20 21 22 23 24 25
let img i =
  let x = Dom_html.createImg d in
  x##src <- Js.string i;
  x##height <- 12;
  (* X##align <- Js.string "bottom"; *)
  node x

26 27 28 29
let img_accept () = img "accept32.png"
let img_help () = img "help32.png"
let img_bug () = img "bug32.png"

MARCHE Claude's avatar
MARCHE Claude committed
30 31 32 33
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
34

MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39 40 41 42 43 44 45
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
46

47

48
(* Interface to Why3 and Alt-Ergo *)
MARCHE Claude's avatar
MARCHE Claude committed
49

50
let why3_conf_file = "/trywhy3.conf"
51

MARCHE Claude's avatar
MARCHE Claude committed
52
open Why3
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
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

83 84 85 86 87 88 89 90 91 92 93 94
module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
module FE = Frontend.Make (SAT)

let print_status fmt _d status steps =
  match status with
  | FE.Unsat _dep ->
    fprintf fmt "Proved (%Ld steps)" steps
  | FE.Inconsistent -> ()
    (* fprintf fmt "Inconsistent assumption" *)
  | FE.Unknown _t | FE.Sat _t ->
      fprintf fmt "Unknown (%Ld steps)@." steps

95 96 97 98 99 100 101 102
type prover_answer = Valid | Unknown of string | Error of string

let report_status report _d status _steps =
  match status with
  | FE.Unsat _dep -> report Valid
  | FE.Inconsistent -> ()
  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")

103 104 105 106
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
107
  let lb = Lexing.from_string text in
108 109 110 111 112 113
(* from Alt-Ergo, src/main/frontend.ml *)
  let a = Why_parser.file Why_lexer.token lb in
  Parsing.clear_parser ();
  let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
  match Why_typing.split_goals ltd with
  | [d] ->
114
    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
115
    SAT.reset_steps ();
116 117 118 119 120 121 122 123 124 125 126
    let stat = ref (Error "no answer from Alt-Ergo") in
    let f s = stat := s in
    begin
      try
        let _x = Queue.fold (FE.process_decl (report_status f))
          (SAT.empty (), true, Explanation.empty) d
        in
        !stat
      with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
    end
  | _ -> Error "zero or more than 1 goal to solve"
127 128

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

130 131 132 133 134
let why3_prove theories =
  let theories =
    Stdlib.Mstr.fold
      (fun thname th acc ->
        let tasks = Task.split_theory th None None in
135
        let tasks = List.rev_map
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
          (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
152
                  let img,res = match result with
153 154 155
                    | Valid -> Html.img_accept, expl
                    | Unknown s -> Html.img_help, expl ^ " (" ^ s ^ ")"
                    | Error s -> Html.img_bug, expl ^ " (" ^ s ^ ")"
156
                  in
157
                  [img (); Html.of_string (" " ^ res)])
158 159 160 161 162
                tl
            in
            [Html.of_string expl; Html.ul tasks])
          tasks
        in
163 164 165 166
        let loc =
          Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
        in
        (loc,[ Html.of_string thname; Html.ul tasks]) :: acc)
167 168
      theories []
  in
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 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
  let s =
    List.sort
      (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
      theories
  in
  Html.ul (List.rev_map snd s)

let execute_symbol m fmt ps =
  match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
  | None ->
    fprintf fmt "function '%s' has no definition"
      ps.Mlw_expr.ps_name.Ident.id_string
  | Some d ->
    let lam = d.Mlw_expr.fun_lambda in
    match lam.Mlw_expr.l_args with
    | [pvs] when
        Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
      begin
        let spec = lam.Mlw_expr.l_spec in
        let eff = spec.Mlw_ty.c_effect in
        let writes = eff.Mlw_ty.eff_writes in
        let body = lam.Mlw_expr.l_expr in
        try
          let res, _final_env =
            Mlw_interp.eval_global_expr env m.Mlw_module.mod_known
              m.Mlw_module.mod_theory.Theory.th_known writes body
          in
          match res with
          | Mlw_interp.Normal v -> Mlw_interp.print_value fmt v
          | Mlw_interp.Excep(x,v) ->
            fprintf fmt "exception %s(%a)"
              x.Mlw_ty.xs_name.Ident.id_string Mlw_interp.print_value v
          | Mlw_interp.Irred e ->
            fprintf fmt "cannot execute expression@ @[%a@]"
              Mlw_pretty.print_expr e
          | Mlw_interp.Fun _ ->
            fprintf fmt "result is a function"
        with e ->
          fprintf fmt
            "failure during execution of function: %a (%s)"
            Exn_printer.exn_printer e
            (Printexc.to_string e)
    end
  | _ ->
    fprintf fmt "Only functions with one unit argument can be executed"
214 215 216 217 218 219

let why3_execute (modules,_theories) =
  let mods =
    Stdlib.Mstr.fold
      (fun _k m acc ->
        let th = m.Mlw_module.mod_theory in
220 221 222 223 224
        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
225 226 227 228 229 230
          let result = Pp.sprintf "%a" (execute_symbol m) ps in
          let loc =
            Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
          in
          (loc,[Html.of_string (modname ^ ".main() returns " ^ result)])
          :: acc
231
        with Not_found -> acc)
232 233
      modules []
  in
MARCHE Claude's avatar
MARCHE Claude committed
234 235 236 237 238 239 240 241 242
  match mods with
  | [] -> Html.par [Html.of_string "No main function found"]
  | _ ->
    let s =
      List.sort
        (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
        mods
    in
    Html.ul (List.rev_map snd s)
243

244

245
(* Connecting Why3 calls to the interface *)
246 247 248

let temp_file_name = "/input.mlw"

MARCHE Claude's avatar
MARCHE Claude committed
249
let () = Sys_js.register_file ~name:temp_file_name ~content:""
250

251
let run_why3 f lang global text =
252 253 254
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
255 256
  try
    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
257 258
    let theories = Env.read_file lang env temp_file_name in
    f theories
259 260 261
  with
  | Loc.Located(loc,e') ->
    let (_,l,b,e) = Loc.get loc in
262 263
    ignore (Js.Unsafe.meth_call global "highlightError"
	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
264 265 266 267 268 269 270 271 272 273 274
    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))]
275

MARCHE Claude's avatar
MARCHE Claude committed
276
let add_why3_cmd buttonname f input_lang =
277 278 279 280
  let handler = Dom.handler
    (fun _ev ->
      let global = Js.Unsafe.global in
      let editor = Js.Unsafe.get global (Js.string "editor") in
281 282
      let lang = "en"
(*
MARCHE Claude's avatar
MARCHE Claude committed
283 284 285
        Js.to_string
          (Js.Unsafe.meth_call editor "getAttribute"
             [| Js.Unsafe.inject (Js.string "lang") |])
286
*)
MARCHE Claude's avatar
MARCHE Claude committed
287
      in
288
      let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
MARCHE Claude's avatar
MARCHE Claude committed
289 290 291
      log ("Why3 is running, lang = " ^ lang);
      let answer = run_why3 f input_lang global code in
      log "Why3 answer given";
292 293 294
      let console =
        get_opt (Dom_html.document ## getElementById (Js.string "console"))
      in
MARCHE Claude's avatar
MARCHE Claude committed
295
      (* remove the previous answer if any *)
296 297 298
      Js.Opt.iter (console##lastChild) (Dom.removeChild console);
      (* put the new answer *)
      Dom.appendChild console answer;
MARCHE Claude's avatar
MARCHE Claude committed
299
      (* give the focus back to the editor *)
300
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
301
      Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
302
  in
303
  let button =
304
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
305 306
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
307

308 309 310 311
let () =
  add_why3_cmd "prove" why3_prove Env.base_language;
  add_why3_cmd "run" why3_execute Mlw_module.mlw_language

312

313
(* Predefined examples *)
314

315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
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";
335 336
(*  add_file_example "simplearith" "/simplearith.why";*)
  add_file_example "bin_mult" "/bin_mult.mlw";
337
  add_file_example "fact" "/fact.mlw";
338 339
  add_file_example "isqrt" "/isqrt.mlw";
  Options.set_steps_bound 100
340

MARCHE Claude's avatar
MARCHE Claude committed
341 342 343 344 345 346

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