trywhy3.ml 4.68 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
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))]

53 54
let rec removeChildren p =
  Js.Opt.iter (p##lastChild) (fun c -> Dom.removeChild p c; removeChildren p)
MARCHE Claude's avatar
MARCHE Claude committed
55 56 57

let temp_file_name = "/input.mlw"

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

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

63 64 65 66 67 68
(* TODO: loading from standard library.

   piste: utiliser Sys_js.register_autoload et
   XmlHttpRequest.get

*)
69
let env = Env.create_env ["/theories" ; "/modules"]
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

(*
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
96
  let text = Js.to_string (textbox##value) in
97 98 99
  let ch = open_out temp_file_name in
  output_string ch text;
  close_out ch;
100 101 102
  let answer = ref [] in
  let push_answer s = answer := s :: !answer in
  begin
MARCHE Claude's avatar
MARCHE Claude committed
103
    try
104
      let x = Env.read_file Env.base_language env temp_file_name in
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
      push_answer
        (Pp.sprintf "parsing and typing OK, %d theories"
           (Stdlib.Mstr.cardinal x));
      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)
        x
122 123 124
    with
    | Loc.Located(loc,Parser.Error) ->
      let (_,l,b,e) = Loc.get loc in
125 126
      push_answer
        (Pp.sprintf "syntax error line %d, columns %d-%d" l b e)
127 128
    | Loc.Located(loc,e') ->
      let (_,l,b,e) = Loc.get loc in
129 130 131
      push_answer
        (Pp.sprintf
           "error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e')
132
    | e ->
133 134 135 136 137 138 139 140
      push_answer
        (Pp.sprintf
           "unexpected exception: %a (%s)" Exn_printer.exn_printer e
           (Printexc.to_string e))
  end;
  removeChildren preview;
  List.iter
    (fun s -> Dom.appendChild preview (html_of_string s)) (List.rev !answer);
MARCHE Claude's avatar
MARCHE Claude committed
141 142 143 144 145 146
  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
147
  (* first, the textbox *)
MARCHE Claude's avatar
MARCHE Claude committed
148 149
  let textbox = D.createTextarea d in
  textbox##rows <- 20; textbox##cols <- 100;
150 151 152 153 154 155 156 157 158 159
  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
160
        (fun (_ : D.mouseEvent Js.t) ->
161 162 163 164 165
          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
166 167
  let go = D.createButton ~name:(Js.string "go") d in
  go##textContent <- Js.some (Js.string "Go");
168 169 170
  Dom.appendChild body go;
  Dom.appendChild body (D.createBr d);
  (* then, the answer zone *)
MARCHE Claude's avatar
MARCHE Claude committed
171
  let preview = D.createDiv d in
172
  go##onclick <- D.handler (run textbox preview);
MARCHE Claude's avatar
MARCHE Claude committed
173 174 175 176 177 178
  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