Add an extract command to why3.

.gitignore

@@ -66,6 +66,9 @@ why3.conf
 /bin/why3doc.byte
 /bin/why3doc.opt
 /bin/why3doc
+/bin/why3extract.byte
+/bin/why3extract.opt
+/bin/why3extract
 /bin/why3prove.byte
 /bin/why3prove.opt
 /bin/why3prove

Makefile.in

@@ -481,7 +481,7 @@ clean::
 # Why3 commands
 ###############
 
-TOOLS_FILES = args why3prove why3realize
+TOOLS_FILES = args why3extract why3prove why3realize
 
 TOOLSMODULES = $(addprefix src/tools/, $(TOOLS_FILES))
 
@@ -492,8 +492,19 @@ TOOLSCMX = $(addsuffix .cmx, $(TOOLSMODULES))
 $(TOOLSDEP): DEPFLAGS += -I src/tools
 $(TOOLSCMO) $(TOOLSCMX): INCLUDES += -I src/tools
 
-byte: bin/why3prove.byte bin/why3realize.byte
-opt:  bin/why3prove.opt  bin/why3realize.opt
+byte: bin/why3extract.byte bin/why3prove.byte bin/why3realize.byte
+opt:  bin/why3extract.opt  bin/why3prove.opt  bin/why3realize.opt
+
+bin/why3extract.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3extract.cmx
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
+
+bin/why3extract.byte: lib/why3/why3.cma src/tools/args.cmo src/tools/why3extract.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
+
+bin/why3extract: bin/why3extract.@OCAMLBEST@
+	ln -sf why3extract.@OCAMLBEST@ $@
 
 bin/why3prove.opt: lib/why3/why3.cmxa src/tools/args.cmx src/tools/why3prove.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -518,13 +529,13 @@ bin/why3realize: bin/why3realize.@OCAMLBEST@
 	ln -sf why3realize.@OCAMLBEST@ $@
 
 clean_old_install::
-	rm -f $(TOOLDIR)/why3prove$(EXE)
+	rm -f  $(TOOLDIR)/why3extract$(EXE) $(TOOLDIR)/why3prove$(EXE) $(TOOLDIR)/why3realize$(EXE)
 
 install_no_local::
 	cp -f bin/why3prove.@OCAMLBEST@ $(TOOLDIR)/why3prove$(EXE)
 	cp -f bin/why3realize.@OCAMLBEST@ $(TOOLDIR)/why3realize$(EXE)
 
-install_local: bin/why3prove bin/why3realize
+install_local: bin/why3extract bin/why3prove bin/why3realize
 
 ifneq "$(MAKECMDGOALS)" "clean"
 include $(TOOLSDEP)
@@ -534,8 +545,10 @@ 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/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/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
 
@@ -1675,7 +1688,7 @@ test-runstrat: test-runstrat.$(OCAMLBEST)
 test-ocaml-extraction: bin/why3.opt lib/why3/why3extract.cmxa
 	@echo "driver ocaml32"
 	@mkdir -p tests/test-extraction
-	@cd tests ; ../bin/why3.opt -E ocaml32 \
+	@cd tests ; ../bin/why3extract.opt -D ocaml32 \
 	  test_extraction.mlw -o test-extraction
 	@cd tests/test-extraction/ ; \
 	  $(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \
@@ -1683,7 +1696,7 @@ test-ocaml-extraction: bin/why3.opt lib/why3/why3extract.cmxa
 	  ref__Refint.ml test_extraction__TestExtraction.ml main.ml
 	@tests/test-extraction/a.out
 	@echo "driver ocaml64"
-	@cd tests ; ../bin/why3.opt -E ocaml64 \
+	@cd tests ; ../bin/why3extract.opt -D ocaml64 \
 	  test_extraction.mlw -o test-extraction
 	@cd tests/test-extraction/ ; \
 	  $(OCAMLOPT) @BIGINTINCLUDE@ -I ../../lib/why3 \

src/tools/why3extract.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
+open Theory
+
+let usage_msg = sprintf
+  "Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
+  (Filename.basename Sys.argv.(0))
+
+let opt_queue = Queue.create ()
+
+let opt_input = ref None
+
+let add_opt_file x =
+  let tlist = Queue.create () in
+  Queue.push (Some x, tlist) opt_queue;
+  opt_input := Some tlist
+
+let add_opt_theory =
+  let rdot = (Str.regexp "\\.") in fun x ->
+  let l = Str.split rdot x in
+  let p, t = match List.rev l with
+    | t::p -> List.rev p, t
+    | _ -> assert false
+  in
+  match !opt_input, p with
+  | None, [] ->
+      eprintf "Option '-T'/'--theory' with a non-qualified \
+        argument requires an input file.@.";
+      exit 1
+  | Some tlist, [] ->
+      Queue.push (x, p, t) tlist
+  | _ ->
+      let tlist = Queue.create () in
+      Queue.push (None, tlist) opt_queue;
+      opt_input := None;
+      Queue.push (x, p, t) tlist
+
+let opt_parser = ref None
+let opt_driver = ref None
+let opt_output = ref None
+
+let option_list = [
+  "-", Arg.Unit (fun () -> add_opt_file "-"),
+      " Read the input file from stdin";
+  "-T", Arg.String add_opt_theory,
+      "<theory> Select <theory> in the input file or in the library";
+  "--theory", Arg.String add_opt_theory,
+      " same as -T";
+  "-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";
+  "-D", Arg.String (fun s -> opt_driver := Some s),
+      "<file> Specify a driver";
+  "--driver", Arg.String (fun s -> opt_driver := Some s),
+      " same as -D";
+  "-o", Arg.String (fun s -> opt_output := Some s),
+      "<dir> Print the selected goals to separate files in <dir>";
+  "--output", Arg.String (fun s -> opt_output := Some s),
+      " same as -o" ]
+
+let (env, config) =
+  Args.initialize option_list add_opt_file usage_msg
+
+let () =
+  if Queue.is_empty opt_queue then begin
+    Arg.usage option_list usage_msg;
+    exit 1
+  end
+
+let opt_output =
+  match !opt_output with
+  | None ->
+    eprintf "Output directory (-o) is required.@.";
+    exit 1
+  | Some d -> d
+
+let opt_driver =
+  match !opt_driver with
+  | None ->
+    eprintf "Driver (-D) is required.@.";
+    exit 1
+  | Some s ->
+    let s =
+      if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
+      else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv")) in
+    let lib = Mlw_main.library_of_env env in
+    Mlw_driver.load_driver lib s []
+
+let extract_to ?fname th extract =
+  let file = Filename.concat opt_output (Mlw_ocaml.extract_filename ?fname th) in
+  let old =
+    if Sys.file_exists file then begin
+      let backup = file ^ ".bak" in
+      Sys.rename file backup;
+      Some (open_in backup)
+    end else None in
+  let cout = open_out file in
+  extract file ?old (formatter_of_out_channel cout);
+  close_out cout
+
+let extract_to =
+  let visited = Ident.Hid.create 17 in
+  fun ?fname th extract ->
+    if not (Ident.Hid.mem visited th.th_name) then begin
+      Ident.Hid.add visited th.th_name ();
+      extract_to ?fname th extract
+    end
+
+let use_iter f th =
+  List.iter (fun d -> match d.td_node with Use t -> f t | _ -> ()) th.th_decls
+
+let rec do_extract_theory ?fname th =
+  let extract file ?old fmt = ignore (old);
+    let tname = th.th_name.Ident.id_string in
+    Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
+    Mlw_ocaml.extract_theory opt_driver ?old ?fname fmt th
+  in
+  extract_to ?fname th extract;
+  let extract_use th' =
+    let fname = if th'.th_path = [] then fname else None in
+    do_extract_theory ?fname th' in
+  use_iter extract_use th
+
+let rec do_extract_module ?fname m =
+  let extract file ?old fmt = ignore (old);
+    let tname = m.Mlw_module.mod_theory.th_name.Ident.id_string in
+    Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
+    Mlw_ocaml.extract_module opt_driver ?old ?fname fmt m
+  in
+  extract_to ?fname m.Mlw_module.mod_theory extract;
+  let extract_use th' =
+    let fname = if th'.th_path = [] then fname else None in
+    match
+      try Some (Mlw_module.restore_module th') with Not_found -> None
+    with
+      | Some m' -> do_extract_module ?fname m'
+      | None    -> do_extract_theory ?fname th' in
+  use_iter extract_use m.Mlw_module.mod_theory
+
+let do_global_extract (tname,p,t) =
+  let lib = opt_driver.Mlw_driver.drv_lib in
+  try
+    let mm, thm = Env.read_lib_file lib p in
+    try
+      let m = Mstr.find t mm in
+      do_extract_module m
+    with Not_found ->
+      let th = Mstr.find t thm in
+      do_extract_theory th
+  with Env.LibFileNotFound _ | Not_found -> try
+    let format = Opt.get_def "why" !opt_parser in
+    let env = Env.env_of_library lib in
+    let th = Env.read_theory ~format env p t in
+    do_extract_theory th
+  with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
+    eprintf "Theory/module '%s' not found.@." tname;
+    exit 1
+
+let do_extract_theory_from fname m (tname,_,t) =
+  let th = try Mstr.find t m with Not_found ->
+    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
+    exit 1
+  in
+  do_extract_theory ~fname th
+
+let do_extract_module_from fname mm thm (tname,_,t) =
+  try
+    let m = Mstr.find t mm in do_extract_module ~fname m
+  with Not_found -> try
+    let th = Mstr.find t thm in do_extract_theory ~fname th
+  with Not_found ->
+    eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
+    exit 1
+
+let do_local_extract fname cin tlist =
+  let lib = opt_driver.Mlw_driver.drv_lib in
+  if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then begin
+    let mm, thm = Mlw_main.read_channel lib [] fname cin in
+    if Queue.is_empty tlist then begin
+      let do_m t m thm =
+        do_extract_module ~fname m; Mstr.remove t thm in
+      let thm = Mstr.fold do_m mm thm in
+      Mstr.iter (fun _ th -> do_extract_theory ~fname th) thm
+    end else
+      Queue.iter (do_extract_module_from fname mm thm) tlist
+  end else begin
+    let m = Env.read_channel ?format:!opt_parser env fname cin in
+    if Queue.is_empty tlist then
+      let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
+      let do_th _ (_,th) = do_extract_theory ~fname th in
+      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
+    else
+      Queue.iter (do_extract_theory_from fname m) tlist
+  end
+
+let do_input = function
+  | None, tlist ->
+    Queue.iter do_global_extract tlist
+  | Some f, tlist ->
+    let fname, cin = match f with
+      | "-" -> "stdin", stdin
+      | f   -> f, open_in f in
+    do_local_extract fname cin tlist;
+    close_in cin
+
+let () =
+  try
+    Queue.iter do_input opt_queue;
+  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:
+*)