Commit 7747ddde authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: execution of main function in each module

parent 01c1e52a
......@@ -65,8 +65,8 @@ let do_input f =
exit 1
| Some d ->
try
printf "@[<hov 2>Execution of %s.%s ():@\n" mid name;
Mlw_interp.eval_global_symbol env m d;
printf "@[<hov 2>Execution of %s.%s ():@\n%a" mid name
(Mlw_interp.eval_global_symbol env m) d
with e when Debug.test_noflag Debug.stack_trace ->
printf "@\n@]@.";
raise e in
......
......@@ -156,8 +156,35 @@ let why3_execute (modules,_theories) =
Stdlib.Mstr.fold
(fun _k m acc ->
let th = m.Mlw_module.mod_theory in
let name = th.Theory.th_name.Ident.id_string in
[Html.of_string ("Module " ^ name)] :: acc)
let modname = th.Theory.th_name.Ident.id_string in
try
let ps =
Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
in
let moduleans = Html.of_string ("Module " ^ modname ^ ": ") in
let ans =
match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
| None ->
[moduleans;
Html.ul
[[Html.of_string "function main has no definition"]]]
| Some d ->
try
[moduleans;
Html.ul
[[Html.of_string
(Pp.sprintf "%a"
(Mlw_interp.eval_global_symbol env m) d)]]]
with e ->
[moduleans;
Html.ul
[[Html.of_string
(Pp.sprintf
"exception during execution of function main : %a (%s)"
Exn_printer.exn_printer e
(Printexc.to_string e))]]]
in ans :: acc
with Not_found -> acc)
modules []
in
Html.ul mods
......
......@@ -1373,7 +1373,7 @@ let eval_global_expr env mkm tkm _writes e =
let eval_global_symbol env m d =
let eval_global_symbol env m fmt d =
let lam = d.Mlw_expr.fun_lambda in
match lam.Mlw_expr.l_args with
| [pvs] when Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
......@@ -1382,7 +1382,7 @@ let eval_global_symbol env m d =
let eff = spec.Mlw_ty.c_effect in
let writes = eff.Mlw_ty.eff_writes in
let body = lam.Mlw_expr.l_expr in
printf "@[<hov 2> type:@ %a@]@."
fprintf fmt "@[<hov 2> type:@ %a@]@."
Mlw_pretty.print_vty body.Mlw_expr.e_vty;
(* printf "effect: %a@\n" *)
(* Mlw_pretty.print_effect body.Mlw_expr.e_effect; *)
......@@ -1393,26 +1393,26 @@ let eval_global_symbol env m d =
in
match res with
| Normal _ ->
printf "@[<hov 2> result:@ %a@\nglobals:@ %a@]@."
fprintf fmt "@[<hov 2> result:@ %a@\nglobals:@ %a@]@."
print_logic_result res print_vsenv final_env
(*
printf "@[<hov 2> result:@ %a@\nstate :@ %a@]@."
fprintf fmt "@[<hov 2> result:@ %a@\nstate :@ %a@]@."
(print_result m.Mlw_module.mod_known
m.Mlw_module.mod_theory.Theory.th_known st) res
print_state st
*)
| Excep _ ->
printf "@[<hov 2>exceptional result:@ %a@\nglobals:@ %a@]@."
fprintf fmt "@[<hov 2>exceptional result:@ %a@\nglobals:@ %a@]@."
print_logic_result res print_vsenv final_env;
(*
printf "@[<hov 2>exceptional result:@ %a@\nstate:@ %a@]@."
fprintf fmt "@[<hov 2>exceptional result:@ %a@\nstate:@ %a@]@."
(print_result m.Mlw_module.mod_known
m.Mlw_module.mod_theory.Theory.th_known st) res
print_state st;
*)
exit 1
| Irred _ | Fun _ ->
printf "@\n@]@.";
fprintf fmt "@\n@]@.";
eprintf "Execution error: %a@." print_logic_result res;
exit 2
end
......
......@@ -15,8 +15,8 @@ type value
val print_value: Format.formatter -> value -> unit
val eval_global_term:
val eval_global_term:
Env.env -> Decl.known_map -> Term.term -> value
val eval_global_symbol:
Env.env -> Mlw_module.modul -> Mlw_expr.fun_defn -> unit
Env.env -> Mlw_module.modul -> Format.formatter -> Mlw_expr.fun_defn -> unit
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