From 7747ddde8e61f4f709d1c1493129286a895c12fd Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Wed, 9 Sep 2015 21:56:07 +0200
Subject: [PATCH] Try Why3: execution of main function in each module

---
 src/tools/why3execute.ml |  4 ++--
 src/trywhy3/trywhy3.ml   | 31 +++++++++++++++++++++++++++++--
 src/whyml/mlw_interp.ml  | 14 +++++++-------
 src/whyml/mlw_interp.mli |  4 ++--
 4 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/src/tools/why3execute.ml b/src/tools/why3execute.ml
index 9430df140..d53eb9cc3 100644
--- a/src/tools/why3execute.ml
+++ b/src/tools/why3execute.ml
@@ -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
diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml
index 839d612e6..65b57202d 100644
--- a/src/trywhy3/trywhy3.ml
+++ b/src/trywhy3/trywhy3.ml
@@ -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
diff --git a/src/whyml/mlw_interp.ml b/src/whyml/mlw_interp.ml
index 911d37fe9..2c9b04a7d 100644
--- a/src/whyml/mlw_interp.ml
+++ b/src/whyml/mlw_interp.ml
@@ -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
diff --git a/src/whyml/mlw_interp.mli b/src/whyml/mlw_interp.mli
index 7e8b7c104..877b1084a 100644
--- a/src/whyml/mlw_interp.mli
+++ b/src/whyml/mlw_interp.mli
@@ -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
-- 
GitLab