trywhy3.ml 7.64 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 ``````"; "Simple Arithmetic"," theory T use import int.Int goal g: exists x:int. x*(x+1) = 42 `````` MARCHE Claude committed Sep 01, 2015 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 `````` MARCHE Claude committed Aug 30, 2015 55 56 ``````end "; `````` MARCHE Claude committed Aug 29, 2015 57 58 `````` ] `````` MARCHE Claude committed Aug 30, 2015 59 60 ``````(** registering the std lib *) `````` MARCHE Claude committed Sep 02, 2015 61 ``````(* `````` MARCHE Claude committed Aug 30, 2015 62 63 64 65 66 ``````let () = List.iter (fun (name,content) -> Sys_js.register_file ~name ~content; ) Theories.theories `````` MARCHE Claude committed Sep 02, 2015 67 ``````*) `````` MARCHE Claude committed Aug 30, 2015 68 `````` `````` MARCHE Claude committed Sep 01, 2015 69 `````` `````` MARCHE Claude committed Aug 29, 2015 70 71 ``````(** Rendering in the browser *) `````` MARCHE Claude committed Aug 29, 2015 72 73 ``````module D = Dom_html `````` MARCHE Claude committed Sep 01, 2015 74 75 ``````module Html = struct `````` MARCHE Claude committed Aug 29, 2015 76 77 78 79 ``````let d = D.document let node x = (x : #Dom.node Js.t :> Dom.node Js.t) `````` MARCHE Claude committed Sep 01, 2015 80 ``````let of_string s = node (d##createTextNode (Js.string s)) `````` MARCHE Claude committed Aug 29, 2015 81 `````` `````` MARCHE Claude committed Sep 01, 2015 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 committed Aug 29, 2015 86 `````` `````` MARCHE Claude committed Sep 01, 2015 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 committed Aug 29, 2015 98 99 `````` let temp_file_name = "/input.mlw" `````` MARCHE Claude committed Sep 02, 2015 100 ``````let why3_conf_file = "/why3.conf" `````` MARCHE Claude committed Aug 29, 2015 101 `````` `````` MARCHE Claude committed Aug 29, 2015 102 ``````let () = `````` MARCHE Claude committed Sep 02, 2015 103 `````` Sys_js.register_file ~name:temp_file_name ~content:"" `````` MARCHE Claude committed Aug 29, 2015 104 `````` `````` MARCHE Claude committed Aug 29, 2015 105 ``````open Why3 `````` MARCHE Claude committed Sep 02, 2015 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 committed Sep 01, 2015 146 `````` `````` MARCHE Claude committed Aug 30, 2015 147 ``````let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t = `````` MARCHE Claude committed Aug 29, 2015 148 `````` let text = Js.to_string (textbox##value) in `````` MARCHE Claude committed Aug 29, 2015 149 150 151 `````` let ch = open_out temp_file_name in output_string ch text; close_out ch; `````` MARCHE Claude committed Sep 01, 2015 152 `````` let answer = `````` MARCHE Claude committed Aug 29, 2015 153 `````` try `````` MARCHE Claude committed Sep 02, 2015 154 `````` (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *) `````` MARCHE Claude committed Sep 01, 2015 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 committed Sep 04, 2015 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 committed Sep 01, 2015 173 `````` let tl = Trans.apply split_trans t in `````` MARCHE Claude committed Sep 04, 2015 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 committed Sep 01, 2015 193 194 195 196 197 `````` in [ Html.of_string ("Theory " ^ thname); Html.ul tasks] :: acc) theories [] in `````` MARCHE Claude committed Sep 02, 2015 198 `````` Html.ul theories `````` MARCHE Claude committed Sep 01, 2015 199 ``````(* `````` MARCHE Claude committed Aug 30, 2015 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 committed Sep 01, 2015 213 ``````*) `````` MARCHE Claude committed Aug 29, 2015 214 215 216 `````` with | Loc.Located(loc,Parser.Error) -> let (_,l,b,e) = Loc.get loc in `````` MARCHE Claude committed Sep 01, 2015 217 218 219 `````` Html.par [Html.of_string (Pp.sprintf "syntax error line %d, columns %d-%d" l b e)] `````` MARCHE Claude committed Aug 29, 2015 220 221 `````` | Loc.Located(loc,e') -> let (_,l,b,e) = Loc.get loc in `````` MARCHE Claude committed Sep 01, 2015 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')] `````` MARCHE Claude committed Aug 29, 2015 227 `````` | e -> `````` MARCHE Claude committed Sep 01, 2015 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 committed Aug 29, 2015 238 239 240 `````` Js._false let onload (_event : #Dom_html.event Js.t) : bool Js.t = `````` MARCHE Claude committed Sep 01, 2015 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 committed Aug 29, 2015 246 `````` (fun () -> assert false) in `````` MARCHE Claude committed Aug 29, 2015 247 `````` (* first, the textbox *) `````` MARCHE Claude committed Sep 01, 2015 248 249 250 `````` let textbox = D.createTextarea Html.d in textbox##rows <- 32; textbox##cols <- 64; Dom.appendChild input textbox; `````` MARCHE Claude committed Aug 29, 2015 251 252 253 `````` (* second, the example buttons *) List.iter (fun (name,text) -> `````` MARCHE Claude committed Sep 01, 2015 254 `````` let b = D.createButton ~name:(Js.string name) Html.d in `````` MARCHE Claude committed Aug 29, 2015 255 `````` b##textContent <- Js.some (Js.string name); `````` MARCHE Claude committed Sep 01, 2015 256 `````` Dom.appendChild output b; `````` MARCHE Claude committed Aug 29, 2015 257 258 `````` b##onclick <- D.handler `````` MARCHE Claude committed Aug 30, 2015 259 `````` (fun (_ : D.mouseEvent Js.t) -> `````` MARCHE Claude committed Sep 02, 2015 260 `````` textbox##value <- Js.string text; `````` MARCHE Claude committed Aug 29, 2015 261 262 `````` Js._false)) examples; `````` MARCHE Claude committed Sep 01, 2015 263 `````` Dom.appendChild output (D.createBr Html.d); `````` MARCHE Claude committed Aug 29, 2015 264 `````` (* third, the go button *) `````` MARCHE Claude committed Sep 01, 2015 265 `````` let go = D.createButton ~name:(Js.string "go") Html.d in `````` MARCHE Claude committed Aug 29, 2015 266 `````` go##textContent <- Js.some (Js.string "Go"); `````` MARCHE Claude committed Sep 01, 2015 267 268 `````` Dom.appendChild output go; Dom.appendChild output (D.createBr Html.d); `````` MARCHE Claude committed Aug 29, 2015 269 `````` (* then, the answer zone *) `````` MARCHE Claude committed Sep 01, 2015 270 `````` let preview = D.createDiv Html.d in `````` MARCHE Claude committed Aug 29, 2015 271 `````` go##onclick <- D.handler (run textbox preview); `````` MARCHE Claude committed Aug 29, 2015 272 273 `````` preview##style##border <- Js.string "1px black"; preview##style##padding <- Js.string "5px"; `````` MARCHE Claude committed Sep 01, 2015 274 `````` Dom.appendChild output preview; `````` MARCHE Claude committed Aug 29, 2015 275 276 277 `````` Js._false let _ = D.window##onload <- D.handler onload `````` MARCHE Claude committed Sep 01, 2015 278 279 280 281 282 283 284 `````` (* Local Variables: compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js" End: *)``````