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

2
3
4
5
6
7
8
9
10
11
12
13
14
(*

  small helpers

 *)

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

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


15
16
17
18
19
20
(*

  module for generating HTML elements

*)

MARCHE Claude's avatar
MARCHE Claude committed
21
22
module Html = struct

23
let d = Dom_html.document
MARCHE Claude's avatar
MARCHE Claude committed
24
25
26

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

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

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

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

46
(*
47

48
  Interface to Why3 and Alt-Ergo
49

50
*)
MARCHE Claude's avatar
MARCHE Claude committed
51

52
let why3_conf_file = "/trywhy3.conf"
53

MARCHE Claude's avatar
MARCHE Claude committed
54
open Why3
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
86
87
88
89
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 ! *)
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(* 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)
*)
111
112
113
  text

let split_trans = Trans.lookup_transform_l "split_goal_wp" env
MARCHE Claude's avatar
MARCHE Claude committed
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
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
        let name = th.Theory.th_name.Ident.id_string in
        [Html.of_string ("Module " ^ name)] :: acc)
      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

*)

191
192
193
194
195
196
197
198
199
200
201
202

(*

   Connecting why3 calls to the interface

 *)

let temp_file_name = "/input.mlw"

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

203
let run_why3 f lang global text =
204
205
206
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
207
208
  try
    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
209
210
    let theories = Env.read_file lang env temp_file_name in
    f theories
211
212
213
  with
  | Loc.Located(loc,e') ->
    let (_,l,b,e) = Loc.get loc in
214
215
    ignore (Js.Unsafe.meth_call global "highlightError"
	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
216
217
218
219
220
221
222
223
224
225
226
    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))]
227
228

let add_why3_cmd buttonname f lang =
229
230
231
232
233
234
  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
235
      let answer = run_why3 f lang global code in
236
237
238
239
240
241
242
      (* 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;
243
      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
244
      Js._false)
MARCHE Claude's avatar
MARCHE Claude committed
245
  in
246
  let button =
247
    get_opt (Dom_html.document ## getElementById (Js.string buttonname))
248
249
  in
  button ## onclick <- handler
MARCHE Claude's avatar
MARCHE Claude committed
250

251
252
253
254
let () =
  add_why3_cmd "prove" why3_prove Env.base_language;
  add_why3_cmd "run" why3_execute Mlw_module.mlw_language

255
256
257
258
259
260
261

(*

  Predefined examples

*)

262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
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
285
286
287
288
289
290

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