Commit 43047de3 authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: added example binary multiplication

parent 50beca0a
......@@ -1460,6 +1460,7 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
--file=try_alt_ergo.drv:/ \
--file=drinkers.why:/ \
--file=simplearith.why:/ \
--file=bin_mult.mlw:/ \
--file=isqrt.mlw:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
......
......@@ -103,10 +103,16 @@
<#en>Drinker's paradox</#en>
<#fr>Paradoxe des buveurs</#fr>
</div></a></li>
<!--
<li><a href="#"><div id="simplearith">
<#en>Simple Arithmetic</#en>
<#fr>Arithm&eacute;tique simple</#fr>
</div></a></li>
-->
<li><a href="#"><div id="bin_mult">
<#en>Binary Multiplication</#en>
<#fr>Multiplication en binaire</#fr>
</div></a></li>
<li><a href="#"><div id="isqrt">
<#en>Integral square root</#en>
<#fr>Racine carr&eacute;e enti&egrave;re</#fr>
......
......@@ -91,7 +91,7 @@ let run_alt_ergo_on_task t =
let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
match Why_typing.split_goals ltd with
| [d] ->
let d = Cnf.make (List.map (fun (f, env) -> f, true) d) in
let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
(*
SAT.reset_steps ();
List.iter
......@@ -182,33 +182,6 @@ let why3_execute (modules,_theories) =
in
Html.ul mods
(* from ../tools/why3execute.ml
let do_exec (mid,name) =
let m = try Mstr.find mid mm with Not_found ->
eprintf "Module '%s' not found.@." mid;
exit 1 in
let ps =
try Mlw_module.ns_find_ps m.Mlw_module.mod_export [name]
with Not_found ->
eprintf "Function '%s' not found in module '%s'.@." name mid;
exit 1 in
match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
| None ->
eprintf "Function '%s.%s' has no definition.@." mid name;
exit 1
| Some d ->
try
printf "@[<hov 2>Execution of %s.%s ():@\n" mid name;
Mlw_interp.eval_global_symbol env m d;
with e when Debug.test_noflag Debug.stack_trace ->
printf "@\n@]@.";
raise e in
Queue.iter do_exec opt_exec
*)
(*
Connecting why3 calls to the interface
......@@ -299,7 +272,8 @@ let add_file_example buttonname file =
let () =
add_file_example "drinkers" "/drinkers.why";
add_file_example "simplearith" "/simplearith.why";
(* add_file_example "simplearith" "/simplearith.why";*)
add_file_example "bin_mult" "/bin_mult.mlw";
add_file_example "isqrt" "/isqrt.mlw"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment