Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

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

2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23


let examples =
  ["Drinkers paradox",
"theory T

   (** 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
"
  ]

(** Rendering in the browser *)

MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
module D = Dom_html

let d = D.document

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

let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e

let html_of_string (s:string) =
  d##createElement (Js.string "p") <|
      [node (d##createTextNode (Js.string s))]

let replace_child p n =
  Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
  Dom.appendChild p n

let temp_file_name = "/input.mlw"

42 43 44
let () =
  Sys_js.register_file ~name:temp_file_name ~content:"";

MARCHE Claude's avatar
MARCHE Claude committed
45 46 47 48
open Why3

let run textbox preview _ =
  let text = Js.to_string (textbox##value) in
49 50 51
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
MARCHE Claude's avatar
MARCHE Claude committed
52 53 54 55
  let env = Env.create_env [] in
  let answer =
    try
      let _x = Env.read_file Env.base_language env temp_file_name in
56 57 58 59 60 61 62
      "parsing and typing OK"
    with
    | Loc.Located(loc,Parser.Error) ->
      let (_,l,b,e) = Loc.get loc in
      Pp.sprintf "syntax error line %d, columns %d-%d" l b e
    | Loc.Located(loc,e') ->
      let (_,l,b,e) = Loc.get loc in
MARCHE Claude's avatar
MARCHE Claude committed
63
      Pp.sprintf
64 65 66 67 68
        "error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e'
    | e ->
      Pp.sprintf
        "unexpected exception: %a (%s)" Exn_printer.exn_printer e
        (Printexc.to_string e)
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72 73 74 75 76
  in
  replace_child preview (html_of_string answer);
  Js._false

let onload (_event : #Dom_html.event Js.t) : bool Js.t =
  let body =
    Js.Opt.get (d##getElementById(Js.string "trywhy3"))
      (fun () -> assert false) in
77
  (* first, the textbox *)
MARCHE Claude's avatar
MARCHE Claude committed
78 79
  let textbox = D.createTextarea d in
  textbox##rows <- 20; textbox##cols <- 100;
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
  Dom.appendChild body textbox;
  Dom.appendChild body (D.createBr d);
  (* second, the example buttons *)
  List.iter
    (fun (name,text) ->
      let b = D.createButton ~name:(Js.string name) d in
      b##textContent <- Js.some (Js.string name);
      Dom.appendChild body b;
      b##onclick <-
        D.handler
        (fun _ ->
          textbox##textContent <- Js.some (Js.string text);
          Js._false))
    examples;
  Dom.appendChild body (D.createBr d);
  (* third, the go button *)
MARCHE Claude's avatar
MARCHE Claude committed
96 97
  let go = D.createButton ~name:(Js.string "go") d in
  go##textContent <- Js.some (Js.string "Go");
98 99 100
  Dom.appendChild body go;
  Dom.appendChild body (D.createBr d);
  (* then, the answer zone *)
MARCHE Claude's avatar
MARCHE Claude committed
101
  let preview = D.createDiv d in
102
  go##onclick <- D.handler (run textbox preview);
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106 107 108
  preview##style##border <- Js.string "1px black";
  preview##style##padding <- Js.string "5px";
  Dom.appendChild body preview;
  Js._false

let _ = D.window##onload <- D.handler onload