Add a why3execute command.

.gitignore

@@ -69,6 +69,9 @@ why3.conf
 /bin/why3extract.byte
 /bin/why3extract.opt
 /bin/why3extract
+/bin/why3execute.byte
+/bin/why3execute.opt
+/bin/why3execute
 /bin/why3prove.byte
 /bin/why3prove.opt
 /bin/why3prove

Makefile.in

@@ -481,7 +481,8 @@ clean::
 # Why3 commands
 ###############
 
-TOOLS_FILES = args why3extract why3prove why3realize
+TOOLS_BIN = why3execute why3extract why3prove why3realize
+TOOLS_FILES = args $(TOOLS_BIN)
 
 TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
 
@@ -492,8 +493,19 @@ TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
 $(TOOLSDEP): DEPFLAGS += -I src/tools
 $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
 
-byte: bin/why3extract.byte bin/why3prove.byte bin/why3realize.byte
-opt:  bin/why3extract.opt  bin/why3prove.opt  bin/why3realize.opt
+byte: $(TOOLS_BIN:%=bin/%.byte)
+opt:  $(TOOLS_BIN:%=bin/%.opt)
+
+bin/why3execute.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3execute.cmx
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
+
+bin/why3execute.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3execute.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
+
+bin/why3execute: bin/why3execute.@OCAMLBEST@
+	ln -sf why3execute.@OCAMLBEST@ $@
 
 bin/why3extract.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3extract.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -529,13 +541,15 @@ bin/why3realize: bin/why3realize.@OCAMLBEST@
 	ln -sf why3realize.@OCAMLBEST@ $@
 
 clean_old_install::
-	rm -f  $(TOOLDIR)/why3extract$(EXE) $(TOOLDIR)/why3prove$(EXE) $(TOOLDIR)/why3realize$(EXE)
+	rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE))
 
 install_no_local::
-	cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
+	cp -f bin/why3execute.@OCAMLBEST@ $(TOOLDIR)/why3execute$(EXE)
+	cp -f bin/why3extract.@OCAMLBEST@ $(TOOLDIR)/why3extract$(EXE)
+	cp -f bin/why3prove.@OCAMLBEST@   $(TOOLDIR)/why3prove$(EXE)
 	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
 
-install_local: bin/why3extract bin/why3prove bin/why3realize
+install_local: $(addprefix bin/,$(TOOLS_BIN))
 
 ifneq "$(MAKECMDGOALS)" "clean"
 include $(TOOLSDEP)
@@ -545,9 +559,11 @@ depend: $(TOOLSDEP)
 
 clean::
 	rm -f src/tools/args.cm[iox] src/tools/args.annot src/tools/args.o src/tools/args.dep
+	rm -f src/tools/why3execute.cm[iox] src/tools/why3execute.annot src/tools/why3execute.o src/tools/why3execute.dep
 	rm -f src/tools/why3extract.cm[iox] src/tools/why3extract.annot src/tools/why3extract.o src/tools/why3extract.dep
 	rm -f src/tools/why3prove.cm[iox] src/tools/why3prove.annot src/tools/why3prove.o src/tools/why3prove.dep
 	rm -f src/tools/why3realize.cm[iox] src/tools/why3realize.annot src/tools/why3realize.o src/tools/why3realize.dep
+	rm -f bin/why3execute.byte bin/why3execute.opt bin/why3execute
 	rm -f bin/why3extract.byte bin/why3extract.opt bin/why3extract
 	rm -f bin/why3prove.byte bin/why3prove.opt bin/why3prove
 	rm -f bin/why3realize.byte bin/why3realize.opt bin/why3realize

bench/bench

@@ -88,12 +88,12 @@ invalid_goals () {
 execute () {
     pgm="bin/why3execute$suffix"
     echo -n "$1 $2... "
-    if $pgm $1 --exec $2 > /dev/null 2>&1; then
+    if $pgm $1 $2 > /dev/null 2>&1; then
         echo "ok"
     else
         echo "execution test failed!"
-        echo $pgm $1 --exec $2
-        $pgm $1 --exec $2
+        echo $pgm $1 $2
+        $pgm $1 $2
         exit 1
     fi
 }

src/tools/why3execute.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+open Format
+open Why3
+open Stdlib
+
+let usage_msg = sprintf
+  "Usage: %s [options] file module.ident..."
+  (Filename.basename Sys.argv.(0))
+
+let opt_file = ref None
+let opt_exec = Queue.create ()
+
+let add_opt =
+  let rdot = Str.regexp "\\." in fun x ->
+  if !opt_file = None then opt_file := Some x else
+  match Str.split rdot x with
+  | [m;i] -> Queue.push (m,i) opt_exec
+  | _ ->
+    Format.eprintf "extra arguments must be of the form 'module.ident'@.";
+    exit 1
+
+let opt_parser = ref None
+
+let option_list = [
+  "-F", Arg.String (fun s -> opt_parser := Some s),
+      "<format> Select input format (default: \"why\")";
+  "--format", Arg.String (fun s -> opt_parser := Some s),
+      " same as -F" ]
+
+let (env, config) =
+  Args.initialize option_list add_opt usage_msg
+
+let () =
+  if !opt_file = None then begin
+    Arg.usage option_list usage_msg;
+    exit 1
+  end
+
+let do_input f =
+  let fname, cin =
+    match f with
+    | "-" -> "stdin", stdin
+    | f   -> f, open_in f in
+  if not (!opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw") then
+    begin
+      eprintf "Execution is available only for mlw files@.";
+      exit 1
+    end;
+  let lib = Mlw_main.library_of_env env in
+  let mm, _thm = Mlw_main.read_channel lib [] fname cin in
+  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
+
+let () =
+  try
+    Opt.iter do_input !opt_file
+  with e when not (Debug.test_flag Debug.stack_trace) ->
+    eprintf "%a@." Exn_printer.exn_printer e;
+    exit 1
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. byte"
+End:
+*)