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 4 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 27 28
";
   "Simple Arithmetic","
theory T

   use import int.Int

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

end
";
29 30
  ]

31 32 33 34 35 36 37 38
(** registering the std lib *)

let () =
  List.iter
    (fun (name,content) ->
      Sys_js.register_file ~name ~content;
    ) Theories.theories

39 40
(** Rendering in the browser *)

MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
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"

59 60 61
let () =
  Sys_js.register_file ~name:temp_file_name ~content:"";

MARCHE Claude's avatar
MARCHE Claude committed
62 63
open Why3

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 90 91 92 93 94 95 96
(* TODO: loading from standard library.

   piste: utiliser Sys_js.register_autoload et
   XmlHttpRequest.get

*)
let env = Env.create_env ["/theories" (*; "/modules"*)]

(*
let bad_suffix path name =
  match path with
  | "/theories" -> not (Filename.check_suffix name ".why")
  | "/modules" -> not (Filename.check_suffix name ".mlw")
  | _ -> true

let load_file_from_the_web (path,name) =
  if bad_suffix path name then None else
  let t = XmlHttpRequest.get
    ("http://why3.lri.fr/try" ^ path ^ "/" ^ name)
  in
  let c = ref "" in
  Lwt.on_success t
    (fun frame ->
      let content = frame. XmlHttpRequest.content in
      (* useless ?
         Sys_js.register_file ~name:(path ^ "/" ^ name) ~content; *)
      c := content);
  Some !c

let () = Sys_js.register_autoload ~path:"/theories" load_file_from_the_web
*)

let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
MARCHE Claude's avatar
MARCHE Claude committed
97
  let text = Js.to_string (textbox##value) in
98 99 100
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
MARCHE Claude's avatar
MARCHE Claude committed
101 102
  let answer =
    try
103 104 105
      let x = Env.read_file Env.base_language env temp_file_name in
      Pp.sprintf "parsing and typing OK, %d theories"
        (Stdlib.Mstr.cardinal x)
106 107 108 109 110 111
    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
112
      Pp.sprintf
113 114 115 116 117
        "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
118 119 120 121 122 123 124 125
  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
126
  (* first, the textbox *)
MARCHE Claude's avatar
MARCHE Claude committed
127 128
  let textbox = D.createTextarea d in
  textbox##rows <- 20; textbox##cols <- 100;
129 130 131 132 133 134 135 136 137 138
  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
139
        (fun (_ : D.mouseEvent Js.t) ->
140 141 142 143 144
          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
145 146
  let go = D.createButton ~name:(Js.string "go") d in
  go##textContent <- Js.some (Js.string "Go");
147 148 149
  Dom.appendChild body go;
  Dom.appendChild body (D.createBr d);
  (* then, the answer zone *)
MARCHE Claude's avatar
MARCHE Claude committed
150
  let preview = D.createDiv d in
151
  go##onclick <- D.handler (run textbox preview);
MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156 157
  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