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

2 3 4


let examples =
5 6
  [ "Drinkers paradox","
theory T
7 8 9 10 11 12 13 14 15 16 17 18

   (** Type of all persons *)
   type person

   (** Predicate saying that some person drinks *)
   predicate drinks person

   (** Paradox: there exists a person x such that if x drinks,
       then everybody drinks *)
   goal drinkers_paradox: exists x:person. drinks x -> forall y:person. drinks y

end
19 20 21 22 23 24 25 26
";
   "Simple Arithmetic","
theory T

   use import int.Int

   goal g: exists x:int. x*(x+1) = 42

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
end
";
"Integral square root","
module M

  use import int.Int
  use import ref.Ref

  function sqr (x:int) : int = x * x

  let isqrt (x:int) : int
    requires { x >= 0 }
    ensures { result >= 0 }
    ensures { result <= x < sqr (result + 1) }
  = let count = ref 0 in
    let sum = ref 1 in
    while !sum <= x do
      invariant { !count >= 0 }
      invariant { x >= sqr !count }
      invariant { !sum = sqr (!count+1) }
      variant   { x - !count }
      count := !count + 1;
      sum := !sum + 2 * !count + 1
    done;
    !count

  let main () ensures { result = 4 } = isqrt 17

55 56
end
";
57 58
  ]

59 60
(** registering the std lib *)

61
(*
62 63 64 65 66
let () =
  List.iter
    (fun (name,content) ->
      Sys_js.register_file ~name ~content;
    ) Theories.theories
67
*)
68

MARCHE Claude's avatar
MARCHE Claude committed
69

70 71
(** Rendering in the browser *)

MARCHE Claude's avatar
MARCHE Claude committed
72 73
module D = Dom_html

MARCHE Claude's avatar
MARCHE Claude committed
74 75
module Html = struct

MARCHE Claude's avatar
MARCHE Claude committed
76 77 78 79
let d = D.document

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

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

MARCHE Claude's avatar
MARCHE Claude committed
82 83 84 85
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
86

MARCHE Claude's avatar
MARCHE Claude committed
87 88 89 90 91 92 93 94 95 96 97
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
98 99

let temp_file_name = "/input.mlw"
100
let why3_conf_file = "/why3.conf"
MARCHE Claude's avatar
MARCHE Claude committed
101

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

MARCHE Claude's avatar
MARCHE Claude committed
105
open Why3
106 107 108 109 110 111 112 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
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 ! *)
  text

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

147
let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
MARCHE Claude's avatar
MARCHE Claude committed
148
  let text = Js.to_string (textbox##value) in
149 150 151
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
MARCHE Claude's avatar
MARCHE Claude committed
152
  let answer =
MARCHE Claude's avatar
MARCHE Claude committed
153
    try
154
      (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
MARCHE Claude's avatar
MARCHE Claude committed
155 156 157 158 159 160 161 162 163 164 165
      let theories = Env.read_file Env.base_language env temp_file_name in
(*
      Html.par
        [Html.of_string
           (Pp.sprintf "parsing and typing OK, %d theories"
              (Stdlib.Mstr.cardinal theories))]
*)
      let theories =
        Stdlib.Mstr.fold
          (fun thname th acc ->
            let tasks = Task.split_theory th None None in
MARCHE Claude's avatar
MARCHE Claude committed
166 167 168 169 170 171 172
            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
MARCHE Claude's avatar
MARCHE Claude committed
173
                let tl = Trans.apply split_trans t in
MARCHE Claude's avatar
MARCHE Claude committed
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
                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
MARCHE Claude's avatar
MARCHE Claude committed
193 194 195 196 197
            in
            [ Html.of_string ("Theory " ^ thname); Html.ul tasks]
            :: acc)
          theories []
      in
198
      Html.ul theories
MARCHE Claude's avatar
MARCHE Claude committed
199
(*
200 201 202 203 204 205 206 207 208 209 210 211 212
      Stdlib.Mstr.iter
        (fun _thname th ->
          let tasks = Task.split_theory th None None in
          List.iter
            (fun task ->
              let (id,expl,_) = Termcode.goal_expl_task ~root:true task in
              let expl = match expl with
                | Some s -> s
                | None -> id.Ident.id_string
              in
              push_answer
                (Pp.sprintf "Goal: %s@\n" expl))
            tasks)
MARCHE Claude's avatar
MARCHE Claude committed
213
*)
214 215 216
    with
    | Loc.Located(loc,Parser.Error) ->
      let (_,l,b,e) = Loc.get loc in
MARCHE Claude's avatar
MARCHE Claude committed
217 218 219
      Html.par
        [Html.of_string
            (Pp.sprintf "syntax error line %d, columns %d-%d" l b e)]
220 221
    | Loc.Located(loc,e') ->
      let (_,l,b,e) = Loc.get loc in
MARCHE Claude's avatar
MARCHE Claude committed
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')]
227
    | e ->
MARCHE Claude's avatar
MARCHE Claude committed
228 229 230 231 232 233 234 235 236 237
      Html.par
        [Html.of_string
            (Pp.sprintf
               "unexpected exception: %a (%s)" Exn_printer.exn_printer e
               (Printexc.to_string e))]
  in
  (* remove the previous answer if any *)
  Js.Opt.iter (preview##lastChild) (Dom.removeChild preview);
  (* put the new answer *)
  Dom.appendChild preview answer;
MARCHE Claude's avatar
MARCHE Claude committed
238 239 240
  Js._false

let onload (_event : #Dom_html.event Js.t) : bool Js.t =
MARCHE Claude's avatar
MARCHE Claude committed
241 242 243 244 245
  let input =
    Js.Opt.get (Html.d##getElementById(Js.string "input"))
      (fun () -> assert false) in
  let output =
    Js.Opt.get (Html.d##getElementById(Js.string "output"))
MARCHE Claude's avatar
MARCHE Claude committed
246
      (fun () -> assert false) in
247
  (* first, the textbox *)
MARCHE Claude's avatar
MARCHE Claude committed
248 249 250
  let textbox = D.createTextarea Html.d in
  textbox##rows <- 32; textbox##cols <- 64;
  Dom.appendChild input textbox;
251 252 253
  (* second, the example buttons *)
  List.iter
    (fun (name,text) ->
MARCHE Claude's avatar
MARCHE Claude committed
254
      let b = D.createButton ~name:(Js.string name) Html.d in
255
      b##textContent <- Js.some (Js.string name);
MARCHE Claude's avatar
MARCHE Claude committed
256
      Dom.appendChild output b;
257 258
      b##onclick <-
        D.handler
259
        (fun (_ : D.mouseEvent Js.t) ->
260
          textbox##value <- Js.string text;
261 262
          Js._false))
    examples;
MARCHE Claude's avatar
MARCHE Claude committed
263
  Dom.appendChild output (D.createBr Html.d);
264
  (* third, the go button *)
MARCHE Claude's avatar
MARCHE Claude committed
265
  let go = D.createButton ~name:(Js.string "go") Html.d in
MARCHE Claude's avatar
MARCHE Claude committed
266
  go##textContent <- Js.some (Js.string "Go");
MARCHE Claude's avatar
MARCHE Claude committed
267 268
  Dom.appendChild output go;
  Dom.appendChild output (D.createBr Html.d);
269
  (* then, the answer zone *)
MARCHE Claude's avatar
MARCHE Claude committed
270
  let preview = D.createDiv Html.d in
271
  go##onclick <- D.handler (run textbox preview);
MARCHE Claude's avatar
MARCHE Claude committed
272 273
  preview##style##border <- Js.string "1px black";
  preview##style##padding <- Js.string "5px";
MARCHE Claude's avatar
MARCHE Claude committed
274
  Dom.appendChild output preview;
MARCHE Claude's avatar
MARCHE Claude committed
275 276 277
  Js._false

let _ = D.window##onload <- D.handler onload
MARCHE Claude's avatar
MARCHE Claude committed
278 279 280 281 282 283 284


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