trywhy3.ml 4.68 KB
 MARCHE Claude committed Aug 29, 2015 1 `````` `````` MARCHE Claude committed Aug 29, 2015 2 3 4 `````` let examples = `````` MARCHE Claude committed Aug 30, 2015 5 6 `````` [ "Drinkers paradox"," theory T `````` MARCHE Claude committed Aug 29, 2015 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 `````` MARCHE Claude committed Aug 30, 2015 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 "; `````` MARCHE Claude committed Aug 29, 2015 29 30 `````` ] `````` MARCHE Claude committed Aug 30, 2015 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 `````` MARCHE Claude committed Aug 29, 2015 39 40 ``````(** Rendering in the browser *) `````` MARCHE Claude committed Aug 29, 2015 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))] `````` MARCHE Claude committed Aug 30, 2015 53 54 ``````let rec removeChildren p = Js.Opt.iter (p##lastChild) (fun c -> Dom.removeChild p c; removeChildren p) `````` MARCHE Claude committed Aug 29, 2015 55 56 57 `````` let temp_file_name = "/input.mlw" `````` MARCHE Claude committed Aug 29, 2015 58 59 60 ``````let () = Sys_js.register_file ~name:temp_file_name ~content:""; `````` MARCHE Claude committed Aug 29, 2015 61 62 ``````open Why3 `````` MARCHE Claude committed Aug 30, 2015 63 64 65 66 67 68 ``````(* TODO: loading from standard library. piste: utiliser Sys_js.register_autoload et XmlHttpRequest.get *) `````` MARCHE Claude committed Aug 30, 2015 69 ``````let env = Env.create_env ["/theories" ; "/modules"] `````` MARCHE Claude committed Aug 30, 2015 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 committed Aug 29, 2015 96 `````` let text = Js.to_string (textbox##value) in `````` MARCHE Claude committed Aug 29, 2015 97 98 99 `````` let ch = open_out temp_file_name in output_string ch text; close_out ch; `````` MARCHE Claude committed Aug 30, 2015 100 101 102 `````` let answer = ref [] in let push_answer s = answer := s :: !answer in begin `````` MARCHE Claude committed Aug 29, 2015 103 `````` try `````` MARCHE Claude committed Aug 30, 2015 104 `````` let x = Env.read_file Env.base_language env temp_file_name in `````` MARCHE Claude committed Aug 30, 2015 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 `````` MARCHE Claude committed Aug 29, 2015 122 123 124 `````` with | Loc.Located(loc,Parser.Error) -> let (_,l,b,e) = Loc.get loc in `````` MARCHE Claude committed Aug 30, 2015 125 126 `````` push_answer (Pp.sprintf "syntax error line %d, columns %d-%d" l b e) `````` MARCHE Claude committed Aug 29, 2015 127 128 `````` | Loc.Located(loc,e') -> let (_,l,b,e) = Loc.get loc in `````` MARCHE Claude committed Aug 30, 2015 129 130 131 `````` push_answer (Pp.sprintf "error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e') `````` MARCHE Claude committed Aug 29, 2015 132 `````` | e -> `````` MARCHE Claude committed Aug 30, 2015 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 committed Aug 29, 2015 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 `````` MARCHE Claude committed Aug 29, 2015 147 `````` (* first, the textbox *) `````` MARCHE Claude committed Aug 29, 2015 148 149 `````` let textbox = D.createTextarea d in textbox##rows <- 20; textbox##cols <- 100; `````` MARCHE Claude committed Aug 29, 2015 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 `````` MARCHE Claude committed Aug 30, 2015 160 `````` (fun (_ : D.mouseEvent Js.t) -> `````` MARCHE Claude committed Aug 29, 2015 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 committed Aug 29, 2015 166 167 `````` let go = D.createButton ~name:(Js.string "go") d in go##textContent <- Js.some (Js.string "Go"); `````` MARCHE Claude committed Aug 29, 2015 168 169 170 `````` Dom.appendChild body go; Dom.appendChild body (D.createBr d); (* then, the answer zone *) `````` MARCHE Claude committed Aug 29, 2015 171 `````` let preview = D.createDiv d in `````` MARCHE Claude committed Aug 29, 2015 172 `````` go##onclick <- D.handler (run textbox preview); `````` MARCHE Claude committed Aug 29, 2015 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``````